Using well-disciplined type-propagation to disambiguate label and constructor names

[vicuna]

Original bug ID: 5759
Reporter: @alainfrisch
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2012-12-07T14:31:22Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.01.0+dev
Fixed in version: 4.01.0+dev
Category: typing
Related to: #6000 #7386
Child of: #6951
Parent of: #5525 #5848 #6784
Monitored by: @bobzhang @gasche @diml @ygrek @jmeber @hcarty @alainfrisch

Bug description

Now that the type-checker has a well-disciplined way to propagate type information (with a way to ensure principality), one should allow explicit type information to disambiguate constructor and label names. This seems to be a low-hanging fruit.

Not being to use in a given context two types sharing some name is an annoying issue with the language, with several workarounds but no satisfactory solution. Being able to share labels has become more important with the introduction of punning. Moreover, having nice short names for AST constructors (in the compiler itself) has become more important with -bin-annot and -ppx, since people are actually going to pattern match and build AST fragments. Later, if we add some "runtime type" features, concrete names used in the type declaration will affect the semantics of programs (e.g. by being directly visible in textual representation of values), making the "prefixing" work-around even less appealing.

File attachments

• better-errors.diff
• disambiguate-with-warnings.diff
• disambiguate.diff
• fix-unify.diff
• fix-warnings.diff
• fix-warnings2.diff
• fix-warnings3.diff
• new-error.diff
• patch_use_all_fields.diff
• record-disambiguation.diffs
• sum_disambiguation.diff

[vicuna]

Comment author: @garrigue

As I told before, I have some 5 lines of code somewhere to make this work for records.
So this is only a political decision :-)
For pattern-matching, this is a little bit more complicated, due to the interaction
with polymorphic variant inference.
I need to find a solution for that, as this causes trouble with GADTs too.

[vicuna]

Comment author: @alainfrisch

Our code base has many instances of declarations with identical names (we currently disambiguate syntactically by prefixing with the type name, using a local hack), so it might be a good test case for a better solution. I volunteer for testing your patch!

[vicuna]

Comment author: @garrigue

OK, I created a branch record-disambiguation, which allows field access based on types.
The patch is attached to this PR.
There is an important limitation: this patch only uses the type to determine the module in which the type was defined, and prefix the (unqualified) label with this module path. If the label is defined in several types in the same module, this may well fail.
Probably the cleanest behavior would be to obtain the label information from the type itself. However, it is not currently available in the environment (we would need a labels_by_path, similar to constrs_by_path). Additionally, one may question the wisdom of allowing to define labels such that only explicit type annotations can select them.

[vicuna]

Comment author: @alainfrisch

obtain the label information from the type itself

We could apply Datarepr.label_descrs. Not very clean (nor efficient), of course! It would make a lot of sense to keep the label descriptions directly in the Type_record constructor. Instead of:

| Type_record of
(Ident.t * mutable_flag * type_expr) list * record_representation

one would have:

| Type_record of label_description list

(and we would keep the Ident.t in lbl_name). The code structure needs to be adapted a little bit, to create the type declaration and the labels (/constructors) at the same time, but I don't see any big problem to do so.

allowing to define labels such that only explicit type annotations can select them

It is a common case in our code base...

I was actually thinking about issuing a warning when an "ambiguous" label or constructor is used without enough type information flowing in to disambiguate it. (Depending on the order of type declarations is a bad idea.)

[vicuna]

Comment author: @gasche

I'm not fond of Jacques' type-based implicit module qualification. I don't really see myself explaining to a surprised beginner reading some code "yeah, in this case you don't need to give the module path, because it was somehow inferred".
Besides, we already have good features to alleviate module access, namely local open, with a compact syntax, so I think you could do something equally convenient, less surprising and more explicit. It may be worth it to look at situations where current local open is not satisfying: does it work in patterns, for example? Or maybe the current state of "declaring a module alias has a heavy semantics with unsavory consequences" is a problem for conveniently short module names, and could be improved.

The nice thing with Alain's proposed semantics is that we're not adding yet another different way to do the same thing, but only using type information to enable a new feature that requires it. I can see myself explaining to a beginner "yeah, you should really avoid having duplicate label names available in the same environment, but if you do you can put annotations to disambiguate" (aside: Agda has type-based disambiguation of constructor names and its users are quite fond of it). I wouldn't personally use that feature much, but if it is considered I strongly support the use of a warning in all ambiguous cases.

Finally, I would like insist on the fact that I don't expect beginners to really understand how type information is propagated, and to adopt an optimistic model of "expect it to work and, if not, add type annotations". This means that what you think of as "if type information is available and is M.t, I can prefix the constructor with the path M" is likely to become, in the mind of the beginner, "I can access constructors under any path M implicitly".
This suggests a very different model of ambiguity in the case of Jacque's feature: if you write the constructor/field K without a path, the implementor point of view is "that can denote any constructor K currently in scope or, if type information is available and shows module M, M.K", but the user point of view is likely to be "it can denote any constructor K available in the environment under any module path". Under this view, I think it is unreasonable to combine both Alain's and Jacques' suggested behavior, because there should be an ambiguity (which ought to result in a warning) as soon as two arbitrarily deep submodules share the same constructor name.

[vicuna]

Comment author: @garrigue

Gabriel, did you read my note?
I was talking about a quick implementation explicitly stating that the behavior was not as thorough as expected.
The reason is that using directly type information in a clean way requires changing the environment data structure and/or type representation, which in turn requires bootstrapping, which is heavy for a very first prototype.
But it is clearly the way to go, as label shadowing would make understanding the behavior complicated (note that the current module qualification mechanism is already broken in this respect, it would be better to fix it too).

