search

jstolarek / inferno

Mirrored from https://gitlab.inria.fr/fpottier/inferno
MIT License
0 stars 1 forks source link

Skolemizing monomorphic quantifiers in bad3 and bad4 #36

Open jstolarek opened 3 years ago

jstolarek commented 3 years ago

In the process of implementing let_mono constraints (#33) I had to comment out an assertion in the unifier:

let skolemize v =
  let descriptor = TUnionFind.find v in
  (* assert (not (descriptor.monomorphic)); *)
  descriptor.skolem <- true

This assertion causes failures in bad3 and bad4. Most likely implementing #35 correctly will fix this. See also #39.