Agda.TypeChecking.Rules.LHS.Unify

Unification algorithm for specializing datatype indices, as described in "Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data" by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2016).

This is the unification algorithm used for checking the left-hand side of clauses (see Agda.TypeChecking.Rules.LHS), coverage checking (see Agda.TypeChecking.Coverage) and indirectly also for interactive case splitting (see Agda.Interaction.MakeCase).

A unification problem (of type UnifyState) consists of:

1. A telescope varTel of free variables, some or all of which are flexible (as indicated by flexVars).
2. A telescope eqTel containing the types of the equations.
3. Left- and right-hand sides for each equation: varTel ⊢ eqLHS : eqTel and varTel ⊢ eqRHS : eqTel.

The unification algorithm can end in three different ways: (type UnificationResult):

• A *positive success* Unifies (tel, sigma, ps) with tel ⊢ sigma : varTel, tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel, and tel ⊢ ps : eqTel. In this case, sigma;ps is an *equivalence* between the telescopes tel and varTel(eqLHS ≡ eqRHS).
• A *negative success* NoUnify err means that a conflicting equation was found (e.g an equation between two distinct constructors or a cycle).
• A *failure* UnifyStuck err means that the unifier got stuck.

The unification algorithm itself consists of two parts:

1. A *unification strategy* takes a unification problem and produces a list of suggested unification rules (of type UnifyStep). Strategies can be constructed by composing simpler strategies (see for example the definition of completeStrategyAt).
2. The *unification engine* unifyStep takes a unification rule and tries to apply it to the given state, writing the result to the UnifyOutput on a success.

The unification steps (of type UnifyStep) are the following:

• *Deletion* removes a reflexive equation u =?= v : a if the left- and right-hand side u and v are (definitionally) equal. This rule results in a failure if --without-K is enabled (see "Pattern Matching Without K" by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014).
• *Solution* solves an equation if one side is (eta-equivalent to) a flexible variable. In case both sides are flexible variables, the unification strategy makes a choice according to the chooseFlex function in Agda.TypeChecking.Rules.LHS.Problem.
• *Injectivity* decomposes an equation of the form c us =?= c vs : D pars is where c : Δc → D pars js is a constructor of the inductive datatype D into a sequence of equations us =?= vs : delta. In case D is an indexed datatype,
• higher-dimensional unification* is applied (see below).
• *Conflict* detects absurd equations of the form c₁ us =?= c₂ vs : D pars is where c₁ and c₂ are two distinct constructors of the datatype D.
• *Cycle* detects absurd equations of the form x =?= v : D pars is where x is a variable of the datatype D that occurs strongly rigid in v.
• *EtaExpandVar* eta-expands a single flexible variable x : R where R is a (eta-expandable) record type, replacing it by one variable for each field of R.
• *EtaExpandEquation* eta-expands an equation u =?= v : R where R is a (eta-expandable) record type, replacing it by one equation for each field of R. The left- and right-hand sides of these equations are the projections of u and v.
• *LitConflict* detects absurd equations of the form l₁ =?= l₂ : A where l₁ and l₂ are distinct literal terms.
• *StripSizeSuc* simplifies an equation of the form sizeSuc x =?= sizeSuc y : Size to x =?= y : Size.
• *SkipIrrelevantEquation@ removes an equation between irrelevant terms.
• *TypeConInjectivity* decomposes an equation of the form D us =?= D vs : Set i where D is a datatype. This rule is only used if --injective-type-constructors is enabled.

Higher-dimensional unification (new, does not yet appear in any paper): If an equation of the form c us =?= c vs : D pars is is encountered where c : Δc → D pars js is a constructor of an indexed datatype D pars : Φ → Set ℓ, it is in general unsound to just simplify this equation to us =?= vs : Δc. For this reason, the injectivity rule in the paper restricts the indices is to be distinct variables that are bound in the telescope eqTel. But we can be more general by introducing new variables ks to the telescope eqTel and equating these to is: Δ₁(x : D pars is)Δ₂ ≃ Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂ Since ks are distinct variables, it's now possible to apply injectivity to the equation x, resulting in the following new equation telescope: Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂ Now we can solve the equations ps by recursively calling the unification algorithm with flexible variables Δ₁(ys : Δc). This is called *higher-dimensional unification* since we are unifying equality proofs rather than terms. If the higher-dimensional unification succeeds, the resulting telescope serves as the new equation telescope for the original unification problem.

