{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}

-- | Types used by the type inference engine
module Elara.TypeInfer.Type (
    -- * Type Variables
    TypeVariable (..),
    UniqueTyVar,

    -- * Types
    Type (..),
    Polytype (..),
    Monotype (..),
    typeLoc,
    polytypeLoc,
    monotypeLoc,
    functionMonotypeResult,
    functionMonotypeArgs,

    -- * Constraints
    Constraint (..),
    constraintLoc,
    simpleEquality,
    equalityWithContext,
    reduce,
    emptyLocation,

    -- * Data Constructors
    DataCon,

    -- * Axiom Schemes
    AxiomScheme (..),

    -- * Substitution
    Substitution (..),
    Substitutable (..),
    substitution,
)
where

import Data.Kind qualified as Kind
import Data.Map qualified as Map
import Elara.AST.Name
import Elara.AST.Region (SourceRegion, generatedSourceRegion)
import Elara.Data.Pretty (Pretty (..), hsep, parens)
import Elara.Data.Pretty.Styles qualified as Style
import Elara.TypeInfer.Context (InferenceContext)
import Elara.TypeInfer.Unique

data TypeVariable = UnificationVar UniqueTyVar | SkolemVar UniqueTyVar
    deriving ((forall x. TypeVariable -> Rep TypeVariable x)
-> (forall x. Rep TypeVariable x -> TypeVariable)
-> Generic TypeVariable
forall x. Rep TypeVariable x -> TypeVariable
forall x. TypeVariable -> Rep TypeVariable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TypeVariable -> Rep TypeVariable x
from :: forall x. TypeVariable -> Rep TypeVariable x
$cto :: forall x. Rep TypeVariable x -> TypeVariable
to :: forall x. Rep TypeVariable x -> TypeVariable
Generic, Int -> TypeVariable -> ShowS
[TypeVariable] -> ShowS
TypeVariable -> String
(Int -> TypeVariable -> ShowS)
-> (TypeVariable -> String)
-> ([TypeVariable] -> ShowS)
-> Show TypeVariable
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeVariable -> ShowS
showsPrec :: Int -> TypeVariable -> ShowS
$cshow :: TypeVariable -> String
show :: TypeVariable -> String
$cshowList :: [TypeVariable] -> ShowS
showList :: [TypeVariable] -> ShowS
Show, TypeVariable -> TypeVariable -> Bool
(TypeVariable -> TypeVariable -> Bool)
-> (TypeVariable -> TypeVariable -> Bool) -> Eq TypeVariable
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypeVariable -> TypeVariable -> Bool
== :: TypeVariable -> TypeVariable -> Bool
$c/= :: TypeVariable -> TypeVariable -> Bool
/= :: TypeVariable -> TypeVariable -> Bool
Eq, Eq TypeVariable
Eq TypeVariable =>
(TypeVariable -> TypeVariable -> Ordering)
-> (TypeVariable -> TypeVariable -> Bool)
-> (TypeVariable -> TypeVariable -> Bool)
-> (TypeVariable -> TypeVariable -> Bool)
-> (TypeVariable -> TypeVariable -> Bool)
-> (TypeVariable -> TypeVariable -> TypeVariable)
-> (TypeVariable -> TypeVariable -> TypeVariable)
-> Ord TypeVariable
TypeVariable -> TypeVariable -> Bool
TypeVariable -> TypeVariable -> Ordering
TypeVariable -> TypeVariable -> TypeVariable
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 :: TypeVariable -> TypeVariable -> Ordering
compare :: TypeVariable -> TypeVariable -> Ordering
$c< :: TypeVariable -> TypeVariable -> Bool
< :: TypeVariable -> TypeVariable -> Bool
$c<= :: TypeVariable -> TypeVariable -> Bool
<= :: TypeVariable -> TypeVariable -> Bool
$c> :: TypeVariable -> TypeVariable -> Bool
> :: TypeVariable -> TypeVariable -> Bool
$c>= :: TypeVariable -> TypeVariable -> Bool
>= :: TypeVariable -> TypeVariable -> Bool
$cmax :: TypeVariable -> TypeVariable -> TypeVariable
max :: TypeVariable -> TypeVariable -> TypeVariable
$cmin :: TypeVariable -> TypeVariable -> TypeVariable
min :: TypeVariable -> TypeVariable -> TypeVariable
Ord)

