New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Redundant type annotation on argument causes polymorphic-recursive definition to be rejected #6673
Comments
Comment author: @gasche This is a known issue with type variables: because they have no explicit binder, it is hard to know where they are introduced; I think they are considered at the level of the innermost toplevel item (they can be nested if we are in a submodule), and this is above the annotation in your example. Constant constructors where introduced to alleviate this issue by having an explicit binding site for rigid variables: let id (type a) : a -> a = fun (x : a) -> x;; The "type a ." syntax desugars to a combination of a constant-constructor binding and a polymorphic annotation: let id : type a . a -> a = fun (x : a) -> x;; (with the somewhat surprising and ugly effect that (type a . ...) scopes outside the (...).) |
Comment author: @gasche You may be amused to know that another workaround is to perform the type annotation "above" the innermost toplevel item by moving it into a signature constraint: include (struct let id = fun (x : 'a) -> x end : sig val id : 'a -> 'a end);; For teaching and readability purposes, I would like the following syntax to be accepted in the future: val id : 'a . 'a -> 'a |
Comment author: @lpw25
Personally, I think the problem here is not that the regular type variables are introduced at the top-level, but that the universal type variables are not introduced at the top-level (even though they are syntactically part of the top-level construct). Is there any strong reason this could not be supported, by introducing universal variables earlier? |
Comment author: @lpw25 Can we stop marking this issue resolved (same as for #6569)? The code in the example is perfectly reasonable, and would ideally be accepted. The issue isn't resolved by the existence of a work-around, because it is not a question of expressibility but a question of disallowing perfectly reasonable code for a reason that is not obvious to even experienced users of the language. |
Comment author: @garrigue There is a confusion here. So, in the following code, the 'a on x denotes another type variable, global this time. Since variables at the global level cannot be generalized locally, this makes typing fail. let f : 'a . 'a -> 'a = fun (x : 'a) -> x;; The solution is to use locally abstract types: let f : type a. a -> a = fun (x : a) -> x;; By the way, allowing the first program would require changing the specification, possibly breaking existing programs. |
Comment author: @fpottier Jacques wrote: "allowing the first program would require changing the specification, possibly breaking existing programs". I am not sure about that. If one decides to change \exists\forall to I would argue that in this code: let f : 'a . 'a -> 'a = fun (x : 'b) -> x;; it makes sense to view the left-hand type annotation as "at the toplevel" Best, |
Comment author: @yakobowski
So this is yet another instance of the fact that named type variables that that are not explicitly bound are quantified at toplevel? I noticed the issue for the first time when working on MLF, and I did not understand why those variables were not bound at the nearest (lowest) possible binding site -- especially given the way type generalization is implemented in OCaml's type checker. I'm afraid I still don't understand :-( (This would be coherent with François's last proposal: 'b would be introduced at the same level as 'a.) |
Comment author: @garrigue Ok, again this proposal of moving to the SML approach of using the innermost level. My point was that, however, this change would not give the behavior that some seemed to expect, namely that 'a is shared between the two annotations. If you want that behavior, there is already a syntax for that. |
Comment author: @lpw25
Sorry, I should have been clearer. When I talked about universal type variables not being introduced at the top-level, I was not referring to their scope, but to their level. At the moment, universal variables are handled at level When I suggest that universal variables be introduced earlier, I mean that they should be handled at the same level as their enclosing The attached patch may not quite be correct, but it illustrates what I am suggesting, and successfully types the example. |
Comment author: @lpw25 Jacques, any thoughts on the patch I attached? |
Comment author: @garrigue OK, what you are suggesting is delaying check_univars until after all the definitions are generalized. This may make sense (i.e., be sound); have to think about that. In that case we probably wouldn't need all the level mangling. |
Comment author: @garrigue It took me a while, but no I recall why this cannot work (at least with the current approach). let rec depth : 'a. 'a t -> _ = (Well, the program is not wrong, but the type inferred is 'a t -> 'b, which is wrong). I see no easy solution, at least level-based. |
Comment author: @lpw25
I see. So the current scheme instantiates the poly type, unifying the result with the type of the expression and then uses This essentially misses out the equivalent of the My patch changes the levels of the free variables in the poly type, so that they may be inappropriately changed into universal variables. It seems to me that a simple solution to this is just to run The attached patch implements this suggestion, and does indeed give an appropriate error for the above example. |
Comment author: @lpw25
There is definitely something wrong with this patch, as it fails one test, but I haven't worked out what it is yet. I will investigate further. |
Comment author: @lpw25
The problem is that the universal variables created by |
Comment author: @lpw25 I've attached a patch implementing a more complete solution. It changes the approach for checking polymorphic types. Instead of generalising the unification variables and then mutating them to be universal variables, it generalises the whole type and then instantiates it with univeral variables for the generalised unification variables. This instance is then unified with the intended polymorphic type -- which allows the usual unification checks to ensure that universal variables do not escape. I believe this approach to be correct, and the patch successfully types the examples in this thread. The patch passes all tests (modulo error messages) but one: unlike current OCaml, the patch allows the following definition to type-check:
I believe this is sound and just illustrates the improvement in flexibility of this approach. (Note that another test was also failing, but it was just an instance of #6744). |
Comment author: @garrigue I didn't check your patch, but I see two problems:
|
Comment author: @lpw25
Sorry, when I said "instantiates it with universal variables for the generalised unification variables" I meant the unification variables returned by The checking of whether the expressions type is sufficiently generalised is basically identical to what is there at the moment. The difference is that, during the check, instead of mutating the expression's type, we create a copy (instance) and surround it with a
I'm afraid I don't really understand what you mean here. Could you make your point more concretely by referring to the patch itself? |
Comment author: @garrigue Sorry, for point (2) I misunderstood your code. I now think that this is sound, but we need a more concrete argument. E, x1 : s1, ..., xn : sn |- Mi : ti Gen(E,ti) < si si = Si(gi) (i=1..n)
|
This has been fixed on trunk by #1132. |
Original bug ID: 6673
Reporter: @fpottier
Assigned to: @garrigue
Status: acknowledged (set by @garrigue on 2014-12-18T01:17:40Z)
Resolution: duplicate
Priority: normal
Severity: minor
Version: 4.01.0
Category: typing
Has duplicate: #7483
Related to: #6569
Monitored by: @ygrek
Bug description
This is accepted:
let f : 'a . 'a -> 'a = fun x -> x;;
And this is accepted too:
let f = fun (x : 'a) -> x;;
But this is rejected:
let f : 'a . 'a -> 'a = fun (x : 'a) -> x;;
Error: This definition has type 'a -> 'a which is less general than
'a0. 'a0 -> 'a0
This behavior seems inconsistent to me, and somewhat unplesant.
(I have teaching in mind.) Is it a bug and could it be fixed?
Thanks
Francois.
File attachments
The text was updated successfully, but these errors were encountered: