Fix #13819 by refactoring TypeEqOrigin.uo_thing
[ghc.git] / compiler / typecheck / TcUnify.hs
index b564f9f..e09b5bf 100644 (file)
@@ -6,23 +6,23 @@
 Type subsumption and unification
 -}
 
-{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
+{-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-}
 
 module TcUnify (
   -- Full-blown subsumption
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
-  tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
-  tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC,
+  tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
+  tcSubTypeDS_NC_O, tcSubTypeET,
   checkConstraints, buildImplicationFor,
 
   -- Various unifications
-  unifyType, unifyTheta, unifyKind, noThing,
-  uType, unifyExpType,
+  unifyType, unifyTheta, unifyKind,
+  uType, promoteTcType,
   swapOverTyVars, canSolveByUnification,
 
   --------------------------------
   -- Holes
-  tcInfer,
+  tcInferInst, tcInferNoInst,
   matchExpectedListTy,
   matchExpectedPArrTy,
   matchExpectedTyConApp,
@@ -31,7 +31,10 @@ module TcUnify (
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  wrapFunResCoercion
+  wrapFunResCoercion,
+
+  occCheckExpand, metaTyVarUpdateOK,
+  occCheckForErrors, OccCheckResult(..)
 
   ) where
 
@@ -49,15 +52,17 @@ import Name ( isSystemName )
 import Inst
 import TyCon
 import TysWiredIn
+import TysPrim( tYPE )
 import Var
 import VarSet
 import VarEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Name   ( Name )
 import Bag
 import Util
+import Pair( pFst )
+import qualified GHC.LanguageExtensions as LangExt
 import Outputable
 import FastString
 
@@ -112,14 +117,15 @@ passed in.
 -}
 
 -- Use this one when you have an "expected" type.
-matchExpectedFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchExpectedFunTys :: forall a.
+                       SDoc   -- See Note [Herald for matchExpectedFunTys]
                     -> Arity
                     -> ExpRhoType  -- deeply skolemised
                     -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
                           -- must fill in these ExpTypes here
                     -> TcM (a, HsWrapper)
 -- If    matchExpectedFunTys n ty = (_, wrap)
--- then  wrap : (t1 -> ... -> tn -> ty_r) "->" ty,
+-- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
 --   where [t1, ..., tn], ty_r are passed to the thing_inside
 matchExpectedFunTys herald arity orig_ty thing_inside
   = case orig_ty of
@@ -131,17 +137,20 @@ matchExpectedFunTys herald arity orig_ty thing_inside
            ; return (result, idHsWrapper) }
 
     go acc_arg_tys n ty
-      | Just ty' <- coreView ty = go acc_arg_tys n ty'
+      | Just ty' <- tcView ty = go acc_arg_tys n ty'
 
     go acc_arg_tys n (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
         do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
                                       (n-1) res_ty
            ; return ( result
-                    , mkWpFun idHsWrapper wrap_res arg_ty res_ty ) }
+                    , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) }
+      where
+        doc = text "When inferring the argument type of a function with type" <+>
+              quotes (ppr orig_ty)
 
     go acc_arg_tys n ty@(TyVarTy tv)
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
+      | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty' -> go acc_arg_tys n ty'
@@ -166,14 +175,16 @@ matchExpectedFunTys herald arity orig_ty thing_inside
                           defer acc_arg_tys n (mkCheckExpType ty)
 
     ------------
+    defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper)
     defer acc_arg_tys n fun_ty
-      = do { more_arg_tys <- replicateM n newOpenInferExpType
-           ; res_ty       <- newOpenInferExpType
+      = do { more_arg_tys <- replicateM n newInferExpTypeNoInst
+           ; res_ty       <- newInferExpTypeInst
            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
            ; more_arg_tys <- mapM readExpType more_arg_tys
            ; res_ty       <- readExpType res_ty
            ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
-           ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty
+           ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty
+                         -- Not a good origin at all :-(
            ; return (result, wrap) }
 
     ------------
@@ -190,24 +201,22 @@ matchExpectedFunTys herald arity orig_ty thing_inside
 
 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
 -- for example in function application
-matchActualFunTys :: Outputable a
-                  => SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                   -> CtOrigin
-                  -> Maybe a   -- the thing with type TcSigmaType
+                  -> Maybe (HsExpr GhcRn)   -- the thing with type TcSigmaType
                   -> Arity
                   -> TcSigmaType
                   -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
 -- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
--- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
+-- then  wrap : ty ~> (t1 -> ... -> tn -> ty_r)
 matchActualFunTys herald ct_orig mb_thing arity ty
   = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
 
 -- | Variant of 'matchActualFunTys' that works when supplied only part
 -- (that is, to the right of some arrows) of the full function type
-matchActualFunTysPart :: Outputable a
-                      => SDoc -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
                       -> CtOrigin
-                      -> Maybe a  -- the thing with type TcSigmaType
+                      -> Maybe (HsExpr GhcRn)  -- the thing with type TcSigmaType
                       -> Arity
                       -> TcSigmaType
                       -> [TcSigmaType] -- reversed args. See (*) below.
@@ -257,16 +266,19 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
         (tvs, theta, _) = tcSplitSigmaTy ty
 
     go n acc_args ty
-      | Just ty' <- coreView ty = go n acc_args ty'
+      | Just ty' <- tcView ty = go n acc_args ty'
 
     go n acc_args (FunTy arg_ty res_ty)
       = ASSERT( not (isPredTy arg_ty) )
         do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
-           ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r
+           ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
                     , arg_ty : tys, ty_r ) }
+      where
+        doc = text "When inferring the argument type of a function with type" <+>
+              quotes (ppr orig_ty)
 
     go n acc_args ty@(TyVarTy tv)
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
+      | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty' -> go n acc_args ty'
@@ -352,10 +364,10 @@ matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 ->
 -- Postcondition: (T k1 k2 k3 a b c) is well-kinded
 
 matchExpectedTyConApp tc orig_ty
-  = go orig_ty
+  = ASSERT(tc /= funTyCon) go orig_ty
   where
     go ty
-       | Just ty' <- coreView ty
+       | Just ty' <- tcView ty
        = go ty'
 
     go ty@(TyConApp tycon args)
@@ -363,7 +375,7 @@ matchExpectedTyConApp tc orig_ty
        = return (mkTcNomReflCo ty, args)
 
     go (TyVarTy tv)
-       | ASSERT( isTcTyVar tv) isMetaTyVar tv
+       | isMetaTyVar tv
        = do { cts <- readMetaTyVar tv
             ; case cts of
                 Indirect ty -> go ty
@@ -383,10 +395,10 @@ matchExpectedTyConApp tc orig_ty
     -- This happened in Trac #7368
     defer
       = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
-           ; traceTc "mtca" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
+           ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
            ; let args = mkTyVarTys arg_tvs
                  tc_template = mkTyConApp tc args
-           ; co <- unifyType noThing tc_template orig_ty
+           ; co <- unifyType Nothing tc_template orig_ty
            ; return (co, args) }
 
 ----------------------
@@ -400,13 +412,13 @@ matchExpectedAppTy orig_ty
   = go orig_ty
   where
     go ty
-      | Just ty' <- coreView ty = go ty'
+      | Just ty' <- tcView ty = go ty'
 
       | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
       = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
 
     go (TyVarTy tv)
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
+      | isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty -> go ty
@@ -418,7 +430,7 @@ matchExpectedAppTy orig_ty
     defer
       = do { ty1 <- newFlexiTyVarTy kind1
            ; ty2 <- newFlexiTyVarTy kind2
-           ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
+           ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
     orig_kind = typeKind orig_ty
@@ -517,88 +529,41 @@ skolemising the type.
 
 -- | Call this variant when you are in a higher-rank situation and
 -- you know the right-hand type is deeply skolemised.
-tcSubTypeHR :: Outputable a
-            => CtOrigin    -- ^ of the actual type
-            -> Maybe a     -- ^ If present, it has type ty_actual
+tcSubTypeHR :: CtOrigin               -- ^ of the actual type
+            -> Maybe (HsExpr GhcRn)   -- ^ If present, it has type ty_actual
             -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
 
-tcSubType :: Outputable a
-          => UserTypeCtxt -> Maybe a  -- ^ If present, it has type ty_actual
-          -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
--- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
-tcSubType ctxt maybe_thing ty_actual ty_expected
-  = tcSubTypeO origin ctxt ty_actual ty_expected
+------------------------
+tcSubTypeET :: CtOrigin -> UserTypeCtxt
+            -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
+-- If wrap = tc_sub_type_et t1 t2
+--    => wrap :: t1 ~> t2
+tcSubTypeET orig ctxt (Check ty_actual) ty_expected
+  = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected
   where
-    origin = TypeEqOrigin { uo_actual   = ty_actual
-                          , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_thing }
-
-
--- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
--- You probably want this only when looking at patterns, never expressions.
-tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeET orig ty_actual ty_expected
-  = uExpTypeX orig ty_expected ty_actual
-              (return . mkWpCastN . mkTcSymCo)
-              (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a
-                                    (mkCheckExpType ty_expected))
-
--- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
--- You probably want this only when looking at patterns, never expressions.
--- Does not add context.
-tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected
-  = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual
-tcSubTypeET_NC ctxt (Check ty_actual) ty_expected
-  = tc_sub_type orig orig ctxt ty_actual ty_expected'
-  where
-    ty_expected' = mkCheckExpType ty_expected
-    orig = TypeEqOrigin { uo_actual   = ty_actual
-                        , uo_expected = ty_expected'
-                        , uo_thing    = Nothing }
+    eq_orig = TypeEqOrigin { uo_actual   = ty_expected
+                           , uo_expected = ty_actual
+                           , uo_thing    = Nothing }
+
+tcSubTypeET _ _ (Infer inf_res) ty_expected
+  = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
+    do { co <- fillInferResult ty_expected inf_res
+       ; return (mkWpCastN (mkTcSymCo co)) }
 
+------------------------
 tcSubTypeO :: CtOrigin      -- ^ of the actual type
            -> UserTypeCtxt  -- ^ of the expected type
            -> TcSigmaType
-           -> ExpSigmaType
+           -> ExpRhoType
            -> TcM HsWrapper
-tcSubTypeO origin ctxt ty_actual ty_expected
-  = addSubTypeCtxt ty_actual ty_expected $
-    do { traceTc "tcSubType" (vcat [ pprCtOrigin origin
-                                   , pprUserTypeCtxt ctxt
-                                   , ppr ty_actual
-                                   , ppr ty_expected ])
-       ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected }
-  where
-    eq_orig | TypeEqOrigin {} <- origin = origin
-            | otherwise
-            = TypeEqOrigin { uo_actual   = ty_actual
-                           , uo_expected = ty_expected
-                           , uo_thing    = Nothing }
-
-tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a  -- ^ has type ty_actual
-            -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
--- Just like tcSubType, but with the additional precondition that
--- ty_expected is deeply skolemised (hence "DS")
-tcSubTypeDS ctxt m_expr ty_actual ty_expected
-  = addSubTypeCtxt ty_actual ty_expected $
-    tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected
-
--- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating
--- the "actual" type
-tcSubTypeDS_O :: Outputable a
-              => CtOrigin -> UserTypeCtxt
-              -> Maybe a -> TcSigmaType -> ExpRhoType
-              -> TcM HsWrapper
-tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected
+tcSubTypeO orig ctxt ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
     do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
                                        , pprUserTypeCtxt ctxt
                                        , ppr ty_actual
                                        , ppr ty_expected ])
-       ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
 addSubTypeCtxt ty_actual ty_expected thing_inside
@@ -628,89 +593,133 @@ addSubTypeCtxt ty_actual ty_expected thing_inside
 -- The "_NC" variants do not add a typechecker-error context;
 -- the caller is assumed to do that
 
-tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
+tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- Checks that actual <= expected
+-- Returns HsWrapper :: actual ~ expected
 tcSubType_NC ctxt ty_actual ty_expected
   = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
+       ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected }
   where
     origin = TypeEqOrigin { uo_actual   = ty_actual
                           , uo_expected = ty_expected
                           , uo_thing    = Nothing }
 
-tcSubTypeDS_NC :: Outputable a
-               => UserTypeCtxt
-               -> Maybe a  -- ^ If present, this has type ty_actual
-               -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
-tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected
-  = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected }
-  where
-    origin = TypeEqOrigin { uo_actual   = ty_actual
-                          , uo_expected = ty_expected
-                          , uo_thing    = mkErrorThing <$> maybe_thing }
+tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
+-- Just like tcSubType, but with the additional precondition that
+-- ty_expected is deeply skolemised (hence "DS")
+tcSubTypeDS orig ctxt ty_actual ty_expected
+  = addSubTypeCtxt ty_actual ty_expected $
+    do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
-tcSubTypeDS_NC_O :: Outputable a
-                 => CtOrigin   -- origin used for instantiation only
+tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
                  -> UserTypeCtxt
-                 -> Maybe a
+                 -> Maybe (HsExpr GhcRn)
                  -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised
-tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et
-  = uExpTypeX eq_orig ty_actual et
-      (return . mkWpCastN)
-      (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual)
-  where
-    eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et
-                           , uo_thing = mkErrorThing <$> m_thing }
+tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
+  = case ty_expected of
+      Infer inf_res -> fillInferResult_Inst inst_orig ty_actual inf_res
+      Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
+         where
+           eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
+                                  , uo_thing  = ppr <$> m_thing }
 
 ---------------
-tc_sub_type :: CtOrigin   -- origin used when calling uType
-            -> CtOrigin   -- origin used when instantiating
-            -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
-tc_sub_type eq_orig inst_orig ctxt ty_actual et
-  = uExpTypeX eq_orig ty_actual et
-      (return . mkWpCastN)
-      (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual)
-
 tc_sub_tc_type :: CtOrigin   -- used when calling uType
                -> CtOrigin   -- used when instantiating
                -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- If wrap = tc_sub_type t1 t2
+--    => wrap :: t1 ~> t2
 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
-  | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
-  = do { lookup_res <- lookupTcTyVar tv_actual
-       ; case lookup_res of
-           Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig
-                                               ctxt ty_actual' ty_expected
-
-             -- It's tempting to see if tv_actual can unify with a polytype
-             -- and, if so, call uType; otherwise, skolemise first. But this
-             -- is wrong, because skolemising will bump the TcLevel and the
-             -- unification will fail anyway.
-             -- It's also tempting to call uUnfilledVar directly, but calling
-             -- uType seems safer in the presence of possible refactoring
-             -- later.
-           Unfilled _        -> mkWpCastN <$>
-                                uType eq_orig TypeLevel ty_actual ty_expected }
-
-  | otherwise  -- See Note [Deep skolemisation]
-  = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
-                                  \ _ sk_rho ->
+  | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
+  , not (possibly_poly ty_actual)
+  = do { traceTc "tc_sub_tc_type (drop to equality)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; mkWpCastN <$>
+         uType eq_orig TypeLevel ty_actual ty_expected }
+
+  | otherwise   -- This is the general case
+  = do { traceTc "tc_sub_tc_type (general case)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
+                                                   \ _ sk_rho ->
                                   tc_sub_type_ds eq_orig inst_orig ctxt
                                                  ty_actual sk_rho
        ; return (sk_wrap <.> inner_wrap) }
