Jason (jcreed) wrote,

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: cyclic, twelf, unification
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded