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

Constant type can not be generalized ? #7636

Closed
vicuna opened this issue Sep 23, 2017 · 15 comments
Closed

Constant type can not be generalized ? #7636

vicuna opened this issue Sep 23, 2017 · 15 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Sep 23, 2017

Original bug ID: 7636
Reporter: ChriChri
Assigned to: @garrigue
Status: confirmed (set by @lpw25 on 2017-10-02T16:40:50Z)
Resolution: open
Priority: normal
Severity: minor
Target version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Monitored by: ChriChri

Bug description

It 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 }
@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: ChriChri

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 }

@vicuna

This comment has been minimized.

@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: @gasche

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.

@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: ChriChri

Thanks. This first example was indeed stupid, I wanted to simplify to much ...
Thanks for the trick ...

@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: @gasche

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>

@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: ChriChri

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>

@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: ChriChri

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 }

@vicuna
Copy link
Author

vicuna commented Sep 23, 2017

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Sep 29, 2017

Comment author: @xavierleroy

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.

@vicuna
Copy link
Author

vicuna commented Oct 2, 2017

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Oct 3, 2017

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Oct 9, 2017

Comment author: @xavierleroy

Marking this for "later", as I'm not expecting a solution any time soon.

@vicuna
Copy link
Author

vicuna commented Nov 13, 2017

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Jan 29, 2018

Comment author: victor-dumitrescu

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

@vicuna
Copy link
Author

vicuna commented Jan 30, 2018

Comment author: @garrigue

Tentative fix: #1588

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