{-# LANGUAGE DeriveAnyClass         #-}
{-# LANGUAGE DerivingStrategies     #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE TemplateHaskell        #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}
-- appears in the generated instances
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module PlutusCore.Error
    ( ParseError (..)
    , AsParseError (..)
    , NormCheckError (..)
    , AsNormCheckError (..)
    , UniqueError (..)
    , AsUniqueError (..)
    , TypeError (..)
    , AsTypeError (..)
    , FreeVariableError (..)
    , AsFreeVariableError (..)
    , Error (..)
    , AsError (..)
    , throwingEither
    , ShowErrorComponent (..)
    ) where

import PlutusPrelude

import PlutusCore.Core
import PlutusCore.DeBruijn.Internal
import PlutusCore.Name
import PlutusCore.Pretty

import Control.Lens hiding (use)
import Control.Monad.Error.Lens
import Control.Monad.Except
import Data.Text qualified as T
import ErrorCode
import Prettyprinter (hardline, indent, squotes, (<+>))
import Text.Megaparsec.Error (ShowErrorComponent, showErrorComponent)
import Text.Megaparsec.Pos (SourcePos, sourcePosPretty)
import Universe (Closed (Everywhere), GEq, GShow)

-- | 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 :: 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 (f :: * -> *) a. Applicative f => a -> f a
pure a
v

-- | An error encountered during parsing.
data ParseError
    = UnknownBuiltinType T.Text SourcePos
    | BuiltinTypeNotAStar T.Text SourcePos
    | UnknownBuiltinFunction T.Text SourcePos
    | InvalidBuiltinConstant T.Text T.Text SourcePos
    deriving stock (ParseError -> ParseError -> Bool
(ParseError -> ParseError -> Bool)
-> (ParseError -> ParseError -> Bool) -> Eq ParseError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ParseError -> ParseError -> Bool
$c/= :: ParseError -> ParseError -> Bool
== :: ParseError -> ParseError -> Bool
$c== :: ParseError -> ParseError -> Bool
Eq, Eq ParseError
Eq ParseError
-> (ParseError -> ParseError -> Ordering)
-> (ParseError -> ParseError -> Bool)
-> (ParseError -> ParseError -> Bool)
-> (ParseError -> ParseError -> Bool)
-> (ParseError -> ParseError -> Bool)
-> (ParseError -> ParseError -> ParseError)
-> (ParseError -> ParseError -> ParseError)
-> Ord ParseError
ParseError -> ParseError -> Bool
ParseError -> ParseError -> Ordering
ParseError -> ParseError -> ParseError
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
min :: ParseError -> ParseError -> ParseError
$cmin :: ParseError -> ParseError -> ParseError
max :: ParseError -> ParseError -> ParseError
$cmax :: ParseError -> ParseError -> ParseError
>= :: ParseError -> ParseError -> Bool
$c>= :: ParseError -> ParseError -> Bool
> :: ParseError -> ParseError -> Bool
$c> :: ParseError -> ParseError -> Bool
<= :: ParseError -> ParseError -> Bool
$c<= :: ParseError -> ParseError -> Bool
< :: ParseError -> ParseError -> Bool
$c< :: ParseError -> ParseError -> Bool
compare :: ParseError -> ParseError -> Ordering
$ccompare :: ParseError -> ParseError -> Ordering
$cp1Ord :: Eq ParseError
Ord, (forall x. ParseError -> Rep ParseError x)
-> (forall x. Rep ParseError x -> ParseError) -> Generic ParseError
forall x. Rep ParseError x -> ParseError
forall x. ParseError -> Rep ParseError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ParseError x -> ParseError
$cfrom :: forall x. ParseError -> Rep ParseError x
Generic)
    deriving anyclass (ParseError -> ()
(ParseError -> ()) -> NFData ParseError
forall a. (a -> ()) -> NFData a
rnf :: ParseError -> ()
$crnf :: ParseError -> ()
NFData)

makeClassyPrisms ''ParseError

instance Show ParseError
    where
      show :: ParseError -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (ParseError -> Doc Any) -> ParseError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> Doc Any
forall a ann. Pretty a => a -> 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
showList :: [UniqueError ann] -> ShowS
$cshowList :: forall ann. Show ann => [UniqueError ann] -> ShowS
show :: UniqueError ann -> String
$cshow :: forall ann. Show ann => UniqueError ann -> String
showsPrec :: Int -> UniqueError ann -> ShowS
$cshowsPrec :: forall ann. Show ann => Int -> 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
/= :: UniqueError ann -> UniqueError ann -> Bool
$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
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
$cto :: forall ann x. Rep (UniqueError ann) x -> UniqueError ann
$cfrom :: forall ann x. UniqueError ann -> Rep (UniqueError ann) x
Generic, a -> UniqueError b -> UniqueError a
(a -> b) -> UniqueError a -> UniqueError b
(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
<$ :: a -> UniqueError b -> UniqueError a
$c<$ :: forall a b. a -> UniqueError b -> UniqueError a
fmap :: (a -> b) -> UniqueError a -> UniqueError b
$cfmap :: forall a b. (a -> b) -> UniqueError a -> UniqueError b
Functor)
    deriving anyclass (UniqueError ann -> ()
(UniqueError ann -> ()) -> NFData (UniqueError ann)
forall ann. NFData ann => UniqueError ann -> ()
forall a. (a -> ()) -> NFData a
rnf :: UniqueError ann -> ()
$crnf :: forall ann. NFData ann => UniqueError ann -> ()
NFData)
makeClassyPrisms ''UniqueError

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 (Int -> NormCheckError tyname name uni fun ann -> ShowS
[NormCheckError tyname name uni fun ann] -> ShowS
NormCheckError tyname name uni fun ann -> String
(Int -> NormCheckError tyname name uni fun ann -> ShowS)
-> (NormCheckError tyname name uni fun ann -> String)
-> ([NormCheckError tyname name uni fun ann] -> ShowS)
-> Show (NormCheckError tyname name uni fun ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show tyname,
 Show name, Show fun) =>
Int -> NormCheckError tyname name uni fun ann -> ShowS
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show tyname,
 Show name, Show fun) =>
[NormCheckError tyname name uni fun ann] -> ShowS
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show tyname,
 Show name, Show fun) =>
NormCheckError tyname name uni fun ann -> String
showList :: [NormCheckError tyname name uni fun ann] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show tyname,
 Show name, Show fun) =>
