1 {-# LANGUAGE TypeFamilyDependencies, DataKinds, UndecidableInstances, PolyKinds,
2 MultiParamTypeClasses, FlexibleInstances #-}
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
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
15 type instance G

Bool Int Char = Int
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
23 type family Id a

= result | result

-> a

24 type instance Id a

= a

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

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
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

)
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
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

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

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

58 instance PolyKindVarsC

'[] where
59 type PolyKindVarsF

'[] = '[]
61 type family PolyKindVars

(a

:: k0

) = (r

:: k1

) | r

-> a

62 type instance PolyKindVars

'[] = '[]
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
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
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

)
77 type family GF1 a

= r | r

-> a

78 type instance GF1

Int = Bool
80 type family GF2 a

= r | r

-> a

81 type instance GF2

Int = Bool
84 type instance HF1

Bool = Bool
86 type family W1 a

= r | r

-> a

87 type instance W1

[a

] = a

89 type family W2 a

= r | r

-> a

90 type instance W2

[a

] = W2 a

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

])
97 type family G1 a

= r | r

-> a

98 type instance G1

[a

] = [a

]
99 type instance G1

(Maybe b

) = [(b

, b

)]
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

)
105 type family G4 a b

= r | r

-> a b

106 type instance G4 a b

= [a

]
108 type family G5 a

= r | r

-> a

109 type instance G5

[a

] = [GF1 a

] -- GF1 injective
110 type instance G5

Int = [Bool]
112 type family G6 a

= r | r

-> a

113 type instance G6

[a

] = [HF1 a

] -- HF1 not injective
114 type instance G6

Bool = Int
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

]
121 type FC a

(b

:: *) = r | r

-> b

122 type instance FC a b

= b

124 instance C

Int Char where
125 type FC

Int Char = Bool
127 -- this should fail because the default instance conflicts with one of the
129 instance C

Int Bool {- where
130 type FC Int Bool = Bool-}
132 -- and this should fail because it violates "bare variable in the RHS"