Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007222OCamltypingpublic2016-04-11 22:472017-09-24 17:32
Reporteroctachron 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.02.3 
Target Version4.03.0+dev / +beta1Fixed in Version4.03.0+dev / +beta1 
Summary0007222: Escaped existential type
DescriptionThe following code leads to a toplevel function with existential type within its type:
"
type +'a n = private int
type nil = private Nil_type
type (_,_) elt =
  | Elt_fine: 'nat n -> ('l,'nat * 'l) elt
  | Elt: 'nat n -> ('l,'nat -> 'l) elt
type _ t = Nil : nil t | Cons : ('x, 'fx) elt * 'x t -> 'fx t

let undetected: ('a -> 'b -> nil) t -> 'a n -> 'b n -> unit = fun sh i j ->
  let Cons(Elt dim, _) = sh in ()
"
The type inferred for "undetected" is "('a -> $'b -> nil) t -> 'a n -> $'b n -> unit ".

As far as I understand, the existential type "$'b" should never appear in the type of a toplevel function and this is a typing error.

Moreover, slightly altering the code to

"
let detected: ('a * 'b * nil) t -> 'a n -> 'b n -> unit = fun sh i j ->
  let Cons(Elt_fine dim, _) = sh in ()
"
triggers a compiler error about the existential type leaving its scope.
The same problem persists from version 4.02.3 to the beta2 version of 4.03.0.

As a supplementary information, calling the full version of this function accross module boundary triggered an internal assertion failure at (File "typing/typecore.ml", line 1903, characters 65-71) within the 4.02.3 compiler.
Unfortunately, I could not try the original code with the 4.03 beta compilers.


TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0015724)
octachron (developer)
2016-04-12 19:54

Correction, the second example also exhibits leaked existential type once its type is corrected to
"
let (*also_not_*)detected: ('a * ('b * nil)) t -> 'a n -> 'b n -> unit
= fun sh i j -> let Cons(Elt_fine dim, _) = sh in ()
(*val detected: ('a * ($'b * nil)) t -> 'a n -> $'b n -> unit*)
"
(0015766)
garrigue (manager)
2016-04-15 16:55

Fixed in 4.03 and trunk by commits f61df10 and 390d0fa.

Error messages could be improved...

- Issue History
Date Modified Username Field Change
2016-04-11 22:47 octachron New Issue
2016-04-12 19:54 octachron Note Added: 0015724
2016-04-14 16:15 doligez Severity crash => major
2016-04-14 16:15 doligez Status new => acknowledged
2016-04-14 16:15 doligez Target Version => 4.03.0+dev / +beta1
2016-04-15 16:55 garrigue Note Added: 0015766
2016-04-15 16:55 garrigue Status acknowledged => resolved
2016-04-15 16:55 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-04-15 16:55 garrigue Resolution open => fixed
2016-04-15 16:55 garrigue Assigned To => garrigue
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:32 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker