diff git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index c6e5a6e..4024098 100644
 a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ 1,2546 +1,2533 @@
{# LANGUAGE CPP #}
module TcSimplify(
simplifyInfer, InferMode(..),
growThetaTyVars,
simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyTopImplic, captureTopConstraints,
simplifyInteractive,
solveEqualities, solveLocalEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
simpl_top,
promoteTyVar,
promoteTyVarSet,
 For Rules we need these
solveWanteds, solveWantedsAndDrop,
approximateWC, runTcSDeriveds
) where
#include "HsVersions.h"
import GhcPrelude
import Bag
import Class ( Class, classKey, classTyCon )
import DynFlags ( WarningFlag ( Opt_WarnMonomorphism )
, WarnReason ( Reason )
, DynFlags( solverIterations ) )
import Id ( idType )
import Inst
import ListSetOps
import Name
import Outputable
import PrelInfo
import PrelNames
import TcErrors
import TcEvidence
import TcInteract
import TcCanonical ( makeSuperClasses, solveCallStack )
import TcMType as TcM
import TcRnMonad as TcM
import TcSMonad as TcS
import TcType
import TrieMap ()  DV: for now
import Type
import TysWiredIn ( liftedRepTy )
import Unify ( tcMatchTyKi )
import Util
import Var
import VarSet
import UniqSet
import BasicTypes ( IntWithInf, intGtLimit )
import ErrUtils ( emptyMessages )
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Data.Foldable ( toList )
import Data.List ( partition )
import Data.List.NonEmpty ( NonEmpty(..) )
import Maybes ( isJust )
{
*********************************************************************************
* *
* External interface *
* *
*********************************************************************************
}
captureTopConstraints :: TcM a > TcM (a, WantedConstraints)
 (captureTopConstraints m) runs m, and returns the type constraints it
 generates plus the constraints produced by static forms inside.
 If it fails with an exception, it reports any insolubles
 (out of scope variables) before doing so
captureTopConstraints thing_inside
= do { static_wc_var < TcM.newTcRef emptyWC ;
; (mb_res, lie) < TcM.updGblEnv (\env > env { tcg_static_wc = static_wc_var } ) $
TcM.tryCaptureConstraints thing_inside
; stWC < TcM.readTcRef static_wc_var
 See TcRnMonad Note [Constraints and errors]
 If the thing_inside threw an exception, but generated some insoluble
 constraints, report the latter before propagating the exception
 Otherwise they will be lost altogether
; case mb_res of
Right res > return (res, lie `andWC` stWC)
Left {} > do { _ < reportUnsolved lie; failM } }
 This call to reportUnsolved is the reason
 this function is here instead of TcRnMonad
simplifyTopImplic :: Bag Implication > TcM ()
simplifyTopImplic implics
= do { empty_binds < simplifyTop (mkImplicWC implics)
 Since all the inputs are implications the returned bindings will be empty
; MASSERT2( isEmptyBag empty_binds, ppr empty_binds )
; return () }
simplifyTop :: WantedConstraints > TcM (Bag EvBind)
 Simplify toplevel constraints
 Usually these will be implications,
 but when there is nothing to quantify we don't wrap
 in a degenerate implication, so we do that here instead
simplifyTop wanteds
= do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
; ((final_wc, unsafe_ol), binds1) < runTcS $
do { final_wc < simpl_top wanteds
; unsafe_ol < getSafeOverlapFailures
; return (final_wc, unsafe_ol) }
; traceTc "End simplifyTop }" empty
; traceTc "reportUnsolved {" empty
; binds2 < reportUnsolved final_wc
; traceTc "reportUnsolved }" empty
; traceTc "reportUnsolved (unsafe overlapping) {" empty
; unless (isEmptyCts unsafe_ol) $ do {
 grab current error messages and clear, warnAllUnsolved will
 update error messages which we'll grab and then restore saved
 messages.
; errs_var < getErrsVar
; saved_msg < TcM.readTcRef errs_var
; TcM.writeTcRef errs_var emptyMessages
; warnAllUnsolved $ WC { wc_simple = unsafe_ol
, wc_impl = emptyBag }
; whyUnsafe < fst <$> TcM.readTcRef errs_var
; TcM.writeTcRef errs_var saved_msg
; recordUnsafeInfer whyUnsafe
}
; traceTc "reportUnsolved (unsafe overlapping) }" empty
; return (evBindMapBinds binds1 `unionBags` binds2) }
  Typecheck a thing that emits only equality constraints, solving any
 constraints we can and reemitting constraints that we can't. The thing_inside
 should generally bump the TcLevel to make sure that this run of the solver
 doesn't affect anything lying around.
solveLocalEqualities :: TcM a > TcM a
solveLocalEqualities thing_inside
= do { traceTc "solveLocalEqualities {" empty
; (result, wanted) < captureConstraints thing_inside
; traceTc "solveLocalEqualities: running solver {" (ppr wanted)
; reduced_wanted < runTcSEqualities (solveWanteds wanted)
; traceTc "solveLocalEqualities: running solver }" (ppr reduced_wanted)
; emitConstraints reduced_wanted
; traceTc "solveLocalEqualities end }" empty
; return result }
  Typecheck a thing that emits only equality constraints, then
 solve those constraints. Fails outright if there is trouble.
 Use this if you're not going to get another crack at solving
 (because, e.g., you're checking a datatype declaration)
solveEqualities :: TcM a > TcM a
solveEqualities thing_inside
= checkNoErrs $  See Note [Fail fast on kind errors]
do { (result, wanted) < captureConstraints thing_inside
; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
; final_wc < runTcSEqualities $ simpl_top wanted
 NB: Use simpl_top here so that we potentially default RuntimeRep
 vars to LiftedRep. This is needed to avoid #14991.
; traceTc "End solveEqualities }" empty
; traceTc "reportAllUnsolved {" empty
; reportAllUnsolved final_wc
; traceTc "reportAllUnsolved }" empty
; return result }
  Simplify toplevel constraints, but without reporting any unsolved
 constraints nor unsafe overlapping.
simpl_top :: WantedConstraints > TcS WantedConstraints
 See Note [Toplevel Defaulting Plan]
simpl_top wanteds
= do { wc_first_go < nestTcS (solveWantedsAndDrop wanteds)
 This is where the main work happens
; try_tyvar_defaulting wc_first_go }
where
try_tyvar_defaulting :: WantedConstraints > TcS WantedConstraints
try_tyvar_defaulting wc
 isEmptyWC wc
= return wc
 otherwise
= do { free_tvs < TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
 zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
 filter isMetaTyVar: we might have runtimeskolems in GHCi,
 and we definitely don't want to try to assign to those!
 The isTyVar is needed to weed out coercion variables
; defaulted < mapM defaultTyVarTcS meta_tvs  Has unification side effects
; if or defaulted
then do { wc_residual < nestTcS (solveWanteds wc)
 See Note [Must simplify after defaulting]
; try_class_defaulting wc_residual }
else try_class_defaulting wc }  No defaulting took place
try_class_defaulting :: WantedConstraints > TcS WantedConstraints
try_class_defaulting wc
 isEmptyWC wc
= return wc
 otherwise  See Note [When to do typeclass defaulting]
= do { something_happened < applyDefaultingRules wc
 See Note [Toplevel Defaulting Plan]
; if something_happened
then do { wc_residual < nestTcS (solveWantedsAndDrop wc)
; try_class_defaulting wc_residual }
 See Note [Overview of implicit CallStacks] in TcEvidence
else try_callstack_defaulting wc }
try_callstack_defaulting :: WantedConstraints > TcS WantedConstraints
try_callstack_defaulting wc
 isEmptyWC wc
= return wc
 otherwise
= defaultCallStacks wc
  Default any remaining @CallStack@ constraints to empty @CallStack@s.
defaultCallStacks :: WantedConstraints > TcS WantedConstraints
 See Note [Overview of implicit CallStacks] in TcEvidence
defaultCallStacks wanteds
= do simples < handle_simples (wc_simple wanteds)
mb_implics < mapBagM handle_implic (wc_impl wanteds)
return (wanteds { wc_simple = simples
, wc_impl = catBagMaybes mb_implics })
where
handle_simples simples
= catBagMaybes <$> mapBagM defaultCallStack simples
handle_implic :: Implication > TcS (Maybe Implication)
 The Maybe is because solving the CallStack constraint
 may well allow us to discard the implication entirely
handle_implic implic
 isSolvedStatus (ic_status implic)
= return (Just implic)
 otherwise
= do { wanteds < setEvBindsTcS (ic_binds implic) $
 defaultCallStack sets a binding, so
 we must set the correct binding group
defaultCallStacks (ic_wanted implic)
; setImplicationStatus (implic { ic_wanted = wanteds }) }
defaultCallStack ct
 ClassPred cls tys < classifyPredType (ctPred ct)
, Just {} < isCallStackPred cls tys
= do { solveCallStack (ctEvidence ct) EvCsEmpty
; return Nothing }
defaultCallStack ct
= return (Just ct)
{ Note [Fail fast on kind errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solveEqualities is used to solve kind equalities when kindchecking
userwritten types. If solving fails we should fail outright, rather
than just accumulate an error message, for two reasons:
* A kindbogus type signature may cause a cascade of knockon
errors if we let it pass
* More seriously, we don't have a convenient termlevel place to add
deferred bindings for unsolved kindequality constraints, so we
don't build evidence bindings (by usine reportAllUnsolved). That
means that we'll be left with with a type that has coercion holes
in it, something like
> cohole
where cohole is not filled in. Eeek! That unfilledin
hole actually causes GHC to crash with "fvProv falls into a hole"
See Trac #11563, #11520, #11516, #11399
So it's important to use 'checkNoErrs' here!
Note [When to do typeclass defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In GHC 7.6 and 7.8.2, we did typeclass defaulting only if insolubleWC
was false, on the grounds that defaulting can't help solve insoluble
constraints. But if we *don't* do defaulting we may report a whole
lot of errors that would be solved by defaulting; these errors are
quite spurious because fixing the single insoluble error means that
defaulting happens again, which makes all the other errors go away.
This is jolly confusing: Trac #9033.
So it seems better to always do typeclass defaulting.
However, always doing defaulting does mean that we'll do it in
situations like this (Trac #5934):
run :: (forall s. GenST s) > Int
run = fromInteger 0
We don't unify the return type of fromInteger with the given function
type, because the latter involves foralls. So we're left with
(Num alpha, alpha ~ (forall s. GenST s) > Int)
Now we do defaulting, get alpha := Integer, and report that we can't
match Integer with (forall s. GenST s) > Int. That's not totally
stupid, but perhaps a little strange.
Another potential alternative would be to suppress *all* noninsoluble
errors if there are *any* insoluble errors, anywhere, but that seems
too drastic.
Note [Must simplify after defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We may have a deeply buried constraint
(t:*) ~ (a:Open)
which we couldn't solve because of the kind incompatibility, and 'a' is free.
Then when we default 'a' we can solve the constraint. And we want to do
that before starting in on type classes. We MUST do it before reporting
errors, because it isn't an error! Trac #7967 was due to this.
Note [Toplevel Defaulting Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We have considered two design choices for where/when to apply defaulting.
(i) Do it in SimplCheck mode only /whenever/ you try to solve some
simple constraints, maybe deep inside the context of implications.
This used to be the case in GHC 7.4.1.
(ii) Do it in a tight loop at simplifyTop, once all other constraints have
finished. This is the current story.
Option (i) had many disadvantages:
a) Firstly, it was deep inside the actual solver.
b) Secondly, it was dependent on the context (Infer a type signature,
or Check a type signature, or Interactive) since we did not want
to always start defaulting when inferring (though there is an exception to
this, see Note [Default while Inferring]).
c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
f :: Int > Bool
f x = const True (\y > let w :: a > a
w a = const a (y+1)
in w y)
We will get an implication constraint (for beta the type of y):
[untch=beta] forall a. 0 => Num beta
which we really cannot default /while solving/ the implication, since beta is
untouchable.
Instead our new defaulting story is to pull defaulting out of the solver loop and
go with option (ii), implemented at SimplifyTop. Namely:
 First, have a go at solving the residual constraint of the whole
program
 Try to approximate it with a simple constraint
 Figure out derived defaulting equations for that simple constraint
 Go round the loop again if you did manage to get some equations
Now, that has to do with class defaulting. However there exists type variable /kind/
defaulting. Again this is done at the toplevel and the plan is:
 At the toplevel, once you had a go at solving the constraint, do
figure out /all/ the touchable unification variables of the wanted constraints.
 Apply defaulting to their kinds
More details in Note [DefaultTyVar].
Note [Safe Haskell Overlapping Instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Safe Haskell, we apply an extra restriction to overlapping instances. The
motive is to prevent untrusted code provided by a thirdparty, changing the
behavior of trusted code through typeclasses. This is due to the global and
implicit nature of typeclasses that can hide the source of the dictionary.
Another way to state this is: if a module M compiles without importing another
module N, changing M to import N shouldn't change the behavior of M.
Overlapping instances with typeclasses can violate this principle. However,
overlapping instances aren't always unsafe. They are just unsafe when the most
selected dictionary comes from untrusted code (code compiled with XSafe) and
overlaps instances provided by other modules.
In particular, in Safe Haskell at a call site with overlapping instances, we
apply the following rule to determine if it is a 'unsafe' overlap:
1) Most specific instance, I1, defined in an `XSafe` compiled module.
2) I1 is an orphan instance or a MPTC.
3) At least one overlapped instance, Ix, is both:
A) from a different module than I1
B) Ix is not marked `OVERLAPPABLE`
This is a slightly involved heuristic, but captures the situation of an
imported module N changing the behavior of existing code. For example, if
condition (2) isn't violated, then the module author M must depend either on a
typeclass or type defined in N.
Secondly, when should these heuristics be enforced? We enforced them when the
typeclass method call site is in a module marked `XSafe` or `XTrustworthy`.
This allows `XUnsafe` modules to operate without restriction, and for Safe
Haskell inferrence to infer modules with unsafe overlaps as unsafe.
One alternative design would be to also consider if an instance was imported as
a `safe` import or not and only apply the restriction to instances imported
safely. However, since instances are global and can be imported through more
than one path, this alternative doesn't work.
Note [Safe Haskell Overlapping Instances Implementation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
How is this implemented? It's complicated! So we'll step through it all:
1) `InstEnv.lookupInstEnv`  Performs instance resolution, so this is where
we check if a particular typeclass method call is safe or unsafe. We do this
through the return type, `ClsInstLookupResult`, where the last parameter is a
list of instances that are unsafe to overlap. When the method call is safe,
the list is null.
2) `TcInteract.matchClassInst`  This module drives the instance resolution
/ dictionary generation. The return type is `LookupInstResult`, which either
says no instance matched, or one found, and if it was a safe or unsafe
overlap.
3) `TcInteract.doTopReactDict`  Takes a dictionary / class constraint and
tries to resolve it by calling (in part) `matchClassInst`. The resolving
mechanism has a work list (of constraints) that it process one at a time. If
the constraint can't be resolved, it's added to an inert set. When compiling
an `XSafe` or `XTrustworthy` module, we follow this approach as we know
compilation should fail. These are handled as normal constraint resolution
failures from hereon (see step 6).
Otherwise, we may be inferring safety (or using `Wunsafe`), and
compilation should succeed, but print warnings and/or mark the compiled module
as `XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
the unsafe (but resolved!) constraint to the `inert_safehask` field of
`InertCans`.
4) `TcSimplify.simplifyTop`:
* Call simpl_top, the toplevel function for driving the simplifier for
constraint resolution.
* Once finished, call `getSafeOverlapFailures` to retrieve the
list of overlapping instances that were successfully resolved,
but unsafe. Remember, this is only applicable for generating warnings
(`Wunsafe`) or inferring a module unsafe. `XSafe` and `XTrustworthy`
cause compilation failure by not resolving the unsafe constraint at all.
* For unresolved constraints (all types), call `TcErrors.reportUnsolved`,
while for resolved but unsafe overlapping dictionary constraints, call
`TcErrors.warnAllUnsolved`. Both functions convert constraints into a
warning message for the user.
* In the case of `warnAllUnsolved` for resolved, but unsafe
dictionary constraints, we collect the generated warning
message (pop it) and call `TcRnMonad.recordUnsafeInfer` to
mark the module we are compiling as unsafe, passing the
warning message along as the reason.
5) `TcErrors.*Unsolved`  Generates error messages for constraints by
actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
know is the constraint that is unresolved or unsafe. For dictionary, all we
know is that we need a dictionary of type C, but not what instances are
available and how they overlap. So we once again call `lookupInstEnv` to
figure that out so we can generate a helpful error message.
6) `TcRnMonad.recordUnsafeInfer`  Save the unsafe result and reason in an
IORef called `tcg_safeInfer`.
7) `HscMain.tcRnModule'`  Reads `tcg_safeInfer` after typechecking, calling
`HscMain.markUnsafeInfer` (passing the reason along) when safeinferrence
failed.
Note [No defaulting in the ambiguity check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When simplifying constraints for the ambiguity check, we use
solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
Trac #11947 was an example:
f :: Num a => Int > Int
This is ambiguous of course, but we don't want to default the
(Num alpha) constraint to (Num Int)! Doing so gives a defaulting
warning, but no error.
}

simplifyAmbiguityCheck :: Type > WantedConstraints > TcM ()
simplifyAmbiguityCheck ty wanteds
= do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
; (final_wc, _) < runTcS $ solveWantedsAndDrop wanteds
 NB: no defaulting! See Note [No defaulting in the ambiguity check]
; traceTc "End simplifyAmbiguityCheck }" empty
 Normally report all errors; but with XAllowAmbiguousTypes
 report only insoluble ones, since they represent genuinely
 inaccessible code
; allow_ambiguous < xoptM LangExt.AllowAmbiguousTypes
; traceTc "reportUnsolved(ambig) {" empty
; unless (allow_ambiguous && not (insolubleWC final_wc))
(discardResult (reportUnsolved final_wc))
; traceTc "reportUnsolved(ambig) }" empty
; return () }

simplifyInteractive :: WantedConstraints > TcM (Bag EvBind)
simplifyInteractive wanteds
= traceTc "simplifyInteractive" empty >>
simplifyTop wanteds

simplifyDefault :: ThetaType  Wanted; has no type variables in it
> TcM ()  Succeeds if the constraint is soluble
simplifyDefault theta
= do { traceTc "simplifyDefault" empty
; wanteds < newWanteds DefaultOrigin theta
; unsolved < runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
; traceTc "reportUnsolved {" empty
; reportAllUnsolved unsolved
; traceTc "reportUnsolved }" empty
; return () }

tcCheckSatisfiability :: Bag EvVar > TcM Bool
 Return True if satisfiable, False if definitely contradictory
tcCheckSatisfiability given_ids
= do { lcl_env < TcM.getLclEnv
; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
; (res, _ev_binds) < runTcS $
do { traceTcS "checkSatisfiability {" (ppr given_ids)
; let given_cts = mkGivens given_loc (bagToList given_ids)
 See Note [Superclasses and satisfiability]
; solveSimpleGivens given_cts
; insols < getInertInsols
; insols < try_harder insols
; traceTcS "checkSatisfiability }" (ppr insols)
; return (isEmptyBag insols) }
; return res }
where
try_harder :: Cts > TcS Cts
 Maybe we have to search up the superclass chain to find
 an unsatisfiable constraint. Example: pmcheck/T3927b.
 At the moment we try just once
try_harder insols
 not (isEmptyBag insols)  We've found that it's definitely unsatisfiable
= return insols  Hurrah  stop now.
 otherwise
