Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007483OCamltypingpublic2017-02-14 01:212017-04-03 16:35
ReporterChriChri 
Assigned Tolpw25 
PrioritynormalSeverityfeatureReproducibilityalways
StatusresolvedResolutionduplicate 
PlatformOSOS Version
Product Version4.04.0 
Target Version4.06.0 +dev/beta1/beta2/rc1Fixed in Version 
Summary0007483: Strange behavior for function with polymorphic type
DescriptionAnnotating 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 Reproducecompile 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
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0006673acknowledgedgarrigue Redundant type annotation on argument causes polymorphic-recursive definition to be rejected 

-  Notes
(0017252)
ChriChri (reporter)
2017-02-14 01:56

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]
(0017253)
frisch (developer)
2017-02-14 09:13

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.
(0017255)
ChriChri (reporter)
2017-02-14 15:02
edited on: 2017-02-14 15:03

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.

(0017256)
ChriChri (reporter)
2017-02-14 15:18
edited on: 2017-02-14 15:19

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 !

(0017260)
yallop (developer)
2017-02-15 13:11

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.
(0017262)
ChriChri (reporter)
2017-02-15 14:16

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 ?
(0017344)
xleroy (administrator)
2017-02-19 16:53

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.
(0017714)
lpw25 (developer)
2017-04-03 16:27

The original example is fixed by:

  https://github.com/ocaml/ocaml/pull/1132 [^]

without changing the scoping rule for type variables.

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

- Issue History
Date Modified Username Field Change
2017-02-14 01:21 ChriChri New Issue
2017-02-14 01:56 ChriChri Note Added: 0017252
2017-02-14 09:13 frisch Note Added: 0017253
2017-02-14 15:02 ChriChri Note Added: 0017255
2017-02-14 15:03 ChriChri Note Edited: 0017255 View Revisions
2017-02-14 15:18 ChriChri Note Added: 0017256
2017-02-14 15:19 ChriChri Note Edited: 0017256 View Revisions
2017-02-14 15:19 ChriChri Note Edited: 0017256 View Revisions
2017-02-15 13:11 yallop Note Added: 0017260
2017-02-15 14:16 ChriChri Note Added: 0017262
2017-02-19 16:53 xleroy Note Added: 0017344
2017-02-19 16:53 xleroy Status new => acknowledged
2017-02-19 16:53 xleroy Target Version => 4.06.0 +dev/beta1/beta2/rc1
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-10 09:39 shinwell Severity minor => feature
2017-04-03 16:27 lpw25 Note Added: 0017714
2017-04-03 16:35 lpw25 Relationship added duplicate of 0006673
2017-04-03 16:35 lpw25 Status acknowledged => resolved
2017-04-03 16:35 lpw25 Resolution open => duplicate
2017-04-03 16:35 lpw25 Assigned To => lpw25


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker