Soundness bug with GADTs and lazy #7421
Description
Original bug ID: 7421
Reporter: @lpw25
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-12-10T02:48:23Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.0
Fixed in version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Category: typing
Monitored by: @gasche @yallop
Bug description
The exhaustivity/refutation checks do not taken into account the hidden | member of the lazy type:
# type (_, _) eq = Refl : ('a, 'a) eq;;
type (_, _) eq = Refl : ('a, 'a) eq
# type empty = (int, unit) eq;;
type empty = (int, unit) eq
# let f (x : ('a, empty Lazy.t) result) =
match x with
| Ok x -> x
| Error (lazy _) -> .;;
val f : ('a, empty Lazy.t) result -> 'a = <fun>
# (f (Error (lazy (raise Not_found))) : string list list);;
Segmentation fault