= do { pending_given < getPendingGivenScs
; new_given < makeSuperClasses pending_given
; solveSimpleGivens new_given
; getInertInsols }
{ Note [Superclasses and satisfiability]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand superclasses before starting, because (Int ~ Bool), has
(Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
as a superclass, and it's the latter that is insoluble. See
Note [The equality types story] in TysPrim.
If we fail to prove unsatisfiability we (arbitrarily) try just once to
find superclasses, using try_harder. Reason: we might have a type
signature
f :: F op (Implements push) => ..
where F is a type function. This happened in Trac #3972.
We could do more than once but we'd have to have /some/ limit: in the
the recursive case, we would go on forever in the common case where
the constraints /are/ satisfiable (Trac #10592 comment:12!).
For stratightforard situations without type functions the try_harder
step does nothing.
***********************************************************************************
* *
* Inference
* *
***********************************************************************************
Note [Inferring the type of a letbound variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f x = rhs
To infer f's type we do the following:
* Gather the constraints for the RHS with ambient level *one more than*
the current one. This is done by the call
pushLevelAndCaptureConstraints (tcMonoBinds...)
in TcBinds.tcPolyInfer
* Call simplifyInfer to simplify the constraints and decide what to
quantify over. We pass in the level used for the RHS constraints,
here called rhs_tclvl.
This ensures that the implication constraint we generate, if any,
has a strictlyincreased level compared to the ambient level outside
the let binding.
}
  How should we choose which constraints to quantify over?
data InferMode = ApplyMR  ^ Apply the monomorphism restriction,
 never quantifying over any constraints
 EagerDefaulting  ^ See Note [TcRnExprMode] in TcRnDriver,
 the :type +d case; this mode refuses
 to quantify over any defaultable constraint
 NoRestrictions  ^ Quantify over any constraint that
 satisfies TcType.pickQuantifiablePreds
instance Outputable InferMode where
ppr ApplyMR = text "ApplyMR"
ppr EagerDefaulting = text "EagerDefaulting"
ppr NoRestrictions = text "NoRestrictions"
simplifyInfer :: TcLevel  Used when generating the constraints
> InferMode
> [TcIdSigInst]  Any signatures (possibly partial)
> [(Name, TcTauType)]  Variables to be generalised,
 and their tautypes
> WantedConstraints
> TcM ([TcTyVar],  Quantify over these type variables
[EvVar],  ... and these constraints (fully zonked)
TcEvBinds,  ... binding these evidence variables
Bool)  True <=> there was an insoluble type error
 in these bindings
simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
 isEmptyWC wanteds
= do { gbl_tvs < tcGetGlobalTyCoVars
; dep_vars < zonkTcTypesAndSplitDepVars (map snd name_taus)
; qtkvs < quantifyTyVars gbl_tvs dep_vars
; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
; return (qtkvs, [], emptyTcEvBinds, False) }
 otherwise
= do { traceTc "simplifyInfer {" $ vcat
[ text "sigs =" <+> ppr sigs
, text "binds =" <+> ppr name_taus
, text "rhs_tclvl =" <+> ppr rhs_tclvl
, text "infer_mode =" <+> ppr infer_mode
, text "(unzonked) wanted =" <+> ppr wanteds
]
; let partial_sigs = filter isPartialSig sigs
psig_theta = concatMap sig_inst_theta partial_sigs
 First do fullblown solving
 NB: we must gather up all the bindings from doing
 this solving; hence (runTcSWithEvBinds ev_binds_var).
 And note that since there are nested implications,
 calling solveWanteds will sideeffect their evidence
 bindings, so we can't just revert to the input
 constraint.
; tc_lcl_env < TcM.getLclEnv
; ev_binds_var < TcM.newTcEvBinds
; psig_theta_vars < mapM TcM.newEvVar psig_theta
; wanted_transformed_incl_derivs
< setTcLevel rhs_tclvl $
runTcSWithEvBinds ev_binds_var $
do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
psig_givens = mkGivens loc psig_theta_vars
; _ < solveSimpleGivens psig_givens
 See Note [Add signature contexts as givens]
; solveWanteds wanteds }
 Find quant_pred_candidates, the predicates that
 we'll consider quantifying over
 NB1: wanted_transformed does not include anything provable from
 the psig_theta; it's just the extra bit
 NB2: We do not do any defaulting when inferring a type, this can lead
 to less polymorphic types, see Note [Default while Inferring]
; wanted_transformed_incl_derivs < TcM.zonkWC wanted_transformed_incl_derivs
; let definite_error = insolubleWC wanted_transformed_incl_derivs
 See Note [Quantification with errors]
 NB: must include derived errors in this test,
 hence "incl_derivs"
wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
quant_pred_candidates
 definite_error = []
 otherwise = ctsPreds (approximateWC False wanted_transformed)
 Decide what type variables and constraints to quantify
 NB: quant_pred_candidates is already fully zonked
 NB: bound_theta are constraints we want to quantify over,
 including the psig_theta, which we always quantify over
 NB: bound_theta are fully zonked
; (qtvs, bound_theta, co_vars) < decideQuantification infer_mode rhs_tclvl
name_taus partial_sigs
quant_pred_candidates
; bound_theta_vars < mapM TcM.newEvVar bound_theta
 We must produce bindings for the psig_theta_vars, because we may have
 used them in evidence bindings constructed by solveWanteds earlier
 Easiest way to do this is to emit them as new Wanteds (Trac #14643)
; ct_loc < getCtLocM AnnOrigin Nothing
; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
, ctev_dest = EvVarDest psig_theta_var
, ctev_nosh = WDeriv
, ctev_loc = ct_loc }
 psig_theta_var < psig_theta_vars ]
 Now we can emil the residual constraints
; emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
name_taus co_vars qtvs
bound_theta_vars
(wanted_transformed `andWC` mkSimpleWC psig_wanted)
 All done!
; traceTc "} simplifyInfer/produced residual implication for quantification" $
vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
, text "psig_theta =" <+> ppr psig_theta
, text "bound_theta =" <+> ppr bound_theta
, text "qtvs =" <+> ppr qtvs
, text "definite_error =" <+> ppr definite_error ]
; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
 NB: bound_theta_vars must be fully zonked

emitResidualConstraints :: TcLevel > TcLclEnv > EvBindsVar
> [(Name, TcTauType)]
> VarSet > [TcTyVar] > [EvVar]
> WantedConstraints > TcM ()
 Emit the remaining constraints from the RHS.
 See Note [Emitting the residual implication in simplifyInfer]
emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
name_taus co_vars qtvs full_theta_vars wanteds
 isEmptyWC wanteds
= return ()
 otherwise
= do { wanted_simple < TcM.zonkSimples (wc_simple wanteds)
; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
; _ < promoteTyVarSet (tyCoVarsOfCts outer_simple)
; unless (isEmptyCts outer_simple) $
do { traceTc "emitResidualConstrants:simple" (ppr outer_simple)
; emitSimples outer_simple }
; let inner_wanted = wanteds { wc_simple = inner_simple }
implic = mk_implic inner_wanted
; unless (isEmptyWC inner_wanted) $
do { traceTc "emitResidualConstraints:implic" (ppr implic)
; emitImplication implic }
}
where
mk_implic inner_wanted
= newImplication { ic_tclvl = rhs_tclvl
, ic_skols = qtvs
, ic_given = full_theta_vars
, ic_wanted = inner_wanted
, ic_binds = ev_binds_var
, ic_info = skol_info
, ic_env = tc_lcl_env }
full_theta = map idType full_theta_vars
skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
 (name, ty) < name_taus ]
 Don't add the quantified variables here, because
 they are also bound in ic_skols and we want them
 to be tidied uniformly

