Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / determinism / determ004 / determ004.hs
1 {-# LANGUAGE TypeOperators, StarIsType
2 , DataKinds
3 , PolyKinds
4 , TypeFamilies
5 , GADTs
6 , UndecidableInstances
7 , RankNTypes
8 , ScopedTypeVariables
9 #-}
10
11 {-# OPTIONS_GHC -Wall #-}
12 {-# OPTIONS_GHC -Werror #-}
13 {-# OPTIONS_GHC -O1 -fspec-constr #-}
14
15 {-
16
17 With reversed order of allocated uniques the type variables would be in
18 wrong order:
19
20 *** Core Lint errors : in result of SpecConstr ***
21 determ004.hs:88:12: warning:
22 [in body of lambda with binder m_azbFg :: a_afdP_azbON]
23 @ (a_afdP_azbON :: BOX) is out of scope
24 *** Offending Program ***
25
26 ...
27
28 Rec {
29 $s$wsFoldr1_szbtK
30 :: forall (m_azbFg :: a_afdP_azbON)
31 (x_azbOM :: TyFun
32 a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> *)
33 -> *)
34 (a_afdP_azbON :: BOX)
35 (ipv_szbwN :: a_afdP_azbON)
36 (ipv_szbwO :: [a_afdP_azbON]).
37 R:Sing[]z (ipv_szbwN : ipv_szbwO)
38 ~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO)
39 -> Sing ipv_szbwO
40 -> Sing ipv_szbwN
41 -> (forall (t_azbNM :: a_afdP_azbON).
42 Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM))
43 -> Sing
44 (Apply
45 (Apply Foldr1Sym0 x_azbOM)
46 (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
47 [LclId,
48 Arity=4,
49 Str=<L,U><L,U><L,U><C(S(C(S))),C(U(1*C1(U)))>]
50 $s$wsFoldr1_szbtK =
51 \ (@ (m_azbFg :: a_afdP_azbON))
52 (@ (x_azbOM :: TyFun
53 a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> *)
54 -> *))
55 (@ (a_afdP_azbON :: BOX))
56 (@ (ipv_szbwN :: a_afdP_azbON))
57 (@ (ipv_szbwO :: [a_afdP_azbON]))
58 (sg_szbtL
59 :: R:Sing[]z (ipv_szbwN : ipv_szbwO)
60 ~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO))
61 (sc_szbtM :: Sing ipv_szbwO)
62 (sc_szbtN :: Sing ipv_szbwN)
63 (sc_szbtP
64 :: forall (t_azbNM :: a_afdP_azbON).
65 Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM)) ->
66 case (SCons
67 @ a_afdP_azbON
68 @ (ipv_szbwN : ipv_szbwO)
69 @ ipv_szbwO
70 @ ipv_szbwN
71 @~ (<ipv_szbwN : ipv_szbwO>_N
72 :: (ipv_szbwN : ipv_szbwO) ~# (ipv_szbwN : ipv_szbwO))
73 sc_szbtN
74 sc_szbtM)
75 `cast` (sg_szbtL
76 ; TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <Let1627448493XsSym4
77 x_azbOM m_azbFg ipv_szbwN ipv_szbwO>_N
78 :: R:Sing[]z (ipv_szbwN : ipv_szbwO)
79 ~R# R:Sing[]z
80 (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
81 of wild_XD {
82 SNil dt_dzbxX ->
83 (lvl_szbwi @ a_afdP_azbON)
84 `cast` ((Sing
85 (Sym (TFCo:R:Foldr1[2] <a_afdP_azbON>_N <x_azbOM>_N)
86 ; Sym
87 (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
88 <a_afdP_azbON>_N <'[]>_N <x_azbOM>_N)
89 ; (Apply
90 (Sym
91 (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
92 (Sym dt_dzbxX))_N))_R
93 :: Sing (Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list")
94 ~R# Sing
95 (Apply
96 (Apply Foldr1Sym0 x_azbOM)
97 (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
98 SCons @ n_azbFh @ m_XzbGe dt_dzbxK _sX_azbOH
99 ds_dzbyu [Dmd=<S,1*U>] ->
100 case ds_dzbyu
101 `cast` (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <n_azbFh>_N
102 :: Sing n_azbFh ~R# R:Sing[]z n_azbFh)
103 of wild_Xo {
104 SNil dt_dzbxk ->
105 (lvl_szbw1 @ a_afdP_azbON @ m_XzbGe)
106 `cast` ((Sing
107 (Sym (TFCo:R:Foldr1[0] <a_afdP_azbON>_N <m_XzbGe>_N <x_azbOM>_N)
108 ; Sym
109 (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
110 <a_afdP_azbON>_N <'[m_XzbGe]>_N <x_azbOM>_N)
111 ; (Apply
112 (Sym
113 (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
114 ((<m_XzbGe>_N ': Sym dt_dzbxk)_N ; Sym dt_dzbxK))_N))_R
115 :: Sing m_XzbGe
116 ~R# Sing
117 (Apply
118 (Apply Foldr1Sym0 x_azbOM)
119 (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
120 SCons @ ipv_XzbxR @ ipv_XzbyV ipv_szbwM ipv_szbwL ipv_szbwK ->
121 case (sc_szbtP @ m_XzbGe _sX_azbOH)
122 `cast` (TFCo:R:Sing(->)f[0]
123 <a_afdP_azbON>_N <a_afdP_azbON>_N <Apply x_azbOM m_XzbGe>_N
124 :: Sing (Apply x_azbOM m_XzbGe)
125 ~R# R:Sing(->)f (Apply x_azbOM m_XzbGe))
126 of wild_X3X { SLambda ds_XzbBr [Dmd=<C(S),1*C1(U)>] ->
127 (ds_XzbBr
128 @ (Foldr1 x_azbOM (ipv_XzbyV : ipv_XzbxR))
129 (($wsFoldr1_szbuc
130 @ a_afdP_azbON
131 @ x_azbOM
132 @ (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR)
133 sc_szbtP
134 ((SCons
135 @ a_afdP_azbON
136 @ (ipv_XzbyV : ipv_XzbxR)
137 @ ipv_XzbxR
138 @ ipv_XzbyV
139 @~ (<ipv_XzbyV : ipv_XzbxR>_N
140 :: (ipv_XzbyV : ipv_XzbxR) ~# (ipv_XzbyV : ipv_XzbxR))
141 ipv_szbwL
142 ipv_szbwK)
143 `cast` (Sym (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N) (Sym
144 (TFCo:R:Apply[][]:$$i[0]
145 <a_afdP_azbON>_N
146 <ipv_XzbxR>_N
147 <ipv_XzbyV>_N)
148 ; (Apply
149 (Sym
150 (TFCo:R:Applyk(->):$l[0]
151 <a_afdP_azbON>_N
152 <ipv_XzbyV>_N))
153 <ipv_XzbxR>_N)_N)
154 :: R:Sing[]z (ipv_XzbyV : ipv_XzbxR)
155 ~R# Sing (Apply (Apply (:$) ipv_XzbyV) ipv_XzbxR))))
156 `cast` ((Sing
157 ((Apply
158 (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N)
159 <Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR>_N)_N
160 ; TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
161 <a_afdP_azbON>_N
162 ((Apply
163 (TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N)
164 <ipv_XzbxR>_N)_N
165 ; TFCo:R:Apply[][]:$$i[0]
166 <a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
167 <x_azbOM>_N))_R
168 :: Sing
169 (Apply
170 (Apply Foldr1Sym0 x_azbOM)
171 (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR))
172 ~R# Sing (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))))
173 `cast` ((Sing
174 ((Apply
175 <Apply x_azbOM m_XzbGe>_N
176 (Sym
177 (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
178 <a_afdP_azbON>_N <ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
179 ; (Apply
180 (Sym
181 (TFCo:R:Apply(->)(->)Foldr1Sym0l[0]
182 <a_afdP_azbON>_N <x_azbOM>_N))
183 (Sym
184 (TFCo:R:Apply[][]:$$i[0]
185 <a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
186 ; (Apply
187 (Sym
188 (TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N))
189 <ipv_XzbxR>_N)_N))_N))_N
190 ; Sym
191 (TFCo:R:Foldr1[1]
192 <a_afdP_azbON>_N
193 <ipv_XzbxR>_N
194 <ipv_XzbyV>_N
195 <m_XzbGe>_N
196 <x_azbOM>_N)
197 ; Sym
198 (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
199 <a_afdP_azbON>_N <m_XzbGe : ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
200 ; (Apply
201 (Sym
202 (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
203 ((<m_XzbGe>_N ': Sym ipv_szbwM)_N ; Sym dt_dzbxK))_N))_R
204 :: Sing
205 (Apply
206 (Apply x_azbOM m_XzbGe)
207 (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))
208 ~R# Sing
209 (Apply
210 (Apply Foldr1Sym0 x_azbOM)
211 (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)))
212 }
213 }
214 }
215 ...
216 -}
217
218 module List (sFoldr1) where
219
220 data Proxy t
221
222 data family Sing (a :: k)
223
224 data TyFun (a :: *) (b :: *)
225
226 type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
227
228 data instance Sing (f :: TyFun k1 k2 -> *) =
229 SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
230
231 type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
232
233 type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
234 singFun2 :: Proxy f -> SingFunction2 f -> Sing f
235 singFun2 _ f = SLambda (\x -> SLambda (f x))
236
237 data (:$$) (j :: a) (i :: TyFun [a] [a])
238 type instance Apply ((:$$) j) i = (:) j i
239
240 data (:$) (l :: TyFun a (TyFun [a] [a] -> *))
241 type instance Apply (:$) l = (:$$) l
242 data instance Sing (z :: [a])
243 = z ~ '[] =>
244 SNil
245 | forall (m :: a)
246 (n :: [a]). z ~ (:) m n =>
247 SCons (Sing m) (Sing n)
248
249 data ErrorSym0 (t1 :: TyFun k1 k2)
250
251 type Let1627448493XsSym4 t_afee t_afef t_afeg t_afeh = Let1627448493Xs t_afee t_afef t_afeg t_afeh
252
253 type Let1627448493Xs f_afe9
254 x_afea
255 wild_1627448474_afeb
256 wild_1627448476_afec =
257 Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec
258 type Foldr1Sym2 (t_afdY :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
259 -> *)
260 (t_afdZ :: [a_afdP]) =
261 Foldr1 t_afdY t_afdZ
262 data Foldr1Sym1 (l_afe3 :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
263 -> *)
264 (l_afe2 :: TyFun [a_afdP] a_afdP)
265 type instance Apply (Foldr1Sym1 l_afe3) l_afe2 = Foldr1Sym2 l_afe3 l_afe2
266
267 data Foldr1Sym0 (l_afe0 :: TyFun (TyFun a_afdP (TyFun a_afdP a_afdP
268 -> *)
269 -> *) (TyFun [a_afdP] a_afdP -> *))
270 type instance Apply Foldr1Sym0 l = Foldr1Sym1 l
271
272 type family Foldr1 (a_afe5 :: TyFun a_afdP (TyFun a_afdP a_afdP
273 -> *)
274 -> *)
275 (a_afe6 :: [a_afdP]) :: a_afdP where
276 Foldr1 z_afe7 '[x_afe8] = x_afe8
277 Foldr1 f_afe9 ((:) x_afea ((:) wild_1627448474_afeb wild_1627448476_afec)) = Apply (Apply f_afe9 x_afea) (Apply (Apply Foldr1Sym0 f_afe9) (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec))
278 Foldr1 z_afew '[] = Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list"
279
280 sFoldr1 ::
281 forall (x :: TyFun a_afdP (TyFun a_afdP a_afdP -> *) -> *)
282 (y :: [a_afdP]).
283 Sing x
284 -> Sing y -> Sing (Apply (Apply Foldr1Sym0 x) y)
285 sFoldr1 _ (SCons _sX SNil) = undefined
286 sFoldr1 sF (SCons sX (SCons sWild_1627448474 sWild_1627448476))
287 = let
288 lambda_afeC ::
289 forall f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec.
290 Sing f_afe9
291 -> Sing x_afea
292 -> Sing wild_1627448474_afeb
293 -> Sing wild_1627448476_afec
294 -> Sing (Apply (Apply Foldr1Sym0 f_afe9) (Apply (Apply (:$) x_afea) (Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec)))
295 lambda_afeC f_afeD x_afeE wild_1627448474_afeF wild_1627448476_afeG
296 = let
297 sXs ::
298 Sing (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec)
299 sXs
300 = applySing
301 (applySing
302 (singFun2 (undefined :: Proxy (:$)) SCons) wild_1627448474_afeF)
303 wild_1627448476_afeG
304 in
305 applySing
306 (applySing f_afeD x_afeE)
307 (applySing
308 (applySing (singFun2 (undefined :: Proxy Foldr1Sym0) sFoldr1) f_afeD)
309 sXs)
310 in lambda_afeC sF sX sWild_1627448474 sWild_1627448476
311 sFoldr1 _ SNil = undefined