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

-- | Errors that can occur when some code is being typechecked.

module Michelson.TypeCheck.Error
  ( TypeContext (..)
  , TopLevelType (..)
  , TCTypeError (..)
  , TCError (..)
  , ExtError (..)
  , StackSize (..)
  , pairWithNodeIndex
  , pairWithElems
  ) where

import Fmt (Buildable(..), pretty, (+|), (|+), (||+))
import Named ((:!), arg)
import Prelude hiding ((<$>), empty)
import Text.PrettyPrint.Leijen.Text hiding (pretty, bool)
import qualified Text.Show (show)

import Michelson.ErrorPos (InstrCallStack(..))
import Michelson.Printer.Util (RenderDoc (..), renderAnyBuildable,
  buildRenderDoc, buildRenderDocExtended, doesntNeedParens, renderDoc, renderDocList)
import Michelson.TypeCheck.TypeCheckedOp (TypeCheckedOp)
import Michelson.TypeCheck.Types (SomeHST(..))
import qualified Michelson.Typed as T
import Michelson.Typed.Annotation (AnnConvergeError(..))
import Michelson.Untyped (StackFn, Ty, Var)
import qualified Michelson.Untyped as U
import Tezos.Address (Address)
import Tezos.Crypto (CryptoParseError)
import qualified Tezos.Crypto.BLS12381 as BLS

-- | Contexts where type error can occur.
data TypeContext
  = LambdaArgument
  | LambdaCode
  | DipCode
  | ConsArgument
  | ComparisonArguments
  | ContractParameter
  | ContractStorage
  | ArithmeticOperation
  | Iteration
  | Cast
  | UnpairArgument
  | CarArgument
  | CdrArgument
  | If
  | ConcatArgument
  | ContainerKeyType
  | ContainerValueType
  | FailwithArgument
  | TicketsJoin
  deriving stock (Int -> TypeContext -> ShowS
[TypeContext] -> ShowS
TypeContext -> String
(Int -> TypeContext -> ShowS)
-> (TypeContext -> String)
-> ([TypeContext] -> ShowS)
-> Show TypeContext
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeContext] -> ShowS
$cshowList :: [TypeContext] -> ShowS
show :: TypeContext -> String
$cshow :: TypeContext -> String
showsPrec :: Int -> TypeContext -> ShowS
$cshowsPrec :: Int -> TypeContext -> ShowS
Show, TypeContext -> TypeContext -> Bool
(TypeContext -> TypeContext -> Bool)
-> (TypeContext -> TypeContext -> Bool) -> Eq TypeContext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeContext -> TypeContext -> Bool
$c/= :: TypeContext -> TypeContext -> Bool
== :: TypeContext -> TypeContext -> Bool
$c== :: TypeContext -> TypeContext -> Bool
Eq, (forall x. TypeContext -> Rep TypeContext x)
-> (forall x. Rep TypeContext x -> TypeContext)
-> Generic TypeContext
forall x. Rep TypeContext x -> TypeContext
forall x. TypeContext -> Rep TypeContext x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypeContext x -> TypeContext
$cfrom :: forall x. TypeContext -> Rep TypeContext x
Generic)
  deriving anyclass (TypeContext -> ()
(TypeContext -> ()) -> NFData TypeContext
forall a. (a -> ()) -> NFData a
rnf :: TypeContext -> ()
$crnf :: TypeContext -> ()
NFData)

instance RenderDoc TypeContext where
  renderDoc :: RenderContext -> TypeContext -> Doc
renderDoc RenderContext
_ = \case
    TypeContext
LambdaArgument -> Doc
"argument to some lambda"
    TypeContext
LambdaCode -> Doc
"code in LAMBDA"
    TypeContext
DipCode -> Doc
"code in DIP"
    TypeContext
ConsArgument -> Doc
"argument to CONS"
    TypeContext
ComparisonArguments -> Doc
"arguments to comparison function"
    TypeContext
ContractParameter -> Doc
"contract parameter"
    TypeContext
ContractStorage -> Doc
"contract storage"
    TypeContext
ArithmeticOperation -> Doc
"arguments to arithmetic operation"
    TypeContext
Iteration -> Doc
"iteration (ITER / MAP / etc) code"
    TypeContext
Cast -> Doc
"argument to CAST"
    TypeContext
UnpairArgument -> Doc
"argument to UNPAIR"
    TypeContext
CarArgument -> Doc
"argument to CAR"
    TypeContext
CdrArgument -> Doc
"argument to CDR"
    TypeContext
If -> Doc
"conditional expression"
    TypeContext
ConcatArgument -> Doc
"argument to CONCAT"
    TypeContext
ContainerKeyType -> Doc
"container key type"
    TypeContext
ContainerValueType -> Doc
"container value type"
    TypeContext
FailwithArgument -> Doc
"argument to FAILWITH"
    TypeContext
TicketsJoin -> Doc
"join of two tickets"

data TopLevelType
  = TltParameterType
  | TltStorageType
  deriving stock (Int -> TopLevelType -> ShowS
[TopLevelType] -> ShowS
TopLevelType -> String
(Int -> TopLevelType -> ShowS)
-> (TopLevelType -> String)
-> ([TopLevelType] -> ShowS)
-> Show TopLevelType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TopLevelType] -> ShowS
$cshowList :: [TopLevelType] -> ShowS
show :: TopLevelType -> String
$cshow :: TopLevelType -> String
showsPrec :: Int -> TopLevelType -> ShowS
$cshowsPrec :: Int -> TopLevelType -> ShowS
Show, TopLevelType -> TopLevelType -> Bool
(TopLevelType -> TopLevelType -> Bool)
-> (TopLevelType -> TopLevelType -> Bool) -> Eq TopLevelType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TopLevelType -> TopLevelType -> Bool
$c/= :: TopLevelType -> TopLevelType -> Bool
== :: TopLevelType -> TopLevelType -> Bool
$c== :: TopLevelType -> TopLevelType -> Bool
Eq, (forall x. TopLevelType -> Rep TopLevelType x)
-> (forall x. Rep TopLevelType x -> TopLevelType)
-> Generic TopLevelType
forall x. Rep TopLevelType x -> TopLevelType
forall x. TopLevelType -> Rep TopLevelType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TopLevelType x -> TopLevelType
$cfrom :: forall x. TopLevelType -> Rep TopLevelType x
Generic)
  deriving anyclass (TopLevelType -> ()
(TopLevelType -> ()) -> NFData TopLevelType
forall a. (a -> ()) -> NFData a
rnf :: TopLevelType -> ()
$crnf :: TopLevelType -> ()
NFData)

instance Buildable TopLevelType where
  build :: TopLevelType -> Builder
build = TopLevelType -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDoc

instance RenderDoc TopLevelType where
  renderDoc :: RenderContext -> TopLevelType -> Doc
renderDoc RenderContext
_ = \case
    TopLevelType
TltParameterType -> Doc
"parameter"
    TopLevelType
TltStorageType -> Doc
"storage"

instance Buildable TypeContext where
  build :: TypeContext -> Builder
build = TypeContext -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDoc

