blob: b655df0efe682c4f6acf06dfe7231ca83dd4236a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
module T11984 where
data family Sing (a :: k)
data Schema = Sch [Bool]
data instance Sing (x :: Schema) where
SSch :: Sing x -> Sing ('Sch x)
data instance Sing (x :: [k]) where
SNil :: Sing '[]
SCons :: Sing a -> Sing b -> Sing (a ': b)
data G a where
GCons :: G ('Sch (a ': b))
eval :: G s -> Sing s -> ()
eval GCons s =
case s of
-- SSch SNil -> undefined
SSch (SCons _ _) -> undefined
|
