Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




data UnificationResult' a Source


Unifies a

Unification succeeded.

NoUnify TCErr

Terms are not unifiable.

DontKnow TCErr

Some other error happened, unification got stuck.

type UnifyOutput = Unifiable Source

Output the result of unification (success or maybe).

data Unifiable Source

Were two terms unifiable or did we have to postpone some equation such that we are not sure?



Unification succeeded.


Unification did not fail, but we had to postpone a part.


Monoid Unifiable Source

Conjunctive monoid.

MonadWriter UnifyOutput Unify Source 

reportPostponing :: Unify () Source

Tell that something could not be unified right now, so the unification succeeds only Possibly.

ifClean :: Unify () -> Unify a -> Unify a -> Unify a Source

Check whether unification proceeded without postponement.

data Equality Source


Equal TypeHH Term Term 


data UnifyState Source




uniSub :: Sub
uniConstr :: [Equality]

projectionMismatch :: QName -> QName -> Unify a Source

Throw-away error message.

modSub :: (Sub -> Sub) -> Unify () Source

checkEquality :: Type -> Term -> Term -> TCM () Source

Force equality now instead of postponing it using addEquality.

checkEqualityHH :: TypeHH -> Term -> Term -> Unify () Source

Try equality. If constraints remain, postpone (enter unsafe mode). Heterogeneous equalities cannot be tried nor reawakened, so we can throw them away and flag "dirty".

forceHom :: TypeHH -> TCM Type Source

Check whether heterogeneous situation is really homogeneous. If not, give up.

makeHom :: TypeHH -> TCM (Maybe Type) Source

Check whether heterogeneous situation is really homogeneous. If not, return Nothing.

tryHom :: TypeHH -> Term -> Term -> TCM TermHH Source

Try to make a possibly heterogeneous term situation homogeneous.

occursCheck :: Nat -> Term -> Type -> Unify () Source

Includes flexible occurrences, metas need to be solved. TODO: relax? TODO: later solutions may remove flexible occurences

(|->) :: Nat -> (Term, Type) -> Unify () Source

Assignment with preceding occurs check.

class UReduce t where Source

Apply the current substitution on a term and reduce to weak head normal form.


ureduce :: t -> Unify t Source

flattenSubstitution :: Substitution -> Substitution Source

Take a substitution σ and ensure that no variables from the domain appear in the targets. The context of the targets is not changed. TODO: can this be expressed using makeSubstitution and applySubst?

data HomHet a Source

Are we in a homogeneous (one type) or heterogeneous (two types) situation?


Hom a


Het a a


leftHH :: HomHet a -> a Source

absAppHH :: SubstHH t tHH => Abs t -> TermHH -> tHH Source

class ApplyHH t where Source


applyHH :: t -> HomHet Args -> HomHet t Source

substHH :: SubstHH t tHH => TermHH -> t -> tHH Source

class SubstHH t tHH where Source

substHH u t substitutes u for the 0th variable in t.


substUnderHH :: Nat -> TermHH -> t -> tHH Source

trivialHH :: t -> tHH Source


SubstHH Type (HomHet Type) Source 
SubstHH Term (HomHet Term) Source 
SubstHH a b => SubstHH (Tele a) (Tele b) Source 
SubstHH a b => SubstHH (Abs a) (Abs b) Source 
SubstHH a b => SubstHH (Dom a) (Dom b) Source 
SubstHH a b => SubstHH (Arg a) (Arg b) Source 
(Free a, Subst a) => SubstHH (HomHet a) (HomHet a) Source 
(SubstHH a a', SubstHH b b') => SubstHH (a, b) (a', b') Source 

unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> Args -> Args -> tcm Substitution Source

Unify indices.

In unifyIndices_ flex a us vs,

a is the type eliminated by us and vs (usally the type of a constructor), need not be reduced,

us and vs are the argument lists to unify,

flex is the set of flexible (instantiable) variabes in us and vs.

The result is the most general unifier of us and vs.

dataOrRecordType Source


:: ConHead

Constructor name.

-> Type

Type of constructor application (must end in data/record).

-> TCM (Maybe Type)

Type of constructor, applied to pars.

Given the type of a constructor application the corresponding data or record type, applied to its parameters (extracted from the given type), is returned.

Precondition: The type has to correspond to an application of the given constructor.

dataOrRecordType' Source


:: ConHead

Constructor name.

-> Type

Type of constructor application (must end in data/record).

-> TCM (Maybe (QName, Type, Args, Args))

Name of data/record type, type of constructor to be applied, data/record parameters, and data indices

dataOrRecordTypeHH Source


:: ConHead

Constructor name.

-> TypeHH

Type(s) of constructor application (must end in same data/record).

-> TCM (Maybe TypeHH)

Type of constructor, instantiated possibly heterogeneously to parameters.

Heterogeneous situation. a1 and a2 need to end in same datatype/record.

isEtaRecordTypeHH :: MonadTCM tcm => TypeHH -> tcm (Maybe (QName, HomHet Args)) Source

Return record type identifier if argument is a record type.

data ShapeView a Source

Views an expression (pair) as type shape. Fails if not same shape.


PiSh (Dom a) (Abs a) 
FunSh (Dom a) a 
DefSh QName


VarSh Nat

neutral type

LitSh Literal

built-in type


some meta


not a type or not definitely same shape


shapeView :: Type -> Unify (Type, ShapeView Type) Source

Return the type and its shape. Expects input in (u)reduced form.

shapeViewHH :: TypeHH -> Unify (TypeHH, ShapeView TypeHH) Source

Return the reduced type(s) and the common shape.

telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH Source

telViewUpToHH n t takes off the first n function types of t. Takes off all if $n < 0$.