1{-# LANGUAGE DataKinds                 #-}
2{-# LANGUAGE MultiParamTypeClasses     #-}
3{-# LANGUAGE PolyKinds                 #-}
4{-# LANGUAGE TypeFamilyDependencies     #-}
5{-# LANGUAGE TypeFamilies     #-}
6{-# LANGUAGE UndecidableInstances      #-}
7{-# LANGUAGE ScopedTypeVariables       #-}
8{-# LANGUAGE NoMonomorphismRestriction #-}
9
10module T6018 where
11
12import T6018a -- defines G, identical to F
13
14type family F a b c = (result :: k) | result -> a b c
15type instance F Int  Char Bool = Bool
16type instance F Char Bool Int  = Int
17type instance F Bool Int  Char = Char
18
19
20type instance G Bool Int  Char = Char
21
22type family I (a :: k) b (c :: k) = r | r -> a b
23type instance I Int  Char Bool = Bool
24type instance I Int  Char Int  = Bool
25type instance I Bool Int  Int  = Int
26
27-- this is injective - a type variable introduced in the LHS is not mentioned on
28-- RHS but we don't claim injectivity in that argument.
29type family J a (b :: k) = r | r -> a
30type instance J Int b = Char
31
32type MaybeSyn a = Maybe a
33newtype MaybeNew a = MaybeNew (Maybe a)
34
35-- make sure we look through type synonyms...
36type family K a = r | r -> a
37type instance K a = MaybeSyn a
38
39-- .. but not newtypes
40type family M a = r | r -> a
41type instance M (Maybe a)    = MaybeSyn a
42type instance M (MaybeNew a) = MaybeNew a
43
44-- Closed type families
45
46-- these are simple conversions from open type families. They should behave the
47-- same
48type family FClosed a b c = result | result -> a b c where
49    FClosed Int  Char Bool = Bool
50    FClosed Char Bool Int  = Int
51    FClosed Bool Int  Char = Char
52
53type family IClosed (a :: *) (b :: *) (c :: *) = r | r -> a b where
54    IClosed Int  Char Bool = Bool
55    IClosed Int  Char Int  = Bool
56    IClosed Bool Int  Int  = Int
57
58type family JClosed a (b :: k) = r | r -> a where
59    JClosed Int b = Char
60
61type family KClosed a = r | r -> a where
62    KClosed a = MaybeSyn a
63
64-- Here the last equation might return both Int and Char but we have to
65-- recognize that it is not possible due to equation overlap
66type family Bak a = r | r -> a where
67     Bak Int  = Char
68     Bak Char = Int
69     Bak a    = a
70
71-- This is similar, except that the last equation contains concrete type.  Since
72-- it is overlapped it should be dropped with a warning
73type family Foo a = r | r -> a where
74    Foo Int  = Bool
75    Foo Bool = Int
76    Foo Bool = Bool
77
78-- this one was tricky in the early implementation of injectivity.  Now it is
79-- identical to the above but we still keep it as a regression test.
80type family Bar a = r | r -> a where
81    Bar Int  = Bool
82    Bar Bool = Int
83    Bar Bool = Char
84
85-- Now let's use declared type families. All the below definitions should work
86
87-- No ambiguity for any of the arguments - all are injective
88f :: F a b c -> F a b c
89f x = x
90
91-- From 1st instance of F: a ~ Int, b ~ Char, c ~ Bool
92fapp :: Bool
93fapp = f True
94
95-- now the closed variant of F
96fc :: FClosed a b c -> FClosed a b c
97fc x = x
98
99fcapp :: Bool
100fcapp = fc True
101
102-- The last argument is not injective so it must be instantiated
103i :: I a b Int -> I a b Int
104i x = x
105
106-- From 1st instance of I: a ~ Int, b ~ Char
107iapp :: Bool
108iapp = i True
109
110-- again, closed variant of I
111ic :: IClosed a b Int -> IClosed a b Int
112ic x = x
113
114icapp :: Bool
115icapp = ic True
116
117-- Now we have to test weird closed type families:
118bak :: Bak a -> Bak a
119bak x = x
120
121bakapp1 :: Char
122bakapp1 = bak 'c'
123
124bakapp2 :: Double
125bakapp2 = bak 1.0
126
127bakapp3 :: ()
128bakapp3 = bak ()
129
130foo :: Foo a -> Foo a
131foo x = x
132
133fooapp1 :: Bool
134fooapp1 = foo True
135
136bar :: Bar a -> Bar a
137bar x = x
138
139barapp1 :: Bool
140barapp1 = bar True
141
142barapp2 :: Int
143barapp2 = bar 1
144
145-- Declarations below test more liberal RHSs of injectivity annotations:
146-- permiting variables to appear in different order than the one in which they
147-- were declared.
148type family H a b = r | r -> b a
149type family Hc a b = r | r -> b a where
150  Hc a b = a b
151class Hcl a b where
152  type Ht a b = r | r -> b a
153
154-- repeated tyvars in the RHS of injectivity annotation: no warnings or errors
155-- (consistent with behaviour for functional dependencies)
156type family Jx a b = r | r -> a a
157type family Jcx a b = r | r -> a a where
158  Jcx a b = a b
159class Jcl a b where
160  type Jt a b = r | r -> a a
161
162type family Kx a b = r | r -> a b b
163type family Kcx a b = r | r -> a b b where
164  Kcx a b = a b
165class Kcl a b where
166  type Kt a b = r | r -> a b b
167
168-- Declaring kind injectivity. Here we only claim that knowing the RHS
169-- determines the LHS kind but not the type.
170type family L (a :: k1) = (r :: k2) | r -> k1 where
171    L 'True  = Int
172    L 'False = Int
173    L Maybe  = 3
174    L IO     = 3
175
176data KProxy (a :: *) = KProxy
177type family KP (kproxy :: KProxy k) = r | r -> k
178type instance KP ('KProxy :: KProxy Bool) = Int
179type instance KP ('KProxy :: KProxy *)    = Char
180
181kproxy_id :: KP ('KProxy :: KProxy k) -> KP ('KProxy :: KProxy k)
182kproxy_id x = x
183
184kproxy_id_use = kproxy_id 'a'
185
186-- Now test some awkward cases from The Injectivity Paper.  All should be
187-- accepted.
188type family Gx a
189type family Hx a
190type family Gi a = r | r -> a
191type instance Gi Int = Char
192type family Hi a = r | r -> a
193
194type family F2 a = r | r -> a
195type instance F2 [a]       = [Gi a]
196type instance F2 (Maybe a) = Hi a -> Int
197
198type family F4 a = r | r -> a
199type instance F4 [a]       = (Gx a, a,   a,    a)
200type instance F4 (Maybe a) = (Hx a, a, Int, Bool)
201
202type family G2 a b = r | r -> a b
203type instance G2 a    Bool = (a, a)
204type instance G2 Bool b    = (b, Bool)
205
206type family G6 a = r | r -> a
207type instance G6 [a]  = [Gi a]
208type instance G6 Bool = Int
209
210g6_id :: G6 a -> G6 a
211g6_id x = x
212
213g6_use :: [Char]
214g6_use = g6_id "foo"
215
216-- A sole exception to "bare variables in the RHS" rule
217type family Id (a :: k) = (result :: k) | result -> a
218type instance Id a = a
219
220-- This makes sure that over-saturated type family applications at the top-level
221-- are accepted.
222type family IdProxy (a :: k) b = r | r -> a
223type instance IdProxy a b = (Id a) b
224
225-- make sure we look through type synonyms properly
226type IdSyn a = Id a
227type family IdProxySyn (a :: k) b = r | r -> a
228type instance IdProxySyn a b = (IdSyn a) b
229
230-- this has bare variable in the RHS but all LHS varaiables are also bare so it
231-- should be accepted
232type family Fa (a :: k) (b :: k) = (r :: k2) | r -> k
233type instance Fa a b = a
234
235-- Taken from #9587. This exposed a bug in the solver.
236type family Arr (repr :: * -> *) (a :: *) (b :: *) = (r :: *) | r -> repr a b
237
238class ESymantics repr where
239    int :: Int  -> repr Int
240    add :: repr Int  -> repr Int -> repr Int
241
242    lam :: (repr a -> repr b) -> repr (Arr repr a b)
243    app :: repr (Arr repr a b) -> repr a -> repr b
244
245te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x))))
246      in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0)
247
248-- This used to fail during development
249class Manifold' a where
250    type Base  a = r | r -> a
251    project :: a -> Base a
252    unproject :: Base a -> a
253
254id' :: forall a. ( Manifold' a ) => Base a -> Base a
255id' = project . unproject
256