{-# OPTIONS_HADDOCK not-home #-}
module Morley.Michelson.Typed.Scope.Internal.WellTyped
( module Morley.Michelson.Typed.Scope.Internal.WellTyped
) where
import Data.Constraint (Dict(..))
import Data.Singletons (Sing, SingI(..), fromSing, withSingI)
import Data.Type.Equality ((:~:)(..))
import Fmt (Buildable(..), quoteOrIndentF, (++|), (|++^))
import Morley.Michelson.Typed.Scope.Internal.Comparable
import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Scope.Internal.Presence
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
data BadTypeForScope
= BtNotComparable
| BtIsOperation
| BtHasBigMap
| BtHasNestedBigMap
| BtHasContract
| BtHasTicket
| BtHasSaplingState
deriving stock (Int -> BadTypeForScope -> ShowS
[BadTypeForScope] -> ShowS
BadTypeForScope -> String
(Int -> BadTypeForScope -> ShowS)
-> (BadTypeForScope -> String)
-> ([BadTypeForScope] -> ShowS)
-> Show BadTypeForScope
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BadTypeForScope -> ShowS
showsPrec :: Int -> BadTypeForScope -> ShowS
$cshow :: BadTypeForScope -> String
show :: BadTypeForScope -> String
$cshowList :: [BadTypeForScope] -> ShowS
showList :: [BadTypeForScope] -> ShowS
Show, BadTypeForScope -> BadTypeForScope -> Bool
(BadTypeForScope -> BadTypeForScope -> Bool)
-> (BadTypeForScope -> BadTypeForScope -> Bool)
-> Eq BadTypeForScope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BadTypeForScope -> BadTypeForScope -> Bool
== :: BadTypeForScope -> BadTypeForScope -> Bool
$c/= :: BadTypeForScope -> BadTypeForScope -> Bool
/= :: BadTypeForScope -> BadTypeForScope -> Bool
Eq, (forall x. BadTypeForScope -> Rep BadTypeForScope x)
-> (forall x. Rep BadTypeForScope x -> BadTypeForScope)
-> Generic BadTypeForScope
forall x. Rep BadTypeForScope x -> BadTypeForScope
forall x. BadTypeForScope -> Rep BadTypeForScope x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BadTypeForScope -> Rep BadTypeForScope x
from :: forall x. BadTypeForScope -> Rep BadTypeForScope x
$cto :: forall x. Rep BadTypeForScope x -> BadTypeForScope
to :: forall x. Rep BadTypeForScope x -> BadTypeForScope
Generic)
deriving anyclass (BadTypeForScope -> ()
(BadTypeForScope -> ()) -> NFData BadTypeForScope
forall a. (a -> ()) -> NFData a
$crnf :: BadTypeForScope -> ()
rnf :: BadTypeForScope -> ()
NFData)
instance Buildable BadTypeForScope where
build :: BadTypeForScope -> Doc
build = \case
BadTypeForScope
BtNotComparable -> Doc
"is not comparable"
BadTypeForScope
BtIsOperation -> Doc
"has 'operation' type"
BadTypeForScope
BtHasBigMap -> Doc
"has 'big_map'"
BadTypeForScope
BtHasNestedBigMap -> Doc
"has nested 'big_map'"
BadTypeForScope
BtHasContract -> Doc
"has 'contract' type"
BadTypeForScope
BtHasTicket -> Doc
"has 'ticket' type"
BadTypeForScope
BtHasSaplingState -> Doc
"has 'sapling_state' type"
type WellTyped :: T -> Constraint
class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t
instance (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t
type WellTypedConstraints :: T -> Constraint
type family WellTypedConstraints t where
WellTypedConstraints ('TSet t) = Comparable t
WellTypedConstraints ('TContract t) = (ForbidOp t, ForbidNestedBigMaps t)
WellTypedConstraints ('TTicket t) = Comparable t
WellTypedConstraints ('TMap k _) = Comparable k
WellTypedConstraints ('TBigMap k v) = (Comparable k, ForbidBigMap v, ForbidOp v)
WellTypedConstraints _ = ()
data NotWellTyped = NotWellTyped
{ NotWellTyped -> T
nwtBadType :: T
, NotWellTyped -> BadTypeForScope
nwtCause :: BadTypeForScope
}
instance Buildable NotWellTyped where
build :: NotWellTyped -> Doc
build (NotWellTyped T
t BadTypeForScope
c) =
Text
"Given type is not well typed because" Text -> ReflowingDoc -> Doc
forall b. FromDoc b => Text -> ReflowingDoc -> b
++| T -> Doc
forall a. Buildable a => a -> Doc
quoteOrIndentF T
t Doc -> Doc -> ReflowingDoc
forall a. Buildable a => a -> Doc -> ReflowingDoc
|++^ BadTypeForScope -> Doc
forall a. Buildable a => a -> Doc
build BadTypeForScope
c
getWTP :: forall t. (SingI t) => Either NotWellTyped (Dict (WellTyped t))
getWTP :: forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP = Sing t -> Either NotWellTyped (Dict (WellTyped t))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing t
forall {k} (a :: k). SingI a => Sing a
sing
getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' :: forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' = \case
Sing t
SingT t
STKey -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STUnit -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STSignature -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STChainId -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STOption Sing n
s -> do
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STList Sing n
s -> do
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STSet Sing n
s -> do
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
Dict (Comparable n)
Dict <- BadTypeForScope
-> SingT n
-> (SingT n -> Maybe (Dict (Comparable n)))
-> Either NotWellTyped (Dict (Comparable n))
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n
SingT n
s Sing n -> Maybe (Dict (Comparable n))
SingT n -> Maybe (Dict (Comparable n))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STOperation -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STContract Sing n
s -> do
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
ContainsT 'PSOp n :~: 'False
Refl <- BadTypeForScope
-> SingT n
-> (SingT n -> Maybe (ContainsT 'PSOp n :~: 'False))
-> Either NotWellTyped (ContainsT 'PSOp n :~: 'False)
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtIsOperation Sing n
SingT n
s ((SingT n -> Maybe (ContainsT 'PSOp n :~: 'False))
-> Either NotWellTyped (ContainsT 'PSOp n :~: 'False))
-> (SingT n -> Maybe (ContainsT 'PSOp n :~: 'False))
-> Either NotWellTyped (ContainsT 'PSOp n :~: 'False)
forall a b. (a -> b) -> a -> b
$ Sing 'PSOp -> Sing n -> Maybe (ContainsT 'PSOp n :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp
ContainsT 'PSNestedBigMaps n :~: 'False
Refl <- BadTypeForScope
-> SingT n
-> (SingT n -> Maybe (ContainsT 'PSNestedBigMaps n :~: 'False))
-> Either NotWellTyped (ContainsT 'PSNestedBigMaps n :~: 'False)
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtHasNestedBigMap Sing n
SingT n
s ((SingT n -> Maybe (ContainsT 'PSNestedBigMaps n :~: 'False))
-> Either NotWellTyped (ContainsT 'PSNestedBigMaps n :~: 'False))
-> (SingT n -> Maybe (ContainsT 'PSNestedBigMaps n :~: 'False))
-> Either NotWellTyped (ContainsT 'PSNestedBigMaps n :~: 'False)
forall a b. (a -> b) -> a -> b
$ Sing 'PSNestedBigMaps
-> Sing n -> Maybe (ContainsT 'PSNestedBigMaps n :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSNestedBigMaps
SingTPredicateSym 'PSNestedBigMaps
SPSNestedBigMaps
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STTicket Sing n
s -> do
Dict (WellTyped n)
Dict <- Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n
s
Dict (Comparable n)
Dict <- BadTypeForScope
-> SingT n
-> (SingT n -> Maybe (Dict (Comparable n)))
-> Either NotWellTyped (Dict (Comparable n))
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n
SingT n
s Sing n -> Maybe (Dict (Comparable n))
SingT n -> Maybe (Dict (Comparable n))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STPair Sing n1
s1 Sing n2
s2 -> do
Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STOr Sing n1
s1 Sing n2
s2 -> do
Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STLambda Sing n1
s1 Sing n2
s2 -> do
Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STMap Sing n1
s1 Sing n2
s2 -> do
Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
Dict (Comparable n1)
Dict <- BadTypeForScope
-> SingT n1
-> (SingT n1 -> Maybe (Dict (Comparable n1)))
-> Either NotWellTyped (Dict (Comparable n1))
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n1
SingT n1
s1 Sing n1 -> Maybe (Dict (Comparable n1))
SingT n1 -> Maybe (Dict (Comparable n1))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STBigMap Sing n1
s1 Sing n2
s2 -> do
Dict (WellTyped n1)
Dict <- Sing n1 -> Either NotWellTyped (Dict (WellTyped n1))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n1
s1
Dict (WellTyped n2)
Dict <- Sing n2 -> Either NotWellTyped (Dict (WellTyped n2))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP' Sing n2
s2
Dict (Comparable n1)
Dict <- BadTypeForScope
-> SingT n1
-> (SingT n1 -> Maybe (Dict (Comparable n1)))
-> Either NotWellTyped (Dict (Comparable n1))
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtNotComparable Sing n1
SingT n1
s1 ((SingT n1 -> Maybe (Dict (Comparable n1)))
-> Either NotWellTyped (Dict (Comparable n1)))
-> (SingT n1 -> Maybe (Dict (Comparable n1)))
-> Either NotWellTyped (Dict (Comparable n1))
forall a b. (a -> b) -> a -> b
$ Sing n1 -> Maybe (Dict (Comparable n1))
SingT n1 -> Maybe (Dict (Comparable n1))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence
ContainsT 'PSOp n2 :~: 'False
Refl <- BadTypeForScope
-> SingT n2
-> (SingT n2 -> Maybe (ContainsT 'PSOp n2 :~: 'False))
-> Either NotWellTyped (ContainsT 'PSOp n2 :~: 'False)
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtIsOperation Sing n2
SingT n2
s2 ((SingT n2 -> Maybe (ContainsT 'PSOp n2 :~: 'False))
-> Either NotWellTyped (ContainsT 'PSOp n2 :~: 'False))
-> (SingT n2 -> Maybe (ContainsT 'PSOp n2 :~: 'False))
-> Either NotWellTyped (ContainsT 'PSOp n2 :~: 'False)
forall a b. (a -> b) -> a -> b
$ Sing 'PSOp -> Sing n2 -> Maybe (ContainsT 'PSOp n2 :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp
ContainsT 'PSBigMap n2 :~: 'False
Refl <- BadTypeForScope
-> SingT n2
-> (SingT n2 -> Maybe (ContainsT 'PSBigMap n2 :~: 'False))
-> Either NotWellTyped (ContainsT 'PSBigMap n2 :~: 'False)
forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
BtHasBigMap Sing n2
SingT n2
s2 ((SingT n2 -> Maybe (ContainsT 'PSBigMap n2 :~: 'False))
-> Either NotWellTyped (ContainsT 'PSBigMap n2 :~: 'False))
-> (SingT n2 -> Maybe (ContainsT 'PSBigMap n2 :~: 'False))
-> Either NotWellTyped (ContainsT 'PSBigMap n2 :~: 'False)
forall a b. (a -> b) -> a -> b
$ Sing 'PSBigMap
-> Sing n2 -> Maybe (ContainsT 'PSBigMap n2 :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
SPSBigMap
Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a. a -> Either NotWellTyped a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STInt -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STNat -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STString -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STBytes -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STMutez -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STBool -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STKeyHash -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STBls12381Fr -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STBls12381G1 -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STBls12381G2 -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STTimestamp -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STAddress -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STChest -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STChestKey -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
Sing t
SingT t
STNever -> Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STSaplingState Sing n
s -> Sing n
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t)))
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
STSaplingTransaction Sing n
s -> Sing n
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
s ((SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t)))
-> (SingI n => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
where
eitherWellTyped
:: BadTypeForScope
-> SingT t
-> (SingT t -> Maybe a)
-> Either NotWellTyped a
eitherWellTyped :: forall (t :: T) a.
BadTypeForScope
-> SingT t -> (SingT t -> Maybe a) -> Either NotWellTyped a
eitherWellTyped BadTypeForScope
bt SingT t
sng SingT t -> Maybe a
f = NotWellTyped -> Maybe a -> Either NotWellTyped a
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped (Sing t -> Demote T
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: T). Sing a -> Demote T
fromSing Sing t
SingT t
sng) BadTypeForScope
bt) (Maybe a -> Either NotWellTyped a)
-> Maybe a -> Either NotWellTyped a
forall a b. (a -> b) -> a -> b
$ SingT t -> Maybe a
f SingT t
sng