blob: 8121760dc887ccf337361f4931d738d7849390f8 (
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
|
{-# LANGUAGE TypeFamilyDependencies, DataKinds, PolyKinds,
UndecidableInstances #-}
module T6018failclosed where
-- Id is injective...
type family IdClosed a = result | result -> a where
IdClosed a = a
-- ...but despite that we disallow a call to Id
type family IdProxyClosed (a :: *) = r | r -> a where
IdProxyClosed a = IdClosed a
data N = Z | S N
-- PClosed 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 PClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
PClosed Z m = m
PClosed (S n) m = S (PClosed n m)
-- this is not injective - not all injective type variables mentioned
-- on LHS are mentioned on RHS
type family JClosed a b c = r | r -> a b where
JClosed Int b c = Char
-- this is not injective - not all injective type variables mentioned
-- on LHS are mentioned on RHS (tyvar is now nested inside a tycon)
type family KClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
KClosed (S n) m = S m
-- hiding a type family application behind a type synonym should be rejected
type MaybeSynClosed a = IdClosed a
type family LClosed a = r | r -> a where
LClosed a = MaybeSynClosed a
type family FClosed a b c = (result :: *) | result -> a b c where
FClosed Int Char Bool = Bool
FClosed Char Bool Int = Int
FClosed Bool Int Char = Int
type family IClosed a b c = r | r -> a b where
IClosed Int Char Bool = Bool
IClosed Int Int Int = Bool
IClosed Bool Int Int = Int
type family E2 (a :: Bool) = r | r -> a where
E2 False = True
E2 True = False
E2 a = False
-- This exposed a subtle bug in the implementation during development. After
-- unifying the RHS of (1) and (2) the LHS substitution was done only in (2)
-- which made it look like an overlapped equation. This is not the case and this
-- definition should be rejected. The first two equations are here to make sure
-- that the internal implementation does list indexing corrcectly (this is a bit
-- tricky because the list is kept in reverse order).
type family F a b = r | r -> a b where
F Float IO = Float
F Bool IO = Bool
F a IO = IO a -- (1)
F Char b = b Int -- (2)
-- 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 -> k where
Gc a b = Int
|
