Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007160OCamltypingpublic2016-03-02 13:242017-09-24 17:32
Reportermandrykin 
Assigned Togarrigue 
PrioritylowSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64OSLinux 3.19.0OS VersionUbuntu 15.04
Product Version 
Target VersionFixed in Version4.03.0+dev / +beta1 
Summary0007160: Type synonym definitions can weaken constraints of previously defined types through their manifests
DescriptionThe 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)
TagsNo tags attached.
Attached Files? file icon incorrect_weakening_through_manifest.ml [^] (370 bytes) 2016-03-02 13:24 [Show Content]
? file icon incorrect_weakening2.ml [^] (286 bytes) 2016-03-02 15:26 [Show Content]

- Relationships

-  Notes
(0015418)
mandrykin (reporter)
2016-03-02 15:27

Attached a smaller example.
(0015422)
garrigue (manager)
2016-03-03 02:20

Thank you, this is a nasty soundness bug, and went completely undetected since the introduction of GADTs.

This is fixed in 4.03 and trunk, at commits e21dd56 and a18af2a.

- Issue History
Date Modified Username Field Change
2016-03-02 13:24 mandrykin New Issue
2016-03-02 13:24 mandrykin File Added: incorrect_weakening_through_manifest.ml
2016-03-02 15:26 mandrykin File Added: incorrect_weakening2.ml
2016-03-02 15:27 mandrykin Note Added: 0015418
2016-03-03 02:20 garrigue Note Added: 0015422
2016-03-03 02:20 garrigue Status new => resolved
2016-03-03 02:20 garrigue Fixed in Version => 4.03.0+dev / +beta1
2016-03-03 02:20 garrigue Resolution open => fixed
2016-03-03 02:20 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