Commit 93fafe05 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Re-polish error messages around injective TFs.

The previous message was wrong, as pointed out by Jan Stolarek.
parent 27f9186d
......@@ -559,27 +559,28 @@ conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
unusedInjectiveVarsErr :: TyVarSet -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
unusedInjectiveVarsErr unused_tyvars errorBuilder tyfamEqn
= errorBuilder (injectivityErrorHerald True $$
mkUnusedInjectiveVarsErr unused_tyvars) [tyfamEqn]
= errorBuilder (injectivityErrorHerald True $$ unusedInjectiveVarsErr)
[tyfamEqn]
where
mkUnusedInjectiveVarsErr :: TyVarSet -> SDoc
mkUnusedInjectiveVarsErr unused_tyvars =
let tyVars = varSetElems $ filterVarSet isTypeVar unused_tyvars
kiVars = varSetElems $ filterVarSet isKindVar unused_tyvars
tyVarsSDoc
= if not (null tyVars)
then text "Injective type variable" <> plural tyVars <+>
pprQuotedList tyVars <+> doOrDoes tyVars <+>
text "not appear on the right-hand side."
else empty
kiVarsSDoc
= if not (null kiVars)
then text "Injective kind variable" <> plural kiVars <+>
pprQuotedList kiVars <+> isOrAre kiVars <+>
text "not inferrable from the RHS type variables."
else empty
in tyVarsSDoc $$ kiVarsSDoc $$
text "In the type family equation:"
tvs = varSetElemsKvsFirst unused_tyvars
has_types = any isTypeVar tvs
has_kinds = any isKindVar tvs
doc = sep [ what <+> text "variable" <>
plural tvs <+> pprQuotedList tvs
, text "cannot be inferred from the right-hand side." ]
what = case (has_types, has_kinds) of
(True, True) -> text "Type and kind"
(True, False) -> text "Type"
(False, True) -> text "Kind"
(False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $
ppr unused_tyvars
print_kinds_info = sdocWithDynFlags $ \ dflags ->
if has_kinds && not (gopt Opt_PrintExplicitKinds dflags)
then text "(enabling -fprint-explicit-kinds might help)"
else empty
unusedInjectiveVarsErr = doc $$ print_kinds_info $$
text "In the type family equation:"
-- | Build error message for equation that has a type family call at the top
-- level of RHS
......
......@@ -22,13 +22,13 @@
<interactive>:40:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘b’ does not appear on the right-hand side.
Type variable ‘b’ cannot be inferred from the right-hand side.
In the type family equation:
J Int b c = Char
<interactive>:44:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘n’ does not appear on the right-hand side.
Type variable ‘n’ cannot be inferred from the right-hand side.
In the type family equation:
K ('S n) m = 'S m
......@@ -39,26 +39,30 @@
<interactive>:55:41: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Kind variable ‘k’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
PolyKindVarsF '[] = '[]
<interactive>:60:15: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k1’ is not inferrable from the RHS type variables.
Kind variable ‘k1’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
PolyKindVars '[] = '[]
<interactive>:64:15: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Kind variable ‘k’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
<interactive>:68:15: error:
Type family equation violates injectivity annotation.
Injective type variables ‘a’, ‘b’ do not appear on the right-hand side.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Type and kind variables ‘k’, ‘a’, ‘b’
cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
......@@ -95,7 +99,7 @@
<interactive>:104:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘b’ does not appear on the right-hand side.
Type variable ‘b’ cannot be inferred from the right-hand side.
In the type family equation:
G4 a b = [a]
......@@ -106,6 +110,6 @@
<interactive>:111:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘a’ does not appear on the right-hand side.
Type variable ‘a’ cannot be inferred from the right-hand side.
In the type family equation:
G6 [a] = [HF1 a]
......@@ -42,13 +42,13 @@ T6018fail.hs:37:15: error:
T6018fail.hs:42:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘b’ does not appear on the right-hand side.
Type variable ‘b’ cannot be inferred from the right-hand side.
In the type family equation:
J Int b c = Char
T6018fail.hs:46:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘n’ does not appear on the right-hand side.
Type variable ‘n’ cannot be inferred from the right-hand side.
In the type family equation:
K ('S n) m = 'S m
......@@ -59,26 +59,30 @@ T6018fail.hs:51:15: error:
T6018fail.hs:59:10: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Kind variable ‘k’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
PolyKindVarsF '[] = '[]
T6018fail.hs:62:15: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k1’ is not inferrable from the RHS type variables.
Kind variable ‘k1’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
PolyKindVars '[] = '[]
T6018fail.hs:66:15: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Kind variable ‘k’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
T6018fail.hs:70:15: error:
Type family equation violates injectivity annotation.
Injective type variables ‘a’, ‘b’ do not appear on the right-hand side.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Type and kind variables ‘k’, ‘a’, ‘b’
cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
......@@ -115,7 +119,7 @@ T6018fail.hs:103:15: error:
T6018fail.hs:106:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘b’ does not appear on the right-hand side.
Type variable ‘b’ cannot be inferred from the right-hand side.
In the type family equation:
G4 a b = [a]
......@@ -126,14 +130,15 @@ T6018fail.hs:110:15: error:
T6018fail.hs:113:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘a’ does not appear on the right-hand side.
Type variable ‘a’ cannot be inferred from the right-hand side.
In the type family equation:
G6 [a] = [HF1 a]
T6018fail.hs:118:15: error:
Type family equation violates injectivity annotation.
Injective type variable ‘c’ does not appear on the right-hand side.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Type and kind variables ‘k’, ‘c’
cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) a b (c :: k). G7 a b c = [G7a a b c]
......
T6018failclosed.hs:11:5:
T6018failclosed.hs:11:5: error:
Type family equation violates injectivity annotation.
RHS of injective type family equation cannot be a type family:
IdProxyClosed a = IdClosed a
In the equations for closed type family ‘IdProxyClosed’
In the type family declaration for ‘IdProxyClosed’
T6018failclosed.hs:19:5:
T6018failclosed.hs:19:5: error:
Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'Z’
......@@ -14,71 +14,73 @@ T6018failclosed.hs:19:5:
In the equations for closed type family ‘PClosed’
In the type family declaration for ‘PClosed’
T6018failclosed.hs:19:5:
T6018failclosed.hs:19:5: error:
Type family equations violate injectivity annotation:
PClosed 'Z m = m
PClosed ('S n) m = 'S (PClosed n m)
In the equations for closed type family ‘PClosed’
In the type family declaration for ‘PClosed’
T6018failclosed.hs:25:5:
T6018failclosed.hs:25:5: error:
Type family equation violates injectivity annotation.
Injective type variable ‘b’ does not appear on the right-hand side.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Type and kind variables ‘k’, ‘b’
cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) (k1 :: BOX) (b :: k) (c :: k1).
JClosed Int b c = Char
In the equations for closed type family ‘JClosed’
In the type family declaration for ‘JClosed’
T6018failclosed.hs:30:5:
T6018failclosed.hs:30:5: error:
Type family equation violates injectivity annotation.
Injective type variable ‘n’ does not appear on the right-hand side.
Type variable ‘n’ cannot be inferred from the right-hand side.
In the type family equation:
KClosed ('S n) m = 'S m
In the equations for closed type family ‘KClosed’
In the type family declaration for ‘KClosed’
T6018failclosed.hs:35:5:
T6018failclosed.hs:35:5: error:
Type family equation violates injectivity annotation.
RHS of injective type family equation cannot be a type family:
forall (k :: BOX) (a :: k). LClosed a = MaybeSynClosed a
In the equations for closed type family ‘LClosed’
In the type family declaration for ‘LClosed’
T6018failclosed.hs:39:5:
T6018failclosed.hs:39:5: error:
Type family equations violate injectivity annotation:
FClosed Char Bool Int = Int
FClosed Bool Int Char = Int
In the equations for closed type family ‘FClosed’
In the type family declaration for ‘FClosed’
T6018failclosed.hs:43:5:
T6018failclosed.hs:43:5: error:
Type family equations violate injectivity annotation:
IClosed Int Char Bool = Bool
IClosed Int Int Int = Bool
In the equations for closed type family ‘IClosed’
In the type family declaration for ‘IClosed’
T6018failclosed.hs:50:3:
T6018failclosed.hs:50:3: error:
Type family equation violates injectivity annotation.
Injective type variable ‘a’ does not appear on the right-hand side.
Type variable ‘a’ cannot be inferred from the right-hand side.
In the type family equation:
E2 a = 'False
In the equations for closed type family ‘E2’
In the type family declaration for ‘E2’
T6018failclosed.hs:61:3:
T6018failclosed.hs:61:3: error:
Type family equations violate injectivity annotation:
F a IO = IO a
F Char b = b Int
In the equations for closed type family ‘F’
In the type family declaration for ‘F’
T6018failclosed.hs:66:5:
T6018failclosed.hs:66:5: error:
Type family equation violates injectivity annotation.
Injective kind variable ‘k’ is not inferrable from the RHS type variables.
Kind variable ‘k’ cannot be inferred from the right-hand side.
(enabling -fprint-explicit-kinds might help)
In the type family equation:
forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
In the equations for closed type family ‘Gc’
In the type family declaration for ‘Gc’
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment