blob: 30020854994fadf1c6f73550d6bf7bfce7dc1f52 (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
module T12545a
( ElemWitness(..)
, ElemAt(..)
, JustElemPath
, FindElem
, IsElem
, ElemOf
, ElemsOf
) where
import Data.Proxy (Proxy(..))
data ElemPath = HeadElem
| TailElem ElemPath
data MaybeElemPath = NotElem
| Elem ElemPath
type family FindElem (p :: ElemPath) (a :: k) (l :: [k]) :: MaybeElemPath where
FindElem p a (a ': t) = 'Elem p
FindElem p a (b ': t) = FindElem ('TailElem p) a t
FindElem p a '[] = 'NotElem
type family JustElemPath (p :: MaybeElemPath) :: ElemPath where
JustElemPath ('Elem p) = p
data ElemWitness (p :: ElemPath) (a :: k) (l :: [k]) where
ElemHeadWitness :: ElemWitness 'HeadElem a (a ': t)
ElemTailWitness :: (ElemAt p a t,
FindElem 'HeadElem a (b ': t) ~ 'Elem ('TailElem p))
=> ElemWitness p a t -> ElemWitness ('TailElem p) a (b ': t)
class (FindElem 'HeadElem a l ~ 'Elem p) => ElemAt p (a :: k) (l :: [k]) where
elemWitness :: Proxy a -> Proxy l -> ElemWitness p a l
instance ElemAt 'HeadElem a (a ': t) where
elemWitness _ _ = ElemHeadWitness
instance (ElemAt p a t, FindElem 'HeadElem a (b ': t) ~ 'Elem ('TailElem p))
=> ElemAt ('TailElem p) a (b ': t) where
elemWitness pa _ = ElemTailWitness (elemWitness pa (Proxy :: Proxy t))
type IsElem a l = ElemAt (JustElemPath (FindElem 'HeadElem a l)) a l
class IsElem t (ElemsOf a) => ElemOf a t where
type family ElemsOf a :: [*]
|
