parmatch: don't rename idents when typing witnesses

[trefis]

I guess this is my alternative #9009 .

Context:
When type_pat is called from Parmatch (eg. to type check a pattern which is supposed to cover values not handled by the pattern matching) it is given: an explode parameter, a constrs parameter and a labels parameter (#9009 proposes to regroup these last two.. but not the first one).

These last two parameters are used in various ways:

• to detect whether we're being called from parmatch (in which case, we, for instance, don't want to record annots) ; that is: their value is not useful
• to do the lookup of the constructors and label names present in the part, instead of going through the environment as one usually would.

That last step is a bit surprising: why wouldn't we want to go through the normal lookup process? My initial guess was: so we avoid marking as used candidates that are rejected, and to avoid getting any warnings (type disambiguation might be happening!).
But the code looks like this:

match lid.txt, constrs with
  Longident.Lident s, Some constrs when Hashtbl.mem constrs s ->
    Ok [Hashtbl.find constrs s, (fun () -> ())]
| _ ->
    Env.lookup_all_constructors Env.Pattern ~loc:lid.loc lid.txt !env

Which is definitely weird: if the ident is not a simple Lident (e.g. if it contains a dot), or if it's not in the table then we revert back to normal resolving?
Well, turns out that Parmatch is "freshening" all the lids (to look #$ID42), so the lookup never actually fails. And if it did, then so would the call to Env.lookup_all_constructors.

So how about we remove all that extra complexity, and just go through the normal lookup process (taking care to silence warnings beforehand)?

Well, then we get two test failures:

1. some lookups now fail if the source contained some pattern-local open. I believe we can get around that by making the lids absolute when creating the candidate in Parmatch. Which should be doable given that we have the type path at that point. (There will be some subtlety regarding inline record fields, and extensible types, but I don't expect any major problem)
2. some match which was marked as exhaustive, is now deemed non exhaustive, namely that one:

  type ab = A | B

  module M : sig
    type mab = A | B

    type _ t = AB : ab t | MAB : mab t

    val ab : mab t
  end = struct
    type mab = ab = A | B

    type _ t = AB : ab t | MAB : mab t

    let ab = AB
  end

  open M

  let f (type x) (t1 : x t) (t2 : x t) (x : x) =
    match t1, t2, x with
    | AB,  AB, A -> 1
    | MAB, _, A -> 2
    | _,  AB, B -> 3
    | _, MAB, B -> 4

But as it turns out, the match is indeed non exhaustive!

# f M.ab MAB A;;
4

Woops.

So what was happening there?

• On this branch, the candidate that is generated is AB, MAB, A, which typechecks fine (because ab and M.mab might be equal).
• On trunk (and older versions) the candidate is #$AB0, #$MAB1, #$A2, and we have a constr table which contains which associates each of these to the right constructor description.
  We then go into type pat, type the first element of the tuple, then the second, then we arrive on the third: so we're in typecore on line 1162 (as of today):
  1. we get the type path through the expected type (it's x, also known as ab, because the first constructor pattern we saw was AB)
  2. we get the constructor description from our table (which in particular has the field cstr_res = mab)
  3. we go on to call Constructor.disambiguate on that single candidate list. Which tries to do type disambiguation, and that fails (because ab is not mab from the point of view of disambiguation), so it then tries to lookup the constructor using the type, but that fails (because #$A2 is not a real constructor), so it... fails.
     That is: our candidate as produced by Parmatch doesn't typecheck. So it must mean that the matching is exhaustive. ¯\(ツ)/¯

So the current PR as it stands is unfinished, and here is a summary of the situation:

• it cleans up some weird logic from typecore and parmatch
• it fixes a typechecker big (which currently leads to a miscompilation)
• it introduces a regression in the handling of pattern-local module opens

I have other things on my plate right now, and @gasche seems to be having a lot of fun in that area f the typechecker. So: @gasche why don't you pick things up from here and give a go at fixing the regression (possibly along the lines suggested above, possibly some other way)?

[garrigue]

IIRC, the problem is deeper than that: contrary to types, shadowing of constructors is allowed. So it might be hidden. Now that we have disambiguation, the situation is a bit better, but you would still need a way to be sure that the right constructor will be selected.

Concerning the bug you found, one way would be to add modules to the environment, and equip the dummy type definitions inside them with equations to the real one, so that the equalities would be kept.

[trefis]

IIRC, the problem is deeper than that: contrary to types, shadowing of constructors is allowed. So it might be hidden

Ack. That would indeed have been a problem before disambiguation.

but you would still need a way to be sure that the right constructor will be selected.

I think the thing I proposed (to make constructor / label paths absolute by using the type information) would take care of that, wouldn't it?

Initially, I thought that reducing the longident to just the constructor/label name (and stripping the rest of the path), and relying on disambiguation (given that we know the expected type) would be sufficient.
But that is not the case in presence of extension constructors:

# module M = struct exception E end;;
module M : sig exception E end
# let f e = match (e : exn) with E -> ();;
Line 1, characters 31-32:
1 | let f e = match (e : exn) with E -> ();;
                                   ^
Error: This variant pattern is expected to have type exn
       The constructor E does not belong to type exn

That's why I'm suggesting to make paths absolute when building the candidate instead (for extensions we can use the Path.t contained in the constructor tag).

Does that seem reasonable to you?

[trefis]

Concerning the bug you found, one way would be to add modules to the environment, and equip the dummy type definitions inside them with equations to the real one, so that the equalities would be kept.

I do not understand what you're talking about there.

[garrigue]

Your idea assumes that type-based disambiguation will be sufficient to find the right constructor.
I haven't thought thoroughly about that, but I'm not sure this is always sufficient.

I had read your report on a small screen, and at first I thought that the problem you were describing was about two identical constructors seen as different. However, this is not what you are describing, and since typing only uses the explicit information inside the original constructor declaration, there is no reason for such a problem.
So, reading properly your example, my conclusion is that this is a bug in disambiguation: if disambiguation doesn't find a constructor, then the default is supposed to be to return the newest one in the environment, ignoring the type.
Usually, one would expect it to be in the list of candidates, but here this is not the case.

[garrigue]

Actually I tried to fix that, by setting opath to None in disambiguate for generated lids, but this doesn't seem to be sufficient. I'm starting to think that we really have to select a constructor with the same name in a different type to make this work, which might just be yet another example that type definitions are not really nominal in ocaml. Note that this would mean that your idea of using full paths would not work here too.

[trefis]

if disambiguation doesn't find a constructor, then the default is supposed to be to return the newest one in the environment, ignoring the type.

I think there is some confusion there: the constructor that currently goes through disambiguation is #$A2, which is not in the environment.

The real problem with the code as it currently stands is that you're calling disambiguation whilst there is no need to.
If I understand your intent correctly when you say you set opath to None, you were trying to not use disambiguation. Which is the right idea, but the wrong way to go at it.

Here is what trunk currently does:

     let candidates =
        match lid.txt, constrs with
          Longident.Lident s, Some constrs when Hashtbl.mem constrs s ->
            Ok [Hashtbl.find constrs s, (fun () -> ())]
        | _ ->
            Env.lookup_all_constructors Env.Pattern ~loc:lid.loc lid.txt !env
      in
      let constr =
        wrap_disambiguate "This variant pattern is expected to have"
          (mk_expected expected_ty)
          (Constructor.disambiguate Env.Pattern lid !env opath) candidates
      in

Change it to:

     let constr =
        match lid.txt, constrs with
          Longident.Lident s, Some constrs ->
            Hashtbl.find constrs s
        | _ ->
            let candidates = Env.lookup_all_constructors Env.Pattern ~loc:lid.loc lid.txt !env in
            wrap_disambiguate "This variant pattern is expected to have"
              (mk_expected expected_ty)
              (Constructor.disambiguate Env.Pattern lid !env opath) candidates
      in

and I believe the problem would also be solved (spoiler: I haven't tried it!).

If it works, then it might indeed be the first step we want to take, before considering the present PR. Can I let you try it out and submit a PR?

---

All that being said, I think the code would come out cleaner by following the approach that this PR suggests, that is: instead of generating fresh unique names in parmatch and building a table to map them to the right constructor, we would use fully qualified paths when building the witness, and rely on type disambiguation (through the expected type) to select the right one whenever shadowing might have happened.

But I don't want to push too strongly for it.

[garrigue]

I tried your version of the fix to disambiguation, which indeed looks nicer, but does not solve the problem anymore than mine. I really believe there is something deeper here.

[trefis]

Indeed.

What is clear is that before (#$AB0, #$MAB1, #$A2) was failing because it couldn't find the constructor description associated to #$A2. Now that part goes through fine, it takes an instance of the constructor (which gives us ty_res), an instance of the expected type, and tries to unify to the two. That is, it tries to unify:

ty_res: Types.type_expr =
  {desc =
    Tconstr
     (Path.Pdot
       (Path.Pident (Ident.Scoped {Ident.name = "M"; stamp = 97; scope = 2}),
       "mab"),
     [], {contents = Mnil});
   level = 11; scope = 0; id = 1356}
expected_ty: Types.type_expr =
  {desc =
    Tconstr
     (Path.Pident (Ident.Scoped {Ident.name = "x"; stamp = 99; scope = 9}),
     [], {contents = Mnil});
   level = 11; scope = 0; id = 1358}

which fails. I haven't looked into why.

Doesn't that seem like a different issue though?
It looks like somehow we have forgotten that x = ab = mab.

[trefis]

It looks like somehow we have forgotten that x = ab = mab.

And indeed, at that point env.local_constraints contains only x = ab if ocamldebug is to be trusted.
That would be because whilst typechecking #$MAB we end up trying to unify M.mab an ab and we decide that "yes, they are compatible", but never remember that.

Basically what I am saying is that:

let f (type x) (t1 : x t) (t2 : x t) (x : x) =
  match t1, t2, x with
  | AB,  AB, A x -> print_int x
  | MAB, _, A x -> print_int x
  | _,  AB, B x -> print_string x
  | _, MAB, B x -> print_string x
  | AB, MAB, (A x : M.mab) -> print_int x

doesn't type check:

25 |   | AB, MAB, (A x : M.mab) -> .
                  ^^^^^^^^^^^^^
Error: This pattern matches values of type M.mab
       but a pattern was expected which matches values of type x = ab

But

let f (type x) (t1 : x t) (t2 : x t) (x : x) =
  match t1, t2, x with
  | AB,  AB, A x -> print_int x
  | MAB, _, A x -> print_int x
  | _,  AB, B x -> print_string x
  | _, MAB, B x -> print_string x
  | AB, MAB, A x -> print_int x

does, because the last A x is inferred to be of type ab.

[trefis]

Just so we're clear: the issue here has nothing to do with disambiguation, or parmatch.
For instance, this doesn't typecheck either:

(* Assume "val M.a : M.mab" *)

let f (type x) (t1 : x t) (t2 : x t) : x =
  match t1, t2 with
  | AB, MAB -> M.a
  | _ -> failwith "whatever"

39 |   | AB, MAB -> M.a
                    ^^^
Error: This expression has type M.mab but an expression was expected of type
         x = ab

[garrigue]

Thank you for the analysis. We still have an interesting bug, isn't it?
The absence of equation is not wrong (you hid it!), but it shouldn't prevent us from generating a typable pattern.
As I pointed in comment #9012 (comment), this really is about using the same constructor name in another type.
In the end, using type disambiguation on untyped terms is probably the only solution: since ocaml allows to hide equalities between types with identical definitions, retyping terms seems to be the correct solution.
My only concern is that I'm not 100% sure of the completeness of the disambiguation code. When I wrote it I had only soundness in mind. Still, we are not interested in all forms of disambiguation, only disambiguation by the return type. And we probably want to ensure that nothing else is used when called from Parmatch.

[lpw25]

The absence of equation is not wrong (you hid it!)

Actually, I think the equation should be there due to the GADT match. The issue seems to be that #7233 only added support for equations on "abstract" types i.e. ones without constructors. This seems just wrong to me -- why would having constructors prevent you from adding equations?

The fix is probably to remove the decl.type_kind = Type_abstract condition from Ctype.is_instantiable and then adding mcomp tests to the appropriate branches of unify3.

[garrigue]

The problem is that the contents of the type definition might not be unifiable either, so that you may have to force-unify recursively. This would require a bit more investigation.

[lpw25]

This bug got me thinking. It seems that the current approach to refuting cases relies on the assumption that if a pattern _, Foo is typeable then so is A, Foo if A has the right type. However, that isn't the case, which leads to a fairly nasty soundness bug:

type _ a_or_b =
  A_or_B : [< `A of string | `B of int] a_or_b

type _ a =
  | A : [> `A of string] a
  | Not_A : _ a

type _ b =
  | B : [> `B of int ] b

let f (type x) (a : x a) (b : x b) (a_or_b : x a_or_b) (x : x) =
  match a, a_or_b, b, x with
  | Not_A, _, B, `B i -> print_int i
  | _, A_or_B, _, `A s -> print_string s

let segfault = f A B A_or_B (`B 0)

[lpw25]

The problem is that the contents of the type definition might not be unifiable either, so that you may have to force-unify recursively.

I see. That would still seem like the most desirable behaviour though. Definitely worth investigating.

[garrigue]

Note also that even if we add the equation in this case, this would not fully solve the problem, as we only add equations for parameter-less types, but two parametric types can be compatible.

[garrigue]

Thinking more, we have here and in #9019 two cases where a constructor can be incompatible with its type due to incompleteness in the GADT type reconstruction. I'm yet to find a counter-example containing neither polymorphic variants nor overloaded constructors as patterns. In particular, constrained types do not seem to allow anything more.
If these are indeed the two only possible cases, then this PR (using disambiguation for normal constructor) and my fix #9022 seem to be the way out.

[garrigue]

By the way, the reason we used a mapping rather than disambiguation for constructors is clear enough: GADTs (and their exhaustiveness check) were introduced before constructor disambiguation, and constructor disambiguation itself was disabled for GADT constructors until recently.
But now it should be fine to get rid of this mapping.

[trefis]

By the way, the reason we used a mapping rather than disambiguation for constructors is clear enough: ...

That makes sense indeed!

[garrigue]

@gasche is pushing for a quick inclusion of this one...
I"m going to have a go at it.
If I understand correctly, we want to keep the defaulting, for cases where disambiguation is not enough to decide which constructor should be used, but let type information override it when available. A new mode for disambiguation?

[garrigue]

Actually, it proved easy to trigger disambiguation using the old approach, while still keeping the defaulting as before. So #9022 now fixes both #9019 and this PR.
The disambiguation-only approach of this PR is still interesting, but it is less urgent now.

[trefis]

If I understand correctly, we want to keep the defaulting, for cases where disambiguation is not enough to decide which constructor should be used, but let type information override it when available. A new mode for disambiguation?

I'm confused, I thought that was already the way disambiguation worked.

---

Let me try to summarize the situation, hopefully that will confirm that we have the same thing in mind.

Currently on trunk, when parmatch uses a constructor (or label) in the witness it produces to show non exhaustivity, it gives that constructor a fresh name, and keeps a pointer from that new name to the relevant constructor description in a table.
The intent being that when we type the witness, we will, without a doubt, use the correct constructor (and not any other one which might use the same name).

What I am proposing instead, is to use the fully qualified name of the constructor in the witness (i.e. to use a fully expanded path to it). I believe that in the absence of shadowing, this is enough to ensure that we will use intended constructor.
However, if the constructor happens to have been shadowed, then type directed disambiguation should select the right one. This relies on type information being available, which I believe it always is in that case.

[garrigue]

Actually disambiguation only works on unqualified names (see lookup_from_type in Typecore).
So you cannot use both qualified names and disambiguation.

However, I was confused when I wrote the previous comment: since Parmatch is always called with the inferred type of the patterns, disambiguation should always succeed even if you use the unqualified name. But maybe we need some more checking to be confident of that.

[garrigue]

This would still leave the problem of extension constructors.
Their cstr_name field just contains the last component of their path, but this isn't sufficient to look up their definition by type.
I wonder whether we can adjust the above example to extension constructors, to find a new unsoundness in #9022.

[trefis]

I believe you're confusing two issues here.

Fully expanding the paths is needed so the call to Env.lookup_all_constructors succeeds (even in the case of extension constructors that you just mentioned, or in the presence of local opens).

After that, disambiguation will work as it normally does.

[garrigue]

There are two different mechanisms.

• disambiguate_by_type tries to find the constructor among the ones visible in the current environment.
  In that case the qualified named in only used to build that list.
• if this fails, lookup_by_type tries to look up the type definition by type only, and then to find the constructor inside this definition. However, this only works for unqualified names.

In some cases, using a qualified named will be sufficient for disambiguate_by_type to work.
By I"m not sure it works if the module containing the constructor was shadowed, for instance.

BTW, extension constructors should not be a concern for soundness, as they are never complete anyway, and not finding a constructor would only fail to restrict the type of its index (if it's a GADT constructor).

[gasche]

@gasche is pushing for a quick inclusion of this one...

To be more clear: when I suggested changing the code of type_pat to clarify it (in #9023 and then a more ambitious follow-up PR that I'm preparing, but remains on the level of the code clarification and documentation and simplification only), @garrigue told me "but you should wait until #9012 is merged". No! Either this PR is ready to merge (as @garrigue seemed to think at the time), and then please merge it, or this PR is not ready to merge, and then I don't see why I would block my own work for it.

If I offer a code cleanup as PR, and then people review it and like it, it could be merged right away. First come (to the "approved and ready to merge" pile) first served. That means that the other PR has some rebase work to do, and that is fair game.

(As to whether this PR is ready to merge, I can't tell, because I don't understand anything about it -- I haven't tried very hard yet. The general tone of your discussion doesn't give a very strong we-have-converged-and-this-is-ready-to-go vibe. I'm putting my own energy in putting proper API and documentation on the part that I do understand -- thanks to the patient explanations of @Octachron -- so that everyone looking at this code in the future has an easier time.)

[trefis]

@gasche: that all sounds reasonable to me. Thanks for clarifying.

[garrigue]

And to clarify a bit more for @gasche: I believe #9022 provides an alternative solution to the soundness problem, so there is no reason to hurry this PR anymore (I think it still provides an interesting simplification of the code). And since #9022 shouldn't have any conflict with your refactorings, I do not see this problem as a reason to delay them anymore. But of course #9022 has to be judged on its own merits.

[gasche]

Note: I sent my second refactoring PR as #9030, and all comments are welcome.

(Jacques: I integrated in the explanations the things that you taught me during our discussion yesterday.)

[trefis]

This PR was useful to get some discussion started, but has been subsumed by various other PRs, so I'm closing it.