-- SPDX-FileCopyrightText: 2023 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# 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(..))

{-$setup
>>> import Morley.Michelson.Typed
>>> import Fmt (pretty)
-}

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"

-- | This class encodes Michelson rules w.r.t where it requires comparable
-- types. Earlier we had a dedicated type for representing comparable types @CT@.
-- But then we integreated those types into @T@. This meant that some of the
-- types that could be formed with various combinations of @T@ would be
-- illegal as per Michelson typing rule. Using this class, we inductively
-- enforce that a type and all types it contains are well typed as per
-- Michelson's rules.
type WellTyped :: T -> Constraint
class (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t
instance (SingI t, RecSuperC WellTyped t, WellTypedConstraints t) => WellTyped t

-- | Additional (non-recursive) constraints on type arguments for specific types
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 _ = ()

-- | Error type for when a value is not well-typed.
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

{- | Given a type, provide evidence that it is well typed w.r.t to the Michelson
rules regarding where comparable types are required.

>>> either pretty print $ getWTP @'TUnit
Dict
>>> either pretty print $ getWTP @('TSet 'TOperation)
Given type is not well typed because 'operation' is not comparable
>>> type Pairs a = 'TPair a a
>>> type Pairs2 = Pairs (Pairs 'TUnit)
>>> either pretty print $ getWTP @('TSet ('TPair Pairs2 'TOperation))
Given type is not well typed because
  pair (pair (pair unit unit) unit unit) operation
is not comparable
-}
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

-- | Version of 'getWTP' that accepts 'Sing' at term-level.
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