Deal with phantom type variables in rules
[ghc.git] / testsuite / tests / simplCore / should_compile / T10689a.hs
1 {-# LANGUAGE TypeOperators
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 ghc-stage2: panic! (the 'impossible' happened)
17 (GHC version 7.11.20150723 for x86_64-unknown-linux):
18 Template variable unbound in rewrite rule
19 -}
20
21 module List (sFoldr1) where
22
23 data Proxy t
24
25 data family Sing (a :: k)
26
27 data TyFun (a :: *) (b :: *)
28
29 type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
30
31 data instance Sing (f :: TyFun k1 k2 -> *) =
32 SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
33
34 type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
35
36 type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
37 singFun2 :: Proxy f -> SingFunction2 f -> Sing f
38 singFun2 _ f = SLambda (\x -> SLambda (f x))
39
40 data (:$$) (j :: a) (i :: TyFun [a] [a])
41 type instance Apply ((:$$) j) i = (:) j i
42
43 data (:$) (l :: TyFun a (TyFun [a] [a] -> *))
44 type instance Apply (:$) l = (:$$) l
45 data instance Sing (z :: [a])
46 = z ~ '[] =>
47 SNil
48 | forall (m :: a)
49 (n :: [a]). z ~ (:) m n =>
50 SCons (Sing m) (Sing n)
51
52 data ErrorSym0 (t1 :: TyFun k1 k2)
53
54 type Let1627448493XsSym4 t_afee t_afef t_afeg t_afeh = Let1627448493Xs t_afee t_afef t_afeg t_afeh
55
56 type Let1627448493Xs f_afe9
57 x_afea
58 wild_1627448474_afeb
59 wild_1627448476_afec =
60 Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec
61 type Foldr1Sym2 (t_afdY :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
62 -> *)
63 (t_afdZ :: [a_afdP]) =
64 Foldr1 t_afdY t_afdZ
65 data Foldr1Sym1 (l_afe3 :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
66 -> *)
67 (l_afe2 :: TyFun [a_afdP] a_afdP)
68 type instance Apply (Foldr1Sym1 l_afe3) l_afe2 = Foldr1Sym2 l_afe3 l_afe2
69
70 data Foldr1Sym0 (l_afe0 :: TyFun (TyFun a_afdP (TyFun a_afdP a_afdP
71 -> *)
72 -> *) (TyFun [a_afdP] a_afdP -> *))
73 type instance Apply Foldr1Sym0 l = Foldr1Sym1 l
74
75 type family Foldr1 (a_afe5 :: TyFun a_afdP (TyFun a_afdP a_afdP
76 -> *)
77 -> *)
78 (a_afe6 :: [a_afdP]) :: a_afdP where
79 Foldr1 z_afe7 '[x_afe8] = x_afe8
80 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))
81 Foldr1 z_afew '[] = Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list"
82
83 sFoldr1 ::
84 forall (x :: TyFun a_afdP (TyFun a_afdP a_afdP -> *) -> *)
85 (y :: [a_afdP]).
86 Sing x
87 -> Sing y -> Sing (Apply (Apply Foldr1Sym0 x) y)
88 sFoldr1 _ (SCons _sX SNil) = undefined
89 sFoldr1 sF (SCons sX (SCons sWild_1627448474 sWild_1627448476))
90 = let
91 lambda_afeC ::
92 forall f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec.
93 Sing f_afe9
94 -> Sing x_afea
95 -> Sing wild_1627448474_afeb
96 -> Sing wild_1627448476_afec
97 -> Sing (Apply (Apply Foldr1Sym0 f_afe9) (Apply (Apply (:$) x_afea) (Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec)))
98 lambda_afeC f_afeD x_afeE wild_1627448474_afeF wild_1627448476_afeG
99 = let
100 sXs ::
101 Sing (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec)
102 sXs
103 = applySing
104 (applySing
105 (singFun2 (undefined :: Proxy (:$)) SCons) wild_1627448474_afeF)
106 wild_1627448476_afeG
107 in
108 applySing
109 (applySing f_afeD x_afeE)
110 (applySing
111 (applySing (singFun2 (undefined :: Proxy Foldr1Sym0) sFoldr1) f_afeD)
112 sXs)
113 in lambda_afeC sF sX sWild_1627448474 sWild_1627448476
114 sFoldr1 _ SNil = undefined