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