Unification failure

[mb64]

Hi! I've come across a strange issue, where this unification problem fails: a:t -> F (G a) = X. But if X is a ground term, it works.

    Makam, version 0.7.40

# %constraints+.
# t : type.
# x : t.
# eq : t -> t -> prop.
# eq X X.
# test : (t -> t) -> (t -> t) -> t -> prop.
# test F G X :- (a:t -> eq (F (G a)) X).
# test F G X ?
Impossible.

# test F G x ?
Yes:
G := G,
F := F.

Deferred Constraints:
eq (F (G a)) x

I have the latest version from npm.

(This isn't urgent to fix, at least not for my code, I'm just reporting in case it's helpful.)

[mb64]

While trying to minimize the issue, I found a stack overflow:

# eq (F X) X ?
Fatal error: exception Stack overflow

[astampoulis]

Hi @mb64 , thank you very much for reporting these issues. I really appreciate your effort to minimize the original issue, uncovering a type-checker issue in the process :smile:

I have looked into the first issue a little; it is in a part of the higher-order unification procedure that does not have a lot of coverage through the current tests. I'll have to dig a little bit more into it to see what might be going on. I am glad to hear that it's not blocking you though :smile: This is the kind of issue that might take a while to identify and fix.

The second issue has to do with the basic Makam type-checker, I am guessing a bug with the occurs check implementation. I am hoping I'll be able to identify and fix this soon.

Going on somewhat of a tangent, I have a question since it seems that you are working with unification problems that leave open constraints a lot. One direction I have been thinking about is to switch to a higher-order pattern unification procedure with a more restrictive pattern fragment, similar to what ELPI does, which does not leave any deferred unification constraints. For example, one idea is to allow unification variables to be applied to fresh variables -- or unification variables that have already been instantiated to fresh variables. While this can simplify the unification implementation and its semantics, it would disallow the test predicate you have (using F a would be OK, but F (G a) would not be). Would that prevent you from using Makam for what you are currently encoding? If so, I would love to understand more about your use case to help with future directions -- feel free to email me at antonis dot stampoulis at gmail dot com if preferred.

[mb64]

I'm glad the bug report is useful.

That restriction would not prevent me from using Makam. I think all my non-pattern-fragment problems have just been from playing around in the REPL, as I try to understand how the higher-order unification algorithm works. As it turns out, the cases I don't understand well turn out to be edge cases involving lots of delayed constraints.