Always display inferred variables using braces

We now always show "forall {a}. T" for inferred variables,
previously this was controlled by -fprint-explicit-foralls.

This implements part 1 of https://github.com/ghc-proposals/ghc-proposals/pull/179.

Part of GHC ticket #16320.

Furthermore, when printing a levity restriction error, we now display
the HsWrap of the expression. This lets users see the full elaboration with
-fprint-typechecker-elaboration (see also #17670)

14 files changed, 29 insertions, 22 deletions

diff --git a/testsuite/tests/typecheck/should_fail/T10285.stderr b/testsuite/tests/typecheck/should_fail/T10285.stderr
index 99edf39591..02215e2f70 100644
--- a/testsuite/tests/typecheck/should_fail/T10285.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10285.stderr
@@ -3,7 +3,7 @@ T10285.hs:8:17: error:
     • Could not deduce: Coercible a b arising from a use of ‘coerce’
       from the context: Coercible (N a) (N b)
         bound by a pattern with constructor:
-                   Coercion :: forall k (a :: k) (b :: k).
+                   Coercion :: forall {k} (a :: k) (b :: k).
                                Coercible a b =>
                                Coercion a b,
                  in an equation for ‘oops’
diff --git a/testsuite/tests/typecheck/should_fail/T10351.stderr b/testsuite/tests/typecheck/should_fail/T10351.stderr
index 782d6e39d8..bd28a5a3e1 100644
--- a/testsuite/tests/typecheck/should_fail/T10351.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10351.stderr
@@ -3,4 +3,4 @@ T10351.hs:6:1: error:
     • Non type-variable argument in the constraint: C [a]
       (Use FlexibleContexts to permit this)
     • When checking the inferred type
-        f :: forall a. C [a] => a -> ()
+        f :: forall {a}. C [a] => a -> ()
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr
index 44937c3c45..0a24b6ec6d 100644
--- a/testsuite/tests/typecheck/should_fail/T12785b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr
@@ -10,7 +10,7 @@ T12785b.hs:29:63: error:
         at T12785b.hs:29:7-51
       ‘s’ is a rigid type variable bound by
         a pattern with constructor:
-          Hide :: forall a (n :: Peano) (f :: a -> *) (s :: HTree n a).
+          Hide :: forall {a} (n :: Peano) (f :: a -> *) (s :: HTree n a).
                   STree n f s -> Hidden n f,
         in an equation for ‘nest’
         at T12785b.hs:29:7-12
diff --git a/testsuite/tests/typecheck/should_fail/T15361.stderr b/testsuite/tests/typecheck/should_fail/T15361.stderr
index 93b01742ff..4b8c23ebf2 100644
--- a/testsuite/tests/typecheck/should_fail/T15361.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15361.stderr
@@ -3,7 +3,7 @@ T15361.hs:13:13: error:
     • Could not deduce: a ~ c
       from the context: b ~ a
         bound by a pattern with constructor:
-                   HRefl :: forall k1 (a :: k1). a :~~: a,
+                   HRefl :: forall {k1} (a :: k1). a :~~: a,
                  in an equation for ‘foo’
         at T15361.hs:13:5-9
       ‘a’ is a rigid type variable bound by
diff --git a/testsuite/tests/typecheck/should_fail/T17773.stderr b/testsuite/tests/typecheck/should_fail/T17773.stderr
index 5a6989a176..401fcc494a 100644
--- a/testsuite/tests/typecheck/should_fail/T17773.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17773.stderr
@@ -3,7 +3,7 @@ T17773.hs:16:22: error:
     • Found hole: _Refl :: Mzero x y :~: (x <|> y)
       Where: ‘x’, ‘f’, ‘k’, ‘a’, ‘y’ are rigid type variables bound by
                the type signature for:
-                 monadPlusMplus :: forall k (f :: k -> *) (a :: k) (x :: f a)
+                 monadPlusMplus :: forall {k} (f :: k -> *) (a :: k) (x :: f a)
                                           (y :: f a).
                                    Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
                at T17773.hs:(13,1)-(15,41)
diff --git a/testsuite/tests/typecheck/should_fail/T1897a.stderr b/testsuite/tests/typecheck/should_fail/T1897a.stderr
index 61de72d6a6..2be4c938bb 100644
--- a/testsuite/tests/typecheck/should_fail/T1897a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1897a.stderr
@@ -3,10 +3,10 @@ T1897a.hs:9:1: error:
     • Could not deduce (Wob a0 b)
       from the context: Wob a b
         bound by the inferred type for ‘foo’:
-                   forall a b. Wob a b => b -> [b]
+                   forall {a} {b}. Wob a b => b -> [b]
         at T1897a.hs:9:1-24
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘foo’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        foo :: forall a b. Wob a b => b -> [b]
+        foo :: forall {a} {b}. Wob a b => b -> [b]
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 64eba564f4..152823c80e 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -82,7 +82,7 @@ T6018fail.hs:68:15: error:
     Type family equation violates the family's injectivity annotation.
     Type/kind variable ‘k’ cannot be inferred from the right-hand side.
     In the type family equation:
-      forall k (a :: k) (b :: k).
+      forall {k} {a :: k} {b :: k}.
         Fc @k a b = Int -- Defined at T6018fail.hs:68:15
 
 T6018fail.hs:72:15: error:
@@ -90,7 +90,7 @@ T6018fail.hs:72:15: error:
     Type/kind variables ‘k’, ‘a’, ‘b’
     cannot be inferred from the right-hand side.
     In the type family equation:
-      forall k (a :: k) (b :: k).
+      forall {k} {a :: k} {b :: k}.
         Gc @k a b = Int -- Defined at T6018fail.hs:72:15
 
 T6018fail.hs:76:15: error:
@@ -151,7 +151,7 @@ T6018fail.hs:120:15: error:
     Type/kind variables ‘k’, ‘c’
     cannot be inferred from the right-hand side.
     In the type family equation:
-      forall k a b (c :: k).
+      forall {k} {a} {b} {c :: k}.
         G7 @k a b c = [G7a @k a b c] -- Defined at T6018fail.hs:120:15
 
 T6018fail.hs:131:1: error:
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index 32bcf83ba5..50df2777ce 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -28,7 +28,7 @@ T6018failclosed.hs:25:5: error:
       Type/kind variables ‘k1’, ‘b’
       cannot be inferred from the right-hand side.
       In the type family equation:
-        forall k1 k2 (b :: k1) (c :: k2).
+        forall {k1} {k2} {b :: k1} {c :: k2}.
           JClosed @{k1} @{k2} Int b c = Char
             -- Defined at T6018failclosed.hs:25:5
     • In the equations for closed type family ‘JClosed’
@@ -45,7 +45,7 @@ T6018failclosed.hs:30:5: error:
 T6018failclosed.hs:35:5: error:
     • Type family equation violates the family's injectivity annotation.
       RHS of injective type family equation cannot be a type family:
-        forall k (a :: k).
+        forall {k} {a :: k}.
           LClosed a = MaybeSynClosed a -- Defined at T6018failclosed.hs:35:5
     • In the equations for closed type family ‘LClosed’
       In the type family declaration for ‘LClosed’
@@ -94,7 +94,7 @@ T6018failclosed.hs:66:5: error:
     • Type family equation violates the family's injectivity annotation.
       Type/kind variable ‘k’ cannot be inferred from the right-hand side.
       In the type family equation:
-        forall k (a :: k) (b :: k).
+        forall {k} {a :: k} {b :: k}.
           Gc @k a b = Int -- Defined at T6018failclosed.hs:66:5
     • In the equations for closed type family ‘Gc’
       In the type family declaration for ‘Gc’
diff --git a/testsuite/tests/typecheck/should_fail/T6022.stderr b/testsuite/tests/typecheck/should_fail/T6022.stderr
index e690095665..6423925b12 100644
--- a/testsuite/tests/typecheck/should_fail/T6022.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6022.stderr
@@ -3,4 +3,4 @@ T6022.hs:3:1: error:
     • Non type-variable argument in the constraint: Eq ([a] -> a)
       (Use FlexibleContexts to permit this)
     • When checking the inferred type
-        f :: forall a. Eq ([a] -> a) => ([a] -> a) -> Bool
+        f :: forall {a}. Eq ([a] -> a) => ([a] -> a) -> Bool
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index d72b6d9a7a..224f5b90fe 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -58,7 +58,7 @@ T7453.hs:21:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> p (bound at T7453.hs:22:21)
+        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/T8883.stderr b/testsuite/tests/typecheck/should_fail/T8883.stderr
index d5a547db7b..c56c434c4c 100644
--- a/testsuite/tests/typecheck/should_fail/T8883.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8883.stderr
@@ -3,6 +3,6 @@ T8883.hs:20:1: error:
     • Non type-variable argument in the constraint: Functor (PF a)
       (Use FlexibleContexts to permit this)
     • When checking the inferred type
-        fold :: forall a b.
+        fold :: forall {a} {b}.
                 (Functor (PF a), Regular a) =>
                 (PF a b -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
index 638dc80ff8..1c39c9133b 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
@@ -1,5 +1,8 @@
-UnliftedNewtypesCoerceFail.hs:15:8:
+
+UnliftedNewtypesCoerceFail.hs:15:8: error:
     Cannot use function with levity-polymorphic arguments:
       coerce :: x -> y
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
     Levity-polymorphic arguments: x :: TYPE rep
-
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
index 90cf5b23aa..70746fd60a 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
@@ -1,4 +1,8 @@
-UnliftedNewtypesLevityBinder.hs:16:7:
+
+UnliftedNewtypesLevityBinder.hs:16:7: error:
     Cannot use function with levity-polymorphic arguments:
-      UnliftedNewtypesLevityBinder.IdentC :: a -> Ident a
+      IdentC :: a -> Ident a
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
     Levity-polymorphic arguments: a :: TYPE r
diff --git a/testsuite/tests/typecheck/should_fail/tcfail080.stderr b/testsuite/tests/typecheck/should_fail/tcfail080.stderr
index 2fd7240182..c6d7fc5c90 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail080.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail080.stderr
@@ -3,10 +3,10 @@ tcfail080.hs:27:1: error:
     • Could not deduce (Collection c0 a)
       from the context: Collection c a
         bound by the inferred type for ‘q’:
-                   forall (c :: * -> *) a. Collection c a => a -> Bool
+                   forall {c :: * -> *} {a}. Collection c a => a -> Bool
         at tcfail080.hs:27:1-27
       The type variable ‘c0’ is ambiguous
     • In the ambiguity check for the inferred type for ‘q’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        q :: forall (c :: * -> *) a. Collection c a => a -> Bool
+        q :: forall {c :: * -> *} {a}. Collection c a => a -> Bool