[NormCheckError tyname name uni fun ann] -> ShowS
show :: NormCheckError tyname name uni fun ann -> String
$cshow :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show tyname,
 Show name, Show fun) =>
NormCheckError tyname name uni fun ann -> String
showsPrec :: Int -> NormCheckError tyname name uni fun ann -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show tyname,
 Show name, Show fun) =>
Int -> NormCheckError tyname name uni fun ann -> ShowS
Show, a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
(a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
(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
<$ :: a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a
-> NormCheckError tyname name uni fun b
-> NormCheckError tyname name uni fun a
fmap :: (a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> NormCheckError tyname name uni fun a
-> NormCheckError tyname name uni fun b
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
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (NormCheckError tyname name uni fun ann) x
-> NormCheckError tyname name uni fun ann
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
NormCheckError tyname name uni fun ann
-> Rep (NormCheckError tyname name uni fun ann) x
Generic)
    deriving anyclass (NormCheckError tyname name uni fun ann -> ()
(NormCheckError tyname name uni fun ann -> ())
-> NFData (NormCheckError tyname name uni fun ann)
forall a. (a -> ()) -> NFData a
forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData tyname,
 NFData name, NFData fun) =>
NormCheckError tyname name uni fun ann -> ()
rnf :: NormCheckError tyname name uni fun ann -> ()
$crnf :: forall tyname name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData tyname,
 NFData name, NFData fun) =>
NormCheckError tyname name uni fun ann -> ()
NFData)
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)
makeClassyPrisms ''NormCheckError

data TypeError term uni fun ann
    = KindMismatch ann (Type TyName uni ()) (Kind ()) (Kind ())
    | TypeMismatch ann
        term
        (Type TyName uni ())
        (Normalized (Type TyName uni ()))
    | 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 ann, Show term, Show fun) =>
