Strange problem

[liamoc]

Hi Daniel

Not sure if you're interested in helping me debug something, but I made use of this implementation as part of a proof assistant I am implementing.

Firstly, I think line 48 (where you check if you should raise a variable) is incorrect. Should it not read:

 LocalVar j -> if j >= lower then LocalVar (i + j) else LocalVar j

?

Secondly, I am now encountering a problem where it fails to make progress on this constraint:

(Lam (Ap (FreeVar 0) (LocalVar 0)),Ap (MetaVar 4) (FreeVar 0))

Pretty-printing this:

(\x. P x)  ~ ?4 P

For some reason, it spins around on this and doesn't find the obvious solution ?4 := (\y.\x. y x). I'd appreciate any help you can give. It's also possible I somehow introduced a bug that wasn't present in your original implementation. If that's the case, I'm sorry to have bothered you!

[jozefg]

Ack, I'm sorry, I just saw this now! Are you still stuck on this issue?

[liamoc]

I'm not stuck anymore, as I switched to pattern unification instead (works for what I'm doing). Still would be interested to figure out what was going wrong, but no urgency!

[jozefg]

I think pattern unification is probably sufficient for a proof assistant yeah, I would like to figure it out as well. I'll have to spend some time looking at code my longtime nemesis (past me) wrote.

[fizruk]

Hello there! I am now also looking at this code as a source of inspiration, thanks for making it public :)

I think that the problem with non-termination is because of this line:

higher-order-unification/src/Unification.hs

Line 199 in 21382f4

if isClosed f then [f] else []]

I believe this line exists to avoid identifying meta-variables with local (bound) variables. This is a bit confusing (why do we need an isClosed check here if we're concerned about bound variables). But what we are trying to check here is that we did not capture any of the bound variables which we previously converted into fresh free variables upon entering the scopes here:

higher-order-unification/src/Unification.hs

Lines 164 to 173 in 21382f4

	| Lam body1 <- t1,
	Lam body2 <- t2 = do
	v <- FreeVar <$> lift gen
	return $ S.singleton (subst v 0 body1, subst v 0 body2)
	| Pi tp1 body1 <- t1,
	Pi tp2 body2 <- t2 = do
	v <- FreeVar <$> lift gen
	return $ S.fromList
	[(subst v 0 body1, subst v 0 body2),
	(tp1, tp2)]

So if you remove isClosed check then the example of @liamoc works well. However, it is not correct to remove it entirely. Instead one could introduce another constructor (e.g. FreeLocalVar or FreshVar or something like that) and check for absence of those.