{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- | A type for unification errors
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

-- | An error that occurred during unification
data UnifyError t h
    = -- | A universally quantified variable was unified with a
      -- different type
      SkolemUnified (h :# t) (h :# t)
    | -- | A universally quantified variable escapes its scope
      SkolemEscape (h :# t)
    | -- | A term violates constraints that should apply to it
      ConstraintsViolation (t h) (TypeConstraintsOf t)
    | -- | Infinite type encountered. A type occurs within itself
      Occurs (t h) (t h)
    | -- | Unification between two mismatching type structures
      Mismatch (t h) (t h)
    deriving (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
            SkolemUnified GetHyperType h ('AHyperType t)
x GetHyperType h ('AHyperType t)
y -> String -> Doc
Pretty.text String
"SkolemUnified" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
r GetHyperType h ('AHyperType t)
x Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
r GetHyperType h ('AHyperType t)
y
            SkolemEscape GetHyperType h ('AHyperType t)
x -> String -> Doc
Pretty.text String
"SkolemEscape:" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
r GetHyperType h ('AHyperType t)
x
            Mismatch t h
x t h
y -> String -> Doc
Pretty.text String
"Mismatch" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
r t h
x Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
r t h
y
            Occurs t h
x t h
y -> 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
<+> forall a. Pretty a => a -> Doc
r t h
x Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
r TypeConstraintsOf t
y
        where
            haveParens :: Bool
haveParens = Rational
p forall a. Ord a => a -> a -> Bool
> Rational
10
            right :: t h -> Doc
right
                | Bool
haveParens = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0
                | Bool
otherwise = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
p
            r :: Pretty a => a -> Pretty.Doc
            r :: forall a. Pretty a => a -> Doc
r = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11