Experimental skolem unification

[jstolarek]

As part of some debugging I came up with experimental unification of skolems. The idea is that variables without a structure and rank -1 (read: uninstantiated quantifiers) can only be unified if one of them is a skolem. This is currently commented out in Unify.unify_descriptors. It doesn't seem to affect anything so the code is commented out. I need to think what to do exactly with that code. I think this is actually more of an assertion if the implementation is valid, and not a behaviour necessary to reject some ill-typed programs.

[jstolarek]

Uncommenting this code in the unifier trips choose_choose_let example. Investigate.

[jstolarek]

The reason why choose_choose_let fails is because when I skolemize the quantifiers in a signature I only skolemize the top level ones and not the nested ones, which I believe is wrong. So the commented out code in unify_descriptors should be an assertion since it isn;t needed to reject ill-typed programs but it can catch implementation bugs.

[jstolarek]

I tried out nested skolemization of quantifiers. It doesn't work and for the wrong reasons. Consider choose_choose_let example:

let (f : (∀ a. a → a → a) → (∀ a. a → a → a)) = choose ~choose
in f ~choose

The solver see quantified a variables in the signature of f as distinct, so the signature on f is internally represented as:

(∀ a. a → a → a) → (∀ b. b → b → b)

However, in the inferred type of the bound expression same quantified variables are used, so internally the type of choose ~choose is:

(∀ c. c → c → c) → (∀ c. c → c → c)

With nested skolemization both a and b are turned into skolems. We then unify ∀ a. a → a → a with ∀ c. c → c → c, turning the inferred type of choose ~choose into:

(∀ a. a → a → a) → (∀ a. a → a → a)

where a is a skolem. When we next attempt to unify ∀ a. a → a → a with ∀ b. b → b → b unification fails because skolems a and b cannot be unified. The right thing to do here would be inferring the type of choose ~choose as:

(∀ c. c → c → c) → (∀ d. d → d → d)

I believe this could be done with a change inside Generalize.instantiate. This is somewhat related to not instantiating nested quantifiers (#7).

[jstolarek]

I implemented freshening of nested quantifiers during instantiation (see f93c968), but that doesn't solve the problem. The issue here is that duplicate appearance of (∀ c. c → c → c) is introduced by unification (no instantiation taking place) and when we unify the signature with the inferred type we crucially don't instantiate the inferred type. This is mandatory for seeing the side effects of unification with the type annotation, which we deeply care about here. I think it might be possible to implement freshening that will traverse the inferred type and freshen the nested quantifiers but keep the generalizable and existential variables intact.

[jstolarek]

I implemented proper freshening of nested quantifiers (G.freshen_nested_quantifiers) and I'm reverting f93c968 since it doesn't seem to be needed for anything and I don't want to introduce unnecessary complications. This function isn't used at the moment, but I'm keeping it for now. This whole idea is basically a deep swamp and I don't intend to go any deeper into it. Fixing one problem (freshening of nested quantifiers, skolemization of nested quantifiers) leads to something breaking and for a good reason. Without a precise formal treatment of skolems there's no point in pursing this using trial and error. Closing.