Treat universal variables as abstract in expected types #12732

lpw25 · 2023-11-12T10:04:32Z

Currently the following code:

type t = { coerce : 'a 'b. ('a, 'b) Type.eq -> 'a -> 'b }

let t = { coerce = fun Equal x -> x }

Does not type-check:

type t = { coerce : 'a 'b. ('a, 'b) Type.eq -> 'a -> 'b; }
Line 3, characters 19-35:
3 | let t = { coerce = fun Equal x -> x }
                       ^^^^^^^^^^^^^^^^
Error: This field value has type "'c. ('c, 'c) Type.eq -> 'c -> 'c"
       which is less general than "'a 'b. ('a, 'b) Type.eq -> 'a -> 'b"

and so must be explicitly annotated with locally abstact types:

let t = { coerce = fun (type a b) (Equal : (a, b) Type.eq) (x : a) : b -> x }

This PR makes fresh abstract types and uses them to stand for the universal variables in expected types. This allows the above example to type without additional annotations. This makes some APIs much more usable, for example the current API for deep effect handlers -- see the updated effect tests.

The same treatment is applied to polymorphic annotations on let and methods. For example, this now type-checks:

let coerce : 'a 'b. ('a, 'b) Type.eq -> 'a -> 'b =
  fun Equal x -> x

For simplicity, the new abstract treatment is not used for universal row variables.

This PR also extends the mechanism added in #12622 to give improved error messages. For example, this code:

let foo : 'a. bool -> 'a -> 'a =
    fun p x -> if p then x else x + 1

previously gave the following error:

Line 2, characters 4-37:
2 |     fun p x -> if p then x else x + 1;;
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This definition has type bool -> int -> int which is less general than
         'a. bool -> 'a -> 'a

whereas this PR gives a much more localized error:

Line 2, characters 32-33:
2 |     fun p x -> if p then x else x + 1;;
                                    ^
Error: This expression has type "$a" but an expression was expected of type "int"
       Hint: "$a" is an abstract type bound by the polymorphic annotation on
         "foo".

In larger more realistic functions the increased precision of these errors is a real improvement, and I think that the Hint sufficiently compensates for the appearance of a fresh abstract type in the message.

garrigue

I'm sorry to have been so long to start reviewing this PR.
Turning universal type variables into abstract types when checking the body is is a good idea, and this PR seems to do a nice job at it.
There are however a number of difficulties in reviewing this PR, due to the size of the changes.
If possible, I would like to see the following points addressed:

The most concrete one: if replace_newtypes is to be used repeatedly, I think that it should not work by modifying types. Either take an explicit copy inside replace_newtypes, or find another approach.
There seems to be a fair amount of code duplication at each point where abstract types are inserted; isn't there a way to factorize that out ?
type_label_exp and type_let have been modified so extensively that reviewing the changes is a real challenge. Could you document what has been really changed, what has been just moved around, and why ?

garrigue · 2024-01-05T02:32:08Z

testsuite/tests/typing-poly/poly.ml

+Error: This expression has type "$a" but an expression was expected of type "int"
+       Hint: "$a" is an abstract type bound by the polymorphic annotation on
+         "depth".
 |}];;


Here there seems to be a problem with the original poly.ml: there should be an expect after each failure, otherwise we only catch the first one. I will fix it, and we need to rebase.

garrigue · 2024-01-05T02:38:14Z

testsuite/tests/typing-poly/poly.ml

+Error: This expression has type "$a -> $a"
+       but an expression was expected of type "$a -> unit"
+       Type "$a" is not compatible with type "unit"
+       Hint: "$a" is an abstract type bound by the polymorphic record field "f".


This one is fine. I would not say it is better, but there is enough information to understand the cause of the error.

garrigue · 2024-01-05T02:44:51Z

testsuite/tests/typing-poly/poly.ml

-       which is less general than "'a 'd. (< x : 'a; .. > as 'd) -> 'a"
+                                                                              ^
+Error: This expression has type "< x : $a; .. >"
+       It has no method "y"


Here there is a change in behavior, due to the row variable being turned into an abstract type.
This contradicts the explanation of the PR (which says that polymorphic row variables were unchanged), but this is correct, as this type already implies that one cannot access methods other than x in the body of the function.

garrigue · 2024-01-05T02:46:43Z

testsuite/tests/typing-poly/poly.ml

           < n : 'irr.
                   ('irr -> unit) * ((< x : 'a; y : 'b; .. > as 'c) -> 'a) >"
       where "'c" is unbound
 |}]


