blob: 98afa3ecd622ca3f9fe1d017a900c6ba763d5d8a (
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
|
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module T14369 where
data family Sing (a :: k)
data instance Sing (z :: Maybe a) where
SNothing :: Sing Nothing
SJust :: Sing x -> Sing (Just x)
class SingKind k where
type Demote k = r | r -> k
fromSing :: Sing (a :: k) -> Demote k
instance SingKind a => SingKind (Maybe a) where
type Demote (Maybe a) = Maybe (Demote a)
fromSing SNothing = Nothing
fromSing (SJust x) = Just (fromSing x)
f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
f = fromSing
|
