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

module Michelson.TypeCheck.Types
    ( HST (..)
    , (-:&)
    , pattern (::&+)
    , SomeHST (..)
    , SomeInstrOut (..)
    , SomeInstr (..)
    , SomeContract (..)
    , SomeContractAndStorage (..)
    , BoundVars (..)
    , TcExtFrames
    , NotWellTyped (..)
    , getWTP
    , withWTPm
    , unsafeWithWTP
    , mapSomeContract
    , noBoundVars
    ) where

import Data.Constraint (Dict(..))
import qualified Data.Map.Lazy as Map
import Data.Singletons (Sing, SingI(..), demote)
import Fmt (Buildable(..), Builder, (+|), (|+))
import Prelude hiding (EQ, GT, LT)
import qualified Text.Show

import Michelson.Typed (ParameterScope, StorageScope, Notes(..), T(..), SingT(..), notesT, starNotes)
import Michelson.Typed.Haskell.Value (WellTyped)
import qualified Michelson.Typed as T
import Michelson.Typed.Instr
import Michelson.Untyped (Type, Var, noAnn)
import Michelson.Untyped.Annotation (VarAnn)
import Util.Typeable

-- | 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 '[]
  (::&) :: (Typeable xs, T.KnownT x)
        => (Notes x, Dict (WellTyped x), VarAnn)
        -> HST xs
        -> HST (x ': xs)

instance NFData (HST ts) where
  rnf :: HST ts -> ()
rnf (HST ts
SNil) = ()
  rnf ((a :: Notes x
a, d :: Dict (WellTyped x)
d, b :: VarAnn
b) ::& hst :: 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 SNil = "[]"
  show (r :: (Notes x, Dict (WellTyped x), VarAnn)
r ::& rs :: HST xs
rs) = "[ " 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 (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> " ]"
    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, _vn :: VarAnn
_vn) ::& (b :: (Notes x, Dict (WellTyped x), VarAnn)
b ::& c :: 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 -> 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 (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(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, _vn :: VarAnn
_vn) ::& 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 SNil = "[]"
  build (r :: (Notes x, Dict (WellTyped x), VarAnn)
r ::& rs :: HST xs
rs) = "[ " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST (x : xs) -> Builder
forall (t :: T) (ts_ :: [T]). HST (t : ts_) -> Builder
showDo ((Notes x, Dict (WellTyped x), VarAnn)
r (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
::& HST xs
rs) Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " ]"
    where
      showDo :: HST (t ': ts_) -> Builder
      showDo :: HST (t : ts_) -> Builder
showDo ((Notes x -> T
forall (t :: T). SingI t => Notes t -> T
notesT -> T
t, Dict, _vn :: VarAnn
_vn) ::& (b :: (Notes x, Dict (WellTyped x), VarAnn)
b ::& c :: HST xs
c)) =
          T -> Builder
forall p. Buildable p => p -> Builder
build T
t Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ", " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST (x : xs) -> Builder
forall (t :: T) (ts_ :: [T]). HST (t : ts_) -> Builder
showDo ((Notes x, Dict (WellTyped x), VarAnn)
b (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(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, _vn :: VarAnn
_vn) ::& SNil) = T -> Builder
forall p. Buildable p => p -> Builder
build T
t

infixr 7 ::&

instance Eq (HST ts) where
  SNil == :: HST ts -> HST ts -> Bool
== SNil = Bool
True
  (n1 :: Notes x
n1, Dict, a1 :: VarAnn
a1) ::& h1 :: HST xs
h1 == (n2 :: Notes x
n2, Dict, a2 :: VarAnn
a2) ::& h2 :: 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
&& VarAnn
a1 VarAnn -> VarAnn -> Bool
forall a. Eq a => a -> a -> Bool
== VarAnn
a2 Bool -> Bool -> Bool
&& 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.
(-:&)
  :: (Typeable xs, WellTyped x)
  => Sing x
  -> HST xs
  -> HST (x ': xs)
_ -:& :: Sing x -> HST xs -> HST (x : xs)
-:& hst :: 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 (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(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)
     , T.KnownT x, Typeable 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), KnownT x, Typeable 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 (_, n :: Notes x
n, d :: Dict (WellTyped x)
d, v :: VarAnn
v) ::&+ hst :: HST xs
hst = (Notes x
n, Dict (WellTyped x)
d, VarAnn
v) (Notes x, Dict (WellTyped x), VarAnn) -> HST xs -> HST (x : xs)
forall (xs :: [T]) (x :: T).
(Typeable xs, KnownT x) =>
(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 :: Typeable ts => HST ts -> SomeHST

deriving stock instance Show SomeHST
instance NFData SomeHST where
  rnf :: SomeHST -> ()
rnf (SomeHST h :: HST ts
h) = HST ts -> ()
forall a. NFData a => a -> ()
rnf HST ts
h

instance Eq SomeHST where
  SomeHST hst1 :: HST ts
hst1 == :: SomeHST -> SomeHST -> Bool
== SomeHST hst2 :: HST ts
hst2 = HST ts
hst1 HST ts -> HST ts -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParam1` 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.
  (:::)
    :: (Typeable 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 (i :: Instr inp out
i ::: out :: 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 -> 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 i :: 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
<> " :: *"

-- | 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 :/

instance Show (ExtInstr inp) => Show (SomeInstr inp) where
  show :: SomeInstr inp -> String
show (inp :: HST inp
inp :/ out :: 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 -> ShowS
forall a. Semigroup a => a -> a -> a
<> SomeInstrOut inp -> String
forall b a. (Show a, IsString b) => a -> b
show SomeInstrOut inp
out

data SomeContract where
  SomeContract :: Contract cp st -> SomeContract

instance NFData SomeContract where
  rnf :: SomeContract -> ()
rnf (SomeContract c :: Contract cp st
c) = Contract cp st -> ()
forall a. NFData a => a -> ()
rnf Contract cp st
c

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 f :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
f (SomeContract fc :: 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

deriving stock instance Show SomeContract

-- | Represents a typed contract & a storage value of the type expected by the contract.
data SomeContractAndStorage where
  SomeContractAndStorage
    :: forall cp st.
       (StorageScope st, ParameterScope cp)
       => Contract cp st
       -> T.Value st
       -> SomeContractAndStorage

deriving stock instance Show SomeContractAndStorage

-- | Set of variables defined in a let-block.
data BoundVars = BoundVars (Map Var Type) (Maybe SomeHST)

noBoundVars :: BoundVars
noBoundVars :: BoundVars
noBoundVars = Map Var Type -> Maybe SomeHST -> BoundVars
BoundVars Map Var Type
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 T

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 ma :: Either e (Dict a)
ma b :: 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 -> 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
  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
  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
  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
  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 -> Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s) (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)
  STList s -> Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s) (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)
  STSet (s :: Sing si) ->
    Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s) ((WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$
    Either NotWellTyped (Dict (Comparable a))
-> (Comparable a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
        ( NotWellTyped
-> Maybe (Dict (Comparable a))
-> Either NotWellTyped (Dict (Comparable a))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> NotWellTyped
NotWellTyped (T -> NotWellTyped) -> T -> NotWellTyped
forall a b. (a -> b) -> a -> b
$ (SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) (Maybe (Dict (Comparable a))
 -> Either NotWellTyped (Dict (Comparable a)))
-> Maybe (Dict (Comparable a))
-> Either NotWellTyped (Dict (Comparable a))
forall a b. (a -> b) -> a -> b
$ Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing a
s
        ) ((Comparable a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (Comparable a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  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 -> Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s) (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)
  STPair s1 s2 -> Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s1) ((WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Either NotWellTyped (Dict (WellTyped b))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing b -> Either NotWellTyped (Dict (WellTyped b))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing b
s2) ((WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STOr s1 s2 -> Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s1) ((WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Either NotWellTyped (Dict (WellTyped b))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing b -> Either NotWellTyped (Dict (WellTyped b))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing b
s2) ((WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STLambda s1 s2 -> Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s1) ((WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Either NotWellTyped (Dict (WellTyped b))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing b -> Either NotWellTyped (Dict (WellTyped b))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing b
s2) ((WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STMap (s1 :: Sing si) s2 ->
      Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s1) ((WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$
      Either NotWellTyped (Dict (WellTyped b))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing b -> Either NotWellTyped (Dict (WellTyped b))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing b
s2) ((WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$
      Either NotWellTyped (Dict (Comparable a))
-> (Comparable a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
        ( NotWellTyped
-> Maybe (Dict (Comparable a))
-> Either NotWellTyped (Dict (Comparable a))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> NotWellTyped
NotWellTyped (T -> NotWellTyped) -> T -> NotWellTyped
forall a b. (a -> b) -> a -> b
$ (SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) (Maybe (Dict (Comparable a))
 -> Either NotWellTyped (Dict (Comparable a)))
-> Maybe (Dict (Comparable a))
-> Either NotWellTyped (Dict (Comparable a))
forall a b. (a -> b) -> a -> b
$ Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing a
s1
        ) ((Comparable a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (Comparable a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  STBigMap (s1 :: Sing si) s2 ->
      Either NotWellTyped (Dict (WellTyped a))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing a -> Either NotWellTyped (Dict (WellTyped a))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing a
s1) ((WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$
      Either NotWellTyped (Dict (WellTyped b))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict (Sing b -> Either NotWellTyped (Dict (WellTyped b))
forall (t1 :: T).
SingI t1 =>
Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ Sing b
s2) ((WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (WellTyped b => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$
      Either NotWellTyped (Dict (Comparable a))
-> (Comparable a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall e (a :: Constraint) (b :: Constraint).
Either e (Dict a) -> (a => Either e (Dict b)) -> Either e (Dict b)
fromEDict
        ( NotWellTyped
-> Maybe (Dict (Comparable a))
-> Either NotWellTyped (Dict (Comparable a))
forall l r. l -> Maybe r -> Either l r
maybeToRight (T -> NotWellTyped
NotWellTyped (T -> NotWellTyped) -> T -> NotWellTyped
forall a b. (a -> b) -> a -> b
$ (SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @si) (Maybe (Dict (Comparable a))
 -> Either NotWellTyped (Dict (Comparable a)))
-> Maybe (Dict (Comparable a))
-> Either NotWellTyped (Dict (Comparable a))
forall a b. (a -> b) -> a -> b
$ Sing a -> Maybe (Dict (Comparable a))
forall (a :: T). Sing a -> Maybe (Dict (Comparable a))
T.getComparableProofS Sing a
s1
        ) ((Comparable a => Either NotWellTyped (Dict (WellTyped t)))
 -> Either NotWellTyped (Dict (WellTyped t)))
-> (Comparable a => Either NotWellTyped (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ Dict (WellTyped t) -> Either NotWellTyped (Dict (WellTyped t))
forall a b. b -> Either a b
Right Dict (WellTyped t)
forall (a :: Constraint). a => Dict a
Dict
  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
  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
  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
  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
  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
  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
  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
  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
  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
  where
    getWTP_ :: forall t1. SingI t1 => Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
    getWTP_ :: Sing t1 -> Either NotWellTyped (Dict (WellTyped t1))
getWTP_ _ = SingI t1 => Either NotWellTyped (Dict (WellTyped t1))
forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t1

-- | 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 a :: 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 -> m a
WellTyped t => m a
a
  Left (NotWellTyped t :: T
t) ->
    String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail ("This type is not well typed because it has an non-comparable type in it: '" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (T -> String
forall b a. (Show a, IsString b) => a -> b
show T
t) String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
      "', where a comparable type is required")

-- | Similar to @withWTPm@ but is mean to be used within tests.
unsafeWithWTP :: forall t a. SingI t => (WellTyped t => a) -> a
unsafeWithWTP :: (WellTyped t => a) -> a
unsafeWithWTP fn :: 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 -> a
WellTyped t => a
fn
  Left (NotWellTyped t :: T
t) -> Text -> a
forall a. HasCallStack => Text -> a
error (Text -> a) -> Text -> a
forall a b. (a -> b) -> a -> b
$ "Type is not well typed: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (T -> Text
forall b a. (Show a, IsString b) => a -> b
show T
t)