I finally found a nice simple example of the oft-mentioned Twelf unification/type-reconstruction bug that happens because of circularity in types of unification variables.

```o : type.
a : o -> type.
b : o -> o -> type.
eq : b M M -> type.
x-c : {w : o} {u : a w -> o} {v : a w} b (u v) w.
%abbrev c = x-c W U V.
test : eq c.
```

Its symptom, like the last bug I mentioned, is non-termination.

The unification problem that comes up is this: find
w : o
u : a w -> o
v : a w
such that
w = u v

Should be simple because the left-hand side is (trivially) a pattern substitution, right? But if you make the substitution w := u v then you're left with the problem of finding
u : a (u v) -> o
v : a (u v)
such that, well, top holds. Twelf stops and proclaims success at this point and runs the abstraction phase, which tries to turn these remaining free unification variables into a sequence of Pi quantifiers — but it can't order them by dependency since there's a cycle, and so loops forever trying.

Supposing your signature has k : o, though, the unification problem that has the additional equation that
u = lambda x . k
is completely solvable. You just get that v is a free variable of type a k.

You can see this explicitly happening on the example
```o : type.
k : o.
a : o -> type.
eq : o -> o -> type.
eqo : (a Z -> o) -> (a Z -> o) -> type.
refl : eq M M.
reflo : eqo M M.

x-c : {W : o} {U : a W -> o} {V : a W}
eqo U ([x] k)
-> eq W (U V)
-> type.
%abbrev c = x-c W U V.
test : c reflo refl.
```

where the typing of test comes back
test : {X1:a k} x-c k ([x:a k] k) X1 reflo refl
Showing that w must be k, and u must be ([x : a k] k),
and v is left free as X1 : a k.

I am beginning to be of the opinion that even the successful inversion of a pattern substitution should be postponed as if it weren't a pattern, if the resulting variable instantiation leads to circularity.
Tags:
• #### (no subject)

K got back tonight, pretty late in subjective time (3-4am or so, coming from europe) but all in one piece. None of her houseplants, which were…

• #### (no subject)

K is off tonight to Old Country for a couple weeks, to fulfill family-seeing obligations. Sad! Thankfully we still have internet and skype and…

• #### (no subject)

noms is a project apparently influenced by camlistore and git. Has a bunch of juicy buzzwords attached to it (Content-addressable, monotonic,…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic