Commit 99f8cc84 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari
Browse files

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
parent 126b4125
...@@ -52,7 +52,8 @@ module IfaceType ( ...@@ -52,7 +52,8 @@ module IfaceType (
import GhcPrelude import GhcPrelude
import {-# SOURCE #-} TysWiredIn ( liftedRepDataConTyCon ) import {-# SOURCE #-} TysWiredIn ( coercibleTyCon, heqTyCon
, liftedRepDataConTyCon )
import {-# SOURCE #-} TyCoRep ( isRuntimeRepTy ) import {-# SOURCE #-} TyCoRep ( isRuntimeRepTy )
import DynFlags import DynFlags
...@@ -220,27 +221,56 @@ Note [Equality predicates in IfaceType] ...@@ -220,27 +221,56 @@ Note [Equality predicates in IfaceType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC has several varieties of type equality (see Note [The equality types story] 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 in TysPrim for details). In an effort to avoid confusing users, we suppress
the differences during "normal" pretty printing. Specifically we display them the differences during pretty printing unless certain flags are enabled.
like this: Here is how each equality predicate* is printed in homogeneous and
heterogeneous contexts, depending on which combination of the
Predicate Pretty-printed as -fprint-explicit-kinds and -fprint-equality-relations flags is used:
Homogeneous case Heterogeneous case
---------------- ----------------- ------------------- ---------------------------------------------------------------------------------------
(~) eqTyCon ~ N/A | Predicate | Neither flag | -fprint-explicit-kinds |
(~~) heqTyCon ~ ~~ |-------------------------------|----------------------------|------------------------|
(~#) eqPrimTyCon ~# ~~ | a ~ b (homogeneous) | a ~ b | (a :: *) ~ (b :: *) |
(~R#) eqReprPrimTyCon Coercible Coercible | a ~~ b, homogeneously | a ~ b | (a :: *) ~ (b :: *) |
| a ~~ b, heterogeneously | a ~~ c | (a :: *) ~~ (c :: k) |
By "homogeneeous case" we mean cases where a hetero-kinded equality | a ~# b, homogeneously | a ~ b | (a :: *) ~ (b :: *) |
(all but the first above) is actually applied to two identical kinds. | a ~# b, heterogeneously | a ~~ c | (a :: *) ~~ (c :: k) |
Unfortunately, determining this from an IfaceType isn't possible since | Coercible a b (homogeneous) | Coercible a b | Coercible * a b |
we can't see through type synonyms. Consequently, we need to record | a ~R# b, homogeneously | Coercible a b | Coercible * a b |
whether this particular application is homogeneous in IfaceTyConSort | 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. 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. See Note [The equality types story] in TysPrim.
-} -}
...@@ -1001,7 +1031,11 @@ ppr_equality ctxt_prec tc args ...@@ -1001,7 +1031,11 @@ ppr_equality ctxt_prec tc args
| otherwise | otherwise
= Nothing = Nothing
where where
homogeneous = case ifaceTyConSort $ ifaceTyConInfo tc of homogeneous = tc_name `hasKey` eqTyConKey -- (~)
|| hetero_tc_used_homogeneously
where
hetero_tc_used_homogeneously
= case ifaceTyConSort $ ifaceTyConInfo tc of
IfaceEqualityTyCon -> True IfaceEqualityTyCon -> True
_other -> False _other -> False
-- True <=> a heterogeneous equality whose arguments -- True <=> a heterogeneous equality whose arguments
...@@ -1013,30 +1047,47 @@ ppr_equality ctxt_prec tc args ...@@ -1013,30 +1047,47 @@ ppr_equality ctxt_prec tc args
hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey -- (~#) hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey -- (~#)
|| tc_name `hasKey` eqReprPrimTyConKey -- (~R#) || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
|| tc_name `hasKey` heqTyConKey -- (~~) || tc_name `hasKey` heqTyConKey -- (~~)
nominal_eq_tc = tc_name `hasKey` heqTyConKey -- (~~)
|| tc_name `hasKey` eqPrimTyConKey -- (~#)
print_equality args = print_equality args =
sdocWithDynFlags $ \dflags -> sdocWithDynFlags $ \dflags ->
getPprStyle $ \style -> getPprStyle $ \style ->
print_equality' args style dflags print_equality' args style dflags
print_equality' (ki1, ki2, ty1, ty2) 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) = ppr_infix_eq (ppr tc)
| hetero_eq_tc | -- Homogeneous use of heterogeneous equality (ty1 ~~ ty2)
, print_kinds || not homogeneous -- or unlifted equality (ty1 ~# ty2)
= ppr_infix_eq (text "~~") 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 | otherwise
= if tc_name `hasKey` eqReprPrimTyConKey = ppr_infix_eq (ppr tc)
then pprIfacePrefixApp ctxt_prec (text "Coercible")
[pp appPrec ty1, pp appPrec ty2]
else pprIfaceInfixApp ctxt_prec (char '~')
(pp opPrec ty1) (pp opPrec ty2)
where where
ppr_infix_eq eq_op ppr_infix_eq :: SDoc -> SDoc
= pprIfaceInfixApp ctxt_prec eq_op ppr_infix_eq eq_op = pprIfaceInfixApp ctxt_prec eq_op
(parens (pp topPrec ty1 <+> dcolon <+> pp opPrec ki1)) (pp_ty_ki ty1 ki1) (pp_ty_ki ty2 ki2)
(parens (pp topPrec ty2 <+> dcolon <+> pp opPrec 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_kinds = gopt Opt_PrintExplicitKinds dflags
print_eqs = gopt Opt_PrintEqualityRelations dflags || print_eqs = gopt Opt_PrintEqualityRelations dflags ||
......
...@@ -12,6 +12,8 @@ listTyCon :: TyCon ...@@ -12,6 +12,8 @@ listTyCon :: TyCon
typeNatKind, typeSymbolKind :: Type typeNatKind, typeSymbolKind :: Type
mkBoxedTupleTy :: [Type] -> Type mkBoxedTupleTy :: [Type] -> Type
coercibleTyCon, heqTyCon :: TyCon
liftedTypeKind :: Kind liftedTypeKind :: Kind
constraintKind :: Kind constraintKind :: Kind
......
...@@ -1170,8 +1170,12 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole }) ...@@ -1170,8 +1170,12 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
, tyvars_msg, type_hole_hint ] , tyvars_msg, type_hole_hint ]
pp_hole_type_with_kind pp_hole_type_with_kind
| isLiftedTypeKind hole_kind = pprType hole_ty | isLiftedTypeKind hole_kind
| otherwise = pprType hole_ty <+> dcolon <+> pprKind 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) $ tyvars_msg = ppUnless (null tyvars) $
text "Where:" <+> (vcat (map loc_msg other_tvs) text "Where:" <+> (vcat (map loc_msg other_tvs)
......
...@@ -11,11 +11,9 @@ T2431.$WRefl [InlPrag=INLINE[2]] :: forall a. a :~: a ...@@ -11,11 +11,9 @@ T2431.$WRefl [InlPrag=INLINE[2]] :: forall a. a :~: a
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False) Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)
Tmpl= \ (@ a) -> Tmpl= \ (@ a) -> T2431.Refl @ a @ a @~ (<a>_N :: a GHC.Prim.~# a)}]
T2431.Refl @ a @ a @~ (<a>_N :: (a :: *) GHC.Prim.~# (a :: *))}]
T2431.$WRefl T2431.$WRefl
= \ (@ a) -> = \ (@ a) -> T2431.Refl @ a @ a @~ (<a>_N :: a GHC.Prim.~# a)
T2431.Refl @ a @ a @~ (<a>_N :: (a :: *) GHC.Prim.~# (a :: *))
-- RHS size: {terms: 4, types: 8, coercions: 0, joins: 0/0} -- RHS size: {terms: 4, types: 8, coercions: 0, joins: 0/0}
absurd :: forall a. (Int :~: Bool) -> a absurd :: forall a. (Int :~: Bool) -> a
......
{-# 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 :: ???
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 :: *)
{-# 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 :: ???
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 :: *)
{-# 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 :: ???
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 :: *)
{-# 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 :: ???
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 ‘_’