-- | A type scheme σ
data Type loc
    = Polytype !(Polytype loc)
    | Lifted (Monotype loc)
    deriving ((forall x. Type loc -> Rep (Type loc) x)
-> (forall x. Rep (Type loc) x -> Type loc) -> Generic (Type loc)
forall x. Rep (Type loc) x -> Type loc
forall x. Type loc -> Rep (Type loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall loc x. Rep (Type loc) x -> Type loc
forall loc x. Type loc -> Rep (Type loc) x
$cfrom :: forall loc x. Type loc -> Rep (Type loc) x
from :: forall x. Type loc -> Rep (Type loc) x
$cto :: forall loc x. Rep (Type loc) x -> Type loc
to :: forall x. Rep (Type loc) x -> Type loc
Generic, Int -> Type loc -> ShowS
[Type loc] -> ShowS
Type loc -> String
(Int -> Type loc -> ShowS)
-> (Type loc -> String) -> ([Type loc] -> ShowS) -> Show (Type loc)
forall loc. Show loc => Int -> Type loc -> ShowS
forall loc. Show loc => [Type loc] -> ShowS
forall loc. Show loc => Type loc -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall loc. Show loc => Int -> Type loc -> ShowS
showsPrec :: Int -> Type loc -> ShowS
$cshow :: forall loc. Show loc => Type loc -> String
show :: Type loc -> String
$cshowList :: forall loc. Show loc => [Type loc] -> ShowS
showList :: [Type loc] -> ShowS
Show, Type loc -> Type loc -> Bool
(Type loc -> Type loc -> Bool)
-> (Type loc -> Type loc -> Bool) -> Eq (Type loc)
forall loc. Eq loc => Type loc -> Type loc -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall loc. Eq loc => Type loc -> Type loc -> Bool
== :: Type loc -> Type loc -> Bool
$c/= :: forall loc. Eq loc => Type loc -> Type loc -> Bool
/= :: Type loc -> Type loc -> Bool
Eq, Eq (Type loc)
Eq (Type loc) =>
(Type loc -> Type loc -> Ordering)
-> (Type loc -> Type loc -> Bool)
-> (Type loc -> Type loc -> Bool)
-> (Type loc -> Type loc -> Bool)
-> (Type loc -> Type loc -> Bool)
-> (Type loc -> Type loc -> Type loc)
-> (Type loc -> Type loc -> Type loc)
-> Ord (Type loc)
Type loc -> Type loc -> Bool
Type loc -> Type loc -> Ordering
Type loc -> Type loc -> Type loc
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
forall loc. Ord loc => Eq (Type loc)
forall loc. Ord loc => Type loc -> Type loc -> Bool
forall loc. Ord loc => Type loc -> Type loc -> Ordering
forall loc. Ord loc => Type loc -> Type loc -> Type loc
$ccompare :: forall loc. Ord loc => Type loc -> Type loc -> Ordering
compare :: Type loc -> Type loc -> Ordering
$c< :: forall loc. Ord loc => Type loc -> Type loc -> Bool
< :: Type loc -> Type loc -> Bool
$c<= :: forall loc. Ord loc => Type loc -> Type loc -> Bool
<= :: Type loc -> Type loc -> Bool
$c> :: forall loc. Ord loc => Type loc -> Type loc -> Bool
> :: Type loc -> Type loc -> Bool
$c>= :: forall loc. Ord loc => Type loc -> Type loc -> Bool
>= :: Type loc -> Type loc -> Bool
$cmax :: forall loc. Ord loc => Type loc -> Type loc -> Type loc
max :: Type loc -> Type loc -> Type loc
$cmin :: forall loc. Ord loc => Type loc -> Type loc -> Type loc
min :: Type loc -> Type loc -> Type loc
Ord)

data Polytype loc
    = Forall loc [UniqueTyVar] (Constraint loc) (Monotype loc)
    deriving ((forall x. Polytype loc -> Rep (Polytype loc) x)
-> (forall x. Rep (Polytype loc) x -> Polytype loc)
-> Generic (Polytype loc)
forall x. Rep (Polytype loc) x -> Polytype loc
forall x. Polytype loc -> Rep (Polytype loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall loc x. Rep (Polytype loc) x -> Polytype loc
forall loc x. Polytype loc -> Rep (Polytype loc) x
$cfrom :: forall loc x. Polytype loc -> Rep (Polytype loc) x
from :: forall x. Polytype loc -> Rep (Polytype loc) x
$cto :: forall loc x. Rep (Polytype loc) x -> Polytype loc
to :: forall x. Rep (Polytype loc) x -> Polytype loc
Generic, Int -> Polytype loc -> ShowS
[Polytype loc] -> ShowS
Polytype loc -> String
(Int -> Polytype loc -> ShowS)
-> (Polytype loc -> String)
-> ([Polytype loc] -> ShowS)
-> Show (Polytype loc)
forall loc. Show loc => Int -> Polytype loc -> ShowS
forall loc. Show loc => [Polytype loc] -> ShowS
forall loc. Show loc => Polytype loc -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall loc. Show loc => Int -> Polytype loc -> ShowS
showsPrec :: Int -> Polytype loc -> ShowS
$cshow :: forall loc. Show loc => Polytype loc -> String
show :: Polytype loc -> String
$cshowList :: forall loc. Show loc => [Polytype loc] -> ShowS
showList :: [Polytype loc] -> ShowS
Show, Polytype loc -> Polytype loc -> Bool
(Polytype loc -> Polytype loc -> Bool)
-> (Polytype loc -> Polytype loc -> Bool) -> Eq (Polytype loc)
forall loc. Eq loc => Polytype loc -> Polytype loc -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall loc. Eq loc => Polytype loc -> Polytype loc -> Bool
== :: Polytype loc -> Polytype loc -> Bool
$c/= :: forall loc. Eq loc => Polytype loc -> Polytype loc -> Bool
/= :: Polytype loc -> Polytype loc -> Bool
Eq, Eq (Polytype loc)
Eq (Polytype loc) =>
(Polytype loc -> Polytype loc -> Ordering)
-> (Polytype loc -> Polytype loc -> Bool)
-> (Polytype loc -> Polytype loc -> Bool)
-> (Polytype loc -> Polytype loc -> Bool)
-> (Polytype loc -> Polytype loc -> Bool)
-> (Polytype loc -> Polytype loc -> Polytype loc)
-> (Polytype loc -> Polytype loc -> Polytype loc)
-> Ord (Polytype loc)
Polytype loc -> Polytype loc -> Bool
Polytype loc -> Polytype loc -> Ordering
Polytype loc -> Polytype loc -> Polytype loc
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
forall loc. Ord loc => Eq (Polytype loc)
forall loc. Ord loc => Polytype loc -> Polytype loc -> Bool
forall loc. Ord loc => Polytype loc -> Polytype loc -> Ordering
forall loc. Ord loc => Polytype loc -> Polytype loc -> Polytype loc
$ccompare :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Ordering
compare :: Polytype loc -> Polytype loc -> Ordering
$c< :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Bool
< :: Polytype loc -> Polytype loc -> Bool
$c<= :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Bool
<= :: Polytype loc -> Polytype loc -> Bool
$c> :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Bool
> :: Polytype loc -> Polytype loc -> Bool
$c>= :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Bool
>= :: Polytype loc -> Polytype loc -> Bool
$cmax :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Polytype loc
max :: Polytype loc -> Polytype loc -> Polytype loc
$cmin :: forall loc. Ord loc => Polytype loc -> Polytype loc -> Polytype loc
min :: Polytype loc -> Polytype loc -> Polytype loc
Ord)

typeLoc :: Type loc -> loc
typeLoc :: forall loc. Type loc -> loc
typeLoc (Polytype Polytype loc
p) = Polytype loc -> loc
forall loc. Polytype loc -> loc
polytypeLoc Polytype loc
p
typeLoc (Lifted Monotype loc
m) = Monotype loc -> loc
forall loc. Monotype loc -> loc
monotypeLoc Monotype loc
m

polytypeLoc :: Polytype loc -> loc
polytypeLoc :: forall loc. Polytype loc -> loc
polytypeLoc (Forall loc
loc [UniqueTyVar]
_ Constraint loc
_ Monotype loc
_) = loc
loc

-- | A constraint Q
data Constraint loc
    = -- | The empty constraint 𝜖
      EmptyConstraint loc
    | -- | The conjunction of two constraints, Q₁ ∧ Q₂
      Conjunction loc (Constraint loc) (Constraint loc)
    | {- | An equality constraint, τ₁ ∼ τ₂
      Now enriched with usage locations and inference context
      -}
      Equality
        { forall loc. Constraint loc -> loc
eqLoc :: loc
        -- ^ Where the constraint was generated
        , forall loc. Constraint loc -> Monotype loc
eqLeft :: Monotype loc
        -- ^ The left-hand side type
        , forall loc. Constraint loc -> Monotype loc
eqRight :: Monotype loc
        -- ^ The right-hand side type
        , forall loc. Constraint loc -> loc
eqLeftUsage :: loc
        -- ^ Where the left type was used/expected
        , forall loc. Constraint loc -> loc
eqRightUsage :: loc
        -- ^ Where the right type was found/provided
        , forall loc. Constraint loc -> Maybe InferenceContext
eqContext :: Maybe InferenceContext
        -- ^ Why we're comparing these types
        }
    deriving ((forall x. Constraint loc -> Rep (Constraint loc) x)
-> (forall x. Rep (Constraint loc) x -> Constraint loc)
-> Generic (Constraint loc)
forall x. Rep (Constraint loc) x -> Constraint loc
forall x. Constraint loc -> Rep (Constraint loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall loc x. Rep (Constraint loc) x -> Constraint loc
forall loc x. Constraint loc -> Rep (Constraint loc) x
$cfrom :: forall loc x. Constraint loc -> Rep (Constraint loc) x
from :: forall x. Constraint loc -> Rep (Constraint loc) x
$cto :: forall loc x. Rep (Constraint loc) x -> Constraint loc
to :: forall x. Rep (Constraint loc) x -> Constraint loc
Generic, Int -> Constraint loc -> ShowS
[Constraint loc] -> ShowS
Constraint loc -> String
(Int -> Constraint loc -> ShowS)
-> (Constraint loc -> String)
-> ([Constraint loc] -> ShowS)
-> Show (Constraint loc)
forall loc. Show loc => Int -> Constraint loc -> ShowS
forall loc. Show loc => [Constraint loc] -> ShowS
forall loc. Show loc => Constraint loc -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall loc. Show loc => Int -> Constraint loc -> ShowS
showsPrec :: Int -> Constraint loc -> ShowS
$cshow :: forall loc. Show loc => Constraint loc -> String
show :: Constraint loc -> String
$cshowList :: forall loc. Show loc => [Constraint loc] -> ShowS
showList :: [Constraint loc] -> ShowS
Show, Constraint loc -> Constraint loc -> Bool
(Constraint loc -> Constraint loc -> Bool)
-> (Constraint loc -> Constraint loc -> Bool)
-> Eq (Constraint loc)
forall loc. Eq loc => Constraint loc -> Constraint loc -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall loc. Eq loc => Constraint loc -> Constraint loc -> Bool
== :: Constraint loc -> Constraint loc -> Bool
$c/= :: forall loc. Eq loc => Constraint loc -> Constraint loc -> Bool
/= :: Constraint loc -> Constraint loc -> Bool
Eq, Eq (Constraint loc)
Eq (Constraint loc) =>
(Constraint loc -> Constraint loc -> Ordering)
-> (Constraint loc -> Constraint loc -> Bool)
-> (Constraint loc -> Constraint loc -> Bool)
-> (Constraint loc -> Constraint loc -> Bool)
-> (Constraint loc -> Constraint loc -> Bool)
-> (Constraint loc -> Constraint loc -> Constraint loc)
-> (Constraint loc -> Constraint loc -> Constraint loc)
-> Ord (Constraint loc)
Constraint loc -> Constraint loc -> Bool
Constraint loc -> Constraint loc -> Ordering
Constraint loc -> Constraint loc -> Constraint loc
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
forall loc. Ord loc => Eq (Constraint loc)
forall loc. Ord loc => Constraint loc -> Constraint loc -> Bool
forall loc. Ord loc => Constraint loc -> Constraint loc -> Ordering
forall loc.
Ord loc =>
Constraint loc -> Constraint loc -> Constraint loc
$ccompare :: forall loc. Ord loc => Constraint loc -> Constraint loc -> Ordering
compare :: Constraint loc -> Constraint loc -> Ordering
$c< :: forall loc. Ord loc => Constraint loc -> Constraint loc -> Bool
< :: Constraint loc -> Constraint loc -> Bool
$c<= :: forall loc. Ord loc => Constraint loc -> Constraint loc -> Bool
<= :: Constraint loc -> Constraint loc -> Bool
$c> :: forall loc. Ord loc => Constraint loc -> Constraint loc -> Bool
> :: Constraint loc -> Constraint loc -> Bool
$c>= :: forall loc. Ord loc => Constraint loc -> Constraint loc -> Bool
>= :: Constraint loc -> Constraint loc -> Bool
$cmax :: forall loc.
Ord loc =>
Constraint loc -> Constraint loc -> Constraint loc
max :: Constraint loc -> Constraint loc -> Constraint loc
$cmin :: forall loc.
Ord loc =>
Constraint loc -> Constraint loc -> Constraint loc
min :: Constraint loc -> Constraint loc -> Constraint loc
Ord)

constraintLoc :: Constraint loc -> loc
constraintLoc :: forall loc. Constraint loc -> loc
constraintLoc (EmptyConstraint loc
loc) = loc
loc
constraintLoc (Conjunction loc
loc Constraint loc
_ Constraint loc
_) = loc
loc
constraintLoc Equality{eqLoc :: forall loc. Constraint loc -> loc
eqLoc = loc
loc} = loc
loc

{- | Smart constructor for simple equality constraints (no context)
Uses the monotype locations as usage locations
-}
simpleEquality :: loc -> Monotype loc -> Monotype loc -> Constraint loc
simpleEquality :: forall loc. loc -> Monotype loc -> Monotype loc -> Constraint loc
simpleEquality loc
loc Monotype loc
left Monotype loc
right =
    Equality
        { eqLoc :: loc
eqLoc = loc
loc
        , eqLeft :: Monotype loc
eqLeft = Monotype loc
left
        , eqRight :: Monotype loc
eqRight = Monotype loc
right
        , eqLeftUsage :: loc
eqLeftUsage = Monotype loc -> loc
forall loc. Monotype loc -> loc
monotypeLoc Monotype loc
left
        , eqRightUsage :: loc
eqRightUsage = Monotype loc -> loc
forall loc. Monotype loc -> loc
monotypeLoc Monotype loc
right
        , eqContext :: Maybe InferenceContext
eqContext = Maybe InferenceContext
forall a. Maybe a
Nothing
        }

-- | Smart constructor for equality constraints with context
equalityWithContext :: loc -> Monotype loc -> Monotype loc -> loc -> loc -> Maybe InferenceContext -> Constraint loc
equalityWithContext :: forall loc.
loc
-> Monotype loc
-> Monotype loc
-> loc
-> loc
-> Maybe InferenceContext
-> Constraint loc
equalityWithContext loc
loc Monotype loc
left Monotype loc
right loc
leftUsage loc
rightUsage Maybe InferenceContext
ctx =
    Equality
        { eqLoc :: loc
eqLoc = loc
loc
        , eqLeft :: Monotype loc
eqLeft = Monotype loc
left
        , eqRight :: Monotype loc
eqRight = Monotype loc
right
        , eqLeftUsage :: loc
eqLeftUsage = loc
leftUsage
        , eqRightUsage :: loc
eqRightUsage = loc
rightUsage
        , eqContext :: Maybe InferenceContext
eqContext = Maybe InferenceContext
ctx
        }

emptyLocation :: SourceRegion
emptyLocation :: SourceRegion
emptyLocation = Maybe String -> SourceRegion
generatedSourceRegion Maybe String
forall a. Maybe a
Nothing

instance {-# OVERLAPPING #-} Monoid (Constraint SourceRegion) where
    mempty :: Constraint SourceRegion
mempty = SourceRegion -> Constraint SourceRegion
forall loc. loc -> Constraint loc
EmptyConstraint SourceRegion
emptyLocation

instance (Monoid loc, Eq loc) => Monoid (Constraint loc) where
    mempty :: Constraint loc
mempty = loc -> Constraint loc
forall loc. loc -> Constraint loc
EmptyConstraint loc
forall a. Monoid a => a
mempty

instance (Eq loc, Semigroup loc) => Semigroup (Constraint loc) where
    (<>) :: (Eq loc, Semigroup loc, HasCallStack) => Constraint loc -> Constraint loc -> Constraint loc
    EmptyConstraint loc
_ <> :: (Eq loc, Semigroup loc, HasCallStack) =>
Constraint loc -> Constraint loc -> Constraint loc
<> Constraint loc
c = Constraint loc
c
    Constraint loc
c <> EmptyConstraint loc
_ = Constraint loc
c
    Constraint loc
c1 <> Constraint loc
c2 | Constraint loc
c1 Constraint loc -> Constraint loc -> Bool
forall a. Eq a => a -> a -> Bool
== Constraint loc
c2 = Constraint loc
c1 -- Reflexivity
    Constraint loc
c1 <> Constraint loc
c2 = loc -> Constraint loc -> Constraint loc -> Constraint loc
forall loc.
loc -> Constraint loc -> Constraint loc -> Constraint loc
Conjunction (Constraint loc -> loc
forall loc. Constraint loc -> loc
constraintLoc Constraint loc
c1) Constraint loc
c1 Constraint loc
c2

reduce :: Constraint a -> Constraint a
reduce :: forall a. Constraint a -> Constraint a
reduce (Conjunction a
l Constraint a
q1 Constraint a
q2) = Constraint a -> Constraint a
forall a. Constraint a -> Constraint a
reduce1 (a -> Constraint a -> Constraint a -> Constraint a
forall loc.
loc -> Constraint loc -> Constraint loc -> Constraint loc
Conjunction a
l (Constraint a -> Constraint a
forall a. Constraint a -> Constraint a
reduce Constraint a
q1) (Constraint a -> Constraint a
forall a. Constraint a -> Constraint a
reduce Constraint a
q2))
  where
    reduce1 :: Constraint loc -> Constraint loc
reduce1 (Conjunction loc
l (EmptyConstraint loc
_) (EmptyConstraint loc
_)) = loc -> Constraint loc
forall loc. loc -> Constraint loc
EmptyConstraint loc
l
    reduce1 (Conjunction loc
_ (EmptyConstraint loc
_) Constraint loc
q) = Constraint loc
q
    reduce1 (Conjunction loc
_ Constraint loc
q (EmptyConstraint{})) = Constraint loc
q
    reduce1 Constraint loc
q = Constraint loc
q
reduce Constraint a
q = Constraint a
q

-- instance Eq loc => Monoid (Constraint loc) where
--     mempty = EmptyConstraint

-- | An axiom scheme QQ
data AxiomScheme loc
    = -- | The empty axiom scheme 𝜖
      EmptyAxiomScheme
    | -- | The conjunction of two axiom schemes, QQ₁ ∧ QQ₂
      ConjunctionAxiomScheme (AxiomScheme loc) (AxiomScheme loc)
    | {- | A universal quantification of an axiom scheme, ∀α. QQ ⇒ QQ
      Practically this could be a declaration like @forall a. Eq a => Eq [a]@
      -}
      ForallAxiomScheme
        -- | Type variable to be quantified
        UniqueTyVar
        -- | Constraint for the quantified variable
        (AxiomScheme loc)
        -- | The axiom
        (AxiomScheme loc)
    deriving ((forall x. AxiomScheme loc -> Rep (AxiomScheme loc) x)
-> (forall x. Rep (AxiomScheme loc) x -> AxiomScheme loc)
-> Generic (AxiomScheme loc)
forall x. Rep (AxiomScheme loc) x -> AxiomScheme loc
forall x. AxiomScheme loc -> Rep (AxiomScheme loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (loc :: k) x. Rep (AxiomScheme loc) x -> AxiomScheme loc
forall k (loc :: k) x. AxiomScheme loc -> Rep (AxiomScheme loc) x
$cfrom :: forall k (loc :: k) x. AxiomScheme loc -> Rep (AxiomScheme loc) x
from :: forall x. AxiomScheme loc -> Rep (AxiomScheme loc) x
$cto :: forall k (loc :: k) x. Rep (AxiomScheme loc) x -> AxiomScheme loc
to :: forall x. Rep (AxiomScheme loc) x -> AxiomScheme loc
Generic, Int -> AxiomScheme loc -> ShowS
[AxiomScheme loc] -> ShowS
AxiomScheme loc -> String
(Int -> AxiomScheme loc -> ShowS)
-> (AxiomScheme loc -> String)
-> ([AxiomScheme loc] -> ShowS)
-> Show (AxiomScheme loc)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (loc :: k). Int -> AxiomScheme loc -> ShowS
forall k (loc :: k). [AxiomScheme loc] -> ShowS
forall k (loc :: k). AxiomScheme loc -> String
$cshowsPrec :: forall k (loc :: k). Int -> AxiomScheme loc -> ShowS
showsPrec :: Int -> AxiomScheme loc -> ShowS
$cshow :: forall k (loc :: k). AxiomScheme loc -> String
show :: AxiomScheme loc -> String
$cshowList :: forall k (loc :: k). [AxiomScheme loc] -> ShowS
showList :: [AxiomScheme loc] -> ShowS
Show, AxiomScheme loc -> AxiomScheme loc -> Bool
(AxiomScheme loc -> AxiomScheme loc -> Bool)
-> (AxiomScheme loc -> AxiomScheme loc -> Bool)
-> Eq (AxiomScheme loc)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
$c== :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
== :: AxiomScheme loc -> AxiomScheme loc -> Bool
$c/= :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
/= :: AxiomScheme loc -> AxiomScheme loc -> Bool
Eq, Eq (AxiomScheme loc)
Eq (AxiomScheme loc) =>
(AxiomScheme loc -> AxiomScheme loc -> Ordering)
-> (AxiomScheme loc -> AxiomScheme loc -> Bool)
-> (AxiomScheme loc -> AxiomScheme loc -> Bool)
-> (AxiomScheme loc -> AxiomScheme loc -> Bool)
-> (AxiomScheme loc -> AxiomScheme loc -> Bool)
-> (AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc)
-> (AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc)
-> Ord (AxiomScheme loc)
AxiomScheme loc -> AxiomScheme loc -> Bool
AxiomScheme loc -> AxiomScheme loc -> Ordering
AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc
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
forall k (loc :: k). Eq (AxiomScheme loc)
forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Ordering
forall k (loc :: k).
AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc
$ccompare :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Ordering
compare :: AxiomScheme loc -> AxiomScheme loc -> Ordering
$c< :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
< :: AxiomScheme loc -> AxiomScheme loc -> Bool
$c<= :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
<= :: AxiomScheme loc -> AxiomScheme loc -> Bool
$c> :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
> :: AxiomScheme loc -> AxiomScheme loc -> Bool
$c>= :: forall k (loc :: k). AxiomScheme loc -> AxiomScheme loc -> Bool
>= :: AxiomScheme loc -> AxiomScheme loc -> Bool
$cmax :: forall k (loc :: k).
AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc
max :: AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc
$cmin :: forall k (loc :: k).
AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc
min :: AxiomScheme loc -> AxiomScheme loc -> AxiomScheme loc
Ord)

-- | A monotype τ
data Monotype (loc :: Kind.Type)
    = -- | A type variable tv
      TypeVar loc TypeVariable
    | -- | A type constructor
      TypeConstructor loc (Qualified TypeName) [Monotype loc]
    | -- | A function type τ₁ → τ₂
      Function loc (Monotype loc) (Monotype loc)
    deriving ((forall x. Monotype loc -> Rep (Monotype loc) x)
-> (forall x. Rep (Monotype loc) x -> Monotype loc)
-> Generic (Monotype loc)
forall x. Rep (Monotype loc) x -> Monotype loc
forall x. Monotype loc -> Rep (Monotype loc) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall loc x. Rep (Monotype loc) x -> Monotype loc
forall loc x. Monotype loc -> Rep (Monotype loc) x
$cfrom :: forall loc x. Monotype loc -> Rep (Monotype loc) x
from :: forall x. Monotype loc -> Rep (Monotype loc) x
$cto :: forall loc x. Rep (Monotype loc) x -> Monotype loc
to :: forall x. Rep (Monotype loc) x -> Monotype loc
Generic, Int -> Monotype loc -> ShowS
[Monotype loc] -> ShowS
Monotype loc -> String
(Int -> Monotype loc -> ShowS)
-> (Monotype loc -> String)
-> ([Monotype loc] -> ShowS)
-> Show (Monotype loc)
forall loc. Show loc => Int -> Monotype loc -> ShowS
forall loc. Show loc => [Monotype loc] -> ShowS
forall loc. Show loc => Monotype loc -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall loc. Show loc => Int -> Monotype loc -> ShowS
showsPrec :: Int -> Monotype loc -> ShowS
$cshow :: forall loc. Show loc => Monotype loc -> String
show :: Monotype loc -> String
$cshowList :: forall loc. Show loc => [Monotype loc] -> ShowS
showList :: [Monotype loc] -> ShowS
Show, Monotype loc -> Monotype loc -> Bool
(Monotype loc -> Monotype loc -> Bool)
-> (Monotype loc -> Monotype loc -> Bool) -> Eq (Monotype loc)
forall loc. Eq loc => Monotype loc -> Monotype loc -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall loc. Eq loc => Monotype loc -> Monotype loc -> Bool
== :: Monotype loc -> Monotype loc -> Bool
$c/= :: forall loc. Eq loc => Monotype loc -> Monotype loc -> Bool
/= :: Monotype loc -> Monotype loc -> Bool
Eq, Eq (Monotype loc)
Eq (Monotype loc) =>
(Monotype loc -> Monotype loc -> Ordering)
-> (Monotype loc -> Monotype loc -> Bool)
-> (Monotype loc -> Monotype loc -> Bool)
-> (Monotype loc -> Monotype loc -> Bool)
-> (Monotype loc -> Monotype loc -> Bool)
-> (Monotype loc -> Monotype loc -> Monotype loc)
-> (Monotype loc -> Monotype loc -> Monotype loc)
-> Ord (Monotype loc)
Monotype loc -> Monotype loc -> Bool
Monotype loc -> Monotype loc -> Ordering
Monotype loc -> Monotype loc -> Monotype loc
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
forall loc. Ord loc => Eq (Monotype loc)
forall loc. Ord loc => Monotype loc -> Monotype loc -> Bool
forall loc. Ord loc => Monotype loc -> Monotype loc -> Ordering
forall loc. Ord loc => Monotype loc -> Monotype loc -> Monotype loc
$ccompare :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Ordering
compare :: Monotype loc -> Monotype loc -> Ordering
$c< :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Bool
< :: Monotype loc -> Monotype loc -> Bool
$c<= :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Bool
<= :: Monotype loc -> Monotype loc -> Bool
$c> :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Bool
> :: Monotype loc -> Monotype loc -> Bool
$c>= :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Bool
>= :: Monotype loc -> Monotype loc -> Bool
$cmax :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Monotype loc
max :: Monotype loc -> Monotype loc -> Monotype loc
$cmin :: forall loc. Ord loc => Monotype loc -> Monotype loc -> Monotype loc
min :: Monotype loc -> Monotype loc -> Monotype loc
Ord)

instance Generic loc => Plated (Monotype loc) (Monotype loc)

monotypeLoc :: Monotype loc -> loc
monotypeLoc :: forall loc. Monotype loc -> loc
monotypeLoc (TypeVar loc
loc TypeVariable
_) = loc
loc
monotypeLoc (TypeConstructor loc
loc Qualified TypeName
_ [Monotype loc]
_) = loc
loc
monotypeLoc (Function loc
loc Monotype loc
_ Monotype loc
_) = loc
loc

functionMonotypeResult :: Monotype loc -> Monotype loc
functionMonotypeResult :: forall loc. Monotype loc -> Monotype loc
functionMonotypeResult = \case
    Function loc
_ Monotype loc
_ Monotype loc
b -> Monotype loc -> Monotype loc
forall loc. Monotype loc -> Monotype loc
functionMonotypeResult Monotype loc
b
    Monotype loc
t -> Monotype loc
t

functionMonotypeArgs :: Monotype loc -> [Monotype loc]
functionMonotypeArgs :: forall loc. Monotype loc -> [Monotype loc]
functionMonotypeArgs = \case
    Function loc
_ Monotype loc
a Monotype loc
b -> Monotype loc
a Monotype loc -> [Monotype loc] -> [Monotype loc]
forall a. a -> [a] -> [a]
: Monotype loc -> [Monotype loc]
forall loc. Monotype loc -> [Monotype loc]
functionMonotypeArgs Monotype loc
b
    Monotype loc
_ -> []

type DataCon = Qualified TypeName

newtype Substitution loc
    = Substitution
        (Map UniqueTyVar (Monotype loc))
    deriving newtype (Semigroup (Substitution loc)
Substitution loc
Semigroup (Substitution loc) =>
Substitution loc
-> (Substitution loc -> Substitution loc -> Substitution loc)
-> ([Substitution loc] -> Substitution loc)
-> Monoid (Substitution loc)
[Substitution loc] -> Substitution loc
Substitution loc -> Substitution loc -> Substitution loc
forall loc. Eq loc => Semigroup (Substitution loc)
forall loc. Eq loc => Substitution loc
forall loc. Eq loc => [Substitution loc] -> Substitution loc
forall loc.
Eq loc =>
Substitution loc -> Substitution loc -> Substitution loc
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: forall loc. Eq loc => Substitution loc
mempty :: Substitution loc
$cmappend :: forall loc.
Eq loc =>
Substitution loc -> Substitution loc -> Substitution loc
mappend :: Substitution loc -> Substitution loc -> Substitution loc
$cmconcat :: forall loc. Eq loc => [Substitution loc] -> Substitution loc
mconcat :: [Substitution loc] -> Substitution loc
Monoid)
    deriving stock (Substitution loc -> Substitution loc -> Bool
(Substitution loc -> Substitution loc -> Bool)
-> (Substitution loc -> Substitution loc -> Bool)
-> Eq (Substitution loc)
forall loc. Eq loc => Substitution loc -> Substitution loc -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall loc. Eq loc => Substitution loc -> Substitution loc -> Bool
== :: Substitution loc -> Substitution loc -> Bool
$c/= :: forall loc. Eq loc => Substitution loc -> Substitution loc -> Bool
/= :: Substitution loc -> Substitution loc -> Bool
Eq, Int -> Substitution loc -> ShowS
[Substitution loc] -> ShowS
Substitution loc -> String
(Int -> Substitution loc -> ShowS)
-> (Substitution loc -> String)
-> ([Substitution loc] -> ShowS)
-> Show (Substitution loc)
forall loc. Show loc => Int -> Substitution loc -> ShowS
forall loc. Show loc => [Substitution loc] -> ShowS
forall loc. Show loc => Substitution loc -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall loc. Show loc => Int -> Substitution loc -> ShowS
showsPrec :: Int -> Substitution loc -> ShowS
$cshow :: forall loc. Show loc => Substitution loc -> String
show :: Substitution loc -> String
$cshowList :: forall loc. Show loc => [Substitution loc] -> ShowS
showList :: [Substitution loc] -> ShowS
Show)

instance Eq loc => Semigroup (Substitution loc) where
    -- When composing s1 <> s2, we need to apply s1 to all types in s2
    Substitution Map UniqueTyVar (Monotype loc)
s1 <> :: Substitution loc -> Substitution loc -> Substitution loc
<> Substitution Map UniqueTyVar (Monotype loc)
s2 =
        Map UniqueTyVar (Monotype loc) -> Substitution loc
forall loc. Map UniqueTyVar (Monotype loc) -> Substitution loc
Substitution (Map UniqueTyVar (Monotype loc) -> Substitution loc)
-> Map UniqueTyVar (Monotype loc) -> Substitution loc
forall a b. (a -> b) -> a -> b
$ (Monotype loc -> Monotype loc)
-> Map UniqueTyVar (Monotype loc) -> Map UniqueTyVar (Monotype loc)
forall a b. (a -> b) -> Map UniqueTyVar a -> Map UniqueTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll (Map UniqueTyVar (Monotype loc) -> Substitution loc
forall loc. Map UniqueTyVar (Monotype loc) -> Substitution loc
Substitution Map UniqueTyVar (Monotype loc)
s1)) Map UniqueTyVar (Monotype loc)
s2 Map UniqueTyVar (Monotype loc)
-> Map UniqueTyVar (Monotype loc) -> Map UniqueTyVar (Monotype loc)
forall a. Semigroup a => a -> a -> a
<> Map UniqueTyVar (Monotype loc)
s1

substitution :: (UniqueTyVar, Monotype loc) -> Substitution loc
substitution :: forall loc. (UniqueTyVar, Monotype loc) -> Substitution loc
substitution = Map UniqueTyVar (Monotype loc) -> Substitution loc
forall loc. Map UniqueTyVar (Monotype loc) -> Substitution loc
Substitution (Map UniqueTyVar (Monotype loc) -> Substitution loc)
-> ((UniqueTyVar, Monotype loc) -> Map UniqueTyVar (Monotype loc))
-> (UniqueTyVar, Monotype loc)
-> Substitution loc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueTyVar, Monotype loc) -> Map UniqueTyVar (Monotype loc)
OneItem (Map UniqueTyVar (Monotype loc))
-> Map UniqueTyVar (Monotype loc)
forall x. One x => OneItem x -> x
one

class Substitutable (a :: Kind.Type -> Kind.Type) loc where
    substitute :: UniqueTyVar -> Monotype loc -> a loc -> a loc

    -- | Apply an entire substitution to a type, recursively until a fixed point is reached
    substituteAll :: Eq (a loc) => Substitution loc -> a loc -> a loc

-- we keep this default impl disabled by default to encourage writing custom efficient implementations
-- substituteAll (Substitution s) a = let subst = foldr (uncurry substitute) a (Map.toList s) in if subst == a then a else defaultSubstituteAll (Substitution s) subst -- recursively apply until we reach a fixed point

instance Eq loc => Substitutable Constraint loc where
    substitute :: UniqueTyVar -> Monotype loc -> Constraint loc -> Constraint loc
substitute UniqueTyVar
_ Monotype loc
_ (EmptyConstraint loc
l) = loc -> Constraint loc
forall loc. loc -> Constraint loc
EmptyConstraint loc
l
    substitute UniqueTyVar
tv Monotype loc
t (Conjunction loc
l Constraint loc
c1 Constraint loc
c2) = loc -> Constraint loc -> Constraint loc -> Constraint loc
forall loc.
loc -> Constraint loc -> Constraint loc -> Constraint loc
Conjunction loc
l (UniqueTyVar -> Monotype loc -> Constraint loc -> Constraint loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Constraint loc
c1) (UniqueTyVar -> Monotype loc -> Constraint loc -> Constraint loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Constraint loc
c2)
    substitute UniqueTyVar
tv Monotype loc
t Equality{loc
Maybe InferenceContext
Monotype loc
eqLoc :: forall loc. Constraint loc -> loc
eqLeft :: forall loc. Constraint loc -> Monotype loc
eqRight :: forall loc. Constraint loc -> Monotype loc
eqLeftUsage :: forall loc. Constraint loc -> loc
eqRightUsage :: forall loc. Constraint loc -> loc
eqContext :: forall loc. Constraint loc -> Maybe InferenceContext
eqLoc :: loc
eqLeft :: Monotype loc
eqRight :: Monotype loc
eqLeftUsage :: loc
eqRightUsage :: loc
eqContext :: Maybe InferenceContext
..} =
        Equality
            { eqLoc :: loc
eqLoc = loc
eqLoc
            , eqLeft :: Monotype loc
eqLeft = UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Monotype loc
eqLeft
            , eqRight :: Monotype loc
eqRight = UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Monotype loc
eqRight
            , eqLeftUsage :: loc
eqLeftUsage = loc
eqLeftUsage
            , eqRightUsage :: loc
eqRightUsage = loc
eqRightUsage
            , eqContext :: Maybe InferenceContext
eqContext = Maybe InferenceContext
eqContext
            }

    substituteAll :: Eq (Constraint loc) =>
Substitution loc -> Constraint loc -> Constraint loc
substituteAll Substitution loc
_ (EmptyConstraint loc
l) = loc -> Constraint loc
forall loc. loc -> Constraint loc
EmptyConstraint loc
l
    substituteAll Substitution loc
s (Conjunction loc
l Constraint loc
c1 Constraint loc
c2) = loc -> Constraint loc -> Constraint loc -> Constraint loc
forall loc.
loc -> Constraint loc -> Constraint loc -> Constraint loc
Conjunction loc
l (Substitution loc -> Constraint loc -> Constraint loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Constraint loc
c1) (Substitution loc -> Constraint loc -> Constraint loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Constraint loc
c2)
    substituteAll Substitution loc
s Equality{loc
Maybe InferenceContext
Monotype loc
eqLoc :: forall loc. Constraint loc -> loc
eqLeft :: forall loc. Constraint loc -> Monotype loc
eqRight :: forall loc. Constraint loc -> Monotype loc
eqLeftUsage :: forall loc. Constraint loc -> loc
eqRightUsage :: forall loc. Constraint loc -> loc
eqContext :: forall loc. Constraint loc -> Maybe InferenceContext
eqLoc :: loc
eqLeft :: Monotype loc
eqRight :: Monotype loc
eqLeftUsage :: loc
eqRightUsage :: loc
eqContext :: Maybe InferenceContext
..} =
        Equality
            { eqLoc :: loc
eqLoc = loc
eqLoc
            , eqLeft :: Monotype loc
eqLeft = Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Monotype loc
eqLeft
            , eqRight :: Monotype loc
eqRight = Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Monotype loc
eqRight
            , eqLeftUsage :: loc
eqLeftUsage = loc
eqLeftUsage
            , eqRightUsage :: loc
eqRightUsage = loc
eqRightUsage
            , eqContext :: Maybe InferenceContext
eqContext = Maybe InferenceContext
eqContext
            }

instance Substitutable Monotype loc where
    substitute :: UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
substitute UniqueTyVar
_ Monotype loc
_ (TypeVar loc
loc (SkolemVar UniqueTyVar
v)) = loc -> TypeVariable -> Monotype loc
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar loc
loc (UniqueTyVar -> TypeVariable
SkolemVar UniqueTyVar
v)
    substitute UniqueTyVar
tv Monotype loc
t (TypeVar loc
_ (UnificationVar UniqueTyVar
v)) | UniqueTyVar
tv UniqueTyVar -> UniqueTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== UniqueTyVar
v = Monotype loc
t
    substitute UniqueTyVar
_ Monotype loc
_ (TypeVar loc
loc TypeVariable
tv) = loc -> TypeVariable -> Monotype loc
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar loc
loc TypeVariable
tv
    substitute UniqueTyVar
tv Monotype loc
t (TypeConstructor loc
loc Qualified TypeName
dc [Monotype loc]
ts) = loc -> Qualified TypeName -> [Monotype loc] -> Monotype loc
forall loc.
loc -> Qualified TypeName -> [Monotype loc] -> Monotype loc
TypeConstructor loc
loc Qualified TypeName
dc (UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t (Monotype loc -> Monotype loc) -> [Monotype loc] -> [Monotype loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Monotype loc]
ts)
    substitute UniqueTyVar
tv Monotype loc
t (Function loc
loc Monotype loc
t1 Monotype loc
t2) = loc -> Monotype loc -> Monotype loc -> Monotype loc
forall loc. loc -> Monotype loc -> Monotype loc -> Monotype loc
Function loc
loc (UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Monotype loc
t1) (UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Monotype loc
t2)

    substituteAll :: Eq (Monotype loc) =>
Substitution loc -> Monotype loc -> Monotype loc
substituteAll (Substitution Map UniqueTyVar (Monotype loc)
m) t :: Monotype loc
t@(TypeVar loc
loc TypeVariable
tv) = case TypeVariable
tv of
        SkolemVar UniqueTyVar
v -> loc -> TypeVariable -> Monotype loc
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar loc
loc (UniqueTyVar -> TypeVariable
SkolemVar UniqueTyVar
v) -- skolems are rigid
        UnificationVar UniqueTyVar
v ->
            -- make sure we recursively apply substitutions until we reach a fixed point
            let r :: Monotype loc
r = case UniqueTyVar
-> Map UniqueTyVar (Monotype loc) -> Maybe (Monotype loc)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup UniqueTyVar
v Map UniqueTyVar (Monotype loc)
m of
                    Just Monotype loc
t' -> Monotype loc
t'
                    Maybe (Monotype loc)
Nothing -> loc -> TypeVariable -> Monotype loc
forall loc. loc -> TypeVariable -> Monotype loc
TypeVar loc
loc (UniqueTyVar -> TypeVariable
UnificationVar UniqueTyVar
v)
             in if Monotype loc
r Monotype loc -> Monotype loc -> Bool
forall a. Eq a => a -> a -> Bool
== Monotype loc
t then Monotype loc
t else Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll (Map UniqueTyVar (Monotype loc) -> Substitution loc
forall loc. Map UniqueTyVar (Monotype loc) -> Substitution loc
Substitution Map UniqueTyVar (Monotype loc)
m) Monotype loc
r
    substituteAll Substitution loc
s (TypeConstructor loc
loc Qualified TypeName
dc [Monotype loc]
ts) = loc -> Qualified TypeName -> [Monotype loc] -> Monotype loc
forall loc.
loc -> Qualified TypeName -> [Monotype loc] -> Monotype loc
TypeConstructor loc
loc Qualified TypeName
dc (Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s (Monotype loc -> Monotype loc) -> [Monotype loc] -> [Monotype loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Monotype loc]
ts)
    substituteAll Substitution loc
s (Function loc
loc Monotype loc
t1 Monotype loc
t2) = loc -> Monotype loc -> Monotype loc -> Monotype loc
forall loc. loc -> Monotype loc -> Monotype loc -> Monotype loc
Function loc
loc (Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Monotype loc
t1) (Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Monotype loc
t2)

instance Substitutable Substitution loc where
    substitute :: UniqueTyVar -> Monotype loc -> Substitution loc -> Substitution loc
substitute UniqueTyVar
tv Monotype loc
t (Substitution Map UniqueTyVar (Monotype loc)
s) = Map UniqueTyVar (Monotype loc) -> Substitution loc
forall loc. Map UniqueTyVar (Monotype loc) -> Substitution loc
Substitution (UniqueTyVar
-> Monotype loc
-> Map UniqueTyVar (Monotype loc)
-> Map UniqueTyVar (Monotype loc)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UniqueTyVar
tv Monotype loc
t Map UniqueTyVar (Monotype loc)
s)

instance Eq loc => Substitutable Type loc where
    substitute :: UniqueTyVar -> Monotype loc -> Type loc -> Type loc
substitute UniqueTyVar
tv Monotype loc
t (Lifted Monotype loc
m) = Monotype loc -> Type loc
forall loc. Monotype loc -> Type loc
Lifted (UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Monotype loc
m)
    substitute UniqueTyVar
tv Monotype loc
t (Polytype (Forall loc
loc [UniqueTyVar]
tvs Constraint loc
c Monotype loc
m)) = Polytype loc -> Type loc
forall loc. Polytype loc -> Type loc
Polytype (loc
-> [UniqueTyVar] -> Constraint loc -> Monotype loc -> Polytype loc
forall loc.
loc
-> [UniqueTyVar] -> Constraint loc -> Monotype loc -> Polytype loc
Forall loc
loc [UniqueTyVar]
tvs (UniqueTyVar -> Monotype loc -> Constraint loc -> Constraint loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Constraint loc
c) (UniqueTyVar -> Monotype loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
Substitutable a loc =>
UniqueTyVar -> Monotype loc -> a loc -> a loc
substitute UniqueTyVar
tv Monotype loc
t Monotype loc
m))

    substituteAll :: Eq (Type loc) => Substitution loc -> Type loc -> Type loc
substituteAll Substitution loc
s (Lifted Monotype loc
m) = Monotype loc -> Type loc
forall loc. Monotype loc -> Type loc
Lifted (Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Monotype loc
m)
    substituteAll Substitution loc
s (Polytype (Forall loc
loc [UniqueTyVar]
tvs Constraint loc
c Monotype loc
m)) = Polytype loc -> Type loc
forall loc. Polytype loc -> Type loc
Polytype (loc
-> [UniqueTyVar] -> Constraint loc -> Monotype loc -> Polytype loc
forall loc.
loc
-> [UniqueTyVar] -> Constraint loc -> Monotype loc -> Polytype loc
Forall loc
loc [UniqueTyVar]
tvs (Substitution loc -> Constraint loc -> Constraint loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Constraint loc
c) (Substitution loc -> Monotype loc -> Monotype loc
forall (a :: * -> *) loc.
(Substitutable a loc, Eq (a loc)) =>
Substitution loc -> a loc -> a loc
substituteAll Substitution loc
s Monotype loc
m))

instance Pretty loc => Pretty (Type loc) where
    pretty :: Type loc -> Doc AnsiStyle
pretty (Polytype Polytype loc
poly) = Polytype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Polytype loc
poly
    pretty (Lifted Monotype loc
m) = Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
m

instance Pretty loc => Pretty (Polytype loc) where
    pretty :: Polytype loc -> Doc AnsiStyle
pretty (Forall loc
_ [UniqueTyVar]
tv Constraint loc
c Monotype loc
m) = Doc AnsiStyle
"∀" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
hsep (UniqueTyVar -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty (UniqueTyVar -> Doc AnsiStyle) -> [UniqueTyVar] -> [Doc AnsiStyle]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UniqueTyVar]
tv) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
". " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Constraint loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Constraint loc
c Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" ⇒ " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
m

instance Pretty loc => Pretty (Constraint loc) where
    pretty :: Constraint loc -> Doc AnsiStyle
pretty EmptyConstraint{} = Doc AnsiStyle -> Doc AnsiStyle
Style.builtin Doc AnsiStyle
"𝜖"
    pretty (Conjunction loc
_ EmptyConstraint{} Constraint loc
c) = Constraint loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Constraint loc
c
    pretty (Conjunction loc
_ Constraint loc
c EmptyConstraint{}) = Constraint loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Constraint loc
c
    pretty (Conjunction loc
_ Constraint loc
c1 Constraint loc
c2) = Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
parens (Constraint loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Constraint loc
c1) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" ∧ " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
parens (Constraint loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Constraint loc
c2)
    pretty Equality{eqLeft :: forall loc. Constraint loc -> Monotype loc
eqLeft = Monotype loc
m1, eqRight :: forall loc. Constraint loc -> Monotype loc
eqRight = Monotype loc
m2} = Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
m1 Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" ∼ " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
m2

instance Pretty (Monotype loc) where
    pretty :: Monotype loc -> Doc AnsiStyle
pretty (TypeVar loc
_ TypeVariable
tv) = Doc AnsiStyle -> Doc AnsiStyle
Style.varName (TypeVariable -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty TypeVariable
tv)
    pretty (TypeConstructor loc
_ Qualified TypeName
dc [Monotype loc]
ts) = Doc AnsiStyle -> Doc AnsiStyle
Style.typeName (Qualified TypeName -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Qualified TypeName
dc) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
hsep (Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty (Monotype loc -> Doc AnsiStyle)
-> [Monotype loc] -> [Doc AnsiStyle]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Monotype loc]
ts)
    pretty (Function loc
_ f :: Monotype loc
f@(Function{}) Monotype loc
t3) = Doc AnsiStyle -> Doc AnsiStyle
forall ann. Doc ann -> Doc ann
parens (Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
f) Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle -> Doc AnsiStyle
Style.operator Doc AnsiStyle
" → " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
t3
    pretty (Function loc
_ Monotype loc
t1 Monotype loc
t2) = Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
t1 Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle -> Doc AnsiStyle
Style.operator Doc AnsiStyle
" → " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Monotype loc -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty Monotype loc
t2

instance Pretty TypeVariable where
    pretty :: TypeVariable -> Doc AnsiStyle
pretty (UnificationVar UniqueTyVar
tv) = UniqueTyVar -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty UniqueTyVar
tv
    pretty (SkolemVar UniqueTyVar
tv) = Doc AnsiStyle
"#" Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> UniqueTyVar -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty UniqueTyVar
tv

instance Pretty (Substitution loc) where
    pretty :: Substitution loc -> Doc AnsiStyle
pretty (Substitution Map UniqueTyVar (Monotype loc)
s) = [Doc AnsiStyle] -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty (((UniqueTyVar, Monotype loc) -> Doc AnsiStyle)
-> [(UniqueTyVar, Monotype loc)] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UniqueTyVar, Monotype loc) -> Doc AnsiStyle
forall {a} {a}. (Pretty a, Pretty a) => (a, a) -> Doc AnsiStyle
prettySubstitution (Map UniqueTyVar (Monotype loc) -> [(UniqueTyVar, Monotype loc)]
forall k a. Map k a -> [(k, a)]
Map.toList Map UniqueTyVar (Monotype loc)
s))
      where
        prettySubstitution :: (a, a) -> Doc AnsiStyle
prettySubstitution (a
tv, a
t) = a -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty a
tv Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> Doc AnsiStyle
" ↦ " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle
forall a. Semigroup a => a -> a -> a
<> a -> Doc AnsiStyle
forall a. Pretty a => a -> Doc AnsiStyle
pretty a
t