{-# LANGUAGE DataKinds
, PolyKinds
, TypeOperators
, GADTs
, TypeFamilies
, FlexibleInstances
, Rank2Types
, UndecidableInstances
, ScopedTypeVariables
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Types.Sing
( Sing(..)
, SingI(..), singOf
, sBool
, sUnit
, sPair
, sEither
, sList
, sMaybe
, sUnMeasure
, sUnArray
, sUnPair, sUnPair'
, sUnEither, sUnEither'
, sUnList
, sUnMaybe
, sUnFun
, someSSymbol, ssymbolVal
, sSymbol_Bool
, sSymbol_Unit
, sSymbol_Pair
, sSymbol_Either
, sSymbol_List
, sSymbol_Maybe
) where
import qualified GHC.TypeLits as TL
import Unsafe.Coerce
import Data.Proxy
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.DataKind
infixr 0 `SFun`
infixr 6 `SPlus`
infixr 7 `SEt`
data family Sing (a :: k) :: *
class SingI (a :: k) where sing :: Sing a
singOf :: SingI a => proxy a -> Sing a
singOf :: proxy a -> Sing a
singOf proxy a
_ = Sing a
forall k (a :: k). SingI a => Sing a
sing
data instance Sing (a :: Hakaru) where
SNat :: Sing 'HNat
SInt :: Sing 'HInt
SProb :: Sing 'HProb
SReal :: Sing 'HReal
SMeasure :: !(Sing a) -> Sing ('HMeasure a)
SArray :: !(Sing a) -> Sing ('HArray a)
SFun :: !(Sing a) -> !(Sing b) -> Sing (a ':-> b)
SData :: !(Sing t) -> !(Sing (Code t)) -> Sing (HData' t)
instance Eq (Sing (a :: Hakaru)) where
== :: Sing a -> Sing a -> Bool
(==) = Sing a -> Sing a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Sing :: Hakaru -> *) where
eq1 :: Sing i -> Sing i -> Bool
eq1 Sing i
x Sing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Sing i -> Sing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing i
x Sing i
y)
instance JmEq1 (Sing :: Hakaru -> *) where
jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)
jmEq1 Sing i
SNat Sing j
SNat = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
SInt Sing j
SInt = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
SProb Sing j
SProb = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
SReal Sing j
SReal = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SMeasure a) (SMeasure b) =
Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl ->
TypeEq ('HMeasure a) ('HMeasure a)
-> Maybe (TypeEq ('HMeasure a) ('HMeasure a))
forall a. a -> Maybe a
Just TypeEq ('HMeasure a) ('HMeasure a)
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SArray a) (SArray b) =
Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl ->
TypeEq ('HArray a) ('HArray a)
-> Maybe (TypeEq ('HArray a) ('HArray a))
forall a. a -> Maybe a
Just TypeEq ('HArray a) ('HArray a)
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SFun a1 a2) (SFun b1 b2) =
Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a1 Sing a
b1 Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl ->
Sing b -> Sing b -> Maybe (TypeEq b b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing b
a2 Sing b
b2 Maybe (TypeEq b b)
-> (TypeEq b b -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq b b
Refl ->
TypeEq (a ':-> b) (a ':-> b)
-> Maybe (TypeEq (a ':-> b) (a ':-> b))
forall a. a -> Maybe a
Just TypeEq (a ':-> b) (a ':-> b)
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SData con1 code1) (SData con2 code2) =
Sing t -> Sing t -> Maybe (TypeEq t t)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing t
con1 Sing t
con2 Maybe (TypeEq t t)
-> (TypeEq t t -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq t t
Refl ->
Sing (Code t) -> Sing (Code t) -> Maybe (TypeEq (Code t) (Code t))
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing (Code t)
code1 Sing (Code t)
Sing (Code t)
code2 Maybe (TypeEq (Code t) (Code t))
-> (TypeEq (Code t) (Code t) -> Maybe (TypeEq i j))
-> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq (Code t) (Code t)
Refl ->
TypeEq ('HData t (Code t)) ('HData t (Code t))
-> Maybe (TypeEq ('HData t (Code t)) ('HData t (Code t)))
forall a. a -> Maybe a
Just TypeEq ('HData t (Code t)) ('HData t (Code t))
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
_ Sing j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Show (Sing (a :: Hakaru)) where
showsPrec :: Int -> Sing a -> ShowS
showsPrec = Int -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Sing a -> String
show = Sing a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Show1 (Sing :: Hakaru -> *) where
showsPrec1 :: Int -> Sing i -> ShowS
showsPrec1 Int
p Sing i
s =
case Sing i
s of
Sing i
SNat -> String -> ShowS
showString String
"SNat"
Sing i
SInt -> String -> ShowS
showString String
"SInt"
Sing i
SProb -> String -> ShowS
showString String
"SProb"
Sing i
SReal -> String -> ShowS
showString String
"SReal"
SMeasure s1 -> Int -> String -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"SMeasure" Sing a
s1
SArray s1 -> Int -> String -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"SArray" Sing a
s1
SFun s1 s2 -> Int -> String -> Sing a -> Sing b -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"SFun" Sing a
s1 Sing b
s2
SData s1 s2 -> Int -> String -> Sing t -> Sing (Code t) -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"SData" Sing t
s1 Sing (Code t)
s2
instance SingI 'HNat where sing :: Sing 'HNat
sing = Sing 'HNat
SNat
instance SingI 'HInt where sing :: Sing 'HInt
sing = Sing 'HInt
SInt
instance SingI 'HProb where sing :: Sing 'HProb
sing = Sing 'HProb
SProb
instance SingI 'HReal where sing :: Sing 'HReal
sing = Sing 'HReal
SReal
instance (SingI a) => SingI ('HMeasure a) where sing :: Sing ('HMeasure a)
sing = Sing a -> Sing ('HMeasure a)
forall (a :: Hakaru). Sing a -> Sing ('HMeasure a)
SMeasure Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (SingI a) => SingI ('HArray a) where sing :: Sing ('HArray a)
sing = Sing a -> Sing ('HArray a)
forall (a :: Hakaru). Sing a -> Sing ('HArray a)
SArray Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (SingI a, SingI b) => SingI (a ':-> b) where sing :: Sing (a ':-> b)
sing = Sing a -> Sing b -> Sing (a ':-> b)
forall (a :: Hakaru) (t :: Hakaru).
Sing a -> Sing t -> Sing (a ':-> t)
SFun Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (sop ~ Code t, SingI t, SingI sop) => SingI ('HData t sop) where
sing :: Sing ('HData t sop)
sing = Sing t -> Sing (Code t) -> Sing (HData' t)
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData Sing t
forall k (a :: k). SingI a => Sing a
sing Sing (Code t)
forall k (a :: k). SingI a => Sing a
sing
sUnMeasure :: Sing ('HMeasure a) -> Sing a
sUnMeasure :: Sing ('HMeasure a) -> Sing a
sUnMeasure (SMeasure a) = Sing a
Sing a
a
sUnArray :: Sing ('HArray a) -> Sing a
sUnArray :: Sing ('HArray a) -> Sing a
sUnArray (SArray a) = Sing a
Sing a
a
sUnit :: Sing HUnit
sUnit :: Sing HUnit
sUnit =
Sing ('TyCon "Unit")
-> Sing (Code ('TyCon "Unit")) -> Sing (HData' ('TyCon "Unit"))
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData (Sing "Unit" -> Sing ('TyCon "Unit")
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing "Unit"
sSymbol_Unit)
(Sing '[]
SDone Sing '[] -> Sing '[] -> Sing '[ '[]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SVoid)
sBool :: Sing HBool
sBool :: Sing HBool
sBool =
Sing ('TyCon "Bool")
-> Sing (Code ('TyCon "Bool")) -> Sing (HData' ('TyCon "Bool"))
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData (Sing "Bool" -> Sing ('TyCon "Bool")
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing "Bool"
sSymbol_Bool)
(Sing '[]
SDone Sing '[] -> Sing '[ '[]] -> Sing '[ '[], '[]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SDone Sing '[] -> Sing '[] -> Sing '[ '[]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SVoid)
sPair :: Sing a -> Sing b -> Sing (HPair a b)
sPair :: Sing a -> Sing b -> Sing (HPair a b)
sPair Sing a
a Sing b
b =
Sing (('TyCon "Pair" ':@ a) ':@ b)
-> Sing (Code (('TyCon "Pair" ':@ a) ':@ b))
-> Sing (HData' (('TyCon "Pair" ':@ a) ':@ b))
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData (Sing "Pair" -> Sing ('TyCon "Pair")
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing "Pair"
sSymbol_Pair Sing ('TyCon "Pair") -> Sing a -> Sing ('TyCon "Pair" ':@ a)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
`STyApp` Sing a
a Sing ('TyCon "Pair" ':@ a)
-> Sing b -> Sing (('TyCon "Pair" ':@ a) ':@ b)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
`STyApp` Sing b
b)
((Sing a -> Sing ('K a)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing a
a Sing ('K a) -> Sing '[ 'K b] -> Sing '[ 'K a, 'K b]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing b -> Sing ('K b)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing b
b Sing ('K b) -> Sing '[] -> Sing '[ 'K b]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing '[]
SDone) Sing '[ 'K a, 'K b] -> Sing '[] -> Sing '[ '[ 'K a, 'K b]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SVoid)
sUnPair :: Sing (HPair a b) -> (Sing a, Sing b)
sUnPair :: Sing (HPair a b) -> (Sing a, Sing b)
sUnPair (SData (STyApp (STyApp (STyCon _) a) b) _) = (Sing a
Sing b
a,Sing b
Sing b
b)
sUnPair Sing (HPair a b)
_ = String -> (Sing a, Sing b)
forall a. HasCallStack => String -> a
error String
"sUnPair: the impossible happened"
sUnPair' :: Sing (x :: Hakaru)
-> (forall (a :: Hakaru) (b :: Hakaru) .
(TypeEq x (HPair a b), Sing a, Sing b) -> r)
-> Maybe r
sUnPair' :: Sing x
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HPair a b), Sing a, Sing b) -> r)
-> Maybe r
sUnPair' (SData (STyApp (STyApp (STyCon t) a) b) _) forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HPair a b), Sing a, Sing b) -> r
k
| Just TypeEq s "Pair"
Refl <- Sing s -> Sing "Pair" -> Maybe (TypeEq s "Pair")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
t Sing "Pair"
sSymbol_Pair = r -> Maybe r
forall a. a -> Maybe a
Just (r -> Maybe r) -> r -> Maybe r
forall a b. (a -> b) -> a -> b
$ (TypeEq x (HPair b b), Sing b, Sing b) -> r
forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HPair a b), Sing a, Sing b) -> r
k (TypeEq x (HPair b b)
forall k (a :: k). TypeEq a a
Refl, Sing b
a, Sing b
b)
sUnPair' Sing x
_ forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HPair a b), Sing a, Sing b) -> r
_ = Maybe r
forall a. Maybe a
Nothing
sEither :: Sing a -> Sing b -> Sing (HEither a b)
sEither :: Sing a -> Sing b -> Sing (HEither a b)
sEither Sing a
a Sing b
b =
Sing (('TyCon "Either" ':@ a) ':@ b)
-> Sing (Code (('TyCon "Either" ':@ a) ':@ b))
-> Sing (HData' (('TyCon "Either" ':@ a) ':@ b))
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData (Sing "Either" -> Sing ('TyCon "Either")
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing "Either"
sSymbol_Either Sing ('TyCon "Either") -> Sing a -> Sing ('TyCon "Either" ':@ a)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
`STyApp` Sing a
a Sing ('TyCon "Either" ':@ a)
-> Sing b -> Sing (('TyCon "Either" ':@ a) ':@ b)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
`STyApp` Sing b
b)
((Sing a -> Sing ('K a)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing a
a Sing ('K a) -> Sing '[] -> Sing '[ 'K a]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing '[]
SDone) Sing '[ 'K a] -> Sing '[ '[ 'K b]] -> Sing '[ '[ 'K a], '[ 'K b]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` (Sing b -> Sing ('K b)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing b
b Sing ('K b) -> Sing '[] -> Sing '[ 'K b]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing '[]
SDone)
Sing '[ 'K b] -> Sing '[] -> Sing '[ '[ 'K b]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SVoid)
sUnEither :: Sing (HEither a b) -> (Sing a, Sing b)
sUnEither :: Sing (HEither a b) -> (Sing a, Sing b)
sUnEither (SData (STyApp (STyApp (STyCon _) a) b) _) = (Sing a
Sing b
a,Sing b
Sing b
b)
sUnEither Sing (HEither a b)
_ = String -> (Sing a, Sing b)
forall a. HasCallStack => String -> a
error String
"sUnEither: the impossible happened"
sUnEither' :: Sing (x :: Hakaru)
-> (forall (a :: Hakaru) (b :: Hakaru) .
(TypeEq x (HEither a b), Sing a, Sing b) -> r)
-> Maybe r
sUnEither' :: Sing x
-> (forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HEither a b), Sing a, Sing b) -> r)
-> Maybe r
sUnEither' (SData (STyApp (STyApp (STyCon t) a) b) _) forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HEither a b), Sing a, Sing b) -> r
k
| Just TypeEq s "Either"
Refl <- Sing s -> Sing "Either" -> Maybe (TypeEq s "Either")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
t Sing "Either"
sSymbol_Either = r -> Maybe r
forall a. a -> Maybe a
Just (r -> Maybe r) -> r -> Maybe r
forall a b. (a -> b) -> a -> b
$ (TypeEq x (HEither b b), Sing b, Sing b) -> r
forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HEither a b), Sing a, Sing b) -> r
k (TypeEq x (HEither b b)
forall k (a :: k). TypeEq a a
Refl, Sing b
a, Sing b
b)
sUnEither' Sing x
_ forall (a :: Hakaru) (b :: Hakaru).
(TypeEq x (HEither a b), Sing a, Sing b) -> r
_ = Maybe r
forall a. Maybe a
Nothing
sList :: Sing a -> Sing (HList a)
sList :: Sing a -> Sing (HList a)
sList Sing a
a =
Sing ('TyCon "List" ':@ a)
-> Sing (Code ('TyCon "List" ':@ a))
-> Sing (HData' ('TyCon "List" ':@ a))
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData (Sing "List" -> Sing ('TyCon "List")
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing "List"
sSymbol_List Sing ('TyCon "List") -> Sing a -> Sing ('TyCon "List" ':@ a)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
`STyApp` Sing a
a)
(Sing '[]
SDone Sing '[] -> Sing '[ '[ 'K a, 'I]] -> Sing '[ '[], '[ 'K a, 'I]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` (Sing a -> Sing ('K a)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing a
a Sing ('K a) -> Sing '[ 'I] -> Sing '[ 'K a, 'I]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing 'I
SIdent Sing 'I -> Sing '[] -> Sing '[ 'I]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing '[]
SDone) Sing '[ 'K a, 'I] -> Sing '[] -> Sing '[ '[ 'K a, 'I]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SVoid)
sUnList :: Sing (HList a) -> Sing a
sUnList :: Sing (HList a) -> Sing a
sUnList (SData (STyApp (STyCon _) a) _) = Sing a
Sing b
a
sUnList Sing (HList a)
_ = String -> Sing a
forall a. HasCallStack => String -> a
error String
"sUnList: the impossible happened"
sMaybe :: Sing a -> Sing (HMaybe a)
sMaybe :: Sing a -> Sing (HMaybe a)
sMaybe Sing a
a =
Sing ('TyCon "Maybe" ':@ a)
-> Sing (Code ('TyCon "Maybe" ':@ a))
-> Sing (HData' ('TyCon "Maybe" ':@ a))
forall (t :: HakaruCon). Sing t -> Sing (Code t) -> Sing (HData' t)
SData (Sing "Maybe" -> Sing ('TyCon "Maybe")
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing "Maybe"
sSymbol_Maybe Sing ('TyCon "Maybe") -> Sing a -> Sing ('TyCon "Maybe" ':@ a)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
`STyApp` Sing a
a)
(Sing '[]
SDone Sing '[] -> Sing '[ '[ 'K a]] -> Sing '[ '[], '[ 'K a]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` (Sing a -> Sing ('K a)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing a
a Sing ('K a) -> Sing '[] -> Sing '[ 'K a]
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
`SEt` Sing '[]
SDone) Sing '[ 'K a] -> Sing '[] -> Sing '[ '[ 'K a]]
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
`SPlus` Sing '[]
SVoid)
sUnMaybe :: Sing (HMaybe a) -> Sing a
sUnMaybe :: Sing (HMaybe a) -> Sing a
sUnMaybe (SData (STyApp (STyCon _) a) _) = Sing a
Sing b
a
sUnMaybe Sing (HMaybe a)
_ = String -> Sing a
forall a. HasCallStack => String -> a
error String
"sUnMaybe: the impossible happened"
sUnFun :: Sing (a ':-> b) -> (Sing a, Sing b)
sUnFun :: Sing (a ':-> b) -> (Sing a, Sing b)
sUnFun (SFun a b) = (Sing a
Sing a
a,Sing b
Sing b
b)
data instance Sing (a :: HakaruCon) where
STyCon :: !(Sing s) -> Sing ('TyCon s :: HakaruCon)
STyApp :: !(Sing a) -> !(Sing b) -> Sing (a ':@ b :: HakaruCon)
instance Eq (Sing (a :: HakaruCon)) where
== :: Sing a -> Sing a -> Bool
(==) = Sing a -> Sing a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Sing :: HakaruCon -> *) where
eq1 :: Sing i -> Sing i -> Bool
eq1 Sing i
x Sing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Sing i -> Sing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing i
x Sing i
y)
instance JmEq1 (Sing :: HakaruCon -> *) where
jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)
jmEq1 (STyCon s) (STyCon z) = Sing s -> Sing s -> Maybe (TypeEq s s)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
s Sing s
z Maybe (TypeEq s s)
-> (TypeEq s s -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq s s
Refl -> TypeEq ('TyCon s) ('TyCon s)
-> Maybe (TypeEq ('TyCon s) ('TyCon s))
forall a. a -> Maybe a
Just TypeEq ('TyCon s) ('TyCon s)
forall k (a :: k). TypeEq a a
Refl
jmEq1 (STyApp f a) (STyApp g b) =
Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
f Sing a
g Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl ->
Sing b -> Sing b -> Maybe (TypeEq b b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing b
a Sing b
b Maybe (TypeEq b b)
-> (TypeEq b b -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq b b
Refl ->
TypeEq (a ':@ b) (a ':@ b) -> Maybe (TypeEq (a ':@ b) (a ':@ b))
forall a. a -> Maybe a
Just TypeEq (a ':@ b) (a ':@ b)
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
_ Sing j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Show (Sing (a :: HakaruCon)) where
showsPrec :: Int -> Sing a -> ShowS
showsPrec = Int -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Sing a -> String
show = Sing a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Show1 (Sing :: HakaruCon -> *) where
showsPrec1 :: Int -> Sing i -> ShowS
showsPrec1 Int
p (STyCon s1) = Int -> String -> Sing s -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"STyCon" Sing s
s1
showsPrec1 Int
p (STyApp s1 s2) = Int -> String -> Sing a -> Sing b -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"STyApp" Sing a
s1 Sing b
s2
instance TL.KnownSymbol s => SingI ('TyCon s :: HakaruCon) where
sing :: Sing ('TyCon s)
sing = Sing s -> Sing ('TyCon s)
forall (s :: Symbol). Sing s -> Sing ('TyCon s)
STyCon Sing s
forall k (a :: k). SingI a => Sing a
sing
instance (SingI a, SingI b) => SingI ((a ':@ b) :: HakaruCon) where
sing :: Sing (a ':@ b)
sing = Sing a -> Sing b -> Sing (a ':@ b)
forall (a :: HakaruCon) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':@ b)
STyApp Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
data instance Sing (s :: Symbol) where
SingSymbol :: TL.KnownSymbol s => Sing (s :: Symbol)
sSymbol_Bool :: Sing "Bool"
sSymbol_Bool :: Sing "Bool"
sSymbol_Bool = Sing "Bool"
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
sSymbol_Unit :: Sing "Unit"
sSymbol_Unit :: Sing "Unit"
sSymbol_Unit = Sing "Unit"
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
sSymbol_Pair :: Sing "Pair"
sSymbol_Pair :: Sing "Pair"
sSymbol_Pair = Sing "Pair"
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
sSymbol_Either :: Sing "Either"
sSymbol_Either :: Sing "Either"
sSymbol_Either = Sing "Either"
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
sSymbol_List :: Sing "List"
sSymbol_List :: Sing "List"
sSymbol_List = Sing "List"
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
sSymbol_Maybe :: Sing "Maybe"
sSymbol_Maybe :: Sing "Maybe"
sSymbol_Maybe = Sing "Maybe"
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
someSSymbol :: String -> (forall s . Sing (s :: Symbol) -> k) -> k
someSSymbol :: String -> (forall (s :: Symbol). Sing s -> k) -> k
someSSymbol String
s forall (s :: Symbol). Sing s -> k
k = case String -> SomeSymbol
TL.someSymbolVal String
s of { TL.SomeSymbol (Proxy n
_::Proxy s) -> Sing n -> k
forall (s :: Symbol). Sing s -> k
k (Sing n
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol :: Sing s) }
ssymbolVal :: forall s. Sing (s :: Symbol) -> String
ssymbolVal :: Sing s -> String
ssymbolVal Sing s
SingSymbol = Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
TL.symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s)
instance Eq (Sing (s :: Symbol)) where
== :: Sing s -> Sing s -> Bool
(==) = Sing s -> Sing s -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Sing :: Symbol -> *) where
eq1 :: Sing i -> Sing i -> Bool
eq1 Sing i
x Sing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Sing i -> Sing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing i
x Sing i
y)
instance JmEq1 (Sing :: Symbol -> *) where
jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)
jmEq1 x :: Sing i
x@Sing i
SingSymbol y :: Sing j
y@Sing j
SingSymbol
| Sing i -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
TL.symbolVal Sing i
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Sing j -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
TL.symbolVal Sing j
y = TypeEq i j -> Maybe (TypeEq i j)
forall a. a -> Maybe a
Just (TypeEq Any Any -> TypeEq i j
forall a b. a -> b
unsafeCoerce TypeEq Any Any
forall k (a :: k). TypeEq a a
Refl)
| Bool
otherwise = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Show (Sing (s :: Symbol)) where
showsPrec :: Int -> Sing s -> ShowS
showsPrec = Int -> Sing s -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Sing s -> String
show = Sing s -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Show1 (Sing :: Symbol -> *) where
showsPrec1 :: Int -> Sing i -> ShowS
showsPrec1 Int
_ s :: Sing i
s@Sing i
SingSymbol =
Bool -> ShowS -> ShowS
showParen Bool
True
( String -> ShowS
showString String
"SingSymbol :: Sing "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (ShowS
forall a. Show a => a -> String
show ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Sing i -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
TL.symbolVal Sing i
s)
)
instance TL.KnownSymbol s => SingI (s :: Symbol) where
sing :: Sing s
sing = Sing s
forall (s :: Symbol). KnownSymbol s => Sing s
SingSymbol
data instance Sing (a :: [[HakaruFun]]) where
SVoid :: Sing ('[] :: [[HakaruFun]])
SPlus
:: !(Sing xs)
-> !(Sing xss)
-> Sing ((xs ': xss) :: [[HakaruFun]])
instance Eq (Sing (a :: [[HakaruFun]])) where
== :: Sing a -> Sing a -> Bool
(==) = Sing a -> Sing a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Sing :: [[HakaruFun]] -> *) where
eq1 :: Sing i -> Sing i -> Bool
eq1 Sing i
x Sing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Sing i -> Sing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing i
x Sing i
y)
instance JmEq1 (Sing :: [[HakaruFun]] -> *) where
jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)
jmEq1 Sing i
SVoid Sing j
SVoid = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SPlus x xs) (SPlus y ys) =
Sing xs -> Sing xs -> Maybe (TypeEq xs xs)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing xs
x Sing xs
y Maybe (TypeEq xs xs)
-> (TypeEq xs xs -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq xs xs
Refl ->
Sing xss -> Sing xss -> Maybe (TypeEq xss xss)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing xss
xs Sing xss
ys Maybe (TypeEq xss xss)
-> (TypeEq xss xss -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq xss xss
Refl ->
TypeEq (xs : xss) (xs : xss)
-> Maybe (TypeEq (xs : xss) (xs : xss))
forall a. a -> Maybe a
Just TypeEq (xs : xss) (xs : xss)
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
_ Sing j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Show (Sing (a :: [[HakaruFun]])) where
showsPrec :: Int -> Sing a -> ShowS
showsPrec = Int -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Sing a -> String
show = Sing a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Show1 (Sing :: [[HakaruFun]] -> *) where
showsPrec1 :: Int -> Sing i -> ShowS
showsPrec1 Int
_ Sing i
SVoid = String -> ShowS
showString String
"SVoid"
showsPrec1 Int
p (SPlus s1 s2) = Int -> String -> Sing xs -> Sing xss -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"SPlus" Sing xs
s1 Sing xss
s2
instance SingI ('[] :: [[HakaruFun]]) where
sing :: Sing '[]
sing = Sing '[]
SVoid
instance (SingI xs, SingI xss) => SingI ((xs ': xss) :: [[HakaruFun]]) where
sing :: Sing (xs : xss)
sing = Sing xs -> Sing xss -> Sing (xs : xss)
forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]).
Sing xs -> Sing xss -> Sing (xs : xss)
SPlus Sing xs
forall k (a :: k). SingI a => Sing a
sing Sing xss
forall k (a :: k). SingI a => Sing a
sing
data instance Sing (a :: [HakaruFun]) where
SDone :: Sing ('[] :: [HakaruFun])
SEt :: !(Sing x) -> !(Sing xs) -> Sing ((x ': xs) :: [HakaruFun])
instance Eq (Sing (a :: [HakaruFun])) where
== :: Sing a -> Sing a -> Bool
(==) = Sing a -> Sing a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Sing :: [HakaruFun] -> *) where
eq1 :: Sing i -> Sing i -> Bool
eq1 Sing i
x Sing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Sing i -> Sing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing i
x Sing i
y)
instance JmEq1 (Sing :: [HakaruFun] -> *) where
jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)
jmEq1 Sing i
SDone Sing j
SDone = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SEt x xs) (SEt y ys) =
Sing x -> Sing x -> Maybe (TypeEq x x)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing x
x Sing x
y Maybe (TypeEq x x)
-> (TypeEq x x -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq x x
Refl ->
Sing xs -> Sing xs -> Maybe (TypeEq xs xs)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing xs
xs Sing xs
ys Maybe (TypeEq xs xs)
-> (TypeEq xs xs -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq xs xs
Refl ->
TypeEq (x : xs) (x : xs) -> Maybe (TypeEq (x : xs) (x : xs))
forall a. a -> Maybe a
Just TypeEq (x : xs) (x : xs)
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
_ Sing j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Show (Sing (a :: [HakaruFun])) where
showsPrec :: Int -> Sing a -> ShowS
showsPrec = Int -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Sing a -> String
show = Sing a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Show1 (Sing :: [HakaruFun] -> *) where
showsPrec1 :: Int -> Sing i -> ShowS
showsPrec1 Int
_ Sing i
SDone = String -> ShowS
showString String
"SDone"
showsPrec1 Int
p (SEt s1 s2) = Int -> String -> Sing x -> Sing xs -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"SEt" Sing x
s1 Sing xs
s2
instance SingI ('[] :: [HakaruFun]) where
sing :: Sing '[]
sing = Sing '[]
SDone
instance (SingI x, SingI xs) => SingI ((x ': xs) :: [HakaruFun]) where
sing :: Sing (x : xs)
sing = Sing x -> Sing xs -> Sing (x : xs)
forall (x :: HakaruFun) (xs :: [HakaruFun]).
Sing x -> Sing xs -> Sing (x : xs)
SEt Sing x
forall k (a :: k). SingI a => Sing a
sing Sing xs
forall k (a :: k). SingI a => Sing a
sing
data instance Sing (a :: HakaruFun) where
SIdent :: Sing 'I
SKonst :: !(Sing a) -> Sing ('K a)
instance Eq (Sing (a :: HakaruFun)) where
== :: Sing a -> Sing a -> Bool
(==) = Sing a -> Sing a -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Sing :: HakaruFun -> *) where
eq1 :: Sing i -> Sing i -> Bool
eq1 Sing i
x Sing i
y = Bool -> (TypeEq i i -> Bool) -> Maybe (TypeEq i i) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> TypeEq i i -> Bool
forall a b. a -> b -> a
const Bool
True) (Sing i -> Sing i -> Maybe (TypeEq i i)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing i
x Sing i
y)
instance JmEq1 (Sing :: HakaruFun -> *) where
jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)
jmEq1 Sing i
SIdent Sing j
SIdent = TypeEq i i -> Maybe (TypeEq i i)
forall a. a -> Maybe a
Just TypeEq i i
forall k (a :: k). TypeEq a a
Refl
jmEq1 (SKonst a) (SKonst b) = Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing a
b Maybe (TypeEq a a)
-> (TypeEq a a -> Maybe (TypeEq i j)) -> Maybe (TypeEq i j)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a a
Refl -> TypeEq ('K a) ('K a) -> Maybe (TypeEq ('K a) ('K a))
forall a. a -> Maybe a
Just TypeEq ('K a) ('K a)
forall k (a :: k). TypeEq a a
Refl
jmEq1 Sing i
_ Sing j
_ = Maybe (TypeEq i j)
forall a. Maybe a
Nothing
instance Show (Sing (a :: HakaruFun)) where
showsPrec :: Int -> Sing a -> ShowS
showsPrec = Int -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: Sing a -> String
show = Sing a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
instance Show1 (Sing :: HakaruFun -> *) where
showsPrec1 :: Int -> Sing i -> ShowS
showsPrec1 Int
_ Sing i
SIdent = String -> ShowS
showString String
"SIdent"
showsPrec1 Int
p (SKonst s1) = Int -> String -> Sing a -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"SKonst" Sing a
s1
instance SingI 'I where
sing :: Sing 'I
sing = Sing 'I
SIdent
instance (SingI a) => SingI ('K a) where
sing :: Sing ('K a)
sing = Sing a -> Sing ('K a)
forall (a :: Hakaru). Sing a -> Sing ('K a)
SKonst Sing a
forall k (a :: k). SingI a => Sing a
sing