Non-aliased Open variants are implicitly univared inside ptyp poly: #14
Conversation
| Error: The method m has type 'a -> 'b but is expected to have type | ||
| [< `Foo of 'x ] -> 'c | ||
| The universal variable 'x would escape its scope | ||
| val n : < m : 'a 'x. ([< `Foo of 'x ] as 'a) -> 'x > = <obj> |
There was a problem hiding this comment.
(Here the printed type shows what we understood, rather than what the user wrote; this is reasonable but one might have expected to reprint the compact form.)
| @@ -488,7 +490,7 @@ and transl_type_aux env ~policy ~row_policy styp = | |||
| let cty = | |||
| try | |||
| let t = TyVarEnv.lookup_local alias in | |||
| let ty = transl_type env ~policy ~row_policy st in | |||
| let ty = transl_type env ~policy ~row_policy:policy st in | |||
There was a problem hiding this comment.
Ah, this is a clever trick. I was not sure how to handle Ptyp_alias.
It's also a bit weird, in the sense that it is syntactic: it disables implicit naming on the left of _ as 'a, instead of disabling it on implicit names that are also explicitly named. This might do a small difference on, for example:
type 'a non_injective = int
type t = < m : 'a . [> `A of 'a ] non_injective -> unit >There was a problem hiding this comment.
I tend to think that we want to be syntactic and consider that we are just adding missing as annotation on polymorphic variant types (with a non-static row variable).
For instance, I am not sure if we want to handle:
type ('a,'b) s = [> `A of 'a ] as 'p
constraint 'b = _ * 'p
let f : 'a. ('a,_) s -> unit = assert false
|
I have added a commit that ensures that we only apply the scoping of the row variable to the last user-written binder and not the empty binders added by the typechecker. |
|
I'm happy with the new state of the PR. But shouldn't we not just decide that your branch is the reference for this branch, and invite you to send the PR to upstream / Jacques? At this point basically all of the code is yours -- and I will be in holidays next week. |
|
There would be little difference once we have a PR, since I will be on holidays from Monday 8th to Friday 19th. But yes, I will send the PR today to see how people react to this proposition. |
.. as ...disable the lifting of type variables to type variables