Int -> TypeError term uni fun ann -> ShowS
forall term (uni :: * -> *) fun ann.
(GShow uni, Show ann, Show term, Show fun) =>
[TypeError term uni fun ann] -> ShowS
forall term (uni :: * -> *) fun ann.
(GShow uni, Show ann, Show term, Show fun) =>
TypeError term uni fun ann -> String
showList :: [TypeError term uni fun ann] -> ShowS
$cshowList :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show ann, Show term, Show fun) =>
[TypeError term uni fun ann] -> ShowS
show :: TypeError term uni fun ann -> String
$cshow :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show ann, Show term, Show fun) =>
TypeError term uni fun ann -> String
showsPrec :: Int -> TypeError term uni fun ann -> ShowS
$cshowsPrec :: forall term (uni :: * -> *) fun ann.
(GShow uni, Show ann, Show term, Show fun) =>
Int -> 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 ann, Eq term, 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 ann, Eq term, 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 ann, Eq term, Eq fun) =>
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
$cto :: forall term (uni :: * -> *) fun ann x.
Rep (TypeError term uni fun ann) x -> TypeError term uni fun ann
$cfrom :: forall term (uni :: * -> *) fun ann x.
TypeError term uni fun ann -> Rep (TypeError term uni fun ann) x
Generic, a -> TypeError term uni fun b -> TypeError term uni fun a
(a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
(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
<$ :: a -> TypeError term uni fun b -> TypeError term uni fun a
$c<$ :: forall term (uni :: * -> *) fun a b.
a -> TypeError term uni fun b -> TypeError term uni fun a
fmap :: (a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
$cfmap :: forall term (uni :: * -> *) fun a b.
(a -> b) -> TypeError term uni fun a -> TypeError term uni fun b
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 -> ()
rnf :: TypeError term uni fun ann -> ()
$crnf :: forall term (uni :: * -> *) fun ann.
(Closed uni, NFData ann, NFData term, NFData fun) =>
TypeError term uni fun ann -> ()
NFData)
makeClassyPrisms ''TypeError

data Error uni fun ann
    = ParseErrorE ParseError
    | UniqueCoherencyErrorE (UniqueError ann)
    | TypeErrorE (TypeError (Term TyName Name uni fun ()) uni fun ann)
    | NormCheckErrorE (NormCheckError TyName Name uni fun ann)
    | FreeVariableErrorE FreeVariableError
    deriving stock (Error uni fun ann -> Error uni fun ann -> Bool
(Error uni fun ann -> Error uni fun ann -> Bool)
-> (Error uni fun ann -> Error uni fun ann -> Bool)
-> Eq (Error uni fun ann)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (uni :: * -> *) fun ann.
(Everywhere uni Eq, GEq uni, Closed uni, Eq ann, Eq fun) =>
Error uni fun ann -> Error uni fun ann -> Bool
/= :: Error uni fun ann -> Error uni fun ann -> Bool
$c/= :: forall (uni :: * -> *) fun ann.
(Everywhere uni Eq, GEq uni, Closed uni, Eq ann, Eq fun) =>
Error uni fun ann -> Error uni fun ann -> Bool
== :: Error uni fun ann -> Error uni fun ann -> Bool
$c== :: forall (uni :: * -> *) fun ann.
(Everywhere uni Eq, GEq uni, Closed uni, Eq ann, Eq fun) =>
Error uni fun ann -> Error uni fun ann -> Bool
Eq, (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
$cto :: forall (uni :: * -> *) fun ann x.
Rep (Error uni fun ann) x -> Error uni fun ann
$cfrom :: forall (uni :: * -> *) fun ann x.
Error uni fun ann -> Rep (Error uni fun ann) x
Generic, a -> Error uni fun b -> Error uni fun a
(a -> b) -> Error uni fun a -> Error uni fun b
(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
<$ :: a -> Error uni fun b -> Error uni fun a
$c<$ :: forall (uni :: * -> *) fun a b.
a -> Error uni fun b -> Error uni fun a
fmap :: (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
Functor)
    deriving anyclass (Error uni fun ann -> ()
(Error uni fun ann -> ()) -> NFData (Error uni fun ann)
forall a. (a -> ()) -> NFData a
forall (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData fun) =>
Error uni fun ann -> ()
rnf :: Error uni fun ann -> ()
$crnf :: forall (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData fun) =>
Error uni fun ann -> ()
NFData)
makeClassyPrisms ''Error
deriving stock instance (Show fun, Show ann, Closed uni, Everywhere uni Show, GShow uni, Show ParseError) => Show (Error uni fun ann)

instance AsParseError (Error uni fun ann) where
    _ParseError :: p ParseError (f ParseError)
-> p (Error uni fun ann) (f (Error uni fun ann))
_ParseError = p ParseError (f ParseError)
-> p (Error uni fun ann) (f (Error uni fun ann))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r ParseError
_ParseErrorE

instance AsUniqueError (Error uni fun ann) ann where
    _UniqueError :: p (UniqueError ann) (f (UniqueError ann))
-> p (Error uni fun ann) (f (Error uni fun 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)
_UniqueCoherencyErrorE

instance AsTypeError (Error uni fun ann) (Term TyName Name uni fun ()) uni fun ann where
    _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))
_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)
_TypeErrorE

instance (tyname ~ TyName, name ~ Name) =>
            AsNormCheckError (Error uni fun ann) tyname name uni fun ann where
    _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))
_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))
forall r (uni :: * -> *) fun ann.
AsError r uni fun ann =>
Prism' r (NormCheckError TyName Name uni fun ann)
_NormCheckErrorE

