-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

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 type holding type information for stack (Heterogeneous Stack Type).
--
-- This data type is used along with instruction data type @Instr@
-- to carry information about its input and output stack types.
--
-- That is, if there is value @instr :: Instr inp out@, along with this
-- @instr@ one may carry @inpHST :: HST inp@ and @outHST :: HST out@ which will
-- contain whole information about input and output stack types for @instr@.
--
-- Data type @HST@ is very similar to @Data.Vinyl.Rec@,
-- but is specialized for a particular purpose.
-- In particular, definition of @HST (t1 ': t2 ': ... tn ': '[])@ requires
-- constraints @(Typeable t1, Typeable t2, ..., Typeable tn)@ as well as
-- constraints @(Typeable '[ t1 ], Typeable '[ t1, t2 ], ...)@.
-- These applications of @Typeable@ class are required for convenient usage
-- of type encoded by @HST ts@ with some functions from @Data.Typeable@.
--
-- Data type @HST@ (Heterogeneous Stack Type) is a heterogenuous list of tuples.
-- First element of tuple is a structure, holding field and type annotations
-- for a given type.
-- Second element of tuple is an optional variable annotation for the stack
-- element.
-- Additionally constructor keeps 'SingI' constraint for the current type.
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

-- | Append a type to 'HST', assuming that notes and annotations
-- for this type are unknown.
(-:&)
  :: (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 -:&

-- | Extended pattern-match - adds @Sing x@ argument.
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

-- | No-argument type wrapper for @HST@ data type.
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

-- | This data type keeps part of type check result - instruction and
-- corresponding output stack.
data SomeInstrOut inp where
  -- | Type-check result with concrete output stack, most common case.
  --
  -- Output stack type is wrapped inside the type and @Typeable@
  -- constraint is provided to allow convenient unwrapping.
  (:::)
    :: SingI out
    => Instr inp out
    -> HST out
    -> SomeInstrOut inp

  -- | Type-check result which matches against arbitrary output stack.
  -- Information about annotations in the output stack is absent.
  --
  -- This case is only possible when the corresponding code terminates
  -- with @FAILWITH@ instruction in all possible executions.
  -- The opposite may be not true though (example: you push always-failing
  -- lambda and immediatelly execute it - stack type is known).
  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 type keeping the whole type check result: instruction and
-- type representations of instruction's input and output.
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

-- | Set of variables defined in a let-block.
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

-- | State for type checking @nop@
type TcExtFrames = [BoundVars]

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

-- | Given a type, provide evidence that it is well typed w.r.t to the
--  Michelson rules regarding where comparable types are required.
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

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

-- | Given a type and an action that requires evidence that the type is well typed,
--  generate the evidence and execute the action, or else fail with an error.
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)

-- | Similar to @withWTPm@ but is meant to be used within tests.
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