never executed always true always false
    1 {-# LANGUAGE ScopedTypeVariables #-}
    2 {-# LANGUAGE TupleSections       #-}
    3 
    4 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
    5 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    6 
    7 {-
    8 (c) The University of Glasgow 2006
    9 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   10 -}
   11 
   12 -- | Type subsumption and unification
   13 module GHC.Tc.Utils.Unify (
   14   -- Full-blown subsumption
   15   tcWrapResult, tcWrapResultO, tcWrapResultMono,
   16   tcSkolemise, tcSkolemiseScoped, tcSkolemiseET,
   17   tcSubType, tcSubTypeSigma, tcSubTypePat,
   18   tcSubMult,
   19   checkConstraints, checkTvConstraints,
   20   buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
   21 
   22   -- Various unifications
   23   unifyType, unifyKind, unifyExpectedType,
   24   uType, promoteTcType,
   25   swapOverTyVars, canSolveByUnification,
   26 
   27   --------------------------------
   28   -- Holes
   29   tcInfer,
   30   matchExpectedListTy,
   31   matchExpectedTyConApp,
   32   matchExpectedAppTy,
   33   matchExpectedFunTys,
   34   matchExpectedFunKind,
   35   matchActualFunTySigma, matchActualFunTysRho,
   36 
   37   checkTyVarEq, checkTyFamEq, checkTypeEq
   38 
   39   ) where
   40 
   41 import GHC.Prelude
   42 
   43 import GHC.Hs
   44 import GHC.Core.TyCo.Rep
   45 import GHC.Core.TyCo.Ppr( debugPprType )
   46 import GHC.Tc.Utils.Concrete ( mkWpFun )
   47 import GHC.Tc.Utils.Env
   48 import GHC.Tc.Utils.Instantiate
   49 import GHC.Tc.Utils.Monad
   50 import GHC.Tc.Utils.TcMType
   51 import GHC.Tc.Utils.TcType
   52 
   53 
   54 import GHC.Core.Type
   55 import GHC.Core.Coercion
   56 import GHC.Core.Multiplicity
   57 
   58 import GHC.Tc.Types.Evidence
   59 import GHC.Tc.Types.Constraint
   60 import GHC.Tc.Types.Origin
   61 import GHC.Types.Name( isSystemName )
   62 
   63 import GHC.Core.TyCon
   64 import GHC.Builtin.Types
   65 import GHC.Types.Var as Var
   66 import GHC.Types.Var.Set
   67 import GHC.Types.Var.Env
   68 import GHC.Utils.Error
   69 import GHC.Driver.Session
   70 import GHC.Types.Basic
   71 import GHC.Data.Bag
   72 import GHC.Utils.Misc
   73 import GHC.Utils.Outputable as Outputable
   74 import GHC.Utils.Panic
   75 import GHC.Utils.Panic.Plain
   76 
   77 import GHC.Exts      ( inline )
   78 import Control.Monad
   79 import Control.Arrow ( second )
   80 import qualified Data.Semigroup as S ( (<>) )
   81 
   82 {- *********************************************************************
   83 *                                                                      *
   84               matchActualFunTys
   85 *                                                                      *
   86 ********************************************************************* -}
   87 
   88 -- | matchActualFunTySigma does looks for just one function arrow
   89 --   returning an uninstantiated sigma-type
   90 matchActualFunTySigma
   91   :: SDoc -- See Note [Herald for matchExpectedFunTys]
   92   -> Maybe SDoc                    -- The thing with type TcSigmaType
   93   -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and
   94                                    -- types of values args to which function has
   95                                    --   been applied already (reversed)
   96                                    -- Both are used only for error messages)
   97   -> TcRhoType                     -- Type to analyse: a TcRhoType
   98   -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
   99 -- The /argument/ is a RhoType
  100 -- The /result/   is an (uninstantiated) SigmaType
  101 --
  102 -- See Note [matchActualFunTy error handling] for the first three arguments
  103 
  104 -- If   (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty
  105 -- then wrap :: fun_ty ~> (arg_ty -> res_ty)
  106 -- and NB: res_ty is an (uninstantiated) SigmaType
  107 
  108 matchActualFunTySigma herald mb_thing err_info fun_ty
  109   = assertPpr (isRhoTy fun_ty) (ppr fun_ty) $
  110     go fun_ty
  111   where
  112     -- Does not allocate unnecessary meta variables: if the input already is
  113     -- a function, we just take it apart.  Not only is this efficient,
  114     -- it's important for higher rank: the argument might be of form
  115     --              (forall a. ty) -> other
  116     -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
  117     -- hide the forall inside a meta-variable
  118     go :: TcRhoType   -- The type we're processing, perhaps after
  119                       -- expanding any type synonym
  120        -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
  121     go ty | Just ty' <- tcView ty = go ty'
  122 
  123     go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
  124       = assert (af == VisArg) $
  125         return (idHsWrapper, Scaled w arg_ty, res_ty)
  126 
  127     go ty@(TyVarTy tv)
  128       | isMetaTyVar tv
  129       = do { cts <- readMetaTyVar tv
  130            ; case cts of
  131                Indirect ty' -> go ty'
  132                Flexi        -> defer ty }
  133 
  134        -- In all other cases we bale out into ordinary unification
  135        -- However unlike the meta-tyvar case, we are sure that the
  136        -- number of arguments doesn't match arity of the original
  137        -- type, so we can add a bit more context to the error message
  138        -- (cf #7869).
  139        --
  140        -- It is not always an error, because specialized type may have
  141        -- different arity, for example:
  142        --
  143        -- > f1 = f2 'a'
  144        -- > f2 :: Monad m => m Bool
  145        -- > f2 = undefined
  146        --
  147        -- But in that case we add specialized type into error context
  148        -- anyway, because it may be useful. See also #9605.
  149     go ty = addErrCtxtM (mk_ctxt ty) (defer ty)
  150 
  151     ------------
  152     defer fun_ty
  153       = do { arg_ty <- newOpenFlexiTyVarTy
  154            ; res_ty <- newOpenFlexiTyVarTy
  155            ; mult <- newFlexiTyVarTy multiplicityTy
  156            ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty
  157            ; co <- unifyType mb_thing fun_ty unif_fun_ty
  158            ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) }
  159 
  160     ------------
  161     mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
  162     mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far)
  163                                      res_ty n_val_args_in_call
  164     (n_val_args_in_call, arg_tys_so_far) = err_info
  165 
  166 {- Note [matchActualFunTy error handling]
  167 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  168 matchActualFunTySigma is made much more complicated by the
  169 desire to produce good error messages. Consider the application
  170     f @Int x y
  171 In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments,
  172 and then call matchActualFunTysPart for each individual value
  173 argument. It, in turn, must instantiate any type/dictionary args,
  174 before looking for an arrow type.
  175 
  176 But if it doesn't find an arrow type, it wants to generate a message
  177 like "f is applied to two arguments but its type only has one".
  178 To do that, it needs to know about the args that tcArgs has already
  179 munched up -- hence passing in n_val_args_in_call and arg_tys_so_far;
  180 and hence also the accumulating so_far arg to 'go'.
  181 
  182 This allows us (in mk_ctxt) to construct f's /instantiated/ type,
  183 with just the values-arg arrows, which is what we really want
  184 in the error message.
  185 
  186 Ugh!
  187 -}
  188 
  189 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
  190 -- for example in function application
  191 matchActualFunTysRho :: SDoc   -- See Note [Herald for matchExpectedFunTys]
  192                      -> CtOrigin
  193                      -> Maybe SDoc  -- the thing with type TcSigmaType
  194                      -> Arity
  195                      -> TcSigmaType
  196                      -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType)
  197 -- If    matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty)
  198 -- then  wrap : ty ~> (t1 -> ... -> tn -> res_ty)
  199 --       and res_ty is a RhoType
  200 -- NB: the returned type is top-instantiated; it's a RhoType
  201 matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
  202   = go n_val_args_wanted [] fun_ty
  203   where
  204     go n so_far fun_ty
  205       | not (isRhoTy fun_ty)
  206       = do { (wrap1, rho) <- topInstantiate ct_orig fun_ty
  207            ; (wrap2, arg_tys, res_ty) <- go n so_far rho
  208            ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
  209 
  210     go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
  211 
  212     go n so_far fun_ty
  213       = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma
  214                                                  herald mb_thing
  215                                                  (n_val_args_wanted, so_far)
  216                                                  fun_ty
  217            ; (wrap_res, arg_tys, res_ty)   <- go (n-1) (arg_ty1:so_far) res_ty1
  218            ; wrap_fun2 <- mkWpFun idHsWrapper wrap_res arg_ty1 res_ty (WpFunFunTy fun_ty)
  219            ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
  220 
  221 {-
  222 ************************************************************************
  223 *                                                                      *
  224              matchExpected functions
  225 *                                                                      *
  226 ************************************************************************
  227 
  228 Note [Herald for matchExpectedFunTys]
  229 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  230 The 'herald' always looks like:
  231    "The equation(s) for 'f' have"
  232    "The abstraction (\x.e) takes"
  233    "The section (+ x) expects"
  234    "The function 'f' is applied to"
  235 
  236 This is used to construct a message of form
  237 
  238    The abstraction `\Just 1 -> ...' takes two arguments
  239    but its type `Maybe a -> a' has only one
  240 
  241    The equation(s) for `f' have two arguments
  242    but its type `Maybe a -> a' has only one
  243 
  244    The section `(f 3)' requires 'f' to take two arguments
  245    but its type `Int -> Int' has only one
  246 
  247    The function 'f' is applied to two arguments
  248    but its type `Int -> Int' has only one
  249 
  250 When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the
  251 picture, we have a choice in deciding whether to count the type applications as
  252 proper arguments:
  253 
  254    The function 'f' is applied to one visible type argument
  255      and two value arguments
  256    but its type `forall a. a -> a` has only one visible type argument
  257      and one value argument
  258 
  259 Or whether to include the type applications as part of the herald itself:
  260 
  261    The expression 'f @Int' is applied to two arguments
  262    but its type `Int -> Int` has only one
  263 
  264 The latter is easier to implement and is arguably easier to understand, so we
  265 choose to implement that option.
  266 
  267 Note [matchExpectedFunTys]
  268 ~~~~~~~~~~~~~~~~~~~~~~~~~~
  269 matchExpectedFunTys checks that a sigma has the form
  270 of an n-ary function.  It passes the decomposed type to the
  271 thing_inside, and returns a wrapper to coerce between the two types
  272 
  273 It's used wherever a language construct must have a functional type,
  274 namely:
  275         A lambda expression
  276         A function definition
  277      An operator section
  278 
  279 This function must be written CPS'd because it needs to fill in the
  280 ExpTypes produced for arguments before it can fill in the ExpType
  281 passed in.
  282 
  283 -}
  284 
  285 -- Use this one when you have an "expected" type.
  286 -- This function skolemises at each polytype.
  287 matchExpectedFunTys :: forall a.
  288                        SDoc   -- See Note [Herald for matchExpectedFunTys]
  289                     -> UserTypeCtxt
  290                     -> Arity
  291                     -> ExpRhoType      -- Skolemised
  292                     -> ([Scaled ExpSigmaType] -> ExpRhoType -> TcM a)
  293                     -> TcM (HsWrapper, a)
  294 -- If    matchExpectedFunTys n ty = (_, wrap)
  295 -- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
  296 --   where [t1, ..., tn], ty_r are passed to the thing_inside
  297 matchExpectedFunTys herald ctx arity orig_ty thing_inside
  298   = case orig_ty of
  299       Check ty -> go [] arity ty
  300       _        -> defer [] arity orig_ty
  301   where
  302     -- Skolemise any foralls /before/ the zero-arg case
  303     -- so that we guarantee to return a rho-type
  304     go acc_arg_tys n ty
  305       | (tvs, theta, _) <- tcSplitSigmaTy ty
  306       , not (null tvs && null theta)
  307       = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' ->
  308                                                go acc_arg_tys n ty'
  309            ; return (wrap_gen <.> wrap_res, result) }
  310 
  311     -- No more args; do this /before/ tcView, so
  312     -- that we do not unnecessarily unwrap synonyms
  313     go acc_arg_tys 0 rho_ty
  314       = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType rho_ty)
  315            ; return (idHsWrapper, result) }
  316 
  317     go acc_arg_tys n ty
  318       | Just ty' <- tcView ty = go acc_arg_tys n ty'
  319 
  320     go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
  321       = assert (af == VisArg) $
  322         do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
  323                                       (n-1) res_ty
  324            ; fun_wrap <- mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty (WpFunFunExpTy orig_ty)
  325            ; return ( fun_wrap, result ) }
  326 
  327     go acc_arg_tys n ty@(TyVarTy tv)
  328       | isMetaTyVar tv
  329       = do { cts <- readMetaTyVar tv
  330            ; case cts of
  331                Indirect ty' -> go acc_arg_tys n ty'
  332                Flexi        -> defer acc_arg_tys n (mkCheckExpType ty) }
  333 
  334        -- In all other cases we bale out into ordinary unification
  335        -- However unlike the meta-tyvar case, we are sure that the
  336        -- number of arguments doesn't match arity of the original
  337        -- type, so we can add a bit more context to the error message
  338        -- (cf #7869).
  339        --
  340        -- It is not always an error, because specialized type may have
  341        -- different arity, for example:
  342        --
  343        -- > f1 = f2 'a'
  344        -- > f2 :: Monad m => m Bool
  345        -- > f2 = undefined
  346        --
  347        -- But in that case we add specialized type into error context
  348        -- anyway, because it may be useful. See also #9605.
  349     go acc_arg_tys n ty = addErrCtxtM (mk_ctxt acc_arg_tys ty) $
  350                           defer acc_arg_tys n (mkCheckExpType ty)
  351 
  352     ------------
  353     defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
  354     defer acc_arg_tys n fun_ty
  355       = do { more_arg_tys <- replicateM n (mkScaled <$> newFlexiTyVarTy multiplicityTy <*> newInferExpType)
  356            ; res_ty       <- newInferExpType
  357            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
  358            ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
  359            ; res_ty       <- readExpType res_ty
  360            ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
  361            ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty
  362                          -- Not a good origin at all :-(
  363            ; return (wrap, result) }
  364 
  365     ------------
  366     mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
  367     mk_ctxt arg_tys res_ty env
  368       = mkFunTysMsg env herald arg_tys' res_ty arity
  369       where
  370         arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $
  371                    reverse arg_tys
  372             -- this is safe b/c we're called from "go"
  373 
  374 mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity
  375             -> TcM (TidyEnv, SDoc)
  376 mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
  377   = do { (env', fun_rho) <- zonkTidyTcType env $
  378                             mkVisFunTys arg_tys res_ty
  379 
  380        ; let (all_arg_tys, _) = splitFunTys fun_rho
  381              n_fun_args = length all_arg_tys
  382 
  383              msg | n_val_args_in_call <= n_fun_args  -- Enough args, in the end
  384                  = text "In the result of a function call"
  385                  | otherwise
  386                  = hang (full_herald <> comma)
  387                       2 (sep [ text "but its type" <+> quotes (pprType fun_rho)
  388                              , if n_fun_args == 0 then text "has none"
  389                                else text "has only" <+> speakN n_fun_args])
  390 
  391        ; return (env', msg) }
  392  where
  393   full_herald = herald <+> speakNOf n_val_args_in_call (text "value argument")
  394 
  395 ----------------------
  396 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
  397 -- Special case for lists
  398 matchExpectedListTy exp_ty
  399  = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
  400       ; return (co, elt_ty) }
  401 
  402 ---------------------
  403 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
  404                       -> TcRhoType            -- orig_ty
  405                       -> TcM (TcCoercionN,    -- T k1 k2 k3 a b c ~N orig_ty
  406                               [TcSigmaType])  -- Element types, k1 k2 k3 a b c
  407 
  408 -- It's used for wired-in tycons, so we call checkWiredInTyCon
  409 -- Precondition: never called with FunTyCon
  410 -- Precondition: input type :: *
  411 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
  412 
  413 matchExpectedTyConApp tc orig_ty
  414   = assert (not $ isFunTyCon tc) $ go orig_ty
  415   where
  416     go ty
  417        | Just ty' <- tcView ty
  418        = go ty'
  419 
  420     go ty@(TyConApp tycon args)
  421        | tc == tycon  -- Common case
  422        = return (mkTcNomReflCo ty, args)
  423 
  424     go (TyVarTy tv)
  425        | isMetaTyVar tv
  426        = do { cts <- readMetaTyVar tv
  427             ; case cts of
  428                 Indirect ty -> go ty
  429                 Flexi       -> defer }
  430 
  431     go _ = defer
  432 
  433     -- If the common case does not occur, instantiate a template
  434     -- T k1 .. kn t1 .. tm, and unify with the original type
  435     -- Doing it this way ensures that the types we return are
  436     -- kind-compatible with T.  For example, suppose we have
  437     --       matchExpectedTyConApp T (f Maybe)
  438     -- where data T a = MkT a
  439     -- Then we don't want to instantiate T's data constructors with
  440     --    (a::*) ~ Maybe
  441     -- because that'll make types that are utterly ill-kinded.
  442     -- This happened in #7368
  443     defer
  444       = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
  445            ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
  446            ; let args = mkTyVarTys arg_tvs
  447                  tc_template = mkTyConApp tc args
  448            ; co <- unifyType Nothing tc_template orig_ty
  449            ; return (co, args) }
  450 
  451 ----------------------
  452 matchExpectedAppTy :: TcRhoType                         -- orig_ty
  453                    -> TcM (TcCoercion,                   -- m a ~N orig_ty
  454                            (TcSigmaType, TcSigmaType))  -- Returns m, a
  455 -- If the incoming type is a mutable type variable of kind k, then
  456 -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
  457 
  458 matchExpectedAppTy orig_ty
  459   = go orig_ty
  460   where
  461     go ty
  462       | Just ty' <- tcView ty = go ty'
  463 
  464       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
  465       = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
  466 
  467     go (TyVarTy tv)
  468       | isMetaTyVar tv
  469       = do { cts <- readMetaTyVar tv
  470            ; case cts of
  471                Indirect ty -> go ty
  472                Flexi       -> defer }
  473 
  474     go _ = defer
  475 
  476     -- Defer splitting by generating an equality constraint
  477     defer
  478       = do { ty1 <- newFlexiTyVarTy kind1
  479            ; ty2 <- newFlexiTyVarTy kind2
  480            ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
  481            ; return (co, (ty1, ty2)) }
  482 
  483     orig_kind = tcTypeKind orig_ty
  484     kind1 = mkVisFunTyMany liftedTypeKind orig_kind
  485     kind2 = liftedTypeKind    -- m :: * -> k
  486                               -- arg type :: *
  487 
  488 {-
  489 ************************************************************************
  490 *                                                                      *
  491                 Subsumption checking
  492 *                                                                      *
  493 ************************************************************************
  494 
  495 Note [Subsumption checking: tcSubType]
  496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  497 All the tcSubType calls have the form
  498                 tcSubType actual_ty expected_ty
  499 which checks
  500                 actual_ty <= expected_ty
  501 
  502 That is, that a value of type actual_ty is acceptable in
  503 a place expecting a value of type expected_ty.  I.e. that
  504 
  505     actual ty   is more polymorphic than   expected_ty
  506 
  507 It returns a wrapper function
  508         co_fn :: actual_ty ~ expected_ty
  509 which takes an HsExpr of type actual_ty into one of type
  510 expected_ty.
  511 -}
  512 
  513 
  514 -----------------
  515 -- tcWrapResult needs both un-type-checked (for origins and error messages)
  516 -- and type-checked (for wrapping) expressions
  517 tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
  518              -> TcM (HsExpr GhcTc)
  519 tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
  520 
  521 tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
  522                -> TcM (HsExpr GhcTc)
  523 tcWrapResultO orig rn_expr expr actual_ty res_ty
  524   = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
  525                                       , text "Expected:" <+> ppr res_ty ])
  526        ; wrap <- tcSubTypeNC orig GenSigCtxt (Just (ppr rn_expr)) actual_ty res_ty
  527        ; return (mkHsWrap wrap expr) }
  528 
  529 tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
  530                  -> TcRhoType   -- Actual -- a rho-type not a sigma-type
  531                  -> ExpRhoType  -- Expected
  532                  -> TcM (HsExpr GhcTc)
  533 -- A version of tcWrapResult to use when the actual type is a
  534 -- rho-type, so nothing to instantiate; just go straight to unify.
  535 -- It means we don't need to pass in a CtOrigin
  536 tcWrapResultMono rn_expr expr act_ty res_ty
  537   = assertPpr (isRhoTy act_ty) (ppr act_ty $$ ppr rn_expr) $
  538     do { co <- unifyExpectedType rn_expr act_ty res_ty
  539        ; return (mkHsWrapCo co expr) }
  540 
  541 unifyExpectedType :: HsExpr GhcRn
  542                   -> TcRhoType   -- Actual -- a rho-type not a sigma-type
  543                   -> ExpRhoType  -- Expected
  544                   -> TcM TcCoercionN
  545 unifyExpectedType rn_expr act_ty exp_ty
  546   = case exp_ty of
  547       Infer inf_res -> fillInferResult act_ty inf_res
  548       Check exp_ty  -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
  549 
  550 ------------------------
  551 tcSubTypePat :: CtOrigin -> UserTypeCtxt
  552             -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
  553 -- Used in patterns; polarity is backwards compared
  554 --   to tcSubType
  555 -- If wrap = tc_sub_type_et t1 t2
  556 --    => wrap :: t1 ~> t2
  557 tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
  558   = do { dflags <- getDynFlags
  559        ; tc_sub_type dflags unifyTypeET inst_orig ctxt ty_actual ty_expected }
  560 
  561 tcSubTypePat _ _ (Infer inf_res) ty_expected
  562   = do { co <- fillInferResult ty_expected inf_res
  563                -- In patterns we do not instantatiate
  564 
  565        ; return (mkWpCastN (mkTcSymCo co)) }
  566 
  567 ---------------
  568 tcSubType :: CtOrigin -> UserTypeCtxt
  569           -> TcSigmaType  -- Actual
  570           -> ExpRhoType   -- Expected
  571           -> TcM HsWrapper
  572 -- Checks that 'actual' is more polymorphic than 'expected'
  573 tcSubType orig ctxt ty_actual ty_expected
  574   = addSubTypeCtxt ty_actual ty_expected $
  575     do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
  576        ; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected }
  577 
  578 tcSubTypeNC :: CtOrigin       -- Used when instantiating
  579             -> UserTypeCtxt   -- Used when skolemising
  580             -> Maybe SDoc     -- The expression that has type 'actual' (if known)
  581             -> TcSigmaType            -- Actual type
  582             -> ExpRhoType             -- Expected type
  583             -> TcM HsWrapper
  584 tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
  585   = case res_ty of
  586       Check ty_expected -> do { dflags <- getDynFlags
  587                               ; tc_sub_type dflags (unifyType m_thing) inst_orig ctxt
  588                                             ty_actual ty_expected }
  589 
  590       Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
  591                                    -- See Note [Instantiation of InferResult]
  592                           ; co <- fillInferResult rho inf_res
  593                           ; return (mkWpCastN co <.> wrap) }
  594 
  595 {- Note [Instantiation of InferResult]
  596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  597 We now always instantiate before filling in InferResult, so that
  598 the result is a TcRhoType: see #17173 for discussion.
  599 
  600 For example:
  601 
  602 1. Consider
  603     f x = (*)
  604    We want to instantiate the type of (*) before returning, else we
  605    will infer the type
  606      f :: forall {a}. a -> forall b. Num b => b -> b -> b
  607    This is surely confusing for users.
  608 
  609    And worse, the monomorphism restriction won't work properly. The MR is
  610    dealt with in simplifyInfer, and simplifyInfer has no way of
  611    instantiating. This could perhaps be worked around, but it may be
  612    hard to know even when instantiation should happen.
  613 
  614 2. Another reason.  Consider
  615        f :: (?x :: Int) => a -> a
  616        g y = let ?x = 3::Int in f
  617    Here want to instantiate f's type so that the ?x::Int constraint
  618    gets discharged by the enclosing implicit-parameter binding.
  619 
  620 3. Suppose one defines plus = (+). If we instantiate lazily, we will
  621    infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
  622    restriction compels us to infer
  623       plus :: Integer -> Integer -> Integer
  624    (or similar monotype). Indeed, the only way to know whether to apply
  625    the monomorphism restriction at all is to instantiate
  626 
  627 There is one place where we don't want to instantiate eagerly,
  628 namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
  629 command. See Note [Implementing :type] in GHC.Tc.Module.
  630 -}
  631 
  632 ---------------
  633 tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
  634 -- External entry point, but no ExpTypes on either side
  635 -- Checks that actual <= expected
  636 -- Returns HsWrapper :: actual ~ expected
  637 tcSubTypeSigma ctxt ty_actual ty_expected
  638   = do { dflags <- getDynFlags
  639        ; tc_sub_type dflags (unifyType Nothing) eq_orig ctxt ty_actual ty_expected }
  640   where
  641     eq_orig = TypeEqOrigin { uo_actual   = ty_actual
  642                            , uo_expected = ty_expected
  643                            , uo_thing    = Nothing
  644                            , uo_visible  = True }
  645 
  646 ---------------
  647 tc_sub_type :: DynFlags
  648             -> (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
  649             -> CtOrigin       -- Used when instantiating
  650             -> UserTypeCtxt   -- Used when skolemising
  651             -> TcSigmaType    -- Actual; a sigma-type
  652             -> TcSigmaType    -- Expected; also a sigma-type
  653             -> TcM HsWrapper
  654 -- Checks that actual_ty is more polymorphic than expected_ty
  655 -- If wrap = tc_sub_type t1 t2
  656 --    => wrap :: t1 ~> t2
  657 tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected
  658   | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
  659   , not (possibly_poly ty_actual)
  660   = do { traceTc "tc_sub_type (drop to equality)" $
  661          vcat [ text "ty_actual   =" <+> ppr ty_actual
  662               , text "ty_expected =" <+> ppr ty_expected ]
  663        ; mkWpCastN <$>
  664          unify ty_actual ty_expected }
  665 
  666   | otherwise   -- This is the general case
  667   = do { traceTc "tc_sub_type (general case)" $
  668          vcat [ text "ty_actual   =" <+> ppr ty_actual
  669               , text "ty_expected =" <+> ppr ty_expected ]
  670 
  671        ; (sk_wrap, inner_wrap)
  672            <- tcSkolemise ctxt ty_expected $ \ sk_rho ->
  673               do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
  674                  ; cow           <- unify rho_a sk_rho
  675                  ; return (mkWpCastN cow <.> wrap) }
  676 
  677        ; return (sk_wrap <.> inner_wrap) }
  678   where
  679     possibly_poly ty = not (isRhoTy ty)
  680 
  681     definitely_poly ty
  682       | (tvs, theta, tau) <- tcSplitSigmaTy ty
  683       , (tv:_) <- tvs
  684       , null theta
  685       , checkTyVarEq dflags tv tau `cterHasProblem` cteInsolubleOccurs
  686       = True
  687       | otherwise
  688       = False
  689 
  690 ------------------------
  691 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
  692 addSubTypeCtxt ty_actual ty_expected thing_inside
  693  | isRhoTy ty_actual        -- If there is no polymorphism involved, the
  694  , isRhoExpTy ty_expected   -- TypeEqOrigin stuff (added by the _NC functions)
  695  = thing_inside             -- gives enough context by itself
  696  | otherwise
  697  = addErrCtxtM mk_msg thing_inside
  698   where
  699     mk_msg tidy_env
  700       = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
  701                    -- might not be filled if we're debugging. ugh.
  702            ; mb_ty_expected          <- readExpType_maybe ty_expected
  703            ; (tidy_env, ty_expected) <- case mb_ty_expected of
  704                                           Just ty -> second mkCheckExpType <$>
  705                                                      zonkTidyTcType tidy_env ty
  706                                           Nothing -> return (tidy_env, ty_expected)
  707            ; ty_expected             <- readExpType ty_expected
  708            ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
  709            ; let msg = vcat [ hang (text "When checking that:")
  710                                  4 (ppr ty_actual)
  711                             , nest 2 (hang (text "is more polymorphic than:")
  712                                          2 (ppr ty_expected)) ]
  713            ; return (tidy_env, msg) }
  714 
  715 {- Note [Don't skolemise unnecessarily]
  716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  717 Suppose we are trying to solve
  718     (Char->Char) <= (forall a. a->a)
  719 We could skolemise the 'forall a', and then complain
  720 that (Char ~ a) is insoluble; but that's a pretty obscure
  721 error.  It's better to say that
  722     (Char->Char) ~ (forall a. a->a)
  723 fails.
  724 
  725 So roughly:
  726  * if the ty_expected has an outermost forall
  727       (i.e. skolemisation is the next thing we'd do)
  728  * and the ty_actual has no top-level polymorphism (but looking deeply)
  729 then we can revert to simple equality.  But we need to be careful.
  730 These examples are all fine:
  731 
  732  * (Char->Char) <= (forall a. Char -> Char)
  733       ty_expected isn't really polymorphic
  734 
  735  * (Char->Char) <= (forall a. (a~Char) => a -> a)
  736       ty_expected isn't really polymorphic
  737 
  738  * (Char->Char) <= (forall a. F [a] Char -> Char)
  739                    where type instance F [x] t = t
  740      ty_expected isn't really polymorphic
  741 
  742 If we prematurely go to equality we'll reject a program we should
  743 accept (e.g. #13752).  So the test (which is only to improve
  744 error message) is very conservative:
  745  * ty_actual is /definitely/ monomorphic
  746  * ty_expected is /definitely/ polymorphic
  747 
  748 Note [Settting the argument context]
  749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  750 Consider we are doing the ambiguity check for the (bogus)
  751   f :: (forall a b. C b => a -> a) -> Int
  752 
  753 We'll call
  754    tcSubType ((forall a b. C b => a->a) -> Int )
  755              ((forall a b. C b => a->a) -> Int )
  756 
  757 with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
  758 on the argument type of the (->) -- and at that point we want to switch
  759 to a UserTypeCtxt of GenSigCtxt.  Why?
  760 
  761 * Error messages.  If we stick with FunSigCtxt we get errors like
  762      * Could not deduce: C b
  763        from the context: C b0
  764         bound by the type signature for:
  765             f :: forall a b. C b => a->a
  766   But of course f does not have that type signature!
  767   Example tests: T10508, T7220a, Simple14
  768 
  769 * Implications. We may decide to build an implication for the whole
  770   ambiguity check, but we don't need one for each level within it,
  771   and GHC.Tc.Utils.Unify.alwaysBuildImplication checks the UserTypeCtxt.
  772   See Note [When to build an implication]
  773 
  774 Note [Wrapper returned from tcSubMult]
  775 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  776 There is no notion of multiplicity coercion in Core, therefore the wrapper
  777 returned by tcSubMult (and derived functions such as tcCheckUsage and
  778 checkManyPattern) is quite unlike any other wrapper: it checks whether the
  779 coercion produced by the constraint solver is trivial, producing a type error
  780 if it is not. This is implemented via the WpMultCoercion wrapper, as desugared
  781 by GHC.HsToCore.Binds.dsHsWrapper, which does the reflexivity check.
  782 
  783 This wrapper needs to be placed in the term; otherwise, checking of the
  784 eventual coercion won't be triggered during desugaring. But it can be put
  785 anywhere, since it doesn't affect the desugared code.
  786 
  787 Why do we check this in the desugarer? It's a convenient place, since it's
  788 right after all the constraints are solved. We need the constraints to be
  789 solved to check whether they are trivial or not.
  790 
  791 An alternative would be to have a kind of constraint which can
  792 only produce trivial evidence. This would allow such checks to happen
  793 in the constraint solver (#18756).
  794 This would be similar to the existing setup for Concrete, see
  795   Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete
  796     (PHASE 1 in particular).
  797 -}
  798 
  799 tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
  800 tcSubMult origin w_actual w_expected
  801   | Just (w1, w2) <- isMultMul w_actual =
  802   do { w1 <- tcSubMult origin w1 w_expected
  803      ; w2 <- tcSubMult origin w2 w_expected
  804      ; return (w1 <.> w2) }
  805   -- Currently, we consider p*q and sup p q to be equal.  Therefore, p*q <= r is
  806   -- equivalent to p <= r and q <= r.  For other cases, we approximate p <= q by p
  807   -- ~ q.  This is not complete, but it's sound. See also Note [Overapproximating
  808   -- multiplicities] in Multiplicity.
  809 tcSubMult origin w_actual w_expected =
  810   case submult w_actual w_expected of
  811     Submult -> return WpHole
  812     Unknown -> tcEqMult origin w_actual w_expected
  813 
  814 tcEqMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
  815 tcEqMult origin w_actual w_expected = do
  816   {
  817   -- Note that here we do not call to `submult`, so we check
  818   -- for strict equality.
  819   ; coercion <- uType TypeLevel origin w_actual w_expected
  820   ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
  821 
  822 
  823 {- *********************************************************************
  824 *                                                                      *
  825                     Generalisation
  826 *                                                                      *
  827 ********************************************************************* -}
  828 
  829 {- Note [Skolemisation]
  830 ~~~~~~~~~~~~~~~~~~~~~~~
  831 tcSkolemise takes "expected type" and strip off quantifiers to expose the
  832 type underneath, binding the new skolems for the 'thing_inside'
  833 The returned 'HsWrapper' has type (specific_ty -> expected_ty).
  834 
  835 Note that for a nested type like
  836    forall a. Eq a => forall b. Ord b => blah
  837 we still only build one implication constraint
  838    forall a b. (Eq a, Ord b) => <constraints>
  839 This is just an optimisation, but it's why we use topSkolemise to
  840 build the pieces from all the layers, before making a single call
  841 to checkConstraints.
  842 
  843 tcSkolemiseScoped is very similar, but differs in two ways:
  844 
  845 * It deals specially with just the outer forall, bringing those type
  846   variables into lexical scope.  To my surprise, I found that doing
  847   this unconditionally in tcSkolemise (i.e. doing it even if we don't
  848   need to bring the variables into lexical scope, which is harmless)
  849   caused a non-trivial (1%-ish) perf hit on the compiler.
  850 
  851 * It always calls checkConstraints, even if there are no skolem
  852   variables at all.  Reason: there might be nested deferred errors
  853   that must not be allowed to float to top level.
  854   See Note [When to build an implication] below.
  855 -}
  856 
  857 tcSkolemise, tcSkolemiseScoped
  858     :: UserTypeCtxt -> TcSigmaType
  859     -> (TcType -> TcM result)
  860     -> TcM (HsWrapper, result)
  861         -- ^ The wrapper has type: spec_ty ~> expected_ty
  862 -- See Note [Skolemisation] for the differences between
  863 -- tcSkolemiseScoped and tcSkolemise
  864 
  865 tcSkolemiseScoped ctxt expected_ty thing_inside
  866   = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
  867        ; let skol_tvs  = map snd tv_prs
  868              skol_info = SigSkol ctxt expected_ty tv_prs
  869 
  870        ; (ev_binds, res)
  871              <- checkConstraints skol_info skol_tvs given $
  872                 tcExtendNameTyVarEnv tv_prs               $
  873                 thing_inside rho_ty
  874 
  875        ; return (wrap <.> mkWpLet ev_binds, res) }
  876 
  877 tcSkolemise ctxt expected_ty thing_inside
  878   | isRhoTy expected_ty  -- Short cut for common case
  879   = do { res <- thing_inside expected_ty
  880        ; return (idHsWrapper, res) }
  881   | otherwise
  882   = do  { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
  883 
  884         ; let skol_tvs  = map snd tv_prs
  885               skol_info = SigSkol ctxt expected_ty tv_prs
  886 
  887         ; (ev_binds, result)
  888               <- checkConstraints skol_info skol_tvs given $
  889                  thing_inside rho_ty
  890 
  891         ; return (wrap <.> mkWpLet ev_binds, result) }
  892           -- The ev_binds returned by checkConstraints is very
  893           -- often empty, in which case mkWpLet is a no-op
  894 
  895 -- | Variant of 'tcSkolemise' that takes an ExpType
  896 tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
  897               -> (ExpRhoType -> TcM result)
  898               -> TcM (HsWrapper, result)
  899 tcSkolemiseET _ et@(Infer {}) thing_inside
  900   = (idHsWrapper, ) <$> thing_inside et
  901 tcSkolemiseET ctxt (Check ty) thing_inside
  902   = tcSkolemise ctxt ty $ \rho_ty ->
  903     thing_inside (mkCheckExpType rho_ty)
  904 
  905 checkConstraints :: SkolemInfo
  906                  -> [TcTyVar]           -- Skolems
  907                  -> [EvVar]             -- Given
  908                  -> TcM result
  909                  -> TcM (TcEvBinds, result)
  910 
  911 checkConstraints skol_info skol_tvs given thing_inside
  912   = do { implication_needed <- implicationNeeded skol_info skol_tvs given
  913 
  914        ; if implication_needed
  915          then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
  916                  ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
  917                  ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
  918                  ; emitImplications implics
  919                  ; return (ev_binds, result) }
  920 
  921          else -- Fast path.  We check every function argument with tcCheckPolyExpr,
  922               -- which uses tcSkolemise and hence checkConstraints.
  923               -- So this fast path is well-exercised
  924               do { res <- thing_inside
  925                  ; return (emptyTcEvBinds, res) } }
  926 
  927 checkTvConstraints :: SkolemInfo
  928                    -> [TcTyVar]          -- Skolem tyvars
  929                    -> TcM result
  930                    -> TcM result
  931 
  932 checkTvConstraints skol_info skol_tvs thing_inside
  933   = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
  934        ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
  935        ; return result }
  936 
  937 emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
  938                          -> TcLevel -> WantedConstraints -> TcM ()
  939 emitResidualTvConstraint skol_info skol_tvs tclvl wanted
  940   | not (isEmptyWC wanted) ||
  941     checkTelescopeSkol skol_info
  942   = -- checkTelescopeSkol: in this case, /always/ emit this implication
  943     -- even if 'wanted' is empty. We need the implication so that we check
  944     -- for a bad telescope. See Note [Skolem escape and forall-types] in
  945     -- GHC.Tc.Gen.HsType
  946     do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
  947        ; emitImplication implic }
  948 
  949   | otherwise  -- Empty 'wanted', emit nothing
  950   = return ()
  951 
  952 buildTvImplication :: SkolemInfo -> [TcTyVar]
  953                    -> TcLevel -> WantedConstraints -> TcM Implication
  954 buildTvImplication skol_info skol_tvs tclvl wanted
  955   = do { ev_binds <- newNoTcEvBinds  -- Used for equalities only, so all the constraints
  956                                      -- are solved by filling in coercion holes, not
  957                                      -- by creating a value-level evidence binding
  958        ; implic   <- newImplication
  959 
  960        ; return (implic { ic_tclvl     = tclvl
  961                         , ic_skols     = skol_tvs
  962                         , ic_given_eqs = NoGivenEqs
  963                         , ic_wanted    = wanted
  964                         , ic_binds     = ev_binds
  965                         , ic_info      = skol_info }) }
  966 
  967 implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
  968 -- See Note [When to build an implication]
  969 implicationNeeded skol_info skol_tvs given
  970   | null skol_tvs
  971   , null given
  972   , not (alwaysBuildImplication skol_info)
  973   = -- Empty skolems and givens
  974     do { tc_lvl <- getTcLevel
  975        ; if not (isTopTcLevel tc_lvl)  -- No implication needed if we are
  976          then return False             -- already inside an implication
  977          else
  978     do { dflags <- getDynFlags       -- If any deferral can happen,
  979                                      -- we must build an implication
  980        ; return (gopt Opt_DeferTypeErrors dflags ||
  981                  gopt Opt_DeferTypedHoles dflags ||
  982                  gopt Opt_DeferOutOfScopeVariables dflags) } }
  983 
  984   | otherwise     -- Non-empty skolems or givens
  985   = return True   -- Definitely need an implication
  986 
  987 alwaysBuildImplication :: SkolemInfo -> Bool
  988 -- See Note [When to build an implication]
  989 alwaysBuildImplication _ = False
  990 
  991 {-  Commmented out for now while I figure out about error messages.
  992     See #14185
  993 
  994 alwaysBuildImplication (SigSkol ctxt _ _)
  995   = case ctxt of
  996       FunSigCtxt {} -> True  -- RHS of a binding with a signature
  997       _             -> False
  998 alwaysBuildImplication (RuleSkol {})      = True
  999 alwaysBuildImplication (InstSkol {})      = True
 1000 alwaysBuildImplication (FamInstSkol {})   = True
 1001 alwaysBuildImplication _                  = False
 1002 -}
 1003 
 1004 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
 1005                    -> [EvVar] -> WantedConstraints
 1006                    -> TcM (Bag Implication, TcEvBinds)
 1007 buildImplicationFor tclvl skol_info skol_tvs given wanted
 1008   | isEmptyWC wanted && null given
 1009              -- Optimisation : if there are no wanteds, and no givens
 1010              -- don't generate an implication at all.
 1011              -- Reason for the (null given): we don't want to lose
 1012              -- the "inaccessible alternative" error check
 1013   = return (emptyBag, emptyTcEvBinds)
 1014 
 1015   | otherwise
 1016   = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
 1017       -- Why allow TyVarTvs? Because implicitly declared kind variables in
 1018       -- non-CUSK type declarations are TyVarTvs, and we need to bring them
 1019       -- into scope as a skolem in an implication. This is OK, though,
 1020       -- because TyVarTvs will always remain tyvars, even after unification.
 1021     do { ev_binds_var <- newTcEvBinds
 1022        ; implic <- newImplication
 1023        ; let implic' = implic { ic_tclvl  = tclvl
 1024                               , ic_skols  = skol_tvs
 1025                               , ic_given  = given
 1026                               , ic_wanted = wanted
 1027                               , ic_binds  = ev_binds_var
 1028                               , ic_info   = skol_info }
 1029 
 1030        ; return (unitBag implic', TcEvBinds ev_binds_var) }
 1031 
 1032 {- Note [When to build an implication]
 1033 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1034 Suppose we have some 'skolems' and some 'givens', and we are
 1035 considering whether to wrap the constraints in their scope into an
 1036 implication.  We must /always/ so if either 'skolems' or 'givens' are
 1037 non-empty.  But what if both are empty?  You might think we could
 1038 always drop the implication.  Other things being equal, the fewer
 1039 implications the better.  Less clutter and overhead.  But we must
 1040 take care:
 1041 
 1042 * If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
 1043   we'll make a /term-level/ evidence binding for 'g = error "blah"'.
 1044   We must have an EvBindsVar those bindings!, otherwise they end up as
 1045   top-level unlifted bindings, which are verboten. This only matters
 1046   at top level, so we check for that
 1047   See also Note [Deferred errors for coercion holes] in GHC.Tc.Errors.
 1048   cf #14149 for an example of what goes wrong.
 1049 
 1050 * If you have
 1051      f :: Int;  f = f_blah
 1052      g :: Bool; g = g_blah
 1053   If we don't build an implication for f or g (no tyvars, no givens),
 1054   the constraints for f_blah and g_blah are solved together.  And that
 1055   can yield /very/ confusing error messages, because we can get
 1056       [W] C Int b1    -- from f_blah
 1057       [W] C Int b2    -- from g_blan
 1058   and fundpes can yield [D] b1 ~ b2, even though the two functions have
 1059   literally nothing to do with each other.  #14185 is an example.
 1060   Building an implication keeps them separate.
 1061 -}
 1062 
 1063 {-
 1064 ************************************************************************
 1065 *                                                                      *
 1066                 Boxy unification
 1067 *                                                                      *
 1068 ************************************************************************
 1069 
 1070 The exported functions are all defined as versions of some
 1071 non-exported generic functions.
 1072 -}
 1073 
 1074 unifyType :: Maybe SDoc  -- ^ If present, the thing that has type ty1
 1075           -> TcTauType -> TcTauType    -- ty1, ty2
 1076           -> TcM TcCoercionN           -- :: ty1 ~# ty2
 1077 -- Actual and expected types
 1078 -- Returns a coercion : ty1 ~ ty2
 1079 unifyType thing ty1 ty2
 1080   = uType TypeLevel origin ty1 ty2
 1081   where
 1082     origin = TypeEqOrigin { uo_actual   = ty1
 1083                           , uo_expected = ty2
 1084                           , uo_thing    = ppr <$> thing
 1085                           , uo_visible  = True }
 1086 
 1087 unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
 1088 -- Like unifyType, but swap expected and actual in error messages
 1089 -- This is used when typechecking patterns
 1090 unifyTypeET ty1 ty2
 1091   = uType TypeLevel origin ty1 ty2
 1092   where
 1093     origin = TypeEqOrigin { uo_actual   = ty2   -- NB swapped
 1094                           , uo_expected = ty1   -- NB swapped
 1095                           , uo_thing    = Nothing
 1096                           , uo_visible  = True }
 1097 
 1098 
 1099 unifyKind :: Maybe SDoc -> TcKind -> TcKind -> TcM CoercionN
 1100 unifyKind mb_thing ty1 ty2
 1101   = uType KindLevel origin ty1 ty2
 1102   where
 1103     origin = TypeEqOrigin { uo_actual   = ty1
 1104                           , uo_expected = ty2
 1105                           , uo_thing    = mb_thing
 1106                           , uo_visible  = True }
 1107 
 1108 
 1109 {-
 1110 %************************************************************************
 1111 %*                                                                      *
 1112                  uType and friends
 1113 %*                                                                      *
 1114 %************************************************************************
 1115 
 1116 uType is the heart of the unifier.
 1117 -}
 1118 
 1119 uType, uType_defer
 1120   :: TypeOrKind
 1121   -> CtOrigin
 1122   -> TcType    -- ty1 is the *actual* type
 1123   -> TcType    -- ty2 is the *expected* type
 1124   -> TcM CoercionN
 1125 
 1126 --------------
 1127 -- It is always safe to defer unification to the main constraint solver
 1128 -- See Note [Deferred unification]
 1129 uType_defer t_or_k origin ty1 ty2
 1130   = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
 1131 
 1132        -- Error trace only
 1133        -- NB. do *not* call mkErrInfo unless tracing is on,
 1134        --     because it is hugely expensive (#5631)
 1135        ; whenDOptM Opt_D_dump_tc_trace $ do
 1136             { ctxt <- getErrCtxt
 1137             ; doc <- mkErrInfo emptyTidyEnv ctxt
 1138             ; traceTc "utype_defer" (vcat [ debugPprType ty1
 1139                                           , debugPprType ty2
 1140                                           , pprCtOrigin origin
 1141                                           , doc])
 1142             ; traceTc "utype_defer2" (ppr co)
 1143             }
 1144        ; return co }
 1145 
 1146 --------------
 1147 uType t_or_k origin orig_ty1 orig_ty2
 1148   = do { tclvl <- getTcLevel
 1149        ; traceTc "u_tys" $ vcat
 1150               [ text "tclvl" <+> ppr tclvl
 1151               , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
 1152               , pprCtOrigin origin]
 1153        ; co <- go orig_ty1 orig_ty2
 1154        ; if isReflCo co
 1155             then traceTc "u_tys yields no coercion" Outputable.empty
 1156             else traceTc "u_tys yields coercion:" (ppr co)
 1157        ; return co }
 1158   where
 1159     go :: TcType -> TcType -> TcM CoercionN
 1160         -- The arguments to 'go' are always semantically identical
 1161         -- to orig_ty{1,2} except for looking through type synonyms
 1162 
 1163      -- Unwrap casts before looking for variables. This way, we can easily
 1164      -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
 1165      -- didn't do it this way, and then the unification above was deferred.
 1166     go (CastTy t1 co1) t2
 1167       = do { co_tys <- uType t_or_k origin t1 t2
 1168            ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
 1169 
 1170     go t1 (CastTy t2 co2)
 1171       = do { co_tys <- uType t_or_k origin t1 t2
 1172            ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
 1173 
 1174         -- Variables; go for uUnfilledVar
 1175         -- Note that we pass in *original* (before synonym expansion),
 1176         -- so that type variables tend to get filled in with
 1177         -- the most informative version of the type
 1178     go (TyVarTy tv1) ty2
 1179       = do { lookup_res <- isFilledMetaTyVar_maybe tv1
 1180            ; case lookup_res of
 1181                Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
 1182                                 ; go ty1 ty2 }
 1183                Nothing  -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
 1184     go ty1 (TyVarTy tv2)
 1185       = do { lookup_res <- isFilledMetaTyVar_maybe tv2
 1186            ; case lookup_res of
 1187                Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
 1188                               ; go ty1 ty2 }
 1189                Nothing  -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
 1190 
 1191       -- See Note [Expanding synonyms during unification]
 1192     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
 1193       | tc1 == tc2
 1194       = return $ mkNomReflCo ty1
 1195 
 1196         -- See Note [Expanding synonyms during unification]
 1197         --
 1198         -- Also NB that we recurse to 'go' so that we don't push a
 1199         -- new item on the origin stack. As a result if we have
 1200         --   type Foo = Int
 1201         -- and we try to unify  Foo ~ Bool
 1202         -- we'll end up saying "can't match Foo with Bool"
 1203         -- rather than "can't match "Int with Bool".  See #4535.
 1204     go ty1 ty2
 1205       | Just ty1' <- tcView ty1 = go ty1' ty2
 1206       | Just ty2' <- tcView ty2 = go ty1  ty2'
 1207 
 1208     -- Functions (t1 -> t2) just check the two parts
 1209     -- Do not attempt (c => t); just defer
 1210     go (FunTy { ft_af = VisArg, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
 1211        (FunTy { ft_af = VisArg, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
 1212       = do { co_l <- uType t_or_k origin arg1 arg2
 1213            ; co_r <- uType t_or_k origin res1 res2
 1214            ; co_w <- uType t_or_k origin w1 w2
 1215            ; return $ mkFunCo Nominal co_w co_l co_r }
 1216 
 1217         -- Always defer if a type synonym family (type function)
 1218         -- is involved.  (Data families behave rigidly.)
 1219     go ty1@(TyConApp tc1 _) ty2
 1220       | isTypeFamilyTyCon tc1 = defer ty1 ty2
 1221     go ty1 ty2@(TyConApp tc2 _)
 1222       | isTypeFamilyTyCon tc2 = defer ty1 ty2
 1223 
 1224     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 1225       -- See Note [Mismatched type lists and application decomposition]
 1226       | tc1 == tc2, equalLength tys1 tys2
 1227       = assertPpr (isGenerativeTyCon tc1 Nominal) (ppr tc1) $
 1228         do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
 1229            ; return $ mkTyConAppCo Nominal tc1 cos }
 1230       where
 1231         origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
 1232                        (tcTyConVisibilities tc1)
 1233 
 1234     go (LitTy m) ty@(LitTy n)
 1235       | m == n
 1236       = return $ mkNomReflCo ty
 1237 
 1238         -- See Note [Care with type applications]
 1239         -- Do not decompose FunTy against App;
 1240         -- it's often a type error, so leave it for the constraint solver
 1241     go (AppTy s1 t1) (AppTy s2 t2)
 1242       = go_app (isNextArgVisible s1) s1 t1 s2 t2
 1243 
 1244     go (AppTy s1 t1) (TyConApp tc2 ts2)
 1245       | Just (ts2', t2') <- snocView ts2
 1246       = assert (not (mustBeSaturated tc2)) $
 1247         go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
 1248 
 1249     go (TyConApp tc1 ts1) (AppTy s2 t2)
 1250       | Just (ts1', t1') <- snocView ts1
 1251       = assert (not (mustBeSaturated tc1)) $
 1252         go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
 1253 
 1254     go (CoercionTy co1) (CoercionTy co2)
 1255       = do { let ty1 = coercionType co1
 1256                  ty2 = coercionType co2
 1257            ; kco <- uType KindLevel
 1258                           (KindEqOrigin orig_ty1 orig_ty2 origin
 1259                                         (Just t_or_k))
 1260                           ty1 ty2
 1261            ; return $ mkProofIrrelCo Nominal kco co1 co2 }
 1262 
 1263         -- Anything else fails
 1264         -- E.g. unifying for-all types, which is relative unusual
 1265     go ty1 ty2 = defer ty1 ty2
 1266 
 1267     ------------------
 1268     defer ty1 ty2   -- See Note [Check for equality before deferring]
 1269       | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
 1270       | otherwise          = uType_defer t_or_k origin ty1 ty2
 1271 
 1272     ------------------
 1273     go_app vis s1 t1 s2 t2
 1274       = do { co_s <- uType t_or_k origin s1 s2
 1275            ; let arg_origin
 1276                    | vis       = origin
 1277                    | otherwise = toInvisibleOrigin origin
 1278            ; co_t <- uType t_or_k arg_origin t1 t2
 1279            ; return $ mkAppCo co_s co_t }
 1280 
 1281 {- Note [Check for equality before deferring]
 1282 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1283 Particularly in ambiguity checks we can get equalities like (ty ~ ty).
 1284 If ty involves a type function we may defer, which isn't very sensible.
 1285 An egregious example of this was in test T9872a, which has a type signature
 1286        Proxy :: Proxy (Solutions Cubes)
 1287 Doing the ambiguity check on this signature generates the equality
 1288    Solutions Cubes ~ Solutions Cubes
 1289 and currently the constraint solver normalises both sides at vast cost.
 1290 This little short-cut in 'defer' helps quite a bit.
 1291 
 1292 Note [Care with type applications]
 1293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1294 Note: type applications need a bit of care!
 1295 They can match FunTy and TyConApp, so use splitAppTy_maybe
 1296 NB: we've already dealt with type variables and Notes,
 1297 so if one type is an App the other one jolly well better be too
 1298 
 1299 Note [Mismatched type lists and application decomposition]
 1300 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1301 When we find two TyConApps, you might think that the argument lists
 1302 are guaranteed equal length.  But they aren't. Consider matching
 1303         w (T x) ~ Foo (T x y)
 1304 We do match (w ~ Foo) first, but in some circumstances we simply create
 1305 a deferred constraint; and then go ahead and match (T x ~ T x y).
 1306 This came up in #3950.
 1307 
 1308 So either
 1309    (a) either we must check for identical argument kinds
 1310        when decomposing applications,
 1311 
 1312    (b) or we must be prepared for ill-kinded unification sub-problems
 1313 
 1314 Currently we adopt (b) since it seems more robust -- no need to maintain
 1315 a global invariant.
 1316 
 1317 Note [Expanding synonyms during unification]
 1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1319 We expand synonyms during unification, but:
 1320  * We expand *after* the variable case so that we tend to unify
 1321    variables with un-expanded type synonym. This just makes it
 1322    more likely that the inferred types will mention type synonyms
 1323    understandable to the user
 1324 
 1325  * Similarly, we expand *after* the CastTy case, just in case the
 1326    CastTy wraps a variable.
 1327 
 1328  * We expand *before* the TyConApp case.  For example, if we have
 1329       type Phantom a = Int
 1330    and are unifying
 1331       Phantom Int ~ Phantom Char
 1332    it is *wrong* to unify Int and Char.
 1333 
 1334  * The problem case immediately above can happen only with arguments
 1335    to the tycon. So we check for nullary tycons *before* expanding.
 1336    This is particularly helpful when checking (* ~ *), because * is
 1337    now a type synonym.
 1338 
 1339 Note [Deferred unification]
 1340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1341 We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
 1342 and yet its consistency is undetermined. Previously, there was no way to still
 1343 make it consistent. So a mismatch error was issued.
 1344 
 1345 Now these unifications are deferred until constraint simplification, where type
 1346 family instances and given equations may (or may not) establish the consistency.
 1347 Deferred unifications are of the form
 1348                 F ... ~ ...
 1349 or              x ~ ...
 1350 where F is a type function and x is a type variable.
 1351 E.g.
 1352         id :: x ~ y => x -> y
 1353         id e = e
 1354 
 1355 involves the unification x = y. It is deferred until we bring into account the
 1356 context x ~ y to establish that it holds.
 1357 
 1358 If available, we defer original types (rather than those where closed type
 1359 synonyms have already been expanded via tcCoreView).  This is, as usual, to
 1360 improve error messages.
 1361 
 1362 
 1363 ************************************************************************
 1364 *                                                                      *
 1365                  uUnfilledVar and friends
 1366 *                                                                      *
 1367 ************************************************************************
 1368 
 1369 @uunfilledVar@ is called when at least one of the types being unified is a
 1370 variable.  It does {\em not} assume that the variable is a fixed point
 1371 of the substitution; rather, notice that @uVar@ (defined below) nips
 1372 back into @uTys@ if it turns out that the variable is already bound.
 1373 -}
 1374 
 1375 ----------
 1376 uUnfilledVar :: CtOrigin
 1377              -> TypeOrKind
 1378              -> SwapFlag
 1379              -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
 1380                                --    definitely not a /filled/ meta-tyvar
 1381              -> TcTauType      -- Type 2
 1382              -> TcM Coercion
 1383 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
 1384 --            It might be a skolem, or untouchable, or meta
 1385 
 1386 uUnfilledVar origin t_or_k swapped tv1 ty2
 1387   = do { ty2 <- zonkTcType ty2
 1388              -- Zonk to expose things to the
 1389              -- occurs check, and so that if ty2
 1390              -- looks like a type variable then it
 1391              -- /is/ a type variable
 1392        ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
 1393 
 1394 ----------
 1395 uUnfilledVar1 :: CtOrigin
 1396               -> TypeOrKind
 1397               -> SwapFlag
 1398               -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
 1399                                 --    definitely not a /filled/ meta-tyvar
 1400               -> TcTauType      -- Type 2, zonked
 1401               -> TcM Coercion
 1402 uUnfilledVar1 origin t_or_k swapped tv1 ty2
 1403   | Just tv2 <- tcGetTyVar_maybe ty2
 1404   = go tv2
 1405 
 1406   | otherwise
 1407   = uUnfilledVar2 origin t_or_k swapped tv1 ty2
 1408 
 1409   where
 1410     -- 'go' handles the case where both are
 1411     -- tyvars so we might want to swap
 1412     -- E.g. maybe tv2 is a meta-tyvar and tv1 is not
 1413     go tv2 | tv1 == tv2  -- Same type variable => no-op
 1414            = return (mkNomReflCo (mkTyVarTy tv1))
 1415 
 1416            | swapOverTyVars False tv1 tv2   -- Distinct type variables
 1417                -- Swap meta tyvar to the left if poss
 1418            = do { tv1 <- zonkTyCoVarKind tv1
 1419                      -- We must zonk tv1's kind because that might
 1420                      -- not have happened yet, and it's an invariant of
 1421                      -- uUnfilledTyVar2 that ty2 is fully zonked
 1422                      -- Omitting this caused #16902
 1423                 ; uUnfilledVar2 origin t_or_k (flipSwap swapped)
 1424                            tv2 (mkTyVarTy tv1) }
 1425 
 1426            | otherwise
 1427            = uUnfilledVar2 origin t_or_k swapped tv1 ty2
 1428 
 1429 ----------
 1430 uUnfilledVar2 :: CtOrigin
 1431               -> TypeOrKind
 1432               -> SwapFlag
 1433               -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
 1434                                 --    definitely not a /filled/ meta-tyvar
 1435               -> TcTauType      -- Type 2, zonked
 1436               -> TcM Coercion
 1437 uUnfilledVar2 origin t_or_k swapped tv1 ty2
 1438   = do { dflags  <- getDynFlags
 1439        ; cur_lvl <- getTcLevel
 1440        ; go dflags cur_lvl }
 1441   where
 1442     go dflags cur_lvl
 1443       | isTouchableMetaTyVar cur_lvl tv1
 1444            -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
 1445       , canSolveByUnification (metaTyVarInfo tv1) ty2
 1446       , cterHasNoProblem (checkTyVarEq dflags tv1 ty2)
 1447            -- See Note [Prevent unification with type families]
 1448       = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1)
 1449            ; traceTc "uUnfilledVar2 ok" $
 1450              vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
 1451                   , ppr ty2 <+> dcolon <+> ppr (tcTypeKind  ty2)
 1452                   , ppr (isTcReflCo co_k), ppr co_k ]
 1453 
 1454            ; if isTcReflCo co_k
 1455                -- Only proceed if the kinds match
 1456                -- NB: tv1 should still be unfilled, despite the kind unification
 1457                --     because tv1 is not free in ty2 (or, hence, in its kind)
 1458              then do { writeMetaTyVar tv1 ty2
 1459                      ; return (mkTcNomReflCo ty2) }
 1460 
 1461              else defer } -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
 1462                           -- Note [Equalities with incompatible kinds]
 1463 
 1464       | otherwise
 1465       = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
 1466                -- Occurs check or an untouchable: just defer
 1467                -- NB: occurs check isn't necessarily fatal:
 1468                --     eg tv1 occurred in type family parameter
 1469             ; defer }
 1470 
 1471     ty1 = mkTyVarTy tv1
 1472     kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
 1473 
 1474     defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
 1475 
 1476 canSolveByUnification :: MetaInfo -> TcType -> Bool
 1477 -- See Note [Unification preconditions, (TYVAR-TV)]
 1478 canSolveByUnification info xi
 1479   = case info of
 1480       CycleBreakerTv -> False
 1481       TyVarTv -> case tcGetTyVar_maybe xi of
 1482                    Nothing -> False
 1483                    Just tv -> case tcTyVarDetails tv of
 1484                                  MetaTv { mtv_info = info }
 1485                                             -> case info of
 1486                                                  TyVarTv -> True
 1487                                                  _       -> False
 1488                                  SkolemTv {} -> True
 1489                                  RuntimeUnk  -> True
 1490       _ -> True
 1491 
 1492 swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
 1493 swapOverTyVars is_given tv1 tv2
 1494   -- See Note [Unification variables on the left]
 1495   | not is_given, pri1 == 0, pri2 > 0 = True
 1496   | not is_given, pri2 == 0, pri1 > 0 = False
 1497 
 1498   -- Level comparison: see Note [TyVar/TyVar orientation]
 1499   | lvl1 `strictlyDeeperThan` lvl2 = False
 1500   | lvl2 `strictlyDeeperThan` lvl1 = True
 1501 
 1502   -- Priority: see Note [TyVar/TyVar orientation]
 1503   | pri1 > pri2 = False
 1504   | pri2 > pri1 = True
 1505 
 1506   -- Names: see Note [TyVar/TyVar orientation]
 1507   | isSystemName tv2_name, not (isSystemName tv1_name) = True
 1508 
 1509   | otherwise = False
 1510 
 1511   where
 1512     lvl1 = tcTyVarLevel tv1
 1513     lvl2 = tcTyVarLevel tv2
 1514     pri1 = lhsPriority tv1
 1515     pri2 = lhsPriority tv2
 1516     tv1_name = Var.varName tv1
 1517     tv2_name = Var.varName tv2
 1518 
 1519 
 1520 lhsPriority :: TcTyVar -> Int
 1521 -- Higher => more important to be on the LHS
 1522 --        => more likely to be eliminated
 1523 -- See Note [TyVar/TyVar orientation]
 1524 lhsPriority tv
 1525   = assertPpr (isTyVar tv) (ppr tv) $
 1526     case tcTyVarDetails tv of
 1527       RuntimeUnk  -> 0
 1528       SkolemTv {} -> 0
 1529       MetaTv { mtv_info = info } -> case info of
 1530                                      CycleBreakerTv -> 0
 1531                                      TyVarTv        -> 1
 1532                                      TauTv          -> 2
 1533                                      RuntimeUnkTv   -> 3
 1534 
 1535 {- Note [Unification preconditions]
 1536 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1537 Question: given a homogeneous equality (alpha ~# ty), when is it OK to
 1538 unify alpha := ty?
 1539 
 1540 This note only applied to /homogeneous/ equalities, in which both
 1541 sides have the same kind.
 1542 
 1543 There are three reasons not to unify:
 1544 
 1545 1. (SKOL-ESC) Skolem-escape
 1546    Consider the constraint
 1547         forall[2] a[2]. alpha[1] ~ Maybe a[2]
 1548    If we unify alpha := Maybe a, the skolem 'a' may escape its scope.
 1549    The level alpha[1] says that alpha may be used outside this constraint,
 1550    where 'a' is not in scope at all.  So we must not unify.
 1551 
 1552    Bottom line: when looking at a constraint alpha[n] := ty, do not unify
 1553    if any free variable of 'ty' has level deeper (greater) than n
 1554 
 1555 2. (UNTOUCHABLE) Untouchable unification variables
 1556    Consider the constraint
 1557         forall[2] a[2]. b[1] ~ Int => alpha[1] ~ Int
 1558    There is no (SKOL-ESC) problem with unifying alpha := Int, but it might
 1559    not be the principal solution. Perhaps the "right" solution is alpha := b.
 1560    We simply can't tell.  See "OutsideIn(X): modular type inference with local
 1561    assumptions", section 2.2.  We say that alpha[1] is "untouchable" inside
 1562    this implication.
 1563 
 1564    Bottom line: at amibient level 'l', when looking at a constraint
 1565    alpha[n] ~ ty, do not unify alpha := ty if there are any given equalities
 1566    between levels 'n' and 'l'.
 1567 
 1568    Exactly what is a "given equality" for the purpose of (UNTOUCHABLE)?
 1569    Answer: see Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
 1570 
 1571 3. (TYVAR-TV) Unifying TyVarTvs and CycleBreakerTvs
 1572    This precondition looks at the MetaInfo of the unification variable:
 1573 
 1574    * TyVarTv: When considering alpha{tyv} ~ ty, if alpha{tyv} is a
 1575      TyVarTv it can only unify with a type variable, not with a
 1576      structured type.  So if 'ty' is a structured type, such as (Maybe x),
 1577      don't unify.
 1578 
 1579    * CycleBreakerTv: never unified, except by restoreTyVarCycles.
 1580 
 1581 
 1582 Needless to say, all three have wrinkles:
 1583 
 1584 * (SKOL-ESC) Promotion.  Given alpha[n] ~ ty, what if beta[k] is free
 1585   in 'ty', where beta is a unification variable, and k>n?  'beta'
 1586   stands for a monotype, and since it is part of a level-n type
 1587   (equal to alpha[n]), we must /promote/ beta to level n.  Just make
 1588   up a fresh gamma[n], and unify beta[k] := gamma[n].
 1589 
 1590 * (TYVAR-TV) Unification variables.  Suppose alpha[tyv,n] is a level-n
 1591   TyVarTv (see Note [TyVarTv] in GHC.Tc.Types.TcMType)? Now
 1592   consider alpha[tyv,n] ~ Bool.  We don't want to unify because that
 1593   would break the TyVarTv invariant.
 1594 
 1595   What about alpha[tyv,n] ~ beta[tau,n], where beta is an ordinary
 1596   TauTv?  Again, don't unify, because beta might later be unified
 1597   with, say Bool.  (If levels permit, we reverse the orientation here;
 1598   see Note [TyVar/TyVar orientation].)
 1599 
 1600 * (UNTOUCHABLE) Untouchability.  When considering (alpha[n] ~ ty), how
 1601   do we know whether there are any given equalities between level n
 1602   and the ambient level?  We answer in two ways:
 1603 
 1604   * In the eager unifier, we only unify if l=n.  If not, alpha may be
 1605     untouchable, and defer to the constraint solver.  This check is
 1606     made in GHC.Tc.Utils.uUnifilledVar2, in the guard
 1607     isTouchableMetaTyVar.
 1608 
 1609   * In the constraint solver, we track where Given equalities occur
 1610     and use that to guard unification in GHC.Tc.Solver.Canonical.touchabilityTest
 1611     More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
 1612 
 1613     Historical note: in the olden days (pre 2021) the constraint solver
 1614     also used to unify only if l=n.  Equalities were "floated" out of the
 1615     implication in a separate step, so that they would become touchable.
 1616     But the float/don't-float question turned out to be very delicate,
 1617     as you can see if you look at the long series of Notes associated with
 1618     GHC.Tc.Solver.floatEqualities, around Nov 2020.  It's much easier
 1619     to unify in-place, with no floating.
 1620 
 1621 Note [TyVar/TyVar orientation]
 1622 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1623 Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)?
 1624 This is a surprisingly tricky question! This is invariant (TyEq:TV).
 1625 
 1626 The question is answered by swapOverTyVars, which is used
 1627   - in the eager unifier, in GHC.Tc.Utils.Unify.uUnfilledVar1
 1628   - in the constraint solver, in GHC.Tc.Solver.Canonical.canEqCanLHS2
 1629 
 1630 First note: only swap if you have to!
 1631    See Note [Avoid unnecessary swaps]
 1632 
 1633 So we look for a positive reason to swap, using a three-step test:
 1634 
 1635 * Level comparison. If 'a' has deeper level than 'b',
 1636   put 'a' on the left.  See Note [Deeper level on the left]
 1637 
 1638 * Priority.  If the levels are the same, look at what kind of
 1639   type variable it is, using 'lhsPriority'.
 1640 
 1641   Generally speaking we always try to put a MetaTv on the left
 1642   in preference to SkolemTv or RuntimeUnkTv:
 1643      a) Because the MetaTv may be touchable and can be unified
 1644      b) Even if it's not touchable, GHC.Tc.Solver.floatEqualities
 1645         looks for meta tyvars on the left
 1646 
 1647   Tie-breaking rules for MetaTvs:
 1648   - CycleBreakerTv: This is essentially a stand-in for another type;
 1649        it's untouchable and should have the same priority as a skolem: 0.
 1650 
 1651   - TyVarTv: These can unify only with another tyvar, but we can't unify
 1652        a TyVarTv with a TauTv, because then the TyVarTv could (transitively)
 1653        get a non-tyvar type. So give these a low priority: 1.
 1654 
 1655   - TauTv: This is the common case; we want these on the left so that they
 1656        can be written to: 2.
 1657 
 1658   - RuntimeUnkTv: These aren't really meta-variables used in type inference,
 1659        but just a convenience in the implementation of the GHCi debugger.
 1660        Eagerly write to these: 3. See Note [RuntimeUnkTv] in
 1661        GHC.Runtime.Heap.Inspect.
 1662 
 1663 * Names. If the level and priority comparisons are all
 1664   equal, try to eliminate a TyVar with a System Name in
 1665   favour of ones with a Name derived from a user type signature
 1666 
 1667 * Age.  At one point in the past we tried to break any remaining
 1668   ties by eliminating the younger type variable, based on their
 1669   Uniques.  See Note [Eliminate younger unification variables]
 1670   (which also explains why we don't do this any more)
 1671 
 1672 Note [Unification variables on the left]
 1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1674 For wanteds, but not givens, swap (skolem ~ meta-tv) regardless of
 1675 level, so that the unification variable is on the left.
 1676 
 1677 * We /don't/ want this for Givens because if we ave
 1678     [G] a[2] ~ alpha[1]
 1679     [W] Bool ~ a[2]
 1680   we want to rewrite the wanted to Bool ~ alpha[1],
 1681   so we can float the constraint and solve it.
 1682 
 1683 * But for Wanteds putting the unification variable on
 1684   the left means an easier job when floating, and when
 1685   reporting errors -- just fewer cases to consider.
 1686 
 1687   In particular, we get better skolem-escape messages:
 1688   see #18114
 1689 
 1690 Note [Deeper level on the left]
 1691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1692 The most important thing is that we want to put tyvars with
 1693 the deepest level on the left.  The reason to do so differs for
 1694 Wanteds and Givens, but either way, deepest wins!  Simple.
 1695 
 1696 * Wanteds.  Putting the deepest variable on the left maximise the
 1697   chances that it's a touchable meta-tyvar which can be solved.
 1698 
 1699 * Givens. Suppose we have something like
 1700      forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
 1701 
 1702   If we orient the Given a[2] on the left, we'll rewrite the Wanted to
 1703   (beta[1] ~ b[1]), and that can float out of the implication.
 1704   Otherwise it can't.  By putting the deepest variable on the left
 1705   we maximise our changes of eliminating skolem capture.
 1706 
 1707   See also GHC.Tc.Solver.InertSet Note [Let-bound skolems] for another reason
 1708   to orient with the deepest skolem on the left.
 1709 
 1710   IMPORTANT NOTE: this test does a level-number comparison on
 1711   skolems, so it's important that skolems have (accurate) level
 1712   numbers.
 1713 
 1714 See #15009 for an further analysis of why "deepest on the left"
 1715 is a good plan.
 1716 
 1717 Note [Avoid unnecessary swaps]
 1718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1719 If we swap without actually improving matters, we can get an infinite loop.
 1720 Consider
 1721     work item:  a ~ b
 1722    inert item:  b ~ c
 1723 We canonicalise the work-item to (a ~ c).  If we then swap it before
 1724 adding to the inert set, we'll add (c ~ a), and therefore kick out the
 1725 inert guy, so we get
 1726    new work item:  b ~ c
 1727    inert item:     c ~ a
 1728 And now the cycle just repeats
 1729 
 1730 Historical Note [Eliminate younger unification variables]
 1731 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1732 Given a choice of unifying
 1733      alpha := beta   or   beta := alpha
 1734 we try, if possible, to eliminate the "younger" one, as determined
 1735 by `ltUnique`.  Reason: the younger one is less likely to appear free in
 1736 an existing inert constraint, and hence we are less likely to be forced
 1737 into kicking out and rewriting inert constraints.
 1738 
 1739 This is a performance optimisation only.  It turns out to fix
 1740 #14723 all by itself, but clearly not reliably so!
 1741 
 1742 It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars).
 1743 But, to my surprise, it didn't seem to make any significant difference
 1744 to the compiler's performance, so I didn't take it any further.  Still
 1745 it seemed too nice to discard altogether, so I'm leaving these
 1746 notes.  SLPJ Jan 18.
 1747 
 1748 Note [Prevent unification with type families]
 1749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1750 We prevent unification with type families because of an uneasy compromise.
 1751 It's perfectly sound to unify with type families, and it even improves the
 1752 error messages in the testsuite. It also modestly improves performance, at
 1753 least in some cases. But it's disastrous for test case perf/compiler/T3064.
 1754 Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
 1755 What do we do? Do we reduce F? Or do we use the given? Hard to know what's
 1756 best. GHC reduces. This is a disaster for T3064, where the type's size
 1757 spirals out of control during reduction. If we prevent
 1758 unification with type families, then the solver happens to use the equality
 1759 before expanding the type family.
 1760 
 1761 It would be lovely in the future to revisit this problem and remove this
 1762 extra, unnecessary check. But we retain it for now as it seems to work
 1763 better in practice.
 1764 
 1765 Revisited in Nov '20, along with removing flattening variables. Problem
 1766 is still present, and the solution is still the same.
 1767 
 1768 Note [Type synonyms and the occur check]
 1769 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1770 Generally speaking we try to update a variable with type synonyms not
 1771 expanded, which improves later error messages, unless looking
 1772 inside a type synonym may help resolve a spurious occurs check
 1773 error. Consider:
 1774           type A a = ()
 1775 
 1776           f :: (A a -> a -> ()) -> ()
 1777           f = \ _ -> ()
 1778 
 1779           x :: ()
 1780           x = f (\ x p -> p x)
 1781 
 1782 We will eventually get a constraint of the form t ~ A t. The ok function above will
 1783 properly expand the type (A t) to just (), which is ok to be unified with t. If we had
 1784 unified with the original type A t, we would lead the type checker into an infinite loop.
 1785 
 1786 Hence, if the occurs check fails for a type synonym application, then (and *only* then),
 1787 the ok function expands the synonym to detect opportunities for occurs check success using
 1788 the underlying definition of the type synonym.
 1789 
 1790 The same applies later on in the constraint interaction code; see GHC.Tc.Solver.Interact,
 1791 function @occ_check_ok@.
 1792 
 1793 Note [Non-TcTyVars in GHC.Tc.Utils.Unify]
 1794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1795 Because the same code is now shared between unifying types and unifying
 1796 kinds, we sometimes will see proper TyVars floating around the unifier.
 1797 Example (from test case polykinds/PolyKinds12):
 1798 
 1799     type family Apply (f :: k1 -> k2) (x :: k1) :: k2
 1800     type instance Apply g y = g y
 1801 
 1802 When checking the instance declaration, we first *kind-check* the LHS
 1803 and RHS, discovering that the instance really should be
 1804 
 1805     type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y
 1806 
 1807 During this kind-checking, all the tyvars will be TcTyVars. Then, however,
 1808 as a second pass, we desugar the RHS (which is done in functions prefixed
 1809 with "tc" in GHC.Tc.TyCl"). By this time, all the kind-vars are proper
 1810 TyVars, not TcTyVars, get some kind unification must happen.
 1811 
 1812 Thus, we always check if a TyVar is a TcTyVar before asking if it's a
 1813 meta-tyvar.
 1814 
 1815 This used to not be necessary for type-checking (that is, before * :: *)
 1816 because expressions get desugared via an algorithm separate from
 1817 type-checking (with wrappers, etc.). Types get desugared very differently,
 1818 causing this wibble in behavior seen here.
 1819 -}
 1820 
 1821 -- | Breaks apart a function kind into its pieces.
 1822 matchExpectedFunKind
 1823   :: Outputable fun
 1824   => fun             -- ^ type, only for errors
 1825   -> Arity           -- ^ n: number of desired arrows
 1826   -> TcKind          -- ^ fun_ kind
 1827   -> TcM Coercion    -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res)
 1828 
 1829 matchExpectedFunKind hs_ty n k = go n k
 1830   where
 1831     go 0 k = return (mkNomReflCo k)
 1832 
 1833     go n k | Just k' <- tcView k = go n k'
 1834 
 1835     go n k@(TyVarTy kvar)
 1836       | isMetaTyVar kvar
 1837       = do { maybe_kind <- readMetaTyVar kvar
 1838            ; case maybe_kind of
 1839                 Indirect fun_kind -> go n fun_kind
 1840                 Flexi ->             defer n k }
 1841 
 1842     go n (FunTy { ft_mult = w, ft_arg = arg, ft_res = res })
 1843       = do { co <- go (n-1) res
 1844            ; return (mkTcFunCo Nominal (mkTcNomReflCo w) (mkTcNomReflCo arg) co) }
 1845 
 1846     go n other
 1847      = defer n other
 1848 
 1849     defer n k
 1850       = do { arg_kinds <- newMetaKindVars n
 1851            ; res_kind  <- newMetaKindVar
 1852            ; let new_fun = mkVisFunTysMany arg_kinds res_kind
 1853                  origin  = TypeEqOrigin { uo_actual   = k
 1854                                         , uo_expected = new_fun
 1855                                         , uo_thing    = Just (ppr hs_ty)
 1856                                         , uo_visible  = True
 1857                                         }
 1858            ; uType KindLevel origin k new_fun }
 1859 
 1860 {- *********************************************************************
 1861 *                                                                      *
 1862                  Equality invariant checking
 1863 *                                                                      *
 1864 ********************************************************************* -}
 1865 
 1866 
 1867 {-  Note [Checking for foralls]
 1868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1869 Unless we have -XImpredicativeTypes (which is a totally unsupported
 1870 feature), we do not want to unify
 1871     alpha ~ (forall a. a->a) -> Int
 1872 So we look for foralls hidden inside the type, and it's convenient
 1873 to do that at the same time as the occurs check (which looks for
 1874 occurrences of alpha).
 1875 
 1876 However, it's not just a question of looking for foralls /anywhere/!
 1877 Consider
 1878    (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
 1879 This is legal; e.g. dependent/should_compile/T11635.
 1880 
 1881 We don't want to reject it because of the forall in beta's kind, but
 1882 (see Note [Occurrence checking: look inside kinds] in GHC.Core.Type)
 1883 we do need to look in beta's kind.  So we carry a flag saying if a
 1884 'forall' is OK, and switch the flag on when stepping inside a kind.
 1885 
 1886 Why is it OK?  Why does it not count as impredicative polymorphism?
 1887 The reason foralls are bad is because we reply on "seeing" foralls
 1888 when doing implicit instantiation.  But the forall inside the kind is
 1889 fine.  We'll generate a kind equality constraint
 1890   (forall k. k->*) ~ (forall k. k->*)
 1891 to check that the kinds of lhs and rhs are compatible.  If alpha's
 1892 kind had instead been
 1893   (alpha :: kappa)
 1894 then this kind equality would rightly complain about unifying kappa
 1895 with (forall k. k->*)
 1896 
 1897 -}
 1898 
 1899 ----------------
 1900 {-# NOINLINE checkTyVarEq #-}  -- checkTyVarEq becomes big after the `inline` fires
 1901 checkTyVarEq :: DynFlags -> TcTyVar -> TcType -> CheckTyEqResult
 1902 checkTyVarEq dflags tv ty
 1903   = inline checkTypeEq dflags (TyVarLHS tv) ty
 1904     -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
 1905 
 1906 {-# NOINLINE checkTyFamEq #-}  -- checkTyFamEq becomes big after the `inline` fires
 1907 checkTyFamEq :: DynFlags
 1908              -> TyCon     -- type function
 1909              -> [TcType]  -- args, exactly saturated
 1910              -> TcType    -- RHS
 1911              -> CheckTyEqResult   -- always drops cteTypeFamily
 1912 checkTyFamEq dflags fun_tc fun_args ty
 1913   = inline checkTypeEq dflags (TyFamLHS fun_tc fun_args) ty
 1914     `cterRemoveProblem` cteTypeFamily
 1915     -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
 1916 
 1917 checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult
 1918 -- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs
 1919 -- is a canonical CEqCan.
 1920 --
 1921 -- In particular, this looks for:
 1922 --   (a) a forall type (forall a. blah)
 1923 --   (b) a predicate type (c => ty)
 1924 --   (c) a type family; see Note [Prevent unification with type families]
 1925 --   (d) a blocking coercion hole
 1926 --   (e) an occurrence of the LHS (occurs check)
 1927 --
 1928 -- Note that an occurs-check does not mean "definite error".  For example
 1929 --   type family F a
 1930 --   type instance F Int = Int
 1931 -- consider
 1932 --   b0 ~ F b0
 1933 -- This is perfectly reasonable, if we later get b0 ~ Int.  But we
 1934 -- certainly can't unify b0 := F b0
 1935 --
 1936 -- For (a), (b), and (c) we check only the top level of the type, NOT
 1937 -- inside the kinds of variables it mentions.  For (d) we look deeply
 1938 -- in coercions when the LHS is a tyvar (but skip coercions for type family
 1939 -- LHSs), and for (e) see Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
 1940 --
 1941 -- checkTypeEq is called from
 1942 --    * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
 1943 --      case-analysis on 'lhs')
 1944 --    * checkEqCanLHSFinish, which does not know the form of 'lhs'
 1945 checkTypeEq dflags lhs ty
 1946   = go ty
 1947   where
 1948     impredicative    = cteProblem cteImpredicative
 1949     type_family      = cteProblem cteTypeFamily
 1950     hole_blocker     = cteProblem cteHoleBlocker
 1951     insoluble_occurs = cteProblem cteInsolubleOccurs
 1952     soluble_occurs   = cteProblem cteSolubleOccurs
 1953 
 1954     -- The GHCi runtime debugger does its type-matching with
 1955     -- unification variables that can unify with a polytype
 1956     -- or a TyCon that would usually be disallowed by bad_tc
 1957     -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect
 1958     ghci_tv
 1959       | TyVarLHS tv <- lhs
 1960       , MetaTv { mtv_info = RuntimeUnkTv } <- tcTyVarDetails tv
 1961       = True
 1962 
 1963       | otherwise
 1964       = False
 1965 
 1966     go :: TcType -> CheckTyEqResult
 1967     go (TyVarTy tv')           = go_tv tv'
 1968     go (TyConApp tc tys)       = go_tc tc tys
 1969     go (LitTy {})              = cteOK
 1970     go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
 1971                                = go w S.<> go a S.<> go r S.<>
 1972                                  if not ghci_tv && af == InvisArg
 1973                                    then impredicative
 1974                                    else cteOK
 1975     go (AppTy fun arg) = go fun S.<> go arg
 1976     go (CastTy ty co)  = go ty  S.<> go_co co
 1977     go (CoercionTy co) = go_co co
 1978     go (ForAllTy (Bndr tv' _) ty) = (case lhs of
 1979       TyVarLHS tv | tv == tv' -> go_occ (tyVarKind tv') S.<> cterClearOccursCheck (go ty)
 1980                   | otherwise -> go_occ (tyVarKind tv') S.<> go ty
 1981       _                       -> go ty)
 1982       S.<>
 1983       if ghci_tv then cteOK else impredicative
 1984 
 1985     go_tv :: TcTyVar -> CheckTyEqResult
 1986       -- this slightly peculiar way of defining this means
 1987       -- we don't have to evaluate this `case` at every variable
 1988       -- occurrence
 1989     go_tv = case lhs of
 1990       TyVarLHS tv -> \ tv' -> go_occ (tyVarKind tv') S.<>
 1991                               if tv == tv' then insoluble_occurs else cteOK
 1992       TyFamLHS {} -> \ _tv' -> cteOK
 1993            -- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type
 1994 
 1995      -- For kinds, we only do an occurs check; we do not worry
 1996      -- about type families or foralls
 1997      -- See Note [Checking for foralls]
 1998     go_occ k = cterFromKind $ go k
 1999 
 2000     go_tc :: TyCon -> [TcType] -> CheckTyEqResult
 2001       -- this slightly peculiar way of defining this means
 2002       -- we don't have to evaluate this `case` at every tyconapp
 2003     go_tc = case lhs of
 2004       TyVarLHS {} -> \ tc tys -> check_tc tc S.<> go_tc_args tc tys
 2005       TyFamLHS fam_tc fam_args -> \ tc tys ->
 2006         if tcEqTyConApps fam_tc fam_args tc tys
 2007           then insoluble_occurs
 2008           else check_tc tc S.<> go_tc_args tc tys
 2009 
 2010       -- just look at arguments, not the tycon itself
 2011     go_tc_args :: TyCon -> [TcType] -> CheckTyEqResult
 2012     go_tc_args tc tys | isGenerativeTyCon tc Nominal = foldMap go tys
 2013                       | otherwise
 2014                       = let (tf_args, non_tf_args) = splitAt (tyConArity tc) tys in
 2015                         cterSetOccursCheckSoluble (foldMap go tf_args) S.<> foldMap go non_tf_args
 2016 
 2017      -- no bother about impredicativity in coercions, as they're
 2018      -- inferred
 2019     go_co co | TyVarLHS tv <- lhs
 2020              , tv `elemVarSet` tyCoVarsOfCo co
 2021              = soluble_occurs S.<> maybe_hole_blocker
 2022 
 2023         -- Don't check coercions for type families; see commentary at top of function
 2024              | otherwise
 2025              = maybe_hole_blocker
 2026       where
 2027         -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
 2028         -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for
 2029         -- deferred type errors
 2030         maybe_hole_blocker | not (gopt Opt_DeferTypeErrors dflags)
 2031                            , hasCoercionHoleCo co
 2032                            = hole_blocker
 2033 
 2034                            | otherwise
 2035                            = cteOK
 2036 
 2037     check_tc :: TyCon -> CheckTyEqResult
 2038     check_tc
 2039       | ghci_tv   = \ _tc -> cteOK
 2040       | otherwise = \ tc  -> (if isTauTyCon tc then cteOK else impredicative) S.<>
 2041                              (if isFamFreeTyCon tc then cteOK else type_family)