Spellchecker hints and type-directed disambiguation for extensible variants: bis

[Octachron]

This PR is an alternative implementation of #1154. Rather than tracking the list of extension constructors associated to a type in Env.t, this implementation splits the list of candidates used in Typescore.NameChoice into a list of spellchecking candidates list and a list of disambiguation candidates. Since the list of spellchecking candidates is only used in a user-facing error path; it can afford to be relatively slow contrarily to the disambiguation candidates list.

This patch keeps the same candidate lists as before for both labels and standard constructors. Contrarily, for extension constructors, the disambiguation candidates are generated with a call to lookup_all_constructors and the computation of the list of all extension constructors associated to a specific type is relegated to the spellchecking path.

[Drup]

At a first glance, I like that version a lot better. The code is much more straightforward and is a simplification over the existing implementation.

I'll take time to review more carefully later.

[gasche]

@Drup, would you by any chance be able to review it now?

[Drup]

I had a look at the new implementation. It's much simpler than the previous version, and I believe it is correct. The test file is very comprehensive, so I'm fairly confident about it. I'll let @Octachron decide what he wants to do for the empty type case, but it's very minor.

[Drup]

Since we have empty sum type now, cstrs = [] doesn't necessarily mean it's an extension constructor. That being said, this simply means doing extra work in a very uncommon cases, and doesn't compromise soundness, so I guess it's fine.

You could make this a bit better with the (unexposed) Env.find_type_full function I suppose.

[Octachron]

I think I will start by extending the comment, I believe that optimization for empty sum types can come later.

[Drup]

Side note: when you rebase, do not forget to rewrite your tests using Armael's new error message syntax.

[lpw25]

Sorry for not commenting on this proposal earlier, but IIUC what you are doing I'm not sure that the disambiguation feature is a good idea. It looks like you're planning to allow:

module M = struct
  type Foo.t += Bar
end
let x : Foo.t = Bar

but this will break as soon as M is lifted out into its own compilation unit. The ability to lift modules like that is a fundamental property of the language and I don't think it is one we should break lightly.

Supporting things like:

module M = struct
  type Foo.t += Bar
end
open M
type Other.t += Bar
let x : Foo.t = Bar

on the other hand would be absolutely fine. It shouldn't be too hard to restrict the disambiguation to cases such as these where the constructor is already available at the given path -- these are the cases that do not raise warning 40.

Note that this criticism does not apply to spell-checking hints -- it is fine for them to change when a module is lifted out to its own module.

[Octachron]

Your first example still fails with this PR since the constructor is not in the environment, whereas the second one compiles fine.

The extension of the environment in Typecore.disambiguation_candidates is here to handle cases like

module M = struct
  module N = struct
    type t = ..
    type t += A
  end
end
let x : M.N.t = A

by making sure that, at least, extension constructors defined in M.N are in the environment when looking for constructors of the type M.N.t. This behavior does not change if M is lifted to its own compilation unit.

It is still posible to get a warning 40, with

module M = struct type t = .. type t+=A end
let f (x:M.t) = x = A

but this the same behavior as the one for classical variants. Should those case be disallowed for extension constructors?

[alainfrisch]

by making sure that, at least, extension constructors defined in M.N are in the environment when looking for constructors of the type M.N.t.

This feels ad hoc. Some constructors in the type M.N.t would be "favored", only because they are defined in the same module as their type. If one wants to create such "favored" constructors, this should be explicit in the syntax, e.g. by defining the constructors together with their type (not just in the same module, but with a single definition).

But this should perhaps be discussed independently from a more basic kind of disambiguation, that only restricts the set of candidates, both for qualified references (when different constructors with the same name but different types are defined in a single module) and for unqualified ones (when different constructors are available in the current scope, for instance following an open).

[Octachron]

This part could be clearly split to a separate PR. Nevertheless, I see it as merely using all information provided by the user for the disambiguation, by acknowledging that the extension constructors defined along the type are easier to find.

[lpw25]

by making sure that, at least, extension constructors defined in M.N are in the environment when looking for constructors of the type M.N.t

Ok, so that is nowhere near as bad as I thought, but I agree with Alain that this is too ad-hoc for my taste. I'm also suspicious of how it works with type aliases like:

module M = struct
  type t = ..
  type t += A
end

module N = struct
  type t = M.t = ..
  type t += A
end

let x : N.t = A

[Octachron]

Ok, I have removed this ad-hoc open.
(@lpw25 , your example resolved to N.A)

[Drup]

Ensuring that the constructors in scope of the type are visible for the disambiguation seemed fairly reasonable to me, since it's just more disambiguation and doesn't impact correctness, but I'm fine either ways.

[alainfrisch]

This should address https://caml.inria.fr/mantis/view.php?id=6514, right?

[Octachron]

This PR is not enough in its current state: the error for multiple definitions would need to be removed, the shadowing in include would need to be refined to handle

type t = ..
type s = ..
module M = struct type t += A end
module N = struct type s += A end
module A = struct include M include N end

without hiding M.A or N.A, and the typing of extension rebinding in Typedecl should be made to use the disambiguation mechanism.

[lpw25]

What's the status of this PR? I got the impression that people were happy with the final design and the code had been reviewed, but it seems to have got blocked anyway.

[Octachron]

I am planning to rebase it after the refactoring of the disambiguation code in #9182. The rebased version will need to re-expose a function to go through all constructors in scope, so your opinion would be welcome.

[Octachron]

I have rebased the PR, and removed some of the logic that was not needed anymore. The PR is now simply removing the logic for removing shadowed extension construction from the lookup; and adding an escape hatch for searching constructors with the right type in the whole environment in the misspelling hint.

[Octachron]

After further discussion with @gasche, I have written an alternative implementation that restrict the special handling for extension constructors to the lookup_from_type function in the Constructor module.

This seemed to be a sensible compromise in term of future compatibility (if we add a notion of extension constructors in scope at a type in the environment) and present complexity.

[gasche]

The new implementation is very simple and clear, thanks. I made some nitpick comments, you should decide whether to take them into account or not.

(This is good to merge when the CI is ready; you should either merge or give me the bit of information on whether you want to work more or not.)

[Octachron]

Let me fix these minor points and squash everything.