instance AsFreeVariableError (Error uni fun ann) where
    _FreeVariableError :: p FreeVariableError (f FreeVariableError)
-> p (Error uni fun ann) (f (Error uni fun ann))
_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
_FreeVariableErrorE

instance Pretty SourcePos where
    pretty :: SourcePos -> Doc ann
pretty = 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 ParseError where
    pretty :: ParseError -> Doc ann
pretty (UnknownBuiltinType Text
s SourcePos
loc)       = Doc ann
"Unknown built-in 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 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 a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc
    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 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 a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc
    pretty (UnknownBuiltinFunction Text
s SourcePos
loc)   = 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 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 a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc
    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 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 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 a ann. Pretty a => a -> Doc ann
pretty SourcePos
loc

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

instance Pretty ann => Pretty (UniqueError ann) where
    pretty :: UniqueError ann -> Doc ann
pretty (MultiplyDefined Unique
u ann
def ann
redef) =
        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
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 a ann. Pretty a => a -> Doc ann
pretty ann
def 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 a ann. Pretty a => a -> Doc ann
pretty ann
redef
    pretty (IncoherentUsage Unique
u ann
def 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
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 a ann. Pretty a => a -> Doc ann
pretty ann
def 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 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
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 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 :: 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 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 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 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 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 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 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
"."

instance (GShow uni, Closed uni, uni `Everywhere` PrettyConst,  Pretty ann, Pretty fun, Pretty term) =>
            PrettyBy PrettyConfigPlc (TypeError term uni fun ann) where
    prettyBy :: PrettyConfigPlc -> TypeError term uni fun ann -> Doc ann
prettyBy PrettyConfigPlc
config e :: TypeError term uni fun ann
e@(KindMismatch ann
ann Type TyName uni ()
ty Kind ()
k Kind ()
k')          =
        ErrorCode -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (TypeError term uni fun ann -> ErrorCode
forall a. HasErrorCode a => a -> ErrorCode
errorCode TypeError term uni fun ann
e) 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
<+>
        Doc ann
"Kind mismatch at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc 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
"in 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 (PrettyConfigPlc -> Type TyName uni () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Type TyName uni ()
ty) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>
        Doc ann
". Expected kind" 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 (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 ann. Doc ann -> Doc ann -> Doc ann
<+>
        Doc ann
", found kind" 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 (PrettyConfigPlc -> Kind () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Kind ()
k')
    prettyBy PrettyConfigPlc
config (TypeMismatch ann
ann term
t Type TyName uni ()
ty 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 a ann. Pretty a => a -> Doc ann
pretty ann
ann 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
" in term" 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 a ann. Pretty a => a -> Doc ann
pretty term
t)) 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
"Expected 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 -> Type TyName uni () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Type TyName uni ()
ty)) 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
"found 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 config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
config Normalized (Type TyName uni ())
ty'))
    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 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 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 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 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 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 a ann. Pretty a => a -> Doc ann
