-- | A type for unification errors

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

-- | An error that occurred during unification
data UnifyError t h
    = SkolemUnified (h :# t) (h :# t)
      -- ^ A universally quantified variable was unified with a
      -- different type
    | SkolemEscape (h :# t)
      -- ^ A universally quantified variable escapes its scope
    | ConstraintsViolation (t h) (TypeConstraintsOf t)
      -- ^ A term violates constraints that should apply to it
    | Occurs (t h) (t h)
      -- ^ Infinite type encountered. A type occurs within itself
    | Mismatch (t h) (t h)
      -- ^ Unification between two mismatching type structures
    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