Safe Haskell | None |
---|---|

Language | Haskell2010 |

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:

- A telescope
`varTel`

of free variables, some or all of which are flexible (as indicated by`flexVars`

). - A telescope
`eqTel`

containing the types of the equations. - 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*
`DontKnow err`

means that the unifier got stuck.

The unification algorithm itself consists of two parts:

- 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`

). - 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.

## Synopsis

- type UnificationResult = UnificationResult' (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern])
- data UnificationResult' a
- unifyIndices :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult

# Documentation

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

Result of `unifyIndices`

.

data UnificationResult' a Source #

Unifies a | Unification succeeded. |

NoUnify NegativeUnification | Terms are not unifiable. |

DontKnow [UnificationFailure] | Some other error happened, unification got stuck. |

## Instances

:: MonadTCM tcm | |

=> Telescope | gamma |

-> FlexibleVars | flex |

-> Type | a |

-> Args | us |

-> Args | vs |

-> tcm 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`

.