ctsPreds :: Cts > [PredType]
ctsPreds cts = [ ctEvPred ev  ct < bagToList cts
, let ev = ctEvidence ct ]
{ Note [Emitting the residual implication in simplifyInfer]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f = e
where f's type is inferred to be something like (a, Proxy k (Int > co))
and we have an asyetunsolved, or perhaps insoluble, constraint
[W] co :: Type ~ k
We can't form types like (forall co. blah), so we can't generalise over
the coercion variable, and hence we can't generalise over things free in
its kind, in the case 'k'. But we can still generalise over 'a'. So
we'll generalise to
f :: forall a. (a, Proxy k (Int > co))
Now we do NOT want to form the residual implication constraint
forall a. [W] co :: Type ~ k
because then co's eventual binding (which will be a value binding if we
use fdefertypeerrors) won't scope over the entire binding for 'f' (whose
type mentions 'co'). Instead, just as we don't generalise over 'co', we
should not bury its constraint inside the implication. Instead, we must
put it outside.
That is the reason for the partitionBag in emitResidualConstraints,
which takes the CoVars free in the inferred type, and pulls their
constraints out. (NB: this set of CoVars should be
closedoverkinds.)
All rather subtle; see Trac #14584.
Note [Add signature contexts as givens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (Trac #11016):
f2 :: (?x :: Int) => _
f2 = ?x
or this
f3 :: a ~ Bool => (a, _)
f3 = (True, False)
or theis
f4 :: (Ord a, _) => a > Bool
f4 x = x==x
We'll use plan InferGen because there are holes in the type. But:
* For f2 we want to have the (?x :: Int) constraint floating around
so that the functional dependencies kick in. Otherwise the
occurrence of ?x on the RHS produces constraint (?x :: alpha), and
we won't unify alpha:=Int.
* For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool)
in the RHS
* For f4 we want to use the (Ord a) in the signature to solve the Eq a
constraint.
Solution: in simplifyInfer, just before simplifying the constraints
gathered from the RHS, add Given constraints for the context of any
type signatures.
************************************************************************
* *
Quantification
* *
************************************************************************
Note [Deciding quantification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the monomorphism restriction does not apply, then we quantify as follows:
* Step 1. Take the global tyvars, and "grow" them using the equality
constraints
E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
happen because alpha is untouchable here) then do not quantify over
beta, because alpha fixes beta, and beta is effectively free in
the environment too
We also account for the monomorphism restriction; if it applies,
add the free vars of all the constraints.
Result is mono_tvs; we will not quantify over these.
* Step 2. Default any nonmono tyvars (i.e ones that are definitely
not going to become further constrained), and resimplify the
candidate constraints.
Motivation for resimplification (Trac #7857): imagine we have a
constraint (C (a>b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
not free in the envt, and instance forall (a::*) (b::*). (C a) => C
(a > b) The instance doesn't match while l1,l2 are polymorphic, but
it will match when we default them to LiftedRep.
This is all very tiresome.
* Step 3: decide which variables to quantify over, as follows:
 Take the free vars of the tautype (zonked_tau_tvs) and "grow"
them using all the constraints. These are tau_tvs_plus
 Use quantifyTyVars to quantify over (tau_tvs_plus  mono_tvs), being
careful to close over kinds, and to skolemise the quantified tyvars.
(This actually unifies each quantifies metatyvar with a fresh skolem.)
Result is qtvs.
* Step 4: Filter the constraints using pickQuantifiablePreds and the
qtvs. We have to zonk the constraints first, so they "see" the
freshly created skolems.
}
decideQuantification
:: InferMode
> TcLevel
> [(Name, TcTauType)]  Variables to be generalised
> [TcIdSigInst]  Partial type signatures (if any)
> [PredType]  Candidate theta; already zonked
> TcM ( [TcTyVar]  Quantify over these (skolems)
, [PredType]  and this context (fully zonked)
, VarSet)
 See Note [Deciding quantification]
decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
= do {  Step 1: find the mono_tvs
; (mono_tvs, candidates, co_vars) < decideMonoTyVars infer_mode
name_taus psigs candidates
 Step 2: default any nonmono tyvars, and resimplify
 This step may do some unification, but result candidates is zonked
; candidates < defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
 Step 3: decide which kind/type variables to quantify over
; qtvs < decideQuantifiedTyVars mono_tvs name_taus psigs candidates
 Step 4: choose which of the remaining candidate
 predicates to actually quantify over
 NB: decideQuantifiedTyVars turned some meta tyvars
 into quantified skolems, so we have to zonk again
; candidates < TcM.zonkTcTypes candidates
; psig_theta < TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
; let quantifiable_candidates
= pickQuantifiablePreds (mkVarSet qtvs) candidates
 NB: do /not/ run pickQuantifiablePreds over psig_theta,
 because we always want to quantify over psig_theta, and not
 drop any of them; e.g. CallStack constraints. c.f Trac #14658
theta = mkMinimalBySCs id $  See Note [Minimize by Superclasses]
(psig_theta ++ quantifiable_candidates)
; traceTc "decideQuantification"
(vcat [ text "infer_mode:" <+> ppr infer_mode
, text "candidates:" <+> ppr candidates
, text "psig_theta:" <+> ppr psig_theta
, text "mono_tvs:" <+> ppr mono_tvs
, text "co_vars:" <+> ppr co_vars
, text "qtvs:" <+> ppr qtvs
, text "theta:" <+> ppr theta ])
; return (qtvs, theta, co_vars) }

decideMonoTyVars :: InferMode
> [(Name,TcType)]
> [TcIdSigInst]
> [PredType]
> TcM (TcTyCoVarSet, [PredType], CoVarSet)
 Decide which tyvars and covars cannot be generalised:
 (a) Free in the environment
 (b) Mentioned in a constraint we can't generalise
 (c) Connected by an equality to (a) or (b)
 Also return CoVars that appear free in the final quatified types
 we can't quantify over these, and we must make sure they are in scope
decideMonoTyVars infer_mode name_taus psigs candidates
= do { (no_quant, maybe_quant) < pick infer_mode candidates
 If possible, we quantify over partialsig qtvs, so they are
 not mono. Need to zonk them because they are metatyvar SigTvs
; psig_qtvs < mapM zonkTcTyVarToTyVar $
concatMap (map snd . sig_inst_skols) psigs
; psig_theta < mapM TcM.zonkTcType $
concatMap sig_inst_theta psigs
; taus < mapM (TcM.zonkTcType . snd) name_taus
; mono_tvs0 < tcGetGlobalTyCoVars
; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
co_vars = coVarsOfTypes (psig_tys ++ taus)
co_var_tvs = closeOverKinds co_vars
 The co_var_tvs are tvs mentioned in the types of covars or
 coercion holes. We can't quantify over these covars, so we
 must include the variable in their types in the mono_tvs.
 E.g. If we can't quantify over co :: k~Type, then we can't
 quantify over k either! Hence closeOverKinds
mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
eq_constraints = filter isEqPred candidates
mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1
constrained_tvs = (growThetaTyVars eq_constraints
(tyCoVarsOfTypes no_quant)
`minusVarSet` mono_tvs2)
`delVarSetList` psig_qtvs
 constrained_tvs: the tyvars that we are not going to
 quantify solely because of the moonomorphism restriction

 (`minusVarSet` mono_tvs1`): a type variable is only
 "constrained" (so that the MR bites) if it is not
 free in the environment (Trac #13785)

 (`delVarSetList` psig_qtvs): if the user has explicitly
 asked for quantification, then that request "wins"
 over the MR. Note: do /not/ delete psig_qtvs from
 mono_tvs1, because mono_tvs1 cannot under any circumstances
 be quantified (Trac #14479); see
 Note [Quantification and partial signatures], Wrinkle 3, 4
mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
 Warn about the monomorphism restriction
; warn_mono < woptM Opt_WarnMonomorphism
; when (case infer_mode of { ApplyMR > warn_mono; _ > False}) $
warnTc (Reason Opt_WarnMonomorphism)
(constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
mr_msg
; traceTc "decideMonoTyVars" $ vcat
[ text "mono_tvs0 =" <+> ppr mono_tvs0
, text "mono_tvs1 =" <+> ppr mono_tvs1
, text "no_quant =" <+> ppr no_quant
, text "maybe_quant =" <+> ppr maybe_quant
, text "eq_constraints =" <+> ppr eq_constraints
, text "mono_tvs =" <+> ppr mono_tvs
, text "co_vars =" <+> ppr co_vars ]
; return (mono_tvs, maybe_quant, co_vars) }
where
pick :: InferMode > [PredType] > TcM ([PredType], [PredType])
 Split the candidates into ones we definitely
 won't quantify, and ones that we might
pick NoRestrictions cand = return ([], cand)
pick ApplyMR cand = return (cand, [])
pick EagerDefaulting cand = do { os < xoptM LangExt.OverloadedStrings
; return (partition (is_int_ct os) cand) }
 For EagerDefaulting, do not quantify over
 over any interactive class constraint
is_int_ct ovl_strings pred
 Just (cls, _) < getClassPredTys_maybe pred
= isInteractiveClass ovl_strings cls
 otherwise
= False
pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
mr_msg =
hang (sep [ text "The Monomorphism Restriction applies to the binding"
<> plural name_taus
, text "for" <+> pp_bndrs ])
2 (hsep [ text "Consider giving"
, text (if isSingleton name_taus then "it" else "them")
, text "a type signature"])

defaultTyVarsAndSimplify :: TcLevel
> TyCoVarSet
> [PredType]  Assumed zonked
> TcM [PredType]  Guaranteed zonked
 Default any tyvar free in the constraints,
 and resimplify in case the defaulting allows further simplification
defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
= do {  Promote any tyvars that we cannot generalise
 See Note [Promote momomorphic tyvars]
; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
; prom < promoteTyVarSet mono_tvs
 Default any kind/levity vars
; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
= candidateQTyVarsOfTypes candidates
; poly_kinds < xoptM LangExt.PolyKinds
; default_kvs < mapM (default_one poly_kinds True)
(dVarSetElems cand_kvs)
; default_tvs < mapM (default_one poly_kinds False)
(dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
; let some_default = or default_kvs  or default_tvs
; case () of
_  some_default > simplify_cand candidates
 prom > mapM TcM.zonkTcType candidates
 otherwise > return candidates
}
where
default_one poly_kinds is_kind_var tv
 not (isMetaTyVar tv)
= return False
 tv `elemVarSet` mono_tvs
= return False
 otherwise
= defaultTyVar (not poly_kinds && is_kind_var) tv
simplify_cand candidates
= do { clone_wanteds < newWanteds DefaultOrigin candidates
; WC { wc_simple = simples } < setTcLevel rhs_tclvl $
simplifyWantedsTcM clone_wanteds
 Discard evidence; simples is fully zonked
; let new_candidates = ctsPreds simples
; traceTc "Simplified after defaulting" $
vcat [ text "Before:" <+> ppr candidates
, text "After:" <+> ppr new_candidates ]
; return new_candidates }

decideQuantifiedTyVars
:: TyCoVarSet  Monomorphic tyvars
> [(Name,TcType)]  Annotated theta and (name,tau) pairs
> [TcIdSigInst]  Partial signatures
> [PredType]  Candidates, zonked
> TcM [TyVar]
 Fix what tyvars we are going to quantify over, and quantify them
decideQuantifiedTyVars mono_tvs name_taus psigs candidates
= do {  Why psig_tys? We try to quantify over everything free in here
 See Note [Quantification and partial signatures]
 Wrinkles 2 and 3
; psig_tv_tys < mapM TcM.zonkTcTyVar [ tv  sig < psigs
, (_,tv) < sig_inst_skols sig ]
; psig_theta < mapM TcM.zonkTcType [ pred  sig < psigs
, pred < sig_inst_theta sig ]
; tau_tys < mapM (TcM.zonkTcType . snd) name_taus
; mono_tvs < TcM.zonkTyCoVarsAndFV mono_tvs
; let  Try to quantify over variables free in these types
psig_tys = psig_tv_tys ++ psig_theta
seed_tys = psig_tys ++ tau_tys
 Now "grow" those seeds to find ones reachable via 'candidates'
grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
 Now we have to classify them into kind variables and type variables
 (sigh) just for the benefit of XNoPolyKinds; see quantifyTyVars

 Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
 them in that order, so that the final qtvs quantifies in the same
 order as the partial signatures do (Trac #13524)
; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
= candidateQTyVarsOfTypes $
psig_tys ++ candidates ++ tau_tys
pick = (`dVarSetIntersectVarSet` grown_tcvs)
dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
; traceTc "decideQuantifiedTyVars" (vcat
[ text "seed_tys =" <+> ppr seed_tys
, text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
, text "grown_tcvs =" <+> ppr grown_tcvs])
; quantifyTyVars mono_tvs dvs_plus }

growThetaTyVars :: ThetaType > TyCoVarSet > TyCoVarSet
 See Note [Growing the tautvs using constraints]
growThetaTyVars theta tcvs
 null theta = tcvs
 otherwise = transCloVarSet mk_next seed_tcvs
where
seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
(ips, non_ips) = partition isIPPred theta
 See Note [Inheriting implicit parameters] in TcType
mk_next :: VarSet > VarSet  Maps current set to newlygrown ones
mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
grow_one so_far pred tcvs
 pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
 otherwise = tcvs
where
pred_tcvs = tyCoVarsOfType pred
{ Note [Promote momomorphic tyvars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Promote any type variables that are free in the environment. Eg
f :: forall qtvs. bound_theta => zonked_tau
The free vars of f's type become free in the envt, and hence will show
up whenever 'f' is called. They may currently at rhs_tclvl, but they
had better be unifiable at the outer_tclvl! Example: envt mentions
alpha[1]
tau_ty = beta[2] > beta[2]
constraints = alpha ~ [beta]
we don't quantify over beta (since it is fixed by envt)
so we must promote it! The inferred type is just
f :: beta > beta
NB: promoteTyVar ignores coercion variables
Note [Quantification and partial signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When choosing type variables to quantify, the basic plan is to
quantify over all type variables that are
* free in the tau_tvs, and
* not forced to be monomorphic (mono_tvs),
for example by being free in the environment.
However, in the case of a partial type signature, be doing inference
*in the presence of a type signature*. For example:
f :: _ > a
f x = ...
or
g :: (Eq _a) => _b > _b
In both cases we use plan InferGen, and hence call simplifyInfer. But
those 'a' variables are skolems (actually SigTvs), and we should be
sure to quantify over them. This leads to several wrinkles:
* Wrinkle 1. In the case of a type error
f :: _ > Maybe a
f x = True && x
The inferred type of 'f' is f :: Bool > Bool, but there's a
leftover error of form (HoleCan (Maybe a ~ Bool)). The errorreporting
machine expects to find a binding site for the skolem 'a', so we
add it to the quantified tyvars.
* Wrinkle 2. Consider the partial type signature
f :: (Eq _) => Int > Int
f x = x
In normal cases that makes sense; e.g.
g :: Eq _a => _a > _a
g x = x
where the signature makes the type less general than it could
be. But for 'f' we must therefore quantify over the userannotated
constraints, to get
f :: forall a. Eq a => Int > Int
(thereby correctly triggering an ambiguity error later). If we don't
we'll end up with a strange open type
f :: Eq alpha => Int > Int
which isn't ambiguous but is still very wrong.
Bottom line: Try to quantify over any variable free in psig_theta,
just like the taupart of the type.
* Wrinkle 3 (Trac #13482). Also consider
f :: forall a. _ => Int > Int
f x = if (undefined :: a) == undefined then x else 0
Here we get an (Eq a) constraint, but it's not mentioned in the
psig_theta nor the type of 'f'. But we still want to quantify
over 'a' even if the monomorphism restriction is on.
* Wrinkle 4 (Trac #14479)
foo :: Num a => a > a
foo xxx = g xxx
where
g :: forall b. Num b => _ > b
g y = xxx + y
In the signature for 'g', we cannot quantify over 'b' because it turns out to
get unified with 'a', which is free in g's environment. So we carefully
refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars. We
report the error later, in TcBinds.chooseInferredQuantifiers.
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Should we quantify over an equality constraint (s ~ t)? In general, we don't.
Doing so may simply postpone a type error from the function definition site to
its call site. (At worst, imagine (Int ~ Bool)).

However, consider this
 forall a. (F [a] ~ Int) => blah
Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
site we will know 'a', and perhaps we have instance F [Bool] = Int.
So we *do* quantify over a typefamily equality where the arguments mention
the quantified variables.

Note [Growing the tautvs using constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(growThetaTyVars insts tvs) is the result of extending the set
of tyvars, tvs, using all conceivable links from pred
E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
Then growThetaTyVars preds tvs = {a,b,c}
Notice that
growThetaTyVars is conservative if v might be fixed by vs
=> v `elem` grow(vs,C)
Note [Quantification with errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we find that the RHS of the definition has some absolutelyinsoluble
constraints (including especially "variable not in scope"), we
* Abandon all attempts to find a context to quantify over,
and instead make the function fullypolymorphic in whatever
type we have found
* Return a flag from simplifyInfer, indicating that we found an
insoluble constraint. This flag is used to suppress the ambiguity
check for the inferred type, which may well be bogus, and which
tends to obscure the real error. This fix feels a bit clunky,
but I failed to come up with anything better.
Reasons:
 Avoid downstream errors
 Do not perform an ambiguity test on a bogus type, which might well
fail spuriously, thereby obfuscating the original insoluble error.
Trac #14000 is an example
I tried an alternative approach: simply failM, after emitting the
residual implication constraint; the exception will be caught in
TcBinds.tcPolyBinds, which gives all the binders in the group the type
(forall a. a). But that didn't work with fdefertypeerrors, because
the recovery from failM emits no code at all, so there is no function
to run! But fdefertypeerrors aspires to produce a runnable program.
NB that we must include *derived* errors in the check for insolubles.
Example:
(a::*) ~ Int#
We get an insoluble derived error *~#, and we don't want to discard
it before doing the isInsolubleWC test! (Trac #8262)
Note [Default while Inferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Our current plan is that defaulting only happens at simplifyTop and
not simplifyInfer. This may lead to some insoluble deferred constraints.
Example:
instance D g => C g Int b
constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
type inferred = gamma > gamma
Now, if we try to default (alpha := Int) we will be able to refine the implication to
(forall b. 0 => C gamma Int b)
which can then be simplified further to
(forall b. 0 => D gamma)
Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
type: forall g. D g => g > g
Instead what will currently happen is that we will get a quantified type
(forall g. g > g) and an implication:
forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
unsolvable implication:
forall g. 0 => (forall b. 0 => D g)
The concrete example would be:
h :: C g a s => g > a > ST s a
f (x::gamma) = (\_ > x) (runST (h x (undefined::alpha)) + 1)
But it is quite tedious to do defaulting and resolve the implication constraints, and
we have not observed code breaking because of the lack of defaulting in inference, so
we don't do it for now.
Note [Minimize by Superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we quantify over a constraint, in simplifyInfer we need to
quantify over a constraint that is minimal in some sense: For
instance, if the final wanted constraint is (Eq alpha, Ord alpha),
we'd like to quantify over Ord alpha, because we can just get Eq alpha
from superclass selection from Ord alpha. This minimization is what
mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
to check the original wanted.
Note [Avoid unnecessary constraint simplification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 NB NB NB (Jun 12) 
This note not longer applies; see the notes with Trac #4361.
But I'm leaving it in here so we remember the issue.)

When inferring the type of a letbinding, with simplifyInfer,
try to avoid unnecessarily simplifying class constraints.
Doing so aids sharing, but it also helps with delicate
situations like
instance C t => C [t] where ..
f :: C [t] => ....
f x = let g y = ...(constraint C [t])...
in ...
When inferring a type for 'g', we don't want to apply the
instance decl, because then we can't satisfy (C t). So we
just notice that g isn't quantified over 't' and partition
the constraints before simplifying.
This only halfworks, but then letgeneralisation only halfworks.
*********************************************************************************
* *
* Main Simplifier *
* *
***********************************************************************************
}
simplifyWantedsTcM :: [CtEvidence] > TcM WantedConstraints
 Solve the specified Wanted constraints
 Discard the evidence binds
 Discards all Derived stuff in result
 Postcondition: fully zonked and unflattened constraints
simplifyWantedsTcM wanted
= do { traceTc "simplifyWantedsTcM {" (ppr wanted)
; (result, _) < runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
; result < TcM.zonkWC result
; traceTc "simplifyWantedsTcM }" (ppr result)
; return result }
solveWantedsAndDrop :: WantedConstraints > TcS WantedConstraints
 Since solveWanteds returns the residual WantedConstraints,
 it should always be called within a runTcS or something similar,
 Result is not zonked
solveWantedsAndDrop wanted
= do { wc < solveWanteds wanted
; return (dropDerivedWC wc) }
solveWanteds :: WantedConstraints > TcS WantedConstraints
 so that the inert set doesn't mindlessly propagate.
 NB: wc_simples may be wanted /or/ derived now
solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
= do { traceTcS "solveWanteds {" (ppr wc)
; wc1 < solveSimpleWanteds simples
 Any insoluble constraints are in 'simples' and so get rewritten
 See Note [Rewrite insolubles] in TcSMonad
; (floated_eqs, implics2) < solveNestedImplications $
implics `unionBags` wc_impl wc1
; dflags < getDynFlags
; final_wc < simpl_loop 0 (solverIterations dflags) floated_eqs
(wc1 { wc_impl = implics2 })
; ev_binds_var < getTcEvBindsVar
; bb < TcS.getTcEvBindsMap ev_binds_var
; traceTcS "solveWanteds }" $
vcat [ text "final wc =" <+> ppr final_wc
, text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
; return final_wc }
simpl_loop :: Int > IntWithInf > Cts
> WantedConstraints > TcS WantedConstraints
simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples })
 n `intGtLimit` limit
= do {  Add an error (not a warning) if we blow the limit,
 Typically if we blow the limit we are going to report some other error
 (an unsolved constraint), and we don't want that error to suppress
 the iteration limit warning!
addErrTcS (hang (text "solveWanteds: too many iterations"
<+> parens (text "limit =" <+> ppr limit))
2 (vcat [ text "Unsolved:" <+> ppr wc
, ppUnless (isEmptyBag floated_eqs) $
text "Floated equalities:" <+> ppr floated_eqs
, text "Set limit with fconstraintsolveriterations=n; n=0 for no limit"
]))
; return wc }
 not (isEmptyBag floated_eqs)
= simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples })
 Put floated_eqs first so they get solved first
 NB: the floated_eqs may include /derived/ equalities
 arising from fundeps inside an implication
 superClassesMightHelp wc
=  We still have unsolved goals, and apparently no way to solve them,
 so try expanding superclasses at this level, both Given and Wanted
do { pending_given < getPendingGivenScs
; let (pending_wanted, simples1) = getPendingWantedScs simples
; if null pending_given && null pending_wanted
then return wc  After all, superclasses did not help
else
do { new_given < makeSuperClasses pending_given
; new_wanted < makeSuperClasses pending_wanted
; solveSimpleGivens new_given  Add the new Givens to the inert set
; simplify_again n limit (null pending_given)
wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
 otherwise
= return wc
simplify_again :: Int > IntWithInf > Bool
> WantedConstraints > TcS WantedConstraints
 We have definitely decided to have another go at solving
 the wanted constraints (we have tried at least once already
simplify_again n limit no_new_given_scs
wc@(WC { wc_simple = simples, wc_impl = implics })
= do { csTraceTcS $
text "simpl_loop iteration=" <> int n
<+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma
, int (lengthBag simples) <+> text "simples to solve" ])
; traceTcS "simpl_loop: wc =" (ppr wc)
; (unifs1, wc1) < reportUnifications $
solveSimpleWanteds $
simples
 See Note [Cutting off simpl_loop]
 We have already tried to solve the nested implications once
 Try again only if we have unified some metavariables
 (which is a bit like adding more givens), or we have some
 new Given superclasses
; let new_implics = wc_impl wc1
; if unifs1 == 0 &&
no_new_given_scs &&
isEmptyBag new_implics
then  Do not even try to solve the implications
simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics })
else  Try to solve the implications
do { (floated_eqs2, implics2) < solveNestedImplications $
implics `unionBags` new_implics
; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 })
} }
solveNestedImplications :: Bag Implication
> TcS (Cts, Bag Implication)
 Precondition: the TcS inerts may contain unsolved simples which have
 to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
 isEmptyBag implics
= return (emptyBag, emptyBag)
 otherwise
= do { traceTcS "solveNestedImplications starting {" empty
; (floated_eqs_s, unsolved_implics) < mapAndUnzipBagM solveImplication implics
; let floated_eqs = concatBag floated_eqs_s
 ... and we are back in the original TcS inerts
 Notice that the original includes the _insoluble_simples so it was safe to ignore
 them in the beginning of this function.
; traceTcS "solveNestedImplications end }" $
vcat [ text "all floated_eqs =" <+> ppr floated_eqs
, text "unsolved_implics =" <+> ppr unsolved_implics ]
; return (floated_eqs, catBagMaybes unsolved_implics) }
solveImplication :: Implication  Wanted
> TcS (Cts,  All wanted or derived floated equalities: var = type
Maybe Implication)  Simplified implication (empty or singleton)
 Precondition: The TcS monad contains an empty worklist and givenonly inerts
 which after trying to solve this implication we must restore to their original value
solveImplication imp@(Implic { ic_tclvl = tclvl
, ic_binds = ev_binds_var
, ic_skols = skols
, ic_given = given_ids
, ic_wanted = wanteds
, ic_info = info
, ic_status = status
, ic_env = env })
 isSolvedStatus status
= return (emptyCts, Just imp)  Do nothing
 otherwise  Even for IC_Insoluble it is worth doing more work
 The insoluble stuff might be in one subimplication
 and other unsolved goals in another; and we want to
 solve the latter as much as possible
= do { inerts < getTcSInerts
; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
 Solve the nested constraints
; (no_given_eqs, given_insols, residual_wanted)
< nestImplicTcS ev_binds_var tclvl $
do { let loc = mkGivenLoc tclvl info env
givens = mkGivens loc given_ids
; solveSimpleGivens givens
; residual_wanted < solveWanteds wanteds
 solveWanteds, *not* solveWantedsAndDrop, because
 we want to retain derived equalities so we can float
 them out in floatEqualities
; (no_eqs, given_insols) < getNoGivenEqs tclvl skols
 Call getNoGivenEqs /after/ solveWanteds, because
 solveWanteds can augment the givens, via expandSuperClasses,
 to reveal given superclass equalities
; return (no_eqs, given_insols, residual_wanted) }
; (floated_eqs, residual_wanted)
< floatEqualities skols given_ids ev_binds_var
no_given_eqs residual_wanted
; traceTcS "solveImplication 2"
(ppr given_insols $$ ppr residual_wanted)
; let final_wanted = residual_wanted `addInsols` given_insols
 Don't lose track of the insoluble givens,
 which signal unreachable code; put them in ic_wanted
; res_implic < setImplicationStatus (imp { ic_no_eqs = no_given_eqs
, ic_wanted = final_wanted })
; evbinds < TcS.getTcEvBindsMap ev_binds_var
; tcvs < TcS.getTcEvTyCoVars ev_binds_var
; traceTcS "solveImplication end }" $ vcat
[ text "no_given_eqs =" <+> ppr no_given_eqs
, text "floated_eqs =" <+> ppr floated_eqs
, text "res_implic =" <+> ppr res_implic
, text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
, text "implication tvcs =" <+> ppr tcvs ]
; return (floated_eqs, res_implic) }

setImplicationStatus :: Implication > TcS (Maybe Implication)
 Finalise the implication returned from solveImplication:
 * Set the ic_status field
 * Trim the ic_wanted field to remove Derived constraints
 Precondition: the ic_status field is not already IC_Solved
 Return Nothing if we can discard the implication altogether
setImplicationStatus implic@(Implic { ic_status = status
, ic_info = info
, ic_wanted = wc
, ic_given = givens })
 ASSERT2( not (isSolvedStatus status ), ppr info )
 Precondition: we only set the status if it is not already solved
not (isSolvedWC pruned_wc)
= do { traceTcS "setImplicationStatus(notallsolved) {" (ppr implic)
; implic < neededEvVars implic
; let new_status  insolubleWC pruned_wc = IC_Insoluble
 otherwise = IC_Unsolved
new_implic = implic { ic_status = new_status
, ic_wanted = pruned_wc }
; traceTcS "setImplicationStatus(notallsolved) }" (ppr new_implic)
; return $ Just new_implic }
 otherwise  Everything is solved
 Set status to IC_Solved,
 and compute the dead givens and outer needs
 See Note [Tracking redundant constraints]
= do { traceTcS "setImplicationStatus(allsolved) {" (ppr implic)
; implic@(Implic { ic_need_inner = need_inner
, ic_need_outer = need_outer }) < neededEvVars implic
; bad_telescope < checkBadTelescope implic
; let dead_givens  warnRedundantGivens info
= filterOut (`elemVarSet` need_inner) givens
 otherwise = []  None to report
discard_entire_implication  Can we discard the entire implication?
= null dead_givens  No warning from this implication
&& not bad_telescope
&& isEmptyWC pruned_wc  No live children
&& isEmptyVarSet need_outer  No needed vars to pass up to parent
final_status
 bad_telescope = IC_BadTelescope
 otherwise = IC_Solved { ics_dead = dead_givens }
final_implic = implic { ic_status = final_status
, ic_wanted = pruned_wc }
; traceTcS "setImplicationStatus(allsolved) }" $
vcat [ text "discard:" <+> ppr discard_entire_implication
, text "new_implic:" <+> ppr final_implic ]
; return $ if discard_entire_implication
then Nothing
else Just final_implic }
where
WC { wc_simple = simples, wc_impl = implics } = wc
pruned_simples = dropDerivedSimples simples
pruned_implics = filterBag keep_me implics
pruned_wc = WC { wc_simple = pruned_simples
, wc_impl = pruned_implics }
keep_me :: Implication > Bool
keep_me ic
 IC_Solved { ics_dead = dead_givens } < ic_status ic
 Fully solved
, null dead_givens  No redundant givens to report
, isEmptyBag (wc_impl (ic_wanted ic))
 And no children that might have things to report
= False  Tnen we don't need to keep it
 otherwise
= True  Otherwise, keep it
checkBadTelescope :: Implication > TcS Bool
 True <=> the skolems form a bad telescope
 See Note [Keeping scoped variables in order: Explicit] in TcHsType
checkBadTelescope (Implic { ic_telescope = m_telescope
, ic_skols = skols })
 isJust m_telescope
= do{ skols < mapM TcS.zonkTcTyCoVarBndr skols
; return (go emptyVarSet (reverse skols))}
 otherwise
= return False
where
go :: TyVarSet  skolems that appear *later* than the current ones
> [TcTyVar]  ordered skolems, in reverse order
> Bool  True <=> there is an outoforder skolem
go _ [] = False
go later_skols (one_skol : earlier_skols)
 tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
= True
 otherwise
= go (later_skols `extendVarSet` one_skol) earlier_skols
warnRedundantGivens :: SkolemInfo > Bool
warnRedundantGivens (SigSkol ctxt _ _)
= case ctxt of
FunSigCtxt _ warn_redundant > warn_redundant
ExprSigCtxt > True
_ > False
 To think about: do we want to report redundant givens for
 pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
warnRedundantGivens (InstSkol {}) = True
warnRedundantGivens _ = False
neededEvVars :: Implication > TcS Implication
 Find all the evidence variables that are "needed",
 and delete dead evidence bindings
 See Note [Tracking redundant constraints]
 See Note [Delete dead Given evidence bindings]

  Start from initial_seeds (from nested implications)

  Add free vars of RHS of all Wanted evidence bindings
 and coercion variables accumulated in tcvs (all Wanted)

  Generate 'needed', the needed set of EvVars, by doing transitive
 closure through Given bindings
 e.g. Needed {a,b}
 Given a = sc_sel a2
 Then a2 is needed too

  Prune out all Given bindings that are not needed

  From the 'needed' set, delete ev_bndrs, the binders of the
 evidence bindings, to give the final needed variables

neededEvVars implic@(Implic { ic_given = givens
, ic_binds = ev_binds_var
, ic_wanted = WC { wc_impl = implics }
, ic_need_inner = old_needs })
= do { ev_binds < TcS.getTcEvBindsMap ev_binds_var
; tcvs < TcS.getTcEvTyCoVars ev_binds_var
; let seeds1 = foldrBag add_implic_seeds old_needs implics
seeds2 = foldEvBindMap add_wanted seeds1 ev_binds
seeds3 = seeds2 `unionVarSet` tcvs
need_inner = findNeededEvVars ev_binds seeds3
live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
need_outer = foldEvBindMap del_ev_bndr need_inner live_ev_binds
`delVarSetList` givens
; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
 See Note [Delete dead Given evidence bindings]
; traceTcS "neededEvVars" $
vcat [ text "old_needs:" <+> ppr old_needs
, text "seeds3:" <+> ppr seeds3
, text "ev_binds:" <+> ppr ev_binds
, text "live_ev_binds:" <+> ppr live_ev_binds ]
; return (implic { ic_need_inner = need_inner
, ic_need_outer = need_outer }) }
where
add_implic_seeds (Implic { ic_need_outer = needs, ic_given = givens }) acc
= (needs `delVarSetList` givens) `unionVarSet` acc
needed_ev_bind needed (EvBind { eb_lhs = ev_var
, eb_is_given = is_given })
 is_given = ev_var `elemVarSet` needed
 otherwise = True  Keep all wanted bindings
del_ev_bndr :: EvBind > VarSet > VarSet
del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v
add_wanted :: EvBind > VarSet > VarSet
add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
 is_given = needs  Add the rhs vars of the Wanted bindings only
 otherwise = evVarsOfTerm rhs `unionVarSet` needs
{ Note [Delete dead Given evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As a result of superclass expansion, we speculatively
generate evidence bindings for Givens. E.g.
f :: (a ~ b) => a > b > Bool
f x y = ...
We'll have
[G] d1 :: (a~b)
and we'll specuatively generate the evidence binding
[G] d2 :: (a ~# b) = sc_sel d
Now d2 is available for solving. But it may not be needed! Usually
such dead superclass selections will eventually be dropped as dead
code, but:
* It won't always be dropped (Trac #13032). In the case of an
unliftedequality superclass like d2 above, we generate
case heq_sc d1 of d2 > ...
and we can't (in general) drop that case exrpession in case
d1 is bottom. So it's technically unsound to have added it
in the first place.
* Simply generating all those extra superclasses can generate lots of
code that has to be zonked, only to be discarded later. Better not
to generate it in the first place.
Moreover, if we simplify this implication more than once
(e.g. because we can't solve it completely on the first iteration
of simpl_looop), we'll generate all the same bindings AGAIN!
Easy solution: take advantage of the work we are doing to track dead
(unused) Givens, and use it to prune the Given bindings too. This is
all done by neededEvVars.
This led to a remarkable 25% overall compiler allocation decrease in
test T12227.
Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which
constraints of a type signature (or instance declaration) are
redundant, and can be omitted. Here is an overview of how it
works:
 What is a redundant constraint?
* The things that can be redundant are precisely the Given
constraints of an implication.
* A constraint can be redundant in two different ways:
a) It is implied by other givens. E.g.
f :: (Eq a, Ord a) => blah  Eq a unnecessary
g :: (Eq a, a~b, Eq b) => blah  Either Eq a or Eq b unnecessary
b) It is not needed by the Wanted constraints covered by the
implication E.g.
f :: Eq a => a > Bool
f x = True  Equality not used
* To find (a), when we have two Given constraints,
we must be careful to drop the one that is a naked variable (if poss).
So if we have
f :: (Eq a, Ord a) => blah
then we may find [G] sc_sel (d1::Ord a) :: Eq a
[G] d2 :: Eq a
We want to discard d2 in favour of the superclass selection from
the Ord dictionary. This is done by TcInteract.solveOneFromTheOther
See Note [Replacement vs keeping].
* To find (b) we need to know which evidence bindings are 'wanted';
hence the eb_is_given field on an EvBind.
 How tracking works
* The ic_need fields of an Implic records inscope (given) evidence
variables bound by the context, that were needed to solve this
implication (so far). See the declaration of Implication.
* When the constraint solver finishes solving all the wanteds in
an implication, it sets its status to IC_Solved
 The ics_dead field, of IC_Solved, records the subset of this
implication's ic_given that are redundant (not needed).
* We compute which evidence variables are needed by an implication
in setImplicationStatus. A variable is needed if
a) it is free in the RHS of a Wanted EvBind,
b) it is free in the RHS of an EvBind whose LHS is needed,
c) it is in the ics_need of a nested implication.
* We need to be careful not to discard an implication
prematurely, even one that is fully solved, because we might
thereby forget which variables it needs, and hence wrongly
report a constraint as redundant. But we can discard it once
its free vars have been incorporated into its parent; or if it
simply has no free vars. This careful discarding is also
handled in setImplicationStatus.
 Reporting redundant constraints
* TcErrors does the actual warning, in warnRedundantConstraints.
* We don't report redundant givens for *every* implication; only
for those which reply True to TcSimplify.warnRedundantGivens:
 For example, in a class declaration, the default method *can*
use the class constraint, but it certainly doesn't *have* to,
and we don't want to report an error there.
 More subtly, in a function definition
f :: (Ord a, Ord a, Ix a) => a > a
f x = rhs
we do an ambiguity check on the type (which would find that one
of the Ord a constraints was redundant), and then we check that
the definition has that type (which might find that both are
redundant). We don't want to report the same error twice, so we
disable it for the ambiguity check. Hence using two different
FunSigCtxts, one with the warnredundant field set True, and the
other set False in
 TcBinds.tcSpecPrag
 TcBinds.tcTySig
This decision is taken in setImplicationStatus, rather than TcErrors
so that we can discard implication constraints that we don't need.
So ics_dead consists only of the *reportable* redundant givens.
 Shortcomings
Consider (see Trac #9939)
f2 :: (Eq a, Ord a) => a > a > Bool
 Ord a redundant, but Eq a is reported
f2 x y = (x == y)
We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
really not easy to detect that!
Note [Cutting off simpl_loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is very important not to iterate in simpl_loop unless there is a chance
of progress. Trac #8474 is a classic example:
* There's a deeplynested chain of implication constraints.
?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
* From the innermost one we get a [D] alpha ~ Int,
but alpha is untouchable until we get out to the outermost one
* We float [D] alpha~Int out (it is in floated_eqs), but since alpha
is untouchable, the solveInteract in simpl_loop makes no progress
* So there is no point in attempting to resolve
?yn:betan => [W] ?x:Int
via solveNestedImplications, because we'll just get the
same [D] again
* If we *do* resolve, we'll get an ininite loop. It is cut off by
the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
exponentially many) iterations!
Conclusion: we should call solveNestedImplications only if we did
some unification in solveSimpleWanteds; because that's the only way
we'll get more Givens (a unification is like adding a Given) to
allow the implication to make progress.
}
promoteTyVar :: TcTyVar > TcM Bool
 When we float a constraint out of an implication we must restore
 invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
 Return True <=> we did some promotion
 See Note [Promoting unification variables]
promoteTyVar tv
= do { tclvl < TcM.getTcLevel
; if (isFloatedTouchableMetaTyVar tclvl tv)
then do { cloned_tv < TcM.cloneMetaTyVar tv
; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
; return True }
else return False }
 Returns whether or not *any* tyvar is defaulted
promoteTyVarSet :: TcTyVarSet > TcM Bool
promoteTyVarSet tvs
= or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
 nondeterminism is OK because order of promotion doesn't matter
promoteTyVarTcS :: TcTyVar > TcS ()
 When we float a constraint out of an implication we must restore
 invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
 See Note [Promoting unification variables]
 We don't just call promoteTyVar because we want to use unifyTyVar,
 not writeMetaTyVar
promoteTyVarTcS tv
= do { tclvl < TcS.getTcLevel
; when (isFloatedTouchableMetaTyVar tclvl tv) $
do { cloned_tv < TcS.cloneMetaTyVar tv
; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
; unifyTyVar tv (mkTyVarTy rhs_tv) } }
  Like 'defaultTyVar', but in the TcS monad.
defaultTyVarTcS :: TcTyVar > TcS Bool
defaultTyVarTcS the_tv
 isRuntimeRepVar the_tv
, not (isSigTyVar the_tv)  SigTvs should only be unified with a tyvar
 never with a type; c.f. TcMType.defaultTyVar
 See Note [Kind generalisation and SigTvs]
= do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
; unifyTyVar the_tv liftedRepTy
; return True }
 otherwise
= return False  the common case
approximateWC :: Bool > WantedConstraints > Cts
 Postcondition: Wanted or Derived Cts
 See Note [ApproximateWC]
approximateWC float_past_equalities wc
= float_wc emptyVarSet wc
where
float_wc :: TcTyCoVarSet > WantedConstraints > Cts
float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
= filterBag (is_floatable trapping_tvs) simples `unionBags`
do_bag (float_implic trapping_tvs) implics
where
float_implic :: TcTyCoVarSet > Implication > Cts
float_implic trapping_tvs imp
 float_past_equalities  ic_no_eqs imp
= float_wc new_trapping_tvs (ic_wanted imp)
 otherwise  Take care with equalities
= emptyCts  See (1) under Note [ApproximateWC]
where
new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
do_bag :: (a > Bag c) > Bag a > Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
is_floatable skol_tvs ct
 isGivenCt ct = False
 isHoleCt ct = False
 insolubleEqCt ct = False
 otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
{ Note [ApproximateWC]
~~~~~~~~~~~~~~~~~~~~~~~
approximateWC takes a constraint, typically arising from the RHS of a
letbinding whose type we are *inferring*, and extracts from it some
*simple* constraints that we might plausibly abstract over. Of course
the toplevel simple constraints are plausible, but we also float constraints
out from inside, if they are not captured by skolems.
The same function is used when doing typeclass defaulting (see the call
to applyDefaultingRules) to extract constraints that that might be defaulted.
There is one caveat:
1. When infering mostgeneral types (in simplifyInfer), we do *not*
float anything out if the implication binds equality constraints,
because that defeats the OutsideIn story. Consider
data T a where
TInt :: T Int
MkT :: T a
f TInt = 3::Int
We get the implication (a ~ Int => res ~ Int), where so far we've decided
f :: T a > res
We don't want to float (res~Int) out because then we'll infer
f :: T a > Int
which is only on of the possible types. (GHC 7.6 accidentally *did*
float out of such implications, which meant it would happily infer
nonprincipal types.)
HOWEVER (Trac #12797) in findDefaultableGroups we are not worried about
the mostgeneral type; and we /do/ want to float out of equalities.
Hence the boolean flag to approximateWC.
 Historical note 
There used to be a second caveat, driven by Trac #8155
2. We do not float out an inner constraint that shares a type variable
(transitively) with one that is trapped by a skolem. Eg
forall a. F a ~ beta, Integral beta
We don't want to float out (Integral beta). Doing so would be bad
when defaulting, because then we'll default beta:=Integer, and that
makes the error message much worse; we'd get
Can't solve F a ~ Integer
rather than
Can't solve Integral (F a)
Moreover, floating out these "contaminated" constraints doesn't help
when generalising either. If we generalise over (Integral b), we still
can't solve the retained implication (forall a. F a ~ b). Indeed,
arguably that too would be a harder error to understand.
But this transitive closure stuff gives rise to a complex rule for
when defaulting actually happens, and one that was never documented.
Moreover (Trac #12923), the more complex rule is sometimes NOT what
you want. So I simply removed the extra code to implement the
contamination stuff. There was zero effect on the testsuite (not even
#8155).
 End of historical note 
Note [DefaultTyVar]
~~~~~~~~~~~~~~~~~~~
defaultTyVar is used on any uninstantiated meta type variables to
default any RuntimeRep variables to LiftedRep. This is important
to ensure that instance declarations match. For example consider
instance Show (a>b)
foo x = show (\_ > True)
Then we'll get a constraint (Show (p >q)) where p has kind (TYPE r),
and that won't match the typeKind (*) in the instance decl. See tests
tc217 and tc175.
We look only at touchable type variables. No further constraints
are going to affect these type variables, so it's time to do it by
hand. However we aren't ready to default them fully to () or
whatever, because the typeclass defaulting rules have yet to run.
An alternate implementation would be to emit a derived constraint setting
the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect.
Note [Promote _and_ default when inferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we are inferring a type, we simplify the constraint, and then use
approximateWC to produce a list of candidate constraints. Then we MUST
a) Promote any metatyvars that have been floated out by
approximateWC, to restore invariant (WantedInv) described in
Note [TcLevel and untouchable type variables] in TcType.
b) Default the kind of any metatyvars that are not mentioned in
in the environment.
To see (b), suppose the constraint is (C ((a :: OpenKind) > Int)), and we
have an instance (C ((x:*) > Int)). The instance doesn't match  but it
should! If we don't solve the constraint, we'll stupidly quantify over
(C (a>Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
(b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
Trac #7641 is a simpler example.
Note [Promoting unification variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we float an equality out of an implication we must "promote" free
unification variables of the equality, in order to maintain Invariant
(WantedInv) from Note [TcLevel and untouchable type variables] in
TcType. for the leftover implication.
This is absolutely necessary. Consider the following example. We start
with two implications and a class with a functional dependency.
class C x y  x > y
instance C [a] [a]
(I1) [untch=beta]forall b. 0 => F Int ~ [beta]
(I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
They may react to yield that (beta := [alpha]) which can then be pushed inwards
the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
class C x y  x > y where
op :: x > y > ()
instance C [a] [a]
type family F a :: *
h :: F Int > ()
h = undefined
data TEx where
TEx :: a > TEx
f (x::beta) =
let g1 :: forall b. b > ()
g1 _ = h [x]
g2 z = case z of TEx y > (h [[undefined]], op x [y])
in (g1 '3', g2 undefined)
*********************************************************************************
* *
* Floating equalities *
* *
*********************************************************************************
Note [Float Equalities out of Implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For ordinary pattern matches (including existentials) we float
equalities out of implications, for instance:
data T where
MkT :: Eq a => a > T
f x y = case x of MkT _ > (y::Int)
We get the implication constraint (x::T) (y::alpha):
forall a. [untouchable=alpha] Eq a => alpha ~ Int
We want to float out the equality into a scope where alpha is no
longer untouchable, to solve the implication!
But we cannot float equalities out of implications whose givens may
yield or contain equalities:
data T a where
T1 :: T Int
T2 :: T Bool
T3 :: T a
h :: T a > a > Int
f x y = case x of
T1 > y::Int
T2 > y::Bool
T3 > h x y
We generate constraint, for (x::T alpha) and (y :: beta):
[untouchables = beta] (alpha ~ Int => beta ~ Int)  From 1st branch
[untouchables = beta] (alpha ~ Bool => beta ~ Bool)  From 2nd branch
(alpha ~ beta)  From 3rd branch
If we float the equality (beta ~ Int) outside of the first implication and
the equality (beta ~ Bool) out of the second we get an insoluble constraint.
But if we just leave them inside the implications, we unify alpha := beta and
solve everything.
Principle:
We do not want to float equalities out which may
need the given *evidence* to become soluble.
Consequence: classes with functional dependencies don't matter (since there is
no evidence for a fundep equality), but equality superclasses do matter (since
they carry evidence).
}
floatEqualities :: [TcTyVar] > [EvId] > EvBindsVar > Bool
> WantedConstraints
> TcS (Cts, WantedConstraints)
 Main idea: see Note [Float Equalities out of Implications]

 Precondition: the wc_simple of the incoming WantedConstraints are
 fully zonked, so that we can see their free variables

 Postcondition: The returned floated constraints (Cts) are only
 Wanted or Derived

 Also performs some unifications (via promoteTyVar), adding to
 monadicallycarried ty_binds. These will be used when processing
 floated_eqs later

 Subtleties: Note [Float equalities from under a skolem binding]
 Note [Skolem escape]
 Note [What prevents a constraint from floating]
floatEqualities skols given_ids ev_binds_var no_given_eqs
wanteds@(WC { wc_simple = simples })
 not no_given_eqs  There are some given equalities, so don't float
= return (emptyBag, wanteds)  Note [Float Equalities out of Implications]
 otherwise
= do {  First zonk: the inert set (from whence they came) is fully
 zonked, but unflattening may have filled in unification
 variables, and we /must/ see them. Otherwise we may float
 constraints that mention the skolems!
simples < TcS.zonkSimples simples
; binds < TcS.getTcEvBindsMap ev_binds_var
 Now we can pick the ones to float
 The constraints are unflattened and decanonicalised
; let seed_skols = mkVarSet skols `unionVarSet`
mkVarSet given_ids `unionVarSet`
foldEvBindMap add_one emptyVarSet binds
add_one bind acc = extendVarSet acc (evBindVar bind)
 seed_skols: See Note [What prevents a constraint from floating] (1,2,3)
(eqs, non_eqs) = partitionBag is_eq_ct simples
extended_skols = transCloVarSet (extra_skols eqs) seed_skols
(flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) eqs
remaining_simples = non_eqs `andCts` no_flt_eqs
 extended_skols: See Note [What prevents a constraint from floating] (3)
 Promote any unification variables mentioned in the floated equalities
 See Note [Promoting unification variables]
; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs)
; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols
, text "Extended skols =" <+> ppr extended_skols
, text "Simples =" <+> ppr simples
, text "Eqs =" <+> ppr eqs
, text "Floated eqs =" <+> ppr flt_eqs])
; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) }
where
is_floatable :: VarSet > Ct > Bool
is_floatable skols ct
 isDerivedCt ct = not (tyCoVarsOfCt ct `intersectsVarSet` skols)
 otherwise = not (ctEvId ct `elemVarSet` skols)
is_eq_ct ct  CTyEqCan {} < ct = True
 is_homo_eq (ctPred ct) = True
 otherwise = False
extra_skols :: Cts > VarSet > VarSet
extra_skols eqs skols = foldrBag extra_skol emptyVarSet eqs
where
extra_skol ct acc
 isDerivedCt ct = acc
 tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct)
 otherwise = acc
 Float out alpha ~ ty, or ty ~ alpha
 which might be unified outside
 See Note [Which equalities to float]
is_homo_eq pred
 EqPred NomEq ty1 ty2 < classifyPredType pred
, typeKind ty1 `tcEqType` typeKind ty2
= case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
(Just tv1, _) > float_tv_eq tv1 ty2
(_, Just tv2) > float_tv_eq tv2 ty1
_ > False
 otherwise
= False
float_tv_eq tv1 ty2  See Note [Which equalities to float]
= isMetaTyVar tv1
&& (not (isSigTyVar tv1)  isTyVarTy ty2)
{ Note [Float equalities from under a skolem binding]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which of the simple equalities can we float out? Obviously, only
ones that don't mention the skolembound variables. But that is
overeager. Consider
[2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int
The second constraint doesn't mention 'a'. But if we float it,
we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that
beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll
we left with the constraint
[2] forall a. a ~ gamma'[1]
which is insoluble because gamma became untouchable.
Solution: float only constraints that stand a jolly good chance of
being soluble simply by being floated, namely ones of form
a ~ ty
where 'a' is a currentlyuntouchable unification variable, but may
become touchable by being floated (perhaps by more than one level).
We had a very complicated rule previously, but this is nice and
simple. (To see the notes, look at this Note in a version of
TcSimplify prior to Oct 2014).
Note [Which equalities to float]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Which equalities should we float? We want to float ones where there
is a decent chance that floating outwards will allow unification to
happen. In particular:
Float out homogeneous equalities of form (alpha ~ ty) or (ty ~ alpha), where
* alpha is a metatyvar.
* And 'alpha' is not a SigTv with 'ty' being a nontyvar. In that
case, floating out won't help either, and it may affect grouping
of error messages.
Why homogeneous (i.e., the kinds of the types are the same)? Because heterogeneous
equalities have derived kind equalities. See Note [Equalities with incompatible kinds]
in TcCanonical. If we float out a hetero equality, then it will spit out the
same derived kind equality again, which might create duplicate error messages.
Instead, we do float out the kind equality (if it's worth floating out, as
above). If/when we solve it, we'll be able to rewrite the original hetero equality
to be homogeneous, and then perhaps make progress / float it out. The duplicate
error message was spotted in typecheck/should_fail/T7368.
Note [Skolem escape]
~~~~~~~~~~~~~~~~~~~~
You might worry about skolem escape with all this floating.
For example, consider
[2] forall a. (a ~ F beta[2] delta,
Maybe beta[2] ~ gamma[1])
The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
solve with gamma := beta. But what if later delta:=Int, and
F b Int = b.
Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
skolem has escaped!
But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
Note [What prevents a constraint from floating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What /prevents/ a constraint from floating? If it mentions one of the
"bound variables of the implication". What are they?
The "bound variables of the implication" are
1. The skolem type variables `ic_skols`
2. The "given" evidence variables `ic_given`. Example:
forall a. (co :: t1 ~# t2) => [W] co : (a ~# b > co)
3. The binders of all evidence bindings in `ic_binds`. Example
forall a. (d :: t1 ~ t2)
EvBinds { (co :: t1 ~# t2) = superclasssel d }
=> [W] co2 : (a ~# b > co)
Here `co` is gotten by superclass selection from `d`, and the
wanted constraint co2 must not float.
4. And the evidence variable of any equality constraint (incl
Wanted ones) whose type mentions a bound variable. Example:
forall k. [W] co1 :: t1 ~# t2 > co2
[W] co2 :: k ~# *
Here, since `k` is bound, so is `co2` and hence so is `co1`.
Here (1,2,3) are handled by the "seed_skols" calculation, and
(4) is done by the transCloVarSet call.
The possible dependence on givens, and evidence bindings, is more
subtle than we'd realised at first. See Trac #14584.
*********************************************************************************
* *
* Defaulting and disambiguation *
* *
*********************************************************************************
}
applyDefaultingRules :: WantedConstraints > TcS Bool
 True <=> I did some defaulting, by unifying a metatyvar
 Input WantedConstraints are not necessarily zonked
applyDefaultingRules wanteds
 isEmptyWC wanteds
= return False
 otherwise
= do { info@(default_tys, _) < getDefaultInfo
; wanteds < TcS.zonkWC wanteds
; let groups = findDefaultableGroups info wanteds
; traceTcS "applyDefaultingRules {" $
vcat [ text "wanteds =" <+> ppr wanteds
, text "groups =" <+> ppr groups
, text "info =" <+> ppr info ]
; something_happeneds < mapM (disambigGroup default_tys) groups
; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
; return (or something_happeneds) }
findDefaultableGroups
:: ( [Type]
, (Bool,Bool) )  (Overloaded strings, extended default rules)
> WantedConstraints  Unsolved (wanted or derived)
> [(TyVar, [Ct])]
findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
 null default_tys
= []
 otherwise
= [ (tv, map fstOf3 group)
 group'@((_,_,tv) : _) < unary_groups
, let group = toList group'
, defaultable_tyvar tv
, defaultable_classes (map sndOf3 group) ]
where
simples = approximateWC True wanteds
(unaries, non_unaries) = partitionWith find_unary (bagToList simples)
unary_groups = equivClasses cmp_tv unaries
unary_groups :: [NonEmpty (Ct, Class, TcTyVar)]  (C tv) constraints
unaries :: [(Ct, Class, TcTyVar)]  (C tv) constraints
non_unaries :: [Ct]  and *other* constraints
 Finds unary typeclass constraints
 But take account of polykinded classes like Typeable,
 which may look like (Typeable * (a:*)) (Trac #8931)
find_unary :: Ct > Either (Ct, Class, TyVar) Ct
find_unary cc
 Just (cls,tys) < getClassPredTys_maybe (ctPred cc)
, [ty] < filterOutInvisibleTypes (classTyCon cls) tys
 Ignore invisible arguments for this purpose
, Just tv < tcGetTyVar_maybe ty
, isMetaTyVar tv  We might have runtimeskolems in GHCi, and
 we definitely don't want to try to assign to those!
= Left (cc, cls, tv)
find_unary cc = Right cc  Non unary or non dictionary
bad_tvs :: TcTyCoVarSet  TyVars mentioned by nonunaries
bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
defaultable_tyvar :: TcTyVar > Bool
defaultable_tyvar tv
= let b1 = isTyConableTyVar tv  Note [Avoiding spurious errors]
b2 = not (tv `elemVarSet` bad_tvs)
in b1 && (b2  extended_defaults)  Note [Multiparameter defaults]
defaultable_classes :: [Class] > Bool
defaultable_classes clss
 extended_defaults = any (isInteractiveClass ovl_strings) clss
 otherwise = all is_std_class clss && (any (isNumClass ovl_strings) clss)
 is_std_class adds IsString to the standard numeric classes,
 when foverloadedstrings is enabled
is_std_class cls = isStandardClass cls 
(ovl_strings && (cls `hasKey` isStringClassKey))

disambigGroup :: [Type]  The default types
> (TcTyVar, [Ct])  All classes of the form (C a)
 sharing same type variable
> TcS Bool  True <=> something happened, reflected in ty_binds
disambigGroup [] _
= return False
disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
= do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
; fake_ev_binds_var < TcS.newTcEvBinds
; tclvl < TcS.getTcLevel
; success < nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
; if success then
 Success: record the type variable binding, and return
do { unifyTyVar the_tv default_ty
; wrapWarnTcS $ warnDefaulting wanteds default_ty
; traceTcS "disambigGroup succeeded }" (ppr default_ty)
; return True }
else
 Failure: try with the next type
do { traceTcS "disambigGroup failed, will try other default types }"
(ppr default_ty)
; disambigGroup default_tys group } }
where
try_group
 Just subst < mb_subst
= do { lcl_env < TcS.getLclEnv
; tc_lvl < TcS.getTcLevel
; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
; wanted_evs < mapM (newWantedEvVarNC loc . substTy subst . ctPred)
wanteds
; fmap isEmptyWC $
solveSimpleWanteds $ listToBag $
map mkNonCanonical wanted_evs }
 otherwise
= return False
the_ty = mkTyVarTy the_tv
mb_subst = tcMatchTyKi the_ty default_ty
 Make sure the kinds match too; hence this call to tcMatchTyKi
 E.g. suppose the only constraint was (Typeable k (a::k))
 With the addition of polykinded defaulting we also want to reject
 illkinded defaulting attempts like (Eq []) or (Foldable Int) here.
 In interactive mode, or with XExtendedDefaultRules,
 we default Show a to Show () to avoid graututious errors on "show []"
isInteractiveClass :: Bool  XOverloadedStrings?
> Class > Bool
isInteractiveClass ovl_strings cls
= isNumClass ovl_strings cls  (classKey cls `elem` interactiveClassKeys)
 isNumClass adds IsString to the standard numeric classes,
 when foverloadedstrings is enabled
isNumClass :: Bool  XOverloadedStrings?
> Class > Bool
isNumClass ovl_strings cls
= isNumericClass cls  (ovl_strings && (cls `hasKey` isStringClassKey))
{
Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
type variables, and simply don't default them. For example:
f = (*)  Monomorphic
g :: Num a => a > a
g x = f x x
Here, we get a complaint when checking the type signature for g,
that g isn't polymorphic enough; but then we get another one when
dealing with the (Num a) context arising from f's definition;
we try to unify a with Int (to default it), but find that it's
already been unified with the rigid variable from g's type sig.
Note [Multiparameter defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With XExtendedDefaultRules, we default only based on singlevariable
constraints, but do not exclude from defaulting any type variables which also
appear in multivariable constraints. This means that the following will
default properly:
default (Integer, Double)
class A b (c :: Symbol) where
a :: b > Proxy c
instance A Integer c where a _ = Proxy
main = print (a 5 :: Proxy "5")
Note that if we change the above instance ("instance A Integer") to
"instance A Double", we get an error:
No instance for (A Integer "5")
This is because the first defaulted type (Integer) has successfully satisfied
its singleparameter constraints (in this case Num).
}
diff git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 26fc9fe..092c5a1 100644
 a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ 1,2699 +1,2712 @@
{
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 19921998
\section[TcType]{Types used in the typechecker}
This module provides the Type interface for frontend parts of the
compiler. These parts
* treat "source types" as opaque:
newtypes, and predicates are meaningful.
* look through usage types
The "tc" prefix is for "TypeChecker", because the type checker
is the principal client.
}
{# LANGUAGE CPP, ScopedTypeVariables, MultiWayIf, FlexibleContexts #}
module TcType (

 Types
TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcTyCon,
ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
SyntaxOpType(..), synKnownType, mkSynFunTys,
 TcLevel
TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
strictlyDeeperThan, sameDepthAs,
tcTypeLevel, tcTyVarLevel, maxTcLevel,
promoteSkolem, promoteSkolemX, promoteSkolemsX,

 MetaDetails
UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe,
TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
MetaDetails(Flexi, Indirect), MetaInfo(..),
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
isSigTyVar, isOverlappableTyVar, isTyConableTyVar,
isFskTyVar, isFmvTyVar, isFlattenTyVar,
isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
isTouchableMetaTyVar,
isFloatedTouchableMetaTyVar,
findDupSigTvs, mkTyVarNamePairs,

 Builders
mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
mkNakedCastTy,

 Splitters
 These are important because they do not look through newtypes
getTyVar,
tcSplitForAllTy_maybe,
tcSplitForAllTys, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBndrs,
tcSplitPhiTy, tcSplitPredFunTy_maybe,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
tcSplitFunTysN,
tcSplitTyConApp, tcSplitTyConApp_maybe,
tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
tcRepGetNumAppTys,
tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,

 Predicates.
 Again, newtypes are opaque
eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck,
checkValidClsArgs, hasTyVarHead,
isRigidTy,

 Misc type manipulators
deNoteType,
orphNamesOfType, orphNamesOfCo,
orphNamesOfTypes, orphNamesOfCoCon,
getDFunTyKey,
evVarPred_maybe, evVarPred,

 Predicate types
mkMinimalBySCs, transSuperClasses,
pickQuantifiablePreds, pickCapturedPreds,
immSuperClasses,
isImprovementPred,
 * Finding type instances
tcTyFamInsts, isTyFamFree,
 * Finding "exact" (nondead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..),
anyRewritableTyVar,

 Foreign import and export
isFFIArgumentTy,  :: DynFlags > Safety > Type > Bool
isFFIImportResultTy,  :: DynFlags > Type > Bool
isFFIExportResultTy,  :: Type > Bool
isFFIExternalTy,  :: Type > Bool
isFFIDynTy,  :: Type > Type > Bool
isFFIPrimArgumentTy,  :: DynFlags > Type > Bool
isFFIPrimResultTy,  :: DynFlags > Type > Bool
isFFILabelTy,  :: Type > Bool
isFFITy,  :: Type > Bool
isFunPtrTy,  :: Type > Bool
tcSplitIOType_maybe,  :: Type > Maybe Type

 Rexported from Kind
Kind, typeKind,
liftedTypeKind,
constraintKind,
isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,

 Rexported from Type
Type, PredType, ThetaType, TyBinder, ArgFlag(..),
mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkInvForAllTy,
mkFunTy, mkFunTys,
mkTyConApp, mkAppTy, mkAppTys,
mkTyConTy, mkTyVarTy,
mkTyVarTys,
isClassPred, isEqPred, isNomEqPred, isIPPred,
mkClassPred,
isDictLikeTy,
tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
isRuntimeRepVar, isKindLevPoly,
isVisibleBinder, isInvisibleBinder,
 Type substitutions
TCvSubst(..),  Representation visible to a few friends
TvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
zipTvSubst,
mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
Type.extendTvSubst,
isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
Type.substTy, substTys, substTyWith, substTyWithCoVars,
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTheta,
isUnliftedType,  Source types are always lifted
isUnboxedTupleType,  Ditto
isPrimitiveType,
tcView, coreView,
tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
tyCoFVsOfType, tyCoFVsOfTypes,
tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
tyCoVarsOfTypeList, tyCoVarsOfTypesList,
noFreeVarsOfType,

pprKind, pprParendKind, pprSigmaType,
pprType, pprParendType, pprTypeApp, pprTyThingCategory, tyThingCategory,
pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred,
pprTvBndr, pprTvBndrs,
TypeSize, sizeType, sizeTypes, toposortTyVars,

 argument visibility
tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
) where
#include "HsVersions.h"
 friends:
import GhcPrelude
import Kind
import TyCoRep
import Class
import Var
import ForeignCall
import VarSet
import Coercion
import Type
import RepType
import TyCon
 others:
import DynFlags
import CoreFVs
import Name  hiding (varName)
 We use this to make dictionaries for type literals.
 Perhaps there's a better way to do this?
import NameSet
import VarEnv
import PrelNames
import TysWiredIn( coercibleClass, unitTyCon, unitTyConKey
, listTyCon, constraintKind )
import BasicTypes
import Util
import Maybes
import ListSetOps ( getNth, findDupsEq )
import Outputable
import FastString
import ErrUtils( Validity(..), MsgDoc, isValid )
import qualified GHC.LanguageExtensions as LangExt
import Data.List ( mapAccumL )
import Data.IORef
import Data.List.NonEmpty( NonEmpty(..) )
import qualified Data.Semigroup as Semi
{
************************************************************************
* *
Types
* *
************************************************************************
The type checker divides the generic Type world into the
following more structured beasts:
sigma ::= forall tyvars. phi
 A sigma type is a qualified type

 Note that even if 'tyvars' is empty, theta
 may not be: e.g. (?x::Int) => Int
 Note that 'sigma' is in prenex form:
 all the foralls are at the front.
 A 'phi' type has no foralls to the right of
 an arrow
phi :: theta => rho
rho ::= sigma > rho
 tau
 A 'tau' type has no quantification anywhere
 Note that the args of a type constructor must be taus
tau ::= tyvar
 tycon tau_1 .. tau_n
 tau_1 tau_2
 tau_1 > tau_2
 In all cases, a (saturated) type synonym application is legal,
 provided it expands to the required form.
Note [TcTyVars and TyVars in the typechecker]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The typechecker uses a lot of type variables with special properties,
notably being a unification variable with a mutable reference. These
use the 'TcTyVar' variant of Var.Var.
Note, though, that a /bound/ type variable can (and probably should)
be a TyVar. E.g
forall a. a > a
Here 'a' is really just a deBruijnnumber; it certainly does not have
a signficant TcLevel (as every TcTyVar does). So a forallbound type
variable should be TyVars; and hence a TyVar can appear free in a TcType.
The type checker and constraint solver can also encounter /free/ type
variables that use the 'TyVar' variant of Var.Var, for a couple of
reasons:
 When typechecking a class decl, say
class C (a :: k) where
foo :: T a > Int
We have first kindcheck the header; fix k and (a:k) to be
TyVars, bring 'k' and 'a' into scope, and kind check the
signature for 'foo'. In doing so we call solveEqualities to
solve any kind equalities in foo's signature. So the solver
may see free occurrences of 'k'.
See calls to tcExtendTyVarEnv for other places that ordinary
TyVars are bought into scope, and hence may show up in the types
and kinds generated by TcHsType.
 The patternmatch overlap checker calls the constraint solver,
long afer TcTyVars have been zonked away
It's convenient to simply treat these TyVars as skolem constants,
which of course they are. We give them a level number of "outermost",
so they behave as global constants. Specifically:
* Var.tcTyVarDetails succeeds on a TyVar, returning
vanillaSkolemTv, as well as on a TcTyVar.
* tcIsTcTyVar returns True for both TyVar and TcTyVar variants
of Var.Var. The "tc" prefix means "a type variable that can be
encountered by the typechecker".
This is a bit of a change from an earlier era when we remoselessly
insisted on real TcTyVars in the type checker. But that seems
unnecessary (for skolems, TyVars are fine) and it's now very hard
to guarantee, with the advent of kind equalities.
Note [Coercion variables in free variable lists]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are several places in the GHC codebase where functions like
tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type
variables of a type. The "Co" part of these functions' names shouldn't be
dismissed, as it is entirely possible that they will include coercion variables
in addition to type variables! As a result, there are some places in TcType
where we must take care to check that a variable is a _type_ variable (using
isTyVar) before calling tcTyVarDetailsa partial function that is not defined
for coercion variableson the variable. Failing to do so led to
GHC Trac #12785.
}
 See Note [TcTyVars and TyVars in the typechecker]
type TcCoVar = CoVar  Used only during type inference
type TcType = Type  A TcType can have mutable type variables
type TcTyCoVar = Var  Either a TcTyVar or a CoVar
 Invariant on ForAllTy in TcTypes:
 forall a. T
 a cannot occur inside a MutTyVar in T; that is,
 T is "flattened" before quantifying over a
type TcTyVarBinder = TyVarBinder
type TcTyCon = TyCon  these can be the TcTyCon constructor
 These types do not have boxy type variables in them
type TcPredType = PredType
type TcThetaType = ThetaType
type TcSigmaType = TcType
type TcRhoType = TcType  Note [TcRhoType]
type TcTauType = TcType
type TcKind = Kind
type TcTyVarSet = TyVarSet
type TcTyCoVarSet = TyCoVarSet
type TcDTyVarSet = DTyVarSet
type TcDTyCoVarSet = DTyCoVarSet
{ *********************************************************************
* *
ExpType: an "expected type" in the type checker
* *
********************************************************************* }
  An expected type to check against during typechecking.
 See Note [ExpType] in TcMType, where you'll also find manipulators.
data ExpType = Check TcType
 Infer !InferResult
data InferResult
= IR { ir_uniq :: Unique  For debugging only
, ir_lvl :: TcLevel  See Note [TcLevel of ExpType] in TcMType
, ir_inst :: Bool  True <=> deeply instantiate before returning
 i.e. return a RhoType
 False <=> do not instantiate before returning
 i.e. return a SigmaType
, ir_ref :: IORef (Maybe TcType) }
 The type that fills in this hole should be a Type,
 that is, its kind should be (TYPE rr) for some rr
type ExpSigmaType = ExpType
type ExpRhoType = ExpType
instance Outputable ExpType where
ppr (Check ty) = text "Check" <> braces (ppr ty)
ppr (Infer ir) = ppr ir
instance Outputable InferResult where
ppr (IR { ir_uniq = u, ir_lvl = lvl
, ir_inst = inst })
= text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
  Make an 'ExpType' suitable for checking.
mkCheckExpType :: TcType > ExpType
mkCheckExpType = Check
{ *********************************************************************
* *
SyntaxOpType
* *
********************************************************************* }
  What to expect for an argument to a rebindablesyntax operator.
 Quite like 'Type', but allows for holes to be filled in by tcSyntaxOp.
 The callback called from tcSyntaxOp gets a list of types; the meaning
 of these types is determined by a lefttoright depthfirst traversal
 of the 'SyntaxOpType' tree. So if you pass in

 > SynAny `SynFun` (SynList `SynFun` SynType Int) `SynFun` SynAny

 you'll get three types back: one for the first 'SynAny', the /element/
 type of the list, and one for the last 'SynAny'. You don't get anything
 for the 'SynType', because you've said positively that it should be an
 Int, and so it shall be.

 This is defined here to avoid defining it in TcExpr.hsboot.
data SyntaxOpType
= SynAny  ^ Any type
 SynRho  ^ A rho type, deeply skolemised or instantiated as appropriate
 SynList  ^ A list type. You get back the element type of the list
 SynFun SyntaxOpType SyntaxOpType
 ^ A function.
 SynType ExpType  ^ A known type.
infixr 0 `SynFun`
  Like 'SynType' but accepts a regular TcType
synKnownType :: TcType > SyntaxOpType
synKnownType = SynType . mkCheckExpType
  Like 'mkFunTys' but for 'SyntaxOpType'
mkSynFunTys :: [SyntaxOpType] > ExpType > SyntaxOpType
mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys
{
Note [TcRhoType]
~~~~~~~~~~~~~~~~
A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
YES (forall a. a>a) > Int
NO forall a. a > Int
NO Eq a => a > a
NO Int > forall a. a > Int
************************************************************************
* *
TyVarDetails, MetaDetails, MetaInfo
* *
************************************************************************
TyVarDetails gives extra info about type variables, used during type
checking. It's attached to mutable type variables only.
It's knottied back to Var.hs. There is no reason in principle
why Var.hs shouldn't actually have the definition, but it "belongs" here.
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
A SigTv is a specialised variant of TauTv, with the following invarints:
* A SigTv can be unified only with a TyVar,
not with any other type
* Its MetaDetails, if filled in, will always be another SigTv
or a SkolemTv
SigTvs are only distinguished to improve error messages.
Consider this
f :: forall a. [a] > Int
f (x::b : xs) = 3
Here 'b' is a lexically scoped type variable, but it turns out to be
the same as the skolem 'a'. So we make them both SigTvs, which can unify
with each other.
Similarly consider
data T (a:k1) = MkT (S a)
data S (b:k2) = MkS (T b)
When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
because they end up unifying; we want those SigTvs again.
SigTvs are used *only* for pattern type signatures.
Note [TyVars and TcTyVars during type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The Var type has constructors TyVar and TcTyVar. They are used
as follows:
* TcTyVar: used /only/ during type checking. Should never appear
afterwards. May contain a mutable field, in the MetaTv case.
* TyVar: is never seen by the constraint solver, except locally
inside a type like (forall a. [a] >[a]), where 'a' is a TyVar.
We instantiate these with TcTyVars before exposing the type
to the constraint solver.
I have swithered about the latter invariant, excluding TyVars from the
constraint solver. It's not strictly essential, and indeed
(historically but still there) Var.tcTyVarDetails returns
vanillaSkolemTv for a TyVar.
But ultimately I want to seeparate Type from TcType, and in that case
we would need to enforce the separation.
}
 A TyVarDetails is inside a TyVar
 See Note [TyVars and TcTyVars]
data TcTyVarDetails
= SkolemTv  A skolem
TcLevel  Level of the implication that binds it
 See TcUnify Note [Deeper level on the left] for
 how this level number is used
Bool  True <=> this skolem type variable can be overlapped
 when looking up instances
 See Note [Binding when looking up instances] in InstEnv
 RuntimeUnk  Stands for an asyetunknown type in the GHCi
 interactive context
 MetaTv { mtv_info :: MetaInfo
, mtv_ref :: IORef MetaDetails
, mtv_tclvl :: TcLevel }  See Note [TcLevel and untouchable type variables]
vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
 See Note [Binding when looking up instances] in InstEnv
vanillaSkolemTv = SkolemTv topTcLevel False  Might be instantiated
superSkolemTv = SkolemTv topTcLevel True  Treat this as a completely distinct type
 The choice of level number here is a bit dodgy, but
 topTcLevel works in the places that vanillaSkolemTv is used

data MetaDetails
= Flexi  Flexi type variables unify to become Indirects
 Indirect TcType
data MetaInfo
= TauTv  This MetaTv is an ordinary unification variable
 A TauTv is always filled in with a tautype, which
 never contains any ForAlls.
 SigTv  A variant of TauTv, except that it should not be
 unified with a type, only with a type variable
 See Note [Signature skolems]
 FlatMetaTv  A flatten metatyvar
 It is a metatyvar, but it is always untouchable, with level 0
 See Note [The flattening story] in TcFlatten
 FlatSkolTv  A flatten skolem tyvar
 Just like FlatMetaTv, but is comletely "owned" by
 its Given CFunEqCan.
 It is filled in /only/ by unflattenGivens
 See Note [The flattening story] in TcFlatten
instance Outputable MetaDetails where
ppr Flexi = text "Flexi"
ppr (Indirect ty) = text "Indirect" <+> ppr ty
pprTcTyVarDetails :: TcTyVarDetails > SDoc
 For debugging
pprTcTyVarDetails (RuntimeUnk {}) = text "rt"
pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl
pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl
pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
= pp_info <> colon <> ppr tclvl
where
pp_info = case info of
TauTv > text "tau"
SigTv > text "sig"
FlatMetaTv > text "fmv"
FlatSkolTv > text "fsk"
{ *********************************************************************
* *
UserTypeCtxt
* *
********************************************************************* }

 UserTypeCtxt describes the origin of the polymorphic type
 in the places where we need to an expression has that type
data UserTypeCtxt
= FunSigCtxt  Function type signature, when checking the type
 Also used for types in SPECIALISE pragmas
Name  Name of the function
Bool  True <=> report redundant constraints
 This is usually True, but False for
 * Record selectors (not important here)
 * Class and instance methods. Here
 the code may legitimately be more
 polymorphic than the signature
 generated from the class
 declaration
 InfSigCtxt Name  Inferred type for function
 ExprSigCtxt  Expression type signature
 KindSigCtxt  Kind signature
 TypeAppCtxt  Visible type application
 ConArgCtxt Name  Data constructor argument
 TySynCtxt Name  RHS of a type synonym decl
 PatSynCtxt Name  Type sig for a pattern synonym
 PatSigCtxt  Type sig in pattern
 eg f (x::t) = ...
 or (x::t, y) = e
 RuleSigCtxt Name  LHS of a RULE forall
 RULE "foo" forall (x :: a > a). f (Just x) = ...
 ResSigCtxt  Result type sig
 f x :: t = ....
 ForSigCtxt Name  Foreign import or export signature
 DefaultDeclCtxt  Types in a default declaration
 InstDeclCtxt  An instance declaration
 SpecInstCtxt  SPECIALISE instance pragma
 ThBrackCtxt  Template Haskell type brackets [t ... ]
 GenSigCtxt  Higherrank or impredicative situations
 e.g. (f e) where f has a higherrank type
 We might want to elaborate this
 GhciCtxt  GHCi command :kind
 ClassSCCtxt Name  Superclasses of a class
 SigmaCtxt  Theta part of a normal forall type
 f :: => a > a
 DataTyCtxt Name  The "stupid theta" part of a data decl
 data => T a = MkT a
 DerivClauseCtxt  A 'deriving' clause
 TyVarBndrKindCtxt Name  The kind of a type variable being bound
 DataKindCtxt Name  The kind of a data/newtype (instance)
 TySynKindCtxt Name  The kind of the RHS of a type synonym
 TyFamResKindCtxt Name  The result kind of a type family
{
 Notes re TySynCtxt
 We allow type synonyms that aren't types; e.g. type List = []

 If the RHS mentions tyvars that aren't in scope, we'll
 quantify over them:
 e.g. type T = a>a
 will become type T = forall a. a>a

 With glaexts that's right, but for H98 we should complain.
}
pprUserTypeCtxt :: UserTypeCtxt > SDoc
pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n)
pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n)
pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt = text "an expression type signature"
pprUserTypeCtxt KindSigCtxt = text "a kind signature"
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t...]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt = text "a type in a `default' declaration"
pprUserTypeCtxt InstDeclCtxt = text "an instance declaration"
pprUserTypeCtxt SpecInstCtxt = text "a SPECIALISE instance pragma"
pprUserTypeCtxt GenSigCtxt = text "a type expected by the context"
pprUserTypeCtxt GhciCtxt = text "a type in a GHCi command"
pprUserTypeCtxt (ClassSCCtxt c) = text "the superclasses of class" <+> quotes (ppr c)
pprUserTypeCtxt SigmaCtxt = text "the context of a polymorphic type"
pprUserTypeCtxt (DataTyCtxt tc) = text "the context of the data type declaration for" <+> quotes (ppr tc)
pprUserTypeCtxt (PatSynCtxt n) = text "the signature for pattern synonym" <+> quotes (ppr n)
pprUserTypeCtxt (DerivClauseCtxt) = text "a `deriving' clause"
pprUserTypeCtxt (TyVarBndrKindCtxt n) = text "the kind annotation on the type variable" <+> quotes (ppr n)
pprUserTypeCtxt (DataKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n)
pprUserTypeCtxt (TySynKindCtxt n) = text "the kind annotation on the declaration for" <+> quotes (ppr n)
pprUserTypeCtxt (TyFamResKindCtxt n) = text "the result kind for" <+> quotes (ppr n)
isSigMaybe :: UserTypeCtxt > Maybe Name
isSigMaybe (FunSigCtxt n _) = Just n
isSigMaybe (ConArgCtxt n) = Just n
isSigMaybe (ForSigCtxt n) = Just n
isSigMaybe (PatSynCtxt n) = Just n
isSigMaybe _ = Nothing
{ *********************************************************************
* *
Untoucable type variables
* *
********************************************************************* }
newtype TcLevel = TcLevel Int deriving( Eq, Ord )
 See Note [TcLevel and untouchable type variables] for what this Int is
 See also Note [TcLevel assignment]
{
Note [TcLevel and untouchable type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Each unification variable (MetaTv)
and each Implication
has a level number (of type TcLevel)
* INVARIANTS. In a tree of Implications,
(ImplicInv) The level number (ic_tclvl) of an Implication is
STRICTLY GREATER THAN that of its parent
(SkolInv) The level number of the skolems (ic_skols) of an
Implication is equal to the level of the implication
itself (ic_tclvl)
(GivenInv) The level number of a unification variable appearing
in the 'ic_given' of an implication I should be
STRICTLY LESS THAN the ic_tclvl of I
(WantedInv) The level number of a unification variable appearing
in the 'ic_wanted' of an implication I should be
LESS THAN OR EQUAL TO the ic_tclvl of I
See Note [WantedInv]
* A unification variable is *touchable* if its level number
is EQUAL TO that of its immediate parent implication,
and it is a TauTv or SigTv (but /not/ FlatMetaTv or FlatSkolTv
Note [WantedInv]
~~~~~~~~~~~~~~~~
Why is WantedInv important? Consider this implication, where
the constraint (C alpha[3]) disobeys WantedInv:
forall[2] a. blah => (C alpha[3])
(forall[3] b. alpha[3] ~ b)
We can unify alpha:=b in the inner implication, because 'alpha' is
touchable; but then 'b' has excaped its scope into the outer implication.
Note [Skolem escape prevention]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only unify touchable unification variables. Because of
(WantedInv), there can be no occurrences of the variable further out,
so the unification can't cause the skolems to escape. Example:
data T = forall a. MkT a (a>Int)
f x (MkT v f) = length [v,x]
We decide (x::alpha), and generate an implication like
[1]forall a. (a ~ alpha[0])
But we must not unify alpha:=a, because the skolem would escape.
For the cases where we DO want to unify, we rely on floating the
equality. Example (with same T)
g x (MkT v f) = x && True
We decide (x::alpha), and generate an implication like
[1]forall a. (Bool ~ alpha[0])
We do NOT unify directly, bur rather float out (if the constraint
does not mention 'a') to get
(Bool ~ alpha[0]) /\ [1]forall a.()
and NOW we can unify alpha.
The same idea of only unifying touchables solves another problem.
Suppose we had
(F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1])
In this example, beta is touchable inside the implication. The
first solveSimpleWanteds step leaves 'uf' ununified. Then we move inside
the implication where a new constraint
uf ~ beta
emerges. If we (wrongly) spontaneously solved it to get uf := beta,
the whole implication disappears but when we pop out again we are left with
(F Int ~ uf) which will be unified by our final zonking stage and
uf will get unified *once more* to (F Int).
Note [TcLevel assignment]
~~~~~~~~~~~~~~~~~~~~~~~~~
We arrange the TcLevels like this
0 Top level
1 Firstlevel implication constraints
2 Secondlevel implication constraints
...etc...
}
maxTcLevel :: TcLevel > TcLevel > TcLevel
maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)
topTcLevel :: TcLevel
 See Note [TcLevel assignment]
topTcLevel = TcLevel 0  0 = outermost level
isTopTcLevel :: TcLevel > Bool
isTopTcLevel (TcLevel 0) = True
isTopTcLevel _ = False
pushTcLevel :: TcLevel > TcLevel
 See Note [TcLevel assignment]
pushTcLevel (TcLevel us) = TcLevel (us + 1)
strictlyDeeperThan :: TcLevel > TcLevel > Bool
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
= tv_tclvl > ctxt_tclvl
sameDepthAs :: TcLevel > TcLevel > Bool
sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
= ctxt_tclvl == tv_tclvl  NB: invariant ctxt_tclvl >= tv_tclvl
 So <= would be equivalent
checkTcLevelInvariant :: TcLevel > TcLevel > Bool
 Checks (WantedInv) from Note [TcLevel and untouchable type variables]
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
= ctxt_tclvl >= tv_tclvl
tcTyVarLevel :: TcTyVar > TcLevel
tcTyVarLevel tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_lvl } > tv_lvl
SkolemTv tv_lvl _ > tv_lvl
RuntimeUnk > topTcLevel
tcTypeLevel :: TcType > TcLevel
 Max level of any free var of the type
tcTypeLevel ty
= foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty)
where
add v lvl
 isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
 otherwise = lvl
instance Outputable TcLevel where
ppr (TcLevel us) = ppr us
promoteSkolem :: TcLevel > TcTyVar > TcTyVar
promoteSkolem tclvl skol
 tclvl < tcTyVarLevel skol
= ASSERT( isTcTyVar skol && isSkolemTyVar skol )
setTcTyVarDetails skol (SkolemTv tclvl (isOverlappableTyVar skol))
 otherwise
= skol
  Change the TcLevel in a skolem, extending a substitution
promoteSkolemX :: TcLevel > TCvSubst > TcTyVar > (TCvSubst, TcTyVar)
promoteSkolemX tclvl subst skol
= ASSERT( isTcTyVar skol && isSkolemTyVar skol )
(new_subst, new_skol)
where
new_skol
 tclvl < tcTyVarLevel skol
= setTcTyVarDetails (updateTyVarKind (substTy subst) skol)
(SkolemTv tclvl (isOverlappableTyVar skol))
 otherwise
= updateTyVarKind (substTy subst) skol
new_subst = extendTvSubstWithClone subst skol new_skol
promoteSkolemsX :: TcLevel > TCvSubst > [TcTyVar] > (TCvSubst, [TcTyVar])
promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
{ *********************************************************************
* *
Finding type family instances
* *
************************************************************************
}
  Finds outermost typefamily applications occuring in a type,
 after expanding synonyms. In the list (F, tys) that is returned
 we guarantee that tys matches F's arity. For example, given
 type family F a :: * > * (arity 1)
 calling tcTyFamInsts on (Maybe (F Int Bool) will return
 (F, [Int]), not (F, [Int,Bool])

 This is important for its use in deciding termination of type
 instances (see Trac #11581). E.g.
 type instance G [Int] = ...(F Int )...
 we don't need to take into account when asking if
 the calls on the RHS are smaller than the LHS
tcTyFamInsts :: Type > [(TyCon, [Type])]
tcTyFamInsts ty
 Just exp_ty < tcView ty = tcTyFamInsts exp_ty
tcTyFamInsts (TyVarTy _) = []
tcTyFamInsts (TyConApp tc tys)
 isTypeFamilyTyCon tc = [(tc, take (tyConArity tc) tys)]
 otherwise = concat (map tcTyFamInsts tys)
tcTyFamInsts (LitTy {}) = []
tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderKind bndr)
++ tcTyFamInsts ty
tcTyFamInsts (FunTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
tcTyFamInsts (AppTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
tcTyFamInsts (CastTy ty _) = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _) = []  don't count tyfams in coercions,
 as they never get normalized, anyway
isTyFamFree :: Type > Bool
 ^ Check that a type does not contain any type family applications.
isTyFamFree = null . tcTyFamInsts
{
************************************************************************
* *
The "exact" free variables of a type
* *
************************************************************************
Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
type T a = Int
What are the free tyvars of (T x)? Empty, of course!
Here's the example that Ralf Laemmel showed me:
foo :: (forall a. C u a > C u a) > u
mappend :: Monoid u => u > u > u
bar :: Monoid u => u
bar = foo (\t > t `mappend` t)
We have to generalise at the arg to f, and we don't
want to capture the constraint (Monad (C u a)) because
it appears to mention a. Pretty silly, but it was useful to him.
exactTyCoVarsOfType is used by the type checker to figure out exactly
which type variables are mentioned in a type. It's also used in the
smartapp checking code  see TcExpr.tcIdApp
On the other hand, consider a *toplevel* definition
f = (\x > x) :: T a > T a
If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
if we have an application like (f "x") we get a confusing error message
involving Any. So the conclusion is this: when generalising
 at top level use tyCoVarsOfType
 in nested bindings use exactTyCoVarsOfType
See Trac #1813 for example.
}
exactTyCoVarsOfType :: Type > TyCoVarSet
 Find the free type variables (of any kind)
 but *expand* type synonyms. See Note [Silly type synonym] above.
exactTyCoVarsOfType ty
= go ty
where
go ty  Just ty' < tcView ty = go ty'  This is the key line
go (TyVarTy tv) = goVar tv
go (TyConApp _ tys) = exactTyCoVarsOfTypes tys
go (LitTy {}) = emptyVarSet
go (AppTy fun arg) = go fun `unionVarSet` go arg
go (FunTy arg res) = go arg `unionVarSet` go res
go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderKind bndr)
go (CastTy ty co) = go ty `unionVarSet` goCo co
go (CoercionTy co) = goCo co
goCo (Refl _ ty) = go ty
goCo (TyConAppCo _ _ args)= goCos args
goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg
goCo (ForAllCo tv k_co co)
= goCo co `delVarSet` tv `unionVarSet` goCo k_co
goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2
goCo (CoVarCo v) = goVar v
goCo (HoleCo h) = goVar (coHoleCoVar h)
goCo (AxiomInstCo _ _ args) = goCos args
goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2
goCo (SymCo co) = goCo co
goCo (TransCo co1 co2) = goCo co1 `unionVarSet` goCo co2
goCo (NthCo _ _ co) = goCo co
goCo (LRCo _ co) = goCo co
goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg
goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
goCo (KindCo co) = goCo co
goCo (SubCo co) = goCo co
goCo (AxiomRuleCo _ c) = goCos c
goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
goProv UnsafeCoerceProv = emptyVarSet
goProv (PhantomProv kco) = goCo kco
goProv (ProofIrrelProv kco) = goCo kco
goProv (PluginProv _) = emptyVarSet
goVar v = unitVarSet v `unionVarSet` go (varType v)
exactTyCoVarsOfTypes :: [Type] > TyVarSet
exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
anyRewritableTyVar :: Bool  Ignore casts and coercions
> EqRel  Ambient role
> (EqRel > TcTyVar > Bool)
> TcType > Bool
 (anyRewritableTyVar ignore_cos pred ty) returns True
 if the 'pred' returns True of any free TyVar in 'ty'
 Do not look inside casts and coercions if 'ignore_cos' is True
 See Note [anyRewritableTyVar must be roleaware]
anyRewritableTyVar ignore_cos role pred ty
= go role emptyVarSet ty
where
go_tv rl bvs tv  tv `elemVarSet` bvs = False
 otherwise = pred rl tv
go rl bvs (TyVarTy tv) = go_tv rl bvs tv
go _ _ (LitTy {}) = False
go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys
go rl bvs (AppTy fun arg) = go rl bvs fun  go NomEq bvs arg
go rl bvs (FunTy arg res) = go rl bvs arg  go rl bvs res
go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty
go rl bvs (CastTy ty co) = go rl bvs ty  go_co rl bvs co
go rl bvs (CoercionTy co) = go_co rl bvs co  ToDo: check
go_tc NomEq bvs _ tys = any (go NomEq bvs) tys
go_tc ReprEq bvs tc tys = foldr ((&&) . go_arg bvs) False $
(tyConRolesRepresentational tc `zip` tys)
go_arg bvs (Nominal, ty) = go NomEq bvs ty
go_arg bvs (Representational, ty) = go ReprEq bvs ty
go_arg _ (Phantom, _) = False  We never rewrite with phantoms
go_co rl bvs co
 ignore_cos = False
 otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co)
 We don't have an equivalent of anyRewritableTyVar for coercions
 (at least not yet) so take the free vars and test them
{ Note [anyRewritableTyVar must be roleaware]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
anyRewritableTyVar is used during kickout from the inert set,
to decide if, given a new equality (a ~ ty), we should kick out
a constraint C. Rather than gather free variables and see if 'a'
is among them, we instead pass in a predicate; this is just efficiency.
Moreover, consider
work item: [G] a ~R f b
inert item: [G] b ~R f a
We use anyRewritableTyVar to decide whether to kick out the inert item,
on the grounds that the work item might rewrite it. Well, 'a' is certainly
free in [G] b ~R f a. But because the role of a type variable ('f' in
this case) is nominal, the work item can't actually rewrite the inert item.
Moreover, if we were to kick out the inert item the exact same situation
would reoccur and we end up with an infinite loop in which each kicks
out the other (Trac #14363).
}
{ *********************************************************************
* *
Type and kind variables in a type
* *
********************************************************************* }
data CandidatesQTvs  See Note [Dependent type variables]
 See Note [CandidatesQTvs determinism]
= DV { dv_kvs :: DTyCoVarSet  "kind" variables (dependent)
, dv_tvs :: DTyVarSet  "type" variables (nondependent)
 A variable may appear in both sets
 E.g. T k (x::k) The first occurrence of k makes it
 show up in dv_tvs, the second in dv_kvs
 See Note [Dependent type variables]
}
instance Semi.Semigroup CandidatesQTvs where
(DV { dv_kvs = kv1, dv_tvs = tv1 }) <> (DV { dv_kvs = kv2, dv_tvs = tv2 })
= DV { dv_kvs = kv1 `unionDVarSet` kv2
, dv_tvs = tv1 `unionDVarSet` tv2}
instance Monoid CandidatesQTvs where
mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet }
mappend = (Semi.<>)
instance Outputable CandidatesQTvs where
ppr (DV {dv_kvs = kvs, dv_tvs = tvs })
= text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs
, text "dv_tvs =" <+> ppr tvs ])
{ Note [Dependent type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Haskell type inference we quantify over type variables; but we only
quantify over /kind/ variables when XPolyKinds is on. Without XPolyKinds
we default the kind variables to *.
So, to support this defaulting, and only for that reason, when
collecting the free vars of a type, prior to quantifying, we must keep
the type and kind variables separate.
But what does that mean in a system where kind variables /are/ type
variables? It's a fairly arbitrary distinction based on how the
variables appear:
 "Kind variables" appear in the kind of some other free variable
PLUS any free coercion variables
These are the ones we default to * if XPolyKinds is off
 "Type variables" are all free vars that are not kind variables
E.g. In the type T k (a::k)
'k' is a kind variable, because it occurs in the kind of 'a',
even though it also appears at "top level" of the type
'a' is a type variable, because it doesn't
We gather these variables using a CandidatesQTvs record:
DV { dv_kvs: Variables free in the kind of a free type variable
or of a forallbound type variable
, dv_tvs: Variables sytactically free in the type }
So: dv_kvs are the kind variables of the type
(dv_tvs  dv_kvs) are the type variable of the type
Note that
* A variable can occur in both.
T k (x::k) The first occurrence of k makes it
show up in dv_tvs, the second in dv_kvs
* We include any coercion variables in the "dependent",
"kindvariable" set because we never quantify over them.
* Both sets are unordered, of course.
* The "kind variables" might depend on each other; e.g
(k1 :: k2), (k2 :: *)
The "type variables" do not depend on each other; if
one did, it'd be classified as a kind variable!
Note [CandidatesQTvs determinism and order]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Determinism: when we quantify over type variables we decide the
order in which they appear in the final type. Because the order of
type variables in the type can end up in the interface file and
affects some optimizations like workerwrapper, we want this order to
be deterministic.
To achieve that we use deterministic sets of variables that can be
converted to lists in a deterministic order. For more information
about deterministic sets see Note [Deterministic UniqFM] in UniqDFM.
* Order: as well as being deterministic, we use an
accumulatingparameter style for candidateQTyVarsOfType so that we
add variables one at a time, left to right. That means we tend to
produce the variables in lefttoright order. This is just to make
it bit more predicatable for the programmer.
}
  Worker for 'splitDepVarsOfType'. This might output the same var
 in both sets, if it's used in both a type and a kind.
 See Note [CandidatesQTvs determinism and order]
 See Note [Dependent type variables]
candidateQTyVarsOfType :: Type > CandidatesQTvs
candidateQTyVarsOfType = split_dvs emptyVarSet mempty
split_dvs :: VarSet > CandidatesQTvs > Type > CandidatesQTvs
split_dvs bound dvs ty
= go dvs ty
where
go dv (AppTy t1 t2) = go (go dv t1) t2
go dv (TyConApp _ tys) = foldl go dv tys
go dv (FunTy arg res) = go (go dv arg) res
go dv (LitTy {}) = dv
go dv (CastTy ty co) = go dv ty `mappend` go_co co
go dv (CoercionTy co) = dv `mappend` go_co co
go dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) (TyVarTy tv)
 tv `elemVarSet` bound
= dv
 otherwise
= DV { dv_kvs = kvs `unionDVarSet`
kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
, dv_tvs = tvs `extendDVarSet` tv }
go dv (ForAllTy (TvBndr tv _) ty)
= DV { dv_kvs = kvs `unionDVarSet`
kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
, dv_tvs = tvs }
where
DV { dv_kvs = kvs, dv_tvs = tvs } = split_dvs (bound `extendVarSet` tv) dv ty
go_co co = DV { dv_kvs = kill_bound (tyCoVarsOfCoDSet co)
, dv_tvs = emptyDVarSet }
kill_bound free
 isEmptyVarSet bound = free
 otherwise = free `dVarSetMinusVarSet` bound
  Like 'splitDepVarsOfType', but over a list of types
candidateQTyVarsOfTypes :: [Type] > CandidatesQTvs
candidateQTyVarsOfTypes = foldl (split_dvs emptyVarSet) mempty
{
************************************************************************
* *
Predicates
* *
************************************************************************
}
tcIsTcTyVar :: TcTyVar > Bool
 See Note [TcTyVars and TyVars in the typechecker]
tcIsTcTyVar tv = isTyVar tv
isTouchableMetaTyVar :: TcLevel > TcTyVar > Bool
isTouchableMetaTyVar ctxt_tclvl tv
 isTyVar tv  See Note [Coercion variables in free variable lists]
, MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } < tcTyVarDetails tv
, not (isFlattenInfo info)
= ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
tv_tclvl `sameDepthAs` ctxt_tclvl
 otherwise = False
