0005689: Problem with GADTs and polymorphic variants

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005689

OCaml

OCaml typing

public

2012-07-16 17:21

2013-04-23 02:53

Reporter

lpw25

Assigned To

garrigue

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

4.01.0+dev

Fixed in Version

4.00.0+dev

Summary

0005689: Problem with GADTs and polymorphic variants

Description

As I understand it the types:

type inkind = [ `Link | `Nonlink ]

type _ inline_t =
    | Text: string -> [< inkind > `Nonlink ] inline_t
    | Bold: 'a inline_t list -> 'a inline_t
    | Link: string -> [< inkind > `Link ] inline_t
    | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] inline_t

should maintain the invariant that a Mref cannot contain another Mref or a Link, because these have type [< inkind > `Link] and the Mref only accepts [ `Nonlink ].

However the attached file uses GADTs to break this invariant producing a value:

val broken_invariant : inkind inline_t = Mref ("foo", [Link <abstr>])

Tags

No tags attached.

Attached Files

broken.ml [^] (1,178 bytes) 2012-07-16 17:21

Relationships

child of

0005998

assigned

garrigue

GADT typing and exhaustiveness bugs

Notes
(0007773) garrigue (manager) 2012-07-18 05:37	Fixed in 4.00 and trunk, revisions 12726 and 12725. Row fields should be handled as fixed when the row variable is a type constructor.

Issue History
Date Modified	Username	Field	Change
2012-07-16 17:21	lpw25	New Issue
2012-07-16 17:21	lpw25	File Added: broken.ml
2012-07-17 14:26	doligez	Status	new => acknowledged
2012-07-17 14:26	doligez	Target Version	=> 4.01.0+dev
2012-07-17 14:26	doligez	Description Updated	View Revisions
2012-07-18 03:22	garrigue	Assigned To	=> garrigue
2012-07-18 03:22	garrigue	Status	acknowledged => assigned
2012-07-18 05:37	garrigue	Note Added: 0007773
2012-07-18 05:37	garrigue	Status	assigned => closed
2012-07-18 05:37	garrigue	Resolution	open => fixed
2012-07-18 05:37	garrigue	Fixed in Version	=> 4.00.0+dev
2013-04-23 02:53	garrigue	Relationship added	child of 0005998