Take account of injectivity when doing fundeps
[ghc.git] / testsuite / tests / typecheck / should_fail / T6018fail.hs
1 {-# LANGUAGE TypeFamilyDependencies, DataKinds, UndecidableInstances, PolyKinds,
2 MultiParamTypeClasses, FlexibleInstances #-}
3
4 module T6018fail where
5
6 import T6018Afail -- defines G, identical to F
7 import T6018Cfail -- imports H from T6018Bfail, defines some equations for H
8 import T6018Dfail -- imports H from T6018Bfail, defines conflicting eqns
9
10 type family F a b c = (result :: *) | result -> a b c
11 type instance F Int Char Bool = Bool
12 type instance F Char Bool Int = Int
13 type instance F Bool Int Char = Int
14
15 type instance G Bool Int Char = Int
16
17 type family I a b c = r | r -> a b
18 type instance I Int Char Bool = Bool
19 type instance I Int Int Int = Bool
20 type instance I Bool Int Int = Int
21
22 -- Id is injective...
23 type family Id a = result | result -> a
24 type instance Id a = a
25
26 -- ...but despite that we disallow a call to Id
27 type family IdProxy a = r | r -> a
28 type instance IdProxy a = Id a
29
30 data N = Z | S N
31
32 -- P is not injective, although the user declares otherwise. This
33 -- should be rejected on the grounds of calling a type family in the
34 -- RHS.
35 type family P (a :: N) (b :: N) = (r :: N) | r -> a b
36 type instance P Z m = m
37 type instance P (S n) m = S (P n m)
38
39 -- this is not injective - not all injective type variables mentioned
40 -- on LHS are mentioned on RHS
41 type family J a b c = r | r -> a b
42 type instance J Int b c = Char
43
44 -- same as above, but tyvar is now nested inside a tycon
45 type family K (a :: N) (b :: N) = (r :: N) | r -> a b
46 type instance K (S n) m = S m
47
48 -- Make sure we look through type synonyms to catch errors
49 type MaybeSyn a = Id a
50 type family L a = r | r -> a
51 type instance L a = MaybeSyn a
52
53 -- These should fail because given the RHS kind
54 -- there is no way to determine LHS kind
55 class PolyKindVarsC a where
56 type PolyKindVarsF a = (r :: k) | r -> a
57
58 instance PolyKindVarsC '[] where
59 type PolyKindVarsF '[] = '[]
60
61 type family PolyKindVars (a :: k0) = (r :: k1) | r -> a
62 type instance PolyKindVars '[] = '[]
63
64 -- This should fail because there is no way to determine k from the RHS
65 type family Fc (a :: k) (b :: k) = r | r -> k
66 type instance Fc a b = Int
67
68 -- This should fail because there is no way to determine a, b and k from the RHS
69 type family Gc (a :: k) (b :: k) = r | r -> a b
70 type instance Gc a b = Int
71
72 -- fails because injectivity is not compositional in this case
73 type family F1 a = r | r -> a
74 type instance F1 [a] = Maybe (GF1 a)
75 type instance F1 (Maybe a) = Maybe (GF2 a)
76
77 type family GF1 a = r | r -> a
78 type instance GF1 Int = Bool
79
80 type family GF2 a = r | r -> a
81 type instance GF2 Int = Bool
82
83 type family HF1 a
84 type instance HF1 Bool = Bool
85
86 type family W1 a = r | r -> a
87 type instance W1 [a] = a
88
89 type family W2 a = r | r -> a
90 type instance W2 [a] = W2 a
91
92 -- not injective because of infinite types
93 type family Z1 a = r | r -> a
94 type instance Z1 [a] = (a, a)
95 type instance Z1 (Maybe b) = (b, [b])
96
97 type family G1 a = r | r -> a
98 type instance G1 [a] = [a]
99 type instance G1 (Maybe b) = [(b, b)]
100
101 type family G3 a b = r | r -> b
102 type instance G3 a Int = (a, Int)
103 type instance G3 a Bool = (Bool, a)
104
105 type family G4 a b = r | r -> a b
106 type instance G4 a b = [a]
107
108 type family G5 a = r | r -> a
109 type instance G5 [a] = [GF1 a] -- GF1 injective
110 type instance G5 Int = [Bool]
111
112 type family G6 a = r | r -> a
113 type instance G6 [a] = [HF1 a] -- HF1 not injective
114 type instance G6 Bool = Int
115
116 type family G7a a b (c :: k) = r | r -> a b
117 type family G7 a b (c :: k) = r | r -> a b c
118 type instance G7 a b c = [G7a a b c]
119
120 class C a b where
121 type FC a (b :: *) = r | r -> b
122 type instance FC a b = b
123
124 instance C Int Char where
125 type FC Int Char = Bool
126
127 -- this should fail because the default instance conflicts with one of the
128 -- earlier instances
129 instance C Int Bool {- where
130 type FC Int Bool = Bool-}
131
132 -- and this should fail because it violates "bare variable in the RHS"
133 -- restriction
134 instance C Char a