A collection of type-inference refactorings.

This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.

1. Modify TcType.ExpType to make a distinct data type,
   InferResult for the Infer case, and consequential
   refactoring.

2. Define a new function TcUnify.fillInferResult, to fill in
   an InferResult. It uses TcMType.promoteTcType to promote
   the type to the level of the InferResult.
   See TcMType Note [Promoting a type]
   This refactoring is in preparation for an improvement
   to typechecking pattern bindings, coming next.

   I flirted with an elaborate scheme to give better
   higher rank inference, but it was just too complicated.
   See TcMType Note [Promotion and higher rank types]

3. Add to InferResult a new field ir_inst :: Bool to say
   whether or not the type used to fill in the
   InferResult should be deeply instantiated.  See
   TcUnify Note [Deep instantiation of InferResult].

4. Add a TcLevel to SkolemTvs. This will be useful generally

    - it's a fast way to see if the type
      variable escapes when floating (not used yet)

    - it provides a good consistency check when updating a
      unification variable (TcMType.writeMetaTyVarRef, the
      level_check_ok check)

   I originally had another reason (related to the flirting
   in (2), but I left it in because it seems like a step in
   the right direction.

5. Reduce and simplify the plethora of uExpType,
   tcSubType and related functions in TcUnify.  It was
   such an opaque mess and it's still not great, but it's
   better.

6. Simplify the uo_expected field of TypeEqOrigin.  Richard
   had generatlised it to a ExpType, but it was almost always
   a Check type.  Now it's back to being a plain TcType which
   is much, much easier.

7. Improve error messages by refraining from skolemisation when
   it's clear that there's an error: see
   TcUnify Note [Don't skolemise unnecessarily]

8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
   so I added it

9. Kill off tcs_used_tcvs.  Its purpose is to track the
   givens used by wanted constraints.  For dictionaries etc
   we do that via the free vars of the /bindings/ in the
   implication constraint ic_binds.  But for coercions we
   just do update-in-place in the type, rather than
   generating a binding.  So we need something analogous to
   bindings, to track what coercions we have added.

   That was the purpose of tcs_used_tcvs.  But it only
   worked for a /single/ iteration, whereas we may have
   multiple iterations of solving an implication.  Look
   at (the old) 'setImplicationStatus'.  If the constraint
   is unsolved, it just drops the used_tvs on the floor.
   If it becomes solved next time round, we'll pick up
   coercions used in that round, but ignore ones used in
   the first round.

   There was an outright bug.  Result = (potentialy) bogus
   unused-constraint errors.  Constructing a case where this
   actually happens seems quite trick so I did not do so.

   Solution: expand EvBindsVar to include the (free vars of
   the) coercions, so that the coercions are tracked in
   essentially the same way as the bindings.

   This turned out to be much simpler.  Less code, more
   correct.

10. Make the ic_binds field in an implication have type
      ic_binds :: EvBindsVar
    instead of (as previously)
       ic_binds :: Maybe EvBindsVar
    This is notably simpler, and faster to use -- less
    testing of the Maybe.  But in the occaional situation
    where we don't have anywhere to put the bindings, the
    belt-and-braces error check is lost.  So I put it back
    as an ASSERT in 'setImplicationStatus' (see the use of
    'termEvidenceAllowed')

All these changes led to quite bit of error message wibbling

55 files changed, 264 insertions, 225 deletions

diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr
index 20f04d01e7..6f9e16f2b4 100644
--- a/testsuite/tests/ado/ado004.stderr
+++ b/testsuite/tests/ado/ado004.stderr
@@ -30,9 +30,9 @@ TYPE SIGNATURES
     (Num t, Monad m) =>
     (t -> m a2) -> (a2 -> a2 -> m a1) -> m a1
   test6 ::
-    forall a (m :: * -> *) t.
+    forall a (m :: * -> *) p.
     (Num (m a), Monad m) =>
-    (m a -> m (m a)) -> t -> m a
+    (m a -> m (m a)) -> p -> m a
 TYPE CONSTRUCTORS
 COERCION AXIOMS
 Dependent modules: []
diff --git a/testsuite/tests/annotations/should_fail/annfail10.stderr b/testsuite/tests/annotations/should_fail/annfail10.stderr
index 6782f27228..6e7732f938 100644
--- a/testsuite/tests/annotations/should_fail/annfail10.stderr
+++ b/testsuite/tests/annotations/should_fail/annfail10.stderr
@@ -1,8 +1,8 @@
 
 annfail10.hs:9:1: error:
-    • Ambiguous type variable ‘t0’ arising from an annotation
-      prevents the constraint ‘(Data.Data.Data t0)’ from being solved.
-      Probable fix: use a type annotation to specify what ‘t0’ should be.
+    • Ambiguous type variable ‘p0’ arising from an annotation
+      prevents the constraint ‘(Data.Data.Data p0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instances exist:
         instance (Data.Data.Data a, Data.Data.Data b) =>
                  Data.Data.Data (Either a b)
@@ -15,9 +15,9 @@ annfail10.hs:9:1: error:
     • In the annotation: {-# ANN f 1 #-}
 
 annfail10.hs:9:11: error:
-    • Ambiguous type variable ‘t0’ arising from the literal ‘1’
-      prevents the constraint ‘(Num t0)’ from being solved.
-      Probable fix: use a type annotation to specify what ‘t0’ should be.
+    • Ambiguous type variable ‘p0’ arising from the literal ‘1’
+      prevents the constraint ‘(Num p0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instances exist:
         instance Num Integer -- Defined in ‘GHC.Num’
         instance Num Double -- Defined in ‘GHC.Float’
diff --git a/testsuite/tests/driver/T2182.stderr b/testsuite/tests/driver/T2182.stderr
index b5a5f1d349..770135a338 100644
--- a/testsuite/tests/driver/T2182.stderr
+++ b/testsuite/tests/driver/T2182.stderr
@@ -1,24 +1,24 @@
 
 T2182.hs:5:5: error:
-    No instance for (Show (t1 -> t1)) arising from a use of ‘show’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: show (\ x -> x)
-    In an equation for ‘y’: y = show (\ x -> x)
+    • No instance for (Show (p1 -> p1)) arising from a use of ‘show’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: show (\ x -> x)
+      In an equation for ‘y’: y = show (\ x -> x)
 
 T2182.hs:6:5: error:
-    No instance for (Eq (t0 -> t0)) arising from a use of ‘==’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: (\ x -> x) == (\ y -> y)
-    In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
+    • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: (\ x -> x) == (\ y -> y)
+      In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
 
 T2182.hs:5:5: error:
-    No instance for (Show (t1 -> t1)) arising from a use of ‘show’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: show (\ x -> x)
-    In an equation for ‘y’: y = show (\ x -> x)
+    • No instance for (Show (p1 -> p1)) arising from a use of ‘show’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: show (\ x -> x)
+      In an equation for ‘y’: y = show (\ x -> x)
 
 T2182.hs:6:5: error:
-    No instance for (Eq (t0 -> t0)) arising from a use of ‘==’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: (\ x -> x) == (\ y -> y)
-    In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
+    • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’
+        (maybe you haven't applied a function to enough arguments?)
+    • In the expression: (\ x -> x) == (\ y -> y)
+      In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 056d451a09..41322f9cbc 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -1,19 +1,19 @@
 
 gadt-escape1.hs:19:58: error:
-    • Couldn't match type ‘t’ with ‘ExpGADT Int’
-        ‘t’ is untouchable
-          inside the constraints: t1 ~ Int
+    • Couldn't match type ‘p’ with ‘ExpGADT Int’
+        ‘p’ is untouchable
+          inside the constraints: t ~ Int
           bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
                    in a case alternative
           at gadt-escape1.hs:19:43-50
-      ‘t’ is a rigid type variable bound by
-        the inferred type of weird1 :: t at gadt-escape1.hs:19:1-58
+      ‘p’ is a rigid type variable bound by
+        the inferred type of weird1 :: p at gadt-escape1.hs:19:1-58
       Possible fix: add a type signature for ‘weird1’
-      Expected type: t
-        Actual type: ExpGADT t1
+      Expected type: p
+        Actual type: ExpGADT t
     • In the expression: a
       In a case alternative: Hidden (ExpInt _) a -> a
       In the expression:
         case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
     • Relevant bindings include
-        weird1 :: t (bound at gadt-escape1.hs:19:1)
+        weird1 :: p (bound at gadt-escape1.hs:19:1)
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index e304430b51..6673ff68b0 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -1,17 +1,17 @@
 
 gadt13.hs:15:13: error:
-    • Couldn't match expected type ‘t’
+    • Couldn't match expected type ‘p’
                   with actual type ‘String -> [Char]’
-        ‘t’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor: I :: Int -> Term Int,
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
-      ‘t’ is a rigid type variable bound by
-        the inferred type of shw :: Term a -> t at gadt13.hs:15:1-30
+      ‘p’ is a rigid type variable bound by
+        the inferred type of shw :: Term a -> p at gadt13.hs:15:1-30
       Possible fix: add a type signature for ‘shw’
     • Possible cause: ‘(.)’ is applied to too many arguments
       In the expression: ("I " ++) . shows t
       In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
     • Relevant bindings include
-        shw :: Term a -> t (bound at gadt13.hs:15:1)
+        shw :: Term a -> p (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index e66226eaea..f75e8c5bff 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,20 +1,20 @@
 
 gadt7.hs:16:38: error:
-    • Couldn't match expected type ‘t’ with actual type ‘t1’
-        ‘t’ is untouchable
+    • Couldn't match expected type ‘p’ with actual type ‘p1’
+        ‘p1’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor: K :: T Int,
                    in a case alternative
           at gadt7.hs:16:33
-      ‘t’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
+      ‘p’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
       In the expression: case t1 of { K -> y1 }
     • Relevant bindings include
-        y1 :: t1 (bound at gadt7.hs:16:16)
-        y :: t1 (bound at gadt7.hs:16:7)
-        i1b :: T a -> t1 -> t (bound at gadt7.hs:16:1)
+        y1 :: p1 (bound at gadt7.hs:16:16)
+        y :: p1 (bound at gadt7.hs:16:7)
+        i1b :: T a -> p1 -> p (bound at gadt7.hs:16:1)
diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout
index 904f0cd3e8..2e86b42713 100644
--- a/testsuite/tests/ghci.debugger/scripts/break012.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout
@@ -1,14 +1,14 @@
 Stopped in Main.g, break012.hs:5:10-18
-_result :: (t, a1 -> a1, (), a -> a -> a) = _
-a :: t = _
+_result :: (p, a1 -> a1, (), a -> a -> a) = _
+a :: p = _
 b :: a2 -> a2 = _
 c :: () = _
 d :: a -> a -> a = _
-a :: t
+a :: p
 b :: a2 -> a2
 c :: ()
 d :: a -> a -> a
-a = (_t1::t)
+a = (_t1::p)
 b = (_t2::a2 -> a2)
 c = (_t3::())
 d = (_t4::a -> a -> a)
diff --git a/testsuite/tests/ghci.debugger/scripts/print022.stdout b/testsuite/tests/ghci.debugger/scripts/print022.stdout
index 40d2b59544..5d81c044c4 100644
--- a/testsuite/tests/ghci.debugger/scripts/print022.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print022.stdout
@@ -2,7 +2,7 @@
 test = C 1 32 1.2 1.23 'x' 1 1.2 1.23
 Breakpoint 0 activated at print022.hs:11:7
 Stopped in Main.f, print022.hs:11:7
-_result :: t = _
-x :: t = _
+_result :: p = _
+x :: p = _
 x = C2 1 (W# 32) (TwoFields 'a' 3)
 x :: T2
diff --git a/testsuite/tests/ghci/scripts/T11524a.stdout b/testsuite/tests/ghci/scripts/T11524a.stdout
index 164e0cf256..27122574e9 100644
--- a/testsuite/tests/ghci/scripts/T11524a.stdout
+++ b/testsuite/tests/ghci/scripts/T11524a.stdout
@@ -2,7 +2,7 @@ without -fprint-explicit-foralls
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 pattern P :: Bool 	-- Defined at <interactive>:16:1
 pattern Pe :: a -> Ex 	-- Defined at <interactive>:17:1
-pattern Pu :: t -> t 	-- Defined at <interactive>:18:1
+pattern Pu :: p -> p 	-- Defined at <interactive>:18:1
 pattern Pue :: a -> a1 -> (a, Ex) 	-- Defined at <interactive>:19:1
 pattern Pur :: (Num a, Eq a) => a -> [a]
   	-- Defined at <interactive>:20:1
@@ -26,7 +26,7 @@ with -fprint-explicit-foralls
 pattern P :: Bool 	-- Defined at <interactive>:16:1
 pattern Pe :: () => forall {a}. a -> Ex
   	-- Defined at <interactive>:17:1
-pattern Pu :: forall {t}. t -> t 	-- Defined at <interactive>:18:1
+pattern Pu :: forall {p}. p -> p 	-- Defined at <interactive>:18:1
 pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
   	-- Defined at <interactive>:19:1
 pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a]
diff --git a/testsuite/tests/ghci/scripts/T2182ghci.stderr b/testsuite/tests/ghci/scripts/T2182ghci.stderr
index 8a8d3dd65b..5f601942ca 100644
--- a/testsuite/tests/ghci/scripts/T2182ghci.stderr
+++ b/testsuite/tests/ghci/scripts/T2182ghci.stderr
@@ -1,25 +1,25 @@
 
 <interactive>:2:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:10:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:19:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:28:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
 
 <interactive>:49:1: error:
-    • No instance for (Show (t0 -> t0)) arising from a use of ‘print’
+    • No instance for (Show (p0 -> p0)) arising from a use of ‘print’
         (maybe you haven't applied a function to enough arguments?)
     • In a stmt of an interactive GHCi command: print it
diff --git a/testsuite/tests/indexed-types/should_fail/T12386.hs b/testsuite/tests/indexed-types/should_fail/T12386.hs
new file mode 100644
index 0000000000..c07881a6bd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T12386.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T12386 where
+
+class C a where
+   type family F a t :: *
+
+   type family T a :: *
+   type T a = F a
diff --git a/testsuite/tests/indexed-types/should_fail/T12386.stderr b/testsuite/tests/indexed-types/should_fail/T12386.stderr
new file mode 100644
index 0000000000..66d812e1fd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T12386.stderr
@@ -0,0 +1,7 @@
+
+T12386.hs:9:15: error:
+    • Expecting one more argument to ‘F a’
+      Expected a type, but ‘F a’ has kind ‘* -> *’
+    • In the type ‘F a’
+      In the default type instance declaration for ‘T’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index f1ae705f5e..9cc8912814 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -1,13 +1,15 @@
 
-T5439.hs:82:28: error:
-    • Couldn't match type ‘Attempt (WaitOpResult (WaitOps rs))’
-                     with ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
-      Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
-        Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
-    • In the first argument of ‘complete’, namely ‘ev’
-      In the expression: complete ev
+T5439.hs:82:33: error:
+    • Couldn't match expected type ‘Attempt (HElemOf rs)’
+                  with actual type ‘Attempt (HHead (HDrop n0 l0))
+                                    -> Attempt (HElemOf l0)’
+    • In the second argument of ‘($)’, namely
+        ‘inj $ Failure (e :: SomeException)’
       In a stmt of a 'do' block:
         c <- complete ev $ inj $ Failure (e :: SomeException)
+      In the expression:
+        do { c <- complete ev $ inj $ Failure (e :: SomeException);
+             return $ c || not first }
     • Relevant bindings include
         register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
           (bound at T5439.hs:64:9)
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index 0332181394..b7b70b8f4e 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,11 +1,11 @@
 
 T7354.hs:28:11: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ Base t1 (Prim [t] t)
-      Expected type: Prim [t] t -> Base t1 (Prim [t] t)
-        Actual type: Prim [t] t -> t
+        p ~ Base t (Prim [p] p)
+      Expected type: Prim [p] p -> Base t (Prim [p] p)
+        Actual type: Prim [p] p -> p
     • In the first argument of ‘ana’, namely ‘alg’
       In the expression: ana alg
       In an equation for ‘foo’: foo = ana alg
     • Relevant bindings include
-        foo :: Prim [t] t -> t1 (bound at T7354.hs:28:1)
+        foo :: Prim [p] p -> t (bound at T7354.hs:28:1)
diff --git a/testsuite/tests/parser/should_compile/read014.stderr b/testsuite/tests/parser/should_compile/read014.stderr
index 09e79ee52c..228672b7a5 100644
--- a/testsuite/tests/parser/should_compile/read014.stderr
+++ b/testsuite/tests/parser/should_compile/read014.stderr
@@ -1,7 +1,7 @@
 
 read014.hs:4:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      ng1 :: Num a => t -> a -> a
+      ng1 :: Num a => p -> a -> a
 
 read014.hs:4:5: warning: [-Wunused-matches (in -Wextra)]
     Defined but not used: ‘x’
diff --git a/testsuite/tests/parser/should_fail/T7848.stderr b/testsuite/tests/parser/should_fail/T7848.stderr
index f7617ee606..fe949d944a 100644
--- a/testsuite/tests/parser/should_fail/T7848.stderr
+++ b/testsuite/tests/parser/should_fail/T7848.stderr
@@ -1,10 +1,7 @@
 
 T7848.hs:6:1: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ t0 -> t1 -> A -> A -> A -> A -> t2 -> t
-    • When checking that:
-          t0 -> t1 -> A -> A -> A -> A -> forall t2. t2 -> t
-        is more polymorphic than: t
+        t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t
     • Relevant bindings include x :: t (bound at T7848.hs:6:1)
 
 T7848.hs:10:9: error:
diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr
index 963bc50d72..2dca583aba 100644
--- a/testsuite/tests/parser/should_fail/readFail003.stderr
+++ b/testsuite/tests/parser/should_fail/readFail003.stderr
@@ -1,7 +1,7 @@
 
 readFail003.hs:4:27: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ (t, [a1], [a])
+        a2 ~ (a2, [a1], [a])
     • In the expression: a
       In a pattern binding:
         ~(a, b, c)
@@ -11,6 +11,6 @@ readFail003.hs:4:27: error:
           where
               nullity = null
     • Relevant bindings include
-        a :: t (bound at readFail003.hs:4:3)
+        a :: a2 (bound at readFail003.hs:4:3)
         b :: [a1] (bound at readFail003.hs:4:5)
         c :: [a] (bound at readFail003.hs:4:7)
diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
index ebf2a759b7..c5238bb474 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
@@ -1,8 +1,8 @@
 
 T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t2’
-      Where: ‘t2’ is a rigid type variable bound by
-               the inferred type of g :: t2 -> t2 at T10438.hs:(6,9)-(8,21)
+    • Found type wildcard ‘_’ standing for ‘p2’
+      Where: ‘p2’ is a rigid type variable bound by
+               the inferred type of g :: p2 -> p2 at T10438.hs:(6,9)-(8,21)
     • In the type signature: x :: _
       In an equation for ‘g’:
           g r
@@ -20,7 +20,7 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
                       x :: _
                       x = r
     • Relevant bindings include
-        r :: t2 (bound at T10438.hs:6:11)
-        g :: t2 -> t2 (bound at T10438.hs:6:9)
-        f :: t1 (bound at T10438.hs:5:5)
-        foo :: t1 -> forall t. t -> t (bound at T10438.hs:5:1)
+        r :: p2 (bound at T10438.hs:6:11)
+        g :: p2 -> p2 (bound at T10438.hs:6:9)
+        f :: p1 (bound at T10438.hs:5:5)
+        foo :: p1 -> p -> p (bound at T10438.hs:5:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T11192.stderr b/testsuite/tests/partial-sigs/should_compile/T11192.stderr
index 7abf6e5845..8e47c4bb70 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11192.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11192.stderr
@@ -1,8 +1,8 @@
 
 T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘Int -> t -> t’
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of go :: Int -> t -> t at T11192.hs:8:8-17
+    • Found type wildcard ‘_’ standing for ‘Int -> p -> p’
+      Where: ‘p’ is a rigid type variable bound by
+               the inferred type of go :: Int -> p -> p at T11192.hs:8:8-17
     • In the type signature: go :: _
       In the expression:
         let
@@ -18,11 +18,11 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Relevant bindings include fails :: a (bound at T11192.hs:6:1)
 
 T11192.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t1 -> t -> t’
-      Where: ‘t1’ is a rigid type variable bound by
-               the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17
-             ‘t’ is a rigid type variable bound by
-               the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17
+    • Found type wildcard ‘_’ standing for ‘p1 -> p -> p’
+      Where: ‘p1’ is a rigid type variable bound by
+               the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17
+             ‘p’ is a rigid type variable bound by
+               the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17
     • In the type signature: go :: _
       In the expression:
         let
diff --git a/testsuite/tests/patsyn/should_compile/T11213.stderr b/testsuite/tests/patsyn/should_compile/T11213.stderr
index 9c438dd176..838d75c3c7 100644
--- a/testsuite/tests/patsyn/should_compile/T11213.stderr
+++ b/testsuite/tests/patsyn/should_compile/T11213.stderr
@@ -8,7 +8,7 @@ T11213.hs:20:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:21:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
-      pattern Pu :: forall t. t -> t
+      pattern Pu :: forall p. p -> p
 
 T11213.hs:22:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Pattern synonym with no type signature:
diff --git a/testsuite/tests/patsyn/should_fail/mono.stderr b/testsuite/tests/patsyn/should_fail/mono.stderr
index 20714e7565..8f370ce2f0 100644
--- a/testsuite/tests/patsyn/should_fail/mono.stderr
+++ b/testsuite/tests/patsyn/should_fail/mono.stderr
@@ -1,8 +1,8 @@
 
 mono.hs:7:4: error:
     • Couldn't match type ‘Bool’ with ‘Int’
-      Expected type: [Int]
-        Actual type: [Bool]
+      Expected type: [Bool]
+        Actual type: [Int]
     • In the pattern: Single x
       In an equation for ‘f’: f (Single x) = x
 
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index 9f8f62e25e..7a079ff102 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,19 +1,19 @@
 
 T7438.hs:6:14: error:
-    • Couldn't match expected type ‘t’ with actual type ‘t1’
-        ‘t’ is untouchable
+    • Couldn't match expected type ‘p’ with actual type ‘p1’
+        ‘p1’ is untouchable
           inside the constraints: b ~ a
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
-      ‘t’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
+      ‘p’ is a rigid type variable bound by
+        the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
     • Relevant bindings include
-        acc :: t1 (bound at T7438.hs:6:8)
-        go :: Thrist a b -> t1 -> t (bound at T7438.hs:6:1)
+        acc :: p1 (bound at T7438.hs:6:8)
+        go :: Thrist a b -> p1 -> p (bound at T7438.hs:6:1)
diff --git a/testsuite/tests/rebindable/rebindable6.stderr b/testsuite/tests/rebindable/rebindable6.stderr
index 241cf76962..712724d28f 100644
--- a/testsuite/tests/rebindable/rebindable6.stderr
+++ b/testsuite/tests/rebindable/rebindable6.stderr
@@ -25,15 +25,15 @@ rebindable6.hs:110:17: error:
                    return b }
 
 rebindable6.hs:111:17: error:
-    • Ambiguous type variables ‘t1’, ‘t0’ arising from a do statement
+    • Ambiguous type variables ‘p0’, ‘t0’ arising from a do statement
       prevents the constraint ‘(HasBind
-                                  (IO (Maybe b) -> (Maybe b -> t1) -> t0))’ from being solved.
+                                  (IO (Maybe b) -> (Maybe b -> p0) -> t0))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
       Relevant bindings include
         g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
           (bound at rebindable6.hs:108:9)
-      Probable fix: use a type annotation to specify what ‘t1’, ‘t0’ should be.
+      Probable fix: use a type annotation to specify what ‘p0’, ‘t0’ should be.
       These potential instance exist:
         instance HasBind (IO a -> (a -> IO b) -> IO b)
           -- Defined at rebindable6.hs:51:18
@@ -49,15 +49,15 @@ rebindable6.hs:111:17: error:
                    return b }
 
 rebindable6.hs:112:17: error:
-    • Ambiguous type variable ‘t1’ arising from a use of ‘return’
-      prevents the constraint ‘(HasReturn (b -> t1))’ from being solved.
+    • Ambiguous type variable ‘p0’ arising from a use of ‘return’
+      prevents the constraint ‘(HasReturn (b -> p0))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
       Relevant bindings include
         b :: b (bound at rebindable6.hs:111:23)
         g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
           (bound at rebindable6.hs:108:9)
-      Probable fix: use a type annotation to specify what ‘t1’ should be.
+      Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instance exist:
         instance HasReturn (a -> IO a) -- Defined at rebindable6.hs:46:18
     • In a stmt of a 'do' block: return b
diff --git a/testsuite/tests/rename/should_compile/T12597.stderr b/testsuite/tests/rename/should_compile/T12597.stderr
index 8364fd07b3..e3df440372 100644
--- a/testsuite/tests/rename/should_compile/T12597.stderr
+++ b/testsuite/tests/rename/should_compile/T12597.stderr
@@ -1,3 +1,3 @@
 
 T12597.hs:5:1: warning: [-Wmissing-signatures (in -Wall)]
-    Top-level binding with no type signature: f :: t -> t
+    Top-level binding with no type signature: f :: p -> p
diff --git a/testsuite/tests/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr
index 982686868f..df20e67f3a 100644
--- a/testsuite/tests/roles/should_compile/T8958.stderr
+++ b/testsuite/tests/roles/should_compile/T8958.stderr
@@ -65,7 +65,8 @@ AbsBinds [a] []
    Exported types: T8958.$fRepresentationala [InlPrag=[ALWAYS] CONLIKE]
                      :: forall a. Representational a
                    [LclIdX[DFunId],
-                    Unf=DFun: \ (@ a[ssk]) -> T8958.C:Representational TYPE: a[ssk]]
+                    Unf=DFun: \ (@ a[ssk:2]) ->
+                          T8958.C:Representational TYPE: a[ssk:2]]
    Binds: $dRepresentational = T8958.C:Representational @ a
    Evidence: [EvBinds{}]}
 AbsBinds [a] []
@@ -74,7 +75,7 @@ AbsBinds [a] []
    Exported types: T8958.$fNominala [InlPrag=[ALWAYS] CONLIKE]
                      :: forall a. Nominal a
                    [LclIdX[DFunId],
-                    Unf=DFun: \ (@ a[ssk]) -> T8958.C:Nominal TYPE: a[ssk]]
+                    Unf=DFun: \ (@ a[ssk:2]) -> T8958.C:Nominal TYPE: a[ssk:2]]
    Binds: $dNominal = T8958.C:Nominal @ a
    Evidence: [EvBinds{}]}
 
diff --git a/testsuite/tests/simplCore/should_compile/noinline01.stderr b/testsuite/tests/simplCore/should_compile/noinline01.stderr
index cecaad16f0..b100172381 100644
--- a/testsuite/tests/simplCore/should_compile/noinline01.stderr
+++ b/testsuite/tests/simplCore/should_compile/noinline01.stderr
@@ -1,7 +1,7 @@
 
 ==================== Pre unarise: ====================
 Noinline01.f [InlPrag=INLINE (sat-args=1)]
-  :: forall t. t -> GHC.Types.Bool
+  :: forall p. p -> GHC.Types.Bool
 [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] =
     \r [eta] GHC.Types.True [];
 
@@ -26,7 +26,7 @@ Noinline01.$trModule :: GHC.Types.Module
 
 ==================== STG syntax: ====================
 Noinline01.f [InlPrag=INLINE (sat-args=1)]
-  :: forall t. t -> GHC.Types.Bool
+  :: forall p. p -> GHC.Types.Bool
 [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] =
     \r [eta] GHC.Types.True [];
 
diff --git a/testsuite/tests/th/T11452.stderr b/testsuite/tests/th/T11452.stderr
index f59fcbd7d2..32064a9c78 100644
--- a/testsuite/tests/th/T11452.stderr
+++ b/testsuite/tests/th/T11452.stderr
@@ -7,7 +7,7 @@ T11452.hs:6:14: error:
       In an equation for ‘impred’: impred = $$([|| \ _ -> () ||])
 
 T11452.hs:6:14: error:
-    • Cannot instantiate unification variable ‘t0’
+    • Cannot instantiate unification variable ‘p0’
       with a type involving foralls: forall a. a -> a
         GHC doesn't yet support impredicative polymorphism
     • In the Template Haskell quotation [|| \ _ -> () ||]
diff --git a/testsuite/tests/th/T2222.stderr b/testsuite/tests/th/T2222.stderr
index 4ddf100bf6..3265a5e938 100644
--- a/testsuite/tests/th/T2222.stderr
+++ b/testsuite/tests/th/T2222.stderr
@@ -1,4 +1,4 @@
-inside b: t_0
+inside b: p_0
 inside d: GHC.Types.Bool
 type of c: GHC.Types.Bool
 inside f: GHC.Types.Bool
diff --git a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr
index 696bff740d..6cc24fcaf6 100644
--- a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr
+++ b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr
@@ -1,6 +1,6 @@
 
 ExPatFail.hs:12:15: error:
-    • Couldn't match expected type ‘t’ with actual type ‘a’
+    • Couldn't match expected type ‘p’ with actual type ‘a’
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         a pattern with constructor:
@@ -11,4 +11,4 @@ ExPatFail.hs:12:15: error:
       In a pattern binding: MkT y _ = x
       In the expression: let MkT y _ = x in y
     • Relevant bindings include
-        f :: T -> t (bound at ExPatFail.hs:12:1)
+        f :: T -> p (bound at ExPatFail.hs:12:1)
diff --git a/testsuite/tests/typecheck/should_compile/T12427.stderr b/testsuite/tests/typecheck/should_compile/T12427.stderr
new file mode 100644
index 0000000000..0519ecba6e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12427.stderr
@@ -0,0 +1 @@
+ 
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr
new file mode 100644
index 0000000000..fc2aece398
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr
@@ -0,0 +1,33 @@
+
+T12427a.hs:17:29: error:
+    • Couldn't match expected type ‘p’
+                  with actual type ‘(forall b. [b] -> [b]) -> Int’
+        ‘p’ is untouchable
+          inside the constraints: ()
+          bound by a pattern with constructor:
+                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
+                   in a case alternative
+          at T12427a.hs:17:19-24
+      ‘p’ is a rigid type variable bound by
+        the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
+      Possible fix: add a type signature for ‘h11’
+    • In the expression: v
+      In a case alternative: T1 _ v -> v
+      In the expression: case y of { T1 _ v -> v }
+    • Relevant bindings include
+        h11 :: T -> p (bound at T12427a.hs:17:1)
+
+T12427a.hs:28:6: error:
+    • Couldn't match expected type ‘p’
+                  with actual type ‘(forall b. [b] -> [b]) -> Int’
+        ‘p’ is untouchable
+          inside the constraints: ()
+          bound by a pattern with constructor:
+                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
+                   in a pattern binding
+          at T12427a.hs:28:1-7
+      ‘p’ is a rigid type variable bound by
+        the inferred type of x1 :: p at T12427a.hs:28:1-19
+      Possible fix: add a type signature for ‘x1’
+    • In the pattern: T1 _ x1
+      In a pattern binding: T1 _ x1 = undefined
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index d205fa9ced..7d0f0815dc 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -35,7 +35,7 @@ tc141.hs:13:13: error:
         in v
 
 tc141.hs:15:18: error:
-    • Couldn't match expected type ‘a2’ with actual type ‘t’
+    • Couldn't match expected type ‘a2’ with actual type ‘p’
         because type variable ‘a2’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
@@ -50,5 +50,5 @@ tc141.hs:15:18: error:
         in v
     • Relevant bindings include
         v :: a2 (bound at tc141.hs:15:14)
-        b :: t (bound at tc141.hs:13:5)
-        g :: a1 -> t -> forall a. a (bound at tc141.hs:13:1)
+        b :: p (bound at tc141.hs:13:5)
+        g :: a1 -> p -> a (bound at tc141.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/T10495.stderr b/testsuite/tests/typecheck/should_fail/T10495.stderr
index e09e60af23..5067d25183 100644
--- a/testsuite/tests/typecheck/should_fail/T10495.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10495.stderr
@@ -1,8 +1,8 @@
 
-T10495.hs:5:1: error:
+T10495.hs:5:7: error:
     • Couldn't match representation of type ‘a0’ with that of ‘b0’
         arising from a use of ‘coerce’
-    • When instantiating ‘foo’, initially inferred to have
-      this overly-general type:
-        forall a b. Coercible a b => a -> b
-      NB: This instantiation can be caused by the monomorphism restriction.
+    • In the expression: coerce
+      In an equation for ‘foo’: foo = coerce
+    • Relevant bindings include
+        foo :: a0 -> b0 (bound at T10495.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr
index 7a27229369..fde2daf8c6 100644
--- a/testsuite/tests/typecheck/should_fail/T10619.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10619.stderr
@@ -17,7 +17,7 @@ T10619.hs:9:15: error:
               else
                   \ y -> y
     • Relevant bindings include
-        foo :: t -> (b -> b) -> b -> b (bound at T10619.hs:8:1)
+        foo :: p -> (b -> b) -> b -> b (bound at T10619.hs:8:1)
 
 T10619.hs:14:15: error:
     • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
@@ -37,7 +37,7 @@ T10619.hs:14:15: error:
               else
                   ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
     • Relevant bindings include
-        bar :: t -> (b -> b) -> b -> b (bound at T10619.hs:12:1)
+        bar :: p -> (b -> b) -> b -> b (bound at T10619.hs:12:1)
 
 T10619.hs:16:13: error:
     • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’
diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr
index 48bf94d2ce..03c885a577 100644
--- a/testsuite/tests/typecheck/should_fail/T12177.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12177.stderr
@@ -2,27 +2,24 @@
 T12177.hs:3:19: error:
     • Found hole: _ :: t
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t2 -> t1 -> t
-               at T12177.hs:3:1-19
+               the inferred type of bar :: p1 -> p -> t at T12177.hs:3:1-19
     • In the expression: _
       In the expression: \ x -> _
       In the expression: \ x -> \ x -> _
     • Relevant bindings include
-        x :: t1 (bound at T12177.hs:3:14)
-        bar :: t2 -> t1 -> t (bound at T12177.hs:3:1)
+        x :: p (bound at T12177.hs:3:14)
+        bar :: p1 -> p -> t (bound at T12177.hs:3:1)
 
 T12177.hs:5:37: error:
     • Found hole: _ :: t
       Where: ‘t’ is a rigid type variable bound by
-               the inferred type of baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t
+               the inferred type of baz :: p4 -> p3 -> p2 -> p1 -> p -> t
                at T12177.hs:5:1-37
     • In the expression: _
       In the expression: \ z -> _
       In the expression: \ x -> \ z -> _
     • Relevant bindings include
-        z :: t1 (bound at T12177.hs:5:32)
-        x :: t2 (bound at T12177.hs:5:26)
-        y :: t4 (bound at T12177.hs:5:14)
-        baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t
-          (bound at T12177.hs:5:1)
-          
\ No newline at end of file
+        z :: p (bound at T12177.hs:5:32)
+        x :: p1 (bound at T12177.hs:5:26)
+        y :: p3 (bound at T12177.hs:5:14)
+        baz :: p4 -> p3 -> p2 -> p1 -> p -> t (bound at T12177.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T3102.hs b/testsuite/tests/typecheck/should_fail/T3102.hs
index dd5abb25e1..910ac06ee9 100644
--- a/testsuite/tests/typecheck/should_fail/T3102.hs
+++ b/testsuite/tests/typecheck/should_fail/T3102.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS -XImplicitParams -XRankNTypes #-}
- module Bug where
+module Bug where
 
 t :: forall a. ((?p :: Int) => a) -> String
 t _ = "Hello"
@@ -10,3 +10,7 @@ f _ = 3
 result :: Int
 result = f t
 
+
+-- This should work.
+-- Elaborated result = f (/\a. \x:a. t @a (\p::Int. x))
+-- But it did not work in 8.0.1; fixed in HEAD
diff --git a/testsuite/tests/typecheck/should_fail/T3102.stderr b/testsuite/tests/typecheck/should_fail/T3102.stderr
index 66979ddf8b..e69de29bb2 100644
--- a/testsuite/tests/typecheck/should_fail/T3102.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3102.stderr
@@ -1,12 +0,0 @@
-
-T3102.hs:11:12: error:
-    • Couldn't match type ‘a’ with ‘(?p::Int) => a0’
-      ‘a’ is a rigid type variable bound by
-        a type expected by the context:
-          forall a. a -> String
-        at T3102.hs:11:10-12
-      Expected type: a -> String
-        Actual type: ((?p::Int) => a0) -> String
-    • In the first argument of ‘f’, namely ‘t’
-      In the expression: f t
-      In an equation for ‘result’: result = f t
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index 6b8e920004..9157e116f5 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -1,13 +1,13 @@
 
 T7453.hs:9:15: error:
-    • Couldn't match type ‘t’ with ‘t1’
-        because type variable ‘t1’ would escape its scope
+    • Couldn't match type ‘p’ with ‘t’
+        because type variable ‘t’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          z :: Id t1
+          z :: Id t
         at T7453.hs:8:11-19
-      Expected type: Id t1
-        Actual type: Id t
+      Expected type: Id t
+        Actual type: Id p
     • In the expression: aux
       In an equation for ‘z’:
           z = aux
@@ -22,20 +22,20 @@ T7453.hs:9:15: error:
                   where
                       aux = Id v
     • Relevant bindings include
-        aux :: Id t (bound at T7453.hs:10:21)
-        z :: Id t1 (bound at T7453.hs:9:11)
-        v :: t (bound at T7453.hs:7:7)
-        cast1 :: t -> a (bound at T7453.hs:7:1)
+        aux :: Id p (bound at T7453.hs:10:21)
+        z :: Id t (bound at T7453.hs:9:11)
+        v :: p (bound at T7453.hs:7:7)
+        cast1 :: p -> a (bound at T7453.hs:7:1)
 
 T7453.hs:15:15: error:
-    • Couldn't match type ‘t1’ with ‘t2’
-        because type variable ‘t2’ would escape its scope
+    • Couldn't match type ‘p’ with ‘t1’
+        because type variable ‘t1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          z :: () -> t2
+          z :: () -> t1
         at T7453.hs:14:11-22
-      Expected type: () -> t2
-        Actual type: () -> t1
+      Expected type: () -> t1
+        Actual type: () -> p
     • In the expression: aux
       In an equation for ‘z’:
           z = aux
@@ -50,17 +50,17 @@ T7453.hs:15:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> t1 (bound at T7453.hs:16:21)
-        z :: () -> t2 (bound at T7453.hs:15:11)
-        v :: t1 (bound at T7453.hs:13:7)
-        cast2 :: t1 -> t (bound at T7453.hs:13:1)
+        aux :: forall b. b -> p (bound at T7453.hs:16:21)
+        z :: () -> t1 (bound at T7453.hs:15:11)
+        v :: p (bound at T7453.hs:13:7)
+        cast2 :: p -> t (bound at T7453.hs:13:1)
 
 T7453.hs:21:15: error:
-    • Couldn't match expected type ‘t2’ with actual type ‘t1’
-        because type variable ‘t2’ would escape its scope
+    • Couldn't match expected type ‘t1’ with actual type ‘p’
+        because type variable ‘t1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
-          z :: t2
+          z :: t1
         at T7453.hs:20:11-16
     • In the expression: v
       In an equation for ‘z’:
@@ -76,7 +76,7 @@ T7453.hs:21:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> t1 (bound at T7453.hs:22:21)
-        z :: t2 (bound at T7453.hs:21:11)
-        v :: t1 (bound at T7453.hs:19:7)
-        cast3 :: t1 -> forall t. t (bound at T7453.hs:19:1)
+        aux :: forall b. b -> p (bound at T7453.hs:22:21)
+        z :: t1 (bound at T7453.hs:21:11)
+        v :: p (bound at T7453.hs:19:7)
+        cast3 :: p -> t (bound at T7453.hs:19:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr
index 8553fdb888..a39b0488c3 100644
--- a/testsuite/tests/typecheck/should_fail/T7734.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7734.stderr
@@ -1,18 +1,18 @@
 
 T7734.hs:4:13: error:
-    • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1
+    • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘f’: x `f` y = x x
     • Relevant bindings include
-        x :: t2 -> t1 (bound at T7734.hs:4:1)
-        f :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:4:3)
+        x :: t1 -> t (bound at T7734.hs:4:1)
+        f :: (t1 -> t) -> p -> t (bound at T7734.hs:4:3)
 
 T7734.hs:5:13: error:
-    • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1
+    • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘&’: (&) x y = x x
     • Relevant bindings include
-        x :: t2 -> t1 (bound at T7734.hs:5:5)
-        (&) :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:5:1)
+        x :: t1 -> t (bound at T7734.hs:5:5)
+        (&) :: (t1 -> t) -> p -> t (bound at T7734.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr
index ce1b09d51c..f30c49bde6 100644
--- a/testsuite/tests/typecheck/should_fail/T9109.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9109.stderr
@@ -1,14 +1,14 @@
 
 T9109.hs:8:13: error:
-    • Couldn't match expected type ‘t’ with actual type ‘Bool’
-        ‘t’ is untouchable
+    • Couldn't match expected type ‘p’ with actual type ‘Bool’
+        ‘p’ is untouchable
           inside the constraints: a ~ Bool
           bound by a pattern with constructor: GBool :: G Bool,
                    in an equation for ‘foo’
           at T9109.hs:8:5-9
-      ‘t’ is a rigid type variable bound by
-        the inferred type of foo :: G a -> t at T9109.hs:8:1-16
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: G a -> p at T9109.hs:8:1-16
       Possible fix: add a type signature for ‘foo’
     • In the expression: True
       In an equation for ‘foo’: foo GBool = True
-    • Relevant bindings include foo :: G a -> t (bound at T9109.hs:8:1)
+    • Relevant bindings include foo :: G a -> p (bound at T9109.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9318.stderr b/testsuite/tests/typecheck/should_fail/T9318.stderr
index 218ae97b77..c637788a7e 100644
--- a/testsuite/tests/typecheck/should_fail/T9318.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9318.stderr
@@ -1,7 +1,7 @@
 
-T9318.hs:12:5:
-    Couldn't match type ‘Char’ with ‘Bool’
-    Expected type: F Int
-      Actual type: Char
-    In the pattern: 'x'
-    In an equation for ‘bar’: bar 'x' = ()
+T9318.hs:12:5: error:
+    • Couldn't match type ‘Bool’ with ‘Char’
+      Expected type: F Int
+        Actual type: Char
+    • In the pattern: 'x'
+      In an equation for ‘bar’: bar 'x' = ()
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index ff90a738c9..17486dfefa 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -13,7 +13,7 @@ VtaFail.hs:12:26: error:
           answer_constraint_fail = addOne @Bool 5
 
 VtaFail.hs:14:17: error:
-    • Cannot apply expression of type ‘t1 -> t1’
+    • Cannot apply expression of type ‘p0 -> p0’
       to a visible type argument ‘Int’
     • In the expression: (\ x -> x) @Int 12
       In an equation for ‘answer_lambda’:
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 98c57e833e..4f2dbc43d5 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -208,7 +208,7 @@ test('T2806', normal, compile_fail, [''])
 test('T3323', normal, compile_fail, [''])
 test('T3406', normal, compile_fail, [''])
 test('T3540', normal, compile_fail, [''])
-test('T3102', normal, compile_fail, [''])
+test('T3102', normal, compile, [''])
 test('T3613', normal, compile_fail, [''])
 test('fd-loop', normal, compile_fail, [''])
 test('T3950', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
index 6755636682..d72a34065e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr
@@ -1,8 +1,8 @@
 
 tcfail002.hs:4:7: error:
-    • Occurs check: cannot construct the infinite type: t ~ [t]
+    • Occurs check: cannot construct the infinite type: p ~ [p]
     • In the expression: z
       In an equation for ‘c’: c z = z
     • Relevant bindings include
-        z :: [t] (bound at tcfail002.hs:4:3)
-        c :: [t] -> t (bound at tcfail002.hs:3:1)
+        z :: [p] (bound at tcfail002.hs:4:3)
+        c :: [p] -> p (bound at tcfail002.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
index 41a55c1ea9..7bf64d841a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
@@ -1,9 +1,9 @@
 
 tcfail004.hs:3:9: error:
-    • Couldn't match expected type ‘(t1, t)’
+    • Couldn't match expected type ‘(a, b)’
                   with actual type ‘(Integer, Integer, Integer)’
     • In the expression: (1, 2, 3)
       In a pattern binding: (f, g) = (1, 2, 3)
     • Relevant bindings include
-        f :: t1 (bound at tcfail004.hs:3:2)
-        g :: t (bound at tcfail004.hs:3:4)
+        f :: a (bound at tcfail004.hs:3:2)
+        g :: b (bound at tcfail004.hs:3:4)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
index 77437cf583..56db4cf58b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
@@ -1,9 +1,9 @@
 
 tcfail005.hs:3:9: error:
-    • Couldn't match expected type ‘[t]’
+    • Couldn't match expected type ‘[a]’
                   with actual type ‘(Integer, Char)’
     • In the expression: (1, 'a')
       In a pattern binding: (h : i) = (1, 'a')
     • Relevant bindings include
-        h :: t (bound at tcfail005.hs:3:2)
-        i :: [t] (bound at tcfail005.hs:3:4)
+        h :: a (bound at tcfail005.hs:3:2)
+        i :: [a] (bound at tcfail005.hs:3:4)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail013.stderr b/testsuite/tests/typecheck/should_fail/tcfail013.stderr
index f3e815bb6e..3803d9ce95 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail013.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail013.stderr
@@ -4,4 +4,4 @@ tcfail013.hs:4:3: error:
     • In the pattern: True
       In an equation for ‘f’: f True = 2
     • Relevant bindings include
-        f :: [a] -> t (bound at tcfail013.hs:3:1)
+        f :: [a] -> p (bound at tcfail013.hs:3:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail014.stderr b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
index a186fb1310..f506bff6f8 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr
@@ -1,9 +1,9 @@
 
 tcfail014.hs:5:33: error:
-    • Occurs check: cannot construct the infinite type: t7 ~ t7 -> t8
+    • Occurs check: cannot construct the infinite type: t4 ~ t4 -> t5
     • In the first argument of ‘z’, namely ‘z’
       In the expression: z z
       In an equation for ‘h’: h z = z z
     • Relevant bindings include
-        z :: t7 -> t8 (bound at tcfail014.hs:5:27)
-        h :: (t7 -> t8) -> t8 (bound at tcfail014.hs:5:25)
+        z :: t4 -> t5 (bound at tcfail014.hs:5:27)
+        h :: (t4 -> t5) -> t5 (bound at tcfail014.hs:5:25)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail018.stderr b/testsuite/tests/typecheck/should_fail/tcfail018.stderr
index 57060a87db..d5594c7c41 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail018.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail018.stderr
@@ -1,5 +1,5 @@
 
 tcfail018.hs:5:10: error:
-    • No instance for (Num [t0]) arising from the literal ‘1’
+    • No instance for (Num [a0]) arising from the literal ‘1’
     • In the expression: 1
       In a pattern binding: (a : []) = 1
diff --git a/testsuite/tests/typecheck/should_fail/tcfail032.stderr b/testsuite/tests/typecheck/should_fail/tcfail032.stderr
index 583e6e3ce5..d2912b2b94 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail032.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail032.stderr
@@ -1,6 +1,6 @@
 
 tcfail032.hs:14:8: error:
-    • Couldn't match expected type ‘a1 -> Int’ with actual type ‘t’
+    • Couldn't match expected type ‘a1 -> Int’ with actual type ‘p’
         because type variable ‘a1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         an expression type signature:
@@ -9,5 +9,5 @@ tcfail032.hs:14:8: error:
     • In the expression: (x :: (Eq a) => a -> Int)
       In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int)
     • Relevant bindings include
-        x :: t (bound at tcfail032.hs:14:3)
-        f :: t -> forall a. Eq a => a -> Int (bound at tcfail032.hs:14:1)
+        x :: p (bound at tcfail032.hs:14:3)
+        f :: p -> a -> Int (bound at tcfail032.hs:14:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail099.stderr b/testsuite/tests/typecheck/should_fail/tcfail099.stderr
index f3908f36e4..bc30866ec2 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail099.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail099.stderr
@@ -1,6 +1,6 @@
 
 tcfail099.hs:9:20: error:
-    • Couldn't match expected type ‘a’ with actual type ‘t’
+    • Couldn't match expected type ‘a’ with actual type ‘p’
         because type variable ‘a’ would escape its scope
       This (rigid, skolem) type variable is bound by
         a pattern with constructor: C :: forall a. (a -> Int) -> DS,
@@ -10,6 +10,6 @@ tcfail099.hs:9:20: error:
       In the expression: f arg
       In an equation for ‘call’: call (C f) arg = f arg
     • Relevant bindings include
-        arg :: t (bound at tcfail099.hs:9:12)
+        arg :: p (bound at tcfail099.hs:9:12)
         f :: a -> Int (bound at tcfail099.hs:9:9)
-        call :: DS -> t -> Int (bound at tcfail099.hs:9:1)
+        call :: DS -> p -> Int (bound at tcfail099.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail104.stderr b/testsuite/tests/typecheck/should_fail/tcfail104.stderr
index a0a6595231..44d8e4888c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail104.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail104.stderr
@@ -3,15 +3,15 @@ tcfail104.hs:14:12: error:
     • Couldn't match type ‘forall a. a -> a’ with ‘Char -> Char’
       Expected type: (Char -> Char) -> Char -> Char
         Actual type: (forall a. a -> a) -> Char -> Char
-    • When checking that: (forall a. a -> a) -> forall a. a -> a
-        is more polymorphic than: (Char -> Char) -> Char -> Char
-      In the expression: (\ (x :: forall a. a -> a) -> x)
+    • In the expression: (\ (x :: forall a. a -> a) -> x)
       In the expression:
         if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+      In the expression:
+        (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
 
 tcfail104.hs:22:15: error:
-    • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘Char -> Char’
+    • Couldn't match expected type ‘Char -> Char’
+                  with actual type ‘forall a. a -> a’
     • When checking that the pattern signature: forall a. a -> a
         fits the type of its context: Char -> Char
       In the pattern: x :: forall a. a -> a
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index f75f77c38a..85217315ca 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -16,7 +16,7 @@ tcfail140.hs:12:10: error:
       In the expression: 3 `f` 4
       In an equation for ‘rot’: rot xs = 3 `f` 4
     • Relevant bindings include
-        rot :: t1 -> t (bound at tcfail140.hs:12:1)
+        rot :: p -> t (bound at tcfail140.hs:12:1)
 
 tcfail140.hs:14:15: error:
     • Couldn't match expected type ‘t -> b’ with actual type ‘Int’
@@ -36,6 +36,6 @@ tcfail140.hs:16:8: error:
       In the expression: (\ Just x -> x) :: Maybe a -> a
 
 tcfail140.hs:19:1: error:
-    • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’
+    • Couldn't match expected type ‘Int’ with actual type ‘p0 -> Bool’
     • The equation(s) for ‘g’ have two arguments,
       but its type ‘Int -> Int’ has only one
diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
index a231133fd4..30e27b8bb7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
@@ -3,7 +3,7 @@ tcfail181.hs:17:9: error:
     • Could not deduce (Monad m0) arising from a use of ‘foo’
       from the context: Monad m
         bound by the inferred type of
-                 wog :: Monad m => t -> Something (m Bool) e
+                 wog :: Monad m => p -> Something (m Bool) e
         at tcfail181.hs:17:1-30
       The type variable ‘m0’ is ambiguous
       These potential instances exist:
diff --git a/testsuite/tests/warnings/should_compile/T12574.stderr b/testsuite/tests/warnings/should_compile/T12574.stderr
index ded88331fa..db435541c1 100644
--- a/testsuite/tests/warnings/should_compile/T12574.stderr
+++ b/testsuite/tests/warnings/should_compile/T12574.stderr
@@ -1,4 +1,4 @@
 
 T12574.hs:3:1: warning: [-Wmissing-local-signatures]
     Polymorphic local binding with no type signature:
-      T12574.id :: forall t. t -> t
+      T12574.id :: forall p. p -> p