Fix impredicativity (again)

This patch fixes Trac #12616.

Dignosis.  In TcUnify.tc_sub_type_ds we were going to some trouble to
support co- and contra-variance even for impredicative types.  With
-XImpredicativeTYpes, this allowed a unification variable to be
unified with a polytype (probably wrongly) and that caused later
trouble in the constraint solver, where -XImpredicativeTypes was /not/
on.  In effect, -XImpredicativeTypes can't be switched on locally.

Why did we want ImpredicativeTypes locally?  Because the program
generated by GND for a higher-rank method involved impredicative
instantation of 'coerce':
      op = coerce op   -- where op has a higher rank type
See Note [Newtype-deriving instances] in TcGenDeriv.

Cure.

1.  It is ghastly to rely on ImpredicativeTypes (a 100% flaky
    feature) to instantiate coerce polymorphically.  Happily we
    now have Visible Type Application, so I've used that instead
    which should be solid and reliable.

2.  I deleted the code in tc_sub_type_ds that allows the constraint
    solver to "look through" a unification variable to find a
    polytype.  That used to be essential in the days of ReturnTv,
    but it's utterly unreliable and should be consigned to the dustbin
    of history.  (We have ExpType now for the essential uses.)

Tests involving ImpredicativeTypes are affected, but I'm not worried
about them... it's advertised as a feature you can't rely on, and
I want to reform it outright.

24 files changed, 230 insertions, 106 deletions

diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index 5e5127295d..07edf0d333 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -32,7 +32,7 @@ module HsUtils(
   nlHsIntLit, nlHsVarApps,
   nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList,
   mkLHsTupleExpr, mkLHsVarTuple, missingTupArg,
-  toLHsSigWcType,
+  typeToLHsType,
 
   -- * Constructing general big tuples
   -- $big_tuples
@@ -597,14 +597,14 @@ mkClassOpSigs sigs
     fiddle (L loc (TypeSig nms ty)) = L loc (ClassOpSig False nms (dropWildCards ty))
     fiddle sig                      = sig
 
-toLHsSigWcType :: Type -> LHsSigWcType RdrName
+typeToLHsType :: Type -> LHsType RdrName
 -- ^ Converting a Type to an HsType RdrName
 -- This is needed to implement GeneralizedNewtypeDeriving.
 --
 -- Note that we use 'getRdrName' extensively, which
 -- generates Exact RdrNames rather than strings.
-toLHsSigWcType ty
-  = mkLHsSigWcType (go ty)
+typeToLHsType ty
+  = go ty
   where
     go :: Type -> LHsType RdrName
     go ty@(FunTy arg _)
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 0b5f07301a..858d9209df 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -2274,6 +2274,8 @@ genInst spec@(DS { ds_tvs = tvs, ds_tc = rep_tycon
                         , ib_pragmas    = []
                         , ib_extensions = [ LangExt.ImpredicativeTypes
                                           , LangExt.RankNTypes ]
+                          -- Both these flags are needed for higher-rank uses of coerce
+                          -- See Note [Newtype-deriving instances] in TcGenDeriv
                         , ib_derived    = True } }
                 , emptyBag
                 , Just $ getName $ head $ tyConDataCons rep_tycon ) }
diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs
index 69f9d983f7..e7d7bd3143 100644
--- a/compiler/typecheck/TcGenDeriv.hs
+++ b/compiler/typecheck/TcGenDeriv.hs
@@ -576,7 +576,7 @@ unliftedCompare lt_op eq_op a_expr b_expr lt eq gt
                         -- mean more tests (dynamically)
         nlHsIf (ascribeBool $ genPrimOpApp a_expr eq_op b_expr) eq gt
   where
-    ascribeBool e = nlExprWithTySig e (toLHsSigWcType boolTy)
+    ascribeBool e = nlExprWithTySig e boolTy
 
 nlConWildPat :: DataCon -> LPat RdrName
 -- The pattern (K {})
@@ -2213,31 +2213,30 @@ coercing from.  So from, say,
   newtype T x = MkT <rep-ty>
 
   instance C a <rep-ty> => C a (T x) where
-    op = (coerce
-             (op :: a -> [<rep-ty>] -> Int)
-         ) :: a -> [T x] -> Int
+    op = coerce @ (a -> [<rep-ty>] -> Int)
+                @ (a -> [T x]      -> Int)
+                op
 
