Original bug ID: 7222 Reporter:@Octachron Assigned to:@garrigue Status: closed (set by @xavierleroy on 2017-09-24T15:32:19Z) Resolution: fixed Priority: normal Severity: major Version: 4.02.3 Target version: 4.03.0+dev / +beta1 Fixed in version: 4.03.0+dev / +beta1 Category: typing Monitored by:@gasche@hcarty
The 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.
The text was updated successfully, but these errors were encountered:
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)