{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- appears in the generated instances

module PlutusCore.Error
  ( ParserError (..)
  , ParserErrorBundle (..)
  , NormCheckError (..)
  , UniqueError (..)
  , ExpectedShapeOr (..)
  , TypeError (..)
  , FreeVariableError (..)
  , Error (..)
  , throwingEither
  , ShowErrorComponent (..)
  , ApplyProgramError (..)
  ) where

import PlutusPrelude

import PlutusCore.Core
import PlutusCore.DeBruijn.Internal
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import Prettyprinter.Custom (sexp)

import Control.Lens hiding (use)
import Control.Monad.Error.Lens
import Control.Monad.Except
import Data.Text qualified as T
import PlutusCore.Annotation (SrcSpan)
import Prettyprinter (hardline, hsep, indent, squotes, (<+>))
import Text.Megaparsec as M
import Universe

-- | Lifts an 'Either' into an error context where we can embed the 'Left' value into the error.
throwingEither :: MonadError e m => AReview e t -> Either t a -> m a
throwingEither :: forall e (m :: * -> *) t a.
MonadError e m =>
AReview e t -> Either t a -> m a
throwingEither AReview e t
r Either t a
e = case Either t a
e of
  Left t
t -> AReview e t -> t -> m a
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e t
r t
t
  Right a
v -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
v

-- | An error encountered during parsing.
data ParserError
  = BuiltinTypeNotAStar !T.Text !SourcePos
  | UnknownBuiltinFunction !T.Text !SourcePos ![T.Text]
  | InvalidBuiltinConstant !T.Text !T.Text !SourcePos
  deriving stock (ParserError -> ParserError -> Bool
(ParserError -> ParserError -> Bool)
-> (ParserError -> ParserError -> Bool) -> Eq ParserError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ParserError -> ParserError -> Bool
== :: ParserError -> ParserError -> Bool
$c/= :: ParserError -> ParserError -> Bool
/= :: ParserError -> ParserError -> Bool
Eq, Eq ParserError
Eq ParserError =>
(ParserError -> ParserError -> Ordering)
-> (ParserError -> ParserError -> Bool)
-> (ParserError -> ParserError -> Bool)
-> (ParserError -> ParserError -> Bool)
-> (ParserError -> ParserError -> Bool)
-> (ParserError -> ParserError -> ParserError)
-> (ParserError -> ParserError -> ParserError)
-> Ord ParserError
ParserError -> ParserError -> Bool
ParserError -> ParserError -> Ordering
ParserError -> ParserError -> ParserError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ParserError -> ParserError -> Ordering
compare :: ParserError -> ParserError -> Ordering
$c< :: ParserError -> ParserError -> Bool
< :: ParserError -> ParserError -> Bool
$c<= :: ParserError -> ParserError -> Bool
<= :: ParserError -> ParserError -> Bool
$c> :: ParserError -> ParserError -> Bool
> :: ParserError -> ParserError -> Bool
$c>= :: ParserError -> ParserError -> Bool
>= :: ParserError -> ParserError -> Bool
$cmax :: ParserError -> ParserError -> ParserError
max :: ParserError -> ParserError -> ParserError
$cmin :: ParserError -> ParserError -> ParserError
min :: ParserError -> ParserError -> ParserError
Ord, (forall x. ParserError -> Rep ParserError x)
-> (forall x. Rep ParserError x -> ParserError)
-> Generic ParserError
forall x. Rep ParserError x -> ParserError
forall x. ParserError -> Rep ParserError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ParserError -> Rep ParserError x
from :: forall x. ParserError -> Rep ParserError x
$cto :: forall x. Rep ParserError x -> ParserError
to :: forall x. Rep ParserError x -> ParserError
Generic)
  deriving anyclass (ParserError -> ()
(ParserError -> ()) -> NFData ParserError
forall a. (a -> ()) -> NFData a
$crnf :: ParserError -> ()
rnf :: ParserError -> ()
NFData)

instance Show ParserError where
  show :: ParserError -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (ParserError -> Doc Any) -> ParserError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParserError -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. ParserError -> Doc ann
pretty

data UniqueError ann
  = MultiplyDefined !Unique !ann !ann
  | IncoherentUsage !Unique !ann !ann
  | FreeVariable !Unique !ann
  deriving stock (Int -> UniqueError ann -> ShowS
[UniqueError ann] -> ShowS
UniqueError ann -> String
(Int -> UniqueError ann -> ShowS)
-> (UniqueError ann -> String)
-> ([UniqueError ann] -> ShowS)
-> Show (UniqueError ann)
forall ann. Show ann => Int -> UniqueError ann -> ShowS
forall ann. Show ann => [UniqueError ann] -> ShowS
forall ann. Show ann => UniqueError ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall ann. Show ann => Int -> UniqueError ann -> ShowS
showsPrec :: Int -> UniqueError ann -> ShowS
$cshow :: forall ann. Show ann => UniqueError ann -> String
show :: UniqueError ann -> String
$cshowList :: forall ann. Show ann => [UniqueError ann] -> ShowS
showList :: [UniqueError ann] -> ShowS
Show, UniqueError ann -> UniqueError ann -> Bool
(UniqueError ann -> UniqueError ann -> Bool)
-> (UniqueError ann -> UniqueError ann -> Bool)
-> Eq (UniqueError ann)
forall ann. Eq ann => UniqueError ann -> UniqueError ann -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall ann. Eq ann => UniqueError ann -> UniqueError ann -> Bool
== :: UniqueError ann -> UniqueError ann -> Bool
$c/= :: forall ann. Eq ann => UniqueError ann -> UniqueError ann -> Bool
/= :: UniqueError ann -> UniqueError ann -> Bool
Eq, (forall x. UniqueError ann -> Rep (UniqueError ann) x)
-> (forall x. Rep (UniqueError ann) x -> UniqueError ann)
-> Generic (UniqueError ann)
forall x. Rep (UniqueError ann) x -> UniqueError ann
forall x. UniqueError ann -> Rep (UniqueError ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ann x. Rep (UniqueError ann) x -> UniqueError ann
forall ann x. UniqueError ann -> Rep (UniqueError ann) x
$cfrom :: forall ann x. UniqueError ann -> Rep (UniqueError ann) x
from :: forall x. UniqueError ann -> Rep (UniqueError ann) x
$cto :: forall ann x. Rep (UniqueError ann) x -> UniqueError ann
to :: forall x. Rep (UniqueError ann) x -> UniqueError ann
Generic, (forall a b. (a -> b) -> UniqueError a -> UniqueError b)
-> (forall a b. a -> UniqueError b -> UniqueError a)
-> Functor UniqueError
forall a b. a -> UniqueError b -> UniqueError a
forall a b. (a -> b) -> UniqueError a -> UniqueError b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UniqueError a -> UniqueError b
fmap :: forall a b. (a -> b) -> UniqueError a -> UniqueError b
$c<$ :: forall a b. a -> UniqueError b -> UniqueError a
<$ :: forall a b. a -> UniqueError b -> UniqueError a
Functor)
  deriving anyclass (UniqueError ann -> ()
(UniqueError ann -> ()) -> NFData (UniqueError ann)
forall ann. NFData ann => UniqueError ann -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall ann. NFData ann => UniqueError ann -> ()
rnf :: UniqueError ann -> ()
NFData)

instance Exception (UniqueError SrcSpan)

data NormCheckError tyname name uni fun ann
  = BadType !ann !(Type tyname uni ann) !T.Text
  | BadTerm !ann !(Term tyname name uni fun ann) !T.Text
  deriving stock ((forall a b.
 (a -> b)
 -> NormCheckError tyname name uni fun a
 -> NormCheckError tyname name uni fun b)
-> (forall a b.
    a
    -> NormCheckError tyname name uni fun b
    -> NormCheckError tyname name uni fun a)
-> Functor (NormCheckError tyname name uni fun)
forall a b.
a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
forall a b.
(a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
fmap :: forall a b.
(a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
<$ :: forall a b.
a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
Functor, (forall x.
 NormCheckError tyname name uni fun ann
 -> Rep (NormCheckError tyname name uni fun ann) x)
-> (forall x.
    Rep (NormCheckError tyname name uni fun ann) x
    -> NormCheckError tyname name uni fun ann)
-> Generic (NormCheckError tyname name uni fun ann)
forall x.
Rep (NormCheckError tyname name uni fun ann) x
-> NormCheckError tyname name uni fun ann
forall x.
NormCheckError tyname name uni fun ann
-> Rep (NormCheckError tyname name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun ann x.
Rep (NormCheckError tyname name uni fun ann) x
-> NormCheckError tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann x.
NormCheckError tyname name uni fun ann
-> Rep (NormCheckError tyname name uni fun ann) x
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
NormCheckError tyname name uni fun ann
-> Rep (NormCheckError tyname name uni fun ann) x
from :: forall x.
NormCheckError tyname name uni fun ann
-> Rep (NormCheckError tyname name uni fun ann) x
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (NormCheckError tyname name uni fun ann) x
-> NormCheckError tyname name uni fun ann
to :: forall x.
Rep (NormCheckError tyname name uni fun ann) x
-> NormCheckError tyname name uni fun ann
Generic)

deriving anyclass instance
  (NFData tyname, NFData name, Closed uni, Everywhere uni NFData, NFData fun, NFData ann)
  => NFData (NormCheckError tyname name uni fun ann)

deriving stock instance
  (Show tyname, Show name, Closed uni, Everywhere uni Show, Show fun, Show ann, GShow uni)
  => Show (NormCheckError tyname name uni fun ann)

deriving stock instance
  ( Eq (Term tyname name uni fun ann)
  , Eq (Type tyname uni ann)
  , GEq uni
  , Closed uni
  , uni `Everywhere` Eq
  , Eq fun
  , Eq ann
  )
  => Eq (NormCheckError tyname name uni fun ann)

{-| This is needed for nice kind/type checking error messages. In some cases the type checker knows
the exact type that an expression has to have for type checking to succeed (see any of
'checkTypeM' functions and its usages), which is what 'ExpectedExact' is suitable for. In other
cases the type checker only cares about the shape of the inferred type, e.g. the type checker
knows that the type of a function has to be @dom -> cod@ for type checking to succeed, but it
doesn't yet care what @dom@ and @cod@ exactly are. Which is what 'ExpectedShape' is useful for as
it allows one to specify the shape of an expected type with some existential variables in it when
it's impossible to provide an exact type. -}
data ExpectedShapeOr a
  = ExpectedShape
      !T.Text
      -- ^ The expected shape potentially referencing existential variables.
      ![T.Text]
      -- ^ The list of existential variables.
  | ExpectedExact !a
  deriving stock (Int -> ExpectedShapeOr a -> ShowS
[ExpectedShapeOr a] -> ShowS
ExpectedShapeOr a -> String
(Int -> ExpectedShapeOr a -> ShowS)
-> (ExpectedShapeOr a -> String)
-> ([ExpectedShapeOr a] -> ShowS)
-> Show (ExpectedShapeOr a)
forall a. Show a => Int -> ExpectedShapeOr a -> ShowS
forall a. Show a => [ExpectedShapeOr a] -> ShowS
forall a. Show a => ExpectedShapeOr a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> ExpectedShapeOr a -> ShowS
showsPrec :: Int -> ExpectedShapeOr a -> ShowS
$cshow :: forall a. Show a => ExpectedShapeOr a -> String
show :: ExpectedShapeOr a -> String
$cshowList :: forall a. Show a => [ExpectedShapeOr a] -> ShowS
showList :: [ExpectedShapeOr a] -> ShowS
Show, ExpectedShapeOr a -> ExpectedShapeOr a -> Bool
(ExpectedShapeOr a -> ExpectedShapeOr a -> Bool)
-> (ExpectedShapeOr a -> ExpectedShapeOr a -> Bool)
-> Eq (ExpectedShapeOr a)
forall a. Eq a => ExpectedShapeOr a -> ExpectedShapeOr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => ExpectedShapeOr a -> ExpectedShapeOr a -> Bool
== :: ExpectedShapeOr a -> ExpectedShapeOr a -> Bool
$c/= :: forall a. Eq a => ExpectedShapeOr a -> ExpectedShapeOr a -> Bool
/= :: ExpectedShapeOr a -> ExpectedShapeOr a -> Bool
Eq, (forall x. ExpectedShapeOr a -> Rep (ExpectedShapeOr a) x)
-> (forall x. Rep (ExpectedShapeOr a) x -> ExpectedShapeOr a)
-> Generic (ExpectedShapeOr a)
forall x. Rep (ExpectedShapeOr a) x -> ExpectedShapeOr a
forall x. ExpectedShapeOr a -> Rep (ExpectedShapeOr a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (ExpectedShapeOr a) x -> ExpectedShapeOr a
forall a x. ExpectedShapeOr a -> Rep (ExpectedShapeOr a) x
$cfrom :: forall a x. ExpectedShapeOr a -> Rep (ExpectedShapeOr a) x
from :: forall x. ExpectedShapeOr a -> Rep (ExpectedShapeOr a) x
$cto :: forall a x. Rep (ExpectedShapeOr a) x -> ExpectedShapeOr a
to :: forall x. Rep (ExpectedShapeOr a) x -> ExpectedShapeOr a
Generic, (forall a b. (a -> b) -> ExpectedShapeOr a -> ExpectedShapeOr b)
-> (forall a b. a -> ExpectedShapeOr b -> ExpectedShapeOr a)
-> Functor ExpectedShapeOr
forall a b. a -> ExpectedShapeOr b -> ExpectedShapeOr a
forall a b. (a -> b) -> ExpectedShapeOr a -> ExpectedShapeOr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ExpectedShapeOr a -> ExpectedShapeOr b
fmap :: forall a b. (a -> b) -> ExpectedShapeOr a -> ExpectedShapeOr b
$c<$ :: forall a b. a -> ExpectedShapeOr b -> ExpectedShapeOr a
<$ :: forall a b. a -> ExpectedShapeOr b -> ExpectedShapeOr a
Functor)
  deriving anyclass (ExpectedShapeOr a -> ()
(ExpectedShapeOr a -> ()) -> NFData (ExpectedShapeOr a)
forall a. NFData a => ExpectedShapeOr a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => ExpectedShapeOr a -> ()
rnf :: ExpectedShapeOr a -> ()
NFData)

data TypeError term uni fun ann
  = KindMismatch
      !ann
      !(Type TyName uni ())
      !(ExpectedShapeOr (Kind ()))
      -- ^ The expected type or the shape of a kind.
      !(Kind ())
      -- ^ The actual kind.
  | TypeMismatch
      !ann
      !term
      !(ExpectedShapeOr (Type TyName uni ()))
      -- ^ The expected type or the shape of a type.
      !(Normalized (Type TyName uni ()))
      -- ^ The actual type.
  | TyNameMismatch !ann !TyName !TyName
  | NameMismatch !ann !Name !Name
  | FreeTypeVariableE !ann !TyName
  | FreeVariableE !ann !Name
  | UnknownBuiltinFunctionE !ann !fun
  | UnsupportedCaseBuiltin !ann !T.Text
  deriving stock (Int -> TypeError term uni fun ann -> ShowS
[TypeError term uni fun ann] -> ShowS
TypeError term uni fun ann -> String
(Int -> TypeError term uni fun ann -> ShowS)
-> (TypeError term uni fun ann -> String)
-> ([TypeError term uni fun ann] -> ShowS)
-> Show (TypeError term uni fun ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show fun, Show ann) =>
Int -> TypeError term uni fun ann -> ShowS
forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show fun, Show ann) =>
[TypeError term uni fun ann] -> ShowS
forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show fun, Show ann) =>
TypeError term uni fun ann -> String
$cshowsPrec :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show fun, Show ann) =>
Int -> TypeError term uni fun ann -> ShowS
showsPrec :: Int -> TypeError term uni fun ann -> ShowS
$cshow :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show fun, Show ann) =>
TypeError term uni fun ann -> String
show :: TypeError term uni fun ann -> String
$cshowList :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show fun, Show ann) =>
[TypeError term uni fun ann] -> ShowS
showList :: [TypeError term uni fun ann] -> ShowS
Show, TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
(TypeError term uni fun ann -> TypeError term uni fun ann -> Bool)
-> (TypeError term uni fun ann
    -> TypeError term uni fun ann -> Bool)
-> Eq (TypeError term uni fun ann)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall term (uni :: * -> *) fun ann.
(GEq uni, Eq term, Eq fun, Eq ann) =>
TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
$c== :: forall term (uni :: * -> *) fun ann.
(GEq uni, Eq term, Eq fun, Eq ann) =>
TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
== :: TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
$c/= :: forall term (uni :: * -> *) fun ann.
(GEq uni, Eq term, Eq fun, Eq ann) =>
TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
/= :: TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
Eq, (forall x.
 TypeError term uni fun ann -> Rep (TypeError term uni fun ann) x)
-> (forall x.
    Rep (TypeError term uni fun ann) x -> TypeError term uni fun ann)
-> Generic (TypeError term uni fun ann)
forall x.
Rep (TypeError term uni fun ann) x -> TypeError term uni fun ann
forall x.
TypeError term uni fun ann -> Rep (TypeError term uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall term (uni :: * -> *) fun ann x.
Rep (TypeError term uni fun ann) x -> TypeError term uni fun ann
forall term (uni :: * -> *) fun ann x.
TypeError term uni fun ann -> Rep (TypeError term uni fun ann) x
$cfrom :: forall term (uni :: * -> *) fun ann x.
TypeError term uni fun ann -> Rep (TypeError term uni fun ann) x
from :: forall x.
TypeError term uni fun ann -> Rep (TypeError term uni fun ann) x
$cto :: forall term (uni :: * -> *) fun ann x.
Rep (TypeError term uni fun ann) x -> TypeError term uni fun ann
to :: forall x.
Rep (TypeError term uni fun ann) x -> TypeError term uni fun ann
Generic, (forall a b.
 (a -> b) -> TypeError term uni fun a -> TypeError term uni fun b)
-> (forall a b.
    a -> TypeError term uni fun b -> TypeError term uni fun a)
-> Functor (TypeError term uni fun)
forall a b.
a -> TypeError term uni fun b -> TypeError term uni fun a
forall a b.
(a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
forall term (uni :: * -> *) fun a b.
a -> TypeError term uni fun b -> TypeError term uni fun a
forall term (uni :: * -> *) fun a b.
(a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall term (uni :: * -> *) fun a b.
(a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
fmap :: forall a b.
(a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
$c<$ :: forall term (uni :: * -> *) fun a b.
a -> TypeError term uni fun b -> TypeError term uni fun a
<$ :: forall a b.
a -> TypeError term uni fun b -> TypeError term uni fun a
Functor)
  deriving anyclass (TypeError term uni fun ann -> ()
(TypeError term uni fun ann -> ())
-> NFData (TypeError term uni fun ann)
forall a. (a -> ()) -> NFData a
forall term (uni :: * -> *) fun ann.
(Closed uni, NFData ann, NFData term, NFData fun) =>
TypeError term uni fun ann -> ()
$crnf :: forall term (uni :: * -> *) fun ann.
(Closed uni, NFData ann, NFData term, NFData fun) =>
TypeError term uni fun ann -> ()
rnf :: TypeError term uni fun ann -> ()
NFData)

-- Make a custom data type and wrap @ParseErrorBundle@ in it so I can use @makeClassyPrisms@
-- on @ParseErrorBundle@.
-- TODO: this can be killed
data ParserErrorBundle
  = ParseErrorB !(ParseErrorBundle T.Text ParserError)
  deriving stock (ParserErrorBundle -> ParserErrorBundle -> Bool
(ParserErrorBundle -> ParserErrorBundle -> Bool)
-> (ParserErrorBundle -> ParserErrorBundle -> Bool)
-> Eq ParserErrorBundle
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ParserErrorBundle -> ParserErrorBundle -> Bool
== :: ParserErrorBundle -> ParserErrorBundle -> Bool
$c/= :: ParserErrorBundle -> ParserErrorBundle -> Bool
/= :: ParserErrorBundle -> ParserErrorBundle -> Bool
Eq, (forall x. ParserErrorBundle -> Rep ParserErrorBundle x)
-> (forall x. Rep ParserErrorBundle x -> ParserErrorBundle)
-> Generic ParserErrorBundle
forall x. Rep ParserErrorBundle x -> ParserErrorBundle
forall x. ParserErrorBundle -> Rep ParserErrorBundle x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ParserErrorBundle -> Rep ParserErrorBundle x
from :: forall x. ParserErrorBundle -> Rep ParserErrorBundle x
$cto :: forall x. Rep ParserErrorBundle x -> ParserErrorBundle
to :: forall x. Rep ParserErrorBundle x -> ParserErrorBundle
Generic)
  deriving anyclass (ParserErrorBundle -> ()
(ParserErrorBundle -> ()) -> NFData ParserErrorBundle
forall a. (a -> ()) -> NFData a
$crnf :: ParserErrorBundle -> ()
rnf :: ParserErrorBundle -> ()
NFData)

instance Pretty ParserErrorBundle where
  pretty :: forall ann. ParserErrorBundle -> Doc ann
pretty (ParseErrorB ParseErrorBundle Text ParserError
err) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text ParserError -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle Text ParserError
err

instance Show ParserErrorBundle where
  show :: ParserErrorBundle -> String
show (ParseErrorB ParseErrorBundle Text ParserError
peb) = ParseErrorBundle Text ParserError -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle Text ParserError
peb

data Error uni fun ann
  = ParseErrorE !ParserErrorBundle
  | UniqueCoherencyErrorE !(UniqueError ann)
  | TypeErrorE !(TypeError (Term TyName Name uni fun ()) uni fun ann)
  | NormCheckErrorE !(NormCheckError TyName Name uni fun ann)
  | FreeVariableErrorE !FreeVariableError
  deriving stock ((forall x. Error uni fun ann -> Rep (Error uni fun ann) x)
-> (forall x. Rep (Error uni fun ann) x -> Error uni fun ann)
-> Generic (Error uni fun ann)
forall x. Rep (Error uni fun ann) x -> Error uni fun ann
forall x. Error uni fun ann -> Rep (Error uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (uni :: * -> *) fun ann x.
Rep (Error uni fun ann) x -> Error uni fun ann
forall (uni :: * -> *) fun ann x.
Error uni fun ann -> Rep (Error uni fun ann) x
$cfrom :: forall (uni :: * -> *) fun ann x.
Error uni fun ann -> Rep (Error uni fun ann) x
from :: forall x. Error uni fun ann -> Rep (Error uni fun ann) x
$cto :: forall (uni :: * -> *) fun ann x.
Rep (Error uni fun ann) x -> Error uni fun ann
to :: forall x. Rep (Error uni fun ann) x -> Error uni fun ann
Generic, (forall a b. (a -> b) -> Error uni fun a -> Error uni fun b)
-> (forall a b. a -> Error uni fun b -> Error uni fun a)
-> Functor (Error uni fun)
forall a b. a -> Error uni fun b -> Error uni fun a
forall a b. (a -> b) -> Error uni fun a -> Error uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (uni :: * -> *) fun a b.
a -> Error uni fun b -> Error uni fun a
forall (uni :: * -> *) fun a b.
(a -> b) -> Error uni fun a -> Error uni fun b
$cfmap :: forall (uni :: * -> *) fun a b.
(a -> b) -> Error uni fun a -> Error uni fun b
fmap :: forall a b. (a -> b) -> Error uni fun a -> Error uni fun b
$c<$ :: forall (uni :: * -> *) fun a b.
a -> Error uni fun b -> Error uni fun a
<$ :: forall a b. a -> Error uni fun b -> Error uni fun a
Functor)

deriving stock instance
  (Eq fun, Eq ann, Closed uni, Everywhere uni Eq, GEq uni, Eq ParserError)
  => Eq (Error uni fun ann)

deriving anyclass instance
  (NFData fun, NFData ann, Closed uni, Everywhere uni NFData, NFData ParserError)
  => NFData (Error uni fun ann)

deriving stock instance
  (Show fun, Show ann, Closed uni, Everywhere uni Show, GShow uni, Show ParserError)
  => Show (Error uni fun ann)

instance Pretty SourcePos where
  pretty :: forall ann. SourcePos -> Doc ann
pretty = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann)
-> (SourcePos -> String) -> SourcePos -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> String
sourcePosPretty

instance Pretty ParserError where
  pretty :: forall ann. ParserError -> Doc ann
pretty (BuiltinTypeNotAStar Text
ty SourcePos
loc) =
    Doc ann
"Expected a type of kind star (to later parse a constant), but got:"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
ty)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SourcePos -> Doc ann
forall ann. SourcePos -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc
  pretty (UnknownBuiltinFunction Text
s SourcePos
loc [Text]
lBuiltin) =
    Doc ann
"Unknown built-in function"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
s)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SourcePos -> Doc ann
forall ann. SourcePos -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"Parsable functions are "
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Text] -> Doc ann
forall ann. [Text] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Text]
lBuiltin
  pretty (InvalidBuiltinConstant Text
c Text
s SourcePos
loc) =
    Doc ann
"Invalid constant"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
c)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of type"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
s)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SourcePos -> Doc ann
forall ann. SourcePos -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc

instance ShowErrorComponent ParserError where
  showErrorComponent :: ParserError -> String
showErrorComponent = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (ParserError -> Doc Any) -> ParserError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParserError -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. ParserError -> Doc ann
pretty

instance Pretty ann => Pretty (UniqueError ann) where
  pretty :: forall ann. UniqueError ann -> Doc ann
pretty (MultiplyDefined Unique
u ann
defd ann
redefd) =
    Doc ann
"Variable"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Unique -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Unique -> Doc ann
pretty Unique
u
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"defined at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
defd
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is redefined at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
redefd
  pretty (IncoherentUsage Unique
u ann
defd ann
use) =
    Doc ann
"Variable"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Unique -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Unique -> Doc ann
pretty Unique
u
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"defined at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
defd
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is used in a different scope at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
use
  pretty (FreeVariable Unique
u ann
use) =
    Doc ann
"Variable" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Unique -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Unique -> Doc ann
pretty Unique
u Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is free at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
use

instance
  ( Pretty ann
  , PrettyBy config (Type tyname uni ann)
  , PrettyBy config (Term tyname name uni fun ann)
  )
  => PrettyBy config (NormCheckError tyname name uni fun ann)
  where
  prettyBy :: forall ann.
config -> NormCheckError tyname name uni fun ann -> Doc ann
prettyBy config
config (BadType ann
ann Type tyname uni ann
ty Text
expct) =
    Doc ann
"Malformed type at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
". Type"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (config -> Type tyname uni ann -> Doc ann
forall ann. config -> Type tyname uni ann -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Type tyname uni ann
ty)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not a"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
expct
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."
  prettyBy config
config (BadTerm ann
ann Term tyname name uni fun ann
t Text
expct) =
    Doc ann
"Malformed term at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
". Term"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (config -> Term tyname name uni fun ann -> Doc ann
forall ann. config -> Term tyname name uni fun ann -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Term tyname name uni fun ann
t)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"is not a"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
expct
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"."

{-| Align a list of existential variables in a pretty way.

>>> :set -XOverloadedStrings
>>> existentialVars []
>>> existentialVars ["'a'"]
 for some 'a'
>>> existentialVars ["'a'", "'b'"]
 for some 'a' and 'b'
>>> existentialVars ["'a'", "'b'", "'c'"]
 for some 'a', 'b' and 'c' -}
existentialVars :: [Doc ann] -> Doc ann
existentialVars :: forall ann. [Doc ann] -> Doc ann
existentialVars [] = Doc ann
""
existentialVars (Doc ann
x0 : [Doc ann]
xs0) = Doc ann
" for some " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> [Doc ann] -> Doc ann
forall {t}. (Semigroup t, IsString t) => t -> [t] -> t
go Doc ann
x0 [Doc ann]
xs0
  where
    go :: t -> [t] -> t
go t
x [] = t
x
    go t
x [t
y] = t
x t -> t -> t
forall a. Semigroup a => a -> a -> a
<> t
" and " t -> t -> t
forall a. Semigroup a => a -> a -> a
<> t
y
    go t
x (t
y : [t]
xs) = t
x t -> t -> t
forall a. Semigroup a => a -> a -> a
<> t
", " t -> t -> t
forall a. Semigroup a => a -> a -> a
<> t -> [t] -> t
go t
y [t]
xs

instance PrettyBy PrettyConfigPlc a => PrettyBy PrettyConfigPlc (ExpectedShapeOr a) where
  prettyBy :: forall ann. PrettyConfigPlc -> ExpectedShapeOr a -> Doc ann
prettyBy PrettyConfigPlc
_ (ExpectedShape Text
shape [Text]
vars) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Doc ann -> [Doc ann] -> Doc ann
forall a. Doc a -> [Doc a] -> Doc a
sexp (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
shape) []) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
existentialVars ((Text -> Doc ann) -> [Text] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (Doc ann -> Doc ann) -> (Text -> Doc ann) -> Text -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty) [Text]
vars)
  prettyBy PrettyConfigPlc
