Test #14038 in dependent/should_compile/T14038
[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 TypeInType #-}
10 {-# LANGUAGE TypeOperators #-}
11 module T14038 where
12
13 import Data.Kind (Type)
14
15 data family Sing (a :: k)
16 data instance Sing (z :: [a]) where
17 SNil :: Sing '[]
18 SCons :: Sing x -> Sing xs -> Sing (x:xs)
19
20 data TyFun :: Type -> Type -> Type
21 type a ~> b = TyFun a b -> Type
22 infixr 0 ~>
23
24 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
25 type a @@ b = Apply a b
26 infixl 9 @@
27
28 data FunArrow = (:->) -- ^ '(->)'
29 | (:~>) -- ^ '(~>)'
30
31 class FunType (arr :: FunArrow) where
32 type Fun (k1 :: Type) arr (k2 :: Type) :: Type
33
34 class FunType arr => AppType (arr :: FunArrow) where
35 type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
36
37 type FunApp arr = (FunType arr, AppType arr)
38
39 instance FunType (:->) where
40 type Fun k1 (:->) k2 = k1 -> k2
41
42 instance AppType (:->) where
43 type App k1 (:->) k2 (f :: k1 -> k2) x = f x
44
45 instance FunType (:~>) where
46 type Fun k1 (:~>) k2 = k1 ~> k2
47
48 instance AppType (:~>) where
49 type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
50
51 infixr 0 -?>
52 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
53
54 elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
55 Sing l
56 -> p '[]
57 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
58 -> p l
59 elimList = elimListPoly @(:->)
60
61 elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
62 Sing l
63 -> p @@ '[]
64 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
65 -> p @@ l
66 elimListTyFun = elimListPoly @(:~>) @_ @p
67
68 elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
69 FunApp arr
70 => Sing l
71 -> App [a] arr Type p '[]
72 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
73 -> App [a] arr Type p l
74 elimListPoly SNil pNil _ = pNil
75 elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)