-- | Data type that represents various errors
-- which are related to type system.
-- These errors are used to specify info about type check errors
-- in @TCError@ data type.
data TCTypeError
  = AnnError AnnConvergeError
  -- ^ Annotation unify error
  | TypeEqError T.T T.T
  -- ^ Type equality error
  | StackEqError [T.T] [T.T]
  -- ^ Stacks equality error
  | UnsupportedTypeForScope T.T T.BadTypeForScope
  -- ^ Error that happens when type cannot be used in the corresponding scope.
  -- Argument of this constructor carries type which violates
  -- the restriction, e.g. @big_map@ in @UNPACK@, and a concrete reason why the
  -- type is unsuported.
  | NotNumericTypes T.T T.T
  -- ^ Arithmetic operation is applied to types, at least one of which is not numeric
  -- (e.g. @timestamp@ and @timestamp@ passed to @MUL@ instruction).
  | UnexpectedType (NonEmpty (NonEmpty Text))
  -- ^ Error that happens when actual types are different from the type that instruction expects.
  -- The param is an non-empty list of all expected stack types that the instruction would accept.
  -- Each expected stack types is represented as non-empty list as well.
  | UnexpectedTopLevelType TopLevelType ("expected" :! T.T) ("got" :! T.T)
  -- ^ Error that happens when the caller expected one top-level type, but
  -- the contract has another type specified.
  | InvalidInstruction U.ExpandedInstr Text
  -- ^ Some instruction is invalid or used in an invalid way.
  -- For example, @PAIR 0@ or @PAIR 1@, or a @SELF@ instruction was used in a @LAMBDA@.
  -- The 'Text' argument is a user-readable explanation of why this instruction is invalid.
  | InvalidValueType T.T
  -- ^ Error that happens when a `U.Value` is never a valid source for this type
  -- (e.g. @timestamp@ cannot be obtained from a `U.ValueTrue`)
  | NotEnoughItemsOnStack
  -- ^ There are not enough items on stack to perform a certain instruction.
  | IllegalEntrypoint T.EpNameFromRefAnnError
  -- ^ Invalid entrypoint name provided
  | UnknownContract Address
  -- ^ Contract with given address is not originated.
  | EntrypointNotFound T.EpName
  -- ^ Given entrypoint is not present.
  | IllegalParamDecl T.ParamEpError
  -- ^ Incorrect parameter declaration (with respect to entrypoints feature).
  | NegativeNat
  -- ^ Natural numbers cannot be negative
  | MutezOverflow
  -- ^ Exceeds the maximal mutez value
  | InvalidAddress T.ParseEpAddressError
  -- ^ Address couldn't be parsed from its textual representation
  | InvalidKeyHash CryptoParseError
  -- ^ KeyHash couldn't be parsed from its textual representation
  | InvalidBls12381Object BLS.DeserializationError
  -- ^ BLS12-381 primitive couldn't be parsed
  | InvalidTimestamp
  -- ^ Timestamp is not RFC339 compliant
  | CodeAlwaysFails
  -- ^ Code always fails, but shouldn't, like in ITER body.
  -- This is actually more general, any instruction that allows no continuation
  -- (like @NEVER@) cannot appear as part of another instruction's body.
  | EmptyCode
  -- ^ Empty block of code, like ITER body.
  | AnyError
  -- ^ Generic error when instruction does not match something sensible.
  deriving stock (Int -> TCTypeError -> ShowS
[TCTypeError] -> ShowS
TCTypeError -> String
(Int -> TCTypeError -> ShowS)
-> (TCTypeError -> String)
-> ([TCTypeError] -> ShowS)
-> Show TCTypeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCTypeError] -> ShowS
$cshowList :: [TCTypeError] -> ShowS
show :: TCTypeError -> String
$cshow :: TCTypeError -> String
showsPrec :: Int -> TCTypeError -> ShowS
$cshowsPrec :: Int -> TCTypeError -> ShowS
Show, TCTypeError -> TCTypeError -> Bool
(TCTypeError -> TCTypeError -> Bool)
-> (TCTypeError -> TCTypeError -> Bool) -> Eq TCTypeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCTypeError -> TCTypeError -> Bool
$c/= :: TCTypeError -> TCTypeError -> Bool
== :: TCTypeError -> TCTypeError -> Bool
$c== :: TCTypeError -> TCTypeError -> Bool
Eq, (forall x. TCTypeError -> Rep TCTypeError x)
-> (forall x. Rep TCTypeError x -> TCTypeError)
-> Generic TCTypeError
forall x. Rep TCTypeError x -> TCTypeError
forall x. TCTypeError -> Rep TCTypeError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TCTypeError x -> TCTypeError
$cfrom :: forall x. TCTypeError -> Rep TCTypeError x
Generic)
  deriving anyclass (TCTypeError -> ()
(TCTypeError -> ()) -> NFData TCTypeError
forall a. (a -> ()) -> NFData a
rnf :: TCTypeError -> ()
$crnf :: TCTypeError -> ()
NFData)

instance Buildable TCTypeError where
  build :: TCTypeError -> Builder
build = TCTypeError -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDocExtended

instance RenderDoc TCTypeError where
  renderDoc :: RenderContext -> TCTypeError -> Doc
renderDoc RenderContext
context = \case
    AnnError AnnConvergeError
e -> AnnConvergeError -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable AnnConvergeError
e
    TypeEqError T
type1 T
type2 ->
      Doc
"Types not equal:" Doc -> Doc -> Doc
<+> (RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
type1) Doc -> Doc -> Doc
<+> Doc
"/=" Doc -> Doc -> Doc
<+> (RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
type2)
    StackEqError [T]
st1 [T]
st2 ->
      Doc
"Stacks not equal:"Doc -> Doc -> Doc
<+> (RenderContext -> [T] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context [T]
st1) Doc -> Doc -> Doc
<+> Doc
"/=" Doc -> Doc -> Doc
<+> (RenderContext -> [T] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context [T]
st2)
    UnsupportedTypeForScope T
typ BadTypeForScope
reason ->
      Doc
"Type '" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
typ) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"' is unsupported here because it"
      Doc -> Doc -> Doc
<+> (RenderContext -> BadTypeForScope -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context BadTypeForScope
reason)
    NotNumericTypes T
t1 T
t2 ->
      Doc
"Some of the types in an arithmetic operation are not numeric:"
      Doc -> Doc -> Doc
<+> (RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
t1) Doc -> Doc -> Doc
<+> Doc
"and" Doc -> Doc -> Doc
<+> (RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
t2)
    UnexpectedType (NonEmpty Text
t :| [NonEmpty Text]
ts) ->
      Doc
"Wrong stack type for instruction, expect stack type to begin with " Doc -> Doc -> Doc
<+>
        ([Doc] -> Doc
cat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"or"
          ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (NonEmpty Text -> Doc) -> [NonEmpty Text] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Text
x :| [Text]
xs) -> [Doc] -> Doc
list ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Text -> Doc) -> [Text] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable) (Text
xText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
xs))
          ([NonEmpty Text] -> [Doc]) -> [NonEmpty Text] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (NonEmpty Text
tNonEmpty Text -> [NonEmpty Text] -> [NonEmpty Text]
forall a. a -> [a] -> [a]
:[NonEmpty Text]
ts)
        )
    UnexpectedTopLevelType TopLevelType
tyDesc (Name "expected" -> ("expected" :! T) -> T
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "expected" (Name "expected")
Name "expected"
#expected -> T
expected) (Name "got" -> ("got" :! T) -> T
forall (name :: Symbol) a. Name name -> (name :! a) -> a
arg IsLabel "got" (Name "got")
Name "got"
#got -> T
got) ->
      Doc
"Unexpected" Doc -> Doc -> Doc
<+> RenderContext -> TopLevelType -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TopLevelType
tyDesc Doc -> Doc -> Doc
<+> Doc
"type:"
      Doc -> Doc -> Doc
<$$> T -> Doc
renderLargeType T
got
      Doc -> Doc -> Doc
<$$> Doc
"Expected:"
      Doc -> Doc -> Doc
<$$> T -> Doc
renderLargeType T
expected
    InvalidInstruction ExpandedInstr
instr Text
reason ->
      Doc
"Invalid instruction" Doc -> Doc -> Doc
<+> (RenderContext -> ExpandedInstr -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ExpandedInstr
instr)
      Doc -> Doc -> Doc