pretty fun
fun

instance (GShow uni, Closed uni, uni `Everywhere` PrettyConst, Pretty fun, Pretty ann) =>
            PrettyBy PrettyConfigPlc (Error uni fun ann) where
    prettyBy :: PrettyConfigPlc -> Error uni fun ann -> Doc ann
prettyBy PrettyConfigPlc
_      (ParseErrorE ParseError
e)           = ParseError -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ParseError
e
    prettyBy PrettyConfigPlc
_      (UniqueCoherencyErrorE UniqueError ann
e) = UniqueError ann -> Doc ann
forall a ann. Pretty a => a -> 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 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 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
pretty FreeVariableError
e

instance HasErrorCode ParseError where
    errorCode :: ParseError -> ErrorCode
errorCode InvalidBuiltinConstant {} = Natural -> ErrorCode
ErrorCode Natural
10
    errorCode UnknownBuiltinFunction {} = Natural -> ErrorCode
ErrorCode Natural
9
    errorCode UnknownBuiltinType {}     = Natural -> ErrorCode
ErrorCode Natural
8
    errorCode BuiltinTypeNotAStar {}    = Natural -> ErrorCode
ErrorCode Natural
51

instance HasErrorCode (UniqueError _a) where
      errorCode :: UniqueError _a -> ErrorCode
errorCode FreeVariable {}    = Natural -> ErrorCode
ErrorCode Natural
21
      errorCode IncoherentUsage {} = Natural -> ErrorCode
ErrorCode Natural
12
      errorCode MultiplyDefined {} = Natural -> ErrorCode
ErrorCode Natural
11

instance HasErrorCode (NormCheckError _a _b _c _d _e) where
      errorCode :: NormCheckError _a _b _c _d _e -> ErrorCode
errorCode BadTerm {} = Natural -> ErrorCode
ErrorCode Natural
14
      errorCode BadType {} = Natural -> ErrorCode
ErrorCode Natural
13

instance HasErrorCode (TypeError _a _b _c _d) where
    errorCode :: TypeError _a _b _c _d -> ErrorCode
errorCode FreeVariableE {}           = Natural -> ErrorCode
ErrorCode Natural
20
    errorCode FreeTypeVariableE {}       = Natural -> ErrorCode
ErrorCode Natural
19
    errorCode TypeMismatch {}            = Natural -> ErrorCode
ErrorCode Natural
16
    errorCode KindMismatch {}            = Natural -> ErrorCode
ErrorCode Natural
15
    errorCode UnknownBuiltinFunctionE {} = Natural -> ErrorCode
ErrorCode Natural
18

instance HasErrorCode (Error _a _b _c) where
    errorCode :: Error _a _b _c -> ErrorCode
errorCode (ParseErrorE ParseError
e)           = ParseError -> ErrorCode
forall a. HasErrorCode a => a -> ErrorCode
errorCode ParseError
e
    errorCode (UniqueCoherencyErrorE UniqueError _c
e) = UniqueError _c -> ErrorCode
forall a. HasErrorCode a => a -> ErrorCode
errorCode UniqueError _c
e
    errorCode (TypeErrorE TypeError (Term TyName Name _a _b ()) _a _b _c
e)            = TypeError (Term TyName Name _a _b ()) _a _b _c -> ErrorCode
forall a. HasErrorCode a => a -> ErrorCode
errorCode TypeError (Term TyName Name _a _b ()) _a _b _c
e
    errorCode (NormCheckErrorE NormCheckError TyName Name _a _b _c
e)       = NormCheckError TyName Name _a _b _c -> ErrorCode
forall a. HasErrorCode a => a -> ErrorCode
errorCode NormCheckError TyName Name _a _b _c
e
    errorCode (FreeVariableErrorE FreeVariableError
e)    = FreeVariableError -> ErrorCode
forall a. HasErrorCode a => a -> ErrorCode
errorCode FreeVariableError
e