Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / polykinds / T14174a.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE TypeFamilies #-}
3 {-# LANGUAGE DataKinds #-}
4 {-# LANGUAGE PolyKinds #-}
5 {-# LANGUAGE TypeOperators #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 module T14174a where
8
9 import Data.Kind
10
11 data TyFun :: Type -> Type -> Type
12 type a ~> b = TyFun a b -> Type
13 infixr 0 ~>
14
15 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
16 type a @@ b = Apply a b
17 infixl 9 @@
18
19 data FunArrow = (:->) | (:~>)
20
21 class FunType (arr :: FunArrow) where
22 type Fun (k1 :: Type) arr (k2 :: Type) :: Type
23
24 class FunType arr => AppType (arr :: FunArrow) where
25 type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
26
27 type FunApp arr = (FunType arr, AppType arr)
28
29 instance FunType (:->) where
30 type Fun k1 (:->) k2 = k1 -> k2
31
32 instance AppType (:->) where
33 type App k1 (:->) k2 (f :: k1 -> k2) x = f x
34
35 instance FunType (:~>) where
36 type Fun k1 (:~>) k2 = k1 ~> k2
37
38 instance AppType (:~>) where
39 type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
40
41 infixr 0 -?>
42 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
43
44 type family ElimBool (p :: Bool -> Type)
45 (z :: Bool)
46 (pFalse :: p False)
47 (pTrue :: p True)
48 :: p z where
49 -- Commenting out the line below makes the panic go away
50 ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue
51
52 type family ElimBoolPoly (arr :: FunArrow)
53 (p :: (Bool -?> Type) arr)
54 (z :: Bool)
55 (pFalse :: App Bool arr Type p False)
56 (pTrue :: App Bool arr Type p True)
57 :: App Bool arr Type p z