The following are GADT examples. I'm not sure this is the right place to put them in the testsuite.
This said, they also exercise features related to poly.ml.

garrigue · 2024-01-05T02:52:24Z

testsuite/tests/typing-gadts/pr10907.ml

+                                 ^^^^^^^
+Error: This expression has type "$a" but an expression was expected of type "$b"
+       Hint: "$a" and "$b" are abstract types
+         bound by the polymorphic annotation on "unsound_cast".


This error message taken individually is a regression. It is more understandable once one looks at the type annotation, and mentally translates it to abstract types.
Maybe the hint could say:
bound by the polymorphic annotation "unsound_cast", which results in the expected type "$a -> $b$".

garrigue · 2024-01-05T06:37:34Z

typing/typecore.ml

+      | _ -> Btype.iter_type_expr loop t
+    end
+  in
+  (fun t -> loop t)


Why this seemingly useless eta-expansion ?

garrigue · 2024-01-05T06:41:52Z

typing/typecore.ml

-    let ety = Subst.type_expr Subst.identity exp_type in
-    replace ety;
+    let ety = instance exp_type in
+    replace_newtypes [id, ty] ety;


Changes in type_newtype do not seem to be related with making universal variables abstract: there are no universal variables here.
It seems to be a result of re-using the replace function that was defined here, but this function always striked me as a rather ad-hoc.

garrigue · 2024-01-05T06:50:05Z

typing/typecore.ml

+                Ident.equal id id') mapping
+          with
+          | None -> ()
+          | Some (_, var) -> link_type t var


I'm not fond of this way of plugging type variable into an existing type.
This does not respect the integrity of types.
Couldn't we find a better approach, if we intend to use it in more places.
A more politically correct approach would be to create two distinct instances.

Also note that @alainfrisch 's original code was using Subst.type_expr to build a fresh copy of the type before doing this substitution, while you are using instance, which does not provide the same guarantee of independence.

garrigue · 2024-01-05T07:10:53Z

typing/typecore.ml

  with Failure msg ->
    raise (Error (loc, env, Invalid_format msg))

-and type_label_exp create env loc ty_expected


The changes here are extensive.
It will take me a while to review that.
Any information on what was done and why would certainly be helpful.

garrigue · 2024-01-05T07:14:27Z

typing/typecore.ml

  let is_recursive = (rec_flag = Recursive) in
-
-  let (pat_list, exp_list, new_env, mvs, _pvs) =
+  let (pat_list, new_env, exp_list, mvs, pvs) =


Same problem here.
The changes are too extensive for a fast review.
More information about what was done and why would help.

gasche · 2024-03-03T21:47:01Z

@lpw25 this PR is waiting for your response to @garrigue's feedback. Do you think that you will have some time to help get it to the finish line? If not, any idea of how to help the change move forward?

lpw25 · 2024-03-04T08:57:44Z

I intend to get to this this month

gasche · 2024-10-05T11:40:34Z

@lpw25 gentle ping; how do you think we could get this PR to the finish line?

lpw25 · 2024-10-07T08:14:00Z

Thanks for the ping. I'd mostly forgotten about this. The last time I tried to move it forward I had to rebase it across some other PRs that require parts of this to be rewritten. I'll try and find time to at least get that rebase finished in the next few weeks, then I can consider how to address the review comments.

lpw25 added 3 commits November 12, 2023 09:09

Add tests that polymorphic annotations give locally abstract types

240d60d

Treat universal variables as abstract

dd45261

Remove unnecessary annotations from effects tests

1386c8f

lpw25 mentioned this pull request Nov 13, 2023

An alternative effect API #12736

Closed

gasche self-assigned this Nov 17, 2023

garrigue reviewed Jan 5, 2024

View reviewed changes

lpw25 mentioned this pull request Nov 27, 2025

RFC: val declarations in structures ocaml/RFCs#59

Open

Treat universal variables as abstract in expected types #12732

Are you sure you want to change the base?

Treat universal variables as abstract in expected types #12732

Uh oh!

Conversation

lpw25 commented Nov 12, 2023

Uh oh!

garrigue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

garrigue Jan 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

garrigue Jan 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gasche commented Mar 3, 2024

Uh oh!

lpw25 commented Mar 4, 2024

Uh oh!

gasche commented Oct 5, 2024

Uh oh!

lpw25 commented Oct 7, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

garrigue Jan 5, 2024 •

edited

Loading

garrigue Jan 5, 2024 •

edited

Loading