Fix #13819 by refactoring TypeEqOrigin.uo_thing
[ghc.git] / compiler / typecheck / TcUnify.hs
index f073c7b..e09b5bf 100644 (file)
@@ -16,7 +16,7 @@ module TcUnify (
   checkConstraints, buildImplicationFor,
 
   -- Various unifications
-  unifyType, unifyTheta, unifyKind, noThing,
+  unifyType, unifyTheta, unifyKind,
   uType, promoteTcType,
   swapOverTyVars, canSolveByUnification,
 
@@ -59,7 +59,6 @@ import VarEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
-import Name   ( Name )
 import Bag
 import Util
 import Pair( pFst )
@@ -138,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'
@@ -199,10 +201,9 @@ 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)
@@ -213,10 +214,9 @@ matchActualFunTys herald ct_orig mb_thing arity ty
 
 -- | 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.
@@ -266,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'
@@ -361,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)
@@ -372,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
@@ -392,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) }
 
 ----------------------
@@ -409,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
@@ -427,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
@@ -526,9 +529,8 @@ 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
 
@@ -561,7 +563,7 @@ tcSubTypeO orig ctxt ty_actual ty_expected
                                        , pprUserTypeCtxt ctxt
                                        , ppr ty_actual
                                        , ppr ty_expected ])
-       ; tcSubTypeDS_NC_O orig ctxt noThing 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
@@ -608,12 +610,11 @@ tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWr
 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 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
@@ -623,7 +624,7 @@ tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
       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 = mkErrorThing <$> m_thing }
+                                  , uo_thing  = ppr <$> m_thing }
 
 ---------------
 tc_sub_tc_type :: CtOrigin   -- used when calling uType
@@ -632,8 +633,8 @@ tc_sub_tc_type :: CtOrigin   -- used when calling uType
 -- If wrap = tc_sub_type t1 t2
 --    => wrap :: t1 ~> t2
 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
-  | is_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
-  , not (is_poly ty_actual)
+  | 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 ]
@@ -650,13 +651,21 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
                                                  ty_actual sk_rho
        ; return (sk_wrap <.> inner_wrap) }
   where
-    is_poly ty
+    possibly_poly ty
       | isForAllTy ty                        = True
-      | Just (_, res) <- splitFunTy_maybe ty = is_poly res
+      | 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -668,11 +677,31 @@ error.  It's better to say that
     (Char->Char) ~ (forall a. a->a)
 fails.
 
-In general,
- * if the RHS type an outermost forall (i.e. skolemisation
-   is the next thing we'd do)
- * and the LHS has no top-level polymorphism (but looking deeply)
-then we can revert to simple equality.
+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
 -}
 
 ---------------
@@ -684,10 +713,13 @@ tc_sub_type_ds :: CtOrigin    -- used when calling uType
 -- 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
@@ -710,14 +742,15 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
       | 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) }
+        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,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) }
 
 -----------------------------------
@@ -863,7 +896,7 @@ 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 instantantiate
+* ir_inst = True: deeply instantiate
 
   Consider
     f x = (*)
@@ -883,7 +916,7 @@ has the ir_inst flag.
   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 instantantiate
+* ir_inst = False: do not instantiate
 
   Consider this (which uses visible type application):
 
@@ -999,7 +1032,7 @@ with constraints
 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 (->) becuase that's part of
+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.
@@ -1028,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' ]
 
@@ -1052,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'
@@ -1121,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
@@ -1133,6 +1164,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
                              , ic_status  = IC_Unsolved
                              , ic_binds = ev_binds_var
                              , ic_env = env
+                             , ic_needed = emptyVarSet
                              , ic_info = skol_info }
 
        ; return (unitBag implic, TcEvBinds ev_binds_var) }
@@ -1148,30 +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
+unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
+                          uType origin TypeLevel ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
-                          , uo_thing  = mkErrorThing <$> thing }
+                          , 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
+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  = mkErrorThing <$> thing }
+                              , uo_thing  = ppr <$> thing }
 
 ---------------
 unifyPred :: PredType -> PredType -> TcM TcCoercionN
 -- Actual and expected types
-unifyPred = unifyType noThing
+unifyPred = unifyType Nothing
 
 ---------------
 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
@@ -1219,7 +1247,7 @@ uType_defer origin t_or_k ty1 ty2
 --------------
 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]
@@ -1264,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
@@ -1290,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 }
@@ -1491,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
@@ -1503,14 +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
+    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
@@ -1562,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.
@@ -1690,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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1711,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
@@ -1734,10 +1792,9 @@ 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 = new_fun
-                                        , uo_thing    = Just thing
+                                        , uo_thing    = Just (ppr hs_ty)
                                         }
            ; co <- uType origin KindLevel k new_fun
            ; return (co, arg_kind, res_kind) }
@@ -1858,8 +1915,7 @@ metaTyVarUpdateOK :: DynFlags
                   -> TcType              -- ty :: k2
                   -> Maybe TcType        -- possibly-expanded ty
 -- (metaTyFVarUpdateOK tv ty)
--- We are about to update the meta-tyvar tv with ty, in
--- our on-the-flyh unifier
+-- 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
@@ -1991,8 +2047,8 @@ occCheckExpand tv ty
     go env ty@(TyConApp tc tys)
       = case mapM (go env) tys of
           Just tys' -> return (mkTyConApp tc tys')
-          Nothing | Just ty' <- coreView ty -> go env ty'
-                  | otherwise               -> Nothing
+          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
@@ -2018,6 +2074,9 @@ occCheckExpand tv ty
                                      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