blob: b8c38cbd58aa45c3ea34224f9070346483710443 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
:set -XTypeFamilyDependencies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
import Data.Kind (Type)
type family F a b c = (result :: Type) | result -> a b c
type instance F Int Char Bool = Bool
type instance F Char Bool Int = Int
type instance F Bool Int Char = Int
type family I a b c = r | r -> a b
type instance I Int Char Bool = Bool
type instance I Int Int Int = Bool
type instance I Bool Int Int = Int
-- Id is injective...
type family Id a = result | result -> a
type instance Id a = a
-- ...but despite that we disallow a call to Id
type family IdProxy a = r | r -> a
type instance IdProxy a = Id a
data N = Z | S N
-- P is not injective, although the user declares otherwise. This
-- should be rejected on the grounds of calling a type family in the
-- RHS.
type family P (a :: N) (b :: N) = (r :: N) | r -> a b
type instance P Z m = m
type instance P (S n) m = S (P n m)
-- this is not injective - not all injective type variables mentioned
-- on LHS are mentioned on RHS
type family J a b c = r | r -> a b
type instance J Int b c = Char
-- same as above, but tyvar is now nested inside a tycon
type family K (a :: N) (b :: N) = (r :: N) | r -> a b
type instance K (S n) m = S m
-- Make sure we look through type synonyms to catch errors
type MaybeSyn a = Id a
type family L a = r | r -> a
type instance L a = MaybeSyn a
-- These should fail because given the RHS kind there is no way to determine LHS
-- kind
class PolyKindVarsC a where { type PolyKindVarsF a = (r :: k) | r -> a }
instance PolyKindVarsC '[] where { type PolyKindVarsF '[] = '[] }
type family PolyKindVars (a :: k0) = (r :: k1) | r -> a
type instance PolyKindVars '[] = '[]
-- This should fail because there is no way to determine k from the RHS
type family Fc (a :: k) (b :: k) = r | r -> k
type instance Fc a b = Int
-- This should fail because there is no way to determine a, b and k from the RHS
type family Gc (a :: k) (b :: k) = r | r -> a b
type instance Gc a b = Int
type family GF1 a = r | r -> a
type instance GF1 Int = Bool
type family GF2 a = r | r -> a
type instance GF2 Int = Bool
type family HF1 a
type instance HF1 Bool = Bool
-- fails because injectivity is not compositional in this case
type family F1 a = r | r -> a
type instance F1 [a] = Maybe (GF1 a)
type instance F1 (Maybe a) = Maybe (GF2 a)
type family W1 a = r | r -> a
type instance W1 [a] = a
type family W2 a = r | r -> a
type instance W2 [a] = W2 a
-- not injective because of infinite types
type family Z1 a = r | r -> a
type instance Z1 [a] = (a, a)
type instance Z1 (Maybe b) = (b, [b])
type family G1 a = r | r -> a
type instance G1 [a] = [a]
type instance G1 (Maybe b) = [(b, b)]
type family G3 a b = r | r -> b
type instance G3 a Int = (a, Int)
type instance G3 a Bool = (Bool, a)
type family G4 a b = r | r -> a b
type instance G4 a b = [a]
type family G5 a = r | r -> a
type instance G5 [a] = [GF1 a] -- GF1 injective
type instance G5 Int = [Bool]
type family G6 a = r | r -> a
type instance G6 [a] = [HF1 a] -- HF1 not injective
type instance G6 Bool = Int
|