isFloatedTouchableMetaTyVar :: TcLevel > TcTyVar > Bool
isFloatedTouchableMetaTyVar ctxt_tclvl tv
 isTyVar tv  See Note [Coercion variables in free variable lists]
, MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } < tcTyVarDetails tv
, not (isFlattenInfo info)
= ASSERT2( tcIsTcTyVar tv, ppr tv )
tv_tclvl `strictlyDeeperThan` ctxt_tclvl
 otherwise = False
isImmutableTyVar :: TyVar > Bool
isImmutableTyVar tv = isSkolemTyVar tv
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
isMetaTyVar, isAmbiguousTyVar,
isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar > Bool
isTyConableTyVar tv
 True of a metatype variable that can be filled in
 with a type constructor application; in particular,
 not a SigTv
 isTyVar tv  See Note [Coercion variables in free variable lists]
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = SigTv } > False
_ > True
 otherwise = True
isFmvTyVar tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = FlatMetaTv } > True
_ > False
isFskTyVar tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = FlatSkolTv } > True
_ > False
  True of both given and wanted flattenskolems (fak and usk)
isFlattenTyVar tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv { mtv_info = info } > isFlattenInfo info
_ > False
isSkolemTyVar tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} > False
_other > True
isOverlappableTyVar tv
 isTyVar tv  See Note [Coercion variables in free variable lists]
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv _ overlappable > overlappable
_ > False
 otherwise = False
