Make a smart mkAppTyM
[ghc.git] / compiler / typecheck / TcUnify.hs
index 269f202..6af873e 100644 (file)
@@ -13,10 +13,11 @@ module TcUnify (
   tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
   tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS,
   tcSubTypeDS_NC_O, tcSubTypeET,
-  checkConstraints, buildImplicationFor,
+  checkConstraints, checkTvConstraints,
+  buildImplicationFor, emitResidualTvConstraint,
 
   -- Various unifications
-  unifyType, unifyTheta, unifyKind,
+  unifyType, unifyKind,
   uType, promoteTcType,
   swapOverTyVars, canSolveByUnification,
 
@@ -24,22 +25,20 @@ module TcUnify (
   -- Holes
   tcInferInst, tcInferNoInst,
   matchExpectedListTy,
-  matchExpectedPArrTy,
   matchExpectedTyConApp,
   matchExpectedAppTy,
   matchExpectedFunTys,
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  wrapFunResCoercion,
-
-  occCheckExpand, metaTyVarUpdateOK,
-  occCheckForErrors, OccCheckResult(..)
+  metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..)
 
   ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import HsSyn
 import TyCoRep
 import TcMType
@@ -48,7 +47,7 @@ import TcType
 import Type
 import Coercion
 import TcEvidence
-import Name ( isSystemName )
+import Name( isSystemName )
 import Inst
 import TyCon
 import TysWiredIn
@@ -61,10 +60,8 @@ import DynFlags
 import BasicTypes
 import Bag
 import Util
-import Pair( pFst )
 import qualified GHC.LanguageExtensions as LangExt
 import Outputable
-import FastString
 
 import Control.Monad
 import Control.Arrow ( second )
@@ -98,6 +95,23 @@ This is used to construct a message of form
    The function 'f' is applied to two arguments
    but its type `Int -> Int' has only one
 
+When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the
+picture, we have a choice in deciding whether to count the type applications as
+proper arguments:
+
+   The function 'f' is applied to one visible type argument
+     and two value arguments
+   but its type `forall a. a -> a` has only one visible type argument
+     and one value argument
+
+Or whether to include the type applications as part of the herald itself:
+
+   The expression 'f @Int' is applied to two arguments
+   but its type `Int -> Int` has only one
+
+The latter is easier to implement and is arguably easier to understand, so we
+choose to implement that option.
+
 Note [matchExpectedFunTys]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 matchExpectedFunTys checks that a sigma has the form
@@ -345,13 +359,6 @@ matchExpectedListTy exp_ty
  = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
       ; return (co, elt_ty) }
 
-----------------------
-matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
--- Special case for parrs
-matchExpectedPArrTy exp_ty
-  = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
-       ; return (co, elt_ty) }
-
 ---------------------
 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
                       -> TcRhoType            -- orig_ty
@@ -389,7 +396,7 @@ matchExpectedTyConApp tc orig_ty
     -- kind-compatible with T.  For example, suppose we have
     --       matchExpectedTyConApp T (f Maybe)
     -- where data T a = MkT a
-    -- Then we don't want to instantate T's data constructors with
+    -- Then we don't want to instantiate T's data constructors with
     --    (a::*) ~ Maybe
     -- because that'll make types that are utterly ill-kinded.
     -- This happened in Trac #7368
@@ -433,7 +440,7 @@ matchExpectedAppTy orig_ty
            ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
-    orig_kind = typeKind orig_ty
+    orig_kind = tcTypeKind orig_ty
     kind1 = mkFunTy liftedTypeKind orig_kind
     kind2 = liftedTypeKind    -- m :: * -> k
                               -- arg type :: *
@@ -549,7 +556,13 @@ tcSubTypeET orig ctxt (Check ty_actual) ty_expected
 
 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
+      -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never
+      -- has the ir_inst field set.  Reason: in patterns (which is what
+      -- tcSubTypeET is used for) do not aggressively instantiate
+    do { co <- fill_infer_result ty_expected inf_res
+               -- Since ir_inst is false, we can skip fillInferResult
+               -- and go straight to fill_infer_result
+
        ; return (mkWpCastN (mkTcSymCo co)) }
 
 ------------------------
@@ -622,7 +635,7 @@ tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
 -- ty_expected is deeply skolemised
 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
+      Infer inf_res -> fillInferResult 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
@@ -737,7 +750,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
     --    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
+    -- simply do not have decent story for impredicative types), but it
     -- caused Trac #12616 because (also bizarrely) 'deriving' code had
     -- -XImpredicativeTypes on.  I deleted the entire case.
 
@@ -745,8 +758,9 @@ 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 given_orig ctxt exp_arg act_arg
+        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 GenSigCtxt exp_arg act_arg
+                         -- GenSigCtxt: See Note [Setting the argument context]
            ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) }
                -- arg_wrap :: exp_arg ~> act_arg
                -- res_wrap :: act-res ~> exp_res
@@ -776,7 +790,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
 
     inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
 
-                           -- if we haven't recurred through an arrow, then
+                           -- If we haven't recurred through an arrow, then
                            -- the eq_orig will list ty_actual. In this case,
                            -- we want to update the origin to reflect the
                            -- instantiation. If we *have* recurred through
@@ -795,6 +809,33 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
      -- use versions without synonyms expanded
     unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected
 
+{- Note [Settting the argument context]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider we are doing the ambiguity check for the (bogus)
+  f :: (forall a b. C b => a -> a) -> Int
+
+We'll call
+   tcSubType ((forall a b. C b => a->a) -> Int )
+             ((forall a b. C b => a->a) -> Int )
+
+with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
+on the argument type of the (->) -- and at that point we want to switch
+to a UserTypeCtxt of GenSigCtxt.  Why?
+
+* Error messages.  If we stick with FunSigCtxt we get errors like
+     * Could not deduce: C b
+       from the context: C b0
+        bound by the type signature for:
+            f :: forall a b. C b => a->a
+  But of course f does not have that type signature!
+  Example tests: T10508, T7220a, Simple14
+
+* Implications. We may decide to build an implication for the whole
+  ambiguity check, but we don't need one for each level within it,
+  and TcUnify.alwaysBuildImplication checks the UserTypeCtxt.
+  See Note [When to build an implication]
+-}
+
 -----------------
 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
 -- expressions
@@ -813,20 +854,6 @@ tcWrapResultO orig rn_expr expr actual_ty res_ty
                                  (Just rn_expr) actual_ty res_ty
        ; return (mkHsWrap cow expr) }
 
------------------------------------
-wrapFunResCoercion
-        :: [TcType]        -- Type of args
-        -> HsWrapper       -- HsExpr a -> HsExpr b
-        -> TcM HsWrapper   -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
-wrapFunResCoercion arg_tys co_fn_res
-  | isIdHsWrapper co_fn_res
-  = return idHsWrapper
-  | null arg_tys
-  = return co_fn_res
-  | otherwise
-  = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
-        ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
-
 
 {- **********************************************************************
 %*                                                                      *
@@ -850,24 +877,24 @@ tcInfer instantiate tc_check
        ; res_ty <- readExpType res_ty
        ; return (result, res_ty) }
 
-fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
--- If wrap = fillInferResult_Inst t1 t2
+fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
+-- If wrap = fillInferResult t1 t2
 --    => wrap :: t1 ~> t2
 -- See Note [Deep instantiation of InferResult]
-fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me })
+fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
   | instantiate_me
   = do { (wrap, rho) <- deeplyInstantiate orig ty
-       ; co <- fillInferResult rho inf_res
+       ; co <- fill_infer_result rho inf_res
        ; return (mkWpCastN co <.> wrap) }
 
   | otherwise
-  = do { co <- fillInferResult ty inf_res
+  = do { co <- fill_infer_result ty inf_res
        ; return (mkWpCastN co) }
 
-fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fillInferResult t1 t2
+fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN
+-- If wrap = fill_infer_result t1 t2
 --    => wrap :: t1 ~> t2
-fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+fill_infer_result 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
 
@@ -884,7 +911,7 @@ fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
       = 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 )
+                       ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
            ; cts <- readTcRef ref
            ; case cts of
                Just already_there -> pprPanic "writeExpType"
@@ -908,7 +935,7 @@ has the ir_inst flag.
     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
+  And worse, the monomorphism restriction won't work 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.
@@ -966,13 +993,13 @@ promoteTcType dest_lvl 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
+           ; let ty_kind = tcTypeKind ty
                  kind_orig = TypeEqOrigin { uo_actual   = ty_kind
                                           , uo_expected = res_kind
                                           , uo_thing    = Nothing
                                           , uo_visible  = False }
-           ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind
-           ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co
+           ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
+           ; let co = mkTcGReflRightCo Nominal ty ki_co
            ; return (co, ty `mkCastTy` ki_co) }
 
 {- Note [Promoting a type]
@@ -1025,7 +1052,7 @@ 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
+Now the promoted 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
@@ -1038,7 +1065,7 @@ 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,
+the polymorphic "shape".  And because of impredicativity,
 GADT matches can't give equalities that affect polymorphic
 shape.
 
@@ -1116,35 +1143,88 @@ checkConstraints :: SkolemInfo
                  -> TcM (TcEvBinds, result)
 
 checkConstraints skol_info skol_tvs given thing_inside
-  = do { (implics, ev_binds, result)
-            <- buildImplication skol_info skol_tvs given thing_inside
-       ; emitImplications implics
-       ; return (ev_binds, result) }
-
-buildImplication :: SkolemInfo
-                 -> [TcTyVar]           -- Skolems
-                 -> [EvVar]             -- Given
-                 -> TcM result
-                 -> TcM (Bag Implication, TcEvBinds, result)
-buildImplication skol_info skol_tvs given thing_inside
-  = do { tc_lvl <- getTcLevel
-       ; deferred_type_errors <- goptM Opt_DeferTypeErrors <||>
-                                 goptM Opt_DeferTypedHoles
-       ; if null skol_tvs && null given && (not deferred_type_errors ||
-                                            not (isTopTcLevel tc_lvl))
-         then do { res <- thing_inside
-                 ; return (emptyBag, emptyTcEvBinds, res) }
-      -- Fast path.  We check every function argument with
-      -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
-      -- But with the solver producing unlifted equalities, we need
-      -- to have an EvBindsVar for them when they might be deferred to
-      -- runtime. Otherwise, they end up as top-level unlifted bindings,
-      -- which are verboten. See also Note [Deferred errors for coercion holes]
-      -- in TcErrors.
+  = do { implication_needed <- implicationNeeded skol_info skol_tvs given
+
+       ; if implication_needed
+         then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+                 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
+                 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
+                 ; emitImplications implics
+                 ; return (ev_binds, result) }
+
+         else -- Fast path.  We check every function argument with
+              -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
+              -- So this fast path is well-exercised
+              do { res <- thing_inside
+                 ; return (emptyTcEvBinds, res) } }
+
+checkTvConstraints :: SkolemInfo
+                   -> Maybe SDoc  -- User-written telescope, if present
+                   -> TcM ([TcTyVar], result)
+                   -> TcM ([TcTyVar], result)
+
+checkTvConstraints skol_info m_telescope thing_inside
+  = do { (tclvl, wanted, (skol_tvs, result))
+             <- pushLevelAndCaptureConstraints thing_inside
+
+       ; emitResidualTvConstraint skol_info m_telescope
+                                  skol_tvs tclvl wanted
+
+       ; return (skol_tvs, result) }
+
+emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
+                         -> TcLevel -> WantedConstraints -> TcM ()
+emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
+  | isEmptyWC wanted
+  = return ()
+  | otherwise
+  = do { ev_binds <- newNoTcEvBinds
+       ; implic   <- newImplication
+       ; emitImplication $
+         implic { ic_tclvl     = tclvl
+                , ic_skols     = skol_tvs
+                , ic_no_eqs    = True
+                , ic_telescope = m_telescope
+                , ic_wanted    = wanted
+                , ic_binds     = ev_binds
+                , ic_info      = skol_info } }
+
+implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
+-- See Note [When to build an implication]
+implicationNeeded skol_info skol_tvs given
+  | null skol_tvs
+  , null given
+  , not (alwaysBuildImplication skol_info)
+  = -- Empty skolems and givens
+    do { tc_lvl <- getTcLevel
+       ; if not (isTopTcLevel tc_lvl)  -- No implication needed if we are
+         then return False             -- already inside an implication
          else
-    do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
-       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
-       ; return (implics, ev_binds, result) }}
+    do { dflags <- getDynFlags       -- If any deferral can happen,
+                                     -- we must build an implication
+       ; return (gopt Opt_DeferTypeErrors dflags ||
+                 gopt Opt_DeferTypedHoles dflags ||
+                 gopt Opt_DeferOutOfScopeVariables dflags) } }
+
+  | otherwise     -- Non-empty skolems or givens
+  = return True   -- Definitely need an implication
+
+alwaysBuildImplication :: SkolemInfo -> Bool
+-- See Note [When to build an implication]
+alwaysBuildImplication _ = False
+
+{-  Commmented out for now while I figure out about error messages.
+    See Trac #14185
+
+alwaysBuildImplication (SigSkol ctxt _ _)
+  = case ctxt of
+      FunSigCtxt {} -> True  -- RHS of a binding with a signature
+      _             -> False
+alwaysBuildImplication (RuleSkol {})      = True
+alwaysBuildImplication (InstSkol {})      = True
+alwaysBuildImplication (FamInstSkol {})   = True
+alwaysBuildImplication _                  = False
+-}
 
 buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
                    -> [EvVar] -> WantedConstraints
@@ -1158,21 +1238,52 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
   = return (emptyBag, emptyTcEvBinds)
 
   | otherwise
-  = ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
+  = ASSERT2( all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs, ppr skol_tvs )
+      -- Why allow TyVarTvs? Because implicitly declared kind variables in
+      -- non-CUSK type declarations are TyVarTvs, and we need to bring them
+      -- into scope as a skolem in an implication. This is OK, though,
+      -- because TyVarTvs will always remain tyvars, even after unification.
     do { ev_binds_var <- newTcEvBinds
-       ; env <- getLclEnv
-       ; let implic = Implic { ic_tclvl = tclvl
-                             , ic_skols = skol_tvs
-                             , ic_no_eqs = False
-                             , ic_given = given
-                             , ic_wanted = 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) }
+       ; implic <- newImplication
+       ; let implic' = implic { ic_tclvl  = tclvl
+                              , ic_skols  = skol_tvs
+                              , ic_given  = given
+                              , ic_wanted = wanted
+                              , ic_binds  = ev_binds_var
+                              , ic_info   = skol_info }
+
+       ; return (unitBag implic', TcEvBinds ev_binds_var) }
+
+{- Note [When to build an implication]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have some 'skolems' and some 'givens', and we are
+considering whether to wrap the constraints in their scope into an
+implication.  We must /always/ so if either 'skolems' or 'givens' are
+non-empty.  But what if both are empty?  You might think we could
+always drop the implication.  Other things being equal, the fewer
+implications the better.  Less clutter and overhead.  But we must
+take care:
+
+* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
+  we'll make a /term-level/ evidence binding for 'g = error "blah"'.
+  We must have an EvBindsVar those bindings!, otherwise they end up as
+  top-level unlifted bindings, which are verboten. This only matters
+  at top level, so we check for that
+  See also Note [Deferred errors for coercion holes] in TcErrors.
+  cf Trac #14149 for an example of what goes wrong.
+
+* If you have
+     f :: Int;  f = f_blah
+     g :: Bool; g = g_blah
+  If we don't build an implication for f or g (no tyvars, no givens),
+  the constraints for f_blah and g_blah are solved together.  And that
+  can yield /very/ confusing error messages, because we can get
+      [W] C Int b1    -- from f_blah
+      [W] C Int b2    -- from g_blan
+  and fundpes can yield [D] b1 ~ b2, even though the two functions have
+  literally nothing to do with each other.  Trac #14185 is an example.
+  Building an implication keeps them separage.
+-}
 
 {-
 ************************************************************************
@@ -1204,18 +1315,6 @@ unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
                               , uo_visible = True } -- also always from a visible context
 
 ---------------
-unifyPred :: PredType -> PredType -> TcM TcCoercionN
--- Actual and expected types
-unifyPred = unifyType Nothing
-
----------------
-unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
--- Actual and expected types
-unifyTheta theta1 theta2
-  = do  { checkTc (equalLength theta1 theta2)
-                  (vcat [text "Contexts differ in length",
-                         nest 2 $ parens $ text "Use RelaxedPolyRec to allow this"])
-        ; zipWithM unifyPred theta1 theta2 }
 
 {-
 %************************************************************************
@@ -1232,7 +1331,7 @@ uType, uType_defer
   -> CtOrigin
   -> TcType    -- ty1 is the *actual* type
   -> TcType    -- ty2 is the *expected* type
-  -> TcM Coercion
+  -> TcM CoercionN
 
 --------------
 -- It is always safe to defer unification to the main constraint solver
@@ -1246,8 +1345,11 @@ uType_defer t_or_k origin ty1 ty2
        ; whenDOptM Opt_D_dump_tc_trace $ do
             { ctxt <- getErrCtxt
             ; doc <- mkErrInfo emptyTidyEnv ctxt
-            ; traceTc "utype_defer" (vcat [ppr co, ppr ty1,
-                                           ppr ty2, pprCtOrigin origin, doc])
+            ; traceTc "utype_defer" (vcat [ debugPprType ty1
+                                          , debugPprType ty2
+                                          , pprCtOrigin origin
+                                          , doc])
+            ; traceTc "utype_defer2" (ppr co)
             }
        ; return co }
 
@@ -1264,10 +1366,21 @@ uType t_or_k origin orig_ty1 orig_ty2
             else traceTc "u_tys yields coercion:" (ppr co)
        ; return co }
   where
-    go :: TcType -> TcType -> TcM Coercion
+    go :: TcType -> TcType -> TcM CoercionN
         -- The arguments to 'go' are always semantically identical
         -- to orig_ty{1,2} except for looking through type synonyms
 
+     -- Unwrap casts before looking for variables. This way, we can easily
+     -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
+     -- didn't do it this way, and then the unification above was deferred.
+    go (CastTy t1 co1) t2
+      = do { co_tys <- uType t_or_k origin t1 t2
+           ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
+
+    go t1 (CastTy t2 co2)
+      = do { co_tys <- uType t_or_k origin t1 t2
+           ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
+
         -- Variables; go for uVar
         -- Note that we pass in *original* (before synonym expansion),
         -- so that type variables tend to get filled in with
@@ -1288,7 +1401,7 @@ uType t_or_k origin orig_ty1 orig_ty2
       -- See Note [Expanding synonyms during unification]
     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
       | tc1 == tc2
-      = return $ mkReflCo Nominal ty1
+      = return $ mkNomReflCo ty1
 
         -- See Note [Expanding synonyms during unification]
         --
@@ -1302,14 +1415,6 @@ uType t_or_k origin orig_ty1 orig_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
-           ; return (mkCoherenceLeftCo co_tys co1) }
-
-    go t1 (CastTy t2 co2)
-      = do { co_tys <- go t1 t2
-           ; return (mkCoherenceRightCo co_tys co2) }
-
         -- Functions (or predicate functions) just check the two parts
     go (FunTy fun1 arg1) (FunTy fun2 arg2)
       = do { co_l <- uType t_or_k origin fun1 fun2
@@ -1345,12 +1450,12 @@ uType t_or_k origin orig_ty1 orig_ty2
 
     go (AppTy s1 t1) (TyConApp tc2 ts2)
       | Just (ts2', t2') <- snocView ts2
-      = ASSERT( mightBeUnsaturatedTyCon tc2 )
+      = ASSERT( not (mustBeSaturated tc2) )
         go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
 
     go (TyConApp tc1 ts1) (AppTy s2 t2)
       | Just (ts1', t1') <- snocView ts1
-      = ASSERT( mightBeUnsaturatedTyCon tc1 )
+      = ASSERT( not (mustBeSaturated tc1) )
         go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
 
     go (CoercionTy co1) (CoercionTy co2)
@@ -1424,6 +1529,9 @@ We expand synonyms during unification, but:
    more likely that the inferred types will mention type synonyms
    understandable to the user
 
+ * Similarly, we expand *after* the CastTy case, just in case the
+   CastTy wraps a variable.
+
  * We expand *before* the TyConApp case.  For example, if we have
       type Phantom a = Int
    and are unifying
@@ -1531,20 +1639,26 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
     go dflags cur_lvl
       | canSolveByUnification cur_lvl tv1 ty2
       , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
-      = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
+      = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
+           ; traceTc "uUnfilledVar2 ok" $
+             vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
+                  , ppr ty2 <+> dcolon <+> ppr (tcTypeKind  ty2)
+                  , ppr (isTcReflCo co_k), ppr co_k ]
+
            ; 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
+
+             else defer } -- This cannot be solved now.  See TcCanonical
+                          -- Note [Equalities with incompatible kinds]
 
       | otherwise
-      = defer
+      = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
                -- Occurs check or an untouchable: just defer
                -- NB: occurs check isn't necessarily fatal:
                --     eg tv1 occured in type family parameter
+            ; defer }
 
     ty1 = mkTyVarTy tv1
     kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
@@ -1553,64 +1667,113 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
 
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
 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
-      -- But see Note [Avoid unnecessary swaps]
-  = case metaTyVarTcLevel_maybe tv2 of
-      Nothing   -> False
-      Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
-                | lvl1 `strictlyDeeperThan` lvl2 -> False
-                | otherwise                      -> nicer_to_update tv2
-
-  -- So tv1 is not a meta tyvar
-  -- If only one is a meta tyvar, put it on the left
-  -- This is not because it'll be solved; but because
-  -- the floating step looks for meta tyvars on the left
-  | isMetaTyVar tv2 = True
-
-  -- So neither is a meta tyvar (including FlatMetaTv)
-
-  -- If only one is a flatten skolem, put it on the left
-  -- See Note [Eliminate flat-skols]
-  | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
+  -- Level comparison: see Note [TyVar/TyVar orientation]
+  | lvl1 `strictlyDeeperThan` lvl2 = False
+  | lvl2 `strictlyDeeperThan` lvl1 = True
 
-  | otherwise = False
+  -- Priority: see Note [TyVar/TyVar orientation]
+  | pri1 > pri2 = False
+  | pri2 > pri1 = True
 
-  where
-    nicer_to_update tv2
-      =  (isSigTyVar tv1                 && not (isSigTyVar tv2))
-      || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
+  -- Names: see Note [TyVar/TyVar orientation]
+  | isSystemName tv2_name, not (isSystemName tv1_name) = True
 
--- @trySpontaneousSolve wi@ solves equalities where one side is a
--- touchable unification variable.
--- Returns True <=> spontaneous solve happened
-canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
-canSolveByUnification tclvl tv xi
-  | isTouchableMetaTyVar tclvl tv
-  = case metaTyVarInfo tv of
-      SigTv -> is_tyvar xi
-      _     -> True
+  | otherwise = False
 
-  | otherwise    -- Untouchable
-  = False
   where
-    is_tyvar xi
-      = case tcGetTyVar_maybe xi of
-          Nothing -> False
-          Just tv -> case tcTyVarDetails tv of
-                       MetaTv { mtv_info = info }
-                                   -> case info of
-                                        SigTv -> True
-                                        _     -> False
-                       SkolemTv {} -> True
-                       RuntimeUnk  -> True
-
-{- Note [Fmv Orientation Invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    lvl1 = tcTyVarLevel tv1
+    lvl2 = tcTyVarLevel tv2
+    pri1 = lhsPriority tv1
+    pri2 = lhsPriority tv2
+    tv1_name = Var.varName tv1
+    tv2_name = Var.varName tv2
+
+
+lhsPriority :: TcTyVar -> Int
+-- Higher => more important to be on the LHS
+-- See Note [TyVar/TyVar orientation]
+lhsPriority tv
+  = ASSERT2( isTyVar tv, ppr tv)
+    case tcTyVarDetails tv of
+      RuntimeUnk  -> 0
+      SkolemTv {} -> 0
+      MetaTv { mtv_info = info } -> case info of
+                                     FlatSkolTv -> 1
+                                     TyVarTv    -> 2
+                                     TauTv      -> 3
+                                     FlatMetaTv -> 4
+{- Note [TyVar/TyVar orientation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)?
+This is a surprisingly tricky question!
+
+First note: only swap if you have to!
+   See Note [Avoid unnecessary swaps]
+
+So we look for a positive reason to swap, using a three-step test:
+
+* Level comparison. If 'a' has deeper level than 'b',
+  put 'a' on the left.  See Note [Deeper level on the left]
+
+* Priority.  If the levels are the same, look at what kind of
+  type variable it is, using 'lhsPriority'
+
+  - FlatMetaTv: Always put on the left.
+    See Note [Fmv Orientation Invariant]
+    NB: FlatMetaTvs always have the current level, never an
+        outer one.  So nothing can be deeper than a FlatMetaTv
+
+
+  - TyVarTv/TauTv: if we have  tyv_tv ~ tau_tv, put tau_tv
+                   on the left because there are fewer
+                   restrictions on updating TauTvs
+
+  - TyVarTv/TauTv:  put on the left either
+     a) Because it's touchable and can be unified, or
+     b) Even if it's not touchable, TcSimplify.floatEqualities
+        looks for meta tyvars on the left
+
+  - FlatSkolTv: Put on the left in preference to a SkolemTv
+                See Note [Eliminate flat-skols]
+
+* Names. If the level and priority comparisons are all
+  equal, try to eliminate a TyVars with a System Name in
+  favour of ones with a Name derived from a user type signature
+
+* Age.  At one point in the past we tried to break any remaining
+  ties by eliminating the younger type variable, based on their
+  Uniques.  See Note [Eliminate younger unification variables]
+  (which also explains why we don't do this any more)
+
+Note [Deeper level on the left]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The most important thing is that we want to put tyvars with
+the deepest level on the left.  The reason to do so differs for
+Wanteds and Givens, but either way, deepest wins!  Simple.
+
+* Wanteds.  Putting the deepest variable on the left maximise the
+  chances that it's a touchable meta-tyvar which can be solved.
+
+* Givens. Suppose we have something like
+     forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2]
+
+  If we orient the Given a[2] on the left, we'll rewrite the Wanted to
+  (beta[1] ~ b[1]), and that can float out of the implication.
+  Otherwise it can't.  By putting the deepest variable on the left
+  we maximise our changes of eliminating skolem capture.
+
+  See also TcSMonad Note [Let-bound skolems] for another reason
+  to orient with the deepest skolem on the left.
+
+  IMPORTANT NOTE: this test does a level-number comparison on
+  skolems, so it's important that skolems have (accurate) level
+  numbers.
+
+See Trac #15009 for an further analysis of why "deepest on the left"
+is a good plan.
+
+Note [Fmv Orientation Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    * We always orient a constraint
         fmv ~ alpha
      with fmv on the left, even if alpha is
@@ -1643,14 +1806,88 @@ T10226, T10009.)
           [WD] F fmv ~ fmv, [WD] fmv ~ a
     And now we are stuck.
 
-So instead the Fmv Orientation Invariant puts te fmv on the
+So instead the Fmv Orientation Invariant puts the 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]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Eliminate flat-skols]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have  [G] Num (F [a])
+then we flatten to
+     [G] Num fsk
+     [G] F [a] ~ fsk
+where fsk is a flatten-skolem (FlatSkolTv). Suppose we have
+      type instance F [a] = a
+then we'll reduce the second constraint to
+     [G] a ~ fsk
+and then replace all uses of 'a' with fsk.  That's bad because
+in error messages instead of saying 'a' we'll say (F [a]).  In all
+places, including those where the programmer wrote 'a' in the first
+place.  Very confusing!  See Trac #7862.
+
+Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate
+the fsk.
+
+Note [Avoid unnecessary swaps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we swap without actually improving matters, we can get an infinite loop.
+Consider
+    work item:  a ~ b
+   inert item:  b ~ c
+We canonicalise the work-item to (a ~ c).  If we then swap it before
+adding to the inert set, we'll add (c ~ a), and therefore kick out the
+inert guy, so we get
+   new work item:  b ~ c
+   inert item:     c ~ a
+And now the cycle just repeats
+
+Note [Eliminate younger unification variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given a choice of unifying
+     alpha := beta   or   beta := alpha
+we try, if possible, to eliminate the "younger" one, as determined
+by `ltUnique`.  Reason: the younger one is less likely to appear free in
+an existing inert constraint, and hence we are less likely to be forced
+into kicking out and rewriting inert constraints.
+
+This is a performance optimisation only.  It turns out to fix
+Trac #14723 all by itself, but clearly not reliably so!
+
+It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars).
+But, to my surprise, it didn't seem to make any significant difference
+to the compiler's performance, so I didn't take it any further.  Still
+it seemed to too nice to discard altogether, so I'm leaving these
+notes.  SLPJ Jan 18.
+-}
+
+-- @trySpontaneousSolve wi@ solves equalities where one side is a
+-- touchable unification variable.
+-- Returns True <=> spontaneous solve happened
+canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
+canSolveByUnification tclvl tv xi
+  | isTouchableMetaTyVar tclvl tv
+  = case metaTyVarInfo tv of
+      TyVarTv -> is_tyvar xi
+      _       -> True
+
+  | otherwise    -- Untouchable
+  = False
+  where
+    is_tyvar xi
+      = case tcGetTyVar_maybe xi of
+          Nothing -> False
+          Just tv -> case tcTyVarDetails tv of
+                       MetaTv { mtv_info = info }
+                                   -> case info of
+                                        TyVarTv -> True
+                                        _       -> False
+                       SkolemTv {} -> True
+                       RuntimeUnk  -> True
+
+{- Note [Prevent unification with type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We prevent unification with type families because of an uneasy compromise.
 It's perfectly sound to unify with type families, and it even improves the
 error messages in the testsuite. It also modestly improves performance, at
@@ -1777,42 +2014,48 @@ lookupTcTyVar tyvar
 Note [Unifying untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We treat an untouchable type variable as if it was a skolem.  That
-ensures it won't unify with anything.  It's a slight had, because
+ensures it won't unify with anything.  It's a slight hack, because
 we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
 -- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Outputable fun
-                     => fun             -- ^ type, only for errors
-                     -> TcKind          -- ^ function kind
-                     -> TcM (Coercion, TcKind, TcKind)
-                                  -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind hs_ty = go
+matchExpectedFunKind
+  :: Outputable fun
+  => fun             -- ^ type, only for errors
+  -> Arity           -- ^ n: number of desired arrows
+  -> TcKind          -- ^ fun_ kind
+  -> TcM Coercion    -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res)
+
+matchExpectedFunKind hs_ty n k = go n k
   where
-    go k | Just k' <- tcView k = go k'
+    go 0 k = return (mkNomReflCo k)
 
-    go k@(TyVarTy kvar)
-      | isTcTyVar kvar, isMetaTyVar kvar
+    go n k | Just k' <- tcView k = go n k'
+
+    go n k@(TyVarTy kvar)
+      | isMetaTyVar kvar
       = do { maybe_kind <- readMetaTyVar kvar
            ; case maybe_kind of
-                Indirect fun_kind -> go fun_kind
-                Flexi ->             defer k }
+                Indirect fun_kind -> go n fun_kind
+                Flexi ->             defer n k }
+
+    go n (FunTy arg res)
+      = do { co <- go (n-1) res
+           ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) }
 
-    go k@(FunTy arg res) = return (mkNomReflCo k, arg, res)
-    go other             = defer other
+    go n other
+     = defer n other
 
-    defer k
-      = do { arg_kind <- newMetaKindVar
-           ; res_kind <- newMetaKindVar
-           ; let new_fun = mkFunTy arg_kind res_kind
+    defer k
+      = do { arg_kinds <- newMetaKindVars n
+           ; res_kind  <- newMetaKindVar
+           ; let new_fun = mkFunTys arg_kinds res_kind
                  origin  = TypeEqOrigin { uo_actual   = k
                                         , uo_expected = new_fun
                                         , uo_thing    = Just (ppr hs_ty)
                                         , uo_visible  = True
                                         }
-           ; co <- uType KindLevel origin k new_fun
-           ; return (co, arg_kind, res_kind) }
-
+           ; uType KindLevel origin k new_fun }
 
 {- *********************************************************************
 *                                                                      *
@@ -1821,38 +2064,12 @@ matchExpectedFunKind hs_ty = go
 ********************************************************************* -}
 
 
-{- 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]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{-  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
+but we must not make the mistake of actually 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.
@@ -1919,7 +2136,7 @@ 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
+      OC_Occurs -> case occCheckExpand [tv] ty of
                      Nothing -> OC_Occurs
                      Just _  -> OC_OK ()
 
@@ -1957,7 +2174,7 @@ metaTyVarUpdateOK dflags tv ty
          -- See Note [Prevent unification with type families]
       OC_OK _   -> Just ty
       OC_Bad    -> Nothing  -- forall or type function
-      OC_Occurs -> occCheckExpand tv ty
+      OC_Occurs -> occCheckExpand [tv] ty
 
 preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
 -- A quick check for
@@ -1992,7 +2209,7 @@ preCheck dflags ty_fam_ok tv ty
     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)
+    fast_check (ForAllTy (Bndr tv' _) ty)
        | not impredicative_ok = OC_Bad
        | tv == tv'            = ok
        | otherwise = do { fast_check_occ (tyVarKind tv')
@@ -2018,120 +2235,10 @@ preCheck dflags ty_fam_ok tv ty
       | 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
+      MetaTv { mtv_info = TyVarTv }    -> False
+      MetaTv { mtv_info = TauTv }      -> xopt LangExt.ImpredicativeTypes dflags
+      _other                           -> True
           -- We can have non-meta tyvars in given constraints