{-# LANGUAGE DataKinds
           , PolyKinds
           , TypeOperators
           , GADTs
           , TypeFamilies
           , FlexibleInstances
           , Rank2Types
           , UndecidableInstances
           , ScopedTypeVariables
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.05.28
-- |
-- Module      :  Language.Hakaru.Types.Sing
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Singleton types for the @Hakaru@ kind, and a decision procedure
-- for @Hakaru@ type-equality.
----------------------------------------------------------------
module Language.Hakaru.Types.Sing
    ( Sing(..)
    , SingI(..), singOf
    -- * Some helpful shorthands for \"built-in\" datatypes
    -- ** Constructing singletons
    , sBool
    , sUnit
    , sPair
    , sEither
    , sList
    , sMaybe
    -- ** Destructing singletons
    , sUnMeasure
    , sUnArray
    , sUnPair, sUnPair'
    , sUnEither, sUnEither'
    , sUnList
    , sUnMaybe
    , sUnFun
    -- ** Singletons for `Symbol`
    , someSSymbol, ssymbolVal
    , sSymbol_Bool
    , sSymbol_Unit
    , sSymbol_Pair
    , sSymbol_Either
    , sSymbol_List
    , sSymbol_Maybe
    ) where

import qualified GHC.TypeLits as TL
-- TODO: should we use @(Data.Type.Equality.:~:)@ everywhere instead of our own 'TypeEq'?
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`


-- | The data families of singletons for each kind.
data family Sing (a :: k) :: *


-- | A class for automatically generating the singleton for a given
-- Hakaru type.
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

{-
-- TODO: we'd much rather have something like this, to prove that
-- we have a SingI instance for /every/ @a :: Hakaru@. Is there any
-- possible way of actually doing this?

class SingI1 (kproxy :: KProxy k) where
    sing1 :: Sing (a :: k)
    -- or, if it helps at all:
    -- > sing1 :: forall (a :: k). proxy a -> Sing a

instance SingI1 ('KProxy :: KProxy Hakaru) where
    sing1 = undefined
-}

----------------------------------------------------------------
-- BUG: data family instances must be fully saturated, but since
-- these are GADTs, the name of the parameter is irrelevant. However,
-- using a wildcard causes GHC to panic. cf.,
-- <https://ghc.haskell.org/trac/ghc/ticket/10586>

-- | Singleton types for the kind of Hakaru types. We need to use
-- this instead of 'Proxy' in order to implement 'jmEq1'.
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)
    -- TODO: would it be clearer to use (:$->) in order to better mirror the type-level (:->)
    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


-- TODO: instance Read (Sing (a :: Hakaru))


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
-- N.B., must use @(~)@ to delay the use of the type family (it's illegal to put it inline in the instance head).
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

-- These aren't pattern synonyms (cf., the problems mentioned
-- elsewhere about those), but they're helpful for generating
-- singletons at least.
-- TODO: we might be able to use 'singByProxy' to generate singletons
-- for Symbols? Doesn't work in pattern synonyms, of course.
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)

-- BUG: what does this "Conflicting definitions for ‘a’" message mean when we try to make this a pattern synonym?
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


-- TODO: instance Read (Sing (a :: HakaruCon))


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


----------------------------------------------------------------
-- | N.B., in order to bring the 'TL.KnownSymbol' dictionary into
-- scope, you need to pattern match on the 'SingSymbol' constructor
-- (similar to when we need to match on 'Refl' explicitly). In
-- general you'll want to do this with an at-pattern so that you
-- can also have a variable name for passing the value around (e.g.
-- to be used as an argument to 'TL.symbolVal').
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

-- TODO: is any meaningful Read (Sing (a :: Symbol)) instance possible?

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)
            )

-- Alas, this requires UndecidableInstances
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


-- TODO: instance Read (Sing (a :: [[HakaruFun]]))


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


-- TODO: instance Read (Sing (a :: [HakaruFun]))


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


-- TODO: instance Read (Sing (a :: HakaruFun))


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

----------------------------------------------------------------
----------------------------------------------------------- fin.