Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / patsyn / should_compile / T13768.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PatternSynonyms #-}
4 {-# LANGUAGE PolyKinds #-}
5 {-# LANGUAGE TypeOperators #-}
6 {-# LANGUAGE ViewPatterns #-}
7 module T13768 where
8
9 import Data.Kind (Type)
10
11 data NS (f :: k -> Type) (xs :: [k]) = NS Int
12
13 data IsNS (f :: k -> Type) (xs :: [k]) where
14 IsZ :: f x -> IsNS f (x ': xs)
15 IsS :: NS f xs -> IsNS f (x ': xs)
16
17 isNS :: NS f xs -> IsNS f xs
18 isNS = undefined
19
20 pattern Z :: () => (xs' ~ (x ': xs)) => f x -> NS f xs'
21 pattern Z x <- (isNS -> IsZ x)
22
23 pattern S :: () => (xs' ~ (x ': xs)) => NS f xs -> NS f xs'
24 pattern S p <- (isNS -> IsS p)
25
26 {-# COMPLETE Z, S #-}
27
28 data SList :: [k] -> Type where
29 SNil :: SList '[]
30 SCons :: SList (x ': xs)
31
32 go :: SList ys -> NS f ys -> Int
33 go SCons (Z _) = 0
34 go SCons (S _) = 1
35 go SNil _ = error "inaccessible"