Type vs Constraint: finally nailed

This big patch addresses the rats-nest of issues that have plagued
us for years, about the relationship between Type and Constraint.
See #11715/#21623.

The main payload of the patch is:
* To introduce CONSTRAINT :: RuntimeRep -> Type
* To make TYPE and CONSTRAINT distinct throughout the compiler

Two overview Notes in GHC.Builtin.Types.Prim

* Note [TYPE and CONSTRAINT]

* Note [Type and Constraint are not apart]
  This is the main complication.

The specifics

* New primitive types (GHC.Builtin.Types.Prim)
  - CONSTRAINT
  - ctArrowTyCon (=>)
  - tcArrowTyCon (-=>)
  - ccArrowTyCon (==>)
  - funTyCon     FUN     -- Not new
  See Note [Function type constructors and FunTy]
  and Note [TYPE and CONSTRAINT]

* GHC.Builtin.Types:
  - New type Constraint = CONSTRAINT LiftedRep
  - I also stopped nonEmptyTyCon being built-in; it only needs to be wired-in

* Exploit the fact that Type and Constraint are distinct throughout GHC
  - Get rid of tcView in favour of coreView.
  - Many tcXX functions become XX functions.
    e.g. tcGetCastedTyVar --> getCastedTyVar

* Kill off Note [ForAllTy and typechecker equality], in (old)
  GHC.Tc.Solver.Canonical.  It said that typechecker-equality should ignore
  the specified/inferred distinction when comparein two ForAllTys.  But
  that wsa only weakly supported and (worse) implies that we need a separate
  typechecker equality, different from core equality. No no no.

* GHC.Core.TyCon: kill off FunTyCon in data TyCon.  There was no need for it,
  and anyway now we have four of them!

* GHC.Core.TyCo.Rep: add two FunTyFlags to FunCo
  See Note [FunCo] in that module.

* GHC.Core.Type.  Lots and lots of changes driven by adding CONSTRAINT.
  The key new function is sORTKind_maybe; most other changes are built
  on top of that.

  See also `funTyConAppTy_maybe` and `tyConAppFun_maybe`.