Concerning the semantics, I have given it some thought over many years, and the catch is of course that we must keep backward compatibility.
When type information is available, we can use it and completely ignore where the label is defined.
However, when it is not, or when there are qualified labels, we need to look them up in the environment, using the current rule.
As you point out, combining the two mechanism may not be very intuitive, and this makes error reporting hard (we don't know the programmer's intent).
Fortunately, the worse think that may happen is a type error.
Concerning ambiguity detection, this is another problem.
This requires a way to keep track of all unqualified labels defined in the environment, but Ident.keys seems to provide that already, so this is actually not too difficult.
This would probably have to be yet another optional warning, since people using the old approach intentionally open modules to use a specific label definition, hiding previous ones.

[vicuna]

Comment author: @gasche

I did indeed read your note, but understood it as "I implemented a first desirable feature, whose more ambitious refinement will have to wait for a larger code change". Sorry for this misunderstanding.

Concerning ambiguity detection, this is another problem.
This would probably have to be yet another optional warning,
since people using the old approach intentionally open modules
to use a specific label definition, hiding previous ones.

Indeed, this is yet another issue. Writing M.(r.f) feels equivalent to r.M.f to the user, but the first is ambiguous and not the second. Or you could choose a different visibility behavior, where opening a module still shadows the previous definition(s) in scope, and the only ambiguity is between two labels defined in the same module. Users would then to have module-qualification to distinguish between modules, and type-annotation between in-module label reuses. Not sure if this is really intuitive, and doesn't cover Alain's use case of allowing name reuse between parsedtree and typedtree.

[vicuna]

Comment author: @alainfrisch

Jacques: I had to add a call to Btype.repr in Env.ty_path, to have 'make world' succeed in the branch (Env.ty_path gets called with a "Tlink(Tconstr("Odoc_types.info",[],[]))"). I thought that lbl_res would always be a Tconstr node. Do you understand why the Btype.repr is now needed?

[vicuna]

Comment author: @garrigue

I have now committed a version that does "the right thing", by keeping the required information in the environment. Hopefully there is still no need to bootstrap.

The fix to the Tlink problem is the last commit.
One should never call expand_head directly on type definitions, I suppose.
It should also apply to the previous patch (but at a different location).

--- typing/typecore.ml (revision 12943)
+++ typing/typecore.ml (working copy)
@@ -2360,7 +2360,8 @@
let record = {record with exp_type = instance env record.exp_type} in
begin try
let (label_path,label) = Env.lookup_label lid.txt env in

•  match ty_exp.desc, (expand_head env label.lbl_res).desc with
  

•  let ty_res = instance Env.empty label.lbl_res in
  

•  match ty_exp.desc, (expand_head env ty_res).desc with
     Tconstr(p1,_,_), Tconstr(p2,_,_) when not (Path.same p1 p2) ->
       raise Exit
   | _ -> (record, label_path, label)
  

[vicuna]

Comment author: @garrigue

I have just committed in record-disambiguation@12945 a complete solution, which supports field access, field mutation, record construction and pattern-matching.

Note that combining two strategies under the same syntax can result in a slightly complex specification.
The worst case is record construction:

• we first check if there is a qualified field name, and use all the labels in its type to handle unqualified fields
• otherwise we use the labels from the type propagated from the context, either by a type annotation or a source expression (with construct)
• if there is no type from the context, we use finally the type from the first unqualified label
  The last case could be discussed, as it means that label order has an impact on typability.
  Add to that principality checks, where the warning should be disabled if there is another way to reach the same result...

See examples in tests/typing-misc/records.ml.
Hopefully error messages are clear enough that the semantics is not too confusing.

Variant constructors are not yet supported.
There is also an interaction with polymorphic variants for pattern-matching, which results in types from the context being ignored if a polymorphic variant appears in one of the patterns.

[vicuna]

Comment author: @alainfrisch

Great! I'll have a look at it soon (not next week, though).

• if there is no type from the context, we use finally the type from the first unqualified label

I think it would be better to look for the "last" defined type which contains all the labels (and give a warning if there are several such types). This is what we do in our version, and it only accepts more programs. It's already a good (syntactic) disambiguation scheme (for records; this doesn't apply so easily to sum types).

[vicuna]

Comment author: @garrigue

Actually the other option I was thinking of was just to revert to the original behavior when there was no type or qualifier.
I only implemented lookup of the first label because it was simpler...

I do not like much looking up types according to multiple labels. This looks robust, but one needs a completely new notion of multi-key lookup. Moreover, if we start having it for record creation and pattern-matching, why not have it for field access (with delayed resolution) too ? This is doable, but this is a real language change, as we need polymorphic records during typing.

[vicuna]

Comment author: @alainfrisch

but one needs a completely new notion of multi-key lookup

The can be implemented with the current environment, using a find_all on the first label to get a list of all matching record types, and then filtering (and issuing a warning if several record types remain).

The extension to field access seems much more complex, I'm not proposing such a language change (especially because disambiguation based on type information gives a simple solution). FWIW, we rarely use field accesses. Since the introduction of record punning and the warning on "non exhaustive" record patterns, we have good incentives to rely almost exclusively on record patterns.

[vicuna]

Comment author: @alainfrisch

There is a bad interaction with private types. The following piece of code:

module rec X : sig
type t = private {x: int}
end = struct
type t = {x: int}

let () = ignore {x = 2}
end

fails with:

Error: Cannot create values of the private type X.t

[vicuna]

Comment author: @gasche

tests/typing-private has no testcase with recursive module (typing-recmod/t16ok.ml has a private type but it's not used in a recursive module either). Maybe you could add this one to the test suite?