Documentation

type UnificationResult = UnificationResult' (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern])

Result of unifyIndices.

data UnificationResult' a

Constructors

Unifies a

Unification succeeded.

NoUnify NegativeUnification

Terms are not unifiable.

UnifyBlocked Blocker

Unification got blocked on a metavariable

UnifyStuck [UnificationFailure]

Some other error happened, unification got stuck.

Instances

Foldable UnificationResult'

Defined in Agda.TypeChecking.Rules.LHS.Unify

Methods

fold :: Monoid m => UnificationResult' m -> m

foldMap :: Monoid m => (a -> m) -> UnificationResult' a -> m

foldMap' :: Monoid m => (a -> m) -> UnificationResult' a -> m

foldr :: (a -> b -> b) -> b -> UnificationResult' a -> b

foldr' :: (a -> b -> b) -> b -> UnificationResult' a -> b

foldl :: (b -> a -> b) -> b -> UnificationResult' a -> b

foldl' :: (b -> a -> b) -> b -> UnificationResult' a -> b

foldr1 :: (a -> a -> a) -> UnificationResult' a -> a

foldl1 :: (a -> a -> a) -> UnificationResult' a -> a

toList :: UnificationResult' a -> [a]

null :: UnificationResult' a -> Bool

length :: UnificationResult' a -> Int

elem :: Eq a => a -> UnificationResult' a -> Bool

maximum :: Ord a => UnificationResult' a -> a

minimum :: Ord a => UnificationResult' a -> a

sum :: Num a => UnificationResult' a -> a

product :: Num a => UnificationResult' a -> a

Traversable UnificationResult'

Defined in Agda.TypeChecking.Rules.LHS.Unify

Methods

traverse :: Applicative f => (a -> f b) -> UnificationResult' a -> f (UnificationResult' b)

sequenceA :: Applicative f => UnificationResult' (f a) -> f (UnificationResult' a)

mapM :: Monad m => (a -> m b) -> UnificationResult' a -> m (UnificationResult' b)

sequence :: Monad m => UnificationResult' (m a) -> m (UnificationResult' a)

Functor UnificationResult'

Defined in Agda.TypeChecking.Rules.LHS.Unify

Methods

fmap :: (a -> b) -> UnificationResult' a -> UnificationResult' b

(<$) :: a -> UnificationResult' b -> UnificationResult' a

Show a => Show (UnificationResult' a)

Defined in Agda.TypeChecking.Rules.LHS.Unify

Methods

showsPrec :: Int -> UnificationResult' a -> ShowS

show :: UnificationResult' a -> String

showList :: [UnificationResult' a] -> ShowS

data NoLeftInv

Constructors

UnsupportedYet

Fields

• badStep :: UnifyStep

Illegal

Fields

• badStep :: UnifyStep

NoCubical

WithKEnabled

SplitOnStrict

splitting on a Strict Set.

SplitOnFlat

splitting on a @♭ argument

UnsupportedCxt

Instances

PrettyTCM NoLeftInv

Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Methods

prettyTCM :: MonadPretty m => NoLeftInv -> m Doc

Show NoLeftInv

Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Methods

showsPrec :: Int -> NoLeftInv -> ShowS

show :: NoLeftInv -> String

showList :: [NoLeftInv] -> ShowS

unifyIndices'

Arguments

:: (PureTCM m, MonadError TCErr m)

=> Maybe NoLeftInv

Do we have a reason for not computing a left inverse?

-> Telescope

gamma

-> FlexibleVars

flex

-> Type

a

-> Args

us

-> Args

vs

-> m FullUnificationResult

unifyIndices

Arguments

:: (PureTCM m, MonadBench m, BenchPhase m ~ Phase, MonadError TCErr m)

=> Maybe NoLeftInv

Do we have a reason for not computing a left inverse?

-> Telescope

gamma

-> FlexibleVars

flex

-> Type

a

-> Args

us

-> Args

vs

-> m UnificationResult

Unify indices.

In unifyIndices gamma flex a us vs,

• us and vs are the argument lists to unify, eliminating type a.
• gamma is the telescope of free variables in us and vs.
• flex is the set of flexible (instantiable) variabes in us and vs.

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