You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
Bug description
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)
"
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
Bug description
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 ->$'b -> nil) t -> 'a n -> $ 'b n -> unit ".
let Cons(Elt dim, _) = sh in ()
"
The type inferred for "undetected" is "('a ->
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: