Top-1.7: Constraint solving framework employed by the Helium Compiler.

Safe HaskellSafe-Infered



A unification algorithm for types, which can take a list of (ordered) type synonyms into account.



data UnificationError Source

There are two reasons why two types cannot be unified: either two (different) type constants clash (they should be the same), or a type variable should be unified with a composed type that contains this same type variable.

mgu :: Tp -> Tp -> Either UnificationError MapSubstitutionSource

The most general unification (substitution) of two types.

equalUnderTypeSynonyms :: OrderedTypeSynonyms -> Tp -> Tp -> Maybe TpSource

Find the most general type for two types that are equal under type synonyms (i.e., the least number of expansions)

unifiable :: OrderedTypeSynonyms -> Tp -> Tp -> BoolSource

Given a set of (ordered) type synonyms, can two types be unified?

unifiableList :: OrderedTypeSynonyms -> Tps -> BoolSource

Same as unifiable, but takes as input a list of types