isMetaTyVar tv
 isTyVar tv  See Note [Coercion variables in free variable lists]
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv {} > True
_ > False
 otherwise = False
 isAmbiguousTyVar is used only when reporting type errors
 It picks out variables that are unbound, namely meta
 type variables and the RuntimUnk variables created by
 RtClosureInspect.zonkRTTIType. These are "ambiguous" in
 the sense that they stand for an asyetunknown type
isAmbiguousTyVar tv
 isTyVar tv  See Note [Coercion variables in free variable lists]
= case tcTyVarDetails tv of
MetaTv {} > True
RuntimeUnk {} > True
_ > False
 otherwise = False
isMetaTyVarTy :: TcType > Bool
isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
isMetaTyVarTy _ = False
metaTyVarInfo :: TcTyVar > MetaInfo
metaTyVarInfo tv
= case tcTyVarDetails tv of
MetaTv { mtv_info = info } > info
_ > pprPanic "metaTyVarInfo" (ppr tv)
isFlattenInfo :: MetaInfo > Bool
isFlattenInfo FlatMetaTv = True
isFlattenInfo FlatSkolTv = True
isFlattenInfo _ = False
metaTyVarTcLevel :: TcTyVar > TcLevel
metaTyVarTcLevel tv
= case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tclvl } > tclvl
_ > pprPanic "metaTyVarTcLevel" (ppr tv)
metaTyVarTcLevel_maybe :: TcTyVar > Maybe TcLevel
metaTyVarTcLevel_maybe tv
= case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tclvl } > Just tclvl
_ > Nothing
metaTyVarRef :: TyVar > IORef MetaDetails
metaTyVarRef tv
= case tcTyVarDetails tv of
MetaTv { mtv_ref = ref } > ref
_ > pprPanic "metaTyVarRef" (ppr tv)
setMetaTyVarTcLevel :: TcTyVar > TcLevel > TcTyVar
setMetaTyVarTcLevel tv tclvl
= case tcTyVarDetails tv of
details@(MetaTv {}) > setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
_ > pprPanic "metaTyVarTcLevel" (ppr tv)
isSigTyVar :: Var > Bool
isSigTyVar tv
= case tcTyVarDetails tv of
MetaTv { mtv_info = SigTv } > True
_ > False
isFlexi, isIndirect :: MetaDetails > Bool
isFlexi Flexi = True
isFlexi _ = False
isIndirect (Indirect _) = True
isIndirect _ = False
isRuntimeUnkSkol :: TyVar > Bool
 Called only in TcErrors; see Note [Runtime skolems] there
