blob: 67fa4dd741059ebced235e0663e1238866a8989b (
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
|
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
{-# LANGUAGE TypeInType, TypeFamilies #-}
{- # LANGUAGE UndecidableInstances #-}
module T15552 where
import Data.Kind
data Elem :: k -> [k] -> Type where
Here :: Elem x (x : xs)
There :: Elem x xs -> Elem x (y : xs)
data EntryOfVal (v :: Type) (kvs :: [Type]) where
EntryOfVal :: forall (v :: Type) (kvs :: [Type]) (k :: Type).
Elem (k, v) kvs -> EntryOfVal v kvs
type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
type family GetEntryOfVal (eov :: EntryOfVal v kvs)
:: Elem (EntryOfValKey eov, v) kvs
where
GetEntryOfVal ('EntryOfVal e) = e
type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs
where FirstEntryOfVal v (_ : kvs)
= 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))
--type instance FirstEntryOfVal v (_ : kvs)
-- = 'EntryOfVal ('There (GetEntryOfVal (FirstEntryOfVal v kvs)))
|