-Notice that we give the 'coerce' call two type signatures: one to
-fix the type of the inner call, and one for the expected type.  The outer
-type signature ought to be redundant, but may improve error messages.
-The inner one is essential to fix the type at which 'op' is called.
+Notice that we give the 'coerce' two explicitly-visible type arguments
+to say how it should be instantiated.  Recall
 
-See #8503 for more discussion.
-
-Here's a wrinkle. Supppose 'op' is locally overloaded:
+  coerce :: Coeercible a b => a -> b
 
-  class C2 b where
-    op2 :: forall a. Eq a => a -> [b] -> Int
+By giving it explicit type arguments we deal with the case where
+'op' has a higher rank type, and so we must instantiae 'coerce' with
+a polytype.  E.g.
+   class C a where op :: forall b. a -> b -> b
+   newtype T x = MkT <rep-ty>
+   instance C <rep-ty> => C (T x) where
+     op = coerce @ (forall b. <rep-ty> -> b -> b)
+                 @ (forall b. T x -> b -> b)
+                op
 
-Then we could do exactly as above, but it's a bit redundant to
-instantiate op, then re-generalise with the inner signature.
-(The inner sig is only there to fix the type at which 'op' is
-called.)  So we just instantiate the signature, and add
+The type checker checks this code, and it currently requires
+-XImpredicativeTypes to permit that polymorphic type instantiation,
+so ew have to switch that flag on locally in TcDeriv.genInst.
 
-  instance C2 <rep-ty> => C2 (T x) where
-    op2 = (coerce
-             (op2 :: a -> [<rep-ty>] -> Int)
-          ) :: forall a. Eq a => a -> [T x] -> Int
+See #8503 for more discussion.
 -}
 
 gen_Newtype_binds :: SrcSpan
@@ -2260,19 +2259,21 @@ gen_Newtype_binds loc cls inst_tvs cls_tys rhs_ty
       where
         Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs cls_tys rhs_ty meth_id
 
