Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / T13938a.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE ExistentialQuantification #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TemplateHaskell #-}
8 {-# LANGUAGE TypeApplications #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE DataKinds #-}
11 {-# LANGUAGE PolyKinds #-}
12 {-# LANGUAGE TypeOperators #-}
13 module T13938a where
14
15 import Data.Kind (Type)
16
17 data family Sing (a :: k)
18 data instance Sing (z :: [a]) where
19 SNil :: Sing '[]
20 SCons :: Sing x -> Sing xs -> Sing (x:xs)
21
22 data TyFun :: Type -> Type -> Type
23 type a ~> b = TyFun a b -> Type
24 infixr 0 ~>
25
26 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
27 type a @@ b = Apply a b
28 infixl 9 @@
29
30 data FunArrow = (:->) -- ^ '(->)'
31 | (:~>) -- ^ '(~>)'
32
33 class FunType (arr :: FunArrow) where
34 type Fun (k1 :: Type) arr (k2 :: Type) :: Type
35
36 class FunType arr => AppType (arr :: FunArrow) where
37 type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
38
39 type FunApp arr = (FunType arr, AppType arr)
40
41 instance FunType (:->) where
42 type Fun k1 (:->) k2 = k1 -> k2
43
44 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
45
46 instance AppType (:->) where
47 type App k1 (:->) k2 (f :: k1 -> k2) x = f x
48
49 instance FunType (:~>) where
50 type Fun k1 (:~>) k2 = k1 ~> k2
51
52 $(return [])
53
54 instance AppType (:~>) where
55 type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
56
57 infixr 0 -?>
58 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
59
60 elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
61 Sing l
62 -> p '[]
63 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
64 -> p l
65 elimList = elimListPoly @(:->)
66
67 elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
68 Sing l
69 -> p @@ '[]
70 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
71 -> p @@ l
72 elimListTyFun = elimListPoly @(:~>) @_ @p
73
74 elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
75 FunApp arr
76 => Sing l
77 -> App [a] arr Type p '[]
78 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
79 -> App [a] arr Type p l
80 elimListPoly SNil pNil _ = pNil
81 elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)