never executed always true always false
    1 {-# LANGUAGE CPP #-}
    2 {-# LANGUAGE DeriveFunctor #-}
    3 {-# LANGUAGE MultiWayIf #-}
    4 
    5 module GHC.Tc.Solver.Canonical(
    6      canonicalize,
    7      unifyDerived,
    8      makeSuperClasses,
    9      StopOrContinue(..), stopWith, continueWith, andWhenContinue,
   10      solveCallStack    -- For GHC.Tc.Solver
   11   ) where
   12 
   13 import GHC.Prelude
   14 
   15 import GHC.Tc.Types.Constraint
   16 import GHC.Core.Predicate
   17 import GHC.Tc.Types.Origin
   18 import GHC.Tc.Utils.Concrete ( newConcretePrimWanted )
   19 import GHC.Tc.Utils.Unify
   20 import GHC.Tc.Utils.TcType
   21 import GHC.Core.Type
   22 import GHC.Tc.Solver.Rewrite
   23 import GHC.Tc.Solver.Monad
   24 import GHC.Tc.Solver.InertSet
   25 import GHC.Tc.Types.Evidence
   26 import GHC.Tc.Types.EvTerm
   27 import GHC.Core.Class
   28 import GHC.Core.TyCon
   29 import GHC.Core.Multiplicity
   30 import GHC.Core.TyCo.Rep   -- cleverly decomposes types, good for completeness checking
   31 import GHC.Core.Coercion
   32 import GHC.Core.Coercion.Axiom
   33 import GHC.Core.Reduction
   34 import GHC.Core
   35 import GHC.Types.Id( mkTemplateLocals )
   36 import GHC.Core.FamInstEnv ( FamInstEnvs )
   37 import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
   38 import GHC.Types.Var
   39 import GHC.Types.Var.Env( mkInScopeSet )
   40 import GHC.Types.Var.Set( delVarSetList, anyVarSet )
   41 import GHC.Utils.Outputable
   42 import GHC.Utils.Panic
   43 import GHC.Utils.Panic.Plain
   44 import GHC.Builtin.Types ( anyTypeOfKind )
   45 import GHC.Builtin.Types.Prim ( concretePrimTyCon )
   46 import GHC.Types.Name.Set
   47 import GHC.Types.Name.Reader
   48 import GHC.Hs.Type( HsIPName(..) )
   49 
   50 import GHC.Data.Pair
   51 import GHC.Utils.Misc
   52 import GHC.Data.Bag
   53 import GHC.Utils.Monad
   54 import Control.Monad
   55 import Data.Maybe ( isJust, isNothing )
   56 import Data.List  ( zip4 )
   57 import GHC.Types.Basic
   58 
   59 import Data.Bifunctor ( bimap )
   60 import Data.Foldable ( traverse_ )
   61 
   62 {-
   63 ************************************************************************
   64 *                                                                      *
   65 *                      The Canonicaliser                               *
   66 *                                                                      *
   67 ************************************************************************
   68 
   69 Note [Canonicalization]
   70 ~~~~~~~~~~~~~~~~~~~~~~~
   71 
   72 Canonicalization converts a simple constraint to a canonical form. It is
   73 unary (i.e. treats individual constraints one at a time).
   74 
   75 Constraints originating from user-written code come into being as
   76 CNonCanonicals. We know nothing about these constraints. So, first:
   77 
   78      Classify CNonCanoncal constraints, depending on whether they
   79      are equalities, class predicates, or other.
   80 
   81 Then proceed depending on the shape of the constraint. Generally speaking,
   82 each constraint gets rewritten and then decomposed into one of several forms
   83 (see type Ct in GHC.Tc.Types).
   84 
   85 When an already-canonicalized constraint gets kicked out of the inert set,
   86 it must be recanonicalized. But we know a bit about its shape from the
   87 last time through, so we can skip the classification step.
   88 
   89 -}
   90 
   91 -- Top-level canonicalization
   92 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   93 
   94 canonicalize :: Ct -> TcS (StopOrContinue Ct)
   95 canonicalize (CNonCanonical { cc_ev = ev })
   96   = {-# SCC "canNC" #-}
   97     canNC ev
   98 
   99 canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
  100   = canForAll ev pend_sc
  101 
  102 canonicalize (CSpecialCan { cc_ev = ev, cc_special_pred = special_pred, cc_xi = xi })
  103   = canSpecial ev special_pred xi
  104 
  105 canonicalize (CIrredCan { cc_ev = ev })
  106   = canNC ev
  107     -- Instead of rewriting the evidence before classifying, it's possible we
  108     -- can make progress without the rewrite. Try this first.
  109     -- For insolubles (all of which are equalities), do /not/ rewrite the arguments
  110     -- In #14350 doing so led entire-unnecessary and ridiculously large
  111     -- type function expansion.  Instead, canEqNC just applies
  112     -- the substitution to the predicate, and may do decomposition;
  113     --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
  114 
  115 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
  116                        , cc_tyargs = xis, cc_pend_sc = pend_sc
  117                        , cc_fundeps = fds })
  118   = {-# SCC "canClass" #-}
  119     canClass ev cls xis pend_sc fds
  120 
  121 canonicalize (CEqCan { cc_ev     = ev
  122                      , cc_lhs    = lhs
  123                      , cc_rhs    = rhs
  124                      , cc_eq_rel = eq_rel })
  125   = {-# SCC "canEqLeafTyVarEq" #-}
  126     canEqNC ev eq_rel (canEqLHSType lhs) rhs
  127 
  128 canNC :: CtEvidence -> TcS (StopOrContinue Ct)
  129 canNC ev =
  130   case classifyPredType pred of
  131       ClassPred cls tys     -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
  132                                   canClassNC ev cls tys
  133       EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
  134                                   canEqNC    ev eq_rel ty1 ty2
  135       IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr pred)
  136                                   canIrred ev
  137       ForAllPred tvs th p   -> do traceTcS "canEvNC:forall" (ppr pred)
  138                                   canForAllNC ev tvs th p
  139       SpecialPred tc ty     -> do traceTcS "canEvNC:special" (ppr pred)
  140                                   canSpecial ev tc ty
  141   where
  142     pred = ctEvPred ev
  143 
  144 {-
  145 ************************************************************************
  146 *                                                                      *
  147 *                      Class Canonicalization
  148 *                                                                      *
  149 ************************************************************************
  150 -}
  151 
  152 canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
  153 -- "NC" means "non-canonical"; that is, we have got here
  154 -- from a NonCanonical constraint, not from a CDictCan
  155 -- Precondition: EvVar is class evidence
  156 canClassNC ev cls tys
  157   | isGiven ev  -- See Note [Eagerly expand given superclasses]
  158   = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
  159        ; emitWork sc_cts
  160        ; canClass ev cls tys False fds }
  161 
  162   | isWanted ev
  163   , Just ip_name <- isCallStackPred cls tys
  164   , isPushCallStackOrigin orig
  165   -- If we're given a CallStack constraint that arose from a function
  166   -- call, we need to push the current call-site onto the stack instead
  167   -- of solving it directly from a given.
  168   -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
  169   -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
  170   = do { -- First we emit a new constraint that will capture the
  171          -- given CallStack.
  172        ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
  173                             -- We change the origin to IPOccOrigin so
  174                             -- this rule does not fire again.
  175                             -- See Note [Overview of implicit CallStacks]
  176 
  177        ; new_ev <- newWantedEvVarNC new_loc pred
  178 
  179          -- Then we solve the wanted by pushing the call-site
  180          -- onto the newly emitted CallStack
  181        ; let ev_cs = EvCsPushCall (callStackOriginFS orig)
  182                                   (ctLocSpan loc) (ctEvExpr new_ev)
  183        ; solveCallStack ev ev_cs
  184 
  185        ; canClass new_ev cls tys
  186                   False -- No superclasses
  187                   False -- No top level instances for fundeps
  188        }
  189 
  190   | otherwise
  191   = canClass ev cls tys (has_scs cls) fds
  192 
  193   where
  194     has_scs cls = not (null (classSCTheta cls))
  195     loc  = ctEvLoc ev
  196     orig = ctLocOrigin loc
  197     pred = ctEvPred ev
  198     fds  = classHasFds cls
  199 
  200 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
  201 -- Also called from GHC.Tc.Solver when defaulting call stacks
  202 solveCallStack ev ev_cs = do
  203   -- We're given ev_cs :: CallStack, but the evidence term should be a
  204   -- dictionary, so we have to coerce ev_cs to a dictionary for
  205   -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
  206   cs_tm <- evCallStack ev_cs
  207   let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
  208   setEvBindIfWanted ev ev_tm
  209 
  210 canClass :: CtEvidence
  211          -> Class -> [Type]
  212          -> Bool            -- True <=> un-explored superclasses
  213          -> Bool            -- True <=> unexploited fundep(s)
  214          -> TcS (StopOrContinue Ct)
  215 -- Precondition: EvVar is class evidence
  216 
  217 canClass ev cls tys pend_sc fds
  218   = -- all classes do *nominal* matching
  219     assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
  220     do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc tys
  221        ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns
  222              mk_ct new_ev = CDictCan { cc_ev = new_ev
  223                                      , cc_tyargs = xis
  224                                      , cc_class = cls
  225                                      , cc_pend_sc = pend_sc
  226                                      , cc_fundeps = fds }
  227        ; mb <- rewriteEvidence ev redn
  228 
  229        ; traceTcS "canClass" (vcat [ ppr ev
  230                                    , ppr xi, ppr mb ])
  231        ; return (fmap mk_ct mb) }
  232   where
  233     cls_tc = classTyCon cls
  234 
  235 {- Note [The superclass story]
  236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  237 We need to add superclass constraints for two reasons:
  238 
  239 * For givens [G], they give us a route to proof.  E.g.
  240     f :: Ord a => a -> Bool
  241     f x = x == x
  242   We get a Wanted (Eq a), which can only be solved from the superclass
  243   of the Given (Ord a).
  244 
  245 * For wanteds [W], and deriveds [WD], [D], they may give useful
  246   functional dependencies.  E.g.
  247      class C a b | a -> b where ...
  248      class C a b => D a b where ...
  249   Now a [W] constraint (D Int beta) has (C Int beta) as a superclass
  250   and that might tell us about beta, via C's fundeps.  We can get this
  251   by generating a [D] (C Int beta) constraint.  It's derived because
  252   we don't actually have to cough up any evidence for it; it's only there
  253   to generate fundep equalities.
  254 
  255 See Note [Why adding superclasses can help].
  256 
  257 For these reasons we want to generate superclass constraints for both
  258 Givens and Wanteds. But:
  259 
  260 * (Minor) they are often not needed, so generating them aggressively
  261   is a waste of time.
  262 
  263 * (Major) if we want recursive superclasses, there would be an infinite
  264   number of them.  Here is a real-life example (#10318);
  265 
  266      class (Frac (Frac a) ~ Frac a,
  267             Fractional (Frac a),
  268             IntegralDomain (Frac a))
  269          => IntegralDomain a where
  270       type Frac a :: *
  271 
  272   Notice that IntegralDomain has an associated type Frac, and one
  273   of IntegralDomain's superclasses is another IntegralDomain constraint.
  274 
  275 So here's the plan:
  276 
  277 1. Eagerly generate superclasses for given (but not wanted)
  278    constraints; see Note [Eagerly expand given superclasses].
  279    This is done using mkStrictSuperClasses in canClassNC, when
  280    we take a non-canonical Given constraint and cannonicalise it.
  281 
  282    However stop if you encounter the same class twice.  That is,
  283    mkStrictSuperClasses expands eagerly, but has a conservative
  284    termination condition: see Note [Expanding superclasses] in GHC.Tc.Utils.TcType.
  285 
  286 2. Solve the wanteds as usual, but do no further expansion of
  287    superclasses for canonical CDictCans in solveSimpleGivens or
  288    solveSimpleWanteds; Note [Danger of adding superclasses during solving]
  289 
  290    However, /do/ continue to eagerly expand superclasses for new /given/
  291    /non-canonical/ constraints (canClassNC does this).  As #12175
  292    showed, a type-family application can expand to a class constraint,
  293    and we want to see its superclasses for just the same reason as
  294    Note [Eagerly expand given superclasses].
  295 
  296 3. If we have any remaining unsolved wanteds
  297         (see Note [When superclasses help] in GHC.Tc.Types.Constraint)
  298    try harder: take both the Givens and Wanteds, and expand
  299    superclasses again.  See the calls to expandSuperClasses in
  300    GHC.Tc.Solver.simpl_loop and solveWanteds.
  301 
  302    This may succeed in generating (a finite number of) extra Givens,
  303    and extra Deriveds. Both may help the proof.
  304 
  305 3a An important wrinkle: only expand Givens from the current level.
  306    Two reasons:
  307       - We only want to expand it once, and that is best done at
  308         the level it is bound, rather than repeatedly at the leaves
  309         of the implication tree
  310       - We may be inside a type where we can't create term-level
  311         evidence anyway, so we can't superclass-expand, say,
  312         (a ~ b) to get (a ~# b).  This happened in #15290.
  313 
  314 4. Go round to (2) again.  This loop (2,3,4) is implemented
  315    in GHC.Tc.Solver.simpl_loop.
  316 
  317 The cc_pend_sc flag in a CDictCan records whether the superclasses of
  318 this constraint have been expanded.  Specifically, in Step 3 we only
  319 expand superclasses for constraints with cc_pend_sc set to true (i.e.
  320 isPendingScDict holds).
  321 
  322 Why do we do this?  Two reasons:
  323 
  324 * To avoid repeated work, by repeatedly expanding the superclasses of
  325   same constraint,
  326 
  327 * To terminate the above loop, at least in the -XNoRecursiveSuperClasses
  328   case.  If there are recursive superclasses we could, in principle,
  329   expand forever, always encountering new constraints.
  330 
  331 When we take a CNonCanonical or CIrredCan, but end up classifying it
  332 as a CDictCan, we set the cc_pend_sc flag to False.
  333 
  334 Note [Superclass loops]
  335 ~~~~~~~~~~~~~~~~~~~~~~~
  336 Suppose we have
  337   class C a => D a
  338   class D a => C a
  339 
  340 Then, when we expand superclasses, we'll get back to the self-same
  341 predicate, so we have reached a fixpoint in expansion and there is no
  342 point in fruitlessly expanding further.  This case just falls out from
  343 our strategy.  Consider
  344   f :: C a => a -> Bool
  345   f x = x==x
  346 Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
  347 G] d2: D a, [G] d3: C a (psc).  (The "psc" means it has its sc_pend flag set.)
  348 When processing d3 we find a match with d1 in the inert set, and we always
  349 keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
  350 GHC.Tc.Solver.Interact.  So d3 dies a quick, happy death.
  351 
  352 Note [Eagerly expand given superclasses]
  353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  354 In step (1) of Note [The superclass story], why do we eagerly expand
  355 Given superclasses by one layer?  (By "one layer" we mean expand transitively
  356 until you meet the same class again -- the conservative criterion embodied
  357 in expandSuperClasses.  So a "layer" might be a whole stack of superclasses.)
  358 We do this eagerly for Givens mainly because of some very obscure
  359 cases like this:
  360 
  361    instance Bad a => Eq (T a)
  362 
  363    f :: (Ord (T a)) => blah
  364    f x = ....needs Eq (T a), Ord (T a)....
  365 
  366 Here if we can't satisfy (Eq (T a)) from the givens we'll use the
  367 instance declaration; but then we are stuck with (Bad a).  Sigh.
  368 This is really a case of non-confluent proofs, but to stop our users
  369 complaining we expand one layer in advance.
  370 
  371 Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
  372 
  373 We also want to do this if we have
  374 
  375    f :: F (T a) => blah
  376 
  377 where
  378    type instance F (T a) = Ord (T a)
  379 
  380 So we may need to do a little work on the givens to expose the
  381 class that has the superclasses.  That's why the superclass
  382 expansion for Givens happens in canClassNC.
  383 
  384 This same scenario happens with quantified constraints, whose superclasses
  385 are also eagerly expanded. Test case: typecheck/should_compile/T16502b
  386 These are handled in canForAllNC, analogously to canClassNC.
  387 
  388 Note [Why adding superclasses can help]
  389 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  390 Examples of how adding superclasses can help:
  391 
  392     --- Example 1
  393         class C a b | a -> b
  394     Suppose we want to solve
  395          [G] C a b
  396          [W] C a beta
  397     Then adding [D] beta~b will let us solve it.
  398 
  399     -- Example 2 (similar but using a type-equality superclass)
  400         class (F a ~ b) => C a b
  401     And try to sllve:
  402          [G] C a b
  403          [W] C a beta
  404     Follow the superclass rules to add
  405          [G] F a ~ b
  406          [D] F a ~ beta
  407     Now we get [D] beta ~ b, and can solve that.
  408 
  409     -- Example (tcfail138)
  410       class L a b | a -> b
  411       class (G a, L a b) => C a b
  412 
  413       instance C a b' => G (Maybe a)
  414       instance C a b  => C (Maybe a) a
  415       instance L (Maybe a) a
  416 
  417     When solving the superclasses of the (C (Maybe a) a) instance, we get
  418       [G] C a b, and hance by superclasses, [G] G a, [G] L a b
  419       [W] G (Maybe a)
  420     Use the instance decl to get
  421       [W] C a beta
  422     Generate its derived superclass
  423       [D] L a beta.  Now using fundeps, combine with [G] L a b to get
  424       [D] beta ~ b
  425     which is what we want.
  426 
  427 Note [Danger of adding superclasses during solving]
  428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  429 Here's a serious, but now out-dated example, from #4497:
  430 
  431    class Num (RealOf t) => Normed t
  432    type family RealOf x
  433 
  434 Assume the generated wanted constraint is:
  435    [W] RealOf e ~ e
  436    [W] Normed e
  437 
  438 If we were to be adding the superclasses during simplification we'd get:
  439    [W] RealOf e ~ e
  440    [W] Normed e
  441    [D] RealOf e ~ fuv
  442    [D] Num fuv
  443 ==>
  444    e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
  445 
  446 While looks exactly like our original constraint. If we add the
  447 superclass of (Normed fuv) again we'd loop.  By adding superclasses
  448 definitely only once, during canonicalisation, this situation can't
  449 happen.
  450 
  451 Mind you, now that Wanteds cannot rewrite Derived, I think this particular
  452 situation can't happen.
  453 
  454 Note [Nested quantified constraint superclasses]
  455 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  456 Consider (typecheck/should_compile/T17202)
  457 
  458   class C1 a
  459   class (forall c. C1 c) => C2 a
  460   class (forall b. (b ~ F a) => C2 a) => C3 a
  461 
  462 Elsewhere in the code, we get a [G] g1 :: C3 a. We expand its superclass
  463 to get [G] g2 :: (forall b. (b ~ F a) => C2 a). This constraint has a
  464 superclass, as well. But we now must be careful: we cannot just add
  465 (forall c. C1 c) as a Given, because we need to remember g2's context.
  466 That new constraint is Given only when forall b. (b ~ F a) is true.
  467 
  468 It's tempting to make the new Given be (forall b. (b ~ F a) => forall c. C1 c),
  469 but that's problematic, because it's nested, and ForAllPred is not capable
  470 of representing a nested quantified constraint. (We could change ForAllPred
  471 to allow this, but the solution in this Note is much more local and simpler.)
  472 
  473 So, we swizzle it around to get (forall b c. (b ~ F a) => C1 c).
  474 
  475 More generally, if we are expanding the superclasses of
  476   g0 :: forall tvs. theta => cls tys
  477 and find a superclass constraint
  478   forall sc_tvs. sc_theta => sc_inner_pred
  479 we must have a selector
  480   sel_id :: forall cls_tvs. cls cls_tvs -> forall sc_tvs. sc_theta => sc_inner_pred
  481 and thus build
  482   g_sc :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred
  483   g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. \ sc_theta_ids.
  484          sel_id tys (g0 tvs theta_ids) sc_tvs sc_theta_ids
  485 
  486 Actually, we cheat a bit by eta-reducing: note that sc_theta_ids are both the
  487 last bound variables and the last arguments. This avoids the need to produce
  488 the sc_theta_ids at all. So our final construction is
  489 
  490   g_sc = /\ tvs. /\ sc_tvs. \ theta_ids.
  491          sel_id tys (g0 tvs theta_ids) sc_tvs
  492 
  493   -}
  494 
  495 makeSuperClasses :: [Ct] -> TcS [Ct]
  496 -- Returns strict superclasses, transitively, see Note [The superclasses story]
  497 -- See Note [The superclass story]
  498 -- The loop-breaking here follows Note [Expanding superclasses] in GHC.Tc.Utils.TcType
  499 -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s
  500 --    superclasses, up to /and including/ the first repetition of C
  501 --
  502 -- Example:  class D a => C a
  503 --           class C [a] => D a
  504 -- makeSuperClasses (C x) will return (D x, C [x])
  505 --
  506 -- NB: the incoming constraints have had their cc_pend_sc flag already
  507 --     flipped to False, by isPendingScDict, so we are /obliged/ to at
  508 --     least produce the immediate superclasses
  509 makeSuperClasses cts = concatMapM go cts
  510   where
  511     go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
  512       = mkStrictSuperClasses ev [] [] cls tys
  513     go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
  514       = assertPpr (isClassPred pred) (ppr pred) $  -- The cts should all have
  515                                                    -- class pred heads
  516         mkStrictSuperClasses ev tvs theta cls tys
  517       where
  518         (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
  519     go ct = pprPanic "makeSuperClasses" (ppr ct)
  520 
  521 mkStrictSuperClasses
  522     :: CtEvidence
  523     -> [TyVar] -> ThetaType  -- These two args are non-empty only when taking
  524                              -- superclasses of a /quantified/ constraint
  525     -> Class -> [Type] -> TcS [Ct]
  526 -- Return constraints for the strict superclasses of
  527 --   ev :: forall as. theta => cls tys
  528 mkStrictSuperClasses ev tvs theta cls tys
  529   = mk_strict_superclasses (unitNameSet (className cls))
  530                            ev tvs theta cls tys
  531 
  532 mk_strict_superclasses :: NameSet -> CtEvidence
  533                        -> [TyVar] -> ThetaType
  534                        -> Class -> [Type] -> TcS [Ct]
  535 -- Always return the immediate superclasses of (cls tys);
  536 -- and expand their superclasses, provided none of them are in rec_clss
  537 -- nor are repeated
  538 mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
  539                        tvs theta cls tys
  540   = concatMapM (do_one_given (mk_given_loc loc)) $
  541     classSCSelIds cls
  542   where
  543     dict_ids  = mkTemplateLocals theta
  544     size      = sizeTypes tys
  545 
  546     do_one_given given_loc sel_id
  547       | isUnliftedType sc_pred
  548       , not (null tvs && null theta)
  549       = -- See Note [Equality superclasses in quantified constraints]
  550         return []
  551       | otherwise
  552       = do { given_ev <- newGivenEvVar given_loc $
  553                          mk_given_desc sel_id sc_pred
  554            ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
  555       where
  556         sc_pred = classMethodInstTy sel_id tys
  557 
  558       -- See Note [Nested quantified constraint superclasses]
  559     mk_given_desc :: Id -> PredType -> (PredType, EvTerm)
  560     mk_given_desc sel_id sc_pred
  561       = (swizzled_pred, swizzled_evterm)
  562       where
  563         (sc_tvs, sc_rho)          = splitForAllTyCoVars sc_pred
  564         (sc_theta, sc_inner_pred) = splitFunTys sc_rho
  565 
  566         all_tvs       = tvs `chkAppend` sc_tvs
  567         all_theta     = theta `chkAppend` (map scaledThing sc_theta)
  568         swizzled_pred = mkInfSigmaTy all_tvs all_theta sc_inner_pred
  569 
  570         -- evar :: forall tvs. theta => cls tys
  571         -- sel_id :: forall cls_tvs. cls cls_tvs
  572         --                        -> forall sc_tvs. sc_theta => sc_inner_pred
  573         -- swizzled_evterm :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred
  574         swizzled_evterm = EvExpr $
  575           mkLams all_tvs $
  576           mkLams dict_ids $
  577           Var sel_id
  578             `mkTyApps` tys
  579             `App` (evId evar `mkVarApps` (tvs ++ dict_ids))
  580             `mkVarApps` sc_tvs
  581 
  582     mk_given_loc loc
  583        | isCTupleClass cls
  584        = loc   -- For tuple predicates, just take them apart, without
  585                -- adding their (large) size into the chain.  When we
  586                -- get down to a base predicate, we'll include its size.
  587                -- #10335
  588 
  589        | GivenOrigin skol_info <- ctLocOrigin loc
  590          -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
  591          -- for explantation of this transformation for givens
  592        = case skol_info of
  593             InstSkol -> loc { ctl_origin = GivenOrigin (InstSC size) }
  594             InstSC n -> loc { ctl_origin = GivenOrigin (InstSC (n `max` size)) }
  595             _        -> loc
  596 
  597        | otherwise  -- Probably doesn't happen, since this function
  598        = loc        -- is only used for Givens, but does no harm
  599 
  600 mk_strict_superclasses rec_clss ev tvs theta cls tys
  601   | all noFreeVarsOfType tys
  602   = return [] -- Wanteds with no variables yield no deriveds.
  603               -- See Note [Improvement from Ground Wanteds]
  604 
  605   | otherwise -- Wanted/Derived case, just add Derived superclasses
  606               -- that can lead to improvement.
  607   = assertPpr (null tvs && null theta) (ppr tvs $$ ppr theta) $
  608     concatMapM do_one_derived (immSuperClasses cls tys)
  609   where
  610     loc = ctEvLoc ev
  611 
  612     do_one_derived sc_pred
  613       = do { sc_ev <- newDerivedNC loc sc_pred
  614            ; mk_superclasses rec_clss sc_ev [] [] sc_pred }
  615 
  616 {- Note [Improvement from Ground Wanteds]
  617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  618 Suppose class C b a => D a b
  619 and consider
  620   [W] D Int Bool
  621 Is there any point in emitting [D] C Bool Int?  No!  The only point of
  622 emitting superclass constraints for W/D constraints is to get
  623 improvement, extra unifications that result from functional
  624 dependencies.  See Note [Why adding superclasses can help] above.
  625 
  626 But no variables means no improvement; case closed.
  627 -}
  628 
  629 mk_superclasses :: NameSet -> CtEvidence
  630                 -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
  631 -- Return this constraint, plus its superclasses, if any
  632 mk_superclasses rec_clss ev tvs theta pred
  633   | ClassPred cls tys <- classifyPredType pred
  634   = mk_superclasses_of rec_clss ev tvs theta cls tys
  635 
  636   | otherwise   -- Superclass is not a class predicate
  637   = return [mkNonCanonical ev]
  638 
  639 mk_superclasses_of :: NameSet -> CtEvidence
  640                    -> [TyVar] -> ThetaType -> Class -> [Type]
  641                    -> TcS [Ct]
  642 -- Always return this class constraint,
  643 -- and expand its superclasses
  644 mk_superclasses_of rec_clss ev tvs theta cls tys
  645   | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
  646                     ; return [this_ct] }  -- cc_pend_sc of this_ct = True
  647   | otherwise  = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
  648                                                           , ppr (isCTupleClass cls)
  649                                                           , ppr rec_clss
  650                                                           ])
  651                     ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
  652                     ; return (this_ct : sc_cts) }
  653                                    -- cc_pend_sc of this_ct = False
  654   where
  655     cls_nm     = className cls
  656     loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
  657                  -- Tuples never contribute to recursion, and can be nested
  658     rec_clss'  = rec_clss `extendNameSet` cls_nm
  659 
  660     this_ct | null tvs, null theta
  661             = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
  662                        , cc_pend_sc = loop_found, cc_fundeps = classHasFds cls }
  663                  -- NB: If there is a loop, we cut off, so we have not
  664                  --     added the superclasses, hence cc_pend_sc = True
  665             | otherwise
  666             = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
  667                              , qci_ev = ev
  668                              , qci_pend_sc = loop_found })
  669 
  670 
  671 {- Note [Equality superclasses in quantified constraints]
  672 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  673 Consider (#15359, #15593, #15625)
  674   f :: (forall a. theta => a ~ b) => stuff
  675 
  676 It's a bit odd to have a local, quantified constraint for `(a~b)`,
  677 but some people want such a thing (see the tickets). And for
  678 Coercible it is definitely useful
  679   f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q)))
  680                  => stuff
  681 
  682 Moreover it's not hard to arrange; we just need to look up /equality/
  683 constraints in the quantified-constraint environment, which we do in
  684 GHC.Tc.Solver.Interact.doTopReactOther.
  685 
  686 There is a wrinkle though, in the case where 'theta' is empty, so
  687 we have
  688   f :: (forall a. a~b) => stuff
  689 
  690 Now, potentially, the superclass machinery kicks in, in
  691 makeSuperClasses, giving us a a second quantified constraint
  692        (forall a. a ~# b)
  693 BUT this is an unboxed value!  And nothing has prepared us for
  694 dictionary "functions" that are unboxed.  Actually it does just
  695 about work, but the simplifier ends up with stuff like
  696    case (/\a. eq_sel d) of df -> ...(df @Int)...
  697 and fails to simplify that any further.  And it doesn't satisfy
  698 isPredTy any more.
  699 
  700 So for now we simply decline to take superclasses in the quantified
  701 case.  Instead we have a special case in GHC.Tc.Solver.Interact.doTopReactOther,
  702 which looks for primitive equalities specially in the quantified
  703 constraints.
  704 
  705 See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
  706 
  707 
  708 ************************************************************************
  709 *                                                                      *
  710 *                      Irreducibles canonicalization
  711 *                                                                      *
  712 ************************************************************************
  713 -}
  714 
  715 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
  716 -- Precondition: ty not a tuple and no other evidence form
  717 canIrred ev
  718   = do { let pred = ctEvPred ev
  719        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
  720        ; redn <- rewrite ev pred
  721        ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
  722 
  723     do { -- Re-classify, in case rewriting has improved its shape
  724          -- Code is like the canNC, except
  725          -- that the IrredPred branch stops work
  726        ; case classifyPredType (ctEvPred new_ev) of
  727            ClassPred cls tys     -> canClassNC new_ev cls tys
  728            EqPred eq_rel ty1 ty2 -> -- IrredPreds have kind Constraint, so
  729                                     -- cannot become EqPreds
  730                                     pprPanic "canIrred: EqPred"
  731                                       (ppr ev $$ ppr eq_rel $$ ppr ty1 $$ ppr ty2)
  732            ForAllPred tvs th p   -> -- this is highly suspect; Quick Look
  733                                     -- should never leave a meta-var filled
  734                                     -- in with a polytype. This is #18987.
  735                                     do traceTcS "canEvNC:forall" (ppr pred)
  736                                        canForAllNC ev tvs th p
  737            SpecialPred tc tys    -> -- IrredPreds have kind Constraint, so cannot
  738                                     -- become SpecialPreds
  739                                     pprPanic "canIrred: SpecialPred"
  740                                       (ppr ev $$ ppr tc $$ ppr tys)
  741            IrredPred {}          -> continueWith $
  742                                     mkIrredCt IrredShapeReason new_ev } }
  743 
  744 {- *********************************************************************
  745 *                                                                      *
  746 *                      Quantified predicates
  747 *                                                                      *
  748 ********************************************************************* -}
  749 
  750 {- Note [Quantified constraints]
  751 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  752 The -XQuantifiedConstraints extension allows type-class contexts like this:
  753 
  754   data Rose f x = Rose x (f (Rose f x))
  755 
  756   instance (Eq a, forall b. Eq b => Eq (f b))
  757         => Eq (Rose f a)  where
  758     (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 == rs2
  759 
  760 Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
  761 This quantified constraint is needed to solve the
  762  [W] (Eq (f (Rose f x)))
  763 constraint which arises form the (==) definition.
  764 
  765 The wiki page is
  766   https://gitlab.haskell.org/ghc/ghc/wikis/quantified-constraints
  767 which in turn contains a link to the GHC Proposal where the change
  768 is specified, and a Haskell Symposium paper about it.
  769 
  770 We implement two main extensions to the design in the paper:
  771 
  772  1. We allow a variable in the instance head, e.g.
  773       f :: forall m a. (forall b. m b) => D (m a)
  774     Notice the 'm' in the head of the quantified constraint, not
  775     a class.
  776 
  777  2. We support superclasses to quantified constraints.
  778     For example (contrived):
  779       f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool
  780       f x y = x==y
  781     Here we need (Eq (m a)); but the quantified constraint deals only
  782     with Ord.  But we can make it work by using its superclass.
  783 
  784 Here are the moving parts
  785   * Language extension {-# LANGUAGE QuantifiedConstraints #-}
  786     and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
  787 
  788   * A new form of evidence, EvDFun, that is used to discharge
  789     such wanted constraints
  790 
  791   * checkValidType gets some changes to accept forall-constraints
  792     only in the right places.
  793 
  794   * Predicate.Pred gets a new constructor ForAllPred, and
  795     and classifyPredType analyses a PredType to decompose
  796     the new forall-constraints
  797 
  798   * GHC.Tc.Solver.Monad.InertCans gets an extra field, inert_insts,
  799     which holds all the Given forall-constraints.  In effect,
  800     such Given constraints are like local instance decls.
  801 
  802   * When trying to solve a class constraint, via
  803     GHC.Tc.Solver.Interact.matchInstEnv, use the InstEnv from inert_insts
  804     so that we include the local Given forall-constraints
  805     in the lookup.  (See GHC.Tc.Solver.Monad.getInstEnvs.)
  806 
  807   * GHC.Tc.Solver.Canonical.canForAll deals with solving a
  808     forall-constraint.  See
  809        Note [Solving a Wanted forall-constraint]
  810 
  811   * We augment the kick-out code to kick out an inert
  812     forall constraint if it can be rewritten by a new
  813     type equality; see GHC.Tc.Solver.Monad.kick_out_rewritable
  814 
  815 Note that a quantified constraint is never /inferred/
  816 (by GHC.Tc.Solver.simplifyInfer).  A function can only have a
  817 quantified constraint in its type if it is given an explicit
  818 type signature.
  819 
  820 -}
  821 
  822 canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
  823             -> TcS (StopOrContinue Ct)
  824 canForAllNC ev tvs theta pred
  825   | isGiven ev  -- See Note [Eagerly expand given superclasses]
  826   , Just (cls, tys) <- cls_pred_tys_maybe
  827   = do { sc_cts <- mkStrictSuperClasses ev tvs theta cls tys
  828        ; emitWork sc_cts
  829        ; canForAll ev False }
  830 
  831   | otherwise
  832   = canForAll ev (isJust cls_pred_tys_maybe)
  833 
  834   where
  835     cls_pred_tys_maybe = getClassPredTys_maybe pred
  836 
  837 canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
  838 -- We have a constraint (forall as. blah => C tys)
  839 canForAll ev pend_sc
  840   = do { -- First rewrite it to apply the current substitution
  841          let pred = ctEvPred ev
  842        ; redn <- rewrite ev pred
  843        ; rewriteEvidence ev redn `andWhenContinue` \ new_ev ->
  844 
  845     do { -- Now decompose into its pieces and solve it
  846          -- (It takes a lot less code to rewrite before decomposing.)
  847        ; case classifyPredType (ctEvPred new_ev) of
  848            ForAllPred tvs theta pred
  849               -> solveForAll new_ev tvs theta pred pend_sc
  850            _  -> pprPanic "canForAll" (ppr new_ev)
  851     } }
  852 
  853 solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool
  854             -> TcS (StopOrContinue Ct)
  855 solveForAll ev tvs theta pred pend_sc
  856   | CtWanted { ctev_dest = dest } <- ev
  857   = -- See Note [Solving a Wanted forall-constraint]
  858     do { let skol_info = QuantCtxtSkol
  859              empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
  860                            tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
  861        ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs
  862        ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
  863 
  864        ; (lvl, (w_id, wanteds))
  865              <- pushLevelNoWorkList (ppr skol_info) $
  866                 do { wanted_ev <- newWantedEvVarNC loc $
  867                                   substTy subst pred
  868                    ; return ( ctEvEvId wanted_ev
  869                             , unitBag (mkNonCanonical wanted_ev)) }
  870 
  871       ; ev_binds <- emitImplicationTcS lvl skol_info skol_tvs
  872                                        given_ev_vars wanteds
  873 
  874       ; setWantedEvTerm dest $
  875         EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
  876               , et_binds = ev_binds, et_body = w_id }
  877 
  878       ; stopWith ev "Wanted forall-constraint" }
  879 
  880   | isGiven ev   -- See Note [Solving a Given forall-constraint]
  881   = do { addInertForAll qci
  882        ; stopWith ev "Given forall-constraint" }
  883 
  884   | otherwise
  885   = do { traceTcS "discarding derived forall-constraint" (ppr ev)
  886        ; stopWith ev "Derived forall-constraint" }
  887   where
  888     loc = ctEvLoc ev
  889     qci = QCI { qci_ev = ev, qci_tvs = tvs
  890               , qci_pred = pred, qci_pend_sc = pend_sc }
  891 
  892 {- Note [Solving a Wanted forall-constraint]
  893 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  894 Solving a wanted forall (quantified) constraint
  895   [W] df :: forall ab. (Eq a, Ord b) => C x a b
  896 is delightfully easy.   Just build an implication constraint
  897     forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a
  898 and discharge df thus:
  899     df = /\ab. \g1 g2. let <binds> in d
  900 where <binds> is filled in by solving the implication constraint.
  901 All the machinery is to hand; there is little to do.
  902 
  903 Note [Solving a Given forall-constraint]
  904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  905 For a Given constraint
  906   [G] df :: forall ab. (Eq a, Ord b) => C x a b
  907 we just add it to TcS's local InstEnv of known instances,
  908 via addInertForall.  Then, if we look up (C x Int Bool), say,
  909 we'll find a match in the InstEnv.
  910 
  911 
  912 ************************************************************************
  913 *                                                                      *
  914 *                       Special predicates
  915 *                                                                      *
  916 ********************************************************************* -}
  917 
  918 -- | Canonicalise a 'SpecialPred' constraint.
  919 canSpecial :: CtEvidence -> SpecialPred -> TcType -> TcS (StopOrContinue Ct)
  920 canSpecial ev special_pred ty
  921   = do { -- Special constraints should never appear in Givens.
  922        ; massertPpr (not $ isGivenOrigin $ ctEvOrigin ev)
  923            (text "canSpecial: Given Special constraint" $$ ppr ev)
  924        ; case special_pred of
  925          { ConcretePrimPred -> canConcretePrim ev ty } }
  926 
  927 {- Note [Canonical Concrete# constraints]
  928 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  929 A 'Concrete#' constraint can be decomposed precisely when
  930 it is an application, possibly nullary, of a concrete 'TyCon'.
  931 
  932 A canonical 'Concrete#' constraint is one that cannot be decomposed.
  933 
  934 To illustrate, when we come across a constraint of the form `Concrete# (f a_1 ... a_n)`,
  935 to canonicalise it, we decompose it into the collection of constraints
  936 `Concrete# a_1`, ..., `Concrete# a_n`, whenever `f` is a concrete type constructor
  937 (that is, it is not a type variable, nor a type-family, nor an abstract 'TyCon'
  938 as declared in a Backpack signature file).
  939 
  940 Writing NC for a non-canonical constraint and C for a canonical one,
  941 here are some examples:
  942 
  943   (1)
  944     NC: Concrete# IntRep
  945       ==> nullary decomposition, by observing that `IntRep = TyConApp intRepTyCon []`
  946 
  947   (2)
  948     NC: Concrete# (TYPE (TupleRep '[Rep, rr])) -- where 'Rep' is an abstract type and 'rr' is a type variable
  949       ==> decompose once, noting that 'TYPE' is a concrete 'TyCon'
  950         NC: Concrete# (TupleRep '[Rep, rr])
  951       ==> decompose again in the same way but with 'TupleRep'
  952         NC: Concrete# ((:) @RuntimeRep Rep ((:) @RuntimeRep rr []))
  953       ==> handle (:) and its type-level argument 'RuntimeRep' (which is concrete)
  954         C: Concrete# Rep, NC: Concrete# ((:) @RuntimeRep rr []))
  955       ==> the second constraint can be decomposed again; 'RuntimeRep' and '[]' are concrete, so we get
  956         C: Concrete# Rep, C: Concrete# rr
  957 
  958 -}
  959 
  960 -- | Canonicalise a 'Concrete#' constraint.
  961 --
  962 -- See Note [Canonical Concrete# constraints] for details.
  963 canConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct)
  964 canConcretePrim ev ty
  965   = do {
  966        -- As per Note [The Concrete mechanism] in GHC.Tc.Instance.Class,
  967        -- in PHASE 1, we don't allow a 'Concrete#' constraint to be rewritten.
  968        -- We still need to zonk, otherwise we can end up stuck with a constraint
  969        -- such as `Concrete# rep` for a unification variable `rep`,
  970        -- which we can't make progress on.
  971        ; ty <- zonkTcType ty
  972        ; traceTcS "canConcretePrim" $
  973            vcat [text "ev =" <+> ppr ev, text "ty =" <+> ppr ty]
  974 
  975        ; decomposeConcretePrim ev ty }
  976 
  977 -- | Try to decompose a 'Concrete#' constraint:
  978 --
  979 --  - calls 'canDecomposableConcretePrim' if the constraint can be decomposed;
  980 --  - calls 'canNonDecomposableConcretePrim' otherwise.
  981 decomposeConcretePrim :: CtEvidence -> Type -> TcS (StopOrContinue Ct)
  982 decomposeConcretePrim ev ty
  983   -- Handle applications of concrete 'TyCon's.
  984   -- See examples (1,2) in Note [Canonical Concrete# constraints].
  985   | (f,args) <- tcSplitAppTys ty
  986   , Just f_tc <- tyConAppTyCon_maybe f
  987   , isConcreteTyCon f_tc
  988   = canDecomposableConcretePrim ev f_tc args
  989 
  990   -- Couldn't decompose the constraint: keep it as-is.
  991   | otherwise
  992   = canNonDecomposableConcretePrim ev ty
  993 
  994 -- | Decompose a constraint of the form @'Concrete#' (f t_1 ... t_n)@,
  995 -- for a concrete `TyCon' `f`.
  996 --
  997 -- This function will emit new Wanted @Concrete# t_i@ constraints, one for
  998 -- each of the arguments of `f`.
  999 --
 1000 -- See Note [Canonical Concrete# constraints].
 1001 canDecomposableConcretePrim :: CtEvidence
 1002                             -> TyCon
 1003                             -> [TcType]
 1004                             -> TcS (StopOrContinue Ct)
 1005 canDecomposableConcretePrim ev f_tc args
 1006   = do { traceTcS "canDecomposableConcretePrim" $
 1007            vcat [text "args =" <+> ppr args, text "ev =" <+> ppr ev]
 1008        ; arg_cos <- mapM (emit_new_concretePrim_wanted (ctEvLoc ev)) args
 1009        ; case ev of
 1010           CtWanted { ctev_dest = dest }
 1011             -> setWantedEvTerm dest (evCoercion $ mkTyConAppCo Nominal f_tc arg_cos)
 1012           _ -> pprPanic "canDecomposableConcretePrim: non-Wanted" $
 1013                   vcat [ text "ev =" <+> ppr ev
 1014                        , text "args =" <+> ppr args ]
 1015        ; stopWith ev "Decomposed Concrete#" }
 1016 
 1017 -- | Canonicalise a non-decomposable 'Concrete#' constraint.
 1018 canNonDecomposableConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct)
 1019 canNonDecomposableConcretePrim ev ty
 1020   = do { -- Update the evidence to account for the zonk to `ty`.
 1021          let ki = typeKind ty
 1022              new_ev = ev { ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] }
 1023              new_ct =
 1024                CSpecialCan { cc_ev = new_ev
 1025                            , cc_special_pred = ConcretePrimPred
 1026                            , cc_xi = ty }
 1027        ; traceTcS "canNonDecomposableConcretePrim" $
 1028            vcat [ text "ty =" <+> ppr ty, text "new_ev =" <+> ppr new_ev ]
 1029        ; continueWith new_ct }
 1030 
 1031 -- | Create a new 'Concrete#' Wanted constraint and immediately add it
 1032 -- to the work list.
 1033 emit_new_concretePrim_wanted :: CtLoc -> Type -> TcS Coercion
 1034 emit_new_concretePrim_wanted loc ty
 1035   = do { (hole, wanted) <- wrapTcS $ newConcretePrimWanted loc ty
 1036        ; emitWorkNC [wanted]
 1037        ; return $ mkHoleCo hole }
 1038 
 1039 {- **********************************************************************
 1040 *                                                                      *
 1041 *        Equalities
 1042 *                                                                      *
 1043 ************************************************************************
 1044 
 1045 Note [Canonicalising equalities]
 1046 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1047 In order to canonicalise an equality, we look at the structure of the
 1048 two types at hand, looking for similarities. A difficulty is that the
 1049 types may look dissimilar before rewriting but similar after rewriting.
 1050 However, we don't just want to jump in and rewrite right away, because
 1051 this might be wasted effort. So, after looking for similarities and failing,
 1052 we rewrite and then try again. Of course, we don't want to loop, so we
 1053 track whether or not we've already rewritten.
 1054 
 1055 It is conceivable to do a better job at tracking whether or not a type
 1056 is rewritten, but this is left as future work. (Mar '15)
 1057 
 1058 Note [Decomposing FunTy]
 1059 ~~~~~~~~~~~~~~~~~~~~~~~~
 1060 can_eq_nc' may attempt to decompose a FunTy that is un-zonked.  This
 1061 means that we may very well have a FunTy containing a type of some
 1062 unknown kind. For instance, we may have,
 1063 
 1064     FunTy (a :: k) Int
 1065 
 1066 Where k is a unification variable. So the calls to getRuntimeRep_maybe may
 1067 fail (returning Nothing).  In that case we'll fall through, zonk, and try again.
 1068 Zonking should fill the variable k, meaning that decomposition will succeed the
 1069 second time around.
 1070 
 1071 Also note that we require the AnonArgFlag to match.  This will stop
 1072 us decomposing
 1073    (Int -> Bool)  ~  (Show a => blah)
 1074 It's as if we treat (->) and (=>) as different type constructors.
 1075 -}
 1076 
 1077 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
 1078 canEqNC ev eq_rel ty1 ty2
 1079   = do { result <- zonk_eq_types ty1 ty2
 1080        ; case result of
 1081            Left (Pair ty1' ty2') -> can_eq_nc False ev eq_rel ty1' ty1 ty2' ty2
 1082            Right ty              -> canEqReflexive ev eq_rel ty }
 1083 
 1084 can_eq_nc
 1085    :: Bool            -- True => both types are rewritten
 1086    -> CtEvidence
 1087    -> EqRel
 1088    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp
 1089    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp
 1090    -> TcS (StopOrContinue Ct)
 1091 can_eq_nc rewritten ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 1092   = do { traceTcS "can_eq_nc" $
 1093          vcat [ ppr rewritten, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
 1094        ; rdr_env <- getGlobalRdrEnvTcS
 1095        ; fam_insts <- getFamInstEnvs
 1096        ; can_eq_nc' rewritten rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
 1097 
 1098 can_eq_nc'
 1099    :: Bool           -- True => both input types are rewritten
 1100    -> GlobalRdrEnv   -- needed to see which newtypes are in scope
 1101    -> FamInstEnvs    -- needed to unwrap data instances
 1102    -> CtEvidence
 1103    -> EqRel
 1104    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp
 1105    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp
 1106    -> TcS (StopOrContinue Ct)
 1107 
 1108 -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
 1109 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
 1110   | tc1 == tc2
 1111   = canEqReflexive ev eq_rel ty1
 1112 
 1113 -- Expand synonyms first; see Note [Type synonyms and canonicalization]
 1114 can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 1115   | Just ty1' <- tcView ty1 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2  ps_ty2
 1116   | Just ty2' <- tcView ty2 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1  ps_ty1 ty2' ps_ty2
 1117 
 1118 -- need to check for reflexivity in the ReprEq case.
 1119 -- See Note [Eager reflexivity check]
 1120 -- Check only when rewritten because the zonk_eq_types check in canEqNC takes
 1121 -- care of the non-rewritten case.
 1122 can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
 1123   | ty1 `tcEqType` ty2
 1124   = canEqReflexive ev ReprEq ty1
 1125 
 1126 -- When working with ReprEq, unwrap newtypes.
 1127 -- See Note [Unwrap newtypes first]
 1128 -- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
 1129 can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 1130   | ReprEq <- eq_rel
 1131   , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
 1132   = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
 1133 
 1134   | ReprEq <- eq_rel
 1135   , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
 1136   = can_eq_newtype_nc ev IsSwapped  ty2 stuff2 ty1 ps_ty1
 1137 
 1138 -- Then, get rid of casts
 1139 can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
 1140   | isNothing (canEqLHS_maybe ty2)  -- See (3) in Note [Equalities with incompatible kinds]
 1141   = canEqCast rewritten ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
 1142 can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
 1143   | isNothing (canEqLHS_maybe ty1)  -- See (3) in Note [Equalities with incompatible kinds]
 1144   = canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
 1145 
 1146 ----------------------
 1147 -- Otherwise try to decompose
 1148 ----------------------
 1149 
 1150 -- Literals
 1151 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
 1152  | l1 == l2
 1153   = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
 1154        ; stopWith ev "Equal LitTy" }
 1155 
 1156 -- Decompose FunTy: (s -> t) and (c => t)
 1157 -- NB: don't decompose (Int -> blah) ~ (Show a => blah)
 1158 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
 1159            (FunTy { ft_mult = am1, ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ps_ty1
 1160            (FunTy { ft_mult = am2, ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ps_ty2
 1161   | af1 == af2   -- Don't decompose (Int -> blah) ~ (Show a => blah)
 1162   , Just ty1a_rep <- getRuntimeRep_maybe ty1a  -- getRutimeRep_maybe:
 1163   , Just ty1b_rep <- getRuntimeRep_maybe ty1b  -- see Note [Decomposing FunTy]
 1164   , Just ty2a_rep <- getRuntimeRep_maybe ty2a
 1165   , Just ty2b_rep <- getRuntimeRep_maybe ty2b
 1166   = canDecomposableTyConAppOK ev eq_rel funTyCon
 1167                               [am1, ty1a_rep, ty1b_rep, ty1a, ty1b]
 1168                               [am2, ty2a_rep, ty2b_rep, ty2a, ty2b]
 1169 
 1170 -- Decompose type constructor applications
 1171 -- NB: we have expanded type synonyms already
 1172 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
 1173   | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
 1174   , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
 1175    -- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
 1176    -- error messages rather than decomposing into AppTys;
 1177    -- hence no direct match on TyConApp
 1178   , not (isTypeFamilyTyCon tc1)
 1179   , not (isTypeFamilyTyCon tc2)
 1180   = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
 1181 
 1182 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
 1183            s1@(ForAllTy (Bndr _ vis1) _) _
 1184            s2@(ForAllTy (Bndr _ vis2) _) _
 1185   | vis1 `sameVis` vis2 -- Note [ForAllTy and typechecker equality]
 1186   = can_eq_nc_forall ev eq_rel s1 s2
 1187 
 1188 -- See Note [Canonicalising type applications] about why we require rewritten types
 1189 -- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
 1190 -- NB: Only decompose AppTy for nominal equality. See Note [Decomposing equality]
 1191 can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
 1192   | Just (t1, s1) <- tcSplitAppTy_maybe ty1
 1193   , Just (t2, s2) <- tcSplitAppTy_maybe ty2
 1194   = can_eq_app ev t1 s1 t2 s2
 1195 
 1196 -------------------
 1197 -- Can't decompose.
 1198 -------------------
 1199 
 1200 -- No similarity in type structure detected. Rewrite and try again.
 1201 can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
 1202   = do { redn1@(Reduction _ xi1) <- rewrite ev ps_ty1
 1203        ; redn2@(Reduction _ xi2) <- rewrite ev ps_ty2
 1204        ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
 1205        ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
 1206 
 1207 ----------------------------
 1208 -- Look for a canonical LHS. See Note [Canonical LHS].
 1209 -- Only rewritten types end up below here.
 1210 ----------------------------
 1211 
 1212 -- NB: pattern match on True: we want only rewritten types sent to canEqLHS
 1213 -- This means we've rewritten any variables and reduced any type family redexes
 1214 -- See also Note [No top-level newtypes on RHS of representational equalities]
 1215 can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 1216   | Just can_eq_lhs1 <- canEqLHS_maybe ty1
 1217   = canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2
 1218 
 1219   | Just can_eq_lhs2 <- canEqLHS_maybe ty2
 1220   = canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1
 1221 
 1222      -- If the type is TyConApp tc1 args1, then args1 really can't be less
 1223      -- than tyConArity tc1. It could be *more* than tyConArity, but then we
 1224      -- should have handled the case as an AppTy. That case only fires if
 1225      -- _both_ sides of the equality are AppTy-like... but if one side is
 1226      -- AppTy-like and the other isn't (and it also isn't a variable or
 1227      -- saturated type family application, both of which are handled by
 1228      -- can_eq_nc'), we're in a failure mode and can just fall through.
 1229 
 1230 ----------------------------
 1231 -- Fall-through. Give up.
 1232 ----------------------------
 1233 
 1234 -- We've rewritten and the types don't match. Give up.
 1235 can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
 1236   = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
 1237        ; case eq_rel of -- See Note [Unsolved equalities]
 1238             ReprEq -> continueWith (mkIrredCt ReprEqReason ev)
 1239             NomEq  -> continueWith (mkIrredCt ShapeMismatchReason ev) }
 1240           -- No need to call canEqFailure/canEqHardFailure because they
 1241           -- rewrite, and the types involved here are already rewritten
 1242 
 1243 {- Note [Unsolved equalities]
 1244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1245 If we have an unsolved equality like
 1246   (a b ~R# Int)
 1247 that is not necessarily insoluble!  Maybe 'a' will turn out to be a newtype.
 1248 So we want to make it a potentially-soluble Irred not an insoluble one.
 1249 Missing this point is what caused #15431
 1250 
 1251 Note [ForAllTy and typechecker equality]
 1252 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1253 Should GHC type-check the following program (adapted from #15740)?
 1254 
 1255   {-# LANGUAGE PolyKinds, ... #-}
 1256   data D a
 1257   type family F :: forall k. k -> Type
 1258   type instance F = D
 1259 
 1260 Due to the way F is declared, any instance of F must have a right-hand side
 1261 whose kind is equal to `forall k. k -> Type`. The kind of D is
 1262 `forall {k}. k -> Type`, which is very close, but technically uses distinct
 1263 Core:
 1264 
 1265   -----------------------------------------------------------
 1266   | Source Haskell    | Core                                |
 1267   -----------------------------------------------------------
 1268   | forall  k.  <...> | ForAllTy (Bndr k Specified) (<...>) |
 1269   | forall {k}. <...> | ForAllTy (Bndr k Inferred)  (<...>) |
 1270   -----------------------------------------------------------
 1271 
 1272 We could deem these kinds to be unequal, but that would imply rejecting
 1273 programs like the one above. Whether a kind variable binder ends up being
 1274 specified or inferred can be somewhat subtle, however, especially for kinds
 1275 that aren't explicitly written out in the source code (like in D above).
 1276 For now, we decide to not make the specified/inferred status of an invisible
 1277 type variable binder affect GHC's notion of typechecker equality
 1278 (see Note [Typechecker equality vs definitional equality] in
 1279 GHC.Tc.Utils.TcType). That is, we have the following:
 1280 
 1281   --------------------------------------------------
 1282   | Type 1            | Type 2            | Equal? |
 1283   --------------------|-----------------------------
 1284   | forall k. <...>   | forall k. <...>   | Yes    |
 1285   |                   | forall {k}. <...> | Yes    |
 1286   |                   | forall k -> <...> | No     |
 1287   --------------------------------------------------
 1288   | forall {k}. <...> | forall k. <...>   | Yes    |
 1289   |                   | forall {k}. <...> | Yes    |
 1290   |                   | forall k -> <...> | No     |
 1291   --------------------------------------------------
 1292   | forall k -> <...> | forall k. <...>   | No     |
 1293   |                   | forall {k}. <...> | No     |
 1294   |                   | forall k -> <...> | Yes    |
 1295   --------------------------------------------------
 1296 
 1297 We implement this nuance by using the GHC.Types.Var.sameVis function in
 1298 GHC.Tc.Solver.Canonical.canEqNC and GHC.Tc.Utils.TcType.tcEqType, which
 1299 respect typechecker equality. sameVis puts both forms of invisible type
 1300 variable binders into the same equivalence class.
 1301 
 1302 Note that we do /not/ use sameVis in GHC.Core.Type.eqType, which implements
 1303 /definitional/ equality, a slighty more coarse-grained notion of equality
 1304 (see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep) that does
 1305 not consider the ArgFlag of ForAllTys at all. That is, eqType would equate all
 1306 of forall k. <...>, forall {k}. <...>, and forall k -> <...>.
 1307 -}
 1308 
 1309 ---------------------------------
 1310 can_eq_nc_forall :: CtEvidence -> EqRel
 1311                  -> Type -> Type    -- LHS and RHS
 1312                  -> TcS (StopOrContinue Ct)
 1313 -- (forall as. phi1) ~ (forall bs. phi2)
 1314 -- Check for length match of as, bs
 1315 -- Then build an implication constraint: forall as. phi1 ~ phi2[as/bs]
 1316 -- But remember also to unify the kinds of as and bs
 1317 --  (this is the 'go' loop), and actually substitute phi2[as |> cos / bs]
 1318 -- Remember also that we might have forall z (a:z). blah
 1319 --  so we must proceed one binder at a time (#13879)
 1320 
 1321 can_eq_nc_forall ev eq_rel s1 s2
 1322  | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
 1323  = do { let free_tvs       = tyCoVarsOfTypes [s1,s2]
 1324             (bndrs1, phi1) = tcSplitForAllTyVarBinders s1
 1325             (bndrs2, phi2) = tcSplitForAllTyVarBinders s2
 1326       ; if not (equalLength bndrs1 bndrs2)
 1327         then do { traceTcS "Forall failure" $
 1328                      vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
 1329                           , ppr (map binderArgFlag bndrs1)
 1330                           , ppr (map binderArgFlag bndrs2) ]
 1331                 ; canEqHardFailure ev s1 s2 }
 1332         else
 1333    do { traceTcS "Creating implication for polytype equality" $ ppr ev
 1334       ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs
 1335       ; (subst1, skol_tvs) <- tcInstSkolTyVarsX empty_subst1 $
 1336                               binderVars bndrs1
 1337 
 1338       ; let skol_info = UnifyForAllSkol phi1
 1339             phi1' = substTy subst1 phi1
 1340 
 1341             -- Unify the kinds, extend the substitution
 1342             go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
 1343                -> TcS (TcCoercion, Cts)
 1344             go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
 1345               = do { let tv2 = binderVar bndr2
 1346                    ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv)
 1347                                                   (substTy subst (tyVarKind tv2))
 1348                    ; let subst' = extendTvSubstAndInScope subst tv2
 1349                                        (mkCastTy (mkTyVarTy skol_tv) kind_co)
 1350                          -- skol_tv is already in the in-scope set, but the
 1351                          -- free vars of kind_co are not; hence "...AndInScope"
 1352                    ; (co, wanteds2) <- go skol_tvs subst' bndrs2
 1353                    ; return ( mkTcForAllCo skol_tv kind_co co
 1354                             , wanteds1 `unionBags` wanteds2 ) }
 1355 
 1356             -- Done: unify phi1 ~ phi2
 1357             go [] subst bndrs2
 1358               = assert (null bndrs2 )
 1359                 unify loc (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2)
 1360 
 1361             go _ _ _ = panic "cna_eq_nc_forall"  -- case (s:ss) []
 1362 
 1363             empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
 1364 
 1365       ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
 1366                                     go skol_tvs empty_subst2 bndrs2
 1367       ; emitTvImplicationTcS lvl skol_info skol_tvs wanteds
 1368 
 1369       ; setWantedEq orig_dest all_co
 1370       ; stopWith ev "Deferred polytype equality" } }
 1371 
 1372  | otherwise
 1373  = do { traceTcS "Omitting decomposition of given polytype equality" $
 1374         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
 1375       ; stopWith ev "Discard given polytype equality" }
 1376 
 1377  where
 1378     unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
 1379     -- This version returns the wanted constraint rather
 1380     -- than putting it in the work list
 1381     unify loc role ty1 ty2
 1382       | ty1 `tcEqType` ty2
 1383       = return (mkTcReflCo role ty1, emptyBag)
 1384       | otherwise
 1385       = do { (wanted, co) <- newWantedEq loc role ty1 ty2
 1386            ; return (co, unitBag (mkNonCanonical wanted)) }
 1387 
 1388 ---------------------------------
 1389 -- | Compare types for equality, while zonking as necessary. Gives up
 1390 -- as soon as it finds that two types are not equal.
 1391 -- This is quite handy when some unification has made two
 1392 -- types in an inert Wanted to be equal. We can discover the equality without
 1393 -- rewriting, which is sometimes very expensive (in the case of type functions).
 1394 -- In particular, this function makes a ~20% improvement in test case
 1395 -- perf/compiler/T5030.
 1396 --
 1397 -- Returns either the (partially zonked) types in the case of
 1398 -- inequality, or the one type in the case of equality. canEqReflexive is
 1399 -- a good next step in the 'Right' case. Returning 'Left' is always safe.
 1400 --
 1401 -- NB: This does *not* look through type synonyms. In fact, it treats type
 1402 -- synonyms as rigid constructors. In the future, it might be convenient
 1403 -- to look at only those arguments of type synonyms that actually appear
 1404 -- in the synonym RHS. But we're not there yet.
 1405 zonk_eq_types :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
 1406 zonk_eq_types = go
 1407   where
 1408     go (TyVarTy tv1) (TyVarTy tv2) = tyvar_tyvar tv1 tv2
 1409     go (TyVarTy tv1) ty2           = tyvar NotSwapped tv1 ty2
 1410     go ty1 (TyVarTy tv2)           = tyvar IsSwapped  tv2 ty1
 1411 
 1412     -- We handle FunTys explicitly here despite the fact that they could also be
 1413     -- treated as an application. Why? Well, for one it's cheaper to just look
 1414     -- at two types (the argument and result types) than four (the argument,
 1415     -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
 1416     -- so we may run into an unzonked type variable while trying to compute the
 1417     -- RuntimeReps of the argument and result types. This can be observed in
 1418     -- testcase tc269.
 1419     go ty1 ty2
 1420       | Just (Scaled w1 arg1, res1) <- split1
 1421       , Just (Scaled w2 arg2, res2) <- split2
 1422       , eqType w1 w2
 1423       = do { res_a <- go arg1 arg2
 1424            ; res_b <- go res1 res2
 1425            ; return $ combine_rev (mkVisFunTy w1) res_b res_a
 1426            }
 1427       | isJust split1 || isJust split2
 1428       = bale_out ty1 ty2
 1429       where
 1430         split1 = tcSplitFunTy_maybe ty1
 1431         split2 = tcSplitFunTy_maybe ty2
 1432 
 1433     go ty1 ty2
 1434       | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
 1435       , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
 1436       = if tc1 == tc2 && tys1 `equalLength` tys2
 1437           -- Crucial to check for equal-length args, because
 1438           -- we cannot assume that the two args to 'go' have
 1439           -- the same kind.  E.g go (Proxy *      (Maybe Int))
 1440           --                        (Proxy (*->*) Maybe)
 1441           -- We'll call (go (Maybe Int) Maybe)
 1442           -- See #13083
 1443         then tycon tc1 tys1 tys2
 1444         else bale_out ty1 ty2
 1445 
 1446     go ty1 ty2
 1447       | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
 1448       , Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
 1449       = do { res_a <- go ty1a ty2a
 1450            ; res_b <- go ty1b ty2b
 1451            ; return $ combine_rev mkAppTy res_b res_a }
 1452 
 1453     go ty1@(LitTy lit1) (LitTy lit2)
 1454       | lit1 == lit2
 1455       = return (Right ty1)
 1456 
 1457     go ty1 ty2 = bale_out ty1 ty2
 1458       -- We don't handle more complex forms here
 1459 
 1460     bale_out ty1 ty2 = return $ Left (Pair ty1 ty2)
 1461 
 1462     tyvar :: SwapFlag -> TcTyVar -> TcType
 1463           -> TcS (Either (Pair TcType) TcType)
 1464       -- Try to do as little as possible, as anything we do here is redundant
 1465       -- with rewriting. In particular, no need to zonk kinds. That's why
 1466       -- we don't use the already-defined zonking functions
 1467     tyvar swapped tv ty
 1468       = case tcTyVarDetails tv of
 1469           MetaTv { mtv_ref = ref }
 1470             -> do { cts <- readTcRef ref
 1471                   ; case cts of
 1472                       Flexi        -> give_up
 1473                       Indirect ty' -> do { trace_indirect tv ty'
 1474                                          ; unSwap swapped go ty' ty } }
 1475           _ -> give_up
 1476       where
 1477         give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
 1478 
 1479     tyvar_tyvar tv1 tv2
 1480       | tv1 == tv2 = return (Right (mkTyVarTy tv1))
 1481       | otherwise  = do { (ty1', progress1) <- quick_zonk tv1
 1482                         ; (ty2', progress2) <- quick_zonk tv2
 1483                         ; if progress1 || progress2
 1484                           then go ty1' ty2'
 1485                           else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
 1486 
 1487     trace_indirect tv ty
 1488        = traceTcS "Following filled tyvar (zonk_eq_types)"
 1489                   (ppr tv <+> equals <+> ppr ty)
 1490 
 1491     quick_zonk tv = case tcTyVarDetails tv of
 1492       MetaTv { mtv_ref = ref }
 1493         -> do { cts <- readTcRef ref
 1494               ; case cts of
 1495                   Flexi        -> return (TyVarTy tv, False)
 1496                   Indirect ty' -> do { trace_indirect tv ty'
 1497                                      ; return (ty', True) } }
 1498       _ -> return (TyVarTy tv, False)
 1499 
 1500       -- This happens for type families, too. But recall that failure
 1501       -- here just means to try harder, so it's OK if the type function
 1502       -- isn't injective.
 1503     tycon :: TyCon -> [TcType] -> [TcType]
 1504           -> TcS (Either (Pair TcType) TcType)
 1505     tycon tc tys1 tys2
 1506       = do { results <- zipWithM go tys1 tys2
 1507            ; return $ case combine_results results of
 1508                Left tys  -> Left (mkTyConApp tc <$> tys)
 1509                Right tys -> Right (mkTyConApp tc tys) }
 1510 
 1511     combine_results :: [Either (Pair TcType) TcType]
 1512                     -> Either (Pair [TcType]) [TcType]
 1513     combine_results = bimap (fmap reverse) reverse .
 1514                       foldl' (combine_rev (:)) (Right [])
 1515 
 1516       -- combine (in reverse) a new result onto an already-combined result
 1517     combine_rev :: (a -> b -> c)
 1518                 -> Either (Pair b) b
 1519                 -> Either (Pair a) a
 1520                 -> Either (Pair c) c
 1521     combine_rev f (Left list) (Left elt) = Left (f <$> elt     <*> list)
 1522     combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
 1523     combine_rev f (Right tys) (Left elt) = Left (f <$> elt     <*> pure tys)
 1524     combine_rev f (Right tys) (Right ty) = Right (f ty tys)
 1525 
 1526 {- See Note [Unwrap newtypes first]
 1527 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1528 Consider
 1529   newtype N m a = MkN (m a)
 1530 Then N will get a conservative, Nominal role for its second parameter 'a',
 1531 because it appears as an argument to the unknown 'm'. Now consider
 1532   [W] N Maybe a  ~R#  N Maybe b
 1533 
 1534 If we decompose, we'll get
 1535   [W] a ~N# b
 1536 
 1537 But if instead we unwrap we'll get
 1538   [W] Maybe a ~R# Maybe b
 1539 which in turn gives us
 1540   [W] a ~R# b
 1541 which is easier to satisfy.
 1542 
 1543 Bottom line: unwrap newtypes before decomposing them!
 1544 c.f. #9123 comment:52,53 for a compelling example.
 1545 
 1546 Note [Newtypes can blow the stack]
 1547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1548 Suppose we have
 1549 
 1550   newtype X = MkX (Int -> X)
 1551   newtype Y = MkY (Int -> Y)
 1552 
 1553 and now wish to prove
 1554 
 1555   [W] X ~R Y
 1556 
 1557 This Wanted will loop, expanding out the newtypes ever deeper looking
 1558 for a solid match or a solid discrepancy. Indeed, there is something
 1559 appropriate to this looping, because X and Y *do* have the same representation,
 1560 in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
 1561 coercion will ever witness it. This loop won't actually cause GHC to hang,
 1562 though, because we check our depth when unwrapping newtypes.
 1563 
 1564 Note [Eager reflexivity check]
 1565 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1566 Suppose we have
 1567 
 1568   newtype X = MkX (Int -> X)
 1569 
 1570 and
 1571 
 1572   [W] X ~R X
 1573 
 1574 Naively, we would start unwrapping X and end up in a loop. Instead,
 1575 we do this eager reflexivity check. This is necessary only for representational
 1576 equality because the rewriter technology deals with the similar case
 1577 (recursive type families) for nominal equality.
 1578 
 1579 Note that this check does not catch all cases, but it will catch the cases
 1580 we're most worried about, types like X above that are actually inhabited.
 1581 
 1582 Here's another place where this reflexivity check is key:
 1583 Consider trying to prove (f a) ~R (f a). The AppTys in there can't
 1584 be decomposed, because representational equality isn't congruent with respect
 1585 to AppTy. So, when canonicalising the equality above, we get stuck and
 1586 would normally produce a CIrredCan. However, we really do want to
 1587 be able to solve (f a) ~R (f a). So, in the representational case only,
 1588 we do a reflexivity check.
 1589 
 1590 (This would be sound in the nominal case, but unnecessary, and I [Richard
 1591 E.] am worried that it would slow down the common case.)
 1592 -}
 1593 
 1594 ------------------------
 1595 -- | We're able to unwrap a newtype. Update the bits accordingly.
 1596 can_eq_newtype_nc :: CtEvidence           -- ^ :: ty1 ~ ty2
 1597                   -> SwapFlag
 1598                   -> TcType                                    -- ^ ty1
 1599                   -> ((Bag GlobalRdrElt, TcCoercion), TcType)  -- ^ :: ty1 ~ ty1'
 1600                   -> TcType               -- ^ ty2
 1601                   -> TcType               -- ^ ty2, with type synonyms
 1602                   -> TcS (StopOrContinue Ct)
 1603 can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
 1604   = do { traceTcS "can_eq_newtype_nc" $
 1605          vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]
 1606 
 1607          -- check for blowing our stack:
 1608          -- See Note [Newtypes can blow the stack]
 1609        ; checkReductionDepth (ctEvLoc ev) ty1
 1610 
 1611          -- Next, we record uses of newtype constructors, since coercing
 1612          -- through newtypes is tantamount to using their constructors.
 1613        ; addUsedGREs gre_list
 1614          -- If a newtype constructor was imported, don't warn about not
 1615          -- importing it...
 1616        ; traverse_ keepAlive $ map greMangledName gre_list
 1617          -- ...and similarly, if a newtype constructor was defined in the same
 1618          -- module, don't warn about it being unused.
 1619          -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.
 1620 
 1621        ; let redn1 = mkReduction co1 ty1'
 1622 
 1623        ; new_ev <- rewriteEqEvidence ev swapped
 1624                      redn1
 1625                      (mkReflRedn Representational ps_ty2)
 1626        ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
 1627   where
 1628     gre_list = bagToList gres
 1629 
 1630 ---------
 1631 -- ^ Decompose a type application.
 1632 -- All input types must be rewritten. See Note [Canonicalising type applications]
 1633 -- Nominal equality only!
 1634 can_eq_app :: CtEvidence       -- :: s1 t1 ~N s2 t2
 1635            -> Xi -> Xi         -- s1 t1
 1636            -> Xi -> Xi         -- s2 t2
 1637            -> TcS (StopOrContinue Ct)
 1638 
 1639 -- AppTys only decompose for nominal equality, so this case just leads
 1640 -- to an irreducible constraint; see typecheck/should_compile/T10494
 1641 -- See Note [Decomposing AppTy at representational role]
 1642 can_eq_app ev s1 t1 s2 t2
 1643   | CtDerived {} <- ev
 1644   = do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
 1645        ; stopWith ev "Decomposed [D] AppTy" }
 1646 
 1647   | CtWanted { ctev_dest = dest } <- ev
 1648   = do { co_s <- unifyWanted loc Nominal s1 s2
 1649        ; let arg_loc
 1650                | isNextArgVisible s1 = loc
 1651                | otherwise           = updateCtLocOrigin loc toInvisibleOrigin
 1652        ; co_t <- unifyWanted arg_loc Nominal t1 t2
 1653        ; let co = mkAppCo co_s co_t
 1654        ; setWantedEq dest co
 1655        ; stopWith ev "Decomposed [W] AppTy" }
 1656 
 1657     -- If there is a ForAll/(->) mismatch, the use of the Left coercion
 1658     -- below is ill-typed, potentially leading to a panic in splitTyConApp
 1659     -- Test case: typecheck/should_run/Typeable1
 1660     -- We could also include this mismatch check above (for W and D), but it's slow
 1661     -- and we'll get a better error message not doing it
 1662   | s1k `mismatches` s2k
 1663   = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
 1664 
 1665   | CtGiven { ctev_evar = evar } <- ev
 1666   = do { let co   = mkTcCoVarCo evar
 1667              co_s = mkTcLRCo CLeft  co
 1668              co_t = mkTcLRCo CRight co
 1669        ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
 1670                                      , evCoercion co_s )
 1671        ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
 1672                                      , evCoercion co_t )
 1673        ; emitWorkNC [evar_t]
 1674        ; canEqNC evar_s NomEq s1 s2 }
 1675 
 1676   where
 1677     loc = ctEvLoc ev
 1678 
 1679     s1k = tcTypeKind s1
 1680     s2k = tcTypeKind s2
 1681 
 1682     k1 `mismatches` k2
 1683       =  isForAllTy k1 && not (isForAllTy k2)
 1684       || not (isForAllTy k1) && isForAllTy k2
 1685 
 1686 -----------------------
 1687 -- | Break apart an equality over a casted type
 1688 -- looking like   (ty1 |> co1) ~ ty2   (modulo a swap-flag)
 1689 canEqCast :: Bool         -- are both types rewritten?
 1690           -> CtEvidence
 1691           -> EqRel
 1692           -> SwapFlag
 1693           -> TcType -> Coercion   -- LHS (res. RHS), ty1 |> co1
 1694           -> TcType -> TcType     -- RHS (res. LHS), ty2 both normal and pretty
 1695           -> TcS (StopOrContinue Ct)
 1696 canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
 1697   = do { traceTcS "Decomposing cast" (vcat [ ppr ev
 1698                                            , ppr ty1 <+> text "|>" <+> ppr co1
 1699                                            , ppr ps_ty2 ])
 1700        ; new_ev <- rewriteEqEvidence ev swapped
 1701                       (mkGReflLeftRedn role ty1 co1)
 1702                       (mkReflRedn role ps_ty2)
 1703        ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
 1704   where
 1705     role = eqRelRole eq_rel
 1706 
 1707 ------------------------
 1708 canTyConApp :: CtEvidence -> EqRel
 1709             -> TyCon -> [TcType]
 1710             -> TyCon -> [TcType]
 1711             -> TcS (StopOrContinue Ct)
 1712 -- See Note [Decomposing TyConApps]
 1713 -- Neither tc1 nor tc2 is a saturated funTyCon
 1714 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
 1715   | tc1 == tc2
 1716   , tys1 `equalLength` tys2
 1717   = do { inerts <- getTcSInerts
 1718        ; if can_decompose inerts
 1719          then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
 1720          else canEqFailure ev eq_rel ty1 ty2 }
 1721 
 1722   -- See Note [Skolem abstract data] in GHC.Core.Tycon
 1723   | tyConSkolem tc1 || tyConSkolem tc2
 1724   = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
 1725        ; continueWith (mkIrredCt AbstractTyConReason ev) }
 1726 
 1727   -- Fail straight away for better error messages
 1728   -- See Note [Use canEqFailure in canDecomposableTyConApp]
 1729   | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
 1730                              isGenerativeTyCon tc2 Representational)
 1731   = canEqFailure ev eq_rel ty1 ty2
 1732   | otherwise
 1733   = canEqHardFailure ev ty1 ty2
 1734   where
 1735     -- Reconstruct the types for error messages. This would do
 1736     -- the wrong thing (from a pretty printing point of view)
 1737     -- for functions, because we've lost the AnonArgFlag; but
 1738     -- in fact we never call canTyConApp on a saturated FunTyCon
 1739     ty1 = mkTyConApp tc1 tys1
 1740     ty2 = mkTyConApp tc2 tys2
 1741 
 1742     loc  = ctEvLoc ev
 1743     pred = ctEvPred ev
 1744 
 1745      -- See Note [Decomposing equality]
 1746     can_decompose inerts
 1747       =  isInjectiveTyCon tc1 (eqRelRole eq_rel)
 1748       || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
 1749 
 1750 {-
 1751 Note [Use canEqFailure in canDecomposableTyConApp]
 1752 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1753 We must use canEqFailure, not canEqHardFailure here, because there is
 1754 the possibility of success if working with a representational equality.
 1755 Here is one case:
 1756 
 1757   type family TF a where TF Char = Bool
 1758   data family DF a
 1759   newtype instance DF Bool = MkDF Int
 1760 
 1761 Suppose we are canonicalising (Int ~R DF (TF a)), where we don't yet
 1762 know `a`. This is *not* a hard failure, because we might soon learn
 1763 that `a` is, in fact, Char, and then the equality succeeds.
 1764 
 1765 Here is another case:
 1766 
 1767   [G] Age ~R Int
 1768 
 1769 where Age's constructor is not in scope. We don't want to report
 1770 an "inaccessible code" error in the context of this Given!
 1771 
 1772 For example, see typecheck/should_compile/T10493, repeated here:
 1773 
 1774   import Data.Ord (Down)  -- no constructor
 1775 
 1776   foo :: Coercible (Down Int) Int => Down Int -> Int
 1777   foo = coerce
 1778 
 1779 That should compile, but only because we use canEqFailure and not
 1780 canEqHardFailure.
 1781 
 1782 Note [Decomposing equality]
 1783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1784 If we have a constraint (of any flavour and role) that looks like
 1785 T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
 1786 of course, is "it depends". This Note spells it all out.
 1787 
 1788 In this Note, "decomposition" refers to taking the constraint
 1789   [fl] (T tys1 ~X T tys2)
 1790 (for some flavour fl and some role X) and replacing it with
 1791   [fls'] (tys1 ~Xs' tys2)
 1792 where that notation indicates a list of new constraints, where the
 1793 new constraints may have different flavours and different roles.
 1794 
 1795 The key property to consider is injectivity. When decomposing a Given, the
 1796 decomposition is sound if and only if T is injective in all of its type
 1797 arguments. When decomposing a Wanted, the decomposition is sound (assuming the
 1798 correct roles in the produced equality constraints), but it may be a guess --
 1799 that is, an unforced decision by the constraint solver. Decomposing Wanteds
 1800 over injective TyCons does not entail guessing. But sometimes we want to
 1801 decompose a Wanted even when the TyCon involved is not injective! (See below.)
 1802 
 1803 So, in broad strokes, we want this rule:
 1804 
 1805 (*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
 1806 at role X.
 1807 
 1808 Pursuing the details requires exploring three axes:
 1809 * Flavour: Given vs. Derived vs. Wanted
 1810 * Role: Nominal vs. Representational
 1811 * TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
 1812 
 1813 (A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case
 1814 in the same table.)
 1815 
 1816 Right away, we can say that Derived behaves just as Wanted for the purposes
 1817 of decomposition. The difference between Derived and Wanted is the handling of
 1818 evidence. Since decomposition in these cases isn't a matter of soundness but of
 1819 guessing, we want the same behaviour regardless of evidence.
 1820 
 1821 Here is a table (discussion following) detailing where decomposition of
 1822    (T s1 ... sn) ~r (T t1 .. tn)
 1823 is allowed.  The first four lines (Data types ... type family) refer
 1824 to TyConApps with various TyCons T; the last line is for AppTy, covering
 1825 both where there is a type variable at the head and the case for an over-
 1826 saturated type family.
 1827 
 1828 NOMINAL               GIVEN        WANTED                         WHERE
 1829 
 1830 Datatype               YES          YES                           canTyConApp
 1831 Newtype                YES          YES                           canTyConApp
 1832 Data family            YES          YES                           canTyConApp
 1833 Type family            NO{1}        YES, in injective args{1}     canEqCanLHS2
 1834 AppTy                  YES          YES                           can_eq_app
 1835 
 1836 REPRESENTATIONAL      GIVEN        WANTED
 1837 
 1838 Datatype               YES          YES                           canTyConApp
 1839 Newtype                NO{2}       MAYBE{2}                canTyConApp(can_decompose)
 1840 Data family            NO{3}       MAYBE{3}                canTyConApp(can_decompose)
 1841 Type family            NO           NO                            canEqCanLHS2
 1842 AppTy                  NO{4}        NO{4}                         can_eq_nc'
 1843 
 1844 {1}: Type families can be injective in some, but not all, of their arguments,
 1845 so we want to do partial decomposition. This is quite different than the way
 1846 other decomposition is done, where the decomposed equalities replace the original
 1847 one. We thus proceed much like we do with superclasses, emitting new Deriveds
 1848 when "decomposing" a partially-injective type family Wanted. Injective type
 1849 families have no corresponding evidence of their injectivity, so we cannot
 1850 decompose an injective-type-family Given.
 1851 
 1852 {2}: See Note [Decomposing newtypes at representational role]
 1853 
 1854 {3}: Because of the possibility of newtype instances, we must treat
 1855 data families like newtypes. See also
 1856 Note [Decomposing newtypes at representational role]. See #10534 and
 1857 test case typecheck/should_fail/T10534.
 1858 
 1859 {4}: See Note [Decomposing AppTy at representational role]
 1860 
 1861 In the implementation of can_eq_nc and friends, we don't directly pattern
 1862 match using lines like in the tables above, as those tables don't cover
 1863 all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
 1864 boiling the tables above down to rule (*). The exceptions to rule (*) are for
 1865 injective type families, which are handled separately from other decompositions,
 1866 and the MAYBE entries above.
 1867 
 1868 Note [Decomposing newtypes at representational role]
 1869 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1870 This note discusses the 'newtype' line in the REPRESENTATIONAL table
 1871 in Note [Decomposing equality]. (At nominal role, newtypes are fully
 1872 decomposable.)
 1873 
 1874 Here is a representative example of why representational equality over
 1875 newtypes is tricky:
 1876 
 1877   newtype Nt a = Mk Bool         -- NB: a is not used in the RHS,
 1878   type role Nt representational  -- but the user gives it an R role anyway
 1879 
 1880 If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
 1881 [W] alpha ~R beta, because it's possible that alpha and beta aren't
 1882 representationally equal. Here's another example.
 1883 
 1884   newtype Nt a = MkNt (Id a)
 1885   type family Id a where Id a = a
 1886 
 1887   [W] Nt Int ~R Nt Age
 1888 
 1889 Because of its use of a type family, Nt's parameter will get inferred to have
 1890 a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
 1891 is unsatisfiable. Unwrapping, though, leads to a solution.
 1892 
 1893 Conclusion:
 1894  * Unwrap newtypes before attempting to decompose them.
 1895    This is done in can_eq_nc'.
 1896 
 1897 It all comes from the fact that newtypes aren't necessarily injective
 1898 w.r.t. representational equality.
 1899 
 1900 Furthermore, as explained in Note [NthCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
 1901 NthCo on representational coercions over newtypes. NthCo comes into play
 1902 only when decomposing givens.
 1903 
 1904 Conclusion:
 1905  * Do not decompose [G] N s ~R N t
 1906 
 1907 Is it sensible to decompose *Wanted* constraints over newtypes?  Yes!
 1908 It's the only way we could ever prove (IO Int ~R IO Age), recalling
 1909 that IO is a newtype.
 1910 
 1911 However we must be careful.  Consider
 1912 
 1913   type role Nt representational
 1914 
 1915   [G] Nt a ~R Nt b       (1)
 1916   [W] NT alpha ~R Nt b   (2)
 1917   [W] alpha ~ a          (3)
 1918 
 1919 If we focus on (3) first, we'll substitute in (2), and now it's
 1920 identical to the given (1), so we succeed.  But if we focus on (2)
 1921 first, and decompose it, we'll get (alpha ~R b), which is not soluble.
 1922 This is exactly like the question of overlapping Givens for class
 1923 constraints: see Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
 1924 
 1925 Conclusion:
 1926   * Decompose [W] N s ~R N t  iff there no given constraint that could
 1927     later solve it.
 1928 
 1929 Note [Decomposing AppTy at representational role]
 1930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1931 We never decompose AppTy at a representational role. For Givens, doing
 1932 so is simply unsound: the LRCo coercion former requires a nominal-roled
 1933 arguments. (See (1) for an example of why.) For Wanteds, decomposing
 1934 would be sound, but it would be a guess, and a non-confluent one at that.
 1935 
 1936 Here is an example:
 1937 
 1938     [G] g1 :: a ~R b
 1939     [W] w1 :: Maybe b ~R alpha a
 1940     [W] w2 :: alpha ~ Maybe
 1941 
 1942 Suppose we see w1 before w2. If we were to decompose, we would decompose
 1943 this to become
 1944 
 1945     [W] w3 :: Maybe ~R alpha
 1946     [W] w4 :: b ~ a
 1947 
 1948 Note that w4 is *nominal*. A nominal role here is necessary because AppCo
 1949 requires a nominal role on its second argument. (See (2) for an example of
 1950 why.) If we decomposed w1 to w3,w4, we would then get stuck, because w4
 1951 is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe,
 1952 all is well, as we can decompose Maybe b ~R Maybe a into b ~R a.
 1953 
 1954 Another example:
 1955 
 1956     newtype Phant x = MkPhant Int
 1957 
 1958     [W] w1 :: Phant Int ~R alpha Bool
 1959     [W] w2 :: alpha ~ Phant
 1960 
 1961 If we see w1 first, decomposing would be disastrous, as we would then try
 1962 to solve Int ~ Bool. Instead, spotting w2 allows us to simplify w1 to become
 1963 
 1964     [W] w1' :: Phant Int ~R Phant Bool
 1965 
 1966 which can then (assuming MkPhant is in scope) be simplified to Int ~R Int,
 1967 and all will be well. See also Note [Unwrap newtypes first].
 1968 
 1969 Bottom line: never decompose AppTy with representational roles.
 1970 
 1971 (1) Decomposing a Given AppTy over a representational role is simply
 1972 unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
 1973 the newtype Phant, above), then we surely don't want any relationship
 1974 between Int and Bool, lest we also have co2 :: Phant ~ a around.
 1975 
 1976 (2) The role on the AppCo coercion is a conservative choice, because we don't
 1977 know the role signature of the function. For example, let's assume we could
 1978 have a representational role on the second argument of AppCo. Then, consider
 1979 
 1980     data G a where    -- G will have a nominal role, as G is a GADT
 1981       MkG :: G Int
 1982     newtype Age = MkAge Int
 1983 
 1984     co1 :: G ~R a        -- by assumption
 1985     co2 :: Age ~R Int    -- by newtype axiom
 1986     co3 = AppCo co1 co2 :: G Age ~R a Int    -- by our broken AppCo
 1987 
 1988 and now co3 can be used to cast MkG to have type G Age, in violation of
 1989 the way GADTs are supposed to work (which is to use nominal equality).
 1990 
 1991 -}
 1992 
 1993 canDecomposableTyConAppOK :: CtEvidence -> EqRel
 1994                           -> TyCon -> [TcType] -> [TcType]
 1995                           -> TcS (StopOrContinue Ct)
 1996 -- Precondition: tys1 and tys2 are the same length, hence "OK"
 1997 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
 1998   = assert (tys1 `equalLength` tys2) $
 1999     do { traceTcS "canDecomposableTyConAppOK"
 2000                   (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2)
 2001        ; case ev of
 2002            CtDerived {}
 2003              -> unifyDeriveds loc tc_roles tys1 tys2
 2004 
 2005            CtWanted { ctev_dest = dest }
 2006                   -- new_locs and tc_roles are both infinite, so
 2007                   -- we are guaranteed that cos has the same length
 2008                   -- as tys1 and tys2
 2009              -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
 2010                    ; setWantedEq dest (mkTyConAppCo role tc cos) }
 2011 
 2012            CtGiven { ctev_evar = evar }
 2013              -> do { let ev_co = mkCoVarCo evar
 2014                    ; given_evs <- newGivenEvVars loc $
 2015                                   [ ( mkPrimEqPredRole r ty1 ty2
 2016                                     , evCoercion $ mkNthCo r i ev_co )
 2017                                   | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
 2018                                   , r /= Phantom
 2019                                   , not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
 2020                    ; emitWorkNC given_evs }
 2021 
 2022     ; stopWith ev "Decomposed TyConApp" }
 2023 
 2024   where
 2025     loc        = ctEvLoc ev
 2026     role       = eqRelRole eq_rel
 2027 
 2028       -- infinite, as tyConRolesX returns an infinite tail of Nominal
 2029     tc_roles   = tyConRolesX role tc
 2030 
 2031       -- Add nuances to the location during decomposition:
 2032       --  * if the argument is a kind argument, remember this, so that error
 2033       --    messages say "kind", not "type". This is determined based on whether
 2034       --    the corresponding tyConBinder is named (that is, dependent)
 2035       --  * if the argument is invisible, note this as well, again by
 2036       --    looking at the corresponding binder
 2037       -- For oversaturated tycons, we need the (repeat loc) tail, which doesn't
 2038       -- do either of these changes. (Forgetting to do so led to #16188)
 2039       --
 2040       -- NB: infinite in length
 2041     new_locs = [ new_loc
 2042                | bndr <- tyConBinders tc
 2043                , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc
 2044                               | otherwise               = loc
 2045                      new_loc  | isInvisibleTyConBinder bndr
 2046                               = updateCtLocOrigin new_loc0 toInvisibleOrigin
 2047                               | otherwise
 2048                               = new_loc0 ]
 2049                ++ repeat loc
 2050 
 2051 -- | Call when canonicalizing an equality fails, but if the equality is
 2052 -- representational, there is some hope for the future.
 2053 -- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
 2054 canEqFailure :: CtEvidence -> EqRel
 2055              -> TcType -> TcType -> TcS (StopOrContinue Ct)
 2056 canEqFailure ev NomEq ty1 ty2
 2057   = canEqHardFailure ev ty1 ty2
 2058 canEqFailure ev ReprEq ty1 ty2
 2059   = do { redn1 <- rewrite ev ty1
 2060        ; redn2 <- rewrite ev ty2
 2061             -- We must rewrite the types before putting them in the
 2062             -- inert set, so that we are sure to kick them out when
 2063             -- new equalities become available
 2064        ; traceTcS "canEqFailure with ReprEq" $
 2065          vcat [ ppr ev, ppr redn1, ppr redn2 ]
 2066        ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
 2067        ; continueWith (mkIrredCt ReprEqReason new_ev) }
 2068 
 2069 -- | Call when canonicalizing an equality fails with utterly no hope.
 2070 canEqHardFailure :: CtEvidence
 2071                  -> TcType -> TcType -> TcS (StopOrContinue Ct)
 2072 -- See Note [Make sure that insolubles are fully rewritten]
 2073 canEqHardFailure ev ty1 ty2
 2074   = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
 2075        ; redn1 <- rewrite ev ty1
 2076        ; redn2 <- rewrite ev ty2
 2077        ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2
 2078        ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
 2079 
 2080 {-
 2081 Note [Decomposing TyConApps]
 2082 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2083 If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
 2084   (s1 ~ s2, t1 ~ t2)
 2085 and push those back into the work list.  But if
 2086   s1 = K k1    s2 = K k2
 2087 then we will just decomopose s1~s2, and it might be better to
 2088 do so on the spot.  An important special case is where s1=s2,
 2089 and we get just Refl.
 2090 
 2091 So canDecomposableTyCon is a fast-path decomposition that uses
 2092 unifyWanted etc to short-cut that work.
 2093 
 2094 Note [Canonicalising type applications]
 2095 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2096 Given (s1 t1) ~ ty2, how should we proceed?
 2097 The simple thing is to see if ty2 is of form (s2 t2), and
 2098 decompose.
 2099 
 2100 However, over-eager decomposition gives bad error messages
 2101 for things like
 2102    a b ~ Maybe c
 2103    e f ~ p -> q
 2104 Suppose (in the first example) we already know a~Array.  Then if we
 2105 decompose the application eagerly, yielding
 2106    a ~ Maybe
 2107    b ~ c
 2108 we get an error        "Can't match Array ~ Maybe",
 2109 but we'd prefer to get "Can't match Array b ~ Maybe c".
 2110 
 2111 So instead can_eq_wanted_app rewrites the LHS and RHS, in the hope of
 2112 replacing (a b) by (Array b), before using try_decompose_app to
 2113 decompose it.
 2114 
 2115 Note [Make sure that insolubles are fully rewritten]
 2116 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2117 When an equality fails, we still want to rewrite the equality
 2118 all the way down, so that it accurately reflects
 2119  (a) the mutable reference substitution in force at start of solving
 2120  (b) any ty-binds in force at this point in solving
 2121 See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet.
 2122 And if we don't do this there is a bad danger that
 2123 GHC.Tc.Solver.applyTyVarDefaulting will find a variable
 2124 that has in fact been substituted.
 2125 
 2126 Note [Do not decompose Given polytype equalities]
 2127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2128 Consider [G] (forall a. t1 ~ forall a. t2).  Can we decompose this?
 2129 No -- what would the evidence look like?  So instead we simply discard
 2130 this given evidence.
 2131 
 2132 
 2133 Note [Combining insoluble constraints]
 2134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2135 As this point we have an insoluble constraint, like Int~Bool.
 2136 
 2137  * If it is Wanted, delete it from the cache, so that subsequent
 2138    Int~Bool constraints give rise to separate error messages
 2139 
 2140  * But if it is Derived, DO NOT delete from cache.  A class constraint
 2141    may get kicked out of the inert set, and then have its functional
 2142    dependency Derived constraints generated a second time. In that
 2143    case we don't want to get two (or more) error messages by
 2144    generating two (or more) insoluble fundep constraints from the same
 2145    class constraint.
 2146 
 2147 Note [No top-level newtypes on RHS of representational equalities]
 2148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2149 Suppose we're in this situation:
 2150 
 2151  work item:  [W] c1 : a ~R b
 2152      inert:  [G] c2 : b ~R Id a
 2153 
 2154 where
 2155   newtype Id a = Id a
 2156 
 2157 We want to make sure canEqCanLHS sees [W] a ~R a, after b is rewritten
 2158 and the Id newtype is unwrapped. This is assured by requiring only rewritten
 2159 types in canEqCanLHS *and* having the newtype-unwrapping check above
 2160 the tyvar check in can_eq_nc.
 2161 
 2162 Note [Put touchable variables on the left]
 2163 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2164 Ticket #10009, a very nasty example:
 2165 
 2166     f :: (UnF (F b) ~ b) => F b -> ()
 2167 
 2168     g :: forall a. (UnF (F a) ~ a) => a -> ()
 2169     g _ = f (undefined :: F a)
 2170 
 2171 For g we get [G]  g1 : UnF (F a) ~ a
 2172              [WD] w1 : UnF (F beta) ~ beta
 2173              [WD] w2 : F a ~ F beta
 2174 
 2175 g1 is canonical (CEqCan). It is oriented as above because a is not touchable.
 2176 See canEqTyVarFunEq.
 2177 
 2178 w1 is similarly canonical, though the occurs-check in canEqTyVarFunEq is key
 2179 here.
 2180 
 2181 w2 is canonical. But which way should it be oriented? As written, we'll be
 2182 stuck. When w2 is added to the inert set, nothing gets kicked out: g1 is
 2183 a Given (and Wanteds don't rewrite Givens), and w2 doesn't mention the LHS
 2184 of w2. We'll thus lose.
 2185 
 2186 But if w2 is swapped around, to
 2187 
 2188     [D] w3 : F beta ~ F a
 2189 
 2190 then (after emitting shadow Deriveds, etc. See GHC.Tc.Solver.Monad
 2191 Note [The improvement story and derived shadows]) we'll kick w1 out of the inert
 2192 set (it mentions the LHS of w3). We then rewrite w1 to
 2193 
 2194     [D] w4 : UnF (F a) ~ beta
 2195 
 2196 and then, using g1, to
 2197 
 2198     [D] w5 : a ~ beta
 2199 
 2200 at which point we can unify and go on to glory. (This rewriting actually
 2201 happens all at once, in the call to rewrite during canonicalisation.)
 2202 
 2203 But what about the new LHS makes it better? It mentions a variable (beta)
 2204 that can appear in a Wanted -- a touchable metavariable never appears
 2205 in a Given. On the other hand, the original LHS mentioned only variables
 2206 that appear in Givens. We thus choose to put variables that can appear
 2207 in Wanteds on the left.
 2208 
 2209 Ticket #12526 is another good example of this in action.
 2210 
 2211 -}
 2212 
 2213 ---------------------
 2214 canEqCanLHS :: CtEvidence            -- ev :: lhs ~ rhs
 2215             -> EqRel -> SwapFlag
 2216             -> CanEqLHS              -- lhs (or, if swapped, rhs)
 2217             -> TcType                -- lhs: pretty lhs, already rewritten
 2218             -> TcType -> TcType      -- rhs: already rewritten
 2219             -> TcS (StopOrContinue Ct)
 2220 canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
 2221   | k1 `tcEqType` k2
 2222   = canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
 2223 
 2224   | otherwise
 2225   = canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 k1 xi2 ps_xi2 k2
 2226 
 2227   where
 2228     k1 = canEqLHSKind lhs1
 2229     k2 = tcTypeKind xi2
 2230 
 2231 canEqCanLHSHetero :: CtEvidence         -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
 2232                   -> EqRel -> SwapFlag
 2233                   -> CanEqLHS -> TcType -- xi1, pretty xi1
 2234                   -> TcKind             -- ki1
 2235                   -> TcType -> TcType   -- xi2, pretty xi2 :: ki2
 2236                   -> TcKind             -- ki2
 2237                   -> TcS (StopOrContinue Ct)
 2238 canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
 2239   -- See Note [Equalities with incompatible kinds]
 2240   = do { kind_co <- emit_kind_co   -- :: ki2 ~N ki1
 2241 
 2242        ; let  -- kind_co :: (ki2 :: *) ~N (ki1 :: *)   (whether swapped or not)
 2243               -- co1     :: kind(tv1) ~N ki1
 2244              ps_rhs' = ps_xi2 `mkCastTy` kind_co   -- :: ki1
 2245 
 2246              lhs_redn = mkReflRedn role xi1
 2247              rhs_redn@(Reduction _ rhs')
 2248                = mkGReflRightRedn role xi2 kind_co
 2249 
 2250        ; traceTcS "Hetero equality gives rise to kind equality"
 2251            (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
 2252        ; type_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn
 2253 
 2254           -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more
 2255        ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 rhs' ps_rhs' }
 2256   where
 2257     emit_kind_co :: TcS CoercionN
 2258     emit_kind_co
 2259       | CtGiven { ctev_evar = evar } <- ev
 2260       = do { let kind_co = maybe_sym $ mkTcKindCo (mkTcCoVarCo evar)  -- :: k2 ~ k1
 2261            ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
 2262            ; emitWorkNC [kind_ev]
 2263            ; return (ctEvCoercion kind_ev) }
 2264 
 2265       | otherwise
 2266       = unifyWanted kind_loc Nominal ki2 ki1
 2267 
 2268     xi1      = canEqLHSType lhs1
 2269     loc      = ctev_loc ev
 2270     role     = eqRelRole eq_rel
 2271     kind_loc = mkKindLoc xi1 xi2 loc
 2272     kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki2 ki1
 2273 
 2274     maybe_sym = case swapped of
 2275           IsSwapped  -> id         -- if the input is swapped, then we already
 2276                                    -- will have k2 ~ k1
 2277           NotSwapped -> mkTcSymCo
 2278 
 2279 -- guaranteed that tcTypeKind lhs == tcTypeKind rhs
 2280 canEqCanLHSHomo :: CtEvidence
 2281                 -> EqRel -> SwapFlag
 2282                 -> CanEqLHS           -- lhs (or, if swapped, rhs)
 2283                 -> TcType             -- pretty lhs
 2284                 -> TcType -> TcType   -- rhs, pretty rhs
 2285                 -> TcS (StopOrContinue Ct)
 2286 canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
 2287   | (xi2', mco) <- split_cast_ty xi2
 2288   , Just lhs2 <- canEqLHS_maybe xi2'
 2289   = canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 (ps_xi2 `mkCastTyMCo` mkTcSymMCo mco) mco
 2290 
 2291   | otherwise
 2292   = canEqCanLHSFinish ev eq_rel swapped lhs1 ps_xi2
 2293 
 2294   where
 2295     split_cast_ty (CastTy ty co) = (ty, MCo co)
 2296     split_cast_ty other          = (other, MRefl)
 2297 
 2298 -- This function deals with the case that both LHS and RHS are potential
 2299 -- CanEqLHSs.
 2300 canEqCanLHS2 :: CtEvidence              -- lhs ~ (rhs |> mco)
 2301                                         -- or, if swapped: (rhs |> mco) ~ lhs
 2302              -> EqRel -> SwapFlag
 2303              -> CanEqLHS                -- lhs (or, if swapped, rhs)
 2304              -> TcType                  -- pretty lhs
 2305              -> CanEqLHS                -- rhs
 2306              -> TcType                  -- pretty rhs
 2307              -> MCoercion               -- :: kind(rhs) ~N kind(lhs)
 2308              -> TcS (StopOrContinue Ct)
 2309 canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
 2310   | lhs1 `eqCanEqLHS` lhs2
 2311     -- It must be the case that mco is reflexive
 2312   = canEqReflexive ev eq_rel (canEqLHSType lhs1)
 2313 
 2314   | TyVarLHS tv1 <- lhs1
 2315   , TyVarLHS tv2 <- lhs2
 2316   , swapOverTyVars (isGiven ev) tv1 tv2
 2317   = do { traceTcS "canEqLHS2 swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
 2318        ; new_ev <- do_swap
 2319        ; canEqCanLHSFinish new_ev eq_rel IsSwapped (TyVarLHS tv2)
 2320                                                    (ps_xi1 `mkCastTyMCo` sym_mco) }
 2321 
 2322   | TyVarLHS tv1 <- lhs1
 2323   , TyFamLHS fun_tc2 fun_args2 <- lhs2
 2324   = canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
 2325 
 2326   | TyFamLHS fun_tc1 fun_args1 <- lhs1
 2327   , TyVarLHS tv2 <- lhs2
 2328   = do { new_ev <- do_swap
 2329        ; canEqTyVarFunEq new_ev eq_rel IsSwapped tv2 ps_xi2
 2330                                                  fun_tc1 fun_args1 ps_xi1 sym_mco }
 2331 
 2332   | TyFamLHS fun_tc1 fun_args1 <- lhs1
 2333   , TyFamLHS fun_tc2 fun_args2 <- lhs2
 2334   = do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
 2335 
 2336          -- emit derived equalities for injective type families
 2337        ; let inj_eqns :: [TypeEqn]  -- TypeEqn = Pair Type
 2338              inj_eqns
 2339                | ReprEq <- eq_rel   = []   -- injectivity applies only for nom. eqs.
 2340                | fun_tc1 /= fun_tc2 = []   -- if the families don't match, stop.
 2341 
 2342                | Injective inj <- tyConInjectivityInfo fun_tc1
 2343                = [ Pair arg1 arg2
 2344                  | (arg1, arg2, True) <- zip3 fun_args1 fun_args2 inj ]
 2345 
 2346                  -- built-in synonym families don't have an entry point
 2347                  -- for this use case. So, we just use sfInteractInert
 2348                  -- and pass two equal RHSs. We *could* add another entry
 2349                  -- point, but then there would be a burden to make
 2350                  -- sure the new entry point and existing ones were
 2351                  -- internally consistent. This is slightly distasteful,
 2352                  -- but it works well in practice and localises the
 2353                  -- problem.
 2354                | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1
 2355                = let ki1 = canEqLHSKind lhs1
 2356                      ki2 | MRefl <- mco
 2357                          = ki1   -- just a small optimisation
 2358                          | otherwise
 2359                          = canEqLHSKind lhs2
 2360 
 2361                      fake_rhs1 = anyTypeOfKind ki1
 2362                      fake_rhs2 = anyTypeOfKind ki2
 2363                  in
 2364                  sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2
 2365 
 2366                | otherwise  -- ordinary, non-injective type family
 2367                = []
 2368 
 2369        ; unless (isGiven ev) $
 2370          mapM_ (unifyDerived (ctEvLoc ev) Nominal) inj_eqns
 2371 
 2372        ; tclvl <- getTcLevel
 2373        ; dflags <- getDynFlags
 2374        ; let tvs1 = tyCoVarsOfTypes fun_args1
 2375              tvs2 = tyCoVarsOfTypes fun_args2
 2376 
 2377              swap_for_rewriting = anyVarSet (isTouchableMetaTyVar tclvl) tvs2 &&
 2378                           -- swap 'em: Note [Put touchable variables on the left]
 2379                                   not (anyVarSet (isTouchableMetaTyVar tclvl) tvs1)
 2380                           -- this check is just to avoid unfruitful swapping
 2381 
 2382                -- If we have F a ~ F (F a), we want to swap.
 2383              swap_for_occurs
 2384                | cterHasNoProblem   $ checkTyFamEq dflags fun_tc2 fun_args2
 2385                                                    (mkTyConApp fun_tc1 fun_args1)
 2386                , cterHasOccursCheck $ checkTyFamEq dflags fun_tc1 fun_args1
 2387                                                    (mkTyConApp fun_tc2 fun_args2)
 2388                = True
 2389 
 2390                | otherwise
 2391                = False
 2392 
 2393        ; if swap_for_rewriting || swap_for_occurs
 2394          then do { new_ev <- do_swap
 2395                  ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
 2396          else finish_without_swapping }
 2397 
 2398   -- that's all the special cases. Now we just figure out which non-special case
 2399   -- to continue to.
 2400   | otherwise
 2401   = finish_without_swapping
 2402 
 2403   where
 2404     sym_mco = mkTcSymMCo mco
 2405 
 2406     do_swap = rewriteCastedEquality ev eq_rel swapped (canEqLHSType lhs1) (canEqLHSType lhs2) mco
 2407     finish_without_swapping = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco)
 2408 
 2409 
 2410 -- This function handles the case where one side is a tyvar and the other is
 2411 -- a type family application. Which to put on the left?
 2412 --   If the tyvar is a touchable meta-tyvar, put it on the left, as this may
 2413 --   be our only shot to unify.
 2414 --   Otherwise, put the function on the left, because it's generally better to
 2415 --   rewrite away function calls. This makes types smaller. And it seems necessary:
 2416 --     [W] F alpha ~ alpha
 2417 --     [W] F alpha ~ beta
 2418 --     [W] G alpha beta ~ Int   ( where we have type instance G a a = a )
 2419 --   If we end up with a stuck alpha ~ F alpha, we won't be able to solve this.
 2420 --   Test case: indexed-types/should_compile/CEqCanOccursCheck
 2421 canEqTyVarFunEq :: CtEvidence               -- :: lhs ~ (rhs |> mco)
 2422                                             -- or (rhs |> mco) ~ lhs if swapped
 2423                 -> EqRel -> SwapFlag
 2424                 -> TyVar -> TcType          -- lhs (or if swapped rhs), pretty lhs
 2425                 -> TyCon -> [Xi] -> TcType  -- rhs (or if swapped lhs) fun and args, pretty rhs
 2426                 -> MCoercion                -- :: kind(rhs) ~N kind(lhs)
 2427                 -> TcS (StopOrContinue Ct)
 2428 canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
 2429   = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv1 rhs
 2430        ; dflags       <- getDynFlags
 2431        ; if | case is_touchable of { Untouchable -> False; _ -> True }
 2432             , cterHasNoProblem $
 2433                 checkTyVarEq dflags tv1 rhs `cterRemoveProblem` cteTypeFamily
 2434             -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs
 2435 
 2436             | otherwise
 2437               -> do { new_ev <- rewriteCastedEquality ev eq_rel swapped
 2438                                   (mkTyVarTy tv1) (mkTyConApp fun_tc2 fun_args2)
 2439                                   mco
 2440                     ; canEqCanLHSFinish new_ev eq_rel IsSwapped
 2441                                   (TyFamLHS fun_tc2 fun_args2)
 2442                                   (ps_xi1 `mkCastTyMCo` sym_mco) } }
 2443   where
 2444     sym_mco = mkTcSymMCo mco
 2445     rhs = ps_xi2 `mkCastTyMCo` mco
 2446 
 2447 -- The RHS here is either not CanEqLHS, or it's one that we
 2448 -- want to rewrite the LHS to (as per e.g. swapOverTyVars)
 2449 canEqCanLHSFinish :: CtEvidence
 2450                   -> EqRel -> SwapFlag
 2451                   -> CanEqLHS             -- lhs (or, if swapped, rhs)
 2452                   -> TcType               -- rhs (or, if swapped, lhs)
 2453                   -> TcS (StopOrContinue Ct)
 2454 canEqCanLHSFinish ev eq_rel swapped lhs rhs
 2455 -- RHS is fully rewritten, but with type synonyms
 2456 -- preserved as much as possible
 2457 -- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K)
 2458 -- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2
 2459 
 2460   = do { dflags <- getDynFlags
 2461        ; new_ev <- rewriteEqEvidence ev swapped
 2462                      (mkReflRedn role lhs_ty)
 2463                      (mkReflRedn role rhs)
 2464 
 2465      -- by now, (TyEq:K) is already satisfied
 2466        ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs)
 2467 
 2468      -- by now, (TyEq:N) is already satisfied (if applicable)
 2469        ; massert (not bad_newtype)
 2470 
 2471      -- guarantees (TyEq:OC), (TyEq:F)
 2472      -- Must do the occurs check even on tyvar/tyvar
 2473      -- equalities, in case have  x ~ (y :: ..x...); this is #12593.
 2474      -- This next line checks also for coercion holes (TyEq:H); see
 2475      -- Note [Equalities with incompatible kinds]
 2476        ; let result0 = checkTypeEq dflags lhs rhs `cterRemoveProblem` cteTypeFamily
 2477      -- type families are OK here
 2478      -- NB: no occCheckExpand here; see Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite
 2479 
 2480 
 2481               -- a ~R# b a is soluble if b later turns out to be Identity
 2482              result = case eq_rel of
 2483                         NomEq  -> result0
 2484                         ReprEq -> cterSetOccursCheckSoluble result0
 2485 
 2486              reason | result `cterHasOnlyProblem` cteHoleBlocker
 2487                     = HoleBlockerReason (coercionHolesOfType rhs)
 2488                     | otherwise
 2489                     = NonCanonicalReason result
 2490 
 2491        ; if cterHasNoProblem result
 2492          then do { traceTcS "CEqCan" (ppr lhs $$ ppr rhs)
 2493                  ; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
 2494                                         , cc_rhs = rhs, cc_eq_rel = eq_rel }) }
 2495 
 2496          else do { m_stuff <- breakTyVarCycle_maybe ev result lhs rhs
 2497                            -- See Note [Type variable cycles];
 2498                            -- returning Nothing is the vastly common case
 2499                  ; case m_stuff of
 2500                      { Nothing ->
 2501                          do { traceTcS "canEqCanLHSFinish can't make a canonical"
 2502                                        (ppr lhs $$ ppr rhs)
 2503                             ; continueWith (mkIrredCt reason new_ev) }
 2504                      ; Just (lhs_tv, rhs_redn@(Reduction _ new_rhs)) ->
 2505               do { traceTcS "canEqCanLHSFinish breaking a cycle" $
 2506                             ppr lhs $$ ppr rhs
 2507                  ; traceTcS "new RHS:" (ppr new_rhs)
 2508 
 2509                    -- This check is Detail (1) in the Note
 2510                  ; if cterHasOccursCheck (checkTyVarEq dflags lhs_tv new_rhs)
 2511 
 2512                    then do { traceTcS "Note [Type variable cycles] Detail (1)"
 2513                                       (ppr new_rhs)
 2514                            ; continueWith (mkIrredCt reason new_ev) }
 2515 
 2516                    else do { -- See Detail (6) of Note [Type variable cycles]
 2517                              new_new_ev <- rewriteEqEvidence new_ev NotSwapped
 2518                                              (mkReflRedn Nominal lhs_ty)
 2519                                              rhs_redn
 2520 
 2521                            ; continueWith (CEqCan { cc_ev = new_new_ev
 2522                                                   , cc_lhs = lhs
 2523                                                   , cc_rhs = new_rhs
 2524                                                   , cc_eq_rel = eq_rel }) }}}}}
 2525   where
 2526     role = eqRelRole eq_rel
 2527 
 2528     lhs_ty = canEqLHSType lhs
 2529 
 2530     -- This is about (TyEq:N)
 2531     bad_newtype | ReprEq <- eq_rel
 2532                 , Just tc <- tyConAppTyCon_maybe rhs
 2533                 = isNewTyCon tc
 2534                 | otherwise
 2535                 = False
 2536 
 2537 -- | Solve a reflexive equality constraint
 2538 canEqReflexive :: CtEvidence    -- ty ~ ty
 2539                -> EqRel
 2540                -> TcType        -- ty
 2541                -> TcS (StopOrContinue Ct)   -- always Stop
 2542 canEqReflexive ev eq_rel ty
 2543   = do { setEvBindIfWanted ev (evCoercion $
 2544                                mkTcReflCo (eqRelRole eq_rel) ty)
 2545        ; stopWith ev "Solved by reflexivity" }
 2546 
 2547 rewriteCastedEquality :: CtEvidence     -- :: lhs ~ (rhs |> mco), or (rhs |> mco) ~ lhs
 2548                       -> EqRel -> SwapFlag
 2549                       -> TcType         -- lhs
 2550                       -> TcType         -- rhs
 2551                       -> MCoercion      -- mco
 2552                       -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs
 2553                                         -- result is independent of SwapFlag
 2554 rewriteCastedEquality ev eq_rel swapped lhs rhs mco
 2555   = rewriteEqEvidence ev swapped lhs_redn rhs_redn
 2556   where
 2557     lhs_redn = mkGReflRightMRedn role lhs sym_mco
 2558     rhs_redn = mkGReflLeftMRedn  role rhs mco
 2559 
 2560     sym_mco = mkTcSymMCo mco
 2561     role    = eqRelRole eq_rel
 2562 
 2563 {- Note [Equalities with incompatible kinds]
 2564 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2565 What do we do when we have an equality
 2566 
 2567   (tv :: k1) ~ (rhs :: k2)
 2568 
 2569 where k1 and k2 differ? Easy: we create a coercion that relates k1 and
 2570 k2 and use this to cast. To wit, from
 2571 
 2572   [X] (tv :: k1) ~ (rhs :: k2)
 2573 
 2574 (where [X] is [G], [W], or [D]), we go to
 2575 
 2576   [noDerived X] co :: k2 ~ k1
 2577   [X]           (tv :: k1) ~ ((rhs |> co) :: k1)
 2578 
 2579 where
 2580 
 2581   noDerived G = G
 2582   noDerived _ = W
 2583 
 2584 For reasons described in Wrinkle (2) below, we want the [X] constraint to be "blocked";
 2585 that is, it should be put aside, and not used to rewrite any other constraint,
 2586 until the kind-equality on which it depends (namely 'co' above) is solved.
 2587 To achieve this
 2588 * The [X] constraint is a CIrredCan
 2589 * With a cc_reason of HoleBlockerReason bchs
 2590 * Where 'bchs' is the set of "blocking coercion holes".  The blocking coercion
 2591   holes are the free coercion holes of [X]'s type
 2592 * When all the blocking coercion holes in the CIrredCan are filled (solved),
 2593   we convert [X] to a CNonCanonical and put it in the work list.
 2594 All this is described in more detail in Wrinkle (2).
 2595 
 2596 Wrinkles:
 2597 
 2598  (1) The noDerived step is because Derived equalities have no evidence.
 2599      And yet we absolutely need evidence to be able to proceed here.
 2600      Given evidence will use the KindCo coercion; Wanted evidence will
 2601      be a coercion hole. Even a Derived hetero equality begets a Wanted
 2602      kind equality.
 2603 
 2604  (2) Though it would be sound to do so, we must not mark the rewritten Wanted
 2605        [W] (tv :: k1) ~ ((rhs |> co) :: k1)
 2606      as canonical in the inert set. In particular, we must not unify tv.
 2607      If we did, the Wanted becomes a Given (effectively), and then can
 2608      rewrite other Wanteds. But that's bad: See Note [Wanteds do not rewrite Wanteds]
 2609      in GHC.Tc.Types.Constraint. The problem is about poor error messages. See #11198 for
 2610      tales of destruction.
 2611 
 2612      So, we have an invariant on CEqCan (TyEq:H) that the RHS does not have
 2613      any coercion holes. This is checked in checkTypeEq. Any equalities that
 2614      have such an RHS are turned into CIrredCans with a HoleBlockerReason. We also
 2615      must be sure to kick out any such CIrredCan constraints that mention coercion holes
 2616      when those holes get filled in, so that the unification step can now proceed.
 2617 
 2618      The kicking out is done in kickOutAfterFillingCoercionHole, and the inerts
 2619      are stored in the inert_blocked field of InertCans.
 2620 
 2621      However, we must be careful: we kick out only when no coercion holes are
 2622      left. The holes in the type are stored in the HoleBlockerReason CtIrredReason.
 2623      The extra check that there are no more remaining holes avoids
 2624      needless work when rewriting evidence (which fills coercion holes) and
 2625      aids efficiency.
 2626 
 2627      Moreover, kicking out when there are remaining unfilled holes can
 2628      cause a loop in the solver in this case:
 2629           [W] w1 :: (ty1 :: F a) ~ (ty2 :: s)
 2630      After canonicalisation, we discover that this equality is heterogeneous.
 2631      So we emit
 2632           [W] co_abc :: F a ~ s
 2633      and preserve the original as
 2634           [W] w2 :: (ty1 |> co_abc) ~ ty2    (blocked on co_abc)
 2635      Then, co_abc comes becomes the work item. It gets swapped in
 2636      canEqCanLHS2 and then back again in canEqTyVarFunEq. We thus get
 2637      co_abc := sym co_abd, and then co_abd := sym co_abe, with
 2638           [W] co_abe :: F a ~ s
 2639      This process has filled in co_abc. Suppose w2 were kicked out.
 2640      When it gets processed,
 2641      would get this whole chain going again. The solution is to
 2642      kick out a blocked constraint only when the result of filling
 2643      in the blocking coercion involves no further blocking coercions.
 2644      Alternatively, we could be careful not to do unnecessary swaps during
 2645      canonicalisation, but that seems hard to do, in general.
 2646 
 2647  (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
 2648      algorithm detailed here, producing [W] co :: k2 ~ k1, and adding
 2649      [W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time
 2650      later, we solve co, and fill in co's coercion hole. This kicks out
 2651      the irreducible as described in (2).
 2652      But now, during canonicalization, we see the cast
 2653      and remove it, in canEqCast. By the time we get into canEqCanLHS, the equality
 2654      is heterogeneous again, and the process repeats.
 2655 
 2656      To avoid this, we don't strip casts off a type if the other type
 2657      in the equality is a CanEqLHS (the scenario above can happen with a
 2658      type family, too. testcase: typecheck/should_compile/T13822).
 2659      And this is an improvement regardless:
 2660      because tyvars can, generally, unify with casted types, there's no
 2661      reason to go through the work of stripping off the cast when the
 2662      cast appears opposite a tyvar. This is implemented in the cast case
 2663      of can_eq_nc'.
 2664 
 2665  (4) Reporting an error for a constraint that is blocked with HoleBlockerReason
 2666      is hard: what would we say to users? And we don't
 2667      really need to report, because if a constraint is blocked, then
 2668      there is unsolved wanted blocking it; that unsolved wanted will
 2669      be reported. We thus push such errors to the bottom of the queue
 2670      in the error-reporting code; they should never be printed.
 2671 
 2672      (4a) It would seem possible to do this filtering just based on the
 2673           presence of a blocking coercion hole. However, this is no good,
 2674           as it suppresses e.g. no-instance-found errors. We thus record
 2675           a CtIrredReason in CIrredCan and filter based on this status.
 2676           This happened in T14584. An alternative approach is to expressly
 2677           look for *equalities* with blocking coercion holes, but actually
 2678           recording the blockage in a status field seems nicer.
 2679 
 2680      (4b) The error message might be printed with -fdefer-type-errors,
 2681           so it still must exist. This is the only reason why there is
 2682           a message at all. Otherwise, we could simply do nothing.
 2683 
 2684 Historical note:
 2685 
 2686 We used to do this via emitting a Derived kind equality and then parking
 2687 the heterogeneous equality as irreducible. But this new approach is much
 2688 more direct. And it doesn't produce duplicate Deriveds (as the old one did).
 2689 
 2690 Note [Type synonyms and canonicalization]
 2691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2692 We treat type synonym applications as xi types, that is, they do not
 2693 count as type function applications.  However, we do need to be a bit
 2694 careful with type synonyms: like type functions they may not be
 2695 generative or injective.  However, unlike type functions, they are
 2696 parametric, so there is no problem in expanding them whenever we see
 2697 them, since we do not need to know anything about their arguments in
 2698 order to expand them; this is what justifies not having to treat them
 2699 as specially as type function applications.  The thing that causes
 2700 some subtleties is that we prefer to leave type synonym applications
 2701 *unexpanded* whenever possible, in order to generate better error
 2702 messages.
 2703 
 2704 If we encounter an equality constraint with type synonym applications
 2705 on both sides, or a type synonym application on one side and some sort
 2706 of type application on the other, we simply must expand out the type
 2707 synonyms in order to continue decomposing the equality constraint into
 2708 primitive equality constraints.  For example, suppose we have
 2709 
 2710   type F a = [Int]
 2711 
 2712 and we encounter the equality
 2713 
 2714   F a ~ [b]
 2715 
 2716 In order to continue we must expand F a into [Int], giving us the
 2717 equality
 2718 
 2719   [Int] ~ [b]
 2720 
 2721 which we can then decompose into the more primitive equality
 2722 constraint
 2723 
 2724   Int ~ b.
 2725 
 2726 However, if we encounter an equality constraint with a type synonym
 2727 application on one side and a variable on the other side, we should
 2728 NOT (necessarily) expand the type synonym, since for the purpose of
 2729 good error messages we want to leave type synonyms unexpanded as much
 2730 as possible.  Hence the ps_xi1, ps_xi2 argument passed to canEqCanLHS.
 2731 
 2732 Note [Type variable cycles]
 2733 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2734 Consider this situation (from indexed-types/should_compile/GivenLoop):
 2735 
 2736   instance C (Maybe b)
 2737   *[G] a ~ Maybe (F a)
 2738   [W] C a
 2739 
 2740 or (typecheck/should_compile/T19682b):
 2741 
 2742   instance C (a -> b)
 2743   *[WD] alpha ~ (Arg alpha -> Res alpha)
 2744   [W] C alpha
 2745 
 2746 In order to solve the final Wanted, we must use the starred constraint
 2747 for rewriting. But note that both starred constraints have occurs-check failures,
 2748 and so we can't straightforwardly add these to the inert set and
 2749 use them for rewriting. (NB: A rigid type constructor is at the
 2750 top of both RHSs. If the type family were at the top, we'd just reorient
 2751 in canEqTyVarFunEq.)
 2752 
 2753 The key idea is to replace the type family applications in the RHS of the
 2754 starred constraints with a fresh variable, which we'll call a cycle-breaker
 2755 variable, or cbv. Then, relate the cbv back with the original type family application
 2756 via new equality constraints. Our situations thus become:
 2757 
 2758   instance C (Maybe b)
 2759   [G] a ~ Maybe cbv
 2760   [G] F a ~ cbv
 2761   [W] C a
 2762 
 2763 or
 2764 
 2765   instance C (a -> b)
 2766   [WD] alpha ~ (cbv1 -> cbv2)
 2767   [WD] Arg alpha ~ cbv1
 2768   [WD] Res alpha ~ cbv2
 2769   [W] C alpha
 2770 
 2771 This transformation (creating the new types and emitting new equality
 2772 constraints) is done in breakTyVarCycle_maybe.
 2773 
 2774 The details depend on whether we're working with a Given or a Derived.
 2775 (Note that the Wanteds are really WDs, above. This is because Wanteds
 2776 are not used for rewriting.)
 2777 
 2778 Given
 2779 -----
 2780 
 2781 We emit a new Given, [G] F a ~ cbv, equating the type family application to
 2782 our new cbv. Note its orientation: The type family ends up on the left; see
 2783 commentary on canEqTyVarFunEq, which decides how to orient such cases. No
 2784 special treatment for CycleBreakerTvs is necessary. This scenario is now
 2785 easily soluble, by using the first Given to rewrite the Wanted, which can now
 2786 be solved.
 2787 
 2788 (The first Given actually also rewrites the second one, giving
 2789 [G] F (Maybe cbv) ~ cbv, but this causes no trouble.)
 2790 
 2791 Of course, we don't want our fresh variables leaking into e.g. error messages.
 2792 So we fill in the metavariables with their original type family applications
 2793 after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds).
 2794 This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in
 2795 InertSet, which contains the pairings invented in breakTyVarCycle_maybe.
 2796 
 2797 That is:
 2798 
 2799 We transform
 2800   [G] g : a ~ ...(F a)...
 2801 to
 2802   [G] (Refl a) : F a ~ cbv      -- CEqCan
 2803   [G] g        : a ~ ...cbv...  -- CEqCan
 2804 
 2805 Note that
 2806 * `cbv` is a fresh cycle breaker variable.
 2807 * `cbv` is a is a meta-tyvar, but it is completely untouchable.
 2808 * We track the cycle-breaker variables in inert_cycle_breakers in InertSet
 2809 * We eventually fill in the cycle-breakers, with `cbv := F a`.
 2810   No one else fills in cycle-breakers!
 2811 * In inert_cycle_breakers, we remember the (cbv, F a) pair; that is, we
 2812   remember the /original/ type.  The [G] F a ~ cbv constraint may be rewritten
 2813   by other givens (eg if we have another [G] a ~ (b,c), but at the end we
 2814   still fill in with cbv := F a
 2815 * This fill-in is done when solving is complete, by restoreTyVarCycles
 2816   in nestImplicTcS and runTcSWithEvBinds.
 2817 * The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is
 2818   ultimately going to happen.
 2819 
 2820 Wanted/Derived
 2821 --------------
 2822 The fresh cycle-breaker variables here must actually be normal, touchable
 2823 metavariables. That is, they are TauTvs. Nothing at all unusual. Repeating
 2824 the example from above, we have
 2825 
 2826   *[WD] alpha ~ (Arg alpha -> Res alpha)
 2827 
 2828 and we turn this into
 2829 
 2830   *[WD] alpha ~ (cbv1 -> cbv2)
 2831   [WD] Arg alpha ~ cbv1
 2832   [WD] Res alpha ~ cbv2
 2833 
 2834 where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below.
 2835 
 2836 Critically, we emit the constraint directly instead of calling unifyWanted.
 2837 Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
 2838 unification happens in the course of normal behavior of top-level
 2839 interactions, later in the solver pipeline. We know this unification will
 2840 indeed happen, because breakTyVarCycle_maybe, which decides whether to apply
 2841 this logic, goes to pains to make sure unification will succeed. Now, we're
 2842 here (including further context from our original example, from the top of the
 2843 Note):
 2844 
 2845   instance C (a -> b)
 2846   [WD] Arg (cbv1 -> cbv2) ~ cbv1
 2847   [WD] Res (cbv1 -> cbv2) ~ cbv2
 2848   [W] C (cbv1 -> cbv2)
 2849 
 2850 The first two WD constraints reduce to reflexivity and are discarded,
 2851 and the last is easily soluble.
 2852 
 2853 [Why TauTvs]:
 2854 Let's look at another example (typecheck/should_compile/T19682) where we need
 2855 to unify the cbvs:
 2856 
 2857   class    (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
 2858   instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
 2859 
 2860   type family SameShapeAs xs ys :: Constraint where
 2861     SameShapeAs '[] ys      = (ys ~ '[])
 2862     SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))
 2863 
 2864   type family AllEqF xs ys :: Constraint where
 2865     AllEqF '[]      '[]      = ()
 2866     AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)
 2867 
 2868   [WD] alpha ~ (Head alpha : Tail alpha)
 2869   [WD] AllEqF '[Bool] alpha
 2870 
 2871 Without the logic detailed in this Note, we're stuck here, as AllEqF cannot
 2872 reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach,
 2873 just as described above. We thus invent cbv1 and cbv2 and unify
 2874 alpha := cbv1 -> cbv2, yielding (after zonking)
 2875 
 2876   [WD] Head (cbv1 : cbv2) ~ cbv1
 2877   [WD] Tail (cbv1 : cbv2) ~ cbv2
 2878   [WD] AllEqF '[Bool] (cbv1 : cbv2)
 2879 
 2880 The first two WD constraints simplify to reflexivity and are discarded.
 2881 But the last reduces:
 2882 
 2883   [WD] Bool ~ cbv1
 2884   [WD] AllEq '[] cbv2
 2885 
 2886 The first of these is solved by unification: cbv1 := Bool. The second
 2887 is solved by the instance for AllEq to become
 2888 
 2889   [WD] AllEqF '[] cbv2
 2890   [WD] SameShapeAs '[] cbv2
 2891 
 2892 While the first of these is stuck, the second makes progress, to lead to
 2893 
 2894   [WD] AllEqF '[] cbv2
 2895   [WD] cbv2 ~ '[]
 2896 
 2897 This second constraint is solved by unification: cbv2 := '[]. We now
 2898 have
 2899 
 2900   [WD] AllEqF '[] '[]
 2901 
 2902 which reduces to
 2903 
 2904   [WD] ()
 2905 
 2906 which is trivially satisfiable. Hooray!
 2907 
 2908 Note that we need to unify the cbvs here; if we did not, there would be
 2909 no way to solve those constraints. That's why the cycle-breakers are
 2910 ordinary TauTvs.
 2911 
 2912 In all cases
 2913 ------------
 2914 
 2915 We detect this scenario by the following characteristics:
 2916  - a constraint with a tyvar on its LHS
 2917  - with a soluble occurs-check failure
 2918  - and a nominal equality
 2919  - and either
 2920     - a Given flavour (but see also Detail (7) below)
 2921     - a Wanted/Derived or just plain Derived flavour, with a touchable metavariable
 2922       on the left
 2923 
 2924 We don't use this trick for representational equalities, as there is no
 2925 concrete use case where it is helpful (unlike for nominal equalities).
 2926 Furthermore, because function applications can be CanEqLHSs, but newtype
 2927 applications cannot, the disparities between the cases are enough that it
 2928 would be effortful to expand the idea to representational equalities. A quick
 2929 attempt, with
 2930 
 2931       data family N a b
 2932 
 2933       f :: (Coercible a (N a b), Coercible (N a b) b) => a -> b
 2934       f = coerce
 2935 
 2936 failed with "Could not match 'b' with 'b'." Further work is held off
 2937 until when we have a concrete incentive to explore this dark corner.
 2938 
 2939 Details:
 2940 
 2941  (1) We don't look under foralls, at all, when substituting away type family
 2942      applications, because doing so can never be fruitful. Recall that we
 2943      are in a case like [G] a ~ forall b. ... a ....   Until we have a type
 2944      family that can pull the body out from a forall, this will always be
 2945      insoluble. Note also that the forall cannot be in an argument to a
 2946      type family, or that outer type family application would already have
 2947      been substituted away.
 2948 
 2949      However, we still must check to make sure that breakTyVarCycle_maybe actually
 2950      succeeds in getting rid of all occurrences of the offending variable. If
 2951      one is hidden under a forall, this won't be true. A similar problem can
 2952      happen if the variable appears only in a kind
 2953      (e.g. k ~ ... (a :: k) ...). So we perform an additional check after
 2954      performing the substitution. It is tiresome to re-run all of checkTyVarEq
 2955      here, but reimplementing just the occurs-check is even more tiresome.
 2956 
 2957      Skipping this check causes typecheck/should_fail/GivenForallLoop and
 2958      polykinds/T18451 to loop.
 2959 
 2960  (2) Our goal here is to avoid loops in rewriting. We can thus skip looking
 2961      in coercions, as we don't rewrite in coercions. (This is another reason
 2962      we need to re-check that we've gotten rid of all occurrences of the
 2963      offending variable.)
 2964 
 2965  (3) As we're substituting, we can build ill-kinded
 2966      types. For example, if we have Proxy (F a) b, where (b :: F a), then
 2967      replacing this with Proxy cbv b is ill-kinded. However, we will later
 2968      set cbv := F a, and so the zonked type will be well-kinded again.
 2969      The temporary ill-kinded type hurts no one, and avoiding this would
 2970      be quite painfully difficult.
 2971 
 2972      Specifically, this detail does not contravene the Purely Kinded Type Invariant
 2973      (Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType).
 2974      The PKTI says that we can call typeKind on any type, without failure.
 2975      It would be violated if we, say, replaced a kind (a -> b) with a kind c,
 2976      because an arrow kind might be consulted in piResultTys. Here, we are
 2977      replacing one opaque type like (F a b c) with another, cbv (opaque in
 2978      that we never assume anything about its structure, like that it has a
 2979      result type or a RuntimeRep argument).
 2980 
 2981  (4) The evidence for the produced Givens is all just reflexive, because
 2982      we will eventually set the cycle-breaker variable to be the type family,
 2983      and then, after the zonk, all will be well.
 2984 
 2985  (5) The approach here is inefficient. For instance, we could choose to
 2986      affect only type family applications that mention the offending variable:
 2987      in a ~ (F b, G a), we need to replace only G a, not F b. Furthermore,
 2988      we could try to detect cases like a ~ (F a, F a) and use the same
 2989      tyvar to replace F a. (Cf.
 2990      Note [Flattening type-family applications when matching instances]
 2991      in GHC.Core.Unify, which
 2992      goes to this extra effort.) There may be other opportunities for
 2993      improvement. However, this is really a very small corner case.
 2994      The investment to craft a clever,
 2995      performant solution seems unworthwhile.
 2996 
 2997  (6) We often get the predicate associated with a constraint from its
 2998      evidence. We thus must not only make sure the generated CEqCan's
 2999      fields have the updated RHS type, but we must also update the
 3000      evidence itself. This is done by the call to rewriteEqEvidence
 3001      in canEqCanLHSFinish.
 3002 
 3003  (7) We don't wish to apply this magic on the equalities created
 3004      by this very same process.
 3005      Consider this, from typecheck/should_compile/ContextStack2:
 3006 
 3007        type instance TF (a, b) = (TF a, TF b)
 3008        t :: (a ~ TF (a, Int)) => ...
 3009 
 3010        [G] a ~ TF (a, Int)
 3011 
 3012      The RHS reduces, so we get
 3013 
 3014        [G] a ~ (TF a, TF Int)
 3015 
 3016      We then break cycles, to get
 3017 
 3018        [G] g1 :: a ~ (cbv1, cbv2)
 3019        [G] g2 :: TF a ~ cbv1
 3020        [G] g3 :: TF Int ~ cbv2
 3021 
 3022      g1 gets added to the inert set, as written. But then g2 becomes
 3023      the work item. g1 rewrites g2 to become
 3024 
 3025        [G] TF (cbv1, cbv2) ~ cbv1
 3026 
 3027      which then uses the type instance to become
 3028 
 3029        [G] (TF cbv1, TF cbv2) ~ cbv1
 3030 
 3031      which looks remarkably like the Given we started with. If left
 3032      unchecked, this will end up breaking cycles again, looping ad
 3033      infinitum (and resulting in a context-stack reduction error,
 3034      not an outright loop). The solution is easy: don't break cycles
 3035      on an equality generated by breaking cycles. Instead, we mark this
 3036      final Given as a CIrredCan with a NonCanonicalReason with the soluble
 3037      occurs-check bit set (only).
 3038 
 3039      We track these equalities by giving them a special CtOrigin,
 3040      CycleBreakerOrigin. This works for both Givens and WDs, as
 3041      we need the logic in the WD case for e.g. typecheck/should_fail/T17139.
 3042 
 3043  (8) We really want to do this all only when there is a soluble occurs-check
 3044      failure, not when other problems arise (such as an impredicative
 3045      equality like alpha ~ forall a. a -> a). That is why breakTyVarCycle_maybe
 3046      uses cterHasOnlyProblem when looking at the result of checkTypeEq, which
 3047      checks for many of the invariants on a CEqCan.
 3048 -}
 3049 
 3050 {-
 3051 ************************************************************************
 3052 *                                                                      *
 3053                   Evidence transformation
 3054 *                                                                      *
 3055 ************************************************************************
 3056 -}
 3057 
 3058 data StopOrContinue a
 3059   = ContinueWith a    -- The constraint was not solved, although it may have
 3060                       --   been rewritten
 3061 
 3062   | Stop CtEvidence   -- The (rewritten) constraint was solved
 3063          SDoc         -- Tells how it was solved
 3064                       -- Any new sub-goals have been put on the work list
 3065   deriving (Functor)
 3066 
 3067 instance Outputable a => Outputable (StopOrContinue a) where
 3068   ppr (Stop ev s)      = text "Stop" <> parens s <+> ppr ev
 3069   ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
 3070 
 3071 continueWith :: a -> TcS (StopOrContinue a)
 3072 continueWith = return . ContinueWith
 3073 
 3074 stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
 3075 stopWith ev s = return (Stop ev (text s))
 3076 
 3077 andWhenContinue :: TcS (StopOrContinue a)
 3078                 -> (a -> TcS (StopOrContinue b))
 3079                 -> TcS (StopOrContinue b)
 3080 andWhenContinue tcs1 tcs2
 3081   = do { r <- tcs1
 3082        ; case r of
 3083            Stop ev s       -> return (Stop ev s)
 3084            ContinueWith ct -> tcs2 ct }
 3085 infixr 0 `andWhenContinue`    -- allow chaining with ($)
 3086 
 3087 rewriteEvidence :: CtEvidence   -- ^ old evidence
 3088                 -> Reduction    -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
 3089                 -> TcS (StopOrContinue CtEvidence)
 3090 -- Returns Just new_ev iff either (i)  'co' is reflexivity
 3091 --                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
 3092 -- In either case, there is nothing new to do with new_ev
 3093 {-
 3094      rewriteEvidence old_ev new_pred co
 3095 Main purpose: create new evidence for new_pred;
 3096               unless new_pred is cached already
 3097 * Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
 3098 * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
 3099 * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
 3100 * Returns Nothing if new_ev is already cached
 3101 
 3102         Old evidence    New predicate is               Return new evidence
 3103         flavour                                        of same flavor
 3104         -------------------------------------------------------------------
 3105         Wanted          Already solved or in inert     Nothing
 3106         or Derived      Not                            Just new_evidence
 3107 
 3108         Given           Already in inert               Nothing
 3109                         Not                            Just new_evidence
 3110 
 3111 Note [Rewriting with Refl]
 3112 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 3113 If the coercion is just reflexivity then you may re-use the same
 3114 variable.  But be careful!  Although the coercion is Refl, new_pred
 3115 may reflect the result of unification alpha := ty, so new_pred might
 3116 not _look_ the same as old_pred, and it's vital to proceed from now on
 3117 using new_pred.
 3118 
 3119 The rewriter preserves type synonyms, so they should appear in new_pred
 3120 as well as in old_pred; that is important for good error messages.
 3121  -}
 3122 
 3123 
 3124 rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred)
 3125   = -- If derived, don't even look at the coercion.
 3126     -- This is very important, DO NOT re-order the equations for
 3127     -- rewriteEvidence to put the isTcReflCo test first!
 3128     -- Why?  Because for *Derived* constraints, c, the coercion, which
 3129     -- was produced by rewriting, may contain suspended calls to
 3130     -- (ctEvExpr c), which fails for Derived constraints.
 3131     -- (Getting this wrong caused #7384.)
 3132     continueWith (old_ev { ctev_pred = new_pred })
 3133 
 3134 rewriteEvidence old_ev (Reduction co new_pred)
 3135   | isTcReflCo co -- See Note [Rewriting with Refl]
 3136   = continueWith (old_ev { ctev_pred = new_pred })
 3137 
 3138 rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred)
 3139   = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
 3140        ; continueWith new_ev }
 3141   where
 3142     -- mkEvCast optimises ReflCo
 3143     new_tm = mkEvCast (evId old_evar)
 3144                 (tcDowngradeRole Representational (ctEvRole ev) co)
 3145 
 3146 rewriteEvidence ev@(CtWanted { ctev_dest = dest
 3147                              , ctev_nosh = si
 3148                              , ctev_loc = loc }) (Reduction co new_pred)
 3149   = do { mb_new_ev <- newWanted_SI si loc new_pred
 3150                -- The "_SI" variant ensures that we make a new Wanted
 3151                -- with the same shadow-info as the existing one (#16735)
 3152        ; massert (tcCoercionRole co == ctEvRole ev)
 3153        ; setWantedEvTerm dest
 3154             (mkEvCast (getEvExpr mb_new_ev)
 3155                       (tcDowngradeRole Representational (ctEvRole ev) (mkSymCo co)))
 3156        ; case mb_new_ev of
 3157             Fresh  new_ev -> continueWith new_ev
 3158             Cached _      -> stopWith ev "Cached wanted" }
 3159 
 3160 
 3161 rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
 3162                                         --              or orhs ~ olhs (swapped)
 3163                   -> SwapFlag
 3164                   -> Reduction          -- lhs_co :: olhs ~ nlhs
 3165                   -> Reduction          -- rhs_co :: orhs ~ nrhs
 3166                   -> TcS CtEvidence     -- Of type nlhs ~ nrhs
 3167 -- With reductions (Reduction lhs_co nlhs) (Reduction rhs_co nrhs),
 3168 -- rewriteEqEvidence yields, for a given equality (Given g olhs orhs):
 3169 -- If not swapped
 3170 --      g1 : nlhs ~ nrhs = sym lhs_co ; g ; rhs_co
 3171 -- If swapped
 3172 --      g1 : nlhs ~ nrhs = sym lhs_co ; Sym g ; rhs_co
 3173 --
 3174 -- For a wanted equality (Wanted w), we do the dual thing:
 3175 -- New  w1 : nlhs ~ nrhs
 3176 -- If not swapped
 3177 --      w : olhs ~ orhs = lhs_co ; w1 ; sym rhs_co
 3178 -- If swapped
 3179 --      w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co
 3180 --
 3181 -- It's all a form of rewriteEvidence, specialised for equalities
 3182 rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs)
 3183   | CtDerived {} <- old_ev  -- Don't force the evidence for a Derived
 3184   = return (old_ev { ctev_pred = new_pred })
 3185 
 3186   | NotSwapped <- swapped
 3187   , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
 3188   , isTcReflCo rhs_co
 3189   = return (old_ev { ctev_pred = new_pred })
 3190 
 3191   | CtGiven { ctev_evar = old_evar } <- old_ev
 3192   = do { let new_tm = evCoercion ( mkTcSymCo lhs_co
 3193                                   `mkTcTransCo` maybeTcSymCo swapped (mkTcCoVarCo old_evar)
 3194                                   `mkTcTransCo` rhs_co)
 3195        ; newGivenEvVar loc' (new_pred, new_tm) }
 3196 
 3197   | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev
 3198   = do { (new_ev, hole_co) <- newWantedEq_SI si loc'
 3199                                              (ctEvRole old_ev) nlhs nrhs
 3200                -- The "_SI" variant ensures that we make a new Wanted
 3201                -- with the same shadow-info as the existing one (#16735)
 3202        ; let co = maybeTcSymCo swapped $
 3203                   lhs_co
 3204                   `mkTransCo` hole_co
 3205                   `mkTransCo` mkTcSymCo rhs_co
 3206        ; setWantedEq dest co
 3207        ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
 3208        ; return new_ev }
 3209 
 3210 #if __GLASGOW_HASKELL__ <= 810
 3211   | otherwise
 3212   = panic "rewriteEvidence"
 3213 #endif
 3214   where
 3215     new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
 3216 
 3217       -- equality is like a type class. Bumping the depth is necessary because
 3218       -- of recursive newtypes, where "reducing" a newtype can actually make
 3219       -- it bigger. See Note [Newtypes can blow the stack].
 3220     loc      = ctEvLoc old_ev
 3221     loc'     = bumpCtLocDepth loc
 3222 
 3223 {-
 3224 ************************************************************************
 3225 *                                                                      *
 3226               Unification
 3227 *                                                                      *
 3228 ************************************************************************
 3229 
 3230 Note [unifyWanted and unifyDerived]
 3231 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 3232 When decomposing equalities we often create new wanted constraints for
 3233 (s ~ t).  But what if s=t?  Then it'd be faster to return Refl right away.
 3234 Similar remarks apply for Derived.
 3235 
 3236 Rather than making an equality test (which traverses the structure of the
 3237 type, perhaps fruitlessly), unifyWanted traverses the common structure, and
 3238 bales out when it finds a difference by creating a new Wanted constraint.
 3239 But where it succeeds in finding common structure, it just builds a coercion
 3240 to reflect it.
 3241 -}
 3242 
 3243 unifyWanted :: CtLoc -> Role
 3244             -> TcType -> TcType -> TcS Coercion
 3245 -- Return coercion witnessing the equality of the two types,
 3246 -- emitting new work equalities where necessary to achieve that
 3247 -- Very good short-cut when the two types are equal, or nearly so
 3248 -- See Note [unifyWanted and unifyDerived]
 3249 -- The returned coercion's role matches the input parameter
 3250 unifyWanted loc Phantom ty1 ty2
 3251   = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
 3252        ; return (mkPhantomCo kind_co ty1 ty2) }
 3253 
 3254 unifyWanted loc role orig_ty1 orig_ty2
 3255   = go orig_ty1 orig_ty2
 3256   where
 3257     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 3258     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 3259 
 3260     go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
 3261       = do { co_s <- unifyWanted loc role s1 s2
 3262            ; co_t <- unifyWanted loc role t1 t2
 3263            ; co_w <- unifyWanted loc Nominal w1 w2
 3264            ; return (mkFunCo role co_w co_s co_t) }
 3265     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 3266       | tc1 == tc2, tys1 `equalLength` tys2
 3267       , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
 3268       = do { cos <- zipWith3M (unifyWanted loc)
 3269                               (tyConRolesX role tc1) tys1 tys2
 3270            ; return (mkTyConAppCo role tc1 cos) }
 3271 
 3272     go ty1@(TyVarTy tv) ty2
 3273       = do { mb_ty <- isFilledMetaTyVar_maybe tv
 3274            ; case mb_ty of
 3275                 Just ty1' -> go ty1' ty2
 3276                 Nothing   -> bale_out ty1 ty2}
 3277     go ty1 ty2@(TyVarTy tv)
 3278       = do { mb_ty <- isFilledMetaTyVar_maybe tv
 3279            ; case mb_ty of
 3280                 Just ty2' -> go ty1 ty2'
 3281                 Nothing   -> bale_out ty1 ty2 }
 3282 
 3283     go ty1@(CoercionTy {}) (CoercionTy {})
 3284       = return (mkReflCo role ty1) -- we just don't care about coercions!
 3285 
 3286     go ty1 ty2 = bale_out ty1 ty2
 3287 
 3288     bale_out ty1 ty2
 3289        | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1)
 3290         -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
 3291        | otherwise = emitNewWantedEq loc role orig_ty1 orig_ty2
 3292 
 3293 unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
 3294 -- See Note [unifyWanted and unifyDerived]
 3295 unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2
 3296 
 3297 unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS ()
 3298 -- See Note [unifyWanted and unifyDerived]
 3299 unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2
 3300 
 3301 unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS ()
 3302 -- Create new Derived and put it in the work list
 3303 -- Should do nothing if the two types are equal
 3304 -- See Note [unifyWanted and unifyDerived]
 3305 unify_derived _   Phantom _        _        = return ()
 3306 unify_derived loc role    orig_ty1 orig_ty2
 3307   = go orig_ty1 orig_ty2
 3308   where
 3309     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
 3310     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 3311 
 3312     go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
 3313       = do { unify_derived loc role s1 s2
 3314            ; unify_derived loc role t1 t2
 3315            ; unify_derived loc Nominal w1 w2 }
 3316     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 3317       | tc1 == tc2, tys1 `equalLength` tys2
 3318       , isInjectiveTyCon tc1 role
 3319       = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2
 3320     go ty1@(TyVarTy tv) ty2
 3321       = do { mb_ty <- isFilledMetaTyVar_maybe tv
 3322            ; case mb_ty of
 3323                 Just ty1' -> go ty1' ty2
 3324                 Nothing   -> bale_out ty1 ty2 }
 3325     go ty1 ty2@(TyVarTy tv)
 3326       = do { mb_ty <- isFilledMetaTyVar_maybe tv
 3327            ; case mb_ty of
 3328                 Just ty2' -> go ty1 ty2'
 3329                 Nothing   -> bale_out ty1 ty2 }
 3330     go ty1 ty2 = bale_out ty1 ty2
 3331 
 3332     bale_out ty1 ty2
 3333        | ty1 `tcEqType` ty2 = return ()
 3334         -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
 3335        | otherwise = emitNewDerivedEq loc role orig_ty1 orig_ty2