Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007636OCamltypingpublic2017-09-23 19:392018-01-30 08:08
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target Version4.07.0+dev/beta2/rc1/rc2Fixed in Version 
Summary0007636: Constant type can not be generalized ?
DescriptionIt looks like if variables were not values in Ocaml ?

This is not accepted :

type 'a iter = { f : 'b.'a -> unit }

let promote f : 'a -> unit = { f }

This works:

let promote f =
  let f : 'b.'a -> unit = fun x -> f x in
  { f = fun x -> f x }

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
ChriChri (reporter)
2017-09-23 19:43

Sory the previous example was too simple.
My real problem is this :

type ('a, 'b) elt = 'a

type 'a iter = { f : 'b.('a, 'b) elt -> unit }

let promote f : 'a -> unit =
  let f : 'b.('a, 'b) elt -> unit = fun x -> f x in
  { f }
ChriChri (reporter)
2017-09-23 19:44

Why can't I edit my original issue ?
gasche (administrator)
2017-09-23 20:04

Your code seems to be wrong: "let promote f : 'a -> unit" should, I suppose, be "let promote (f : 'a -> unit)".

For your first code example, the following works:

# type 'a iter = { f : 'b.'a -> unit };;
# let promote (f : 'a -> unit) = { f = f };;
val promote : ('a -> unit) -> 'a iter = <fun>

For you second example, this seems related to the fact that ('a, 'b) elt is a type synonym, which confuses the type-checking of polymorphic methods. Indeed,
this works:

# type ('a, 'b) elt = 'a * unit;;
# type 'a iter = { f : 'b. ('a, 'b) elt -> unit };;
# let promote (iter : 'a iter) : 'a iter = { f = iter.f };;
val promote : 'a iter -> 'a iter = <fun>

but this fails:

# type ('a, 'b) elt = 'a;;
# type 'a iter = { f : 'b. ('a, 'b) elt -> unit };;
# let promote (iter : 'a iter) : 'a iter = { f = iter.f };;
Error: This field value has type ('a, 'c) elt -> unit
       which is less general than 'b. ('a0, 'b) elt -> unit

This may be a bug.
ChriChri (reporter)
2017-09-23 21:50

Thanks. This first example was indeed stupid, I wanted to simplify to much ...
Thanks for the trick ...
gasche (administrator)
2017-09-23 21:54
edited on: 2017-09-23 21:55

Note that recent versions of OCaml (>= 4.04.0) can make the trick work without any change to the data representation:

# type 'a id = Id of 'a [@@unboxed];;
# type ('a, 'b) elt = 'a id;;
# type 'a iter = { f : 'b. ('a, 'b) elt -> unit };;
# let promote { f } = { f };;
val promote : 'a iter -> 'a iter = <fun>

ChriChri (reporter)
2017-09-23 21:56

The following indeed works ! Very strange that 'a is not like 'a * unit
in this case:

# type ('a, 'b) elt = 'a * unit
# type 'a iter = { f : 'b.'a -> unit }
# let promote f = { f }
type 'a iter = { f : 'a -> unit; }
val promote : ('a -> unit) -> 'a iter = <fun>
ChriChri (reporter)
2017-09-23 21:58

And this works too:

type 'a t = U of 'a [@@unboxed]
type ('a, 'b) elt = 'a t
type 'a iter = { f : 'b.'a -> unit }

let promote (f : 'a t -> unit) = { f }
lpw25 (developer)
2017-09-24 01:06

This is an interesting one. If you have a type:

  type ('a, 'b) t = 'a

and you unify ('p, 'q) t with ('r, 's) t then it will essentially unify ('p, 'q) t with 'r. That means that if the level of 'r is lower than the level of 'q then the level of 'q will be lowered. (I'm glossing over some slight details of how the levels are handled here, but this is the basic idea).

In your example the 'r is 'a and the 'q is 'b. The level from 'a is too low to be generalized, and thus 'b cannot be generalised either, which causes the error.

I'm not sure what the best thing to do here is. In this case we would essentially like 'r to unify with 'p and thus leave the level of 'q untouched, but I'm not sure that is the right thing to do in general.
xleroy (administrator)
2017-09-29 20:09

Reading this discussion I can't see whether (1) everything works as intended even though the behavior is surprising in the end, or (2) something might possibly need to be changed. Please classify this PR according to the answer to this question.
lpw25 (developer)
2017-10-02 18:43

I think it is worth trying to do better here, so I'm marking as confirmed. In particular, this seems like a potential problem for principality or at least a case where we are not really inferring the most general type possible.
garrigue (manager)
2017-10-03 09:53

Unfortunately, I don't think that we can really do better, short of changing to some extent our approach to abbreviations.

Namely, if your analysis is correct (and I think it is), the problem comes from the way abbreviations types are unified; i.e. both sides are first expanded, and the expanded type is redirected to point to (one of) the abbreviations. In doing that, the levels of type variables in that abbreviation are lowered to that of the root of the expanded type. This is fine if the type variables actually occur in the expanded type, but this may lower them more than needed if they don't. Yet not lowering them would break the invariant that levels in types go down towards the leaves.

A fix would be to only redirect to abbreviations if their variables all appear in the expanded type.
But is it really what we want?
In this case yes, as the expanded type is actually a parameter of the abbreviation. In general it is much harder to tell.

First option, fix just this example: if the expansion of an abbreviation is in one of its parameters, then do not redirect to it. I'm not sure what the cost would be; probably not that high.

Second option, consider abbreviations less important than principality: as soon as one of the parameters of an abbreviation does not appear in its (fully expanded) body, do not redirect to it. In theory, this could be very easy to check: this amounts to empty variance information for this parameter. In practice, there are many corner cases where this information is not accurate, and I'm not sure how far we want to go.

Anyway, this is good to understand what is happening, as this can help working around the problem.
I don't think fixing this is urgent, we can first discuss what is the correct approach.
xleroy (administrator)
2017-10-09 20:18

Marking this for "later", as I'm not expecting a solution any time soon.
garrigue (manager)
2017-11-13 17:49

I intend to fix it for 4.07, but sill need to decide how to do it.
Suggestion by Didier Rémy: do not lower levels on "absent" type variables, based on variance.
This breaks the invariant that levels should decrease, but the variable doesn't matter anyway.
Need to look into it.
victor-dumitrescu (reporter)
2018-01-29 11:53

We've encountered an instance of this issue in F* extraction to OCaml (4.02.3 and 4.05.0). Currently we are extracting polymorphic functions in this form:

type 'a t = int
let test : 'a. int -> 'a t = fun i -> i

This fails with
Error: This definition has type 'a t -> 'a t which is less general than
         'a0. 'a t -> 'a0 t

However, it does go through when using the -principal flag.

It doesn't seem to be an issue when writing this function slightly differently. All of the following are accepted:

let test2 : int -> 'a t = fun i -> i
let test3 : type a. int -> a t = fun i -> i
let test4 : 'a. int -> 'a t = fun i -> let i: int = i in i
garrigue (manager)
2018-01-30 08:08

Tentative fix: [^]

- Issue History
Date Modified Username Field Change
2017-09-23 19:39 ChriChri New Issue
2017-09-23 19:43 ChriChri Note Added: 0018313
2017-09-23 19:44 ChriChri Note Added: 0018314
2017-09-23 20:04 gasche Note Added: 0018315
2017-09-23 21:50 ChriChri Note Added: 0018316
2017-09-23 21:54 gasche Note Added: 0018317
2017-09-23 21:55 gasche Note Edited: 0018317 View Revisions
2017-09-23 21:56 ChriChri Note Added: 0018318
2017-09-23 21:58 ChriChri Note Added: 0018319
2017-09-24 01:06 lpw25 Note Added: 0018320
2017-09-29 20:09 xleroy Note Added: 0018404
2017-09-29 20:09 xleroy Status new => acknowledged
2017-10-02 18:40 lpw25 Assigned To => lpw25
2017-10-02 18:40 lpw25 Status acknowledged => confirmed
2017-10-02 18:43 lpw25 Note Added: 0018454
2017-10-03 09:53 garrigue Note Added: 0018463
2017-10-09 20:18 xleroy Note Added: 0018524
2017-10-09 20:18 xleroy Target Version => later
2017-11-13 17:49 garrigue Note Added: 0018659
2017-11-13 17:49 garrigue Assigned To lpw25 => garrigue
2017-11-13 17:49 garrigue Target Version later => 4.07.0+dev/beta2/rc1/rc2
2018-01-29 11:53 victor-dumitrescu Note Added: 0018858
2018-01-30 08:08 garrigue Note Added: 0018860

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker