0005785: Misbehaviour with abstracted structural type used as GADT index - MantisBT

Mantis Bug Tracker

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0005785

OCaml

OCaml typing

public

2012-10-11 21:43

2013-04-23 02:45

Reporter

yallop

Assigned To

garrigue

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

4.00.1

Target Version

Fixed in Version

4.00.2+dev

Summary

0005785: Misbehaviour with abstracted structural type used as GADT index

Description

$ cat test.ml
module Add (T : sig type two end) =
struct
  type _ t =
  | One : [`One] t
  | Two : T.two t

  let add (type a) : a t * a t -> string = function
    | One, One -> "two"
    | Two, Two -> "four"
end

module M = Add(struct type two = [`One] end)

let _ =
  begin
    print_endline (M.add (M.One, M.Two));
    print_endline (M.add (M.Two, M.One));
  end
$ ocamlc -w A test.ml -o test
$ ./test
two
four

Tags

No tags attached.

test.ml [^] (353 bytes) 2012-10-11 21:43

Relationships

child of

assigned

GADT typing and exhaustiveness bugs

Notes
(0008248) garrigue (manager) 2012-10-12 03:44	Indeed, the fact that a structural type may be compatible with an aliasable type was not taken into account in the compatibility check, and as a result the pattern-matching was wrongly deemed exhaustive. This is fixed in 4.00 and trunk, at revisions 13009 and 13008.

Issue History
Date Modified	Username	Field	Change
2012-10-11 21:43	yallop	New Issue
2012-10-11 21:43	yallop	File Added: test.ml
2012-10-12 03:44	garrigue	Note Added: 0008248
2012-10-12 03:44	garrigue	Status	new => closed
2012-10-12 03:44	garrigue	Assigned To	=> garrigue
2012-10-12 03:44	garrigue	Resolution	open => fixed
2012-10-12 03:44	garrigue	Fixed in Version	=> 4.00.2+dev
2013-04-23 02:45	garrigue	Relationship added	child of 0005998

Copyright © 2000 - 2011 MantisBT Group