Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0004862OCamlOCaml generalpublic2009-09-09 16:062010-06-08 04:45
Reporterlavi 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version3.11.1 
Target VersionFixed in Version3.12.0+dev 
Summary0004862: small bug in relaxed value restriction
DescriptionVraiment pas important, mais il me semble que le programme suivant devrait être accepté:

# type t = {f: 'a. ('a list -> int) Lazy.t}
  let l : t = { f = lazy (raise Not_found)};;
Characters 62-84:
    let l : t = { f = lazy (raise Not_found)};;
                      ^^^^^^^^^^^^^^^^^^^^^^
Error: This field value has type ('a list -> int) Lazy.t
       which is less general than 'b. ('b list -> int) Lazy.t

Le type de f ('a Lazy.t) pourrait pourtant bien être généralisé. D'ailleurs, si l'on passe par une variable intermédiaire, ça passe:

type t = {f: 'a. ('a list -> int) Lazy.t}
let tmp = lazy (raise Not_found)
let l : t = { f = tmp }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005073)
garrigue (manager)
2009-09-09 16:31

Je comprends votre confusion, mais cet exemple n'est pas un bug, meme si il demontre la fragilite de la relaxed value restriction dans certains cas.
En effet le type de [lazy (raise Not_found)] n'est pas le meme quand on le met directement dans l'enregistrement ou lorsqu'on definit une valeur intermediaire.
Dans le premier cas, la contrainte de type induite par l'enregistrement donne le type
[('a list -> int) Lazy.t] qui n'est pas generalisable suivant la restriction relaxee (occurence contravariante).
Dans le second cas c'est ['a Lazy.t] qui est lui generalisable (occurence covariante).
Ce genre de phenomene n'est pas rare, et c'est donc une bonne idee d'utiliser un let explicite pour aider le typeur. On pourrait en theorie retarder l'application de la contrainte de type pour pouvoir mieux generaliser, mais ca risquerait d'induire des messages d'erreur moins clairs.
(0005074)
lavi (reporter)
2009-09-09 16:53

Hum ça reste bizarre, parce que le code suivant ne passe pas non plus :

# type t = {f: 'a. ('a list -> int) Lazy.t}
  let l = { f = let tmp = raise Not_found in tmp };;

pour le coup, c'est la première fois que je vois le type changer selon que l'on utilise un "let" ou un "let in"...
(ceci n'est évidemment pas grave, et ne me gène aucunement dans ma programmation en caml, qui reste un merveilleux langage !)
(0005075)
lavi (reporter)
2009-09-09 16:59

oups typo:
let l = { f = let tmp = lazy (raise Not_found) in tmp };;

mais ça reste vrai: si on sort le "let tmp", ça passe...
(0005381)
garrigue (manager)
2010-04-27 03:09

Je ne vois pas de solution simple: le problème vient du fait qu'on propage le type attendu vers
l'expression à typer, ce qui rend impossible de généraliser une variable devenue contravariante.
La seule option ici semble être de backtracker, pour retyper sans propagation...
(0005548)
garrigue (manager)
2010-06-08 04:45

Fixed in version/3.12, revision 10538.
Used backtracking, but as long as one doesn't nest polymorphic record expressions, this shouldn't cause an exponential behaviour,

- Issue History
Date Modified Username Field Change
2009-09-09 16:06 lavi New Issue
2009-09-09 16:31 garrigue Note Added: 0005073
2009-09-09 16:31 garrigue Status new => resolved
2009-09-09 16:31 garrigue Resolution open => no change required
2009-09-09 16:31 garrigue Assigned To => garrigue
2009-09-09 16:53 lavi Note Added: 0005074
2009-09-09 16:53 lavi Status resolved => feedback
2009-09-09 16:53 lavi Resolution no change required => reopened
2009-09-09 16:59 lavi Note Added: 0005075
2010-04-27 03:09 garrigue Note Added: 0005381
2010-06-08 04:45 garrigue Note Added: 0005548
2010-06-08 04:45 garrigue Status feedback => closed
2010-06-08 04:45 garrigue Resolution reopened => fixed
2010-06-08 04:45 garrigue Fixed in Version => 3.12.0+dev


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker