Skip to content
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

Closed
vicuna opened this issue Feb 14, 2017 · 8 comments
Closed

Strange behavior for function with polymorphic type #7483

vicuna opened this issue Feb 14, 2017 · 8 comments

Comments

@vicuna
Copy link

vicuna commented Feb 14, 2017

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

@vicuna
Copy link
Author

vicuna commented Feb 14, 2017

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]

@vicuna
Copy link
Author

vicuna commented Feb 14, 2017

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 ->
let rec aux : t list -> t list = function
| [] -> [a]
| b::l -> if cmp a b then a::b::l else b::aux l
in aux l

In this form, the scope of the locally abstract type t include the body of the declaration.

@vicuna
Copy link
Author

vicuna commented Feb 14, 2017

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 ->
let rec aux : 'b list -> 'b list = function
| [] -> [a]
| b::l -> if cmp a b then a::b::l else b::aux l
in aux l

Fails too (no matter if you use 'a or 'b in aux)

This is wrong

  • 'b unif var should be able to take the type of the element whatever it is
  • once you fixed this annotation for insert, it is not possible I think to annotate aux. I feel that you must be able to annotate any subterm with a type ... and "'a . ..." seems to break such a property.

@vicuna
Copy link
Author

vicuna commented Feb 14, 2017

Comment author: ChriChri

I answered too quickly

The inner function is thus monomorphic in the context where it appears.

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 !

@vicuna
Copy link
Author

vicuna commented Feb 15, 2017

Comment author: @yallop

Here's a simpler example that illustrates the same issue

let id : 'a -> 'a = fun x -> x in
(id (), id 1)

This is rejected as it is, but accepted if the annotation is removed, for the reasons frisch explains.

@vicuna
Copy link
Author

vicuna commented Feb 15, 2017

Comment author: ChriChri

This is not exactly the same. Because aux is only used once.
In the following:

let insert : type t. (t -> t -> bool) -> t -> t list -> t 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

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
to fix this kind of behavior ?

@vicuna
Copy link
Author

vicuna commented Feb 19, 2017

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.

@vicuna
Copy link
Author

vicuna commented Apr 3, 2017

Comment author: @lpw25

The original example is fixed by:

#1132

without changing the scoping rule for type variables.

That patch is originally from issue #6673, and indeed this issue is a duplicate of that one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants