Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005689OCamlOCaml typingpublic2012-07-16 17:212013-04-23 02:53
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target Version4.01.0+devFixed in Version4.00.0+dev 
Summary0005689: Problem with GADTs and polymorphic variants
DescriptionAs 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>])
TagsNo tags attached.
Attached Files? file icon broken.ml [^] (1,178 bytes) 2012-07-16 17:21 [Show Content]

- Relationships
child of 0005998assignedgarrigue 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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker