Original bug ID: 7160
Reporter: mandrykin
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:01Z)
Resolution: fixed
Priority: low
Severity: crash
Platform: x86_64
OS: Linux 3.19.0
OS Version: Ubuntu 15.04
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Monitored by: @hcarty

Bug description

The attached example shows how type defining a type synonym with an incompatible manifest can actually change the previous definition instead of being rejected. This can potentially lead to segmentation faults when ill-typed programs are accepted.

Steps to reproduce

ocaml

(* OCaml version 4.03.0+beta1*)
type 'a any = [< A | B] as 'a;;
(* type 'a any = 'a constraint 'a = [< A | B ] )
type _ t = X : int -> [A] t | Y : string -> [B] t | C : (_ any as 'l) t -> 'l t;;
( type _ t =
X : int -> [ A ] t | Y : string -> [ B ] t
| C : 'a any t -> ([< A | B ] as 'a) any t )
let rec f = function Y s -> s | C y -> f y;;
( val f : [ B ] any t -> string = <fun> *) f (Y "5");; (* - : string = "5" *) f (C (Y "5"));; (* - : string = "5" *) f (X 5);; (* Error: This expression has type [ A ] t
but an expression was expected of type [ B ] any t Type [ A ] is not compatible with type [ B ] any = [ B ]
These two variant types have no intersection )
f (C (X 5));;
( Error: This expression has type [ A ] t but an expression was expected of type [ B ] any any t
Type [ A ] is not compatible with type [ B ] any any = [ B ] These two variant types have no intersection *) (* Until now everything is OK *) type 'a tt = 'a t = X : int -> [A] tt | Y : string -> [B] tt | C : [< A | B] t -> [< A | B] tt;; (* type 'a tt = 'a t = X : int -> [ A ] tt
| Y : string -> [ B ] tt | C : [< A | B ] t -> [< A | B ] tt *) (* This type synonym definition is accepted though its constraints for the C constructor are different (no equality previously expressed with variable 'l) *) (* Now even the definition of type _ t itself is changed *) f (Y "5");; (* - : string = "5" *) f (C (Y "5"));; (* - : string = "5" *) f (X 5);; (* Error: This expression has type [ A ] tt = [ A ] t but an expression was expected of type [ B ] any t
Type [ A ] is not compatible with type [ B ] any = [ `B ]
These two variant types have no intersection )
( The following should not be accepted *)
f (C (X 5));;
Segmentation fault (core dumped)

File attachments

• incorrect_weakening2.ml
• incorrect_weakening_through_manifest.ml