blob: 745f9b92c121b5d60f83e7e14c065f97e85dcaa9 (
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
30
31
32
33
|
{-# LANGUAGE Haskell2010 #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, MultiParamTypeClasses, KindSignatures,
FunctionalDependencies, FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}
module T6068 where
import Prelude hiding (Maybe, Nothing)
import Data.Kind (Type)
data Maybe :: Type -> Type where
Nothing :: Maybe a
data family Sing (a :: k)
data instance Sing (a :: Maybe k) where
SNothing :: Sing Nothing
data KProxy (a :: Type) = KProxy
data Existential (p :: KProxy k) =
forall (a :: k). Exists (Sing a)
class HasSingleton a (kp :: KProxy k) | a -> kp where
exists :: a -> Existential kp
class Floop a b | a -> b
instance Floop a (mp :: KProxy (Maybe ak)) => HasSingleton (Maybe a) mp where
exists Nothing = Exists SNothing
-- instance forall (a ::Type) (mp :: KProxy (Maybe ak)).
-- HasSingleton (Maybe ak) (Maybe a) mp where
-- exists Nothing = Exists SNothing
|
