module Michelson.TypeCheck.Types
( HST (..)
, (-:&)
, pattern (::&+)
, SomeHST (..)
, SomeInstrOut (..)
, SomeInstr (..)
, BoundVars (..)
, TcExtFrames
, NotWellTyped (..)
, getWTP
, getWTP_
, withWTPm
, unsafeWithWTP
, mapSomeContract
, mapSomeInstr
, mapSomeInstrOut
, noBoundVars
) where
import Data.Constraint (Dict(..))
import qualified Data.Map.Lazy as Map
import Data.Singletons (Sing, SingI(..), demote, withSingI)
import Fmt (Buildable(..), pretty)
import Prelude hiding (EQ, GT, LT)
import qualified Text.Show
import Text.PrettyPrint.Leijen.Text hiding (pretty)
import Michelson.Typed (Notes(..), SingT(..), SomeContract(..), T(..), notesT, starNotes)
import qualified Michelson.Typed as T
import Michelson.Typed.Haskell.Value (WellTyped)
import Michelson.Typed.Instr
import Michelson.Printer.Util
import Michelson.Untyped (Ty, Var, noAnn)
import Michelson.Untyped.Annotation (VarAnn)
import Util.Sing (eqParamSing)
data HST (ts :: [T]) where
SNil :: HST '[]
(::&) :: (T.SingI x, T.SingI xs)
=> (Notes x, Dict (WellTyped x), VarAnn)
-> HST xs
-> HST (x ': xs)
instance NFData (HST ts) where
rnf :: HST ts -> ()
rnf (HST ts
SNil) = ()
rnf ((Notes x
a, Dict (WellTyped x)
d, VarAnn
b) ::& HST xs
hst) = (Notes x, Dict (WellTyped x), VarAnn, HST xs) -> ()
forall a. NFData a => a -> ()
rnf (Notes x
a, Dict (WellTyped x)
d, VarAnn
b, HST xs
hst)
instance Show (HST ts) where
show :: HST ts -> String
show HST ts
SNil = String
"[]"
show ((Notes x, Dict (WellTyped x), VarAnn)
r ::& HST xs
rs) = String
"[ " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> HST (x : xs) -> String
forall (t :: T) (ts_ :: [T]). HST (t : ts_) -> String
showDo ((Notes x, Dict (WellTyped x), VarAnn)
r (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" ]"
where
showDo :: HST (t ': ts_) -> String
showDo :: HST (t : ts_) -> String
showDo ((Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT -> T
t, Dict (WellTyped x)
Dict, VarAnn
_vn) ::& ((Notes x, Dict (WellTyped x), VarAnn)
b ::& HST xs
c)) =
T -> String
forall b a. (Show a, IsString b) => a -> b
show T
t String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> HST (x : xs) -> String
forall (t :: T) (ts_ :: [T]). HST (t : ts_) -> String
showDo ((Notes x, Dict (WellTyped x), VarAnn)
b (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
c)
showDo ((Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT -> T
t, Dict (WellTyped x)
Dict, VarAnn
_vn) ::& HST xs
SNil) = T -> String
forall b a. (Show a, IsString b) => a -> b
show T
t
instance Buildable (HST ts) where
build :: HST ts -> Builder
build = HST ts -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDocExtended
instance RenderDoc (HST ts) where
renderDoc :: RenderContext -> HST ts -> Doc
renderDoc RenderContext
_ HST ts
SNil = Doc
"[]"
renderDoc RenderContext
context ((Notes x, Dict (WellTyped x), VarAnn)
r ::& HST xs
rs) = Doc
"[" Doc -> Doc -> Doc
<+> HST (x : xs) -> Doc
forall (t :: T) (ts_ :: [T]). HST (t : ts_) -> Doc
doRender ((Notes x, Dict (WellTyped x), VarAnn)
r (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs) Doc -> Doc -> Doc
<+> Doc
"]"
where
doRender :: HST (t ': ts_) -> Doc
doRender :: HST (t : ts_) -> Doc
doRender ((Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT -> T
t, Dict (WellTyped x)
Dict, VarAnn
_vn) ::& ((Notes x, Dict (WellTyped x), VarAnn)
b ::& HST xs
c)) =
RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
t Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"," Doc -> Doc -> Doc
<+> HST (x : xs) -> Doc
forall (t :: T) (ts_ :: [T]). HST (t : ts_) -> Doc
doRender ((Notes x, Dict (WellTyped x), VarAnn)
b (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
c)
doRender ((Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT -> T
t, Dict (WellTyped x)
Dict, VarAnn
_vn) ::& HST xs
SNil) = RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
t
infixr 7 ::&
instance Eq (HST ts) where
HST ts
SNil == :: HST ts -> HST ts -> Bool
== HST ts
SNil = Bool
True
(Notes x
n1, Dict (WellTyped x)
Dict, VarAnn
a1) ::& HST xs
h1 == (Notes x
n2, Dict (WellTyped x)
Dict, VarAnn
a2) ::& HST xs
h2 =
Notes x
n1 Notes x -> Notes x -> Bool
forall a. Eq a => a -> a -> Bool
== Notes x
Notes x
n2 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& VarAnn
a1 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
a2 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& HST xs
h1 HST xs -> HST xs -> Bool
forall a. Eq a => a -> a -> Bool
== HST xs
HST xs
h2
(-:&)
:: (WellTyped x, SingI xs)
=> Sing x
-> HST xs
-> HST (x ': xs)
Sing x
_ -:& :: Sing x -> HST xs -> HST (x : xs)
-:& HST xs
hst = (Notes x
forall (t :: T). SingI t => Notes t
starNotes, Dict (WellTyped x)
forall (a :: Constraint). a => Dict a
Dict, VarAnn
forall k (a :: k). Annotation a
noAnn) (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hst
infixr 7 -:&
infixr 7 ::&+
pattern (::&+)
:: ()
=> ( ys ~ (x ': xs)
, SingI x, SingI xs
)
=> (Sing x, Notes x, Dict (WellTyped x), VarAnn)
-> HST xs
-> HST ys
pattern x $b::&+ :: (Sing x, Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST ys
$m::&+ :: forall r (ys :: [T]).
HST ys
-> (forall (x :: T) (xs :: [T]).
(ys ~ (x : xs), SingI x, SingI xs) =>
(Sing x, Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> r)
-> (Void# -> r)
-> r
::&+ hst <- ((\(n, d, v) -> (T.notesSing n, n, d, v)) -> x) ::& hst
where (Sing x
_, Notes x
n, Dict (WellTyped x)
d, VarAnn
v) ::&+ HST xs
hst = (Notes x
n, Dict (WellTyped x)
d, VarAnn
v) (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (x :: T) (xs :: [T]).
(SingI x, SingI xs) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
hst
data SomeHST where
SomeHST :: SingI ts => HST ts -> SomeHST
deriving stock instance Show SomeHST
instance NFData SomeHST where
rnf :: SomeHST -> ()
rnf (SomeHST HST ts
h) = HST ts -> ()
forall a. NFData a => a -> ()
rnf HST ts
h
instance Eq SomeHST where
SomeHST HST ts
hst1 == :: SomeHST -> SomeHST -> Bool
== SomeHST HST ts
hst2 = HST ts
hst1 HST ts -> HST ts -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` HST ts
hst2
data SomeInstrOut inp where
(:::)
:: SingI out
=> Instr inp out
-> HST out
-> SomeInstrOut inp
AnyOutInstr
:: (forall out. Instr inp out)
-> SomeInstrOut inp
infix 9 :::
instance Show (ExtInstr inp) => Show (SomeInstrOut inp) where
show :: SomeInstrOut inp -> String
show (Instr inp out
i ::: HST out
out) = Instr inp out -> String
forall b a. (Show a, IsString b) => a -> b
show Instr inp out
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" :: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> HST out -> String
forall b a. (Show a, IsString b) => a -> b
show HST out
out
show (AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp Any -> String
forall b a. (Show a, IsString b) => a -> b
show Instr inp Any
forall (out :: [T]). Instr inp out
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" :: *"
data SomeInstr inp where
(:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp
infix 8 :/
mapSomeInstrOut
:: (forall out. Instr inp out -> Instr inp' out)
-> SomeInstrOut inp
-> SomeInstrOut inp'
mapSomeInstrOut :: (forall (out :: [T]). Instr inp out -> Instr inp' out)
-> SomeInstrOut inp -> SomeInstrOut inp'
mapSomeInstrOut forall (out :: [T]). Instr inp out -> Instr inp' out
f (Instr inp out
i ::: HST out
out) = Instr inp out -> Instr inp' out
forall (out :: [T]). Instr inp out -> Instr inp' out
f Instr inp out
i Instr inp' out -> HST out -> SomeInstrOut inp'
forall (out :: [T]) (inp :: [T]).
SingI out =>
Instr inp out -> HST out -> SomeInstrOut inp
::: HST out
out
mapSomeInstrOut forall (out :: [T]). Instr inp out -> Instr inp' out
f (AnyOutInstr forall (out :: [T]). Instr inp out
i) = (forall (out :: [T]). Instr inp' out) -> SomeInstrOut inp'
forall (inp :: [T]).
(forall (out :: [T]). Instr inp out) -> SomeInstrOut inp
AnyOutInstr (Instr inp out -> Instr inp' out
forall (out :: [T]). Instr inp out -> Instr inp' out
f Instr inp out
forall (out :: [T]). Instr inp out
i)
mapSomeInstr
:: (forall out. Instr inp out -> Instr inp out)
-> SomeInstr inp
-> SomeInstr inp
mapSomeInstr :: (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstr inp -> SomeInstr inp
mapSomeInstr forall (out :: [T]). Instr inp out -> Instr inp out
f (HST inp
inp :/ SomeInstrOut inp
instrAndOut) = HST inp
inp HST inp -> SomeInstrOut inp -> SomeInstr inp
forall (inp :: [T]). HST inp -> SomeInstrOut inp -> SomeInstr inp
:/ (forall (out :: [T]). Instr inp out -> Instr inp out)
-> SomeInstrOut inp -> SomeInstrOut inp
forall (inp :: [T]) (inp' :: [T]).
(forall (out :: [T]). Instr inp out -> Instr inp' out)
-> SomeInstrOut inp -> SomeInstrOut inp'
mapSomeInstrOut forall (out :: [T]). Instr inp out -> Instr inp out
f SomeInstrOut inp
instrAndOut
instance Show (ExtInstr inp) => Show (SomeInstr inp) where
show :: SomeInstr inp -> String
show (HST inp
inp :/ SomeInstrOut inp
out) = HST inp -> String
forall b a. (Show a, IsString b) => a -> b
show HST inp
inp String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" -> " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> SomeInstrOut inp -> String
forall b a. (Show a, IsString b) => a -> b
show SomeInstrOut inp
out
mapSomeContract ::
(forall inp out. Instr inp out -> Instr inp out)
-> SomeContract
-> SomeContract
mapSomeContract :: (forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out)
-> SomeContract -> SomeContract
mapSomeContract forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
f (SomeContract Contract cp st
fc) = Contract cp st -> SomeContract
forall (cp :: T) (st :: T). Contract cp st -> SomeContract
SomeContract (Contract cp st -> SomeContract) -> Contract cp st -> SomeContract
forall a b. (a -> b) -> a -> b
$ (ContractCode cp st -> ContractCode cp st)
-> Contract cp st -> Contract cp st
forall (cp :: T) (st :: T).
(ContractCode cp st -> ContractCode cp st)
-> Contract cp st -> Contract cp st
mapContractCode ContractCode cp st -> ContractCode cp st
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
f Contract cp st
fc
data BoundVars = BoundVars (Map Var Ty) (Maybe SomeHST)
noBoundVars :: BoundVars
noBoundVars :: BoundVars
noBoundVars = Map Var Ty -> Maybe SomeHST -> BoundVars
BoundVars Map Var Ty
forall k a. Map k a
Map.empty Maybe SomeHST
forall a. Maybe a
Nothing
type TcExtFrames = [BoundVars]
data NotWellTyped = NotWellTyped
{ NotWellTyped -> T
nwtBadType :: T
, NotWellTyped -> BadTypeForScope
nwtCause :: T.BadTypeForScope
}
instance Buildable NotWellTyped where
build :: NotWellTyped -> Builder
build (NotWellTyped T
t BadTypeForScope
c) =
Builder
"Given type is not well typed because '" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (T -> Builder
forall p. Buildable p => p -> Builder
build T
t) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"' " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (BadTypeForScope -> Builder
forall p. Buildable p => p -> Builder
build BadTypeForScope
c)
fromEDict :: Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict :: Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict Either e (Dict a)
ma a => Either e (Dict b)
b = Either e (Dict a)
ma Either e (Dict a)
-> (Dict a -> Either e (Dict b)) -> Either e (Dict b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Dict a
Dict -> Either e (Dict b)
a => Either e (Dict b)
b)
getWTP :: forall t. (SingI t) => Either NotWellTyped (Dict (WellTyped t))
getWTP :: Either NotWellTyped (Dict (WellTyped t))
getWTP = case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t of
Sing 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
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
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
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 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
$ Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TOption n))))
-> Either NotWellTyped (Dict (WellTyped ('TOption n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s) (Dict (WellTyped ('TOption n))
-> Either NotWellTyped (Dict (WellTyped ('TOption n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TOption n))
forall (a :: Constraint). a => Dict a
Dict)
STList 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
$ Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TList n))))
-> Either NotWellTyped (Dict (WellTyped ('TList n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s) (Dict (WellTyped ('TList n))
-> Either NotWellTyped (Dict (WellTyped ('TList n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TList n))
forall (a :: Constraint). a => Dict a
Dict)
STSet (s :: Sing si) ->
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
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> Either NotWellTyped (Dict (WellTyped ('TSet n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s) ((WellTyped n => Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> Either NotWellTyped (Dict (WellTyped ('TSet n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (Comparable n))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> Either NotWellTyped (Dict (WellTyped ('TSet n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) BadTypeForScope
T.BtNotComparable) (Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n)))
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (Comparable n))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing n
s
) ((Comparable n => Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TSet n))))
-> Either NotWellTyped (Dict (WellTyped ('TSet n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TSet n))
-> Either NotWellTyped (Dict (WellTyped ('TSet n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TSet n))
forall (a :: Constraint). a => Dict a
Dict
Sing 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 (s :: Sing si) ->
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
$ Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> Either NotWellTyped (Dict (WellTyped ('TContract n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> Either NotWellTyped (Dict (WellTyped ('TContract n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (HasNoOp n))
-> (HasNoOp n =>
Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> Either NotWellTyped (Dict (WellTyped ('TContract n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (HasNoOp n))
-> Either NotWellTyped (Dict (HasNoOp n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) BadTypeForScope
T.BtIsOperation) (Maybe (Dict (HasNoOp n))
-> Either NotWellTyped (Dict (HasNoOp n)))
-> Maybe (Dict (HasNoOp n))
-> Either NotWellTyped (Dict (HasNoOp n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (HasNoOp n))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoOp t)
T.opAbsense Sing n
s
) ((HasNoOp n =>
Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> (HasNoOp n =>
Either NotWellTyped (Dict (WellTyped ('TContract n))))
-> Either NotWellTyped (Dict (WellTyped ('TContract n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TContract n))
-> Either NotWellTyped (Dict (WellTyped ('TContract n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TContract n))
forall (a :: Constraint). a => Dict a
Dict
STTicket (s :: Sing si) ->
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
$ Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (Comparable n))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) BadTypeForScope
T.BtNotComparable) (Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n)))
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (Comparable n))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing n
s
) ((Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TTicket n))))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TTicket n))
-> Either NotWellTyped (Dict (WellTyped ('TTicket n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TTicket n))
forall (a :: Constraint). a => Dict a
Dict
STPair s1 s2 ->
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
s1 ((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
$
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
s2 ((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
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s1) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s2) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TPair n n))))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TPair n n))
-> Either NotWellTyped (Dict (WellTyped ('TPair n n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TPair n n))
forall (a :: Constraint). a => Dict a
Dict
STOr s1 s2 ->
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
s1 ((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
$
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
s2 ((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
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s1) ((WellTyped n => Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s2) ((WellTyped n => Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TOr n n))))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TOr n n))
-> Either NotWellTyped (Dict (WellTyped ('TOr n n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TOr n n))
forall (a :: Constraint). a => Dict a
Dict
STLambda s1 s2 ->
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
s1 ((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
$
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
s2 ((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
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s1) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n)))
forall a b. (a -> b) -> a -> b
$ Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s2) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TLambda n n))))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TLambda n n))
-> Either NotWellTyped (Dict (WellTyped ('TLambda n n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TLambda n n))
forall (a :: Constraint). a => Dict a
Dict
STMap (s1 :: Sing si) s2 ->
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
s1 ((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
$
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
s2 ((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
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s1) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s2) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (Comparable n))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) BadTypeForScope
T.BtNotComparable) (Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n)))
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (Comparable n))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing n
s1
) ((Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TMap n n))
-> Either NotWellTyped (Dict (WellTyped ('TMap n n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TMap n n))
forall (a :: Constraint). a => Dict a
Dict
STBigMap (s1 :: Sing si) (s2 :: Sing si2) ->
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
s1 ((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
$
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
s2 ((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
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s1) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (WellTyped n))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing n -> Either NotWellTyped (Dict (WellTyped n))
forall (t :: T). Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing n
s2) ((WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> (WellTyped n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (Comparable n))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) BadTypeForScope
T.BtNotComparable) (Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n)))
-> Maybe (Dict (Comparable n))
-> Either NotWellTyped (Dict (Comparable n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (Comparable n))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing n
s1
) ((Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> (Comparable n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (HasNoOp n))
-> (HasNoOp n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (HasNoOp n))
-> Either NotWellTyped (Dict (HasNoOp n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si2) BadTypeForScope
T.BtIsOperation) (Maybe (Dict (HasNoOp n))
-> Either NotWellTyped (Dict (HasNoOp n)))
-> Maybe (Dict (HasNoOp n))
-> Either NotWellTyped (Dict (HasNoOp n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (HasNoOp n))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoOp t)
T.opAbsense Sing n
s2
) ((HasNoOp n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> (HasNoOp n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall a b. (a -> b) -> a -> b
$
Either NotWellTyped (Dict (HasNoBigMap n))
-> (HasNoBigMap n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
( NotWellTyped
-> Maybe (Dict (HasNoBigMap n))
-> Either NotWellTyped (Dict (HasNoBigMap n))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> BadTypeForScope -> NotWellTyped
NotWellTyped ((SingKind T, SingI n) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si2) BadTypeForScope
T.BtHasBigMap) (Maybe (Dict (HasNoBigMap n))
-> Either NotWellTyped (Dict (HasNoBigMap n)))
-> Maybe (Dict (HasNoBigMap n))
-> Either NotWellTyped (Dict (HasNoBigMap n))
forall a b. (a -> b) -> a -> b
$ Sing n -> Maybe (Dict (HasNoBigMap n))
forall (t :: T). Sing t -> Maybe (Dict $ HasNoBigMap t)
T.bigMapAbsense Sing n
s2
) ((HasNoBigMap n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> (HasNoBigMap n =>
Either NotWellTyped (Dict (WellTyped ('TBigMap n n))))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped ('TBigMap n n))
-> Either NotWellTyped (Dict (WellTyped ('TBigMap n n)))
forall a b. b -> Either a b
Right Dict (WellTyped ('TBigMap n n))
forall (a :: Constraint). a => Dict a
Dict
Sing 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
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
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
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
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
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
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
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
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
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
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
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
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
getWTP_ :: forall t. Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ :: Sing t -> Either NotWellTyped (Dict (WellTyped t))
getWTP_ Sing t
s = Sing t
-> (SingI t => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing t
s ((SingI t => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t)))
-> (SingI t => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ SingI t => Either NotWellTyped (Dict (WellTyped t))
forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t
withWTPm :: forall t m a. (MonadFail m, SingI t) => (WellTyped t => m a) -> m a
withWTPm :: (WellTyped t => m a) -> m a
withWTPm WellTyped t => m a
a = case SingI t => Either NotWellTyped (Dict (WellTyped t))
forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t of
Right Dict (WellTyped t)
Dict -> m a
WellTyped t => m a
a
Left NotWellTyped
e -> String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (NotWellTyped -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty NotWellTyped
e)
unsafeWithWTP :: forall t a. SingI t => (WellTyped t => a) -> a
unsafeWithWTP :: (WellTyped t => a) -> a
unsafeWithWTP WellTyped t => a
fn = case SingI t => Either NotWellTyped (Dict (WellTyped t))
forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t of
Right Dict (WellTyped t)
Dict -> a
WellTyped t => a
fn
Left NotWellTyped
e -> Text -> a
forall a. HasCallStack => Text -> a
error (Text -> a) -> Text -> a
forall a b. (a -> b) -> a -> b
$ NotWellTyped -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty NotWellTyped
e