<$$> Doc
"Reason:" Doc -> Doc -> Doc
<+> Text -> Doc
textStrict Text
reason
    InvalidValueType T
t ->
      Doc
"Value type is never a valid" Doc -> Doc -> Doc
<+> Doc -> Doc -> Doc -> Doc
enclose Doc
"`" Doc
"`" (RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context T
t)
    TCTypeError
NotEnoughItemsOnStack ->
      Doc
"Not enough items on stack"
    UnknownContract Address
addr ->
      Doc
"Contract is not registered:" Doc -> Doc -> Doc
<+> (Address -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable Address
addr)
    IllegalEntrypoint EpNameFromRefAnnError
err -> RenderContext -> EpNameFromRefAnnError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context EpNameFromRefAnnError
err
    EntrypointNotFound EpName
ep ->
      Doc
"No such entrypoint" Doc -> Doc -> Doc
<+> Doc -> Doc -> Doc -> Doc
enclose Doc
"`" Doc
"`" (EpName -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable EpName
ep)
    IllegalParamDecl ParamEpError
err -> RenderContext -> ParamEpError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ParamEpError
err
    TCTypeError
NegativeNat -> Doc
"Natural number cannot be negative"
    TCTypeError
MutezOverflow -> Doc
"Exceeds maximal value for mutez"
    InvalidAddress ParseEpAddressError
e -> RenderContext -> ParseEpAddressError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ParseEpAddressError
e
    InvalidKeyHash CryptoParseError
e -> RenderContext -> CryptoParseError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context CryptoParseError
e
    InvalidBls12381Object DeserializationError
e -> RenderContext -> DeserializationError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context DeserializationError
e
    TCTypeError
InvalidTimestamp -> Doc
"Is not a valid RFC3339 timestamp"
    TCTypeError
CodeAlwaysFails ->
      Doc
"Cannot use a terminate instruction (like FAILWITH) as part of another \
      \instruction's body"
    TCTypeError
EmptyCode -> Doc
"Code block is empty"
    TCTypeError
AnyError -> Doc
"Some of the arguments have invalid types"
    where
      renderLargeType :: T.T -> Doc
      renderLargeType :: T -> Doc
renderLargeType = Int -> Doc -> Doc
indent Int
2 (Doc -> Doc) -> (T -> Doc) -> T -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RenderContext -> Ty -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens (Ty -> Doc) -> (T -> Ty) -> T -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Ty
T.toUType

