Fix #15039 by pretty-printing equalities more systematically

GHC previously had a handful of special cases for
pretty-printing equalities in a more user-friendly manner, but they
were far from comprehensive (see #15039 for an example of where this
fell apart).

This patch makes the pretty-printing of equalities much more
systematic. I've adopted the approach laid out in
https://ghc.haskell.org/trac/ghc/ticket/15039#comment:4, and updated
`Note [Equality predicates in IfaceType]` accordingly. We are now
more careful to respect the properties of the
`-fprint-explicit-kinds` and `-fprint-equality-relations` flags,
which led to some improvements in error message outputs.

Along the way, I also tweaked the error-reporting machinery not to
print out the type of a typed hole when the type is an unlifted
equality, since it's kind (`TYPE ('TupleRep '[])`) was more
confusing than anything.

Test Plan: make test TEST="T15039a T15039b T15039c T15039d"

Reviewers: simonpj, goldfire, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15039

Differential Revision: https://phabricator.haskell.org/D4696

17 files changed, 496 insertions, 49 deletions

diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 81d070a493..6f548f5b12 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -52,7 +52,8 @@ module IfaceType (
 
 import GhcPrelude
 
-import {-# SOURCE #-} TysWiredIn ( liftedRepDataConTyCon )
+import {-# SOURCE #-} TysWiredIn ( coercibleTyCon, heqTyCon
+                                 , liftedRepDataConTyCon )
 import {-# SOURCE #-} TyCoRep    ( isRuntimeRepTy )
 
 import DynFlags
@@ -220,27 +221,56 @@ Note [Equality predicates in IfaceType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 GHC has several varieties of type equality (see Note [The equality types story]
 in TysPrim for details).  In an effort to avoid confusing users, we suppress
-the differences during "normal" pretty printing.  Specifically we display them
-like this:
-
- Predicate                         Pretty-printed as
-                          Homogeneous case        Heterogeneous case
- ----------------        -----------------        -------------------
- (~)    eqTyCon                 ~                  N/A
- (~~)   heqTyCon                ~                  ~~
- (~#)   eqPrimTyCon             ~#                 ~~
- (~R#)  eqReprPrimTyCon         Coercible          Coercible
-
-By "homogeneeous case" we mean cases where a hetero-kinded equality
-(all but the first above) is actually applied to two identical kinds.
-Unfortunately, determining this from an IfaceType isn't possible since
-we can't see through type synonyms. Consequently, we need to record
-whether this particular application is homogeneous in IfaceTyConSort
+the differences during pretty printing unless certain flags are enabled.
+Here is how each equality predicate* is printed in homogeneous and
+heterogeneous contexts, depending on which combination of the
+-fprint-explicit-kinds and -fprint-equality-relations flags is used:
+
+---------------------------------------------------------------------------------------
+|         Predicate             |        Neither flag        | -fprint-explicit-kinds |
+|-------------------------------|----------------------------|------------------------|
+| a ~ b         (homogeneous)   |        a ~ b               | (a :: *) ~  (b :: *)   |
+| a ~~ b,       homogeneously   |        a ~ b               | (a :: *) ~  (b :: *)   |
+| a ~~ b,       heterogeneously |        a ~~ c              | (a :: *) ~~ (c :: k)   |
+| a ~# b,       homogeneously   |        a ~ b               | (a :: *) ~  (b :: *)   |
+| a ~# b,       heterogeneously |        a ~~ c              | (a :: *) ~~ (c :: k)   |
+| Coercible a b (homogeneous)   |        Coercible a b       | Coercible * a b        |
+| a ~R# b,      homogeneously   |        Coercible a b       | Coercible * a b        |
+| a ~R# b,      heterogeneously |        a ~R# b             | (a :: *) ~R# (c :: k)  |
+|-------------------------------|----------------------------|------------------------|
+|         Predicate             | -fprint-equality-relations |      Both flags        |
+|-------------------------------|----------------------------|------------------------|
+| a ~ b         (homogeneous)   |        a ~  b              | (a :: *) ~  (b :: *)   |
+| a ~~ b,       homogeneously   |        a ~~ b              | (a :: *) ~~ (b :: *)   |
+| a ~~ b,       heterogeneously |        a ~~ c              | (a :: *) ~~ (c :: k)   |
+| a ~# b,       homogeneously   |        a ~# b              | (a :: *) ~# (b :: *)   |
+| a ~# b,       heterogeneously |        a ~# c              | (a :: *) ~# (c :: k)   |
+| Coercible a b (homogeneous)   |        Coercible a b       | Coercible * a b        |
+| a ~R# b,      homogeneously   |        a ~R# b             | (a :: *) ~R# (b :: *)  |
+| a ~R# b,      heterogeneously |        a ~R# b             | (a :: *) ~R# (c :: k)  |
+---------------------------------------------------------------------------------------
+
+(* There is no heterogeneous, representational, lifted equality counterpart
+to (~~). There could be, but there seems to be no use for it.)
+
+This table adheres to the following rules:
+
+A. With -fprint-equality-relations, print the true equality relation.
+B. Without -fprint-equality-relations:
+     i. If the equality is representational and homogeneous, use Coercible.
+    ii. Otherwise, if the equality is representational, use ~R#.
+   iii. If the equality is nominal and homogeneous, use ~.
+    iv. Otherwise, if the equality is nominal, use ~~.
+C. With -fprint-explicit-kinds, print kinds on both sides of an infix operator,
+   as above; or print the kind with Coercible.
+D. Without -fprint-explicit-kinds, don't print kinds.
+
+A hetero-kinded equality is used homogeneously when it is applied to two
+identical kinds. Unfortunately, determining this from an IfaceType isn't
+possible since we can't see through type synonyms. Consequently, we need to
+record whether this particular application is homogeneous in IfaceTyConSort
 for the purposes of pretty-printing.
 
-All this suppresses information. To get the ground truth, use -dppr-debug
-(see 'print_eqs' in 'ppr_equality').
-
 See Note [The equality types story] in TysPrim.
 -}
 
@@ -1001,11 +1031,15 @@ ppr_equality ctxt_prec tc args
   | otherwise
   = Nothing
   where
-    homogeneous = case ifaceTyConSort $ ifaceTyConInfo tc of
-                    IfaceEqualityTyCon -> True
-                    _other             -> False
-       -- True <=> a heterogeneous equality whose arguments
-       --          are (in this case) of the same kind
+    homogeneous = tc_name `hasKey` eqTyConKey -- (~)
+               || hetero_tc_used_homogeneously
+      where
+        hetero_tc_used_homogeneously
+          = case ifaceTyConSort $ ifaceTyConInfo tc of
+                          IfaceEqualityTyCon -> True
+                          _other             -> False
+             -- True <=> a heterogeneous equality whose arguments
+             --          are (in this case) of the same kind
 
     tc_name = ifaceTyConName tc
     pp = ppr_ty
@@ -1013,30 +1047,47 @@ ppr_equality ctxt_prec tc args
     hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey     -- (~#)
                 || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
                 || tc_name `hasKey` heqTyConKey        -- (~~)
+    nominal_eq_tc = tc_name `hasKey` heqTyConKey       -- (~~)
+                 || tc_name `hasKey` eqPrimTyConKey    -- (~#)
     print_equality args =
         sdocWithDynFlags $ \dflags ->
         getPprStyle      $ \style  ->
         print_equality' args style dflags
 
     print_equality' (ki1, ki2, ty1, ty2) style dflags
-      | print_eqs   -- No magic, just print the original TyCon
+      | -- If -fprint-equality-relations is on, just print the original TyCon
+        print_eqs
       = ppr_infix_eq (ppr tc)
 
-      | hetero_eq_tc
-      , print_kinds || not homogeneous
-      = ppr_infix_eq (text "~~")
+      | -- Homogeneous use of heterogeneous equality (ty1 ~~ ty2)
+        --                 or unlifted equality      (ty1 ~# ty2)
+        nominal_eq_tc, homogeneous
+      = ppr_infix_eq (text "~")
+
+      | -- Heterogeneous use of unlifted equality (ty1 ~# ty2)
+        not homogeneous
+      = ppr_infix_eq (ppr heqTyCon)
 
+      | -- Homogeneous use of representational unlifted equality (ty1 ~R# ty2)
+        tc_name `hasKey` eqReprPrimTyConKey, homogeneous
+      = let ki | print_kinds = [pp appPrec ki1]
+               | otherwise   = []
+        in pprIfacePrefixApp ctxt_prec (ppr coercibleTyCon)
+                            (ki ++ [pp appPrec ty1, pp appPrec ty2])
+
+        -- The other cases work as you'd expect
       | otherwise
-      = if tc_name `hasKey` eqReprPrimTyConKey
-        then pprIfacePrefixApp ctxt_prec (text "Coercible")
-                               [pp appPrec ty1, pp appPrec ty2]
-        else pprIfaceInfixApp ctxt_prec (char '~')
-                 (pp opPrec ty1) (pp opPrec ty2)
+      = ppr_infix_eq (ppr tc)
       where
-        ppr_infix_eq eq_op
-           = pprIfaceInfixApp ctxt_prec eq_op
-                 (parens (pp topPrec ty1 <+> dcolon <+> pp opPrec ki1))
-                 (parens (pp topPrec ty2 <+> dcolon <+> pp opPrec ki2))
+        ppr_infix_eq :: SDoc -> SDoc
+        ppr_infix_eq eq_op = pprIfaceInfixApp ctxt_prec eq_op
+                               (pp_ty_ki ty1 ki1) (pp_ty_ki ty2 ki2)
+          where
+            pp_ty_ki ty ki
+              | print_kinds
+              = parens (pp topPrec ty <+> dcolon <+> pp opPrec ki)
+              | otherwise
+              = pp opPrec ty
 
         print_kinds = gopt Opt_PrintExplicitKinds dflags
         print_eqs   = gopt Opt_PrintEqualityRelations dflags ||
diff --git a/compiler/prelude/TysWiredIn.hs-boot b/compiler/prelude/TysWiredIn.hs-boot
index 26e42010c9..b777fa187b 100644
--- a/compiler/prelude/TysWiredIn.hs-boot
+++ b/compiler/prelude/TysWiredIn.hs-boot
@@ -12,6 +12,8 @@ listTyCon :: TyCon
 typeNatKind, typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
 
+coercibleTyCon, heqTyCon :: TyCon
+
 liftedTypeKind :: Kind
 constraintKind :: Kind
 
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 5fa69867df..7a681b53a8 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1170,8 +1170,12 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
                           , tyvars_msg, type_hole_hint ]
 
     pp_hole_type_with_kind
-      | isLiftedTypeKind hole_kind = pprType hole_ty
-      | otherwise                  = pprType hole_ty <+> dcolon <+> pprKind hole_kind
+      | isLiftedTypeKind hole_kind
+        || isCoercionType hole_ty -- Don't print the kind of unlifted
+                                  -- equalities (#15039)
+      = pprType hole_ty
+      | otherwise
+      = pprType hole_ty <+> dcolon <+> pprKind hole_kind
 
     tyvars_msg = ppUnless (null tyvars) $
                  text "Where:" <+> (vcat (map loc_msg other_tvs)
diff --git a/testsuite/tests/deSugar/should_compile/T2431.stderr b/testsuite/tests/deSugar/should_compile/T2431.stderr
index e1c4b43d16..3c1c232887 100644
--- a/testsuite/tests/deSugar/should_compile/T2431.stderr
+++ b/testsuite/tests/deSugar/should_compile/T2431.stderr
@@ -11,11 +11,9 @@ T2431.$WRefl [InlPrag=INLINE[2]] :: forall a. a :~: a
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (@ a) ->
-                 T2431.Refl @ a @ a @~ (<a>_N :: (a :: *) GHC.Prim.~# (a :: *))}]
+         Tmpl= \ (@ a) -> T2431.Refl @ a @ a @~ (<a>_N :: a GHC.Prim.~# a)}]
 T2431.$WRefl
-  = \ (@ a) ->
-      T2431.Refl @ a @ a @~ (<a>_N :: (a :: *) GHC.Prim.~# (a :: *))
+  = \ (@ a) -> T2431.Refl @ a @ a @~ (<a>_N :: a GHC.Prim.~# a)
 
 -- RHS size: {terms: 4, types: 8, coercions: 0, joins: 0/0}
 absurd :: forall a. (Int :~: Bool) -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.hs b/testsuite/tests/partial-sigs/should_compile/T15039a.hs
new file mode 100644
index 0000000000..7f32cb8488
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039a.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+module T15039a where
+
+import Data.Coerce
+import Data.Kind
+import Data.Type.Coercion
+import Data.Type.Equality
+
+data Dict :: Constraint -> Type where
+  Dict :: c => Dict c
+
+ex1 :: Dict ((a :: *) ~ (b :: *)) -> ()
+ex1 (Dict :: _) = ()
+
+ex2 :: Dict ((a :: *) ~~ (b :: *)) -> ()
+ex2 (Dict :: _) = ()
+
+ex3 :: Dict ((a :: *) ~~ (b :: k)) -> ()
+ex3 (Dict :: _) = ()
+
+-- Don't know how to make GHC print an unlifted, nominal equality in an error
+-- message.
+--
+-- ex4, ex5 :: ???
+
+ex6 :: Dict (Coercible (a :: *) (b :: *)) -> ()
+ex6 (Dict :: _) = ()
+
+ex7 :: _ => Coercion (a :: *) (b :: *)
+ex7 = Coercion
+
+-- Don't know how to make GHC print an unlifted, heterogeneous,
+-- representational equality in an error message.
+--
+-- ex8 :: ???
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
new file mode 100644
index 0000000000..c45e82e5ef
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
@@ -0,0 +1,55 @@
+
+T15039a.hs:19:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (a ~ b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex1 :: forall a b. Dict (a ~ b) -> ()
+               at T15039a.hs:18:1-39
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex1’: ex1 (Dict :: _) = ()
+    • Relevant bindings include
+        ex1 :: Dict (a ~ b) -> () (bound at T15039a.hs:19:1)
+
+T15039a.hs:22:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (a ~ b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex2 :: forall a b. Dict (a ~ b) -> ()
+               at T15039a.hs:21:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex2’: ex2 (Dict :: _) = ()
+    • Relevant bindings include
+        ex2 :: Dict (a ~ b) -> () (bound at T15039a.hs:22:1)
+
+T15039a.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
+      Where: ‘a’, ‘b’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 ex3 :: forall k a (b :: k). Dict (a ~~ b) -> ()
+               at T15039a.hs:24:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex3’: ex3 (Dict :: _) = ()
+    • Relevant bindings include
+        ex3 :: Dict (a ~~ b) -> () (bound at T15039a.hs:25:1)
+
+T15039a.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (Coercible a b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex6 :: forall a b. Dict (Coercible a b) -> ()
+               at T15039a.hs:32:1-47
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex6’: ex6 (Dict :: _) = ()
+    • Relevant bindings include
+        ex6 :: Dict (Coercible a b) -> () (bound at T15039a.hs:33:1)
+
+T15039a.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Coercible a b’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the inferred type of ex7 :: Coercible a b => Coercion a b
+               at T15039a.hs:36:1-14
+    • In the type signature: ex7 :: _ => Coercion (a :: *) (b :: *)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.hs b/testsuite/tests/partial-sigs/should_compile/T15039b.hs
new file mode 100644
index 0000000000..4966059912
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039b.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+module T15039b where
+
+import Data.Coerce
+import Data.Kind
+import Data.Type.Coercion
+import Data.Type.Equality
+
+data Dict :: Constraint -> Type where
+  Dict :: c => Dict c
+
+ex1 :: Dict ((a :: *) ~ (b :: *)) -> ()
+ex1 (Dict :: _) = ()
+
+ex2 :: Dict ((a :: *) ~~ (b :: *)) -> ()
+ex2 (Dict :: _) = ()
+
+ex3 :: Dict ((a :: *) ~~ (b :: k)) -> ()
+ex3 (Dict :: _) = ()
+
+-- Don't know how to make GHC print an unlifted, nominal equality in an error
+-- message.
+--
+-- ex4, ex5 :: ???
+
+ex6 :: Dict (Coercible (a :: *) (b :: *)) -> ()
+ex6 (Dict :: _) = ()
+
+ex7 :: _ => Coercion (a :: *) (b :: *)
+ex7 = Coercion
+
+-- Don't know how to make GHC print an unlifted, heterogeneous,
+-- representational equality in an error message.
+--
+-- ex8 :: ???
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
new file mode 100644
index 0000000000..dffde1c8f1
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
@@ -0,0 +1,56 @@
+
+T15039b.hs:19:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict ((a :: *) ~ (b :: *))’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex1 :: forall a b. Dict ((a :: *) ~ (b :: *)) -> ()
+               at T15039b.hs:18:1-39
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex1’: ex1 (Dict :: _) = ()
+    • Relevant bindings include
+        ex1 :: Dict ((a :: *) ~ (b :: *)) -> () (bound at T15039b.hs:19:1)
+
+T15039b.hs:22:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict ((a :: *) ~ (b :: *))’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex2 :: forall a b. Dict ((a :: *) ~ (b :: *)) -> ()
+               at T15039b.hs:21:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex2’: ex2 (Dict :: _) = ()
+    • Relevant bindings include
+        ex2 :: Dict ((a :: *) ~ (b :: *)) -> () (bound at T15039b.hs:22:1)
+
+T15039b.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’
+        standing for ‘Dict ((a :: *) ~~ (b :: k))’
+      Where: ‘a’, ‘b’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
+               at T15039b.hs:24:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex3’: ex3 (Dict :: _) = ()
+    • Relevant bindings include
+        ex3 :: Dict ((a :: *) ~~ (b :: k)) -> () (bound at T15039b.hs:25:1)
+
+T15039b.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (Coercible * a b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex6 :: forall a b. Dict (Coercible * a b) -> ()
+               at T15039b.hs:32:1-47
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex6’: ex6 (Dict :: _) = ()
+    • Relevant bindings include
+        ex6 :: Dict (Coercible * a b) -> () (bound at T15039b.hs:33:1)
+
+T15039b.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Coercible * a b’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the inferred type of ex7 :: Coercible * a b => Coercion * a b
+               at T15039b.hs:36:1-14
+    • In the type signature: ex7 :: _ => Coercion (a :: *) (b :: *)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.hs b/testsuite/tests/partial-sigs/should_compile/T15039c.hs
new file mode 100644
index 0000000000..aa54c4e919
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039c.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+module T15039c where
+
+import Data.Coerce
+import Data.Kind
+import Data.Type.Coercion
+import Data.Type.Equality
+
+data Dict :: Constraint -> Type where
+  Dict :: c => Dict c
+
+ex1 :: Dict ((a :: *) ~ (b :: *)) -> ()
+ex1 (Dict :: _) = ()
+
+ex2 :: Dict ((a :: *) ~~ (b :: *)) -> ()
+ex2 (Dict :: _) = ()
+
+ex3 :: Dict ((a :: *) ~~ (b :: k)) -> ()
+ex3 (Dict :: _) = ()
+
+-- Don't know how to make GHC print an unlifted, nominal equality in an error
+-- message.
+--
+-- ex4, ex5 :: ???
+
+ex6 :: Dict (Coercible (a :: *) (b :: *)) -> ()
+ex6 (Dict :: _) = ()
+
+ex7 :: _ => Coercion (a :: *) (b :: *)
+ex7 = Coercion
+
+-- Don't know how to make GHC print an unlifted, heterogeneous,
+-- representational equality in an error message.
+--
+-- ex8 :: ???
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
new file mode 100644
index 0000000000..bf3aff1081
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
@@ -0,0 +1,55 @@
+
+T15039c.hs:19:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (a ~ b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex1 :: forall a b. Dict (a ~ b) -> ()
+               at T15039c.hs:18:1-39
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex1’: ex1 (Dict :: _) = ()
+    • Relevant bindings include
+        ex1 :: Dict (a ~ b) -> () (bound at T15039c.hs:19:1)
+
+T15039c.hs:22:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex2 :: forall a b. Dict (a ~~ b) -> ()
+               at T15039c.hs:21:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex2’: ex2 (Dict :: _) = ()
+    • Relevant bindings include
+        ex2 :: Dict (a ~~ b) -> () (bound at T15039c.hs:22:1)
+
+T15039c.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
+      Where: ‘a’, ‘b’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 ex3 :: forall k a (b :: k). Dict (a ~~ b) -> ()
+               at T15039c.hs:24:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex3’: ex3 (Dict :: _) = ()
+    • Relevant bindings include
+        ex3 :: Dict (a ~~ b) -> () (bound at T15039c.hs:25:1)
+
+T15039c.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (Coercible a b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex6 :: forall a b. Dict (Coercible a b) -> ()
+               at T15039c.hs:32:1-47
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex6’: ex6 (Dict :: _) = ()
+    • Relevant bindings include
+        ex6 :: Dict (Coercible a b) -> () (bound at T15039c.hs:33:1)
+
+T15039c.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘a ~R# b’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the inferred type of ex7 :: (a ~R# b) => Coercion a b
+               at T15039c.hs:36:1-14
+    • In the type signature: ex7 :: _ => Coercion (a :: *) (b :: *)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.hs b/testsuite/tests/partial-sigs/should_compile/T15039d.hs
new file mode 100644
index 0000000000..3b5a5a27c3
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039d.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+module T15039d where
+
+import Data.Coerce
+import Data.Kind
+import Data.Type.Coercion
+import Data.Type.Equality
+
+data Dict :: Constraint -> Type where
+  Dict :: c => Dict c
+
+ex1 :: Dict ((a :: *) ~ (b :: *)) -> ()
+ex1 (Dict :: _) = ()
+
+ex2 :: Dict ((a :: *) ~~ (b :: *)) -> ()
+ex2 (Dict :: _) = ()
+
+ex3 :: Dict ((a :: *) ~~ (b :: k)) -> ()
+ex3 (Dict :: _) = ()
+
+-- Don't know how to make GHC print an unlifted, nominal equality in an error
+-- message.
+--
+-- ex4, ex5 :: ???
+
+ex6 :: Dict (Coercible (a :: *) (b :: *)) -> ()
+ex6 (Dict :: _) = ()
+
+ex7 :: _ => Coercion (a :: *) (b :: *)
+ex7 = Coercion
+
+-- Don't know how to make GHC print an unlifted, heterogeneous,
+-- representational equality in an error message.
+--
+-- ex8 :: ???
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
new file mode 100644
index 0000000000..8595955f87
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
@@ -0,0 +1,58 @@
+
+T15039d.hs:19:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict ((a :: *) ~ (b :: *))’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex1 :: forall a b. Dict ((a :: *) ~ (b :: *)) -> ()
+               at T15039d.hs:18:1-39
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex1’: ex1 (Dict :: _) = ()
+    • Relevant bindings include
+        ex1 :: Dict ((a :: *) ~ (b :: *)) -> () (bound at T15039d.hs:19:1)
+
+T15039d.hs:22:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’
+        standing for ‘Dict ((a :: *) ~~ (b :: *))’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex2 :: forall a b. Dict ((a :: *) ~~ (b :: *)) -> ()
+               at T15039d.hs:21:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex2’: ex2 (Dict :: _) = ()
+    • Relevant bindings include
+        ex2 :: Dict ((a :: *) ~~ (b :: *)) -> () (bound at T15039d.hs:22:1)
+
+T15039d.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’
+        standing for ‘Dict ((a :: *) ~~ (b :: k))’
+      Where: ‘a’, ‘b’, ‘k’ are rigid type variables bound by
+               the type signature for:
+                 ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
+               at T15039d.hs:24:1-40
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex3’: ex3 (Dict :: _) = ()
+    • Relevant bindings include
+        ex3 :: Dict ((a :: *) ~~ (b :: k)) -> () (bound at T15039d.hs:25:1)
+
+T15039d.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Dict (Coercible * a b)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the type signature for:
+                 ex6 :: forall a b. Dict (Coercible * a b) -> ()
+               at T15039d.hs:32:1-47
+    • In a pattern type signature: _
+      In the pattern: Dict :: _
+      In an equation for ‘ex6’: ex6 (Dict :: _) = ()
+    • Relevant bindings include
+        ex6 :: Dict (Coercible * a b) -> () (bound at T15039d.hs:33:1)
+
+T15039d.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘(a :: *) ~R# (b :: *)’
+      Where: ‘a’, ‘b’ are rigid type variables bound by
+               the inferred type of
+                 ex7 :: ((a :: *) ~R# (b :: *)) => Coercion * a b
+               at T15039d.hs:36:1-14
+    • In the type signature: ex7 :: _ => Coercion (a :: *) (b :: *)
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 0a0483b139..bdfc13d284 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -75,4 +75,8 @@ test('T14217', normal, compile_fail, [''])
 test('T14643', normal, compile, [''])
 test('T14643a', normal, compile, [''])
 test('T14715', normal, compile, [''])
-
+test('T15039a', normal, compile, [''])
+test('T15039b', normal, compile, ['-fprint-explicit-kinds'])
+test('T15039c', normal, compile, ['-fprint-equality-relations'])
+test('T15039d', normal, compile,
+                ['-fprint-explicit-kinds -fprint-equality-relations'])
diff --git a/testsuite/tests/patsyn/should_compile/T14394.stdout b/testsuite/tests/patsyn/should_compile/T14394.stdout
index 6495f9ee35..557b8f4a74 100644
--- a/testsuite/tests/patsyn/should_compile/T14394.stdout
+++ b/testsuite/tests/patsyn/should_compile/T14394.stdout
@@ -3,7 +3,7 @@ pattern Foo :: () => (b ~ a) => a :~~: b
 pattern Bar
   :: forall k2 k1 (a :: k1) (b :: k2).
      () =>
-     (k2 ~ k1, (b :: k2) ~~ (a :: k1)) =>
+     (k2 ~ k1, b ~~ a) =>
      a :~~: b
   	-- Defined at <interactive>:11:1
 pattern Bam :: () => Ord a => a -> a -> (S a, S a)
diff --git a/testsuite/tests/roles/should_compile/Roles13.stderr b/testsuite/tests/roles/should_compile/Roles13.stderr
index 67ff4035c3..29b7b2de26 100644
--- a/testsuite/tests/roles/should_compile/Roles13.stderr
+++ b/testsuite/tests/roles/should_compile/Roles13.stderr
@@ -14,7 +14,7 @@ convert :: Wrap Age -> Int
 convert
   = convert1
     `cast` (<Wrap Age>_R ->_R Roles13.N:Wrap[0] (Roles13.N:Age[0])
-            :: (Wrap Age -> Wrap Age :: *) ~R# (Wrap Age -> Int :: *))
+            :: (Wrap Age -> Wrap Age) ~R# (Wrap Age -> Int))
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
 $trModule1 :: GHC.Prim.Addr#
diff --git a/testsuite/tests/typecheck/should_compile/T13032.stderr b/testsuite/tests/typecheck/should_compile/T13032.stderr
index f7620c75a2..5492b791d7 100644
--- a/testsuite/tests/typecheck/should_compile/T13032.stderr
+++ b/testsuite/tests/typecheck/should_compile/T13032.stderr
@@ -4,7 +4,7 @@ Result size of Desugar (after optimization)
   = {terms: 13, types: 24, coercions: 0, joins: 0/0}
 
 -- RHS size: {terms: 6, types: 11, coercions: 0, joins: 0/0}
-f :: forall a b. ((a :: *) ~ (b :: *)) => a -> b -> Bool
+f :: forall a b. (a ~ b) => a -> b -> Bool
 [LclIdX]
 f = \ (@ a) (@ b) _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] ->
       GHC.Types.True
diff --git a/testsuite/tests/typecheck/should_fail/T14390.stderr b/testsuite/tests/typecheck/should_fail/T14390.stderr
index f94bf40700..0dd72a1e3e 100644
--- a/testsuite/tests/typecheck/should_fail/T14390.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14390.stderr
@@ -1,5 +1,5 @@
 
 T14390.hs:4:10: error:
-    • Illegal instance declaration for ‘(Int :: *) ~~ (Int :: *)’
+    • Illegal instance declaration for ‘Int ~~ Int’
         Manual instances of this class are not permitted.
     • In the instance declaration for ‘(~~) Int Int’