isRuntimeUnkSkol x
 RuntimeUnk < tcTyVarDetails x = True
 otherwise = False
mkTyVarNamePairs :: [TyVar] > [(Name,TyVar)]
 Just pair each TyVar with its own name
mkTyVarNamePairs tvs = [(tyVarName tv, tv)  tv < tvs]
findDupSigTvs :: [(Name,TcTyVar)] > [(Name,Name)]
 If we have [...(x1,tv)...(x2,tv)...]
 return (x1,x2) in the result list
findDupSigTvs prs
= concatMap mk_result_prs $
findDupsEq eq_snd prs
where
eq_snd (_,tv1) (_,tv2) = tv1 == tv2
mk_result_prs ((n1,_) : xs) = map (\(n2,_) > (n1,n2)) xs
{
************************************************************************
* *
\subsection{Tau, sigma and rho}
* *
************************************************************************
}
mkSigmaTy :: [TyVarBinder] > [PredType] > Type > Type
mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau)
  Make a sigma ty where all type variables are 'Inferred'. That is,
 they cannot be used with visible type application.
mkInfSigmaTy :: [TyVar] > [PredType] > Type > Type
mkInfSigmaTy tyvars theta ty = mkSigmaTy (mkTyVarBinders Inferred tyvars) theta ty
  Make a sigma ty where all type variables are "specified". That is,
 they can be used with visible type application
mkSpecSigmaTy :: [TyVar] > [PredType] > Type > Type
mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyVarBinders Specified tyvars) preds ty
mkPhiTy :: [PredType] > Type > Type
mkPhiTy = mkFunTys

getDFunTyKey :: Type > OccName  Get some string from a type, to be used to
 construct a dictionary function name
getDFunTyKey ty  Just ty' < coreView ty = getDFunTyKey ty'
getDFunTyKey (TyVarTy tv) = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (LitTy x) = getDFunTyLitKey x
getDFunTyKey (AppTy fun _) = getDFunTyKey fun
getDFunTyKey (FunTy _ _) = getOccName funTyCon
getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
getDFunTyKey (CastTy ty _) = getDFunTyKey ty
getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t)
getDFunTyLitKey :: TyLit > OccName
getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n)
getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n)  hm

mkNakedTyConApp :: TyCon > [Type] > Type
 Builds a TyConApp
 * without being strict in TyCon,
 * without satisfying the invariants of TyConApp
 A subsequent zonking will establish the invariants
 See Note [Typechecking inside the knot] in TcHsType
mkNakedTyConApp tc tys = TyConApp tc tys
mkNakedAppTys :: Type > [Type] > Type
 See Note [Typechecking inside the knot] in TcHsType
mkNakedAppTys ty1 [] = ty1
mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2
mkNakedAppTy :: Type > Type > Type
 See Note [Typechecking inside the knot] in TcHsType
mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
mkNakedCastTy :: Type > Coercion > Type
 Do /not/ attempt to get rid of the cast altogether,
 even if it is Refl: see Note [The wellkinded type invariant]
 Even doing (t > co1) > co2 > t > (co1;co2)
 does not seem worth the bother

 NB: zonking will get rid of these casts, because it uses mkCastTy

 In fact the calls to mkNakedCastTy ar pretty few and far between.
mkNakedCastTy ty co = CastTy ty co
{ Note [The wellkinded type invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During type inference, we maintain the invariant that
INVARIANT: every type is wellkinded /without/ zonking
and in particular that typeKind does not fail (as it can for
illkinded types).
Now suppose we are kindchecking the type (a Int), where (a :: kappa).
Then in tcInferApps we'll run out of binders on a's kind, so
we'll call matchExpectedFunKind, and unify
kappa := kappa1 > kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
That evidence is actually Refl, but we must not discard the cast to
form the result type
((a::kappa) (Int::*))
bacause that does not satisfy the invariant, and crashes TypeKind. This
caused Trac #14174 and #14520.
Solution: make mkNakedCastTy use an actual CastTy, without optimising
for Refl. Now everything is wellkinded. The CastTy will be removed
later, when we zonk. Still, it's distressingly delicate.
NB: mkNakedCastTy is only called in two places:
in tcInferApps and in checkExpectedResultKind.
See Note [The tcType invariant] in TcHsType.
}
{
************************************************************************
* *
\subsection{Expanding and splitting}
* *
************************************************************************
These tcSplit functions are like their nonTc analogues, but
*) they do not look through newtypes
However, they are nonmonadic and do not follow through mutable type
variables. It's up to you to make sure this doesn't matter.
}
  Splits a forall type into a list of 'TyBinder's and the inner type.
 Always succeeds, even if it returns an empty list.
