Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / simplCore / should_run / T13750a.hs
1 {-# LANGUAGE GADTs #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE TypeFamilies #-}
4 {-# LANGUAGE TypeOperators #-}
5 {-# LANGUAGE PatternSynonyms #-}
6 {-# LANGUAGE ViewPatterns #-}
7 module T13750a where
8
9 import Data.Kind (Type)
10 import Unsafe.Coerce
11
12 type family AnyT :: Type where {}
13 type family AnyList :: [Type] where {}
14
15 newtype NP (xs :: [Type]) = NP [AnyT]
16
17 data IsNP (xs :: [Type]) where
18 IsNil :: IsNP '[]
19 IsCons :: x -> NP xs -> IsNP (x ': xs)
20
21 isNP :: NP xs -> IsNP xs
22 isNP (NP xs) =
23 if null xs
24 then unsafeCoerce IsNil
25 else unsafeCoerce (IsCons (head xs) (NP (tail xs)))
26
27 pattern Nil :: () => (xs ~ '[]) => NP xs
28 pattern Nil <- (isNP -> IsNil)
29 where
30 Nil = NP []
31
32 pattern (:*) :: () => (xs' ~ (x ': xs)) => x -> NP xs -> NP xs'
33 pattern x :* xs <- (isNP -> IsCons x xs)
34 where
35 x :* NP xs = NP (unsafeCoerce x : xs)
36 infixr 5 :*
37
38 data NS (xs :: [[Type]]) = NS !Int (NP AnyList)
39
40 data IsNS (xs :: [[Type]]) where
41 IsZ :: NP x -> IsNS (x ': xs)
42 IsS :: NS xs -> IsNS (x ': xs)
43
44 isNS :: NS xs -> IsNS xs
45 isNS (NS i x)
46 | i == 0 = unsafeCoerce (IsZ (unsafeCoerce x))
47 | otherwise = unsafeCoerce (IsS (NS (i - 1) x))
48
49 pattern Z :: () => (xs' ~ (x ': xs)) => NP x -> NS xs'
50 pattern Z x <- (isNS -> IsZ x)
51 where
52 Z x = NS 0 (unsafeCoerce x)
53
54 pattern S :: () => (xs' ~ (x ': xs)) => NS xs -> NS xs'
55 pattern S p <- (isNS -> IsS p)