{-# LANGUAGE TemplateHaskell, UndecidableInstances #-}
module Hyper.Unify.Error
( UnifyError(..)
, _SkolemUnified, _SkolemEscape, _ConstraintsViolation
, _Occurs, _Mismatch
) where
import Generics.Constraints (Constraints)
import Hyper
import Hyper.Unify.Constraints (TypeConstraintsOf)
import Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)
import Hyper.Internal.Prelude
data UnifyError t h
= SkolemUnified (h :# t) (h :# t)
| SkolemEscape (h :# t)
| ConstraintsViolation (t h) (TypeConstraintsOf t)
| Occurs (t h) (t h)
| Mismatch (t h) (t h)
deriving (forall x. UnifyError t h -> Rep (UnifyError t h) x)
-> (forall x. Rep (UnifyError t h) x -> UnifyError t h)
-> Generic (UnifyError t h)
forall x. Rep (UnifyError t h) x -> UnifyError t h
forall x. UnifyError t h -> Rep (UnifyError t h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: HyperType) (h :: AHyperType) x.
Rep (UnifyError t h) x -> UnifyError t h
forall (t :: HyperType) (h :: AHyperType) x.
UnifyError t h -> Rep (UnifyError t h) x
$cto :: forall (t :: HyperType) (h :: AHyperType) x.
Rep (UnifyError t h) x -> UnifyError t h
$cfrom :: forall (t :: HyperType) (h :: AHyperType) x.
UnifyError t h -> Rep (UnifyError t h) x
Generic
makePrisms ''UnifyError
makeCommonInstances [''UnifyError]
makeHTraversableAndBases ''UnifyError
instance Constraints (UnifyError t h) Pretty => Pretty (UnifyError t h) where
pPrintPrec :: PrettyLevel -> Rational -> UnifyError t h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p =
Bool -> Doc -> Doc
maybeParens Bool
haveParens (Doc -> Doc) -> (UnifyError t h -> Doc) -> UnifyError t h -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
SkolemUnified h :# t
x h :# t
y -> String -> Doc
Pretty.text String
"SkolemUnified" Doc -> Doc -> Doc
<+> (h :# t) -> Doc
forall a. Pretty a => a -> Doc
r h :# t
x Doc -> Doc -> Doc
<+> (h :# t) -> Doc
forall a. Pretty a => a -> Doc
r h :# t
y
SkolemEscape h :# t
x -> String -> Doc
Pretty.text String
"SkolemEscape:" Doc -> Doc -> Doc
<+> (h :# t) -> Doc
forall a. Pretty a => a -> Doc
r h :# t
x
Mismatch t h
x t h
y -> String -> Doc
Pretty.text String
"Mismatch" Doc -> Doc -> Doc
<+> t h -> Doc
forall a. Pretty a => a -> Doc
r t h
x Doc -> Doc -> Doc
<+> t h -> Doc
forall a. Pretty a => a -> Doc
r t h
y
Occurs t h
x t h
y -> t h -> Doc
forall a. Pretty a => a -> Doc
r t h
x Doc -> Doc -> Doc
<+> String -> Doc
Pretty.text String
"occurs in itself, expands to:" Doc -> Doc -> Doc
<+> t h -> Doc
right t h
y
ConstraintsViolation t h
x TypeConstraintsOf t
y -> String -> Doc
Pretty.text String
"ConstraintsViolation" Doc -> Doc -> Doc
<+> t h -> Doc
forall a. Pretty a => a -> Doc
r t h
x Doc -> Doc -> Doc
<+> TypeConstraintsOf t -> Doc
forall a. Pretty a => a -> Doc
r TypeConstraintsOf t
y
where
haveParens :: Bool
haveParens = Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
10
right :: t h -> Doc
right
| Bool
haveParens = PrettyLevel -> Rational -> t h -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0
| Bool
otherwise = PrettyLevel -> Rational -> t h -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
p
r :: Pretty a => a -> Pretty.Doc
r :: a -> Doc
r = PrettyLevel -> Rational -> a -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11