+  where
+    possibly_poly ty
+      | isForAllTy ty                        = True
+      | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
+      | otherwise                            = False
+      -- NB *not* tcSplitFunTy, because here we want
+      -- to decompose type-class arguments too
+
+    definitely_poly ty
+      | (tvs, theta, tau) <- tcSplitSigmaTy ty
+      , (tv:_) <- tvs
+      , null theta
+      , isInsolubleOccursCheck NomEq tv tau
+      = True
+      | otherwise
+      = False
+
+{- Note [Don't skolemise unnecessarily]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to solve
+    (Char->Char) <= (forall a. a->a)
+We could skolemise the 'forall a', and then complain
+that (Char ~ a) is insoluble; but that's a pretty obscure
+error.  It's better to say that
+    (Char->Char) ~ (forall a. a->a)
+fails.
+
+So roughly:
+ * if the ty_expected has an outermost forall
+      (i.e. skolemisation is the next thing we'd do)
+ * and the ty_actual has no top-level polymorphism (but looking deeply)
+then we can revert to simple equality.  But we need to be careful.
+These examples are all fine:
+
+ * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
+      Polymorphism is buried in ty_actual
+
+ * (Char->Char) <= (forall a. Char -> Char)
+      ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. (a~Char) => a -> a)
+      ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. F [a] Char -> Char)
+                   where type instance F [x] t = t
+     ty_expected isn't really polymorphic
+
+If we prematurely go to equality we'll reject a program we should
+accept (e.g. Trac #13752).  So the test (which is only to improve
+error message) is very conservative:
+ * ty_actual is /definitely/ monomorphic
+ * ty_expected is /definitely/ polymorphic
+-}
 
 ---------------
 tc_sub_type_ds :: CtOrigin    -- used when calling uType
                -> CtOrigin    -- used when instantiating
                -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
--- Just like tcSubType, but with the additional precondition that
--- ty_expected is deeply skolemised
+-- If wrap = tc_sub_type_ds t1 t2
+--    => wrap :: t1 ~> t2
+-- Here is where the work actually happens!
+-- Precondition: ty_expected is deeply skolemised
 tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
-  = go ty_actual ty_expected
+  = do { traceTc "tc_sub_type_ds" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; go ty_actual ty_expected }
   where
-    go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
-                 | Just ty_e' <- coreView ty_e = go ty_a  ty_e'
+    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
+                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
 
     go (TyVarTy tv_a) ty_e
       = do { lookup_res <- lookupTcTyVar tv_a
@@ -721,40 +730,27 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
                     ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
                Unfilled _   -> unify }
 
-
-    go ty_a (TyVarTy tv_e)
-      = do { dflags <- getDynFlags
-           ; tclvl  <- getTcLevel
-           ; lookup_res <- lookupTcTyVar tv_e
-           ; case lookup_res of
-               Filled ty_e' ->
-                 do { traceTc "tcSubTypeDS_NC_O following filled exp meta-tyvar:"
-                        (ppr tv_e <+> text "-->" <+> ppr ty_e')
-                    ; tc_sub_tc_type eq_orig inst_orig ctxt ty_a ty_e' }
-               Unfilled details
-                 |  canUnifyWithPolyType dflags details
-                    && isTouchableMetaTyVar tclvl tv_e  -- don't want skolems here
-                 -> unify
-
-     -- We've avoided instantiating ty_actual just in case ty_expected is
-     -- polymorphic. But we've now assiduously determined that it is *not*
-     -- polymorphic. So instantiate away. This is needed for e.g. test
-     -- typecheck/should_compile/T4284.
-                 |  otherwise
-                 -> inst_and_unify }
+    -- Historical note (Sept 16): there was a case here for
+    --    go ty_a (TyVarTy alpha)
+    -- which, in the impredicative case unified  alpha := ty_a
+    -- where th_a is a polytype.  Not only is this probably bogus (we
+    -- simply do not have decent story for imprdicative types), but it
+    -- caused Trac #12616 because (also bizarrely) 'deriving' code had
+    -- -XImpredicativeTypes on.  I deleted the entire case.
 
     go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
       | not (isPredTy act_arg)
       , not (isPredTy exp_arg)
       = -- See Note [Co/contra-variance of subsumption checking]
-        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
-           ; arg_wrap
-               <- tc_sub_tc_type eq_orig (GivenOrigin
-                                          (SigSkol GenSigCtxt exp_arg))
-                                 ctxt exp_arg act_arg
-           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
-               -- arg_wrap :: exp_arg ~ act_arg
-               -- res_wrap :: act-res ~ exp_res
+        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig  ctxt act_res exp_res
+           ; arg_wrap <- tc_sub_tc_type eq_orig given_orig ctxt exp_arg act_arg
+           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) }
+               -- arg_wrap :: exp_arg ~> act_arg
+               -- res_wrap :: act-res ~> exp_res
+      where
+        given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg [])
+        doc = text "When checking that" <+> quotes (ppr ty_actual) <+>
+              text "is more polymorphic than" <+> quotes (ppr ty_expected)
 
     go ty_a ty_e
       | let (tvs, theta, _) = tcSplitSigmaTy ty_a
@@ -762,8 +758,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
       = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
            ; body_wrap <- tc_sub_type_ds
                             (eq_orig { uo_actual = in_rho
-                                     , uo_expected =
-                                         mkCheckExpType ty_expected })
+                                     , uo_expected = ty_expected })
                             inst_orig ctxt in_rho ty_e
            ; return (body_wrap <.> in_wrap) }
 
@@ -800,19 +795,19 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
 -----------------
 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
 -- expressions
-tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> ExpRhoType
-             -> TcM (HsExpr TcId)
-tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)
+tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+             -> TcM (HsExpr GhcTcId)
+tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
 
 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
 -- convenient.
-tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> ExpRhoType
-               -> TcM (HsExpr TcId)
-tcWrapResultO orig expr actual_ty res_ty
+tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+               -> TcM (HsExpr GhcTcId)
+tcWrapResultO orig rn_expr expr actual_ty res_ty
   = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                       , text "Expected:" <+> ppr res_ty ])
        ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
-                                 (Just expr) actual_ty res_ty
+                                 (Just rn_expr) actual_ty res_ty
        ; return (mkHsWrap cow expr) }
 
 -----------------------------------
@@ -829,24 +824,230 @@ wrapFunResCoercion arg_tys co_fn_res
   = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
         ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
 
------------------------------------
+
+{- **********************************************************************
+%*                                                                      *
+            ExpType functions: tcInfer, fillInferResult
+%*                                                                      *
+%********************************************************************* -}
+
 -- | Infer a type using a fresh ExpType
 -- See also Note [ExpType] in TcMType
-tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_check
-  = do { res_ty <- newOpenInferExpType
+-- Does not attempt to instantiate the inferred type
+tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInferNoInst = tcInfer False
+
+tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
+tcInferInst = tcInfer True
+
+tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInfer instantiate tc_check
+  = do { res_ty <- newInferExpType instantiate
        ; result <- tc_check res_ty
        ; res_ty <- readExpType res_ty
        ; return (result, res_ty) }
 
-{-
-************************************************************************
+fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- If wrap = fillInferResult_Inst t1 t2
+--    => wrap :: t1 ~> t2
+-- See Note [Deep instantiation of InferResult]
+fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me })
+  | instantiate_me
+  = do { (wrap, rho) <- deeplyInstantiate orig ty
+       ; co <- fillInferResult rho inf_res
+       ; return (mkWpCastN co <.> wrap) }
+
+  | otherwise
+  = do { co <- fillInferResult ty inf_res
+       ; return (mkWpCastN co) }
+
+fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
+-- If wrap = fillInferResult t1 t2
+--    => wrap :: t1 ~> t2
+fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+                            , ir_ref = ref })
+  = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
+
+       ; traceTc "Filling ExpType" $
+         ppr u <+> text ":=" <+> ppr ty_to_fill_with
+
+       ; when debugIsOn (check_hole ty_to_fill_with)
+
+       ; writeTcRef ref (Just ty_to_fill_with)
+
+       ; return ty_co }
+  where
+    check_hole ty   -- Debug check only
+      = do { let ty_lvl = tcTypeLevel ty
+           ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
+                       ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
+                       ppr ty <+> ppr (typeKind ty) $$ ppr orig_ty )
+           ; cts <- readTcRef ref
+           ; case cts of
+               Just already_there -> pprPanic "writeExpType"
+                                       (vcat [ ppr u
+                                             , ppr ty
+                                             , ppr already_there ])
+               Nothing -> return () }
+
+{- Note [Deep instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In some cases we want to deeply instantiate before filling in
+an InferResult, and in some cases not.  That's why InferReult
+has the ir_inst flag.
+
+* ir_inst = True: deeply instantiate
+
+  Consider
+    f x = (*)
+  We want to instantiate the type of (*) before returning, else we
+  will infer the type
+    f :: forall {a}. a -> forall b. Num b => b -> b -> b
+  This is surely confusing for users.
+
+  And worse, the the monomorphism restriction won't properly. The MR is
+  dealt with in simplifyInfer, and simplifyInfer has no way of
+  instantiating. This could perhaps be worked around, but it may be
+  hard to know even when instantiation should happen.
+
+  Another reason.  Consider
+       f :: (?x :: Int) => a -> a
+       g y = let ?x = 3::Int in f
+  Here want to instantiate f's type so that the ?x::Int constraint
+  gets discharged by the enclosing implicit-parameter binding.
+
+* ir_inst = False: do not instantiate
+
+  Consider this (which uses visible type application):
+
+    (let { f :: forall a. a -> a; f x = x } in f) @Int
+
+  We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
+  And we don't want to instantite the type of 'f' when we reach it,
+  else the outer visible type application won't work
+-}
+
+{- *********************************************************************
 *                                                                      *
-\subsection{Generalisation}
+              Promoting types
 *                                                                      *
-************************************************************************
+********************************************************************* -}
+
+promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
+-- See Note [Promoting a type]
+-- promoteTcType level ty = (co, ty')
+--   * Returns ty'  whose max level is just 'level'
+--             and  whose kind is ~# to the kind of 'ty'
+--             and  whose kind has form TYPE rr
+--   * and co :: ty ~ ty'
+--   * and emits constraints to justify the coercion
+promoteTcType dest_lvl ty
+  = do { cur_lvl <- getTcLevel
+       ; if (cur_lvl `sameDepthAs` dest_lvl)
+         then dont_promote_it
+         else promote_it }
+  where
+    promote_it :: TcM (TcCoercion, TcType)
+    promote_it  -- Emit a constraint  (alpha :: TYPE rr) ~ ty
+                -- where alpha and rr are fresh and from level dest_lvl
+      = do { rr      <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
+           ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
+           ; let eq_orig = TypeEqOrigin { uo_actual   = ty
+                                        , uo_expected = prom_ty
+                                        , uo_thing    = Nothing }
+
+           ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
+           ; return (co, prom_ty) }
+
+    dont_promote_it :: TcM (TcCoercion, TcType)
+    dont_promote_it  -- Check that ty :: TYPE rr, for some (fresh) rr
+      = do { res_kind <- newOpenTypeKind
+           ; let ty_kind = typeKind ty
+                 kind_orig = TypeEqOrigin { uo_actual   = ty_kind
+                                          , uo_expected = res_kind
+                                          , uo_thing    = Nothing }
+           ; ki_co <- uType kind_orig KindLevel (typeKind ty) res_kind
+           ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co
+           ; return (co, ty `mkCastTy` ki_co) }
+
+{- Note [Promoting a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #12427)
+
+  data T where
+    MkT :: (Int -> Int) -> a -> T
+
+  h y = case y of MkT v w -> v
+
+We'll infer the RHS type with an expected type ExpType of
+  (IR { ir_lvl = l, ir_ref = ref, ... )
+where 'l' is the TcLevel of the RHS of 'h'.  Then the MkT pattern
+match will increase the level, so we'll end up in tcSubType, trying to
+unify the type of v,
+  v :: Int -> Int
+with the expected type.  But this attempt takes place at level (l+1),
+rightly so, since v's type could have mentioned existential variables,
+(like w's does) and we want to catch that.
+
+So we
+  - create a new meta-var alpha[l+1]
+  - fill in the InferRes ref cell 'ref' with alpha
+  - emit an equality constraint, thus
+        [W] alpha[l+1] ~ (Int -> Int)
+
+That constraint will float outwards, as it should, unless v's
+type mentions a skolem-captured variable.
+
+This approach fails if v has a higher rank type; see
+Note [Promotion and higher rank types]
+
+
+Note [Promotion and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
+then we'd emit an equality
+        [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
+which will sadly fail because we can't unify a unification variable
+with a polytype.  But there is nothing really wrong with the program
+here.
+
+We could just about solve this by "promote the type" of v, to expose
+its polymorphic "shape" while still leaving constraints that will
+prevent existential escape.  But we must be careful!  Exposing
+the "shape" of the type is precisely what we must NOT do under
+a GADT pattern match!  So in this case we might promote the type
+to
+        (forall a. a->a) -> alpha[l+1]
+and emit the constraint
+        [W] alpha[l+1] ~ Int
+Now the poromoted type can fill the ref cell, while the emitted
+equality can float or not, according to the usual rules.
+
+But that's not quite right!  We are exposing the arrow! We could
+deal with that too:
+        (forall a. mu[l+1] a a) -> alpha[l+1]
+with constraints
+        [W] alpha[l+1] ~ Int
+        [W] mu[l+1] ~ (->)
+Here we abstract over the '->' inside the forall, in case that
+is subject to an equality constraint from a GADT match.
+
+Note that we kept the outer (->) because that's part of
+the polymorphic "shape".  And becauuse of impredicativity,
+GADT matches can't give equalities that affect polymorphic
+shape.
+
+This reasoning just seems too complicated, so I decided not
+to do it.  These higher-rank notes are just here to record
+the thinking.
 -}
 
+{- *********************************************************************
+*                                                                      *
+                    Generalisation
+*                                                                      *
+********************************************************************* -}
+
 -- | Take an "expected type" and strip off quantifiers to expose the
 -- type underneath, binding the new skolems for the @thing_inside@.
 -- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
@@ -860,14 +1061,14 @@ tcSkolemise ctxt expected_ty thing_inside
    -- We expect expected_ty to be a forall-type
    -- If not, the call is a no-op
   = do  { traceTc "tcSkolemise" Outputable.empty
-        ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
+        ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty
 
         ; lvl <- getTcLevel
         ; when debugIsOn $
               traceTc "tcSkolemise" $ vcat [
                 ppr lvl,
                 text "expected_ty" <+> ppr expected_ty,
-                text "inst tyvars" <+> ppr tvs',
+                text "inst tyvars" <+> ppr tv_prs,
                 text "given"       <+> ppr given,
                 text "inst type"   <+> ppr rho' ]
 
@@ -884,9 +1085,8 @@ tcSkolemise ctxt expected_ty thing_inside
         -- TcTyVars, all this is handled automatically with no need for
         -- extra faffing around
 
-        -- Use the *instantiated* type in the SkolemInfo
-        -- so that the names of displayed type variables line up
-        ; let skol_info = SigSkol ctxt (mkFunTys (map varType given) rho')
+        ; let tvs' = map snd tv_prs
+              skol_info = SigSkol ctxt expected_ty tv_prs
 
         ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
                                 thing_inside tvs' rho'
@@ -953,8 +1153,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
   = return (emptyBag, emptyTcEvBinds)
 
   | otherwise
-  = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
-    ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
+  = ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
     do { ev_binds_var <- newTcEvBinds
        ; env <- getLclEnv
        ; let implic = Implic { ic_tclvl = tclvl
@@ -963,8 +1162,9 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
                              , ic_given = given
                              , ic_wanted = wanted
                              , ic_status  = IC_Unsolved
-                             , ic_binds = Just ev_binds_var
+                             , ic_binds = ev_binds_var
                              , ic_env = env
+                             , ic_needed = emptyVarSet
                              , ic_info = skol_info }
 
        ; return (unitBag implic, TcEvBinds ev_binds_var) }
@@ -980,40 +1180,26 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 -}
 
-unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
+unifyType :: Maybe (HsExpr GhcRn)   -- ^ If present, has type 'ty1'
           -> TcTauType -> TcTauType -> TcM TcCoercionN
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
-unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
-  where
-    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
-                          , uo_thing  = mkErrorThing <$> thing }
-
--- | Variant of 'unifyType' that takes an 'ExpType' as its second type
-unifyExpType :: Outputable a => Maybe a
-             -> TcTauType -> ExpType -> TcM TcCoercionN
-unifyExpType mb_thing ty1 ty2
-  = uExpType ty_orig ty1 ty2
+unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType origin TypeLevel ty1 ty2
   where
-    ty_orig   = TypeEqOrigin { uo_actual   = ty1
-                             , uo_expected = ty2
-                             , uo_thing    = mkErrorThing <$> mb_thing }
+    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
+                          , uo_thing  = ppr <$> thing }
 
--- | Use this instead of 'Nothing' when calling 'unifyType' without
--- a good "thing" (where the "thing" has the "actual" type passed in)
--- This has an 'Outputable' instance, avoiding amgiguity problems.
-noThing :: Maybe (HsExpr Name)
-noThing = Nothing
-
-unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN
-unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
-  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2
-                              , uo_thing  = mkErrorThing <$> thing }
+unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
+unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType origin KindLevel ty1 ty2
+  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
+                              , uo_thing  = ppr <$> thing }
 
 ---------------
 unifyPred :: PredType -> PredType -> TcM TcCoercionN
 -- Actual and expected types
-unifyPred = unifyType noThing
+unifyPred = unifyType Nothing
 
 ---------------
 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
@@ -1034,34 +1220,6 @@ unifyTheta theta1 theta2
 uType is the heart of the unifier.
 -}
 
-uExpType :: CtOrigin -> TcType -> ExpType -> TcM CoercionN
-uExpType orig ty1 et
-  = uExpTypeX orig ty1 et return $
-    uType orig TypeLevel ty1
-
--- | Tries to unify with an ExpType. If the ExpType is filled in, calls the first
--- continuation with the produced coercion. Otherwise, calls the second
--- continuation. This can happen either with a Check or with an untouchable
--- ExpType that reverts to a tau-type. See Note [TcLevel of ExpType]
-uExpTypeX :: CtOrigin -> TcType -> ExpType
-          -> (TcCoercionN -> TcM a)   -- Infer case, co :: TcType ~N ExpType
-          -> (TcType -> TcM a)        -- Check / untouchable case
-          -> TcM a
-uExpTypeX orig ty1 et@(Infer _ tc_lvl ki _) coercion_cont type_cont
-  = do { cur_lvl <- getTcLevel
-       ; if cur_lvl `sameDepthAs` tc_lvl
-         then do { ki_co <- uType kind_orig KindLevel (typeKind ty1) ki
-                 ; writeExpType et (ty1 `mkCastTy` ki_co)
-                 ; coercion_cont $ mkTcNomReflCo ty1 `mkTcCoherenceRightCo` ki_co }
-         else do { traceTc "Preventing writing to untouchable ExpType" empty
-                 ; tau <- expTypeToType et -- See Note [TcLevel of ExpType]
-                 ; type_cont tau }}
-  where
-    kind_orig = KindEqOrigin ty1 Nothing orig (Just TypeLevel)
-uExpTypeX _ _ (Check ty2) _ type_cont
-  = type_cont ty2
-
-------------
 uType, uType_defer
   :: CtOrigin
   -> TypeOrKind
@@ -1073,28 +1231,23 @@ uType, uType_defer
 -- It is always safe to defer unification to the main constraint solver
 -- See Note [Deferred unification]
 uType_defer origin t_or_k ty1 ty2
-  = do { hole <- newCoercionHole
-       ; loc <- getCtLocM origin (Just t_or_k)
-       ; emitSimple $ mkNonCanonical $
-             CtWanted { ctev_dest = HoleDest hole
-                      , ctev_pred = mkPrimEqPred ty1 ty2
-                      , ctev_loc = loc }
+  = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
 
        -- Error trace only
-       -- NB. do *not* call mkErrInfo unless tracing is on, because
-       -- it is hugely expensive (#5631)
+       -- NB. do *not* call mkErrInfo unless tracing is on,
+       --     because it is hugely expensive (#5631)
        ; whenDOptM Opt_D_dump_tc_trace $ do
             { ctxt <- getErrCtxt
             ; doc <- mkErrInfo emptyTidyEnv ctxt
-            ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1,
+            ; traceTc "utype_defer" (vcat [ppr co, ppr ty1,
                                            ppr ty2, pprCtOrigin origin, doc])
             }
-       ; return (mkHoleCo hole Nominal ty1 ty2) }
+       ; return co }
 
 --------------
 uType origin t_or_k orig_ty1 orig_ty2
   = do { tclvl <- getTcLevel
-       ; traceTc "u_tys " $ vcat
+       ; traceTc "u_tys" $ vcat
               [ text "tclvl" <+> ppr tclvl
               , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
               , pprCtOrigin origin]
@@ -1139,8 +1292,8 @@ uType origin t_or_k orig_ty1 orig_ty2
         -- we'll end up saying "can't match Foo with Bool"
         -- rather than "can't match "Int with Bool".  See Trac #4535.
     go ty1 ty2
-      | Just ty1' <- coreView ty1 = go ty1' ty2
-      | Just ty2' <- coreView ty2 = go ty1  ty2'
+      | Just ty1' <- tcView ty1 = go ty1' ty2
+      | Just ty2' <- tcView ty2 = go ty1  ty2'
 
     go (CastTy t1 co1) t2
       = do { co_tys <- go t1 t2
@@ -1165,7 +1318,7 @@ uType origin t_or_k orig_ty1 orig_ty2
 
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       -- See Note [Mismatched type lists and application decomposition]
-      | tc1 == tc2, length tys1 == length tys2
+      | tc1 == tc2, equalLength tys1 tys2
       = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
         do { cos <- zipWithM (uType origin t_or_k) tys1 tys2
            ; return $ mkTyConAppCo Nominal tc1 cos }
@@ -1320,7 +1473,7 @@ uUnfilledVar origin t_or_k swapped tv1 ty2
              -- Zonk to expose things to the
              -- occurs check, and so that if ty2
              -- looks like a type variable then it
-             -- is a type variable
+             -- /is/ a type variable
        ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
 
 ----------
@@ -1366,11 +1519,16 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
       | canSolveByUnification cur_lvl tv1 ty2
       , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
       = do { co_k <- uType kind_origin KindLevel (typeKind ty2') (tyVarKind tv1)
-           ; co   <- updateMeta tv1 ty2' co_k
-           ; return (maybe_sym swapped co) }
+           ; if isTcReflCo co_k  -- only proceed if the kinds matched.
+
+             then do { writeMetaTyVar tv1 ty2'
+                     ; return (mkTcNomReflCo ty2') }
+             else defer } -- this cannot be solved now.
+                          -- See Note [Equalities with incompatible kinds]
+                          -- in TcCanonical
 
       | otherwise
-      = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
+      = defer
                -- Occurs check or an untouchable: just defer
                -- NB: occurs check isn't necessarily fatal:
                --     eg tv1 occured in type family parameter
@@ -1378,84 +1536,13 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
     ty1 = mkTyVarTy tv1
     kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
 
--- | apply sym iff swapped
-maybe_sym :: SwapFlag -> Coercion -> Coercion
-maybe_sym IsSwapped  = mkSymCo
-maybe_sym NotSwapped = id
-
-----------------
-metaTyVarUpdateOK :: DynFlags
-                  -> TcTyVar             -- tv :: k1
-                  -> TcType              -- ty :: k2
-                  -> Maybe TcType        -- possibly-expanded ty
--- (metaTyFVarUpdateOK tv ty)
--- We are about to update the meta-tyvar tv with ty.
--- Check (a) that tv doesn't occur in ty (occurs check)
---       (b) that ty does not have any foralls
---           (in the impredicative case), or type functions
---
--- We have two possible outcomes:
--- (1) Return the type to update the type variable with,
---        [we know the update is ok]
--- (2) Return Nothing,
---        [the update might be dodgy]
---
--- Note that "Nothing" does not mean "definite error".  For example
---   type family F a
---   type instance F Int = Int
--- consider
---   a ~ F a
--- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
--- we return Nothing, leaving it to the later constraint simplifier to
--- sort matters out.
-
-metaTyVarUpdateOK dflags tv ty
-  = case defer_me impredicative ty of
-      OC_OK _   -> Just ty
-      OC_Forall -> Nothing  -- forall or type function
-      OC_Occurs -> occCheckExpand tv ty
-  where
-    details       = tcTyVarDetails tv
-    impredicative = canUnifyWithPolyType dflags details
-
-    defer_me :: Bool    -- True <=> foralls are ok
-             -> TcType
-             -> OccCheckResult ()
-    -- Checks for (a) occurrence of tv
-    --            (b) type family applications
-    --            (c) foralls if the Bool is false
-    -- See Note [Prevent unification with type families]
-    -- See Note [Refactoring hazard: checkTauTvUpdate]
-    -- See Note [Checking for foralls] in TcType
-
-    defer_me _ (TyVarTy tv')
-       | tv == tv' = OC_Occurs
-       | otherwise = defer_me True (tyVarKind tv')
-    defer_me b (TyConApp tc tys)
-       | isTypeFamilyTyCon tc = OC_Forall   -- We use OC_Forall to signal
-                                            -- forall /or/ type function
-       | not (isTauTyCon tc)  = OC_Forall
-       | otherwise            = mapM (defer_me b) tys >> OC_OK ()
-
-    defer_me b (ForAllTy (TvBndr tv' _) t)
-       | not b     = OC_Forall
-       | tv == tv' = OC_OK ()
-       | otherwise = do { defer_me True (tyVarKind tv'); defer_me b t }
-
-    defer_me _ (LitTy {})        = OC_OK ()
-    defer_me b (FunTy fun arg)   = defer_me b fun >> defer_me b arg
-    defer_me b (AppTy fun arg)   = defer_me b fun >> defer_me b arg
-    defer_me b (CastTy ty co)    = defer_me b ty  >> defer_me_co co
-    defer_me _ (CoercionTy co)   = defer_me_co co
-
-      -- We don't really care if there are type families in a coercion,
-      -- but we still can't have an occurs-check failure
-    defer_me_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
-                   | otherwise                       = OC_OK ()
+    defer = unSwap swapped (uType_defer origin t_or_k) ty1 ty2
 
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
--- See Note [Canonical orientation for tyvar/tyvar equality constraints]
 swapOverTyVars tv1 tv2
+  | isFmvTyVar tv1 = False  -- See Note [Fmv Orientation Invariant]
+  | isFmvTyVar tv2 = True
+
   | Just lvl1 <- metaTyVarTcLevel_maybe tv1
       -- If tv1 is touchable, swap only if tv2 is also
       -- touchable and it's strictly better to update the latter
@@ -1507,10 +1594,48 @@ canSolveByUnification tclvl tv xi
                                         SigTv -> True
                                         _     -> False
                        SkolemTv {} -> True
-                       FlatSkol {} -> False
                        RuntimeUnk  -> True
 
-{-
+{- Note [Fmv Orientation Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   * We always orient a constraint
+        fmv ~ alpha
+     with fmv on the left, even if alpha is
+     a touchable unification variable
+
+Reason: doing it the other way round would unify alpha:=fmv, but that
+really doesn't add any info to alpha.  But a later constraint alpha ~
+Int might unlock everything.  Comment:9 of #12526 gives a detailed
+example.
+
+WARNING: I've gone to and fro on this one several times.
+I'm now pretty sure that unifying alpha:=fmv is a bad idea!
+So orienting with fmvs on the left is a good thing.
+
+This example comes from IndTypesPerfMerge. (Others include
+T10226, T10009.)
+    From the ambiguity check for
+      f :: (F a ~ a) => a
+    we get:
+          [G] F a ~ a
+          [WD] F alpha ~ alpha, alpha ~ a
+
+    From Givens we get
+          [G] F a ~ fsk, fsk ~ a
+
+    Now if we flatten we get
+          [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
+
+    Now, if we unified alpha := fmv, we'd get
+          [WD] F fmv ~ fmv, [WD] fmv ~ a
+    And now we are stuck.
+
+So instead the Fmv Orientation Invariant puts te fmv on the
+left, giving
+      [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
+
+    Now we get alpha:=a, and everything works out
+
 Note [Prevent unification with type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We prevent unification with type families because of an uneasy compromise.
@@ -1635,18 +1760,6 @@ lookupTcTyVar tyvar
   where
     details = tcTyVarDetails tyvar
 
--- | Fill in a meta-tyvar
-updateMeta :: TcTyVar            -- ^ tv to fill in, tv :: k1
-           -> TcType             -- ^ ty2 :: k2
-           -> Coercion           -- ^ kind_co :: k2 ~N k1
-           -> TcM Coercion       -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2)
-updateMeta tv1 ty2 kind_co
-  = do { let ty2'     = ty2 `mkCastTy` kind_co
-             ty2_refl = mkNomReflCo ty2
-             co       = mkCoherenceLeftCo ty2_refl kind_co
-       ; writeMetaTyVar tv1 ty2'
-       ; return co }
-
 {-
 Note [Unifying untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1656,14 +1769,14 @@ we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
 -- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Arity           -- ^ # of args remaining, only for errors
-                     -> TcType          -- ^ type, only for errors
+matchExpectedFunKind :: Outputable fun
+                     => fun             -- ^ type, only for errors
                      -> TcKind          -- ^ function kind
                      -> TcM (Coercion, TcKind, TcKind)
                                   -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind num_args_remaining ty = go
+matchExpectedFunKind hs_ty = go
   where
-    go k | Just k' <- coreView k = go k'
+    go k | Just k' <- tcView k = go k'
 
     go k@(TyVarTy kvar)
       | isTcTyVar kvar, isMetaTyVar kvar
@@ -1679,11 +1792,332 @@ matchExpectedFunKind num_args_remaining ty = go
       = do { arg_kind <- newMetaKindVar
            ; res_kind <- newMetaKindVar
            ; let new_fun = mkFunTy arg_kind res_kind
-                 thing   = mkTypeErrorThingArgs ty num_args_remaining
                  origin  = TypeEqOrigin { uo_actual   = k
-                                        , uo_expected = mkCheckExpType new_fun
-                                        , uo_thing    = Just thing
+                                        , uo_expected = new_fun
+                                        , uo_thing    = Just (ppr hs_ty)
                                         }
            ; co <- uType origin KindLevel k new_fun
            ; return (co, arg_kind, res_kind) }
-      where
+
+
+{- *********************************************************************
+*                                                                      *
+                 Occurrence checking
+*                                                                      *
+********************************************************************* -}
+
+
+{- Note [Occurs check expansion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
+of occurrences of tv outside type function arguments, if that is
+possible; otherwise, it returns Nothing.
+
+For example, suppose we have
+  type F a b = [a]
+Then
+  occCheckExpand b (F Int b) = Just [Int]
+but
+  occCheckExpand a (F a Int) = Nothing
+
+We don't promise to do the absolute minimum amount of expanding
+necessary, but we try not to do expansions we don't need to.  We
+prefer doing inner expansions first.  For example,
+  type F a b = (a, Int, a, [a])
+  type G b   = Char
+We have
+  occCheckExpand b (F (G b)) = Just (F Char)
+even though we could also expand F to get rid of b.
+
+The two variants of the function are to support TcUnify.checkTauTvUpdate,
+which wants to prevent unification with type families. For more on this
+point, see Note [Prevent unification with type families] in TcUnify.
+
+Note [Occurrence checking: look inside kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are considering unifying
+   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
+This may be an error (what is that alpha doing inside beta's kind?),
+but we must not make the mistake of actuallyy unifying or we'll
+build an infinite data structure.  So when looking for occurrences
+of alpha in the rhs, we must look in the kinds of type variables
+that occur there.
+
+NB: we may be able to remove the problem via expansion; see
+    Note [Occurs check expansion].  So we have to try that.
+
+Note [Checking for foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Unless we have -XImpredicativeTypes (which is a totally unsupported
+feature), we do not want to unify
+    alpha ~ (forall a. a->a) -> Int
+So we look for foralls hidden inside the type, and it's convenient
+to do that at the same time as the occurs check (which looks for
+occurrences of alpha).
+
+However, it's not just a question of looking for foralls /anywhere/!
+Consider
+   (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
+This is legal; e.g. dependent/should_compile/T11635.
+
+We don't want to reject it because of the forall in beta's kind,
+but (see Note [Occurrence checking: look inside kinds]) we do
+need to look in beta's kind.  So we carry a flag saying if a 'forall'
+is OK, and sitch the flag on when stepping inside a kind.
+
+Why is it OK?  Why does it not count as impredicative polymorphism?
+The reason foralls are bad is because we reply on "seeing" foralls
+when doing implicit instantiation.  But the forall inside the kind is
+fine.  We'll generate a kind equality constraint
+  (forall k. k->*) ~ (forall k. k->*)
+to check that the kinds of lhs and rhs are compatible.  If alpha's
+kind had instead been
+  (alpha :: kappa)
+then this kind equality would rightly complain about unifying kappa
+with (forall k. k->*)
+
+-}
+
+data OccCheckResult a
+  = OC_OK a
+  | OC_Bad     -- Forall or type family
+  | OC_Occurs
+
+instance Functor OccCheckResult where
+      fmap = liftM
+
+instance Applicative OccCheckResult where
+      pure = OC_OK
+      (<*>) = ap
+
+instance Monad OccCheckResult where
+  OC_OK x    >>= k = k x
+  OC_Bad     >>= _ = OC_Bad
+  OC_Occurs  >>= _ = OC_Occurs
+
+occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
+-- Just for error-message generation; so we return OccCheckResult
+-- so the caller can report the right kind of error
+-- Check whether
+--   a) the given variable occurs in the given type.
+--   b) there is a forall in the type (unless we have -XImpredicativeTypes)
+occCheckForErrors dflags tv ty
+  = case preCheck dflags True tv ty of
+      OC_OK _   -> OC_OK ()
+      OC_Bad    -> OC_Bad
+      OC_Occurs -> case occCheckExpand tv ty of
+                     Nothing -> OC_Occurs
+                     Just _  -> OC_OK ()
+
+----------------
+metaTyVarUpdateOK :: DynFlags
+                  -> TcTyVar             -- tv :: k1
+                  -> TcType              -- ty :: k2
+                  -> Maybe TcType        -- possibly-expanded ty
+-- (metaTyFVarUpdateOK tv ty)
+-- We are about to update the meta-tyvar tv with ty
+-- Check (a) that tv doesn't occur in ty (occurs check)
+--       (b) that ty does not have any foralls
+--           (in the impredicative case), or type functions
+--
+-- We have two possible outcomes:
+-- (1) Return the type to update the type variable with,
+--        [we know the update is ok]
+-- (2) Return Nothing,
+--        [the update might be dodgy]
+--
+-- Note that "Nothing" does not mean "definite error".  For example
+--   type family F a
+--   type instance F Int = Int
+-- consider
+--   a ~ F a
+-- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
+-- we return Nothing, leaving it to the later constraint simplifier to
+-- sort matters out.
+--
+-- See Note [Refactoring hazard: checkTauTvUpdate]
+
+metaTyVarUpdateOK dflags tv ty
+  = case preCheck dflags False tv ty of
+         -- False <=> type families not ok
+         -- See Note [Prevent unification with type families]
+      OC_OK _   -> Just ty
+      OC_Bad    -> Nothing  -- forall or type function
+      OC_Occurs -> occCheckExpand tv ty
+
+preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
+-- A quick check for
+--   (a) a forall type (unless -XImpredivativeTypes)
+--   (b) a type family
+--   (c) an occurrence of the type variable (occurs check)
+--
+-- For (a) and (b) we check only the top level of the type, NOT
+-- inside the kinds of variables it mentions.  But for (c) we do
+-- look in the kinds of course.
+
+preCheck dflags ty_fam_ok tv ty
+  = fast_check ty
+  where
+    details          = tcTyVarDetails tv
+    impredicative_ok = canUnifyWithPolyType dflags details
+
+    ok :: OccCheckResult ()
+    ok = OC_OK ()
+
+    fast_check :: TcType -> OccCheckResult ()
+    fast_check (TyVarTy tv')
+      | tv == tv' = OC_Occurs
+      | otherwise = fast_check_occ (tyVarKind tv')
+           -- See Note [Occurrence checking: look inside kinds]
+
+    fast_check (TyConApp tc tys)
+      | bad_tc tc              = OC_Bad
+      | otherwise              = mapM fast_check tys >> ok
+    fast_check (LitTy {})      = ok
+    fast_check (FunTy a r)     = fast_check a   >> fast_check r
+    fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
+    fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
+    fast_check (CoercionTy co) = fast_check_co co
+    fast_check (ForAllTy (TvBndr tv' _) ty)
+       | not impredicative_ok = OC_Bad
+       | tv == tv'            = ok
+       | otherwise = do { fast_check_occ (tyVarKind tv')
+                        ; fast_check_occ ty }
+       -- Under a forall we look only for occurrences of
+       -- the type variable
+
+     -- For kinds, we only do an occurs check; we do not worry
+     -- about type families or foralls
+     -- See Note [Checking for foralls]
+    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
+                     | otherwise                        = ok
+
+     -- For coercions, we are only doing an occurs check here;
+     -- no bother about impredicativity in coercions, as they're
+     -- inferred
+    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+                     | otherwise                       = ok
+
+    bad_tc :: TyCon -> Bool
+    bad_tc tc
+      | not (impredicative_ok || isTauTyCon tc)     = True
+      | not (ty_fam_ok        || isFamFreeTyCon tc) = True
+      | otherwise                                   = False
+
+occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
+-- See Note [Occurs check expansion]
+-- We may have needed to do some type synonym unfolding in order to
+-- get rid of the variable (or forall), so we also return the unfolded
+-- version of the type, which is guaranteed to be syntactically free
+-- of the given type variable.  If the type is already syntactically
+-- free of the variable, then the same type is returned.
+occCheckExpand tv ty
+  = go emptyVarEnv ty
+  where
+    go :: VarEnv TyVar -> Type -> Maybe Type
+          -- The VarEnv carries mappings necessary
+          -- because of kind expansion
+    go env (TyVarTy tv')
+      | tv == tv'                         = Nothing
+      | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
+      | otherwise                         = do { k' <- go env (tyVarKind tv')
+                                               ; return (mkTyVarTy $
+                                                         setTyVarKind tv' k') }
+           -- See Note [Occurrence checking: look inside kinds]
+
+    go _   ty@(LitTy {}) = return ty
+    go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
+                                ; ty2' <- go env ty2
+                                ; return (mkAppTy ty1' ty2') }
+    go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
+                                ; ty2' <- go env ty2
+                                ; return (mkFunTy ty1' ty2') }
+    go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
+       | tv == tv'         = return ty
+       | otherwise         = do { ki' <- go env (tyVarKind tv')
+                                ; let tv'' = setTyVarKind tv' ki'
+                                      env' = extendVarEnv env tv' tv''
+                                ; body' <- go env' body_ty
+                                ; return (ForAllTy (TvBndr tv'' vis) body') }
+
+    -- For a type constructor application, first try expanding away the
+    -- offending variable from the arguments.  If that doesn't work, next
+    -- see if the type constructor is a type synonym, and if so, expand
+    -- it and try again.
+    go env ty@(TyConApp tc tys)
+      = case mapM (go env) tys of
+          Just tys' -> return (mkTyConApp tc tys')
+          Nothing | Just ty' <- tcView ty -> go env ty'
+                  | otherwise             -> Nothing
+                      -- Failing that, try to expand a synonym
+
+    go env (CastTy ty co) =  do { ty' <- go env ty
+                                ; co' <- go_co env co
+                                ; return (mkCastTy ty' co') }
+    go env (CoercionTy co) = do { co' <- go_co env co
+                                ; return (mkCoercionTy co') }
+
+    ------------------
+    go_co env (Refl r ty)               = do { ty' <- go env ty
+                                             ; return (mkReflCo r ty') }
+      -- Note: Coercions do not contain type synonyms
+    go_co env (TyConAppCo r tc args)    = do { args' <- mapM (go_co env) args
+                                             ; return (mkTyConAppCo r tc args') }
+    go_co env (AppCo co arg)            = do { co' <- go_co env co
+                                             ; arg' <- go_co env arg
+                                             ; return (mkAppCo co' arg') }
+    go_co env co@(ForAllCo tv' kind_co body_co)
+      | tv == tv'         = return co
+      | otherwise         = do { kind_co' <- go_co env kind_co
+                               ; let tv'' = setTyVarKind tv' $
+                                            pFst (coercionKind kind_co')
+                                     env' = extendVarEnv env tv' tv''
+                               ; body' <- go_co env' body_co
+                               ; return (ForAllCo tv'' kind_co' body') }
+    go_co env (FunCo r co1 co2)         = do { co1' <- go_co env co1
+                                             ; co2' <- go_co env co2
+                                             ; return (mkFunCo r co1' co2') }
+    go_co env (CoVarCo c)               = do { k' <- go env (varType c)
+                                             ; return (mkCoVarCo (setVarType c k')) }
+    go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
+                                             ; return (mkAxiomInstCo ax ind args') }
+    go_co env (UnivCo p r ty1 ty2)      = do { p' <- go_prov env p
+                                             ; ty1' <- go env ty1
+                                             ; ty2' <- go env ty2
+                                             ; return (mkUnivCo p' r ty1' ty2') }
+    go_co env (SymCo co)                = do { co' <- go_co env co
+                                             ; return (mkSymCo co') }
+    go_co env (TransCo co1 co2)         = do { co1' <- go_co env co1
+                                             ; co2' <- go_co env co2
+                                             ; return (mkTransCo co1' co2') }
+    go_co env (NthCo n co)              = do { co' <- go_co env co
+                                             ; return (mkNthCo n co') }
+    go_co env (LRCo lr co)              = do { co' <- go_co env co
+                                             ; return (mkLRCo lr co') }
+    go_co env (InstCo co arg)           = do { co' <- go_co env co
+                                             ; arg' <- go_co env arg
+                                             ; return (mkInstCo co' arg') }
+    go_co env (CoherenceCo co1 co2)     = do { co1' <- go_co env co1
+                                             ; co2' <- go_co env co2
+                                             ; return (mkCoherenceCo co1' co2') }
+    go_co env (KindCo co)               = do { co' <- go_co env co
+                                             ; return (mkKindCo co') }
+    go_co env (SubCo co)                = do { co' <- go_co env co
+                                             ; return (mkSubCo co') }
+    go_co env (AxiomRuleCo ax cs)       = do { cs' <- mapM (go_co env) cs
+                                             ; return (mkAxiomRuleCo ax cs') }
+
+    ------------------
+    go_prov _   UnsafeCoerceProv    = return UnsafeCoerceProv
+    go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
+    go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
+    go_prov _   p@(PluginProv _)    = return p
+    go_prov _   p@(HoleProv _)      = return p
+
+canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
+canUnifyWithPolyType dflags details
+  = case details of
+      MetaTv { mtv_info = SigTv }    -> False
+      MetaTv { mtv_info = TauTv }    -> xopt LangExt.ImpredicativeTypes dflags
+      _other                         -> True
+          -- We can have non-meta tyvars in given constraints