config (ExpectedExact a
thing) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (PrettyConfigPlc -> a -> Doc ann
forall ann. PrettyConfigPlc -> a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config a
thing)

instance
  (Pretty term, PrettyUni uni, Pretty fun, Pretty ann)
  => PrettyBy PrettyConfigPlc (TypeError term uni fun ann)
  where
  prettyBy :: forall ann.
PrettyConfigPlc -> TypeError term uni fun ann -> Doc ann
prettyBy PrettyConfigPlc
config (KindMismatch ann
ann Type TyName uni ()
ty ExpectedShapeOr (Kind ())
shapeOrK Kind ()
k') =
    Doc ann
"Kind mismatch at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"Expected a type of kind"
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (PrettyConfigPlc -> ExpectedShapeOr (Kind ()) -> Doc ann
forall ann. PrettyConfigPlc -> ExpectedShapeOr (Kind ()) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config ExpectedShapeOr (Kind ())
shapeOrK)
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"But found one of kind"
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (PrettyConfigPlc -> Kind () -> Doc ann
forall ann. PrettyConfigPlc -> Kind () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Kind ()
k'))
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"Namely,"
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (PrettyConfigPlc -> Type TyName uni () -> Doc ann
forall ann. PrettyConfigPlc -> Type TyName uni () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Type TyName uni ()
ty))
  prettyBy PrettyConfigPlc
config (TypeMismatch ann
ann term
t ExpectedShapeOr (Type TyName uni ())
shapeOrTy Normalized (Type TyName uni ())
ty') =
    Doc ann
"Type mismatch at"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"Expected a term of type"
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (PrettyConfigPlc -> ExpectedShapeOr (Type TyName uni ()) -> Doc ann
forall ann.
PrettyConfigPlc -> ExpectedShapeOr (Type TyName uni ()) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config ExpectedShapeOr (Type TyName uni ())
shapeOrTy)
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"But found one of type"
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (PrettyConfigPlc -> Normalized (Type TyName uni ()) -> Doc ann
forall ann.
PrettyConfigPlc -> Normalized (Type TyName uni ()) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Normalized (Type TyName uni ())
ty'))
      Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> ( if PrettyConfigPlcOptions -> CondensedErrors
_pcpoCondensedErrors (PrettyConfigPlc -> PrettyConfigPlcOptions
_pcpOptions PrettyConfigPlc
config) CondensedErrors -> CondensedErrors -> Bool
forall a. Eq a => a -> a -> Bool
== CondensedErrors
CondensedErrorsYes
             then Doc ann
forall a. Monoid a => a
mempty
             -- TODO: we should use prettyBy here but the problem is
             -- that `instance PrettyClassic PIR.Term` whereas `instance PrettyPLC PLC.Term`
             else Doc ann
forall ann. Doc ann
hardline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"Namely," Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
hardline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
squotes (term -> Doc ann
forall ann. term -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty term
t))
         )
  prettyBy PrettyConfigPlc
config (FreeTypeVariableE ann
ann TyName
name) =
    Doc ann
"Free type variable at " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
": " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> PrettyConfigPlc -> TyName -> Doc ann
forall ann. PrettyConfigPlc -> TyName -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config TyName
name
  prettyBy PrettyConfigPlc
config (FreeVariableE ann
ann Name
name) =
    Doc ann
"Free variable at " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
": " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> PrettyConfigPlc -> Name -> Doc ann
forall ann. PrettyConfigPlc -> Name -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Name
name
  prettyBy PrettyConfigPlc
_ (UnknownBuiltinFunctionE ann
ann fun
fun) =
    Doc ann
"An unknown built-in function at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> fun -> Doc ann
forall ann. fun -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty fun
fun
  prettyBy PrettyConfigPlc
_ (TyNameMismatch ann
ann TyName
name1 TyName
name2) =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep
      [ Doc ann
"Type-level name mismatch at"
      , ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":"
      , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ TyName
name1 TyName -> Getting Text TyName Text -> Text
forall s a. s -> Getting a s a -> a
^. Getting Text TyName Text
forall a. HasText a => Lens' a Text
Lens' TyName Text
theText
      , Doc ann
"is in scope, but"
      , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ TyName
name2 TyName -> Getting Text TyName Text -> Text
forall s a. s -> Getting a s a -> a
^. Getting Text TyName Text
forall a. HasText a => Lens' a Text
Lens' TyName Text
theText
      , Doc ann
"having the same Unique"
      , Unique -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Unique -> Doc ann
pretty (Unique -> Doc ann) -> Unique -> Doc ann
forall a b. (a -> b) -> a -> b
$ TyName
name1 TyName -> Getting Unique TyName Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique TyName Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' TyName Unique
theUnique
      , Doc ann
"is attempted to be referenced"
      ]
  prettyBy PrettyConfigPlc
_ (NameMismatch ann
ann Name
name1 Name
name2) =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep
      [ Doc ann
"Term-level name mismatch at"
      , ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":"
      , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Name
name1 Name -> Getting Text Name Text -> Text
forall s a. s -> Getting a s a -> a
^. Getting Text Name Text
forall a. HasText a => Lens' a Text
Lens' Name Text
theText
      , Doc ann
"is in scope, but"
      , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann) -> Text -> Doc ann
forall a b. (a -> b) -> a -> b
$ Name
name2 Name -> Getting Text Name Text -> Text
forall s a. s -> Getting a s a -> a
^. Getting Text Name Text
forall a. HasText a => Lens' a Text
Lens' Name Text
theText
      , Doc ann
"having the same Unique"
      , Unique -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Unique -> Doc ann
pretty (Unique -> Doc ann) -> Unique -> Doc ann
forall a b. (a -> b) -> a -> b
$ Name
name1 Name -> Getting Unique Name Unique -> Unique
forall s a. s -> Getting a s a -> a
^. Getting Unique Name Unique
forall name unique. HasUnique name unique => Lens' name Unique
Lens' Name Unique
theUnique
      , Doc ann
"is attempted to be referenced"
      ]
  prettyBy PrettyConfigPlc
_ (UnsupportedCaseBuiltin ann
ann Text
err) =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep
      [ Doc ann
"Unsupported 'case' of a value of a built-in type at"
      , ann -> Doc ann
forall ann. ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ann
ann Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":"
      , Doc ann
forall ann. Doc ann
hardline
      , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
err
      ]

instance
  (PrettyUni uni, Pretty fun, Pretty ann)
  => PrettyBy PrettyConfigPlc (Error uni fun ann)
  where
  prettyBy :: forall ann. PrettyConfigPlc -> Error uni fun ann -> Doc ann
prettyBy PrettyConfigPlc
_ (ParseErrorE ParserErrorBundle
e) = ParserErrorBundle -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ParserErrorBundle -> Doc ann
pretty ParserErrorBundle
e
  prettyBy PrettyConfigPlc
_ (UniqueCoherencyErrorE UniqueError ann
e) = UniqueError ann -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. UniqueError ann -> Doc ann
pretty UniqueError ann
e
  prettyBy PrettyConfigPlc
config (TypeErrorE TypeError (Term TyName Name uni fun ()) uni fun ann
e) = PrettyConfigPlc
-> TypeError (Term TyName Name uni fun ()) uni fun ann -> Doc ann
forall ann.
PrettyConfigPlc
-> TypeError (Term TyName Name uni fun ()) uni fun ann -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config TypeError (Term TyName Name uni fun ()) uni fun ann
e
  prettyBy PrettyConfigPlc
config (NormCheckErrorE NormCheckError TyName Name uni fun ann
e) = PrettyConfigPlc
-> NormCheckError TyName Name uni fun ann -> Doc ann
forall ann.
PrettyConfigPlc
-> NormCheckError TyName Name uni fun ann -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config NormCheckError TyName Name uni fun ann
e
  prettyBy PrettyConfigPlc
_ (FreeVariableErrorE FreeVariableError
e) = FreeVariableError -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FreeVariableError -> Doc ann
pretty FreeVariableError
e

-- | Errors from `applyProgram` for PIR, PLC, UPLC.
data ApplyProgramError
  = MkApplyProgramError Version Version

instance Show ApplyProgramError where
  show :: ApplyProgramError -> String
show (MkApplyProgramError Version
v1 Version
v2) =
    String
"Cannot apply two programs together: the first program has version "
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Version -> String
forall a. Show a => a -> String
show Version
v1
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" but the second program has version "
      String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Version -> String
forall a. Show a => a -> String
show Version
v2

instance Exception ApplyProgramError