-- | Type check error
data TCError
  = TCFailedOnInstr U.ExpandedInstr SomeHST InstrCallStack (Maybe TypeContext) (Maybe TCTypeError)
  | TCFailedOnValue U.Value T.T Text InstrCallStack (Maybe TCTypeError)
  | TCContractError Text (Maybe TCTypeError)
  | TCUnreachableCode InstrCallStack (NonEmpty U.ExpandedOp)
  | TCExtError SomeHST InstrCallStack ExtError
  | TCIncompletelyTyped TCError (U.Contract' TypeCheckedOp)
  deriving stock (TCError -> TCError -> Bool
(TCError -> TCError -> Bool)
-> (TCError -> TCError -> Bool) -> Eq TCError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCError -> TCError -> Bool
$c/= :: TCError -> TCError -> Bool
== :: TCError -> TCError -> Bool
$c== :: TCError -> TCError -> Bool
Eq, (forall x. TCError -> Rep TCError x)
-> (forall x. Rep TCError x -> TCError) -> Generic TCError
forall x. Rep TCError x -> TCError
forall x. TCError -> Rep TCError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TCError x -> TCError
$cfrom :: forall x. TCError -> Rep TCError x
Generic)

instance NFData TCError

instance Buildable TCError where
  build :: TCError -> Builder
build = TCError -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDocExtended

instance RenderDoc TCError where
  renderDoc :: RenderContext -> TCError -> Doc
renderDoc RenderContext
context = \case
    TCFailedOnInstr ExpandedInstr
instr (SomeHST HST ts
t) InstrCallStack
ics Maybe TypeContext
mbTCTypeContext Maybe TCTypeError
mbTCTypeError -> Doc
line
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"Error checking expression:"
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
surroundWithNewLines (RenderContext -> ExpandedInstr -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ExpandedInstr
instr)
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"against input stack type:"
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
surroundWithNewLines (RenderContext -> HST ts -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context HST ts
t)
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (TypeContext -> Doc) -> Maybe TypeContext -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"" (\TypeContext
c -> Doc
"Error in" Doc -> Doc -> Doc
<+> RenderContext -> TypeContext -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TypeContext
c) Maybe TypeContext
mbTCTypeContext
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> (TCTypeError -> Doc) -> Maybe TCTypeError -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"" (\TCTypeError
e -> Doc
":" Doc -> Doc -> Doc
<+> (RenderContext -> TCTypeError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TCTypeError
e) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"." Doc -> Doc -> Doc
<$$> Doc
line) Maybe TCTypeError
mbTCTypeError
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (RenderContext -> InstrCallStack -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context InstrCallStack
ics)
    TCFailedOnValue Value
v T
t Text
custom InstrCallStack
ics Maybe TCTypeError
mbTCTypeError ->
      Doc
"Error checking value"
      Doc -> Doc -> Doc
<$$> (RenderContext -> Value -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context Value
v) Doc -> Doc -> Doc
<+> Doc
"against type"
      Doc -> Doc -> Doc
<+> (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 -> Bool -> Doc
forall a. a -> a -> Bool -> a
bool (Doc
":" Doc -> Doc -> Doc
<+> (Text -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable Text
custom)) Doc
"." (Text -> Bool
forall t. Container t => t -> Bool
null Text
custom))
      Doc -> Doc -> Doc
<+> (Doc -> (TCTypeError -> Doc) -> Maybe TCTypeError -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"" (\TCTypeError
e -> Doc
line Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (RenderContext -> TCTypeError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TCTypeError
e) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
line) Maybe TCTypeError
mbTCTypeError)
      Doc -> Doc -> Doc
<+> (RenderContext -> InstrCallStack -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context InstrCallStack
ics)
    TCContractError Text
msg Maybe TCTypeError
typeError ->
      Doc
"Error occurred during contract typecheck:"
      Doc -> Doc -> Doc
<$$> (Text -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable Text
msg) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (Doc -> (TCTypeError -> Doc) -> Maybe TCTypeError -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"" (\TCTypeError
e -> Doc
" " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (RenderContext -> TCTypeError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TCTypeError
e)) Maybe TCTypeError
typeError)
    TCUnreachableCode InstrCallStack
ics NonEmpty ExpandedOp
instrs ->
      Doc
"Unreachable code:" Doc -> Doc -> Doc
<$$> Int -> [ExpandedOp] -> Doc
buildTruncated Int
3 (NonEmpty ExpandedOp -> [Element (NonEmpty ExpandedOp)]
forall t. Container t => t -> [Element t]
toList NonEmpty ExpandedOp
instrs) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Doc -> Doc -> Doc
<+> (RenderContext -> InstrCallStack -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context InstrCallStack
ics)
    TCExtError (SomeHST HST ts
t) InstrCallStack
ics ExtError
e ->
      Doc
"Error occurred during Morley extension typecheck:" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
      (ExtError -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable ExtError
e) Doc -> Doc -> Doc
<+> Doc
"on stack" Doc -> Doc -> Doc
<+> (RenderContext -> HST ts -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context HST ts
t) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Doc -> Doc -> Doc
<+> (RenderContext -> InstrCallStack -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context InstrCallStack
ics)
    TCIncompletelyTyped TCError
err Contract' TypeCheckedOp
contract ->
      Doc
line
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> RenderContext -> Contract' TypeCheckedOp -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens Contract' TypeCheckedOp
contract
      Doc -> Doc -> Doc
<$> RenderContext -> TCError -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TCError
err
    where
    buildTruncated :: Int -> [ExpandedOp] -> Doc
buildTruncated Int
k [ExpandedOp]
l
      | [ExpandedOp] -> Bool
forall t. Container t => t -> Bool
null (Int -> [ExpandedOp] -> [ExpandedOp]
forall a. Int -> [a] -> [a]
drop Int
k [ExpandedOp]
l) = RenderContext -> [ExpandedOp] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context [ExpandedOp]
l
      | Bool
otherwise = (RenderContext -> [ExpandedOp] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context (Int -> [ExpandedOp] -> [ExpandedOp]
forall a. Int -> [a] -> [a]
take Int
k [ExpandedOp]
l)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" ..."

    -- | Helper to format a line using empty lines at the end and at the beginning,
    -- and 4-space indents for the line itself
    surroundWithNewLines :: Doc -> Doc
    surroundWithNewLines :: Doc -> Doc
surroundWithNewLines Doc
l =
      Doc
line
      Doc -> Doc -> Doc
<$$> Int -> Doc -> Doc
indent Int
4 Doc
l
      Doc -> Doc -> Doc
<$$> Doc
line

instance Show TCError where
  show :: TCError -> String
show = TCError -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty

instance Exception TCError

newtype StackSize = StackSize Natural
  deriving stock (Int -> StackSize -> ShowS
[StackSize] -> ShowS
StackSize -> String
(Int -> StackSize -> ShowS)
-> (StackSize -> String)
-> ([StackSize] -> ShowS)
-> Show StackSize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StackSize] -> ShowS
$cshowList :: [StackSize] -> ShowS
show :: StackSize -> String
$cshow :: StackSize -> String
showsPrec :: Int -> StackSize -> ShowS
$cshowsPrec :: Int -> StackSize -> ShowS
Show, StackSize -> StackSize -> Bool
(StackSize -> StackSize -> Bool)
-> (StackSize -> StackSize -> Bool) -> Eq StackSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StackSize -> StackSize -> Bool
$c/= :: StackSize -> StackSize -> Bool
== :: StackSize -> StackSize -> Bool
$c== :: StackSize -> StackSize -> Bool
Eq, (forall x. StackSize -> Rep StackSize x)
-> (forall x. Rep StackSize x -> StackSize) -> Generic StackSize
forall x. Rep StackSize x -> StackSize
forall x. StackSize -> Rep StackSize x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep StackSize x -> StackSize
$cfrom :: forall x. StackSize -> Rep StackSize x
Generic)

instance NFData StackSize

-- | Various type errors possible when checking Morley extension commands
data ExtError =
    LengthMismatch U.StackTypePattern
  | VarError Text StackFn
  | TypeMismatch U.StackTypePattern Int TCTypeError
  | TyVarMismatch Var Ty U.StackTypePattern Int TCTypeError
  | StkRestMismatch U.StackTypePattern SomeHST SomeHST TCTypeError
  | TestAssertError Text
  | InvalidStackReference U.StackRef StackSize
  deriving stock (ExtError -> ExtError -> Bool
(ExtError -> ExtError -> Bool)
-> (ExtError -> ExtError -> Bool) -> Eq ExtError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExtError -> ExtError -> Bool
$c/= :: ExtError -> ExtError -> Bool
== :: ExtError -> ExtError -> Bool
$c== :: ExtError -> ExtError -> Bool
Eq, (forall x. ExtError -> Rep ExtError x)
-> (forall x. Rep ExtError x -> ExtError) -> Generic ExtError
forall x. Rep ExtError x -> ExtError
forall x. ExtError -> Rep ExtError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ExtError x -> ExtError
$cfrom :: forall x. ExtError -> Rep ExtError x
Generic)

instance NFData ExtError

instance Buildable ExtError where
  build :: ExtError -> Builder
build = \case
    LengthMismatch StackTypePattern
stk ->
      Builder
"Unexpected length of stack: pattern "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" has length "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ([TyVar] -> Int
forall t. Container t => t -> Int
length ([TyVar] -> Int)
-> (StackTypePattern -> [TyVar]) -> StackTypePattern -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([TyVar], Bool) -> [TyVar]
forall a b. (a, b) -> a
fst (([TyVar], Bool) -> [TyVar])
-> (StackTypePattern -> ([TyVar], Bool))
-> StackTypePattern
-> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StackTypePattern -> ([TyVar], Bool)
U.stackTypePatternToList) StackTypePattern
stk Int -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    VarError Text
t StackFn
sf ->
      Builder
"In defenition of " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Text
t Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
": VarError "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackFn
sf StackFn -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    TypeMismatch StackTypePattern
stk Int
i TCTypeError
e ->
      Builder
"TypeMismatch: Pattern " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" at index "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Int
i Int -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" with error: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    TyVarMismatch Var
v Ty
t StackTypePattern
stk Int
i TCTypeError
e ->
      Builder
"TyVarMismach: Variable " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Var
v Var -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" is bound to type "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Ty
t Ty -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" but pattern " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" failed at index "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Int
i Int -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" with error: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    StkRestMismatch StackTypePattern
stk (SomeHST HST ts
r) (SomeHST HST ts
r') TCTypeError
e ->
      Builder
"StkRestMismatch in pattern " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackTypePattern
stk StackTypePattern -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+
      Builder
" against stacks " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST ts
r HST ts -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ Builder
" and " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| HST ts
r' HST ts -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+
      Builder
" with error: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| TCTypeError
e TCTypeError -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    TestAssertError Text
t ->
      Builder
"TestAssertError: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Text
t Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    InvalidStackReference StackRef
i StackSize
lhs ->
      Builder
"InvalidStackReference: reference is out of the stack: "
      Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackRef
i StackRef -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ Builder
" >= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| StackSize
lhs StackSize -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ Builder
""

----------------------------------------------------------------------------
-- Helpers for formatting types
----------------------------------------------------------------------------

-- | Given a node index @ix@, creates a string representing the
-- smallest possible right-combed pair with at least @ix+1@ nodes.
--
-- Since the node index 0 is valid even for non-pair values
-- (e.g. we can run @GET 0@ on a @string@ or an @int@),
-- we simply return a type variable @'a@ in this case.
--
-- >>> pairWithNodeIndex 0
-- "'a"
--
-- >>> pairWithNodeIndex 4
-- "pair 'a1 'a2 'a3"
--
-- >>> pairWithNodeIndex 5
-- "pair 'a1 'a2 'a3 'a4"
pairWithNodeIndex :: Word -> Text
pairWithNodeIndex :: Word -> Text
pairWithNodeIndex = \case
  Word
0 -> Text
"'a"
  Word
ix -> Word -> Text
pairWithElems (Word -> Word
minPairLength Word
ix)
  where
    -- | Given a node index @ix@, calculates the minimum number of
    -- elements a pair must have for that index to be valid.
    minPairLength :: Word -> Word
    minPairLength :: Word -> Word
minPairLength = \case
      Word
0 -> Word
2
      Word
ix -> (Word
ix Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
3) Word -> Word -> Word
forall a. Integral a => a -> a -> a
`div` Word
2

-- | Given a number @n@, creates a string representing a
-- right-combed pair of arity @n@.
--
-- > pairType 3 == "pair 'a1 'a2 'a3"
pairWithElems :: Word -> Text
pairWithElems :: Word -> Text
pairWithElems Word
n =
  Text
"pair "
  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat (Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
intersperse Text
" " ([Word
1 .. Word
n] [Word] -> (Word -> Text) -> [Text]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Word
i -> Text
"'a" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Word -> Text
forall b a. (Show a, IsString b) => a -> b
show Word
i))