Lower precedence for {-# UNPACK #-}
[ghc.git] / testsuite / tests / typecheck / should_fail / T6018failclosed.hs
1 {-# LANGUAGE TypeFamilyDependencies, DataKinds, PolyKinds,
2 UndecidableInstances #-}
3 module T6018failclosed where
4
5 -- Id is injective...
6 type family IdClosed a = result | result -> a where
7 IdClosed a = a
8
9 -- ...but despite that we disallow a call to Id
10 type family IdProxyClosed (a :: *) = r | r -> a where
11 IdProxyClosed a = IdClosed a
12
13 data N = Z | S N
14
15 -- PClosed is not injective, although the user declares otherwise. This
16 -- should be rejected on the grounds of calling a type family in the
17 -- RHS.
18 type family PClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
19 PClosed Z m = m
20 PClosed (S n) m = S (PClosed n m)
21
22 -- this is not injective - not all injective type variables mentioned
23 -- on LHS are mentioned on RHS
24 type family JClosed a b c = r | r -> a b where
25 JClosed Int b c = Char
26
27 -- this is not injective - not all injective type variables mentioned
28 -- on LHS are mentioned on RHS (tyvar is now nested inside a tycon)
29 type family KClosed (a :: N) (b :: N) = (r :: N) | r -> a b where
30 KClosed (S n) m = S m
31
32 -- hiding a type family application behind a type synonym should be rejected
33 type MaybeSynClosed a = IdClosed a
34 type family LClosed a = r | r -> a where
35 LClosed a = MaybeSynClosed a
36
37 type family FClosed a b c = (result :: *) | result -> a b c where
38 FClosed Int Char Bool = Bool
39 FClosed Char Bool Int = Int
40 FClosed Bool Int Char = Int
41
42 type family IClosed a b c = r | r -> a b where
43 IClosed Int Char Bool = Bool
44 IClosed Int Int Int = Bool
45 IClosed Bool Int Int = Int
46
47 type family E2 (a :: Bool) = r | r -> a where
48 E2 False = True
49 E2 True = False
50 E2 a = False
51
52 -- This exposed a subtle bug in the implementation during development. After
53 -- unifying the RHS of (1) and (2) the LHS substitution was done only in (2)
54 -- which made it look like an overlapped equation. This is not the case and this
55 -- definition should be rejected. The first two equations are here to make sure
56 -- that the internal implementation does list indexing corrcectly (this is a bit
57 -- tricky because the list is kept in reverse order).
58 type family F a b = r | r -> a b where
59 F Float IO = Float
60 F Bool IO = Bool
61 F a IO = IO a -- (1)
62 F Char b = b Int -- (2)
63
64 -- This should fail because there is no way to determine a, b and k from the RHS
65 type family Gc (a :: k) (b :: k) = r | r -> k where
66 Gc a b = Int