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