tcSplitPiTys :: Type > ([TyBinder], Type)
tcSplitPiTys = splitPiTys
  Splits a type into a TyBinder and a body, if possible. Panics otherwise
tcSplitPiTy_maybe :: Type > Maybe (TyBinder, Type)
tcSplitPiTy_maybe = splitPiTy_maybe
tcSplitForAllTy_maybe :: Type > Maybe (TyVarBinder, Type)
tcSplitForAllTy_maybe ty  Just ty' < tcView ty = tcSplitForAllTy_maybe ty'
tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
tcSplitForAllTy_maybe _ = Nothing
  Like 'tcSplitPiTys', but splits off only named binders, returning
 just the tycovars.
tcSplitForAllTys :: Type > ([TyVar], Type)
tcSplitForAllTys = splitForAllTys
  Like 'tcSplitForAllTys', but splits off only named binders.
tcSplitForAllTyVarBndrs :: Type > ([TyVarBinder], Type)
tcSplitForAllTyVarBndrs = splitForAllTyVarBndrs
  Is this a ForAllTy with a named binder?
tcIsForAllTy :: Type > Bool
tcIsForAllTy ty  Just ty' < tcView ty = tcIsForAllTy ty'
tcIsForAllTy (ForAllTy {}) = True
tcIsForAllTy _ = False
tcSplitPredFunTy_maybe :: Type > Maybe (PredType, Type)
 Split off the first predicate argument from a type
tcSplitPredFunTy_maybe ty
 Just ty' < tcView ty = tcSplitPredFunTy_maybe ty'
tcSplitPredFunTy_maybe (FunTy arg res)
 isPredTy arg = Just (arg, res)
tcSplitPredFunTy_maybe _
= Nothing
tcSplitPhiTy :: Type > (ThetaType, Type)
tcSplitPhiTy ty
= split ty []
where
split ty ts
= case tcSplitPredFunTy_maybe ty of
Just (pred, ty) > split ty (pred:ts)
Nothing > (reverse ts, ty)
  Split a sigma type into its parts.
tcSplitSigmaTy :: Type > ([TyVar], ThetaType, Type)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
(tvs, rho) > case tcSplitPhiTy rho of
(theta, tau) > (tvs, theta, tau)
  Split a sigma type into its parts, going underneath as many @ForAllTy@s
 as possible. For example, given this type synonym:

 @
 type Traversal s t a b = forall f. Applicative f => (a > f b) > s > f t
 @

 if you called @tcSplitSigmaTy@ on this type:

 @
 forall s t a b. Each s t a b => Traversal s t a b
 @

 then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
 if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
 @([s,t,a,b,f], [Each s t a b, Applicative f], (a > f b) > s > f t)@.
tcSplitNestedSigmaTys :: Type > ([TyVar], ThetaType, Type)
 NB: This is basically a pure version of deeplyInstantiate (from Inst) that
 doesn't compute an HsWrapper.
tcSplitNestedSigmaTys ty
 If there's a forall, split it apart and try splitting the rho type
 underneath it.
 Just (arg_tys, tvs1, theta1, rho1) < tcDeepSplitSigmaTy_maybe ty
= let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
in (tvs1 ++ tvs2, theta1 ++ theta2, mkFunTys arg_tys rho2)
 If there's no forall, we're done.
 otherwise = ([], [], ty)

tcDeepSplitSigmaTy_maybe
:: TcSigmaType > Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
 Looks for a *nontrivial* quantified type, under zero or more function arrows
 By "nontrivial" we mean either tyvars or constraints are nonempty
tcDeepSplitSigmaTy_maybe ty
 Just (arg_ty, res_ty) < tcSplitFunTy_maybe ty
, Just (arg_tys, tvs, theta, rho) < tcDeepSplitSigmaTy_maybe res_ty
= Just (arg_ty:arg_tys, tvs, theta, rho)
 (tvs, theta, rho) < tcSplitSigmaTy ty
, not (null tvs && null theta)
= Just ([], tvs, theta, rho)
 otherwise = Nothing

tcTyConAppTyCon :: Type > TyCon
tcTyConAppTyCon ty
= case tcTyConAppTyCon_maybe ty of
Just tc > tc
Nothing > pprPanic "tcTyConAppTyCon" (pprType ty)
  Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
tcTyConAppTyCon_maybe :: Type > Maybe TyCon
tcTyConAppTyCon_maybe ty
 Just ty' < tcView ty = tcTyConAppTyCon_maybe ty'
tcTyConAppTyCon_maybe (TyConApp tc _)
= Just tc
tcTyConAppTyCon_maybe (FunTy _ _)
= Just funTyCon
tcTyConAppTyCon_maybe _
= Nothing
tcTyConAppArgs :: Type > [Type]
tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
Just (_, args) > args
Nothing > pprPanic "tcTyConAppArgs" (pprType ty)
tcSplitTyConApp :: Type > (TyCon, [Type])
tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
Just stuff > stuff
Nothing > pprPanic "tcSplitTyConApp" (pprType ty)
  Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if,

 1. the type is structurally not a type constructor application, or

 2. the type is a function type (e.g. application of 'funTyCon'), but we
 currently don't even enough information to fully determine its RuntimeRep
 variables. For instance, @FunTy (a :: k) Int@.

 By contrast 'tcRepSplitTyConApp_maybe' panics in the second case.

 The behavior here is needed during canonicalization; see Note [FunTy and
 decomposing tycon applications] in TcCanonical for details.
tcRepSplitTyConApp_maybe' :: HasCallStack => Type > Maybe (TyCon, [Type])
tcRepSplitTyConApp_maybe' (TyConApp tc tys) = Just (tc, tys)
tcRepSplitTyConApp_maybe' (FunTy arg res)
 Just arg_rep < getRuntimeRep_maybe arg
, Just res_rep < getRuntimeRep_maybe res
= Just (funTyCon, [arg_rep, res_rep, arg, res])
tcRepSplitTyConApp_maybe' _ = Nothing