* Fix a longstanding bug in GHC.Core.Type.typeKind, and Core Lint, in
  kinding ForAllTys.  See new tules (FORALL1) and (FORALL2) in GHC.Core.Type.
  (The bug was that before (forall (cv::t1 ~# t2). blah), where
  blah::TYPE IntRep, would get kind (TYPE IntRep), but it should be
  (TYPE LiftedRep).  See Note [Kinding rules for types] in GHC.Core.Type.

* GHC.Core.TyCo.Compare is a new module in which we do eqType and cmpType.
  Of course, no tcEqType any more.

* GHC.Core.TyCo.FVs. I moved some free-var-like function into this module:
  tyConsOfType, visVarsOfType, and occCheckExpand.  Refactoring only.

* GHC.Builtin.Types.  Compiletely re-engineer boxingDataCon_maybe to
  have one for each /RuntimeRep/, rather than one for each /Type/.
  This dramatically widens the range of types we can auto-box.
  See Note [Boxing constructors] in GHC.Builtin.Types
  The boxing types themselves are declared in library ghc-prim:GHC.Types.

  GHC.Core.Make.  Re-engineer the treatment of "big" tuples (mkBigCoreVarTup
  etc) GHC.Core.Make, so that it auto-boxes unboxed values and (crucially)
  types of kind Constraint. That allows the desugaring for arrows to work;
  it gathers up free variables (including dictionaries) into tuples.
  See  Note [Big tuples] in GHC.Core.Make.

  There is still work to do here: #22336. But things are better than
  before.

* GHC.Core.Make.  We need two absent-error Ids, aBSENT_ERROR_ID for types of
  kind Type, and aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint.
  Ditto noInlineId vs noInlieConstraintId in GHC.Types.Id.Make;
  see Note [inlineId magic].

* GHC.Core.TyCo.Rep. Completely refactor the NthCo coercion.  It is now called
  SelCo, and its fields are much more descriptive than the single Int we used to
  have.  A great improvement.  See Note [SelCo] in GHC.Core.TyCo.Rep.

* GHC.Core.RoughMap.roughMatchTyConName.  Collapse TYPE and CONSTRAINT to
  a single TyCon, so that the rough-map does not distinguish them.

* GHC.Core.DataCon
  - Mainly just improve documentation

* Some significant renamings:
  GHC.Core.Multiplicity: Many -->  ManyTy (easier to grep for)
                         One  -->  OneTy
  GHC.Core.TyCo.Rep TyCoBinder      -->   GHC.Core.Var.PiTyBinder
  GHC.Core.Var      TyCoVarBinder   -->   ForAllTyBinder
                    AnonArgFlag     -->   FunTyFlag
                    ArgFlag         -->   ForAllTyFlag
  GHC.Core.TyCon    TyConTyCoBinder --> TyConPiTyBinder
  Many functions are renamed in consequence
  e.g. isinvisibleArgFlag becomes isInvisibleForAllTyFlag, etc

* I refactored FunTyFlag (was AnonArgFlag) into a simple, flat data type
    data FunTyFlag
      = FTF_T_T           -- (->)  Type -> Type
      | FTF_T_C           -- (-=>) Type -> Constraint
      | FTF_C_T           -- (=>)  Constraint -> Type
      | FTF_C_C           -- (==>) Constraint -> Constraint

* GHC.Tc.Errors.Ppr.  Some significant refactoring in the TypeEqMisMatch case
  of pprMismatchMsg.

* I made the tyConUnique field of TyCon strict, because I
  saw code with lots of silly eval's.  That revealed that
  GHC.Settings.Constants.mAX_SUM_SIZE can only be 63, because
  we pack the sum tag into a 6-bit field.  (Lurking bug squashed.)

Fixes
* #21530

Updates haddock submodule slightly.

Performance changes
~~~~~~~~~~~~~~~~~~~
I was worried that compile times would get worse, but after
some careful profiling we are down to a geometric mean 0.1%
increase in allocation (in perf/compiler).  That seems fine.

There is a big runtime improvement in T10359

Metric Decrease:
    LargeRecord
    MultiLayerModulesTH_OneShot
    T13386
    T13719
Metric Increase:
    T8095

28 files changed, 65 insertions, 105 deletions

diff --git a/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr b/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
index 7804228b0b..a67bfdcc7e 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
@@ -4,9 +4,9 @@ ExprSigLocal.hs:9:35: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefa
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of <expression> :: a -> a
                at ExprSigLocal.hs:9:27
-    • In the type ‘a -> _’
-      In an expression type signature: forall a. a -> _
+    • In an expression type signature: forall a. a -> _
       In the expression: (\ x -> x) :: forall a. a -> _
+      In an equation for ‘y’: y = ((\ x -> x) :: forall a. a -> _)
     • Relevant bindings include
         y :: b -> b (bound at ExprSigLocal.hs:9:1)
 
@@ -15,5 +15,4 @@ ExprSigLocal.hs:11:21: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdef
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of g :: a -> a
                at ExprSigLocal.hs:11:13
-    • In the type ‘a -> _’
-      In the type signature: g :: forall a. a -> _
+    • In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
index 1f776ecc42..9c16399db7 100644
--- a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
@@ -3,8 +3,7 @@
 
 SplicesUsed.hs:7:15: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Maybe Bool’
-    • In the type ‘_’
-      In the type signature: maybeBool :: (_)
+    • In the type signature: maybeBool :: _
 
 SplicesUsed.hs:8:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_a’ standing for ‘w’
@@ -21,8 +20,9 @@ SplicesUsed.hs:8:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefau
 SplicesUsed.hs:8:26: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Bool’
     • In the first argument of ‘Maybe’, namely ‘_’
-      In the type ‘Maybe _’
       In an expression type signature: Maybe _
+      In the first argument of ‘id :: _a -> _a’, namely
+        ‘(Just True :: Maybe _)’
     • Relevant bindings include
         maybeBool :: Maybe Bool (bound at SplicesUsed.hs:8:1)
 
@@ -31,32 +31,28 @@ SplicesUsed.hs:10:16: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefa
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of charA :: a -> (Char, a)
                at SplicesUsed.hs:10:1-26
-    • In the type ‘a -> (_)’
-      In the type signature: charA :: a -> (_)
+    • In the type signature: charA :: a -> _
 
 SplicesUsed.hs:13:13: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a -> Bool’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of filter' :: (a -> Bool) -> [a] -> [a]
                at SplicesUsed.hs:14:1-16
-    • In the type ‘_ -> _ -> _’
-      In the type signature: filter' :: (_ -> _ -> _)
+    • In the type signature: filter' :: (_ -> _ -> _)
 
 SplicesUsed.hs:13:13: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘[a]’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of filter' :: (a -> Bool) -> [a] -> [a]
                at SplicesUsed.hs:14:1-16
-    • In the type ‘_ -> _ -> _’
-      In the type signature: filter' :: (_ -> _ -> _)
+    • In the type signature: filter' :: (_ -> _ -> _)
 
 SplicesUsed.hs:13:13: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘[a]’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of filter' :: (a -> Bool) -> [a] -> [a]
                at SplicesUsed.hs:14:1-16
-    • In the type ‘_ -> _ -> _’
-      In the type signature: filter' :: (_ -> _ -> _)
+    • In the type signature: filter' :: (_ -> _ -> _)
 
 SplicesUsed.hs:16:2: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found extra-constraints wildcard standing for ‘Eq a’
diff --git a/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr b/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
index d4049ce61e..2347b8e0c4 100644
--- a/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SuperCls.stderr
@@ -1,4 +1,4 @@
 
 SuperCls.hs:4:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature: f :: (Ord a, _) => a -> Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T11016.stderr b/testsuite/tests/partial-sigs/should_compile/T11016.stderr
index 667fcddfdf..44b6fd6c57 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11016.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11016.stderr
@@ -1,6 +1,6 @@
 
 T11016.hs:5:19: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature: f1 :: (?x :: Int, _) => Int
 
 T11016.hs:8:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
diff --git a/testsuite/tests/partial-sigs/should_compile/T11670.stderr b/testsuite/tests/partial-sigs/should_compile/T11670.stderr
index 8a5a342e81..b64df03c1c 100644
--- a/testsuite/tests/partial-sigs/should_compile/T11670.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T11670.stderr
@@ -2,8 +2,8 @@
 T11670.hs:10:42: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘CLong’
     • In the first argument of ‘IO’, namely ‘_’
-      In the type ‘IO _’
       In an expression type signature: IO _
+      In the expression: peekElemOff undefined 0 :: IO _
     • Relevant bindings include
         ptr :: Ptr a (bound at T11670.hs:10:6)
         peek :: Ptr a -> IO CLong (bound at T11670.hs:10:1)
@@ -27,8 +27,8 @@ T11670.hs:13:48: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
                the inferred type of <expression> :: Storable w => IO w
                at T11670.hs:13:40-48
     • In the first argument of ‘IO’, namely ‘_’
-      In the type ‘IO _’
       In an expression type signature: _ => IO _
+      In the expression: peekElemOff undefined 0 :: _ => IO _
     • Relevant bindings include
         ptr :: Ptr a (bound at T11670.hs:13:7)
         peek2 :: Ptr a -> IO CLong (bound at T11670.hs:13:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T12845.stderr b/testsuite/tests/partial-sigs/should_compile/T12845.stderr
index 912784a092..d5600c5f9f 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12845.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12845.stderr
@@ -1,6 +1,6 @@
 
 T12845.hs:18:70: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature:
         broken :: forall r r' rngs. ('(r, r') ~ Head rngs,
                                      Bar r r' ~ 'True,
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643.stderr b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
index cc8920f705..ecc629b76b 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14643.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
@@ -1,8 +1,8 @@
 
 T14643.hs:5:18: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature: af :: (Num a, _) => a -> a
 
 T14643.hs:5:18: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
index d8f7b19a02..8791cf6d6a 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
@@ -1,8 +1,8 @@
 
 T14643a.hs:5:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature: af :: (Num a, _) => a -> a
 
 T14643a.hs:8:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
     • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.stderr b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
index 6768b12d48..b8445729d4 100644
--- a/testsuite/tests/partial-sigs/should_compile/T16728.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
@@ -6,4 +6,4 @@ T16728.hs:8:37: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
                at T16728.hs:8:13
     • In the kind ‘_’
       In the first argument of ‘Proxy’, namely ‘(x :: _)’
-      In the type ‘Proxy (x :: _)’
+      In the type signature: f :: forall k (x :: k). Proxy (x :: _)
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.stderr b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
index a78fb1f2a6..20e8d933b6 100644
--- a/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
@@ -6,8 +6,7 @@ T16728a.hs:4:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
                  g :: a -> w
                  h :: a -> w
                at T16728a.hs:(5,1)-(7,9)
-    • In the type ‘a -> _’
-      In the type signature: g :: forall a. a -> _
+    • In the type signature: g :: forall a. a -> _
 
 T16728a.hs:4:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘w’
@@ -16,5 +15,4 @@ T16728a.hs:4:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
                  g :: a -> w
                  h :: a -> w
                at T16728a.hs:(5,1)-(7,9)
-    • In the type ‘a -> _’
-      In the type signature: h :: forall a. a -> _
+    • In the type signature: h :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
index 02dcbac79e..5f3d0648e0 100644
--- a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
@@ -4,10 +4,8 @@ T16728b.hs:4:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of g :: a -> a
                at T16728b.hs:4:14
-    • In the type ‘a -> _’
-      In the type signature: g :: forall a. a -> _
+    • In the type signature: g :: forall a. a -> _
 
 T16728b.hs:4:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Bool’
-    • In the type ‘a -> _’
-      In the type signature: h :: forall a. a -> _
+    • In the type signature: h :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/T18008.stderr b/testsuite/tests/partial-sigs/should_compile/T18008.stderr
index d5b35c957d..21c75abb52 100644
--- a/testsuite/tests/partial-sigs/should_compile/T18008.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T18008.stderr
@@ -1,5 +1,5 @@
 
 T18008.hs:5:43: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘String’
-    • In the type ‘(forall a. Show a => a -> String) -> _’
-      In the type signature: f :: (forall a. Show a => a -> String) -> _
+    • In the type signature:
+        f :: (forall a. Show a => a -> String) -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/T21667.stderr b/testsuite/tests/partial-sigs/should_compile/T21667.stderr
index b76d5bd952..aed4ac1782 100644
--- a/testsuite/tests/partial-sigs/should_compile/T21667.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T21667.stderr
@@ -2,5 +2,4 @@
 T21667.hs:46:40: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘"1" :: Symbol’
     • In the second argument of ‘ExoticTraversal'’, namely ‘_’
-      In the type ‘ExoticTraversal' a _ f’
       In the type signature: test :: forall a f. ExoticTraversal' a _ f
diff --git a/testsuite/tests/partial-sigs/should_compile/T22065.stderr b/testsuite/tests/partial-sigs/should_compile/T22065.stderr
index c1ee219723..558ebcc4de 100644
--- a/testsuite/tests/partial-sigs/should_compile/T22065.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T22065.stderr
@@ -21,8 +21,7 @@ T22065.hs:12:9: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
       Where: ‘w’ is a rigid type variable bound by
                the inferred type of f :: [w] -> Int
                at T22065.hs:13:3-19
-    • In the type ‘[_] -> Int’
-      In the type signature: f :: [_] -> Int
+    • In the type signature: f :: [_] -> Int
       In an equation for ‘foo’:
           foo
             = Apply f x :: forall a. _
@@ -40,8 +39,7 @@ T22065.hs:15:9: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
       Where: ‘w’ is a rigid type variable bound by
                the inferred type of x :: [w]
                at T22065.hs:16:3-17
-    • In the type ‘[_]’
-      In the type signature: x :: [_]
+    • In the type signature: x :: [_]
       In an equation for ‘foo’:
           foo
             = Apply f x :: forall a. _
diff --git a/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr b/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr
index 7e48c8f80a..891e71e1ff 100644
--- a/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/TypedSplice.stderr
@@ -1,9 +1,9 @@
 
 TypedSplice.hs:9:22: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Bool’
-    • In the type ‘_ -> _b’
-      In an expression type signature: _ -> _b
+    • In an expression type signature: _ -> _b
       In the Template Haskell quotation [|| not :: _ -> _b ||]
+      In the expression: [|| not :: _ -> _b ||]
     • Relevant bindings include
         metaExp :: Code Q (Bool -> Bool) (bound at TypedSplice.hs:9:1)
 
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index ee483a62a6..16a82f7aba 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -20,29 +20,25 @@ WarningWildcardInstantiations.hs:5:18: warning: [GHC-88464] [-Wpartial-type-sign
 
 WarningWildcardInstantiations.hs:5:30: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘String’
-    • In the type ‘_a -> _’
-      In the type signature: foo :: (Show _a, _) => _a -> _
+    • In the type signature: foo :: (Show _a, _) => _a -> _
 
 WarningWildcardInstantiations.hs:8:8: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘t’
       Where: ‘t’ is a rigid type variable bound by
                the inferred type of bar :: t -> (t -> w) -> w
                at WarningWildcardInstantiations.hs:9:1-13
-    • In the type ‘_ -> _ -> _’
-      In the type signature: bar :: _ -> _ -> _
+    • In the type signature: bar :: _ -> _ -> _
 
 WarningWildcardInstantiations.hs:8:13: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘t -> w’
       Where: ‘t’, ‘w’ are rigid type variables bound by
                the inferred type of bar :: t -> (t -> w) -> w
                at WarningWildcardInstantiations.hs:9:1-13
-    • In the type ‘_ -> _ -> _’
-      In the type signature: bar :: _ -> _ -> _
+    • In the type signature: bar :: _ -> _ -> _
 
 WarningWildcardInstantiations.hs:8:18: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘w’
       Where: ‘w’ is a rigid type variable bound by
                the inferred type of bar :: t -> (t -> w) -> w
                at WarningWildcardInstantiations.hs:9:1-13
-    • In the type ‘_ -> _ -> _’
-      In the type signature: bar :: _ -> _ -> _
+    • In the type signature: bar :: _ -> _ -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr b/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr
index eb49a8bfed..4f916c20e2 100644
--- a/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/PartialTypeSignaturesDisabled.stderr
@@ -2,11 +2,9 @@
 PartialTypeSignaturesDisabled.hs:4:8: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘Bool’
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _’
-      In the type signature: foo :: _ -> _
+    • In the type signature: foo :: _ -> _
 
 PartialTypeSignaturesDisabled.hs:4:13: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘Bool’
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _’
-      In the type signature: foo :: _ -> _
+    • In the type signature: foo :: _ -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/T10615.stderr b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
index b2390ffa41..8dae5a32f8 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10615.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
@@ -3,8 +3,7 @@ T10615.hs:5:7: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘w1’
       Where: ‘w1’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> f’
-      In the type signature: f1 :: _ -> f
+    • In the type signature: f1 :: _ -> f
 
 T10615.hs:6:6: error: [GHC-25897]
     • Couldn't match type ‘f’ with ‘b1 -> w1’
@@ -21,8 +20,7 @@ T10615.hs:8:7: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘w0’
       Where: ‘w0’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _f’
-      In the type signature: f2 :: _ -> _f
+    • In the type signature: f2 :: _ -> _f
 
 T10615.hs:9:6: error: [GHC-25897]
     • Couldn't match type ‘_f’ with ‘b0 -> w0’
diff --git a/testsuite/tests/partial-sigs/should_fail/T10999.stderr b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
index 39e94b5033..aa22ff9944 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10999.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10999.stderr
@@ -13,8 +13,7 @@ T10999.hs:5:17: error: [GHC-88464]
                the inferred type of f :: Ord a => () -> Set.Set a
                at T10999.hs:6:1-28
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘() -> _’
-      In the type signature: f :: _ => () -> _
+    • In the type signature: f :: _ => () -> _
 
 T10999.hs:8:28: error: [GHC-39999]
     • Ambiguous type variable ‘b1’ arising from a use of ‘f’
@@ -25,7 +24,7 @@ T10999.hs:8:28: error: [GHC-39999]
         instance Ord a => Ord (Set.Set a) -- Defined in ‘Data.Set.Internal’
         instance Ord Ordering -- Defined in ‘GHC.Classes’
         ...plus 24 others
-        ...plus two instances involving out-of-scope types
+        ...plus three instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the second argument of ‘($)’, namely ‘f ()’
       In the second argument of ‘($)’, namely ‘Set.toList $ f ()’
diff --git a/testsuite/tests/partial-sigs/should_fail/T11122.stderr b/testsuite/tests/partial-sigs/should_fail/T11122.stderr
index 1a173ec11a..6fbe3ecdce 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11122.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11122.stderr
@@ -2,5 +2,4 @@
 T11122.hs:19:18: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Int’
     • In the first argument of ‘Parser’, namely ‘_’
-      In the type ‘Parser _’
       In the type signature: parser :: Parser _
diff --git a/testsuite/tests/partial-sigs/should_fail/T11515.stderr b/testsuite/tests/partial-sigs/should_fail/T11515.stderr
index 389b1331b3..c113d8ad6a 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11515.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11515.stderr
@@ -1,5 +1,5 @@
 
 T11515.hs:7:20: error: [GHC-88464]
-    • Found extra-constraints wildcard standing for ‘()’
+    • Found extra-constraints wildcard standing for ‘() :: Constraint’
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (ShowSyn a, _) => a -> String
diff --git a/testsuite/tests/partial-sigs/should_fail/T11976.stderr b/testsuite/tests/partial-sigs/should_fail/T11976.stderr
index a2a1fead7d..f50719ac35 100644
--- a/testsuite/tests/partial-sigs/should_fail/T11976.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T11976.stderr
@@ -1,6 +1,6 @@
 
 T11976.hs:7:20: error: [GHC-83865]
     • Expected kind ‘k0 -> *’, but ‘Lens _ _’ has kind ‘*’
-    • In the type ‘Lens _ _ _’
-      In an expression type signature: Lens _ _ _
+    • In an expression type signature: Lens _ _ _
       In the expression: undefined :: Lens _ _ _
+      In an equation for ‘foo’: foo = undefined :: Lens _ _ _
diff --git a/testsuite/tests/partial-sigs/should_fail/T12634.stderr b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
index 19a65352db..3c2eb498d5 100644
--- a/testsuite/tests/partial-sigs/should_fail/T12634.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T12634.stderr
@@ -1,10 +1,9 @@
 
 T12634.hs:15:58: error: [GHC-83865]
-    • Expected a type, but
-      ‘'(t, m, m', r)’ has kind
+    • Expected a type,
+      but ‘'(t, m, m', r)’ has kind
       ‘(k1 -> k2 -> *, k0, k1, k2)’
     • In the first argument of ‘Bench’, namely ‘'(t, m, m', r)’
-      In the type ‘t m' r -> Bench '(t, m, m', r)’
       In the type signature:
         bench_twacePow :: forall t m m' r. _ =>
                                            t m' r -> Bench '(t, m, m', r)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 6f5ee1ff2e..5614422045 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -3,17 +3,12 @@ T14040a.hs:26:46: error: [GHC-46956]
     • Couldn't match kind ‘k1’ with ‘WeirdList z’
       Expected kind ‘WeirdList k1’,
         but ‘xs’ has kind ‘WeirdList (WeirdList z)’
-    • because kind variable ‘z’ would escape its scope
-    This (rigid, skolem) kind variable is bound by
-      an explicit forall (z :: Type) (x :: z)
-                         (xs :: WeirdList (WeirdList z))
-      at T14040a.hs:25:26-77
+        because kind variable ‘z’ would escape its scope
+      This (rigid, skolem) kind variable is bound by
+        an explicit forall (z :: Type) (x :: z)
+                           (xs :: WeirdList (WeirdList z))
+        at T14040a.hs:25:26-77
     • In the second argument of ‘p’, namely ‘xs’
-      In the type ‘Sing wl
-                   -> (forall (y :: Type). p _ WeirdNil)
-                      -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
-                          Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-                         -> p _ wl’
       In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
@@ -33,17 +28,12 @@ T14040a.hs:27:27: error: [GHC-46956]
     • Couldn't match kind ‘k0’ with ‘z’
       Expected kind ‘WeirdList k0’,
         but ‘WeirdCons x xs’ has kind ‘WeirdList z’
-    • because kind variable ‘z’ would escape its scope
-    This (rigid, skolem) kind variable is bound by
-      an explicit forall (z :: Type) (x :: z)
-                         (xs :: WeirdList (WeirdList z))
-      at T14040a.hs:25:26-77
+        because kind variable ‘z’ would escape its scope
+      This (rigid, skolem) kind variable is bound by
+        an explicit forall (z :: Type) (x :: z)
+                           (xs :: WeirdList (WeirdList z))
+        at T14040a.hs:25:26-77
     • In the second argument of ‘p’, namely ‘(WeirdCons x xs)’
-      In the type ‘Sing wl
-                   -> (forall (y :: Type). p _ WeirdNil)
-                      -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
-                          Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-                         -> p _ wl’
       In the type signature:
         elimWeirdList :: forall (a :: Type)
                                 (wl :: WeirdList a)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index 67ccd9d0da..fcad722d63 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -42,7 +42,8 @@ T14584.hs:57:60: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
                the instance declaration
                at T14584.hs:55:10-89
     • In the first argument of ‘Sing’, namely ‘_’
-      In the type ‘Sing _’
       In an expression type signature: Sing _
+      In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
     • Relevant bindings include
         monHom :: a -> a (bound at T14584.hs:57:3)
diff --git a/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr b/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
index b354fd8d01..6b3e70e8b9 100644
--- a/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/TidyClash.stderr
@@ -5,8 +5,7 @@ TidyClash.hs:8:19: error: [GHC-88464]
                the inferred type of bar :: w_ -> (w_, w1 -> w2)
                at TidyClash.hs:9:1-28
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘w_ -> (w_, _ -> _)’
-      In the type signature: bar :: w_ -> (w_, _ -> _)
+    • In the type signature: bar :: w_ -> (w_, _ -> _)
 
 TidyClash.hs:8:24: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘w2’
@@ -14,5 +13,4 @@ TidyClash.hs:8:24: error: [GHC-88464]
                the inferred type of bar :: w_ -> (w_, w1 -> w2)
                at TidyClash.hs:9:1-28
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘w_ -> (w_, _ -> _)’
-      In the type signature: bar :: w_ -> (w_, _ -> _)
+    • In the type signature: bar :: w_ -> (w_, _ -> _)
diff --git a/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr b/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
index d6c07d7ba7..acab0a2052 100644
--- a/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/TidyClash2.stderr
@@ -5,8 +5,7 @@ TidyClash2.hs:13:20: error: [GHC-88464]
                the inferred type of barry :: w1 -> w2 -> t
                at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _ -> t’
-      In the type signature: barry :: forall t. _ -> _ -> t
+    • In the type signature: barry :: forall t. _ -> _ -> t
 
 TidyClash2.hs:13:25: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘w2’
@@ -14,8 +13,7 @@ TidyClash2.hs:13:25: error: [GHC-88464]
                the inferred type of barry :: w1 -> w2 -> t
                at TidyClash2.hs:14:1-40
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _ -> t’
-      In the type signature: barry :: forall t. _ -> _ -> t
+    • In the type signature: barry :: forall t. _ -> _ -> t
 
 TidyClash2.hs:14:13: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘w1’
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index a9804d8dcb..7bab8376f9 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -18,8 +18,7 @@ WildcardInstantiations.hs:5:18: error: [GHC-88464]
 WildcardInstantiations.hs:5:30: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘String’
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_a -> _’
-      In the type signature: foo :: (Show _a, _) => _a -> _
+    • In the type signature: foo :: (Show _a, _) => _a -> _
 
 WildcardInstantiations.hs:8:8: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘t’
@@ -27,8 +26,7 @@ WildcardInstantiations.hs:8:8: error: [GHC-88464]
                the inferred type of bar :: t -> (t -> w) -> w
                at WildcardInstantiations.hs:9:1-13
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _ -> _’
-      In the type signature: bar :: _ -> _ -> _
+    • In the type signature: bar :: _ -> _ -> _
 
 WildcardInstantiations.hs:8:13: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘t -> w’
@@ -36,8 +34,7 @@ WildcardInstantiations.hs:8:13: error: [GHC-88464]
                the inferred type of bar :: t -> (t -> w) -> w
                at WildcardInstantiations.hs:9:1-13
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _ -> _’
-      In the type signature: bar :: _ -> _ -> _
+    • In the type signature: bar :: _ -> _ -> _
 
 WildcardInstantiations.hs:8:18: error: [GHC-88464]
     • Found type wildcard ‘_’ standing for ‘w’
@@ -45,5 +42,4 @@ WildcardInstantiations.hs:8:18: error: [GHC-88464]
                the inferred type of bar :: t -> (t -> w) -> w
                at WildcardInstantiations.hs:9:1-13
       To use the inferred type, enable PartialTypeSignatures
-    • In the type ‘_ -> _ -> _’
-      In the type signature: bar :: _ -> _ -> _
+    • In the type signature: bar :: _ -> _ -> _