Errata for
Andreas Abel and Brigitte Pientka
Higher-Order Dynamic Pattern Unification for Dependent Types and Records
TLCA 2011
2017-07-02 Andreas Abel: Intersection cannot be extended beyond variable substitutions.
2014-08-04 Andreas Abel: Fix for pruning did not get far enough.
2014-01-15 Andreas Abel: Initial errata.
1. Problem with pruning detected 2011-09-16.
Pruning as described in the paper is overzealous and loses solutions.
Given meta variables
u [x : A]
v [z : A × B]
with constraint
x : A, y : B ⊢ u[x] = v[(x,y)] : A
the proposed algorithm prunes v's argument, since it contains the
variable y which is not bound on the lhs of the constraint. This
loses the solution
v[z] = fst z
u[x] = x
Arguments of meta-variables should only be pruned if they have an
unbound variable in a *non-eliminateable* rigid occurrence. This means, if
there is no instance of the meta-variable that would project away the
bad parts of the argument. In particular, such an instance cannot
exist if the offending variable appears in the head of the argument.
Another example is
u [x : A]
v [z : (A -> A -> A) -> A]
x : A |- u[x] = v[\k. k x y]
Pruning the argument of v would lose the solution
v[z] = z (\x y. x)
Fix: In Fig.5, replace FV^rig(M) ⊈ ρ with the new judgement
badOcc_ρ(M) which is given by the rules
x ∉ ρ
--------------
badOcc_ρ(E[x])
badOcc_ρ(M)
--------------
badOcc_ρ(λy.M)
badOcc_ρ(M₁) badOcc_ρ(M₂)
-------------------------
badOcc_ρ(M₁,M₂)
In an extension of unification to full-fledged dependent types, such
as Agda, one can also prune type arguments with rigid occurrences of
bad variables.
FV^rig(A) ⊈ ρ
------------- A is definitely a type expression
badOcc_ρ(A)
where "definitely type expressions" are Π, Σ, and base types, i.e.,
everything that is given in the grammar for A in Fig.1.
Agda had the same problem, see Agda issue 458,
http://code.google.com/p/agda/issues/detail?id=458.
2. Problem with non-linearity detected 2013-10-18.
The proposed extension to non-linear patterns produces ill-typed
solutions in some cases. For example, consider meta variable
u : B [A : type, x : A, B : type]
and constraint
A : type, x : A |- u[A,x,A] = x : A.
The proposed algorithm would solve with
u[A,x,B] = x
but this solution is ill-typed.
(See Agda issue 920, http://code.google.com/p/agda/issues/detail?id=920.)
Fix: The free variable check has to take the types (A) of all the
subexpressions of the rhs (here, just x) into account to see whether
the non-linear variable (A) is actually unused in the solution.
3. Problem with informal statement about intersection for non-variable substitutions,
detected 2017-07-02
The following statement in Section 3.5 is wrong:
> Although we have restricted intersection to variable substitutions, it
> could be extended to meta-ground substitutions, i.e., substitutions
> that do not contain any meta-variables.
Counterexample: Consider the problem
(λf. f ∘ f, g, N) ∩ (id, g ∘ g, N) : (x : (A→A)→A→A, y : A→A, z : P(x y))
where N : P (g ∘ g). We cannot remove x and y from the context, as
P(x y) would be ill-formed then.
The deeper reason is that substitution is not injective, i.e., we can
have [σ]M =β [τ]M but σ(x) ≠ τ(x) for some x ∈ FV(M).