Language.Symantic.Typing.Unify

Type Subst

newtype Subst src vs

Type variable substitution.

WARNING: a Subst MUST be without loops, and fully expanded.

Constructors

Subst (Map IndexVar (VT src vs))

Instances

Source src => Show (Subst src vs)

Methods

showsPrec :: Int -> Subst src vs -> ShowS

show :: Subst src vs -> String

showList :: [Subst src vs] -> ShowS

Semigroup (Subst src vs)

Methods

(<>) :: Subst src vs -> Subst src vs -> Subst src vs

sconcat :: NonEmpty (Subst src vs) -> Subst src vs

stimes :: Integral b => b -> Subst src vs -> Subst src vs

Monoid (Subst src vs)

Methods

mempty :: Subst src vs

mappend :: Subst src vs -> Subst src vs -> Subst src vs

mconcat :: [Subst src vs] -> Subst src vs

unionSubst :: Subst src vs -> Subst src vs -> Subst src vs

Unify two Substs.

NOTE: the union is left-biased: in case of duplicate Vars, it keeps the one from the first Subst given.

NOTE: the first Subst given is applied to the second (with subst), this way each Var directly maps to an expanded Type, so that, when using the resulting Subst, there is no need to apply it multiple times until there is no more substitution to be done.

Type VT

data VT src vs

A Var and a Type existentialized over their type index.

Constructors

VT (Var src vs t) (Type src vs t)

Instances

Source src => Show (VT src vs)

Methods

showsPrec :: Int -> VT src vs -> ShowS

show :: VT src vs -> String

showList :: [VT src vs] -> ShowS

insertSubst :: Var src vs v -> Type src vs v -> Subst src vs -> Subst src vs

lookupSubst :: Var src vs v -> Subst src vs -> Maybe (Type src vs v)

Class Substable

class Substable a where

Minimal complete definition

substVarUnsafe, subst

Methods

substVarUnsafe :: src ~ SourceOf a => vs ~ VarsOf a => Var src vs v -> Type src vs v -> a -> a

Like substVar, but without the occurence check.

subst :: src ~ SourceOf a => vs ~ VarsOf a => Subst src vs -> a -> a

Substitute all the Vars which have a match in given Subst.

Instances

Substable (Types src vs ts)

Methods

substVarUnsafe :: ((* ~ src) (SourceOf (Types src vs ts)), ([Type] ~ vs) (VarsOf (Types src vs ts))) => Var kt src vs v -> Type kt src vs v -> Types src vs ts -> Types src vs ts

subst :: ((* ~ src) (SourceOf (Types src vs ts)), ([Type] ~ vs) (VarsOf (Types src vs ts))) => Subst src vs -> Types src vs ts -> Types src vs ts

Substable (Type kt src vs t)

Methods

substVarUnsafe :: ((* ~ src) (SourceOf (Type kt src vs t)), ([Type] ~ vs) (VarsOf (Type kt src vs t))) => Var kt src vs v -> Type kt src vs v -> Type kt src vs t -> Type kt src vs t

subst :: ((* ~ src) (SourceOf (Type kt src vs t)), ([Type] ~ vs) (VarsOf (Type kt src vs t))) => Subst src vs -> Type kt src vs t -> Type kt src vs t

substVar :: src ~ SourceOf a => vs ~ VarsOf a => Source src => VarOccursIn a => Substable a => Var src vs v -> Type src vs v -> a -> Maybe a

Substitute the given Var by the given Type, returning Nothing if this Type contains the Var (occurence check).

Type Error_Unify

data Error_Unify src

Reasons why two Types cannot be unified.

Constructors

Error_Unify_Var_loop IndexVar (TypeVT src)

occurence check: a Var is unified with a Type which contains this same Var.

Error_Unify_Const_mismatch (TypeVT src) (TypeVT src)

Two TyConsts should be the same, but are different.

Error_Unify_Kind_mismatch (KindK src) (KindK src)

Two Kinds should be the same, but are different.

Error_Unify_Kind (Con_Kind src)

Two Kinds mismatch.

Error_Unify_mismatch (TypeVT src) (TypeVT src)

Cannot unify those two Types.

Instances

Source src => Eq (Error_Unify src)

Methods

(==) :: Error_Unify src -> Error_Unify src -> Bool

(/=) :: Error_Unify src -> Error_Unify src -> Bool

Source src => Show (Error_Unify src)

Methods

showsPrec :: Int -> Error_Unify src -> ShowS

show :: Error_Unify src -> String

showList :: [Error_Unify src] -> ShowS

Inj_Error (Con_Kind src) (Error_Unify src)

Methods

inj_Error :: Con_Kind src -> Error_Unify src

Inj_Error (Error_Unify src) (Error_Unify src)

Methods

inj_Error :: Error_Unify src -> Error_Unify src

Inj_Error (Error_Unify src) (Error_Beta src)

Methods

inj_Error :: Error_Unify src -> Error_Beta src

spineTy :: forall src vs t. Source src => Inj_Source (TypeVT src) src => Type src vs t -> (TypeT src vs, [TypeT src vs])

Return the left spine of a Type: the root Type and its Type parameters, from the left to the right.

unifyType :: forall ki x y vs src. Inj_Source (TypeVT src) src => Inj_Error (Con_Kind src) (Error_Unify src) => Subst src vs -> Type src vs (x :: ki) -> Type src vs (y :: ki) -> Either (Error_Unify src) (Subst src vs)

Return the most general unification of two Types, when it exists.