-        -- See "wrinkle" in Note [Newtype-deriving instances]
-        (_, _, from_ty') = tcSplitSigmaTy from_ty
-
         meth_RDR = getRdrName meth_id
 
-        rhs_expr = ( nlHsVar coerce_RDR
-                      `nlHsApp`
-                    (nlHsVar meth_RDR `nlExprWithTySig` toLHsSigWcType from_ty'))
-                  `nlExprWithTySig` toLHsSigWcType to_ty
+        rhs_expr = nlHsVar coerce_RDR `nlHsAppType` from_ty
+                                      `nlHsAppType` to_ty
+                                      `nlHsApp`     nlHsVar meth_RDR
 
+nlHsAppType :: LHsExpr RdrName -> Type -> LHsExpr RdrName
+nlHsAppType e s = noLoc (e `HsAppType` hs_ty)
+  where
+    hs_ty = mkHsWildCardBndrs (typeToLHsType s)
 
-nlExprWithTySig :: LHsExpr RdrName -> LHsSigWcType RdrName -> LHsExpr RdrName
-nlExprWithTySig e s = noLoc (ExprWithTySig e s)
+nlExprWithTySig :: LHsExpr RdrName -> Type -> LHsExpr RdrName
+nlExprWithTySig e s = noLoc (e `ExprWithTySig` hs_ty)
+  where
+    hs_ty = mkLHsSigWcType (typeToLHsType s)
 
 mkCoerceClassMethEqn :: Class   -- the class being derived
                      -> [TyVar] -- the tvs in the instance head
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b564f9fd9a..2712c4a5c5 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -721,27 +721,13 @@ 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)
@@ -1320,7 +1306,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 }
 
 ----------
diff --git a/testsuite/tests/boxy/Base1.hs b/testsuite/tests/boxy/Base1.hs
index 88e7e80f17..3f027bb93c 100644
--- a/testsuite/tests/boxy/Base1.hs
+++ b/testsuite/tests/boxy/Base1.hs
@@ -1,30 +1,33 @@
 {-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
 
-module Base1 where 
--- basic examples of impredicative instantiation of variables 
+-- Sept 16: now failing, beause I've furter reduced the scop
+--          of impredicative types
 
-data MEither a b = MLeft a 
-                 | MRight b 
+module Base1 where
+-- basic examples of impredicative instantiation of variables
+
+data MEither a b = MLeft a
+                 | MRight b
                  | MEmpty
 
-type Sid = forall a. a -> a 
+type Sid = forall a. a -> a
 
--- no need for impredicativity 
-test0 = MRight id 
+-- no need for impredicativity
+test0 = MRight id
 
--- requires impredicativity 
+-- requires impredicativity
 test1 :: Sid -> MEither Sid b
-test1 fid = MLeft fid 
+test1 fid = MLeft fid
 
-test2 :: MEither b Sid -> Maybe (Sid,Sid) 
-test2 m = case (test1 id) of 
-             MLeft x -> case m of 
-                          MRight y -> Just (x,y) 
-                          _ -> Nothing 
+test2 :: MEither b Sid -> Maybe (Sid,Sid)
+test2 m = case (test1 id) of
+             MLeft x -> case m of
+                          MRight y -> Just (x,y)
+                          _ -> Nothing
              _ -> Nothing
 
 test3 :: MEither a b -> b
-test3 (MRight x) = x 
+test3 (MRight x) = x
 
-test4 = test3 (test1 id) 
+test4 = test3 (test1 id)
 
diff --git a/testsuite/tests/boxy/T2193.hs b/testsuite/tests/boxy/T2193.hs
index 904a13721c..c36503eae7 100644
--- a/testsuite/tests/boxy/T2193.hs
+++ b/testsuite/tests/boxy/T2193.hs
@@ -1,5 +1,7 @@
 {-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
 
+-- Sept 16: now scraping through with -XImpredicateTypes
+
 module Main where
 
 data Foo x y = Foo {foo1 :: x, foo2 :: y}
diff --git a/testsuite/tests/boxy/all.T b/testsuite/tests/boxy/all.T
index d2be5e314b..99ab5367f2 100644
--- a/testsuite/tests/boxy/all.T
+++ b/testsuite/tests/boxy/all.T
@@ -1,6 +1,6 @@
 # Boxy-type tests
 
-test('Base1',    normal, compile, [''])
+test('Base1',    normal, compile_fail, [''])
 test('Church1',  expect_broken(4295), compile, [''])
 test('Church2',  expect_broken(1330), compile_fail, [''])
 test('PList1',   expect_broken(4295), compile, [''])
@@ -8,4 +8,4 @@ test('PList2',   expect_broken(4295), compile, [''])
 test('SystemF',  expect_broken(4295), compile, [''])
 test('boxy',     expect_broken(4295), compile, [''])
 test('Compose',  normal, compile, [''])
-test('T2193',    expect_broken(4295), compile_and_run, [''])
+test('T2193',    normal, compile_and_run, [''])
diff --git a/testsuite/tests/deriving/should_compile/T12616.hs b/testsuite/tests/deriving/should_compile/T12616.hs
new file mode 100644
index 0000000000..0d2b04dac5
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T12616.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T12616 where
+
+type m ~> n = forall a. m a -> n a
+
+class MonadTrans t where
+  -- > this line works:
+  -- lift :: (Monad m) => m a -> t m a
+  -- > this line doesn't:
+  lift :: (Monad m) => m ~> t m
+
+data StateT s m a = StateT { runStateT :: s -> m (a, s) }
+
+instance MonadTrans (StateT s) where
+  lift xM = StateT $ \ s -> do { x <- xM ; return (x,s) }
+
+newtype OtherStateT s m a = OtherStateT { runOtherStateT :: StateT s m a }
+  deriving (MonadTrans)
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 6beae8abee..1b4c8b36ad 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -73,3 +73,4 @@ test('T11833', normal, compile, [''])
 test('T12245', normal, compile, [''])
 test('T12399', normal, compile, [''])
 test('T12583', normal, compile, [''])
+test('T12616', normal, compile, [''])
diff --git a/testsuite/tests/deriving/should_fail/T4846.stderr b/testsuite/tests/deriving/should_fail/T4846.stderr
index 3d3ccc4b86..9642132f99 100644
--- a/testsuite/tests/deriving/should_fail/T4846.stderr
+++ b/testsuite/tests/deriving/should_fail/T4846.stderr
@@ -3,9 +3,9 @@ T4846.hs:29:1: error:
     • Couldn't match type ‘Bool’ with ‘BOOL’
         arising from a use of ‘GHC.Prim.coerce’
     • In the expression:
-          GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
+        GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr
       In an equation for ‘mkExpr’:
-          mkExpr = GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL
+          mkExpr = GHC.Prim.coerce @(Expr Bool) @(Expr BOOL) mkExpr
       When typechecking the code for ‘mkExpr’
         in a derived instance for ‘B BOOL’:
         To see the code I am typechecking, use -ddump-deriv
diff --git a/testsuite/tests/typecheck/should_compile/T11319.hs b/testsuite/tests/typecheck/should_compile/T11319.hs
index 5f09d22f33..30879a30a1 100644
--- a/testsuite/tests/typecheck/should_compile/T11319.hs
+++ b/testsuite/tests/typecheck/should_compile/T11319.hs
@@ -1,5 +1,8 @@
 {-# LANGUAGE ImpredicativeTypes #-}
 
+-- Sept 16: this compiles again now, because I've weakened
+--          ImpredicativeTypes a lot
+
 module T11319 where
 
 f :: Monad m => m (Maybe a)
diff --git a/testsuite/tests/typecheck/should_compile/T12644.hs b/testsuite/tests/typecheck/should_compile/T12644.hs
new file mode 100644
index 0000000000..622012286c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12644.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module T12644 where
+
+data T a = T1 Int
+
+instance Show (T a) where
+  show (T1 x) = show x
+
+t1 :: T a
+t1 = T1 1
+
+f :: String
+f = show t1
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 40d986a617..28d7369cae 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -504,7 +504,7 @@ test('T11462',
 test('T11480', normal, compile, [''])
 test('RebindHR', normal, compile, [''])
 test('RebindNegate', normal, compile, [''])
-test('T11319', expect_broken(11319), compile, [''])
+test('T11319', normal, compile, [''])
 test('T11397', normal, compile, [''])
 test('T11458', normal, compile, [''])
 test('T11524', normal, compile, [''])
@@ -541,3 +541,4 @@ test('T10635', normal, compile, [''])
 test('T12170b', normal, compile, [''])
 test('T12466', normal, compile, [''])
 test('T12466a', normal, compile, [''])
+test('T12644', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc211.hs b/testsuite/tests/typecheck/should_compile/tc211.hs
index 7dc45e5be7..e132cd8c80 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.hs
+++ b/testsuite/tests/typecheck/should_compile/tc211.hs
@@ -6,6 +6,9 @@
 -- Here are a bunch of tests for impredicative polymorphism
 -- mainly written by Dimitrios
 
+-- Sept 16: I'm just accepting the bizarre output.
+-- None of this is right
+
 module ShouldCompile where
 
 xs :: [forall a. a->a]
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index 89c82c4f9a..5cda3a1e97 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,9 +1,79 @@
 
-tc211.hs:73:9: error:
-    • Couldn't match type ‘forall a2. a2 -> a2’ with ‘a1 -> a1’
+tc211.hs:20:8: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘a1 -> a1’
+    • In the expression:
+          (:) ::
+            (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
+      In the expression:
+        ((:) ::
+           (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
+          (head foo) foo
+      In an equation for ‘bar’:
+          bar
+            = ((:) ::
+                 (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
+                (head foo) foo
+
+tc211.hs:25:8: error:
+    • Couldn't match type ‘a3 -> a3’ with ‘forall a. a -> a’
+      Expected type: [forall a. a -> a]
+        Actual type: [a3 -> a3]
+    • In the expression: (head foo) : (tail foo)
+      In an equation for ‘barr’: barr = (head foo) : (tail foo)
+
+tc211.hs:25:20: error:
+    • Couldn't match type ‘forall a. a -> a’ with ‘a3 -> a3’
+      Expected type: [a3 -> a3]
+        Actual type: [forall a. a -> a]
+    • In the second argument of ‘(:)’, namely ‘(tail foo)’
+      In the expression: (head foo) : (tail foo)
+      In an equation for ‘barr’: barr = (head foo) : (tail foo)
+
+tc211.hs:62:18: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘a0 -> a0’
+    • In the expression:
+          Cons ::
+            (forall a. a -> a)
+            -> List (forall a. a -> a) -> List (forall a. a -> a)
+      In an equation for ‘cons’:
+          cons
+            = Cons ::
+                (forall a. a -> a)
+                -> List (forall a. a -> a) -> List (forall a. a -> a)
+      In the expression:
+        let
+          cons
+            = Cons ::
+                (forall a. a -> a)
+                -> List (forall a. a -> a) -> List (forall a. a -> a)
+        in cons (\ x -> x) Nil
+
+tc211.hs:68:8: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘a2 -> a2’
+    • In the expression:
+          Cons ::
+            (forall a. a -> a)
+            -> List (forall a. a -> a) -> List (forall a. a -> a)
+      In the expression:
+        (Cons ::
+           (forall a. a -> a)
+           -> List (forall a. a -> a) -> List (forall a. a -> a))
+          (\ x -> x) Nil
+      In an equation for ‘xs2’:
+          xs2
+            = (Cons ::
+                 (forall a. a -> a)
+                 -> List (forall a. a -> a) -> List (forall a. a -> a))
+                (\ x -> x) Nil
+
+tc211.hs:76:9: error:
+    • Couldn't match type ‘forall a5. a5 -> a5’ with ‘a4 -> a4’
       Expected type: List (forall a. a -> a)
-                     -> (forall a. a -> a) -> a1 -> a1
-        Actual type: List (a1 -> a1) -> (a1 -> a1) -> a1 -> a1
+                     -> (forall a. a -> a) -> a4 -> a4
+        Actual type: List (a4 -> a4) -> (a4 -> a4) -> a4 -> a4
     • In the expression:
           foo2 ::
             List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr
index e002759ba0..7a27229369 100644
--- a/testsuite/tests/typecheck/should_fail/T10619.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10619.stderr
@@ -20,14 +20,9 @@ T10619.hs:9:15: error:
         foo :: t -> (b -> b) -> b -> b (bound at T10619.hs:8:1)
 
 T10619.hs:14:15: error:
-    • Couldn't match type ‘b’ with ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
-        a type expected by the context:
-          a -> a
-        at T10619.hs:14:15-65
+    • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
       Expected type: (b -> b) -> b -> b
-        Actual type: (forall a. a -> a) -> forall b. b -> b
+        Actual type: (forall a. a -> a) -> b -> b
     • In the expression:
         ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
       In the expression:
@@ -56,14 +51,9 @@ T10619.hs:16:13: error:
         baz :: Bool -> (b -> b) -> b -> b (bound at T10619.hs:16:1)
 
 T10619.hs:20:14: error:
-    • Couldn't match type ‘b’ with ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
-        a type expected by the context:
-          a -> a
-        at T10619.hs:20:14-64
+    • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
       Expected type: (b -> b) -> b -> b
-        Actual type: (forall a. a -> a) -> forall b. b -> b
+        Actual type: (forall a. a -> a) -> b -> b
     • In the expression:
           (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
       In an equation for ‘quux’:
diff --git a/testsuite/tests/typecheck/should_fail/T2846b.stderr b/testsuite/tests/typecheck/should_fail/T2846b.stderr
index 371d0ce5ca..8c52fd7d33 100644
--- a/testsuite/tests/typecheck/should_fail/T2846b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2846b.stderr
@@ -1,6 +1,7 @@
 
 T2846b.hs:5:5: error:
-    • No instance for (Show (forall a. [Num a => a]))
+    • No instance for (Show (Num a0 => a0))
         arising from a use of ‘show’
+        (maybe you haven't applied a function to enough arguments?)
     • In the expression: show ([1, 2, 3] :: [Num a => a])
       In an equation for ‘f’: f = show ([1, 2, 3] :: [Num a => a])
diff --git a/testsuite/tests/typecheck/should_fail/T8428.stderr b/testsuite/tests/typecheck/should_fail/T8428.stderr
index 97cd9f7806..ce83c3efe5 100644
--- a/testsuite/tests/typecheck/should_fail/T8428.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8428.stderr
@@ -1,8 +1,11 @@
 
 T8428.hs:11:19: error:
-    • Couldn't match type ‘forall s1. ST s1’ with ‘ST s’
+    • Couldn't match type ‘(forall s. ST s) a’ with ‘forall s. ST s a’
       Expected type: IdentityT (forall s. ST s) a -> forall s. ST s a
         Actual type: IdentityT (forall s. ST s) a -> (forall s. ST s) a
     • In the second argument of ‘(.)’, namely ‘runIdentityT’
       In the expression: runST . runIdentityT
       In an equation for ‘runIdST’: runIdST = runST . runIdentityT
+    • Relevant bindings include
+        runIdST :: IdentityT (forall s. ST s) a -> a
+          (bound at T8428.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 62734f861c..c5596d6ee1 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -147,7 +147,7 @@ test('tcfail160', normal, compile_fail, [''])
 test('tcfail161', normal, compile_fail, [''])
 test('tcfail162', normal, compile_fail, [''])
 test('tcfail164', normal, compile_fail, [''])
-test('tcfail165', normal, compile, [''])
+test('tcfail165', normal, compile_fail, [''])
 test('tcfail166', normal, compile_fail, [''])
 test('tcfail167', normal, compile_fail, [''])
 test('tcfail168', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail016.stderr b/testsuite/tests/typecheck/should_fail/tcfail016.stderr
index 3430c2d830..20b9e0fa36 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail016.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail016.stderr
@@ -1,6 +1,6 @@
 
 tcfail016.hs:8:1: error:
-    • Couldn't match type ‘(a, Expr a)’ with ‘Expr a’
+    • Couldn't match type ‘Expr a’ with ‘(a, Expr a)’
       Expected type: AnnExpr a -> [[Char]]
         Actual type: Expr a -> [[Char]]
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail165.hs b/testsuite/tests/typecheck/should_fail/tcfail165.hs
index 8b4cabdc8e..11c016b08b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail165.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail165.hs
@@ -10,8 +10,10 @@ import Control.Concurrent
 -- Actually (Dec 06) it succeeds now
 --
 -- In GHC 7.0 it fails again! (and rightly so)
-
+--
 -- With the Visible Type Application patch, this succeeds again.
+--
+-- Sept 16: fails again as it should
 
 foo = do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
          putMVar var (show :: forall b. Show b => b -> String)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail165.stderr b/testsuite/tests/typecheck/should_fail/tcfail165.stderr
new file mode 100644
index 0000000000..07d293dcd3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/tcfail165.stderr
@@ -0,0 +1,12 @@
+
+tcfail165.hs:19:23: error:
+    • Couldn't match expected type ‘forall a. Show a => a -> String’
+                  with actual type ‘b0 -> String’
+    • In the second argument of ‘putMVar’, namely
+        ‘(show :: forall b. Show b => b -> String)’
+      In a stmt of a 'do' block:
+        putMVar var (show :: forall b. Show b => b -> String)
+      In the expression:
+        do { var <- newEmptyMVar ::
+                      IO (MVar (forall a. Show a => a -> String));
+             putMVar var (show :: forall b. Show b => b -> String) }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.hs b/testsuite/tests/typecheck/should_fail/tcfail174.hs
index 41fc18fc66..85c5e1c961 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.hs
@@ -8,6 +8,8 @@ data Capture a = Base a
 g :: Capture (forall a . a ->  a)
 g = Base id  -- Fails; need a rigid signature on 'id'
     -- Actually, succeeds now, with visible type application
+    -- Disagree: should not succeed becuase it instantiates
+    --           Base with a forall type
 
 -- This function should definitely be rejected, with or without type signature
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index 653daaffbb..6cc3fffdd3 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -1,30 +1,37 @@
 
-tcfail174.hs:14:14: error:
+tcfail174.hs:9:5: error:
+    • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
+      Expected type: Capture (forall a. a -> a)
+        Actual type: Capture (a0 -> a0)
+    • In the expression: Base id
+      In an equation for ‘g’: g = Base id
+
+tcfail174.hs:16:14: error:
     • Couldn't match type ‘a’ with ‘a1’
         because type variable ‘a1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type a1 -> a1
-        at tcfail174.hs:14:1-14
+        at tcfail174.hs:16:1-14
       Expected type: Capture (forall x. x -> a)
         Actual type: Capture (forall a. a -> a)
     • In the first argument of ‘Capture’, namely ‘g’
       In the expression: Capture g
       In an equation for ‘h1’: h1 = Capture g
     • Relevant bindings include
-        h1 :: Capture a (bound at tcfail174.hs:14:1)
+        h1 :: Capture a (bound at tcfail174.hs:16:1)
 
-tcfail174.hs:17:14: error:
+tcfail174.hs:19:14: error:
     • Couldn't match type ‘a’ with ‘b’
       ‘a’ is a rigid type variable bound by
         the type a -> a at tcfail174.hs:1:1
       ‘b’ is a rigid type variable bound by
         the type signature for:
           h2 :: forall b. Capture b
-        at tcfail174.hs:16:1-15
+        at tcfail174.hs:18:1-15
       Expected type: Capture (forall x. x -> b)
         Actual type: Capture (forall a. a -> a)
     • In the first argument of ‘Capture’, namely ‘g’
       In the expression: Capture g
       In an equation for ‘h2’: h2 = Capture g
     • Relevant bindings include
-        h2 :: Capture b (bound at tcfail174.hs:17:1)
+        h2 :: Capture b (bound at tcfail174.hs:19:1)