Add regression tests for #13601, #13780, #13877
[ghc.git] / testsuite / tests / indexed-types / should_fail / T13877.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE Trustworthy #-}
7 {-# LANGUAGE TypeApplications #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE TypeInType #-}
10 {-# LANGUAGE TypeOperators #-}
11 module T13877 where
12
13 import Data.Kind
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 :: * -> * -> *
21 type a ~> b = TyFun a b -> *
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 class FunType (arr :: FunArrow) where
31 type Fun (k1 :: Type) arr (k2 :: Type) :: Type
32
33 class FunType arr => AppType (arr :: FunArrow) where
34 type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
35
36 type FunApp arr = (FunType arr, AppType arr)
37
38 instance FunType (:->) where
39 type Fun k1 (:->) k2 = k1 -> k2
40
41 instance AppType (:->) where
42 type App k1 (:->) k2 (f :: k1 -> k2) x = f x
43
44 instance FunType (:~>) where
45 type Fun k1 (:~>) k2 = k1 ~> k2
46
47 instance AppType (:~>) where
48 type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
49
50 infixr 0 -?>
51 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
52
53 listElim :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
54 Sing l
55 -> p '[]
56 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
57 -> p l
58 listElim = listElimPoly @(:->) @a @p @l
59
60 listElimTyFun :: 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 listElimTyFun = listElimPoly @(:->) @a @p @l
66
67 listElimPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
68 FunApp arr
69 => Sing l
70 -> App [a] arr Type p '[]
71 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
72 -> App [a] arr Type p l
73 listElimPoly SNil pNil _ = pNil
74 listElimPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (listElimPoly @arr @a @p @xs xs pNil pCons)