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

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

module Morley.Michelson.TypeCheck.Error
  ( TypeContext (..)
  , TopLevelType (..)
  , TcTypeError (..)
  , TcError
  , TcError' (..)
  , ExtError (..)
  , StackSize (..)
  , pairWithNodeIndex
  , pairWithElems
  ) where

import Fmt (Buildable(..), pretty, (+|), (|+))
import Prelude hiding (empty, (<$>))
import Text.PrettyPrint.Leijen.Text
  (Doc, cat, enclose, indent, line, list, punctuate, textStrict, (<$$>), (<$>), (<+>))

import Morley.Michelson.ErrorPos (ErrorSrcPos(..))
import Morley.Michelson.Printer.Util
  (RenderDoc(..), buildRenderDoc, buildRenderDocExtended, doesntNeedParens, renderAnyBuildable,
  renderDoc, renderDocList)
import Morley.Michelson.TypeCheck.TypeCheckedOp (TypeCheckedOp)
import Morley.Michelson.TypeCheck.Types (SomeHST(..))
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address
import Morley.Tezos.Crypto (CryptoParseError)
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Util.MismatchError

-- | Contexts where type error can occur.
data TypeContext
  = LambdaArgument
  | LambdaCodeCtx
  | DipCode
  | ConsArgument
  | ComparisonArguments
  | ContractParameter
  | ContractStorage
  | ArithmeticOperation
  | Iteration
  | Cast
  | UnpairArgument
  | CarArgument
  | CdrArgument
  | If
  | ConcatArgument
  | ContainerKeyType
  | ContainerValueType
  | FailwithArgument
  | TicketsJoin
  | ViewBlock
  | EmitArgument
  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
LambdaCodeCtx -> 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"
    TypeContext
ViewBlock -> Doc
"top-level view block"
    TypeContext
EmitArgument -> Doc
"argument to EMIT"

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
  = TypeEqError (MismatchError T.T)
  -- ^ Type equality error
  | StackEqError (MismatchError [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 (MismatchError T.T)
  -- ^ Error that happens when the caller expected one top-level type, but
  -- the contract has another type specified.
  | InvalidInstruction (U.InstrAbstract ()) 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.
  --
  -- Since this makes sense only for primitive instructions, we keep
  -- @U.InstrAbstract@ with @()@ type argument.
  | 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 ContractAddress
  -- ^ Contract with given address is not originated.
  | TxRollupContract TxRollupAddress
  -- ^ Provided txr1 address as contract.
  | 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.
  | InvalidBigMapId Integer
  -- ^ A big_map with the given ID was not found.
  | UnexpectedBigMapType
  -- ^ We found a big_map with the given big_map ID, but
  -- its key and/or value types are not the same as the requested types.
      Integer -- ^ The big_map ID we used to lookup a big_map value.
      (MismatchError T.T)
  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
    TypeEqError MismatchError T
merr ->
      Doc
"Types not equal:" Doc -> Doc -> Doc
<$> RenderContext -> MismatchError T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context MismatchError T
merr
    StackEqError MismatchError [T]
merr ->
      Doc
"Stacks not equal:" Doc -> Doc -> Doc
<$> RenderContext -> MismatchError [T] -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context MismatchError [T]
merr
    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 MismatchError T
mmerr ->
      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
<$$> RenderContext -> MismatchError T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens MismatchError T
mmerr
    InvalidInstruction InstrAbstract ()
instr Text
reason ->
      Doc
"Invalid instruction" Doc -> Doc -> Doc
<+> (RenderContext -> InstrAbstract Text -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context (InstrAbstract ()
instr InstrAbstract () -> Text -> InstrAbstract Text
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> (Text
"..." :: Text)))
      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 ContractAddress
addr ->
      Doc
"Contract is not registered:" Doc -> Doc -> Doc
<+> (ContractAddress -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable ContractAddress
addr)
    TxRollupContract TxRollupAddress
addr ->
      Doc
"txr1 address can not be used as a contract:" Doc -> Doc -> Doc
<+> (TxRollupAddress -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable TxRollupAddress
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) in this block"
    TcTypeError
EmptyCode -> Doc
"Code block is empty"
    TcTypeError
AnyError -> Doc
"Some of the arguments have invalid types"
    InvalidBigMapId Integer
bigMapId ->
      Doc
"No big_map with ID" Doc -> Doc -> Doc
<+> Integer -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable Integer
bigMapId Doc -> Doc -> Doc
<+> Doc
"was found."
    UnexpectedBigMapType Integer
bigMapId MismatchError T
mismatchError ->
      Doc
"A big_map with the ID" Doc -> Doc -> Doc
<+> Integer -> Doc
forall a. Buildable a => a -> Doc
renderAnyBuildable Integer
bigMapId Doc -> Doc -> Doc
<+> Doc
"was found, but it does not have the expected type."
      Doc -> Doc -> Doc
<$$> RenderContext -> MismatchError T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context MismatchError T
mismatchError

instance Exception TcTypeError

-- | Type check error
data TcError' op
  = TcFailedOnInstr (U.InstrAbstract op) SomeHST ErrorSrcPos (Maybe TypeContext) (Maybe TcTypeError)
  | TcFailedOnValue (U.Value' op) T.T Text ErrorSrcPos (Maybe TcTypeError)
  | TcContractError Text (Maybe TcTypeError)
  | TcViewError Text U.ViewName (Maybe TcTypeError)
  | TcUnreachableCode ErrorSrcPos (NonEmpty op)
  | TcExtError SomeHST ErrorSrcPos ExtError
  | TcIncompletelyTyped (TcError' op) (U.Contract' (TypeCheckedOp op))
  | TcIncompletelyTypedView (TcError' op) (U.View' (TypeCheckedOp op))
  | TcDeprecatedType Text T.T
  deriving stock (Int -> TcError' op -> ShowS
[TcError' op] -> ShowS
TcError' op -> String
(Int -> TcError' op -> ShowS)
-> (TcError' op -> String)
-> ([TcError' op] -> ShowS)
-> Show (TcError' op)
forall op. Show op => Int -> TcError' op -> ShowS
forall op. Show op => [TcError' op] -> ShowS
forall op. Show op => TcError' op -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TcError' op] -> ShowS
$cshowList :: forall op. Show op => [TcError' op] -> ShowS
show :: TcError' op -> String
$cshow :: forall op. Show op => TcError' op -> String
showsPrec :: Int -> TcError' op -> ShowS
$cshowsPrec :: forall op. Show op => Int -> TcError' op -> ShowS
Show, TcError' op -> TcError' op -> Bool
(TcError' op -> TcError' op -> Bool)
-> (TcError' op -> TcError' op -> Bool) -> Eq (TcError' op)
forall op. Eq op => TcError' op -> TcError' op -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TcError' op -> TcError' op -> Bool
$c/= :: forall op. Eq op => TcError' op -> TcError' op -> Bool
== :: TcError' op -> TcError' op -> Bool
$c== :: forall op. Eq op => TcError' op -> TcError' op -> Bool
Eq, (forall x. TcError' op -> Rep (TcError' op) x)
-> (forall x. Rep (TcError' op) x -> TcError' op)
-> Generic (TcError' op)
forall x. Rep (TcError' op) x -> TcError' op
forall x. TcError' op -> Rep (TcError' op) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall op x. Rep (TcError' op) x -> TcError' op
forall op x. TcError' op -> Rep (TcError' op) x
$cto :: forall op x. Rep (TcError' op) x -> TcError' op
$cfrom :: forall op x. TcError' op -> Rep (TcError' op) x
Generic)

type TcError = TcError' U.ExpandedOp

instance (NFData op, NFData (TypeCheckedOp op)) => NFData (TcError' op)

instance RenderDoc op => Buildable (TcError' op) where
  build :: TcError' op -> Builder
build = TcError' op -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDocExtended

instance RenderDoc op => RenderDoc (TcError' op) where
  renderDoc :: RenderContext -> TcError' op -> Doc
renderDoc RenderContext
context = \case
    TcFailedOnInstr InstrAbstract op
instr (SomeHST HST ts
t) ErrorSrcPos
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 -> InstrAbstract op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context InstrAbstract op
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 -> ErrorSrcPos -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ErrorSrcPos
ics)
    TcFailedOnValue Value' op
v T
t Text
custom ErrorSrcPos
ics Maybe TcTypeError
mbTcTypeError ->
      Doc
"Error checking value"
      Doc -> Doc -> Doc
<$$> (RenderContext -> Value' op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context Value' op
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 -> ErrorSrcPos -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ErrorSrcPos
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)
    TcViewError Text
msg ViewName
viewName Maybe TcTypeError
typeError ->
      Doc
"Error occurred during typecheck of view " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> RenderContext -> ViewName -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ViewName
viewName Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
":"
      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 ErrorSrcPos
ics NonEmpty op
instrs ->
      Doc
"Unreachable code:" Doc -> Doc -> Doc
<$$> Int -> [op] -> Doc
buildTruncated Int
3 (NonEmpty op -> [Element (NonEmpty op)]
forall t. Container t => t -> [Element t]
toList NonEmpty op
instrs) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
      Doc -> Doc -> Doc
<+> (RenderContext -> ErrorSrcPos -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ErrorSrcPos
ics)
    TcExtError (SomeHST HST ts
t) ErrorSrcPos
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 -> ErrorSrcPos -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context ErrorSrcPos
ics)
    TcIncompletelyTyped TcError' op
err Contract' (TypeCheckedOp op)
contract ->
      Doc
line
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> RenderContext -> Contract' (TypeCheckedOp op) -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens Contract' (TypeCheckedOp op)
contract
      Doc -> Doc -> Doc
<$> RenderContext -> TcError' op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TcError' op
err
    TcIncompletelyTypedView TcError' op
err View' (TypeCheckedOp op)
_view ->
      Doc
line
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> RenderContext -> TcError' op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context TcError' op
err
    TcDeprecatedType Text
err T
ty ->
      Doc
"Found deprecated type:" Doc -> Doc -> Doc
<+> RenderContext -> T -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens T
ty Doc -> Doc -> Doc
<$> RenderContext -> Text -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens Text
err
    where
    buildTruncated :: Int -> [op] -> Doc
buildTruncated Int
k [op]
l
      | [op] -> Bool
forall t. Container t => t -> Bool
null (Int -> [op] -> [op]
forall a. Int -> [a] -> [a]
drop Int
k [op]
l) = RenderContext -> [op] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context [op]
l
      | Bool
otherwise = (RenderContext -> [op] -> Doc
forall a. RenderDoc a => RenderContext -> [a] -> Doc
renderDocList RenderContext
context (Int -> [op] -> [op]
forall a. Int -> [a] -> [a]
take Int
k [op]
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 Exception TcError where
  displayException :: TcError -> String
displayException = TcError -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty

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

instance Buildable StackSize where
  build :: StackSize -> Builder
build (StackSize Natural
n) = Builder
"stack size " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Natural
n Natural -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""

-- | Various type errors possible when checking Morley extension commands
data ExtError =
    LengthMismatch U.StackTypePattern
  | TypeMismatch U.StackTypePattern Int TcTypeError
  | StkRestMismatch U.StackTypePattern SomeHST SomeHST TcTypeError
  | TestAssertError Text
  | InvalidStackReference U.StackRef StackSize
  deriving stock (Int -> ExtError -> ShowS
[ExtError] -> ShowS
ExtError -> String
(Int -> ExtError -> ShowS)
-> (ExtError -> String) -> ([ExtError] -> ShowS) -> Show ExtError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtError] -> ShowS
$cshowList :: [ExtError] -> ShowS
show :: ExtError -> String
$cshow :: ExtError -> String
showsPrec :: Int -> ExtError -> ShowS
$cshowsPrec :: Int -> ExtError -> ShowS
Show, 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
""
    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
""
    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. (Buildable 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. (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
""
    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. (Buildable 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. (Buildable 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. (PrettyShow a, Show a, IsString b) => a -> b
show Word
i))