tcSplitFunTys :: Type > ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
Nothing > ([], ty)
Just (arg,res) > (arg:args, res')
where
(args,res') = tcSplitFunTys res
tcSplitFunTy_maybe :: Type > Maybe (Type, Type)
tcSplitFunTy_maybe ty  Just ty' < tcView ty = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (FunTy arg res)  not (isPredTy arg) = Just (arg, res)
tcSplitFunTy_maybe _ = Nothing
 Note the typeKind guard
 Consider (?x::Int) => Bool
 We don't want to treat this as a function type!
 A concrete example is test tc230:
 f :: () > (?p :: ()) => () > ()

 g = f () ()
tcSplitFunTysN :: Arity  N: Number of desired args
> TcRhoType
> Either Arity  Number of missing arrows
([TcSigmaType],  Arg types (always N types)
TcSigmaType)  The rest of the type
 ^ Split off exactly the specified number argument types
 Returns
 (Left m) if there are 'm' missing arrows in the type
 (Right (tys,res)) if the type looks like t1 > ... > tn > res
tcSplitFunTysN n ty
 n == 0
= Right ([], ty)
 Just (arg,res) < tcSplitFunTy_maybe ty
= case tcSplitFunTysN (n1) res of
Left m > Left m
Right (args,body) > Right (arg:args, body)
 otherwise
= Left n
tcSplitFunTy :: Type > (Type, Type)
tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
tcFunArgTy :: Type > Type
tcFunArgTy ty = fst (tcSplitFunTy ty)
tcFunResultTy :: Type > Type
tcFunResultTy ty = snd (tcSplitFunTy ty)
  Strips off n *visible* arguments and returns the resulting type
tcFunResultTyN :: HasDebugCallStack => Arity > Type > Type
tcFunResultTyN n ty
 Right (_, res_ty) < tcSplitFunTysN n ty
= res_ty
 otherwise
= pprPanic "tcFunResultTyN" (ppr n <+> ppr ty)

tcSplitAppTy_maybe :: Type > Maybe (Type, Type)
tcSplitAppTy_maybe ty  Just ty' < tcView ty = tcSplitAppTy_maybe ty'
tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty
tcSplitAppTy :: Type > (Type, Type)
tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
Just stuff > stuff
Nothing > pprPanic "tcSplitAppTy" (pprType ty)
tcSplitAppTys :: Type > (Type, [Type])
tcSplitAppTys ty
= go ty []
where
go ty args = case tcSplitAppTy_maybe ty of
Just (ty', arg) > go ty' (arg:args)
Nothing > (ty,args)
  Returns the number of arguments in the given type, without
 looking through synonyms. This is used only for error reporting.
 We don't look through synonyms because of #11313.
tcRepGetNumAppTys :: Type > Arity
tcRepGetNumAppTys = length . snd . repSplitAppTys

  If the type is a tyvar, possibly under a cast, returns it, along
 with the coercion. Thus, the co is :: kind tv ~N kind type
tcGetCastedTyVar_maybe :: Type > Maybe (TyVar, CoercionN)
tcGetCastedTyVar_maybe ty  Just ty' < tcView ty = tcGetCastedTyVar_maybe ty'
tcGetCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co)
tcGetCastedTyVar_maybe (TyVarTy tv) = Just (tv, mkNomReflCo (tyVarKind tv))
tcGetCastedTyVar_maybe _ = Nothing
tcGetTyVar_maybe :: Type > Maybe TyVar
tcGetTyVar_maybe ty  Just ty' < tcView ty = tcGetTyVar_maybe ty'
tcGetTyVar_maybe (TyVarTy tv) = Just tv
tcGetTyVar_maybe _ = Nothing
tcGetTyVar :: String > Type > TyVar
tcGetTyVar msg ty
= case tcGetTyVar_maybe ty of
Just tv > tv
Nothing > pprPanic msg (ppr ty)
tcIsTyVarTy :: Type > Bool
tcIsTyVarTy ty  Just ty' < tcView ty = tcIsTyVarTy ty'
tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty  look through casts, as
 this is only used for
 e.g., FlexibleContexts
tcIsTyVarTy (TyVarTy _) = True
tcIsTyVarTy _ = False

tcSplitDFunTy :: Type > ([TyVar], [Type], Class, [Type])
 Split the type of a dictionary function
 We don't use tcSplitSigmaTy, because a DFun may (with NDP)
 have nonPred arguments, such as
 df :: forall m. (forall b. Eq b => Eq (m b)) > C m

 Also NB splitFunTys, not tcSplitFunTys;
 the latter specifically stops at PredTy arguments,
 and we don't want to do that here
tcSplitDFunTy ty
= case tcSplitForAllTys ty of { (tvs, rho) >
case splitFunTys rho of { (theta, tau) >
case tcSplitDFunHead tau of { (clas, tys) >
(tvs, theta, clas, tys) }}}
tcSplitDFunHead :: Type > (Class, [Type])
tcSplitDFunHead = getClassPredTys
tcSplitMethodTy :: Type > ([TyVar], PredType, Type)
 A class method (selector) always has a type like
 forall as. C as => blah
 So if the class looks like
 class C a where
 op :: forall b. (Eq a, Ix b) => a > b
 the class method type looks like
 op :: forall a. C a => forall b. (Eq a, Ix b) => a > b

 tcSplitMethodTy just peels off the outer forall and
 that first predicate
tcSplitMethodTy ty
 (sel_tyvars,sel_rho) < tcSplitForAllTys ty
, Just (first_pred, local_meth_ty) < tcSplitPredFunTy_maybe sel_rho
= (sel_tyvars, first_pred, local_meth_ty)
 otherwise
= pprPanic "tcSplitMethodTy" (ppr ty)
{ *********************************************************************
* *
Type equalities
* *
********************************************************************* }
tcEqKind :: HasDebugCallStack => TcKind > TcKind > Bool
tcEqKind = tcEqType
tcEqType :: HasDebugCallStack => TcType > TcType > Bool
 tcEqType is a proper implements the same Note [Nontrivial definitional
 equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
 Constraint), and that is NOT what we want in the type checker!
tcEqType ty1 ty2
= isNothing (tc_eq_type tcView ki1 ki2) &&
isNothing (tc_eq_type tcView ty1 ty2)
where
ki1 = typeKind ty1
ki2 = typeKind ty2
  Just like 'tcEqType', but will return True for types of different kinds
 as long as their noncoercion structure is identical.
tcEqTypeNoKindCheck :: TcType > TcType > Bool
tcEqTypeNoKindCheck ty1 ty2
= isNothing $ tc_eq_type tcView ty1 ty2
  Like 'tcEqType', but returns information about whether the difference
 is visible in the case of a mismatch.
 @Nothing@ : the types are equal
 @Just True@ : the types differ, and the point of difference is visible
 @Just False@ : the types differ, and the point of difference is invisible
tcEqTypeVis :: TcType > TcType > Maybe Bool
tcEqTypeVis ty1 ty2
= tc_eq_type tcView ty1 ty2 invis (tc_eq_type tcView ki1 ki2)
where
ki1 = typeKind ty1
ki2 = typeKind ty2
 convert Just True to Just False
invis :: Maybe Bool > Maybe Bool
invis = fmap (const False)
() :: Maybe Bool > Maybe Bool > Maybe Bool
Nothing x = x
Just True _ = Just True
Just _vis Just True = Just True
Just vis _ = Just vis
infixr 3
  Real worker for 'tcEqType'. No kind check!
tc_eq_type :: (TcType > Maybe TcType)  ^ @tcView@, if you want unwrapping
> Type > Type > Maybe Bool
tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
where
go :: Bool > RnEnv2 > Type > Type > Maybe Bool
go vis env t1 t2  Just t1' < view_fun t1 = go vis env t1' t2
go vis env t1 t2  Just t2' < view_fun t2 = go vis env t1 t2'
go vis env (TyVarTy tv1) (TyVarTy tv2)
= check vis $ rnOccL env tv1 == rnOccR env tv2
go vis _ (LitTy lit1) (LitTy lit2)
= check vis $ lit1 == lit2
go vis env (ForAllTy (TvBndr tv1 vis1) ty1)
(ForAllTy (TvBndr tv2 vis2) ty2)
= go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2)
go vis (rnBndr2 env tv1 tv2) ty1 ty2
check vis (vis1 == vis2)
 Make sure we handle all FunTy cases since falling through to the
 AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
 kind variable, which causes things to blow up.
go vis env (FunTy arg1 res1) (FunTy arg2 res2)
= go vis env arg1 arg2 go vis env res1 res2
go vis env ty (FunTy arg res)
= eqFunTy vis env arg res ty
go vis env (FunTy arg res) ty
= eqFunTy vis env arg res ty
 See Note [Equality on AppTys] in Type
go vis env (AppTy s1 t1) ty2
 Just (s2, t2) < tcRepSplitAppTy_maybe ty2
= go vis env s1 s2 go vis env t1 t2
go vis env ty1 (AppTy s2 t2)
 Just (s1, t1) < tcRepSplitAppTy_maybe ty1
= go vis env s1 s2 go vis env t1 t2
go vis env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
= check vis (tc1 == tc2) gos (tc_vis vis tc1) env ts1 ts2
go vis env (CastTy t1 _) t2 = go vis env t1 t2
go vis env t1 (CastTy t2 _) = go vis env t1 t2
go _ _ (CoercionTy {}) (CoercionTy {}) = Nothing
go vis _ _ _ = Just vis
gos _ _ [] [] = Nothing
gos (v:vs) env (t1:ts1) (t2:ts2) = go v env t1 t2 gos vs env ts1 ts2
gos (v:_) _ _ _ = Just v
gos _ _ _ _ = panic "tc_eq_type"
tc_vis :: Bool > TyCon > [Bool]
tc_vis True tc = viss ++ repeat True
 the repeat True is necessary because tycons can legitimately
 be oversaturated
where
bndrs = tyConBinders tc
viss = map isVisibleTyConBinder bndrs
tc_vis False _ = repeat False  if we're not in a visible context, our args
 aren't either
check :: Bool > Bool > Maybe Bool
check _ True = Nothing
check vis False = Just vis
orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
 @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is
 sometimes hard to know directly because @ty@ might have some casts
 obscuring the FunTy. And 'splitAppTy' is difficult because we can't
 always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
 res is unzonked/unflattened. Thus this function, which handles this
 corner case.
eqFunTy :: Bool > RnEnv2 > Type > Type > Type > Maybe Bool
eqFunTy vis env arg res (FunTy arg' res')
= go vis env arg arg' go vis env res res'
eqFunTy vis env arg res ty@(AppTy{})
 Just (tc, [_, _, arg', res']) < get_args ty []
, tc == funTyCon
= go vis env arg arg' go vis env res res'
where
get_args :: Type > [Type] > Maybe (TyCon, [Type])
get_args (AppTy f x) args = get_args f (x:args)
get_args (CastTy t _) args = get_args t args
get_args (TyConApp tc tys) args = Just (tc, tys ++ args)
get_args _ _ = Nothing
eqFunTy vis _ _ _ _
= Just vis
  Like 'pickyEqTypeVis', but returns a Bool for convenience
pickyEqType :: TcType > TcType > Bool
 Check when two types _look_ the same, _including_ synonyms.
 So (pickyEqType String [Char]) returns False
 This ignores kinds and coercions, because this is used only for printing.
pickyEqType ty1 ty2
= isNothing $
tc_eq_type (const Nothing) ty1 ty2
{ *********************************************************************
* *
Predicate types
* *
************************************************************************
Deconstructors and tests on predicate types
Note [Kind polymorphic type classes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
class C f where...  C :: forall k. k > Constraint
g :: forall (f::*). C f => f > f
Here the (C f) in the signature is really (C * f), and we
don't want to complain that the * isn't a type variable!
}
isTyVarClassPred :: PredType > Bool
isTyVarClassPred ty = case getClassPredTys_maybe ty of
Just (_, tys) > all isTyVarTy tys
_ > False

checkValidClsArgs :: Bool > Class > [KindOrType] > Bool
 If the Bool is True (flexible contexts), return True (i.e. ok)
 Otherwise, check that the type (not kind) args are all headed by a tyvar
 E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
 This function is here rather than in TcValidity because it is
 called from TcSimplify, which itself is imported by TcValidity
checkValidClsArgs flexible_contexts cls kts
 flexible_contexts = True
 otherwise = all hasTyVarHead tys
where
tys = filterOutInvisibleTypes (classTyCon cls) kts
hasTyVarHead :: Type > Bool
 Returns true of (a t1 .. tn), where 'a' is a type variable
hasTyVarHead ty  Haskell 98 allows predicates of form
 tcIsTyVarTy ty = True  C (a ty1 .. tyn)
 otherwise  where a is a type variable
= case tcSplitAppTy_maybe ty of
Just (ty, _) > hasTyVarHead ty
Nothing > False
evVarPred_maybe :: EvVar > Maybe PredType
evVarPred_maybe v = if isPredTy ty then Just ty else Nothing
where ty = varType v
evVarPred :: EvVar > PredType
evVarPred var
 debugIsOn
= case evVarPred_maybe var of
Just pred > pred
Nothing > pprPanic "tcEvVarPred" (ppr var <+> ppr (varType var))
 otherwise
= varType var

  When inferring types, should we quantify over a given predicate?
 Generally true of classes; generally false of equality constraints.
 Equality constraints that mention quantified type variables and
 implicit variables complicate the story. See Notes
 [Inheriting implicit parameters] and [Quantifying over equality constraints]
pickQuantifiablePreds
:: TyVarSet  Quantifying over these
> TcThetaType  Proposed constraints to quantify
> TcThetaType  A subset that we can actually quantify
 This function decides whether a particular constraint should be
 quantified over, given the type variables that are being quantified
pickQuantifiablePreds qtvs theta
= let flex_ctxt = True in  Quantify over nontyvar constraints, even without
 XFlexibleContexts: see Trac #10608, #10351
 flex_ctxt < xoptM Opt_FlexibleContexts
filter (pick_me flex_ctxt) theta
where
pick_me flex_ctxt pred
= case classifyPredType pred of
ClassPred cls tys
 Just {} < isCallStackPred cls tys
 NEVER infer a CallStack constraint
 Otherwise, we let the constraints bubble up to be
 solved from the outer context, or be defaulted when we
 reach the toplevel.
 see Note [Overview of implicit CallStacks]
> False
 isIPClass cls > True  See note [Inheriting implicit parameters]
 otherwise
> pick_cls_pred flex_ctxt cls tys
EqPred ReprEq ty1 ty2 > pick_cls_pred flex_ctxt coercibleClass [ty1, ty2]
 representational equality is like a class constraint
EqPred NomEq ty1 ty2 > quant_fun ty1  quant_fun ty2
IrredPred ty > tyCoVarsOfType ty `intersectsVarSet` qtvs
ForAllPred {} > False
pick_cls_pred flex_ctxt cls tys
= tyCoVarsOfTypes tys `intersectsVarSet` qtvs
&& (checkValidClsArgs flex_ctxt cls tys)
 Only quantify over predicates that checkValidType
 will pass! See Trac #10351.
 See Note [Quantifying over equality constraints]
quant_fun ty
= case tcSplitTyConApp_maybe ty of
Just (tc, tys)  isTypeFamilyTyCon tc
> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
_ > False
pickCapturedPreds
:: TyVarSet  Quantifying over these
> TcThetaType  Proposed constraints to quantify
> TcThetaType  A subset that we can actually quantify
 A simpler version of pickQuantifiablePreds, used to winnow down
 the inferred constraints of a group of bindings, into those for
 one particular identifier
pickCapturedPreds qtvs theta
= filter captured theta
where
captured pred = isIPPred pred  (tyCoVarsOfType pred `intersectsVarSet` qtvs)
 Superclasses
type PredWithSCs a = (PredType, [PredType], a)
mkMinimalBySCs :: forall a. (a > PredType) > [a] > [a]
 Remove predicates that

  are the same as another predicate

  can be deduced from another by superclasses,

  are a reflexive equality (e.g * ~ *)
 (see Note [Remove redundant provided dicts] in PatSyn)

 The result is a subset of the input.
 The 'a' is just paired up with the PredType;
 typically it might be a dictionary Id
mkMinimalBySCs get_pred xs = go preds_with_scs []
where
preds_with_scs :: [PredWithSCs a]
preds_with_scs = [ (pred, pred : transSuperClasses pred, x)
 x < xs
, let pred = get_pred x ]
go :: [PredWithSCs a]  Work list
> [PredWithSCs a]  Accumulating result
> [a]
go [] min_preds
= reverse (map thdOf3 min_preds)
 The 'reverse' isn't strictly necessary, but it
 means that the results are returned in the same
 order as the input, which is generally saner
go (work_item@(p,_,_) : work_list) min_preds
 EqPred _ t1 t2 < classifyPredType p
, t1 `tcEqType` t2  See Note [Discard reflexive equalities]
= go work_list min_preds
 p `in_cloud` work_list  p `in_cloud` min_preds
= go work_list min_preds
 otherwise
= go work_list (work_item : min_preds)
in_cloud :: PredType > [PredWithSCs a] > Bool
in_cloud p ps = or [ p `tcEqType` p'  (_, scs, _) < ps, p' < scs ]
transSuperClasses :: PredType > [PredType]
 (transSuperClasses p) returns (p's superclasses) not including p
 Stop if you encounter the same class again
 See Note [Expanding superclasses]
transSuperClasses p
= go emptyNameSet p
where
go :: NameSet > PredType > [PredType]
go rec_clss p
 ClassPred cls tys < classifyPredType p
, let cls_nm = className cls
, not (cls_nm `elemNameSet` rec_clss)
, let rec_clss'  isCTupleClass cls = rec_clss
 otherwise = rec_clss `extendNameSet` cls_nm
= [ p'  sc < immSuperClasses cls tys
, p' < sc : go rec_clss' sc ]
 otherwise
= []
immSuperClasses :: Class > [Type] > [PredType]
immSuperClasses cls tys
= substTheta (zipTvSubst tyvars tys) sc_theta
where
(tyvars,sc_theta,_,_) = classBigSig cls
isImprovementPred :: PredType > Bool
 Either it's an equality, or has some functional dependency
isImprovementPred ty
= case classifyPredType ty of
EqPred NomEq t1 t2 > not (t1 `tcEqType` t2)
EqPred ReprEq _ _ > False
ClassPred cls _ > classHasFds cls
IrredPred {} > True  Might have equalities after reduction?
ForAllPred {} > False
{ Note [Expanding superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we expand superclasses, we use the following algorithm:
expand( so_far, pred ) returns the transitive superclasses of pred,
not including pred itself
1. If pred is not a class constraint, return empty set
Otherwise pred = C ts
2. If C is in so_far, return empty set (breaks loops)
3. Find the immediate superclasses constraints of (C ts)
4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )
Notice that
* With normal Haskell98 classes, the loopdetector will never bite,
so we'll get all the superclasses.
* Since there is only a finite number of distinct classes, expansion
must terminate.
* The loop breaking is a bit conservative. Notably, a tuple class
could contain many times without threatening termination:
(Eq a, (Ord a, Ix a))
And this is try of any class that we can statically guarantee
as nonrecursive (in some sense). For now, we just make a special
case for tuples. Something better would be cool.
See also TcTyDecls.checkClassCycles.
+Note [Quantifying over equality constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should we quantify over an equality constraint (s ~ t)? In general, we don't.
+Doing so may simply postpone a type error from the function definition site to
+its call site. (At worst, imagine (Int ~ Bool)).
+
+However, consider this
+ forall a. (F [a] ~ Int) => blah
+Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call
+site we will know 'a', and perhaps we have instance F [Bool] = Int.
+So we *do* quantify over a typefamily equality where the arguments mention
+the quantified variables.
+
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
f x = (x::Int) + ?y
where f is *not* a toplevel binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:
f :: Int > Int
(so we get ?y from the context of f's definition), or
f :: (?y::Int) => Int > Int
At first you might think the first was better, because then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site. But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.
BOTTOM LINE: when *inferring types* you must quantify over implicit
parameters, *even if* they don't mention the bound type variables.
Reason: because implicit parameters, uniquely, have local instance
declarations. See pickQuantifiablePreds.
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Should we quantify over an equality constraint (s ~ t)? In general, we don't.
Doing so may simply postpone a type error from the function definition site to
its call site. (At worst, imagine (Int ~ Bool)).
However, consider this
forall a. (F [a] ~ Int) => blah
Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call
site we will know 'a', and perhaps we have instance F [Bool] = Int.
So we *do* quantify over a typefamily equality where the arguments mention
the quantified variables.
************************************************************************
* *
\subsection{Predicates}
* *
************************************************************************
}
isSigmaTy :: TcType > Bool
 isSigmaTy returns true of any qualified type. It doesn't
 *necessarily* have any foralls. E.g
 f :: (?x::Int) => Int > Int
isSigmaTy ty  Just ty' < tcView ty = isSigmaTy ty'
isSigmaTy (ForAllTy {}) = True
isSigmaTy (FunTy a _) = isPredTy a
isSigmaTy _ = False
isRhoTy :: TcType > Bool  True of TcRhoTypes; see Note [TcRhoType]
isRhoTy ty  Just ty' < tcView ty = isRhoTy ty'
isRhoTy (ForAllTy {}) = False
isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r
isRhoTy _ = True
  Like 'isRhoTy', but also says 'True' for 'Infer' types
isRhoExpTy :: ExpType > Bool
isRhoExpTy (Check ty) = isRhoTy ty
isRhoExpTy (Infer {}) = True
isOverloadedTy :: Type > Bool
 Yes for a type of a function that might require evidencepassing
 Used only by bindLocalMethods
isOverloadedTy ty  Just ty' < tcView ty = isOverloadedTy ty'
isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty
isOverloadedTy (FunTy a _) = isPredTy a
isOverloadedTy _ = False
isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
isUnitTy, isCharTy, isAnyTy :: Type > Bool
isFloatTy = is_tc floatTyConKey
isDoubleTy = is_tc doubleTyConKey
isIntegerTy = is_tc integerTyConKey
isIntTy = is_tc intTyConKey
isWordTy = is_tc wordTyConKey
isBoolTy = is_tc boolTyConKey
isUnitTy = is_tc unitTyConKey
isCharTy = is_tc charTyConKey
isAnyTy = is_tc anyTyConKey
  Does a type represent a floatingpoint number?
isFloatingTy :: Type > Bool
isFloatingTy ty = isFloatTy ty  isDoubleTy ty
  Is a type 'String'?
isStringTy :: Type > Bool
isStringTy ty
= case tcSplitTyConApp_maybe ty of
Just (tc, [arg_ty]) > tc == listTyCon && isCharTy arg_ty
_ > False
  Is a type a 'CallStack'?
isCallStackTy :: Type > Bool
isCallStackTy ty
 Just tc < tyConAppTyCon_maybe ty
= tc `hasKey` callStackTyConKey
 otherwise
= False
  Is a 'PredType' a 'CallStack' implicit parameter?

 If so, return the name of the parameter.
isCallStackPred :: Class > [Type] > Maybe FastString
isCallStackPred cls tys
 [ty1, ty2] < tys
, isIPClass cls
, isCallStackTy ty2
= isStrLitTy ty1
 otherwise
= Nothing
hasIPPred :: PredType > Bool
hasIPPred pred
= case classifyPredType pred of
ClassPred cls tys
 isIPClass cls > True
 isCTupleClass cls > any hasIPPred tys
_other > False
is_tc :: Unique > Type > Bool
 Newtypes are opaque to this
is_tc uniq ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) > uniq == getUnique tc
Nothing > False
  Does the given tyvar appear at the head of a chain of applications
 (a t1 ... tn)
isTyVarHead :: TcTyVar > TcType > Bool
isTyVarHead tv (TyVarTy tv') = tv == tv'
isTyVarHead tv (AppTy fun _) = isTyVarHead tv fun
isTyVarHead tv (CastTy ty _) = isTyVarHead tv ty
isTyVarHead _ (TyConApp {}) = False
isTyVarHead _ (LitTy {}) = False
isTyVarHead _ (ForAllTy {}) = False
isTyVarHead _ (FunTy {}) = False
isTyVarHead _ (CoercionTy {}) = False
  Is the equality
 a ~r ...a....
 definitely insoluble or not?
 a ~r Maybe a  Definitely insoluble
 a ~N ...(F a)...  Not definitely insoluble
  Perhaps (F a) reduces to Int
 a ~R ...(N a)...  Not definitely insoluble
  Perhaps newtype N a = MkN Int
 See Note [Occurs check error] in
 TcCanonical for the motivation for this function.
isInsolubleOccursCheck :: EqRel > TcTyVar > TcType > Bool
isInsolubleOccursCheck eq_rel tv ty
= go ty
where
go ty  Just ty' < tcView ty = go ty'
go (TyVarTy tv') = tv == tv'  go (tyVarKind tv')
go (LitTy {}) = False
go (AppTy t1 t2) = case eq_rel of  See Note [AppTy and ReprEq]
NomEq > go t1  go t2
ReprEq > go t1
go (FunTy t1 t2) = go t1  go t2
go (ForAllTy (TvBndr tv' _) inner_ty)
 tv' == tv = False
 otherwise = go (tyVarKind tv')  go inner_ty
go (CastTy ty _) = go ty  ToDo: what about the coercion
go (CoercionTy _) = False  ToDo: what about the coercion
go (TyConApp tc tys)
 isGenerativeTyCon tc role = any go tys
 otherwise = any go (drop (tyConArity tc) tys)
 (a ~ F b a), where F has arity 1,
 has an insoluble occurs check
role = eqRelRole eq_rel
{ Note [AppTy and ReprEq]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a ~R# b a
a ~R# a b
The former is /not/ a definite error; we might instantiate 'b' with Id
newtype Id a = MkId a
but the latter /is/ a definite error.
On the other hand, with nominal equality, both are definite errors
}
isRigidTy :: TcType > Bool
isRigidTy ty
 Just (tc,_) < tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
 Just {} < tcSplitAppTy_maybe ty = True
 isForAllTy ty = True
 otherwise = False
{
************************************************************************
* *
\subsection{Misc}
* *
************************************************************************
Note [Visible type application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC implements a generalisation of the algorithm described in the
"Visible Type Application" paper (available from
http://www.cis.upenn.edu/~sweirich/publications.html). A key part
of that algorithm is to distinguish userspecified variables from inferred
variables. For example, the following should typecheck:
f :: forall a b. a > b > b
f = const id
g = const id
x = f @Int @Bool 5 False
y = g 5 @Bool False
The idea is that we wish to allow visible type application when we are
instantiating a specified, fixed variable. In practice, specified, fixed
variables are either written in a type signature (or
annotation), OR are imported from another module. (We could do better here,
for example by doing SCC analysis on parts of a module and considering any
type from outside one's SCC to be fully specified, but this is very confusing to
users. The simple rule above is much more straightforward and predictable.)
So, both of f's quantified variables are specified and may be instantiated.
But g has no type signature, so only id's variable is specified (because id
is imported). We write the type of g as forall {a}. a > forall b. b > b.
Note that the a is in braces, meaning it cannot be instantiated with
visible type application.
Tracking specified vs. inferred variables is done conveniently by a field
in TyBinder.
}
deNoteType :: Type > Type
 Remove all *outermost* type synonyms and other notes
deNoteType ty  Just ty' < coreView ty = deNoteType ty'
deNoteType ty = ty
{
Find the free tycons and classes of a type. This is used in the front
end of the compiler.
}
{
************************************************************************
* *
\subsection[TysWiredInexttype]{External types}
* *
************************************************************************
The compiler's foreign function interface supports the passing of a
restricted set of types as arguments and results (the restricting factor
being the )
}
tcSplitIOType_maybe :: Type > Maybe (TyCon, Type)
 (tcSplitIOType_maybe t) returns Just (IO,t',co)
 if co : t ~ IO t'
 returns Nothing otherwise
tcSplitIOType_maybe ty
= case tcSplitTyConApp_maybe ty of
Just (io_tycon, [io_res_ty])
 io_tycon `hasKey` ioTyConKey >
Just (io_tycon, io_res_ty)
_ >
Nothing
isFFITy :: Type > Bool
 True for any TyCon that can possibly be an arg or result of an FFI call
isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
isFFIArgumentTy :: DynFlags > Safety > Type > Validity
 Checks for valid argument type for a 'foreign import'
isFFIArgumentTy dflags safety ty
= checkRepTyCon (legalOutgoingTyCon dflags safety) ty
isFFIExternalTy :: Type > Validity
 Types that are allowed as arguments of a 'foreign export'
isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
isFFIImportResultTy :: DynFlags > Type > Validity
isFFIImportResultTy dflags ty
= checkRepTyCon (legalFIResultTyCon dflags) ty
isFFIExportResultTy :: Type > Validity
isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
isFFIDynTy :: Type > Type > Validity
 The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
 either, and the wrapped function type must be equal to the given type.
 We assume that all types have been run through normaliseFfiType, so we don't
 need to worry about expanding newtypes here.
isFFIDynTy expected ty
 Note [Foreign import dynamic]
 In the example below, expected would be 'CInt > IO ()', while ty would
 be 'FunPtr (CDouble > IO ())'.
 Just (tc, [ty']) < splitTyConApp_maybe ty
, tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey]
, eqType ty' expected
= IsValid
 otherwise
= NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma
, text " Actual:" <+> ppr ty ])
isFFILabelTy :: Type > Validity
 The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
isFFILabelTy ty = checkRepTyCon ok ty
where
ok tc  tc `hasKey` funPtrTyConKey  tc `hasKey` ptrTyConKey
= IsValid
 otherwise
= NotValid (text "A foreignimported address (via &foo) must have type (Ptr a) or (FunPtr a)")
isFFIPrimArgumentTy :: DynFlags > Type > Validity
 Checks for valid argument type for a 'foreign import prim'
 Currently they must all be simple unlifted types, or the wellknown type
 Any, which can be used to pass the address to a Haskell object on the heap to
 the foreign function.
isFFIPrimArgumentTy dflags ty
 isAnyTy ty = IsValid
 otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
isFFIPrimResultTy :: DynFlags > Type > Validity
 Checks for valid result type for a 'foreign import prim' Currently
 it must be an unlifted type, including unboxed tuples, unboxed
 sums, or the wellknown type Any.
isFFIPrimResultTy dflags ty
 isAnyTy ty = IsValid
 otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
isFunPtrTy :: Type > Bool
isFunPtrTy ty
 Just (tc, [_]) < splitTyConApp_maybe ty
= tc `hasKey` funPtrTyConKey
 otherwise
= False
 normaliseFfiType gets run before checkRepTyCon, so we don't
 need to worry about looking through newtypes or type functions
 here; that's already been taken care of.
checkRepTyCon :: (TyCon > Validity) > Type > Validity
checkRepTyCon check_tc ty
= case splitTyConApp_maybe ty of
Just (tc, tys)
 isNewTyCon tc > NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
 otherwise > case check_tc tc of
IsValid > IsValid
NotValid extra > NotValid (msg $$ extra)
Nothing > NotValid (quotes (ppr ty) <+> text "is not a data type")
where
msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call"
mk_nt_reason tc tys
 null tys = text "because its data constructor is not in scope"
 otherwise = text "because the data constructor for"
<+> quotes (ppr tc) <+> text "is not in scope"
nt_fix = text "Possible fix: import the data constructor to bring it into scope"
{
Note [Foreign import dynamic]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A dynamic stub must be of the form 'FunPtr ft > ft' where ft is any foreign
type. Similarly, a wrapper stub must be of the form 'ft > IO (FunPtr ft)'.
We use isFFIDynTy to check whether a signature is wellformed. For example,
given a (illegal) declaration like:
foreign import ccall "dynamic"
foo :: FunPtr (CDouble > IO ()) > CInt > IO ()
isFFIDynTy will compare the 'FunPtr' type 'CDouble > IO ()' with the curried
result type 'CInt > IO ()', and return False, as they are not equal.

These chaps do the work; they are not exported

}
legalFEArgTyCon :: TyCon > Validity
legalFEArgTyCon tc
 It's illegal to make foreign exports that take unboxed
 arguments. The RTS API currently can't invoke such things. SDM 7/2000
= boxedMarshalableTyCon tc
legalFIResultTyCon :: DynFlags > TyCon > Validity
legalFIResultTyCon dflags tc
 tc == unitTyCon = IsValid
 otherwise = marshalableTyCon dflags tc
legalFEResultTyCon :: TyCon > Validity
legalFEResultTyCon tc
 tc == unitTyCon = IsValid
 otherwise = boxedMarshalableTyCon tc
legalOutgoingTyCon :: DynFlags > Safety > TyCon > Validity
 Checks validity of types going from Haskell > external world
legalOutgoingTyCon dflags _ tc
= marshalableTyCon dflags tc
legalFFITyCon :: TyCon > Validity
 True for any TyCon that can possibly be an arg or result of an FFI call
legalFFITyCon tc
 isUnliftedTyCon tc = IsValid
 tc == unitTyCon = IsValid
 otherwise = boxedMarshalableTyCon tc
marshalableTyCon :: DynFlags > TyCon > Validity
marshalableTyCon dflags tc
 isUnliftedTyCon tc
, not (isUnboxedTupleTyCon tc  isUnboxedSumTyCon tc)
, not (null (tyConPrimRep tc))  Note [Marshalling void]
= validIfUnliftedFFITypes dflags
 otherwise
= boxedMarshalableTyCon tc
boxedMarshalableTyCon :: TyCon > Validity
boxedMarshalableTyCon tc
 getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
, int32TyConKey, int64TyConKey
, wordTyConKey, word8TyConKey, word16TyConKey
, word32TyConKey, word64TyConKey
, floatTyConKey, doubleTyConKey
, ptrTyConKey, funPtrTyConKey
, charTyConKey
, stablePtrTyConKey
, boolTyConKey
]
= IsValid
 otherwise = NotValid empty
legalFIPrimArgTyCon :: DynFlags > TyCon > Validity
 Check args of 'foreign import prim', only allow simple unlifted types.
 Strictly speaking it is unnecessary to ban unboxed tuples and sums here since
 currently they're of the wrong kind to use in function args anyway.
legalFIPrimArgTyCon dflags tc
 isUnliftedTyCon tc
, not (isUnboxedTupleTyCon tc  isUnboxedSumTyCon tc)
= validIfUnliftedFFITypes dflags
 otherwise
= NotValid unlifted_only
legalFIPrimResultTyCon :: DynFlags > TyCon > Validity
 Check result type of 'foreign import prim'. Allow simple unlifted
 types and also unboxed tuple and sum result types.
legalFIPrimResultTyCon dflags tc
 isUnliftedTyCon tc
, isUnboxedTupleTyCon tc  isUnboxedSumTyCon tc
 not (null (tyConPrimRep tc))  Note [Marshalling void]
= validIfUnliftedFFITypes dflags
 otherwise
= NotValid unlifted_only
unlifted_only :: MsgDoc
unlifted_only = text "foreign import prim only accepts simple unlifted types"
validIfUnliftedFFITypes :: DynFlags > Validity
validIfUnliftedFFITypes dflags
 xopt LangExt.UnliftedFFITypes dflags = IsValid
 otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes")
{
Note [Marshalling void]
~~~~~~~~~~~~~~~~~~~~~~~
We don't treat State# (whose PrimRep is VoidRep) as marshalable.
In turn that means you can't write
foreign import foo :: Int > State# RealWorld
Reason: the back end falls over with panic "primRepHint:VoidRep";
and there is no compelling reason to permit it
}
{
************************************************************************
* *
The "Paterson size" of a type
* *
************************************************************************
}
{
Note [Paterson conditions on PredTypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We are considering whether *class* constraints terminate
(see Note [Paterson conditions]). Precisely, the Paterson conditions
would have us check that "the constraint has fewer constructors and variables
(taken together and counting repetitions) than the head.".
However, we can be a bit more refined by looking at which kind of constraint
this actually is. There are two main tricks:
1. It seems like it should be OK not to count the tuple type constructor
for a PredType like (Show a, Eq a) :: Constraint, since we don't
count the "implicit" tuple in the ThetaType itself.
In fact, the Paterson test just checks *each component* of the top level
ThetaType against the size bound, one at a time. By analogy, it should be
OK to return the size of the *largest* tuple component as the size of the
whole tuple.
2. Once we get into an implicit parameter or equality we
can't get back to a class constraint, so it's safe
to say "size 0". See Trac #4200.
NB: we don't want to detect PredTypes in sizeType (and then call
sizePred on them), or we might get an infinite loop if that PredType
is irreducible. See Trac #5581.
}
type TypeSize = IntWithInf
sizeType :: Type > TypeSize
 Size of a type: the number of variables and constructors
 Ignore kinds altogether
sizeType = go
where
go ty  Just exp_ty < tcView ty = go exp_ty
go (TyVarTy {}) = 1
go (TyConApp tc tys)
 isTypeFamilyTyCon tc = infinity  Typefamily applications can
 expand to any arbitrary size
 otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1
 Why filter out invisible args? I suppose any
 size ordering is sound, but why is this better?
 I came across this when investigating #14010.
go (LitTy {}) = 1
go (FunTy arg res) = go arg + go res + 1
go (AppTy fun arg) = go fun + go arg
go (ForAllTy (TvBndr tv vis) ty)
 isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1
 otherwise = go ty + 1
go (CastTy ty _) = go ty
go (CoercionTy {}) = 0
sizeTypes :: [Type] > TypeSize
sizeTypes tys = sum (map sizeType tys)



  For every arg a tycon can take, the returned list says True if the argument
 is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
 allow for oversaturation.
tcTyConVisibilities :: TyCon > [Bool]
tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
where
tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc)
tc_return_kind_viss = map isVisibleBinder (fst $ tcSplitPiTys (tyConResKind tc))
  If the tycon is applied to the types, is the next argument visible?
isNextTyConArgVisible :: TyCon > [Type] > Bool
isNextTyConArgVisible tc tys
= tcTyConVisibilities tc `getNth` length tys
  Should this type be applied to a visible argument?
isNextArgVisible :: TcType > Bool
isNextArgVisible ty
 Just (bndr, _) < tcSplitPiTy_maybe ty = isVisibleBinder bndr
 otherwise = True
 this second case might happen if, say, we have an unzonked TauTv.
 But TauTvs can't range over types that take invisible arguments