blob: e3416d1420a611b691891a79cb4832a006cf0b41 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs, RankNTypes #-}
module T7176 where
type family Sing (a :: b)
data SMaybe (a :: Maybe c) where
SNothing :: SMaybe Nothing
SJust :: Sing a -> SMaybe (Just a)
type instance Sing (a :: Maybe d) = SMaybe a
sIsJust :: forall (a :: Maybe e). Sing a -> ()
sIsJust SNothing = ()
sIsJust (SJust _) = ()
|
