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