blob: 013b18c55eb1c4efc4fbf3d49097221992b7c733 (
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 e (a :: Maybe e). Sing a -> ()
sIsJust SNothing = ()
sIsJust (SJust _) = ()
|
