summaryrefslogtreecommitdiff
path: root/tests/examples/pre-ghc86
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/pre-ghc86')
-rw-r--r--tests/examples/pre-ghc86/BadTelescope.hs9
-rw-r--r--tests/examples/pre-ghc86/BadTelescope2.hs14
-rw-r--r--tests/examples/pre-ghc86/BadTelescope3.hs9
-rw-r--r--tests/examples/pre-ghc86/BadTelescope4.hs13
-rw-r--r--tests/examples/pre-ghc86/Dep3.hs26
-rw-r--r--tests/examples/pre-ghc86/KindEqualities2.hs43
-rw-r--r--tests/examples/pre-ghc86/LiftedConstructors.hs25
-rw-r--r--tests/examples/pre-ghc86/RAE_T32a.hs35
-rw-r--r--tests/examples/pre-ghc86/RAE_T32b.hs23
-rw-r--r--tests/examples/pre-ghc86/Rae31.hs24
-rw-r--r--tests/examples/pre-ghc86/RaeBlogPost.hs63
-rw-r--r--tests/examples/pre-ghc86/RenamingStar.hs5
-rw-r--r--tests/examples/pre-ghc86/SlidingTypeSyn.hs14
-rw-r--r--tests/examples/pre-ghc86/T10134a.hs11
-rw-r--r--tests/examples/pre-ghc86/T10321.hs14
-rw-r--r--tests/examples/pre-ghc86/T10689a.hs114
-rw-r--r--tests/examples/pre-ghc86/T10934.hs38
-rw-r--r--tests/examples/pre-ghc86/T11142.hs10
-rw-r--r--tests/examples/pre-ghc86/T3927b.hs76
-rw-r--r--tests/examples/pre-ghc86/T9632.hs11
-rw-r--r--tests/examples/pre-ghc86/TensorTests.hs43
-rw-r--r--tests/examples/pre-ghc86/UnicodeSyntax.hs243
-rw-r--r--tests/examples/pre-ghc86/Vect.hs70
-rw-r--r--tests/examples/pre-ghc86/Webhook.hs176
-rw-r--r--tests/examples/pre-ghc86/determ004.hs311
-rw-r--r--tests/examples/pre-ghc86/dynamic-paper.hs341
-rw-r--r--tests/examples/pre-ghc86/mkGADTVars.hs9
-rw-r--r--tests/examples/pre-ghc86/overloadedrecflds_generics.hs50
28 files changed, 1820 insertions, 0 deletions
diff --git a/tests/examples/pre-ghc86/BadTelescope.hs b/tests/examples/pre-ghc86/BadTelescope.hs
new file mode 100644
index 0000000..acabffe
--- /dev/null
+++ b/tests/examples/pre-ghc86/BadTelescope.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType #-}
+
+module BadTelescope where
+
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+data X a k (b :: k) (c :: SameKind a b)
diff --git a/tests/examples/pre-ghc86/BadTelescope2.hs b/tests/examples/pre-ghc86/BadTelescope2.hs
new file mode 100644
index 0000000..6237df4
--- /dev/null
+++ b/tests/examples/pre-ghc86/BadTelescope2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeInType, ExplicitForAll #-}
+
+module BadTelescope2 where
+
+import Data.Kind
+import Data.Proxy
+
+data SameKind :: k -> k -> *
+
+foo :: forall a k (b :: k). SameKind a b
+foo = undefined
+
+bar :: forall a (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
+bar = undefined
diff --git a/tests/examples/pre-ghc86/BadTelescope3.hs b/tests/examples/pre-ghc86/BadTelescope3.hs
new file mode 100644
index 0000000..807479f
--- /dev/null
+++ b/tests/examples/pre-ghc86/BadTelescope3.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType, ExplicitForAll #-}
+
+module BadTelescope3 where
+
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+type S a k (b :: k) = SameKind a b
diff --git a/tests/examples/pre-ghc86/BadTelescope4.hs b/tests/examples/pre-ghc86/BadTelescope4.hs
new file mode 100644
index 0000000..566922a
--- /dev/null
+++ b/tests/examples/pre-ghc86/BadTelescope4.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE ExistentialQuantification, TypeInType #-}
+module BadTelescope4 where
+
+import Data.Proxy
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
+
+data Borked a (b :: k) = forall (c :: k). B (Proxy c)
+ -- this last one is OK. But there was a bug involving renaming
+ -- that failed here, so the test case remains.
diff --git a/tests/examples/pre-ghc86/Dep3.hs b/tests/examples/pre-ghc86/Dep3.hs
new file mode 100644
index 0000000..cba5043
--- /dev/null
+++ b/tests/examples/pre-ghc86/Dep3.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TypeFamilies, TypeInType, GADTs #-}
+
+module Dep3 where
+
+import Data.Kind
+import GHC.Exts ( Constraint )
+
+type Star1 = *
+
+data Id1 (a :: Star1) where
+ Id1 :: a -> Id1 a
+
+data Id1' :: Star1 -> * where
+ Id1' :: a -> Id1' a
+
+type family Star2 x where
+ Star2 x = *
+
+data Id2a (a :: Star2 Constraint) = Id2a a
+
+
+data Id2 (a :: Star2 Constraint) where
+ Id2 :: a -> Id2 a
+
+data Id2' :: Star2 Constraint -> * where
+ Id2' :: a -> Id2' a
diff --git a/tests/examples/pre-ghc86/KindEqualities2.hs b/tests/examples/pre-ghc86/KindEqualities2.hs
new file mode 100644
index 0000000..5a6f60d
--- /dev/null
+++ b/tests/examples/pre-ghc86/KindEqualities2.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
+ TemplateHaskell, UndecidableInstances, ScopedTypeVariables,
+ TypeInType #-}
+
+module KindEqualities2 where
+
+import Data.Kind
+import GHC.Exts ( Any )
+
+data Kind = Star | Arr Kind Kind
+
+data Ty :: Kind -> * where
+ TInt :: Ty Star
+ TBool :: Ty Star
+ TMaybe :: Ty (Arr Star Star)
+ TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2
+
+
+data TyRep (k :: Kind) (t :: Ty k) where
+ TyInt :: TyRep Star TInt
+ TyBool :: TyRep Star TBool
+ TyMaybe :: TyRep (Arr Star Star) TMaybe
+ TyApp :: TyRep (Arr k1 k2) a -> TyRep k1 b -> TyRep k2 (TApp a b)
+
+type family IK (k :: Kind)
+type instance IK Star = *
+type instance IK (Arr k1 k2) = IK k1 -> IK k2
+
+$(return []) -- necessary because the following instances depend on the
+ -- previous ones.
+
+type family I (t :: Ty k) :: IK k
+type instance I TInt = Int
+type instance I TBool = Bool
+type instance I TMaybe = Maybe
+type instance I (TApp a b) = (I a) (I b)
+
+zero :: forall (a :: Ty 'Star). TyRep Star a -> I a
+zero TyInt = 0
+zero TyBool = False
+zero (TyApp TyMaybe TyInt) = Nothing
+
+main = print $ zero (TyApp TyMaybe TyInt)
diff --git a/tests/examples/pre-ghc86/LiftedConstructors.hs b/tests/examples/pre-ghc86/LiftedConstructors.hs
new file mode 100644
index 0000000..af14b4a
--- /dev/null
+++ b/tests/examples/pre-ghc86/LiftedConstructors.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds, TypeOperators, GADTs #-}
+
+give :: b -> Pattern '[b] a
+give b = Pattern (const (Just $ oneT b))
+
+
+pfail :: Pattern '[] a
+pfail = is (const False)
+
+(/\) :: Pattern vs1 a -> Pattern vs2 a -> Pattern (vs1 :++: vs2) a
+(/\) = mk2 (\a -> Just (a,a))
+
+data Pattern :: [*] -> * where
+ Nil :: Pattern '[]
+ Cons :: Maybe h -> Pattern t -> Pattern (h ': t)
+
+type Pos = '("vpos", V3 GLfloat)
+type Tag = '("tagByte", V1 Word8)
+
+-- | Alias for the 'In' type from the 'Direction' kind, allows users to write
+-- the 'BroadcastChan In a' type without enabling DataKinds.
+type In = 'In
+-- | Alias for the 'Out' type from the 'Direction' kind, allows users to write
+-- the 'BroadcastChan Out a' type without enabling DataKinds.
+type Out = 'Out
diff --git a/tests/examples/pre-ghc86/RAE_T32a.hs b/tests/examples/pre-ghc86/RAE_T32a.hs
new file mode 100644
index 0000000..08a4ad7
--- /dev/null
+++ b/tests/examples/pre-ghc86/RAE_T32a.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds,
+ PolyKinds, TypeFamilies, GADTs, TypeInType #-}
+
+module RAE_T32a where
+
+import Data.Kind
+
+data family Sing (k :: *) :: k -> *
+
+data TyArr' (a :: *) (b :: *) :: *
+type TyArr (a :: *) (b :: *) = TyArr' a b -> *
+type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
+data TyPi' (a :: *) (b :: TyArr a *) :: *
+type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
+type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
+$(return [])
+
+data MkStar (p :: *) (x :: TyArr' p *)
+type instance MkStar p @@ x = *
+$(return [])
+
+data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where
+ Sigma ::
+ forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
+ Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b -> Sigma p r
+$(return [])
+
+data instance Sing Sigma (Sigma p r) x where
+ SSigma ::
+ forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a)
+ (sp :: Sing * p) (sr :: Sing (TyPi p (MkStar p)) r) (sa :: Sing p a) (sb :: Sing (r @@@ a) b).
+ Sing (Sing (r @@@ a) b) sb ->
+ Sing (Sigma p r) ('Sigma sp sr sa sb)
+
+-- I (RAE) believe this last definition is ill-typed.
diff --git a/tests/examples/pre-ghc86/RAE_T32b.hs b/tests/examples/pre-ghc86/RAE_T32b.hs
new file mode 100644
index 0000000..7e06709
--- /dev/null
+++ b/tests/examples/pre-ghc86/RAE_T32b.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds,
+ RankNTypes, TypeOperators, TypeInType #-}
+
+module RAE_T32b where
+
+import Data.Kind
+
+data family Sing (k :: *) :: k -> *
+
+data TyArr (a :: *) (b :: *) :: *
+type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2
+$(return [])
+
+data Sigma (p :: *) (r :: TyArr p * -> *) :: * where
+ Sigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a).
+ Sing * p -> Sing (TyArr p * -> *) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r
+$(return [])
+
+data instance Sing (Sigma p r) (x :: Sigma p r) :: * where
+ SSigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a)
+ (sp :: Sing * p) (sr :: Sing (TyArr p * -> *) r) (sa :: Sing p a) (sb :: Sing (r @@ a) b).
+ Sing (Sing (r @@ a) b) sb ->
+ Sing (Sigma p r) ('Sigma sp sr sa sb)
diff --git a/tests/examples/pre-ghc86/Rae31.hs b/tests/examples/pre-ghc86/Rae31.hs
new file mode 100644
index 0000000..cedc019
--- /dev/null
+++ b/tests/examples/pre-ghc86/Rae31.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds,
+ TypeFamilies, TypeInType #-}
+
+module A where
+
+import Data.Kind
+
+data family Sing (k :: *) :: k -> *
+type Sing' (x :: k) = Sing k x
+data TyFun' (a :: *) (b :: *) :: *
+type TyFun (a :: *) (b :: *) = TyFun' a b -> *
+type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
+data TyPi' (a :: *) (b :: TyFun a *) :: *
+type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
+type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
+$(return [])
+
+data A (a :: *) (b :: a) (c :: TyFun' a *) -- A :: forall a -> a -> a ~> *
+type instance (@@) (A a b) c = *
+$(return [])
+data B (a :: *) (b :: TyFun' a *) -- B :: forall a -> a ~> *
+type instance (@@) (B a) b = TyPi a (A a b)
+$(return [])
+data C (a :: *) (b :: TyPi a (B a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ c @@@ d) *)
diff --git a/tests/examples/pre-ghc86/RaeBlogPost.hs b/tests/examples/pre-ghc86/RaeBlogPost.hs
new file mode 100644
index 0000000..e99c7b5
--- /dev/null
+++ b/tests/examples/pre-ghc86/RaeBlogPost.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies,
+ TypeInType #-}
+{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
+
+module RaeBlogPost where
+
+import Data.Kind
+
+-- a Proxy type with an explicit kind
+data Proxy k (a :: k) = P
+prox :: Proxy * Bool
+prox = P
+
+prox2 :: Proxy Bool 'True
+prox2 = P
+
+-- implicit kinds still work
+data A
+data B :: A -> *
+data C :: B a -> *
+data D :: C b -> *
+data E :: D c -> *
+-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> *
+
+-- a kind-indexed GADT
+data TypeRep (a :: k) where
+ TInt :: TypeRep Int
+ TMaybe :: TypeRep Maybe
+ TApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
+
+zero :: TypeRep a -> a
+zero TInt = 0
+zero (TApp TMaybe _) = Nothing
+
+data Nat = Zero | Succ Nat
+type family a + b where
+ 'Zero + b = b
+ ('Succ a) + b = 'Succ (a + b)
+
+data Vec :: * -> Nat -> * where
+ Nil :: Vec a 'Zero
+ (:>) :: a -> Vec a n -> Vec a ('Succ n)
+infixr 5 :>
+
+-- promoted GADT, and using + as a "kind family":
+type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
+ 'Nil ++ y = y
+ (h ':> t) ++ y = h ':> (t ++ y)
+
+-- datatype that mentions *
+data U = Star (*)
+ | Bool Bool
+
+-- kind synonym
+type Monadish = * -> *
+class MonadTrans (t :: Monadish -> Monadish) where
+ lift :: Monad m => m a -> t m a
+data Free :: Monadish where
+ Return :: a -> Free a
+ Bind :: Free a -> (a -> Free b) -> Free b
+
+-- yes, * really does have type *.
+type Star = (* :: (* :: (* :: *)))
diff --git a/tests/examples/pre-ghc86/RenamingStar.hs b/tests/examples/pre-ghc86/RenamingStar.hs
new file mode 100644
index 0000000..255021c
--- /dev/null
+++ b/tests/examples/pre-ghc86/RenamingStar.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeInType #-}
+
+module RenamingStar where
+
+data Foo :: *
diff --git a/tests/examples/pre-ghc86/SlidingTypeSyn.hs b/tests/examples/pre-ghc86/SlidingTypeSyn.hs
new file mode 100644
index 0000000..1a60d1f
--- /dev/null
+++ b/tests/examples/pre-ghc86/SlidingTypeSyn.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+
+type ( f :-> g) (r :: * -> *) ix = f r ix -> g r ix
+
+type ( f :--> g) b ix = f b ix -> g b ix
+
+type ((f :---> g)) b ix = f b ix -> g b ix
diff --git a/tests/examples/pre-ghc86/T10134a.hs b/tests/examples/pre-ghc86/T10134a.hs
new file mode 100644
index 0000000..0d84d56
--- /dev/null
+++ b/tests/examples/pre-ghc86/T10134a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T10134a where
+
+import GHC.TypeLits
+
+data Vec :: Nat -> * -> * where
+ Nil :: Vec 0 a
+ (:>) :: a -> Vec n a -> Vec (n + 1) a
diff --git a/tests/examples/pre-ghc86/T10321.hs b/tests/examples/pre-ghc86/T10321.hs
new file mode 100644
index 0000000..44d264a
--- /dev/null
+++ b/tests/examples/pre-ghc86/T10321.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T10321 where
+
+import GHC.TypeLits
+
+data Vec :: Nat -> * -> * where
+ Nil :: Vec 0 a
+ (:>) :: a -> Vec n a -> Vec (n + 1) a
+
+infixr 5 :>
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
diff --git a/tests/examples/pre-ghc86/T10934.hs b/tests/examples/pre-ghc86/T10934.hs
new file mode 100644
index 0000000..fb7a538
--- /dev/null
+++ b/tests/examples/pre-ghc86/T10934.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE
+ ScopedTypeVariables
+ , DataKinds
+ , GADTs
+ , RankNTypes
+ , TypeOperators
+ , PolyKinds -- Comment out PolyKinds and the bug goes away.
+ #-}
+{-# OPTIONS_GHC -O #-}
+ -- The bug is in SimplUtils.abstractFloats, so we need -O to trigger it
+
+module KeyValue where
+
+data AccValidation err a = AccFailure err | AccSuccess a
+
+data KeyValueError = MissingValue
+
+type WithKeyValueError = AccValidation [KeyValueError]
+
+missing :: forall f rs. RecApplicative rs => Rec (WithKeyValueError :. f) rs
+missing = rpure missingField
+ where
+ missingField :: forall x. (WithKeyValueError :. f) x
+ missingField = Compose $ AccFailure [MissingValue]
+
+data Rec :: (u -> *) -> [u] -> * where
+ RNil :: Rec f '[]
+ (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
+
+newtype Compose (f :: l -> *) (g :: k -> l) (x :: k)
+ = Compose { getCompose :: f (g x) }
+
+type (:.) f g = Compose f g
+
+class RecApplicative rs where
+ rpure
+ :: (forall x. f x)
+ -> Rec f rs
diff --git a/tests/examples/pre-ghc86/T11142.hs b/tests/examples/pre-ghc86/T11142.hs
new file mode 100644
index 0000000..58eb3b6
--- /dev/null
+++ b/tests/examples/pre-ghc86/T11142.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeInType, RankNTypes #-}
+
+module T11142 where
+
+import Data.Kind
+
+data SameKind :: k -> k -> *
+
+foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
+foo = undefined
diff --git a/tests/examples/pre-ghc86/T3927b.hs b/tests/examples/pre-ghc86/T3927b.hs
new file mode 100644
index 0000000..98e4cb9
--- /dev/null
+++ b/tests/examples/pre-ghc86/T3927b.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
+
+module T3927b where
+
+import Data.Proxy
+import GHC.Exts
+
+data Message
+
+data SocketType = Dealer | Push | Pull
+
+data SocketOperation = Read | Write
+
+type family Restrict (a :: SocketOperation) (as :: [SocketOperation]) :: Constraint where
+ Restrict a (a ': as) = ()
+ Restrict x (a ': as) = Restrict x as
+ Restrict x '[] = ("Error!" ~ "Tried to apply a restricted type!")
+
+type family Implements (t :: SocketType) :: [SocketOperation] where
+ Implements Dealer = ['Read, Write]
+ Implements Push = '[Write]
+ Implements Pull = '[ 'Read]
+
+data SockOp :: SocketType -> SocketOperation -> * where
+ SRead :: SockOp sock 'Read
+ SWrite :: SockOp sock Write
+
+data Socket :: SocketType -> * where
+ Socket :: proxy sock
+ -> (forall op . Restrict op (Implements sock) => SockOp sock op -> Operation op)
+ -> Socket sock
+
+type family Operation (op :: SocketOperation) :: * where
+ Operation 'Read = IO Message
+ Operation Write = Message -> IO ()
+
+class Restrict 'Read (Implements t) => Readable t where
+ readSocket :: Socket t -> Operation 'Read
+ readSocket (Socket _ f) = f (SRead :: SockOp t 'Read)
+
+instance Readable Dealer
+
+type family Writable (t :: SocketType) :: Constraint where
+ Writable Dealer = ()
+ Writable Push = ()
+
+dealer :: Socket Dealer
+dealer = Socket (Proxy :: Proxy Dealer) f
+ where
+ f :: Restrict op (Implements Dealer) => SockOp Dealer op -> Operation op
+ f SRead = undefined
+ f SWrite = undefined
+
+push :: Socket Push
+push = Socket (Proxy :: Proxy Push) f
+ where
+ f :: Restrict op (Implements Push) => SockOp Push op -> Operation op
+ f SWrite = undefined
+
+pull :: Socket Pull
+pull = Socket (Proxy :: Proxy Pull) f
+ where
+ f :: Restrict op (Implements Pull) => SockOp Pull op -> Operation op
+ f SRead = undefined
+
+foo :: IO Message
+foo = readSocket dealer
diff --git a/tests/examples/pre-ghc86/T9632.hs b/tests/examples/pre-ghc86/T9632.hs
new file mode 100644
index 0000000..bea468f
--- /dev/null
+++ b/tests/examples/pre-ghc86/T9632.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeInType #-}
+
+module T9632 where
+
+import Data.Kind
+
+data B = T | F
+data P :: B -> *
+
+type B' = B
+data P' :: B' -> *
diff --git a/tests/examples/pre-ghc86/TensorTests.hs b/tests/examples/pre-ghc86/TensorTests.hs
new file mode 100644
index 0000000..497b839
--- /dev/null
+++ b/tests/examples/pre-ghc86/TensorTests.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE ConstraintKinds, FlexibleContexts, DataKinds, NoImplicitPrelude,
+ RebindableSyntax, ScopedTypeVariables, TypeFamilies, TypeOperators,
+ UndecidableInstances #-}
+
+module TensorTests (tensorTests) where
+
+import Apply.Cyc
+import Tests
+import Utils
+
+import TestTypes
+
+import Crypto.Lol
+import Crypto.Lol.CRTrans
+import Crypto.Lol.Cyclotomic.Tensor
+import Crypto.Lol.Types
+
+import Control.Applicative
+
+import Data.Maybe
+
+import Data.Singletons
+import Data.Promotion.Prelude.Eq
+import Data.Singletons.TypeRepStar ()
+
+import qualified Test.Framework as TF
+
+type TMRParams = ( '( , ,) <$> Tensors <*> Tensors) <*> MRCombos
+
+type TMRParams = ( '(,) <$> Tensors) <*> MRCombos
+tmrParams :: Proxy TMRParams
+tmrParams = Proxy
+
+--type ExtParams = ( '(,) <$> Tensors) <*> MRExtCombos
+type TrEmParams = ( '(,) <$> Tensors) <*> MM'RCombos
+tremParams :: Proxy TrEmParams
+tremParams = Proxy
+
+type NormParams = ( '(,) <$> '[RT]) <*> (Filter Liftable MRCombos)
+
+data Liftable :: TyFun (Factored, *) Bool -> *
+type instance Apply Liftable '(m,zq) = Int64 :== (LiftOf zq)
+
diff --git a/tests/examples/pre-ghc86/UnicodeSyntax.hs b/tests/examples/pre-ghc86/UnicodeSyntax.hs
new file mode 100644
index 0000000..9e4cc50
--- /dev/null
+++ b/tests/examples/pre-ghc86/UnicodeSyntax.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE Arrows #-}
+
+module Tutorial where
+
+-- import Abt.Class
+-- import Abt.Types
+-- import Abt.Concrete.LocallyNameless
+
+import Control.Applicative
+import Control.Monad.Trans.State.Strict
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Except
+-- import Data.Vinyl
+import Prelude hiding (pi)
+
+-- | We'll start off with a monad in which to manipulate ABTs; we'll need some
+-- state for fresh variable generation.
+--
+newtype M α
+ = M
+ { _M ∷ State Int α
+ } deriving (Functor, Applicative, Monad)
+
+-- | We'll run an ABT computation by starting the variable counter at @0@.
+--
+runM ∷ M α → α
+runM (M m) = evalState m 0
+
+-- | Check out the source to see fresh variable generation.
+--
+instance MonadVar Var M where
+ fresh = M $ do
+ n ← get
+ let n' = n + 1
+ put n'
+ return $ Var Nothing n'
+
+ named a = do
+ v ← fresh
+ return $ v { _varName = Just a }
+
+-- | Next, we'll define the operators for a tiny lambda calculus as a datatype
+-- indexed by arities.
+--
+data Lang ns where
+ LAM ∷ Lang '[S Z]
+ APP ∷ Lang '[Z, Z]
+ PI ∷ Lang '[Z, S Z]
+ UNIT ∷ Lang '[]
+ AX ∷ Lang '[]
+
+instance Show1 Lang where
+ show1 = \case
+ LAM → "lam"
+ APP → "ap"
+ PI → "pi"
+ UNIT → "unit"
+ AX → "<>"
+
+instance HEq1 Lang where
+ heq1 LAM LAM = Just Refl
+ heq1 APP APP = Just Refl
+ heq1 PI PI = Just Refl
+ heq1 UNIT UNIT = Just Refl
+ heq1 AX AX = Just Refl
+ heq1 _ _ = Nothing
+
+lam ∷ Tm Lang (S Z) → Tm0 Lang
+lam e = LAM $$ e :& RNil
+
+app ∷ Tm0 Lang → Tm0 Lang → Tm0 Lang
+app m n = APP $$ m :& n :& RNil
+
+ax ∷ Tm0 Lang
+ax = AX $$ RNil
+
+unit ∷ Tm0 Lang
+unit = UNIT $$ RNil
+
+pi ∷ Tm0 Lang → Tm Lang (S Z) → Tm0 Lang
+pi α xβ = PI $$ α :& xβ :& RNil
+
+-- | A monad transformer for small step operational semantics.
+--
+newtype StepT m α
+ = StepT
+ { runStepT ∷ MaybeT m α
+ } deriving (Monad, Functor, Applicative, Alternative)
+
+-- | To indicate that a term is in normal form.
+--
+stepsExhausted
+ ∷ Applicative m
+ ⇒ StepT m α
+stepsExhausted = StepT . MaybeT $ pure Nothing
+
+instance MonadVar Var m ⇒ MonadVar Var (StepT m) where
+ fresh = StepT . MaybeT $ Just <$> fresh
+ named str = StepT . MaybeT $ Just <$> named str
+
+-- | A single evaluation step.
+--
+step
+ ∷ Tm0 Lang
+ → StepT M (Tm0 Lang)
+step tm =
+ out tm >>= \case
+ APP :$ m :& n :& RNil →
+ out m >>= \case
+ LAM :$ xe :& RNil → xe // n
+ _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n
+ PI :$ α :& xβ :& RNil → pi <$> step α <*> pure xβ
+ _ → stepsExhausted
+
+-- | The reflexive-transitive closure of a small-step operational semantics.
+--
+star
+ ∷ Monad m
+ ⇒ (α → StepT m α)
+ → (α → m α)
+star f a =
+ runMaybeT (runStepT $ f a) >>=
+ return a `maybe` star f
+
+-- | Evaluate a term to normal form
+--
+eval ∷ Tm0 Lang → Tm0 Lang
+eval = runM . star step
+
+newtype JudgeT m α
+ = JudgeT
+ { runJudgeT ∷ ExceptT String m α
+ } deriving (Monad, Functor, Applicative, Alternative)
+
+instance MonadVar Var m ⇒ MonadVar Var (JudgeT m) where
+ fresh = JudgeT . ExceptT $ Right <$> fresh
+ named str = JudgeT . ExceptT $ Right <$> named str
+
+type Ctx = [(Var, Tm0 Lang)]
+
+raise ∷ Monad m ⇒ String → JudgeT m α
+raise = JudgeT . ExceptT . return . Left
+
+checkTy
+ ∷ Ctx
+ → Tm0 Lang
+ → Tm0 Lang
+ → JudgeT M ()
+checkTy g tm ty = do
+ let ntm = eval tm
+ nty = eval ty
+ (,) <$> out ntm <*> out nty >>= \case
+ (LAM :$ xe :& RNil, PI :$ α :& yβ :& RNil) → do
+ z ← fresh
+ ez ← xe // var z
+ βz ← yβ // var z
+ checkTy ((z,α):g) ez βz
+ (AX :$ RNil, UNIT :$ RNil) → return ()
+ _ → do
+ ty' ← inferTy g tm
+ if ty' === nty
+ then return ()
+ else raise "Type error"
+
+inferTy
+ ∷ Ctx
+ → Tm0 Lang
+ → JudgeT M (Tm0 Lang)
+inferTy g tm = do
+ out (eval tm) >>= \case
+ V v | Just (eval → ty) ← lookup v g → return ty
+ | otherwise → raise "Ill-scoped variable"
+ APP :$ m :& n :& RNil → do
+ inferTy g m >>= out >>= \case
+ PI :$ α :& xβ :& RNil → do
+ checkTy g n α
+ eval <$> xβ // n
+ _ → raise "Expected pi type for lambda abstraction"
+ _ → raise "Only infer neutral terms"
+
+-- | @λx.x@
+--
+identityTm ∷ M (Tm0 Lang)
+identityTm = do
+ x ← fresh
+ return $ lam (x \\ var x)
+
+-- | @(λx.x)(λx.x)@
+--
+appTm ∷ M (Tm0 Lang)
+appTm = do
+ tm ← identityTm
+ return $ app tm tm
+
+-- | A demonstration of evaluating (and pretty-printing). Output:
+--
+-- @
+-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@4.\@4]
+-- @
+--
+main ∷ IO ()
+main = do
+ -- Try out the type checker
+ either fail print . runM . runExceptT . runJudgeT $ do
+ x ← fresh
+ checkTy [] (lam (x \\ var x)) (pi unit (x \\ unit))
+
+ print . runM $ do
+ mm ← appTm
+ mmStr ← toString mm
+ mmStr' ← toString $ eval mm
+ return $ mmStr ++ " ~>* " ++ mmStr'
+
+doMap ∷ FilePath → IOSArrow XmlTree TiledMap
+doMap mapPath = proc m → do
+ mapWidth ← getAttrR "width" ⤙ m
+ returnA -< baz
+
+-- ^ An opaque ESD handle for recording data from the soundcard via ESD.
+data Recorder fr ch (r ∷ ★ → ★)
+ = Recorder {
+ reRate ∷ !Int
+ , reHandle ∷ !Handle
+ , reCloseH ∷ !(FinalizerHandle r)
+ }
+
+-- from ghc-prim
+
+-- | A backward-compatible (pre-GHC 8.0) synonym for 'Type'
+type * = TYPE 'PtrRepLifted
+
+-- | A unicode backward-compatible (pre-GHC 8.0) synonym for 'Type'
+type ★ = TYPE 'PtrRepLifted
diff --git a/tests/examples/pre-ghc86/Vect.hs b/tests/examples/pre-ghc86/Vect.hs
new file mode 100644
index 0000000..59c8404
--- /dev/null
+++ b/tests/examples/pre-ghc86/Vect.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE ParallelArrays #-}
+{-# OPTIONS_GHC -fvectorise #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module Vect where
+
+-- import Data.Array.Parallel
+
+
+{-# VECTORISe isFive = blah #-}
+{-# NoVECTORISE isEq #-}
+
+{-# VECTORISE SCALAR type Int #-}
+{-# VECTORISE type Char #-}
+{-# VECTORISE type ( ) #-}
+{-# VECTORISE type (# #) #-}
+
+{-# VECTORISE SCALAR type Integer = Int #-}
+{-# VECTORISE type Bool = String #-}
+
+{-# Vectorise class Eq #-}
+
+blah = 5
+
+data MyBool = MyTrue | MyFalse
+
+class Eq a => Cmp a where
+ cmp :: a -> a -> Bool
+
+-- FIXME:
+-- instance Cmp Int where
+-- cmp = (==)
+-- isFive :: (Eq a, Num a) => a -> Bool
+isFive :: Int -> Bool
+isFive x = x == 5
+
+isEq :: Eq a => a -> Bool
+isEq x = x == x
+
+
+fiveEq :: Int -> Bool
+fiveEq x = isFive x && isEq x
+
+cmpArrs :: PArray Int -> PArray Int -> Bool
+{-# NOINLINE cmpArrs #-}
+cmpArrs v w = cmpArrs' (fromPArrayP v) (fromPArrayP w)
+
+cmpArrs' :: [:Int:] -> [:Int:] -> Bool
+cmpArrs' xs ys = andP [:x == y | x <- xs | y <- ys:]
+
+isFives :: PArray Int -> Bool
+{-# NOINLINE isFives #-}
+isFives xs = isFives' (fromPArrayP xs)
+
+isFives' :: [:Int:] -> Bool
+isFives' xs = andP (mapP isFive xs)
+
+isEqs :: PArray Int -> Bool
+{-# NOINLINE isEqs #-}
+isEqs xs = isEqs' (fromPArrayP xs)
+
+isEqs' :: [:Int:] -> Bool
+isEqs' xs = undefined -- andP (mapP isEq xs)
+
+-- fudge for compiler
+
+fromPArrayP = undefined
+andP = undefined
+mapP = undefined
+data PArray a = PArray a
diff --git a/tests/examples/pre-ghc86/Webhook.hs b/tests/examples/pre-ghc86/Webhook.hs
new file mode 100644
index 0000000..decc719
--- /dev/null
+++ b/tests/examples/pre-ghc86/Webhook.hs
@@ -0,0 +1,176 @@
+{-|
+Module : Servant.GitHub.Webhook
+Description : Easily write safe GitHub webhook handlers with Servant
+Copyright : (c) Jacob Thomas Errington, 2016
+License : MIT
+Maintainer : servant-github-webhook@mail.jerrington.me
+Stability : experimental
+
+The GitHub webhook machinery will attach three headers to the HTTP requests
+that it fires: @X-Github-Event@, @X-Hub-Signature@, and @X-Github-Delivery@.
+The former two headers correspond with the 'GitHubEvent' and
+'GitHubSignedReqBody''' routing combinators. This library ignores the
+@X-Github-Delivery@ header; if you would like to access its value, then use the
+builtin 'Header' combinator from Servant.
+
+Usage of the library is straightforward: protect routes with the 'GitHubEvent'
+combinator to ensure that the route is only reached for specific
+'RepoWebhookEvent's, and replace any 'ReqBody' combinators you would write
+under that route with 'GitHubSignedReqBody'. It is advised to always include a
+'GitHubSignedReqBody''', as this is the only way you can be sure that it is
+GitHub who is sending the request, and not a malicious user. If you don't care
+about the request body, then simply use Aeson\'s 'Object' type as the
+deserialization target -- @GitHubSignedReqBody' key '[JSON] Object@ -- and
+ignore the @Object@ in the handler.
+
+The 'GitHubSignedReqBody''' combinator makes use of the Servant 'Context' in
+order to extract the signing key. This is the same key that must be entered in
+the configuration of the webhook on GitHub. See 'GitHubKey'' for more details.
+
+In order to support multiple keys on a per-route basis, the basic combinator
+@GitHubSignedReqBody''@ takes as a type parameter as a key index. To use this,
+create a datatype, e.g. @KeyIndex@ whose constructors identify the different
+keys you will be using. Generally, this means one constructor per repository.
+Use the @DataKinds@ extension to promote this datatype to a kind, and write an
+instance of 'Reflect' for each promoted constructor of your datatype. Finally,
+create a 'Context' containing 'GitHubKey'' whose wrapped function's domain is
+the datatype you've built up. Thus, your function can determine which key to
+retrieve.
+-}
+
+{-# LANGUAGE CPP #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- GHC 8 seems to have improved its decidability check for type family
+-- instances and class instances. In particular, without UndecidableInstances
+-- enabled, the Demote' instance for lists, which we need, will not compile.
+-- Similarly, the Reflect instance for Symbol, which just requires KnownSymbol,
+-- won't compile on GHC < 8 because the instance head is no smaller than the
+-- instance head.
+#if __GLASGOW_HASKELL__ < 800
+{-# LANGUAGE UndecidableInstances #-}
+#endif
+
+module Servant.GitHub.Webhook
+( -- * Servant combinators
+ GitHubSignedReqBody''
+, GitHubSignedReqBody'
+, GitHubSignedReqBody
+, GitHubEvent
+
+ -- ** Security
+, GitHubKey'(..)
+, GitHubKey
+, gitHubKey
+
+ -- * Reexports
+ --
+ -- | We reexport a few datatypes that are typically needed to use the
+ -- library.
+, RepoWebhookEvent(..)
+, KProxy(..)
+
+ -- * Implementation details
+
+ -- ** Type-level programming machinery
+, Demote
+, Demote'
+, Reflect(..)
+
+ -- ** Stringy stuff
+, parseHeaderMaybe
+, matchEvent
+
+ -- * Examples
+ --
+ -- $example1
+ --
+ -- $example2
+) where
+
+import Control.Monad.IO.Class ( liftIO )
+import Data.Aeson ( decode', encode )
+import qualified Data.ByteString as BS
+import Data.ByteString.Lazy ( fromStrict, toStrict )
+import qualified Data.ByteString.Base16 as B16
+import Data.HMAC ( hmac_sha1 )
+import Data.List ( intercalate )
+import Data.Maybe ( catMaybes, fromMaybe )
+import Data.Monoid ( (<>) )
+import Data.Proxy
+import Data.String.Conversions ( cs )
+import qualified Data.Text.Encoding as E
+import GHC.TypeLits
+import GitHub.Data.Webhooks
+import Network.HTTP.Types hiding (Header, ResponseHeaders)
+import Network.Wai ( requestHeaders, strictRequestBody )
+import Servant
+import Servant.API.ContentTypes ( AllCTUnrender(..) )
+import Servant.Server.Internal
+
+
+-- | A clone of Servant's 'ReqBody' combinator, except that it will also
+-- verify the signature provided by GitHub in the @X-Hub-Signature@ header by
+-- computing the SHA1 HMAC of the request body and comparing.
+--
+-- The use of this combinator will require that the router context contain an
+-- appropriate 'GitHubKey'' entry. Specifically, the type parameter of
+-- 'GitHubKey'' must correspond with @Demote k@ where @k@ is the kind of the
+-- index @key@ used here. Consequently, it will be necessary to use
+-- 'serveWithContext' instead of 'serve'.
+--
+-- Other routes are not tried upon the failure of this combinator, and a 401
+-- response is generated.
+--
+-- Use of this datatype directly is discouraged, since the choice of the index
+-- @key@ determines its kind @k@ and hence @proxy@, which is . Instead, use
+-- 'GitHubSignedReqBody'', which computes the @proxy@ argument given just
+-- @key@. The proxy argument is necessary to avoid @UndecidableInstances@ for
+-- the implementation of the 'HasServer' instance for the datatype.
+data GitHubSignedReqBody''
+ (proxy :: KProxy k)
+ (key :: k)
+ (list :: [*])
+ (result :: *) where
+
+-- | Convenient synonym for 'GitHubSignedReqBody''' that computes its first
+-- type argument given just the second one.
+--
+-- Use this type synonym if you are creating a webhook server to handle
+-- webhooks from multiple repositories, with different secret keys.
+type GitHubSignedReqBody' (key :: k)
+ = GitHubSignedReqBody'' ('KProxy :: KProxy k) key
+
+-- | A convenient alias for a trivial key index.
+--
+-- USe this type synonym if you are creating a webhook server to handle only
+-- webhooks from a single repository, or for mutliple repositories using the
+-- same secret key.
+type GitHubSignedReqBody = GitHubSignedReqBody' '()
+
+-- | A routing combinator that succeeds only for a webhook request that matches
+-- one of the given 'RepoWebhookEvent' given in the type-level list @events@.
+--
+-- If the list contains 'WebhookWildcardEvent', then all events will be
+-- matched.
+--
+-- The combinator will require that its associated handler take a
+-- 'RepoWebhookEvent' parameter, and the matched event will be passed to the
+-- handler. This allows the handler to determine which event triggered it from
+-- the list.
+--
+-- Other routes are tried if there is a mismatch.
+data GitHubEvent (events :: [RepoWebhookEvent]) where
+
diff --git a/tests/examples/pre-ghc86/determ004.hs b/tests/examples/pre-ghc86/determ004.hs
new file mode 100644
index 0000000..c74f8d0
--- /dev/null
+++ b/tests/examples/pre-ghc86/determ004.hs
@@ -0,0 +1,311 @@
+{-# LANGUAGE TypeOperators
+ , DataKinds
+ , PolyKinds
+ , TypeFamilies
+ , GADTs
+ , UndecidableInstances
+ , RankNTypes
+ , ScopedTypeVariables
+ #-}
+
+{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS_GHC -Werror #-}
+{-# OPTIONS_GHC -O1 -fspec-constr #-}
+
+{-
+
+With reversed order of allocated uniques the type variables would be in
+wrong order:
+
+*** Core Lint errors : in result of SpecConstr ***
+determ004.hs:88:12: warning:
+ [in body of lambda with binder m_azbFg :: a_afdP_azbON]
+ @ (a_afdP_azbON :: BOX) is out of scope
+*** Offending Program ***
+
+...
+
+Rec {
+$s$wsFoldr1_szbtK
+ :: forall (m_azbFg :: a_afdP_azbON)
+ (x_azbOM :: TyFun
+ a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> *)
+ -> *)
+ (a_afdP_azbON :: BOX)
+ (ipv_szbwN :: a_afdP_azbON)
+ (ipv_szbwO :: [a_afdP_azbON]).
+ R:Sing[]z (ipv_szbwN : ipv_szbwO)
+ ~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO)
+ -> Sing ipv_szbwO
+ -> Sing ipv_szbwN
+ -> (forall (t_azbNM :: a_afdP_azbON).
+ Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM))
+ -> Sing
+ (Apply
+ (Apply Foldr1Sym0 x_azbOM)
+ (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
+[LclId,
+ Arity=4,
+ Str=DmdType <L,U><L,U><L,U><C(S(C(S))),C(U(1*C1(U)))>]
+$s$wsFoldr1_szbtK =
+ \ (@ (m_azbFg :: a_afdP_azbON))
+ (@ (x_azbOM :: TyFun
+ a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> *)
+ -> *))
+ (@ (a_afdP_azbON :: BOX))
+ (@ (ipv_szbwN :: a_afdP_azbON))
+ (@ (ipv_szbwO :: [a_afdP_azbON]))
+ (sg_szbtL
+ :: R:Sing[]z (ipv_szbwN : ipv_szbwO)
+ ~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO))
+ (sc_szbtM :: Sing ipv_szbwO)
+ (sc_szbtN :: Sing ipv_szbwN)
+ (sc_szbtP
+ :: forall (t_azbNM :: a_afdP_azbON).
+ Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM)) ->
+ case (SCons
+ @ a_afdP_azbON
+ @ (ipv_szbwN : ipv_szbwO)
+ @ ipv_szbwO
+ @ ipv_szbwN
+ @~ (<ipv_szbwN : ipv_szbwO>_N
+ :: (ipv_szbwN : ipv_szbwO) ~# (ipv_szbwN : ipv_szbwO))
+ sc_szbtN
+ sc_szbtM)
+ `cast` (sg_szbtL
+ ; TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <Let1627448493XsSym4
+ x_azbOM m_azbFg ipv_szbwN ipv_szbwO>_N
+ :: R:Sing[]z (ipv_szbwN : ipv_szbwO)
+ ~R# R:Sing[]z
+ (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
+ of wild_XD {
+ SNil dt_dzbxX ->
+ (lvl_szbwi @ a_afdP_azbON)
+ `cast` ((Sing
+ (Sym (TFCo:R:Foldr1[2] <a_afdP_azbON>_N <x_azbOM>_N)
+ ; Sym
+ (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+ <a_afdP_azbON>_N <'[]>_N <x_azbOM>_N)
+ ; (Apply
+ (Sym
+ (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
+ (Sym dt_dzbxX))_N))_R
+ :: Sing (Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list")
+ ~R# Sing
+ (Apply
+ (Apply Foldr1Sym0 x_azbOM)
+ (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
+ SCons @ n_azbFh @ m_XzbGe dt_dzbxK _sX_azbOH
+ ds_dzbyu [Dmd=<S,1*U>] ->
+ case ds_dzbyu
+ `cast` (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <n_azbFh>_N
+ :: Sing n_azbFh ~R# R:Sing[]z n_azbFh)
+ of wild_Xo {
+ SNil dt_dzbxk ->
+ (lvl_szbw1 @ a_afdP_azbON @ m_XzbGe)
+ `cast` ((Sing
+ (Sym (TFCo:R:Foldr1[0] <a_afdP_azbON>_N <m_XzbGe>_N <x_azbOM>_N)
+ ; Sym
+ (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+ <a_afdP_azbON>_N <'[m_XzbGe]>_N <x_azbOM>_N)
+ ; (Apply
+ (Sym
+ (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
+ ((<m_XzbGe>_N ': Sym dt_dzbxk)_N ; Sym dt_dzbxK))_N))_R
+ :: Sing m_XzbGe
+ ~R# Sing
+ (Apply
+ (Apply Foldr1Sym0 x_azbOM)
+ (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
+ SCons @ ipv_XzbxR @ ipv_XzbyV ipv_szbwM ipv_szbwL ipv_szbwK ->
+ case (sc_szbtP @ m_XzbGe _sX_azbOH)
+ `cast` (TFCo:R:Sing(->)f[0]
+ <a_afdP_azbON>_N <a_afdP_azbON>_N <Apply x_azbOM m_XzbGe>_N
+ :: Sing (Apply x_azbOM m_XzbGe)
+ ~R# R:Sing(->)f (Apply x_azbOM m_XzbGe))
+ of wild_X3X { SLambda ds_XzbBr [Dmd=<C(S),1*C1(U)>] ->
+ (ds_XzbBr
+ @ (Foldr1 x_azbOM (ipv_XzbyV : ipv_XzbxR))
+ (($wsFoldr1_szbuc
+ @ a_afdP_azbON
+ @ x_azbOM
+ @ (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR)
+ sc_szbtP
+ ((SCons
+ @ a_afdP_azbON
+ @ (ipv_XzbyV : ipv_XzbxR)
+ @ ipv_XzbxR
+ @ ipv_XzbyV
+ @~ (<ipv_XzbyV : ipv_XzbxR>_N
+ :: (ipv_XzbyV : ipv_XzbxR) ~# (ipv_XzbyV : ipv_XzbxR))
+ ipv_szbwL
+ ipv_szbwK)
+ `cast` (Sym (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N) (Sym
+ (TFCo:R:Apply[][]:$$i[0]
+ <a_afdP_azbON>_N
+ <ipv_XzbxR>_N
+ <ipv_XzbyV>_N)
+ ; (Apply
+ (Sym
+ (TFCo:R:Applyk(->):$l[0]
+ <a_afdP_azbON>_N
+ <ipv_XzbyV>_N))
+ <ipv_XzbxR>_N)_N)
+ :: R:Sing[]z (ipv_XzbyV : ipv_XzbxR)
+ ~R# Sing (Apply (Apply (:$) ipv_XzbyV) ipv_XzbxR))))
+ `cast` ((Sing
+ ((Apply
+ (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N)
+ <Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR>_N)_N
+ ; TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+ <a_afdP_azbON>_N
+ ((Apply
+ (TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N)
+ <ipv_XzbxR>_N)_N
+ ; TFCo:R:Apply[][]:$$i[0]
+ <a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
+ <x_azbOM>_N))_R
+ :: Sing
+ (Apply
+ (Apply Foldr1Sym0 x_azbOM)
+ (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR))
+ ~R# Sing (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))))
+ `cast` ((Sing
+ ((Apply
+ <Apply x_azbOM m_XzbGe>_N
+ (Sym
+ (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+ <a_afdP_azbON>_N <ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
+ ; (Apply
+ (Sym
+ (TFCo:R:Apply(->)(->)Foldr1Sym0l[0]
+ <a_afdP_azbON>_N <x_azbOM>_N))
+ (Sym
+ (TFCo:R:Apply[][]:$$i[0]
+ <a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
+ ; (Apply
+ (Sym
+ (TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N))
+ <ipv_XzbxR>_N)_N))_N))_N
+ ; Sym
+ (TFCo:R:Foldr1[1]
+ <a_afdP_azbON>_N
+ <ipv_XzbxR>_N
+ <ipv_XzbyV>_N
+ <m_XzbGe>_N
+ <x_azbOM>_N)
+ ; Sym
+ (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+ <a_afdP_azbON>_N <m_XzbGe : ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
+ ; (Apply
+ (Sym
+ (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
+ ((<m_XzbGe>_N ': Sym ipv_szbwM)_N ; Sym dt_dzbxK))_N))_R
+ :: Sing
+ (Apply
+ (Apply x_azbOM m_XzbGe)
+ (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))
+ ~R# Sing
+ (Apply
+ (Apply Foldr1Sym0 x_azbOM)
+ (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)))
+ }
+ }
+ }
+...
+-}
+
+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
diff --git a/tests/examples/pre-ghc86/dynamic-paper.hs b/tests/examples/pre-ghc86/dynamic-paper.hs
new file mode 100644
index 0000000..4e89209
--- /dev/null
+++ b/tests/examples/pre-ghc86/dynamic-paper.hs
@@ -0,0 +1,341 @@
+{- This is the code extracted from "A reflection on types", by Simon PJ,
+Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
+
+{-# LANGUAGE RankNTypes, PolyKinds, TypeOperators,
+ ScopedTypeVariables, GADTs, FlexibleInstances,
+ UndecidableInstances, RebindableSyntax,
+ DataKinds, MagicHash, AutoDeriveTypeable, TypeInType #-}
+{-# OPTIONS_GHC -fno-warn-missing-methods -fno-warn-redundant-constraints #-}
+
+module Dynamic where
+
+import Data.Map ( Map )
+import qualified Data.Map as Map
+import Unsafe.Coerce ( unsafeCoerce )
+import Control.Monad ( (<=<) )
+import Prelude hiding ( lookup, fromInteger, replicate )
+import qualified Prelude
+import qualified Data.Typeable
+import qualified Data.Data
+import Data.Kind
+
+lookupMap = Map.lookup
+insertMap = Map.insert
+
+-- let's ignore overloaded numbers
+fromInteger :: Integer -> Int
+fromInteger = Prelude.fromInteger
+
+insertStore = undefined
+schema = undefined
+withTypeable = undefined
+throw# = undefined
+
+toDynamicST = undefined
+fromDynamicST = undefined
+
+extendStore :: Typeable a => STRef s a -> a -> Store -> Store
+lookupStore :: Typeable a => STRef s a -> Store -> Maybe a
+
+type Key = Int
+data STRef s a = STR Key
+type Store = Map Key Dynamic
+
+extendStore (STR k) v s = insertMap k (toDynamicST v) s
+lookupStore (STR k) s = case lookupMap k s of
+ Just d -> fromDynamicST d
+ Nothing -> Nothing
+
+toDynamicST :: Typeable a => a -> Dynamic
+fromDynamicST :: Typeable a => Dynamic -> Maybe a
+
+eval = undefined
+data Term
+
+data DynamicSilly = DIntSilly Int
+ | DBoolSilly Bool
+ | DCharSilly Char
+ | DPairSilly DynamicSilly DynamicSilly
+
+
+toDynInt :: Int -> DynamicSilly
+toDynInt = DIntSilly
+
+fromDynInt :: DynamicSilly -> Maybe Int
+fromDynInt (DIntSilly n) = Just n
+fromDynInt _ = Nothing
+
+toDynPair :: DynamicSilly -> DynamicSilly -> DynamicSilly
+toDynPair = DPairSilly
+
+dynFstSilly :: DynamicSilly -> Maybe DynamicSilly
+dynFstSilly (DPairSilly x1 x2) = Just x1
+dynFstSilly _ = Nothing
+
+eval :: Term -> DynamicSilly
+
+eqT = undefined
+
+instance Typeable (->)
+instance Typeable Maybe
+instance Typeable Bool
+instance Typeable Int
+instance (Typeable a, Typeable b) => Typeable (a b)
+instance Typeable (,)
+
+instance Eq TypeRepX
+
+data Dynamic where
+ Dyn :: TypeRep a -> a -> Dynamic
+
+toDynamic :: Typeable a => a -> Dynamic
+toDynamic x = Dyn typeRep x
+
+eqTNoKind = undefined
+
+eqTNoKind :: TypeRep a -> TypeRep b -> Maybe (a :***: b)
+ -- Primitive; implemented by compiler
+
+data a :***: b where
+ ReflNoKind :: a :***: a
+
+fromDynamic :: forall d. Typeable d => Dynamic -> Maybe d
+fromDynamic (Dyn (ra :: TypeRep a) (x :: a))
+ = case eqT ra (typeRep :: TypeRep d) of
+ Nothing -> Nothing
+ Just Refl -> Just x
+
+fromDynamicMonad :: forall d. Typeable d => Dynamic -> Maybe d
+
+fromDynamicMonad (Dyn ra x)
+ = do Refl <- eqT ra (typeRep :: TypeRep d)
+ return x
+
+cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
+cast x = do Refl <- eqT (typeRep :: TypeRep a)
+ (typeRep :: TypeRep b)
+ return x
+
+gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
+gcast x = do Refl <- eqT (typeRep :: TypeRep a)
+ (typeRep :: TypeRep b)
+ return x
+
+data SameKind :: k -> k -> *
+type CheckAppResult = SameKind AppResult AppResultNoKind
+ -- not the most thorough check
+foo :: AppResult x -> AppResultNoKind x
+foo (App y z) = AppNoKind y z
+
+splitApp :: TypeRep a -> Maybe (AppResult a)
+splitApp = undefined
+splitAppNoKind = undefined
+splitAppNoKind :: TypeRep a -> Maybe (AppResultNoKind a)
+ -- Primitive; implemented by compiler
+
+data AppResultNoKind t where
+ AppNoKind :: TypeRep a -> TypeRep b -> AppResultNoKind (a b)
+
+dynFstNoKind :: Dynamic -> Maybe Dynamic
+dynFstNoKind (Dyn rpab x)
+ = do AppNoKind rpa rb <- splitAppNoKind rpab
+ AppNoKind rp ra <- splitAppNoKind rpa
+ Refl <- eqT rp (typeRep :: TypeRep (,))
+ return (Dyn ra (fst x))
+
+dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
+dynApply (Dyn rf f) (Dyn rx x) = do
+ App ra rt2 <- splitApp rf
+ App rtc rt1 <- splitApp ra
+ Refl <- eqT rtc (typeRep :: TypeRep (->))
+ Refl <- eqT rt1 rx
+ return (Dyn rt2 (f x))
+
+data TypeRepAbstract (a :: k) -- primitive, indexed by type and kind
+
+class Typeable (a :: k) where
+ typeRep :: TypeRep a
+
+data AppResult (t :: k) where
+ App :: forall k1 k (a :: k1 -> k) (b :: k1).
+ TypeRep a -> TypeRep b -> AppResult (a b)
+
+dynFst :: Dynamic -> Maybe Dynamic
+dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
+
+ = do App (rpa :: TypeRep pa ) (rb :: TypeRep b) <- splitApp rpab
+ -- introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2|
+
+ App (rp :: TypeRep p ) (ra :: TypeRep a) <- splitApp rpa
+ -- introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1|
+
+ Refl <- eqT rp (typeRep :: TypeRep (,))
+ -- introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)|
+
+ return (Dyn ra (fst x))
+
+eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b)
+
+data (a :: k1) :~: (b :: k2) where
+ Refl :: forall k (a :: k). a :~: a
+
+castDance :: (Typeable a, Typeable b) => a -> Maybe b
+castDance = castR typeRep typeRep
+
+withTypeable :: TypeRep a -> (Typeable a => r) -> r
+
+castR :: TypeRep a -> TypeRep b -> a -> Maybe b
+castR ta tb = withTypeable ta (withTypeable tb castDance)
+
+cmpT = undefined
+compareTypeRep = undefined
+
+data TypeRepX where
+ TypeRepX :: TypeRep a -> TypeRepX
+
+type TyMapLessTyped = Map TypeRepX Dynamic
+
+insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
+insertLessTyped x = Map.insert (TypeRepX (typeRep :: TypeRep a)) (toDynamic x)
+
+lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a
+lookupLessTyped = fromDynamic <=< Map.lookup (TypeRepX (typeRep :: TypeRep a))
+
+instance Ord TypeRepX where
+ compare (TypeRepX tr1) (TypeRepX tr2) = compareTypeRep tr1 tr2
+
+compareTypeRep :: TypeRep a -> TypeRep b -> Ordering -- primitive
+
+data TyMap = Empty | Node Dynamic TyMap TyMap
+
+lookup :: TypeRep a -> TyMap -> Maybe a
+lookup tr1 (Node (Dyn tr2 v) left right) =
+ case compareTypeRep tr1 tr2 of
+ LT -> lookup tr1 left
+ EQ -> castR tr2 tr1 v -- know this cast will succeed
+ GT -> lookup tr1 right
+lookup tr1 Empty = Nothing
+
+cmpT :: TypeRep a -> TypeRep b -> OrderingT a b
+ -- definition is primitive
+
+data OrderingT a b where
+ LTT :: OrderingT a b
+ EQT :: OrderingT t t
+ GTT :: OrderingT a b
+
+data TypeRep (a :: k) where
+ TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
+ TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k)
+
+data TyCon = TyCon { tc_module :: Module, tc_name :: String }
+data Module = Module { mod_pkg :: String, mod_name :: String }
+
+tcMaybe :: TyCon
+tcMaybe = TyCon { tc_module = Module { mod_pkg = "base"
+ , mod_name = "Data.Maybe" }
+ , tc_name = "Maybe" }
+
+rt = undefined
+
+delta1 :: Dynamic -> Dynamic
+delta1 dn = case fromDynamic dn of
+ Just f -> f dn
+ Nothing -> dn
+loop1 = delta1 (toDynamic delta1)
+
+data Rid = MkT (forall a. TypeRep a -> a -> a)
+rt :: TypeRep Rid
+delta :: forall a. TypeRep a -> a -> a
+delta ra x = case (eqT ra rt) of
+ Just Refl -> case x of MkT y -> y rt x
+ Nothing -> x
+loop = delta rt (MkT delta)
+
+throw# :: SomeException -> a
+
+data SomeException where
+ SomeException :: Exception e => e -> SomeException
+
+class (Typeable e, Show e) => Exception e where { }
+
+data Company
+data Salary
+incS :: Float -> Salary -> Salary
+incS = undefined
+
+-- some impedance matching with SYB
+instance Data.Data.Data Company
+instance {-# INCOHERENT #-} Data.Typeable.Typeable a => Typeable a
+
+mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a
+mkT f x = case (cast f) of
+ Just g -> g x
+ Nothing -> x
+
+data Expr a
+frontEnd = undefined
+
+data DynExp where
+ DE :: TypeRep a -> Expr a -> DynExp
+
+frontEnd :: String -> DynExp
+
+data TyConOld
+
+typeOf = undefined
+eqTOld = undefined
+funTcOld = undefined :: TyConOld
+splitTyConApp = undefined
+mkTyCon3 = undefined
+boolTcOld = undefined
+tupleTc = undefined
+mkTyConApp = undefined
+instance Eq TypeRepOld
+instance Eq TyConOld
+
+data TypeRepOld -- Abstract
+
+class TypeableOld a where
+ typeRepOld :: proxy a -> TypeRepOld
+
+data DynamicOld where
+ DynOld :: TypeRepOld -> a -> DynamicOld
+
+data Proxy a = Proxy
+
+fromDynamicOld :: forall d. TypeableOld d => DynamicOld -> Maybe d
+fromDynamicOld (DynOld trx x)
+ | typeRepOld (Proxy :: Proxy d) == trx = Just (unsafeCoerce x)
+ | otherwise = Nothing
+
+dynApplyOld :: DynamicOld -> DynamicOld -> Maybe DynamicOld
+dynApplyOld (DynOld trf f) (DynOld trx x) =
+ case splitTyConApp trf of
+ (tc, [t1,t2]) | tc == funTcOld && t1 == trx ->
+ Just (DynOld t2 ((unsafeCoerce f) x))
+ _ -> Nothing
+
+data DynamicClosed where
+ DynClosed :: TypeRepClosed a -> a -> DynamicClosed
+
+data TypeRepClosed (a :: *) where
+ TBool :: TypeRepClosed Bool
+ TFun :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
+ TProd :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)
+
+
+lookupPil = undefined
+
+lookupPil :: Typeable a => [Dynamic] -> Maybe a
+
+data Dyn1 = Dyn1 Int
+ | DynFun (Dyn1 -> Dyn1)
+ | DynPair (Dyn1, Dyn1)
+
+data TypeEnum = IntType | FloatType | BoolType | DateType | StringType
+data Schema = Object [Schema] |
+ Field TypeEnum |
+ Array Schema
+
+schema :: Typeable a => a -> Schema
diff --git a/tests/examples/pre-ghc86/mkGADTVars.hs b/tests/examples/pre-ghc86/mkGADTVars.hs
new file mode 100644
index 0000000..1e74c69
--- /dev/null
+++ b/tests/examples/pre-ghc86/mkGADTVars.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs, TypeInType #-}
+
+module GADTVars where
+
+import Data.Kind
+import Data.Proxy
+
+data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
+ MkT :: T x1 * (Proxy (y :: x1), z) z
diff --git a/tests/examples/pre-ghc86/overloadedrecflds_generics.hs b/tests/examples/pre-ghc86/overloadedrecflds_generics.hs
new file mode 100644
index 0000000..c2b4bd6
--- /dev/null
+++ b/tests/examples/pre-ghc86/overloadedrecflds_generics.hs
@@ -0,0 +1,50 @@
+-- Test that DuplicateRecordFields doesn't affect the metadata
+-- generated by GHC.Generics or Data.Data
+
+-- Based on a Stack Overflow post by bennofs
+-- (http://stackoverflow.com/questions/24474581)
+-- licensed under cc by-sa 3.0
+
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Generics
+import Data.Data
+import Data.Proxy
+
+type family FirstSelector (f :: * -> *) :: Meta
+type instance FirstSelector (M1 D x f) = FirstSelector f
+type instance FirstSelector (M1 C x f) = FirstSelector f
+type instance FirstSelector (a :*: b) = FirstSelector a
+type instance FirstSelector (M1 S s f) = s
+
+data SelectorProxy (s :: Meta) (f :: * -> *) a = SelectorProxy
+type SelectorProxy' (s :: Meta) = SelectorProxy s Proxy ()
+
+-- Extract the first selector name using GHC.Generics
+firstSelectorName :: forall a. Selector (FirstSelector (Rep a))
+ => Proxy a -> String
+firstSelectorName _ =
+ selName (SelectorProxy :: SelectorProxy' (FirstSelector (Rep a)))
+
+-- Extract the list of selector names for a constructor using Data.Data
+selectorNames :: Data a => a -> [String]
+selectorNames = constrFields . toConstr
+
+data T = MkT { foo :: Int } deriving (Data, Generic)
+data U = MkU { foo :: Int, bar :: Bool } deriving (Data, Generic)
+
+main = do -- This should yield "foo", not "$sel:foo:MkT"
+ print (firstSelectorName (Proxy :: Proxy T))
+ -- Similarly this should yield "foo"
+ print (firstSelectorName (Proxy :: Proxy U))
+ -- This should yield ["foo"]
+ print (selectorNames (MkT 3))
+ -- And this should yield ["foo","bar"]
+ print (selectorNames (MkU 3 True))