summaryrefslogtreecommitdiff
path: root/tests/examples/pre-ghc86/T10689a.hs
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/pre-ghc86/T10689a.hs')
-rw-r--r--tests/examples/pre-ghc86/T10689a.hs114
1 files changed, 114 insertions, 0 deletions
diff --git a/tests/examples/pre-ghc86/T10689a.hs b/tests/examples/pre-ghc86/T10689a.hs
new file mode 100644
index 0000000..5b21b42
--- /dev/null
+++ b/tests/examples/pre-ghc86/T10689a.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE TypeOperators
+ , DataKinds
+ , PolyKinds
+ , TypeFamilies
+ , GADTs
+ , UndecidableInstances
+ , RankNTypes
+ , ScopedTypeVariables
+ #-}
+
+{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS_GHC -Werror #-}
+{-# OPTIONS_GHC -O1 -fspec-constr #-}
+
+{-
+ghc-stage2: panic! (the 'impossible' happened)
+ (GHC version 7.11.20150723 for x86_64-unknown-linux):
+ Template variable unbound in rewrite rule
+-}
+
+module List (sFoldr1) where
+
+data Proxy t
+
+data family Sing (a :: k)
+
+data TyFun (a :: *) (b :: *)
+
+type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
+
+data instance Sing (f :: TyFun k1 k2 -> *) =
+ SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+
+type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
+
+type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
+singFun2 :: Proxy f -> SingFunction2 f -> Sing f
+singFun2 _ f = SLambda (\x -> SLambda (f x))
+
+data (:$$) (j :: a) (i :: TyFun [a] [a])
+type instance Apply ((:$$) j) i = (:) j i
+
+data (:$) (l :: TyFun a (TyFun [a] [a] -> *))
+type instance Apply (:$) l = (:$$) l
+data instance Sing (z :: [a])
+ = z ~ '[] =>
+ SNil
+ | forall (m :: a)
+ (n :: [a]). z ~ (:) m n =>
+ SCons (Sing m) (Sing n)
+
+data ErrorSym0 (t1 :: TyFun k1 k2)
+
+type Let1627448493XsSym4 t_afee t_afef t_afeg t_afeh = Let1627448493Xs t_afee t_afef t_afeg t_afeh
+
+type Let1627448493Xs f_afe9
+ x_afea
+ wild_1627448474_afeb
+ wild_1627448476_afec =
+ Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec
+type Foldr1Sym2 (t_afdY :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
+ -> *)
+ (t_afdZ :: [a_afdP]) =
+ Foldr1 t_afdY t_afdZ
+data Foldr1Sym1 (l_afe3 :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
+ -> *)
+ (l_afe2 :: TyFun [a_afdP] a_afdP)
+type instance Apply (Foldr1Sym1 l_afe3) l_afe2 = Foldr1Sym2 l_afe3 l_afe2
+
+data Foldr1Sym0 (l_afe0 :: TyFun (TyFun a_afdP (TyFun a_afdP a_afdP
+ -> *)
+ -> *) (TyFun [a_afdP] a_afdP -> *))
+type instance Apply Foldr1Sym0 l = Foldr1Sym1 l
+
+type family Foldr1 (a_afe5 :: TyFun a_afdP (TyFun a_afdP a_afdP
+ -> *)
+ -> *)
+ (a_afe6 :: [a_afdP]) :: a_afdP where
+ Foldr1 z_afe7 '[x_afe8] = x_afe8
+ 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))
+ Foldr1 z_afew '[] = Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list"
+
+sFoldr1 ::
+ forall (x :: TyFun a_afdP (TyFun a_afdP a_afdP -> *) -> *)
+ (y :: [a_afdP]).
+ Sing x
+ -> Sing y -> Sing (Apply (Apply Foldr1Sym0 x) y)
+sFoldr1 _ (SCons _sX SNil) = undefined
+sFoldr1 sF (SCons sX (SCons sWild_1627448474 sWild_1627448476))
+ = let
+ lambda_afeC ::
+ forall f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec.
+ Sing f_afe9
+ -> Sing x_afea
+ -> Sing wild_1627448474_afeb
+ -> Sing wild_1627448476_afec
+ -> Sing (Apply (Apply Foldr1Sym0 f_afe9) (Apply (Apply (:$) x_afea) (Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec)))
+ lambda_afeC f_afeD x_afeE wild_1627448474_afeF wild_1627448476_afeG
+ = let
+ sXs ::
+ Sing (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec)
+ sXs
+ = applySing
+ (applySing
+ (singFun2 (undefined :: Proxy (:$)) SCons) wild_1627448474_afeF)
+ wild_1627448476_afeG
+ in
+ applySing
+ (applySing f_afeD x_afeE)
+ (applySing
+ (applySing (singFun2 (undefined :: Proxy Foldr1Sym0) sFoldr1) f_afeD)
+ sXs)
+ in lambda_afeC sF sX sWild_1627448474 sWild_1627448476
+sFoldr1 _ SNil = undefined