{-# 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 (..)
    , AsParserErrorBundle (..)
    , ParserErrorBundle (..)
    , NormCheckError (..)
    , AsNormCheckError (..)
    , UniqueError (..)
    , AsUniqueError (..)
    , ExpectedShapeOr (..)
    , TypeError (..)
    , AsTypeError (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , Error (..)
    , AsError (..)
    , 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
    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 ann, Show fun) =>
Int -> TypeError term uni fun ann -> ShowS
forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show ann, Show fun) =>
[TypeError term uni fun ann] -> ShowS
forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show ann, Show fun) =>
TypeError term uni fun ann -> String
$cshowsPrec :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show ann, Show fun) =>
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 ann, Show fun) =>
TypeError term uni fun ann -> String
show :: TypeError term uni fun ann -> String
$cshowList :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show term, Show ann, Show fun) =>
[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 ann, Eq fun) =>
TypeError term uni fun ann -> TypeError term uni fun ann -> Bool
$c== :: forall term (uni :: * -> *) fun ann.
(GEq uni, Eq term, Eq ann, Eq fun) =>
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 ann, Eq fun) =>
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@.
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"
        ]

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

makeClassyPrisms ''ParseError
makeClassyPrisms ''ParserErrorBundle
makeClassyPrisms ''UniqueError
makeClassyPrisms ''NormCheckError
makeClassyPrisms ''TypeError
makeClassyPrisms ''Error

instance AsParserErrorBundle (Error uni fun ann) where
    _ParserErrorBundle :: Prism' (Error uni fun ann) ParserErrorBundle
_ParserErrorBundle = p ParserErrorBundle (f ParserErrorBundle)
-> p (Error uni fun ann) (f (Error uni fun ann))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r ParserErrorBundle
Prism' (Error uni fun ann) ParserErrorBundle
_ParseErrorE

instance AsUniqueError (Error uni fun ann) ann where
    _UniqueError :: Prism' (Error uni fun ann) (UniqueError ann)
_UniqueError = p (UniqueError ann) (f (UniqueError ann))
-> p (Error uni fun ann) (f (Error uni fun ann))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r (UniqueError ann)
Prism' (Error uni fun ann) (UniqueError ann)
_UniqueCoherencyErrorE

instance AsTypeError (Error uni fun ann) (Term TyName Name uni fun ()) uni fun ann where
    _TypeError :: Prism'
  (Error uni fun ann)
  (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeError = p (TypeError (Term TyName Name uni fun ()) uni fun ann)
  (f (TypeError (Term TyName Name uni fun ()) uni fun ann))
-> p (Error uni fun ann) (f (Error uni fun ann))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r (TypeError (Term TyName Name uni fun ()) uni fun ann)
Prism'
  (Error uni fun ann)
  (TypeError (Term TyName Name uni fun ()) uni fun ann)
_TypeErrorE

instance (tyname ~ TyName, name ~ Name) =>
            AsNormCheckError (Error uni fun ann) tyname name uni fun ann where
    _NormCheckError :: Prism' (Error uni fun ann) (NormCheckError tyname name uni fun ann)
_NormCheckError = p (NormCheckError tyname name uni fun ann)
  (f (NormCheckError tyname name uni fun ann))
-> p (Error uni fun ann) (f (Error uni fun ann))
p (NormCheckError TyName Name uni fun ann)
  (f (NormCheckError TyName Name uni fun ann))
-> p (Error uni fun ann) (f (Error uni fun ann))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r (NormCheckError TyName Name uni fun ann)
Prism' (Error uni fun ann) (NormCheckError TyName Name uni fun ann)
_NormCheckErrorE

instance AsFreeVariableError (Error uni fun ann) where
    _FreeVariableError :: Prism' (Error uni fun ann) FreeVariableError
_FreeVariableError = p FreeVariableError (f FreeVariableError)
-> p (Error uni fun ann) (f (Error uni fun ann))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r FreeVariableError
Prism' (Error uni fun ann) FreeVariableError
_FreeVariableErrorE

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