Agda.TypeChecking.Rules.LHS.Unify

Documentation

newtype Unify a

Constructors

U

Fields

unUnify :: ExceptionT UnifyException (StateT UnifyState TCM) a

Instances

Monad Unify

Functor Unify

Applicative Unify

MonadIO Unify

MonadTCM Unify

MonadReader TCEnv Unify

MonadState TCState Unify

MonadException UnifyException Unify

data Equality

Constructors

Equal Type Term Term

Instances

Subst Equality

type Sub = Map Nat Term

data UnifyException

Constructors

ConstructorMismatch Type Term Term

GenericUnifyException String

Instances

Error UnifyException

MonadException UnifyException Unify

data UnifyState

Constructors

USt

Fields

uniSub :: Sub

uniConstr :: [Equality]

constructorMismatch :: Type -> Term -> Term -> Unify a

getSub :: Unify Sub

onSub :: (Sub -> a) -> Unify a

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

checkEqualities :: [Equality] -> TCM ()

addEquality :: Type -> Term -> Term -> Unify ()

takeEqualities :: Unify [Equality]

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

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

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

makeSubstitution :: Sub -> [Term]

ureduce :: Term -> Unify Term

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

flattenSubstitution :: Substitution -> Substitution

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 substs?

data UnificationResult

Constructors

Unifies Substitution

NoUnify Type Term Term

DontKnow TCErr

unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution

Unify indices.

unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult

dataOrRecordType

Arguments

:: MonadTCM tcm

=> QName

Constructor name.

-> Type

-> tcm Type

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.