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
Strange behavior for function with polymorphic type #7483
Comments
Comment author: ChriChri By the way, the bug is not (only) the bad error message. The function should be accepted. It is accepted if one remove the annotation on [aux] |
Comment author: @alainfrisch I think this works as expected (even if very confusing). The scope of the first 'a is only the type annotation. So the second 'a is a fresh type variable, and its scope is thus the entire "structure item" declaration (i.e. above the first quantification), as for any free type variable. The inner function is thus monomorphic in the context where it appears. You can see that by using different type variable names. It's usually better to use the alternative form with a locally abstract type: let insert : type t. (t -> t -> bool) -> t -> t list -> t list = fun cmp a l -> In this form, the scope of the locally abstract type t include the body of the declaration. |
Comment author: ChriChri I am aware of the solution with type a. ... Still let insert : 'a.('a -> 'a -> bool) -> 'a -> 'a list -> 'a list = fun cmp a l -> Fails too (no matter if you use 'a or 'b in aux) This is wrong
|
Comment author: ChriChri I answered too quickly
Yes the inner function is monomorphic and annotated as such in my example by 'a list -> 'a list (trying to reuse the 'a of insert) or 'b list -> 'b list. The generalisation that is failing is the generalisation of insert ! |
Comment author: @yallop Here's a simpler example that illustrates the same issue let id : 'a -> 'a = fun x -> x in This is rejected as it is, but accepted if the annotation is removed, for the reasons frisch explains. |
Comment author: ChriChri This is not exactly the same. Because aux is only used once. let insert : type t. (t -> t -> bool) -> t -> t list -> t list = fun cmp a l -> I do not see why OCaml could not take 'a = t in unification. Yet, I think generalisation could be done in the local let after using the type annotation and the id exemple should be accepted too, because it is accepted if we replace 'in' with ';;'. OCaml typing is hard to explain to beginners ... Would not it be possible |
Comment author: @xavierleroy This is working as intended. It's just that the intention is not intuitive at all. One day we'll need to decide whether to 1- live with it, 2- document it better, or 3- reconsider the scoping rules for "'a" type variables. |
Original bug ID: 7483
Reporter: ChriChri
Assigned to: @lpw25
Status: resolved (set by @lpw25 on 2017-04-03T14:35:39Z)
Resolution: duplicate
Priority: normal
Severity: feature
Version: 4.04.0
Target version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Duplicate of: #6673
Bug description
Annotating function with type 'a. ... and using 'a in the type of
auxilliary recursive function yield obscure error message.
Tested on 3.12 and 4.04
Steps to reproduce
compile the following:
let insert : 'a.('a -> 'a -> bool) -> 'a -> 'a list -> 'a list = fun cmp a l ->
let rec aux : 'a list -> 'a list = function
| [] -> [a]
| b::l -> if cmp a b then a::b::l else b::aux l
in aux l
yield
Error: This definition has type
('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
which is less general than
'a0. ('a0 -> 'a0 -> bool) -> 'a0 -> 'a0 list -> 'a0 list
The text was updated successfully, but these errors were encountered: