Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007592OCamltypingpublic2017-07-21 13:112017-10-10 14:31
Reporterlavi 
Assigned Togarrigue 
PrioritynormalSeverityfeatureReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product Version4.05.0 
Target VersionFixed in Version 
Summary0007592: strange behavior of GADT with plymorphic variants
DescriptionThis is not a bug as OCaml stay in the safe side, but behavior of GADT in presence of polymorphic variant is sometimes disturbing.

For example, the following is accepted:

type _ c1 = C1 : [> `A | `B ] c1
type _ c2 = C2 : [> `A | `C ] c2
let f : type a. a c1 -> a c2 -> a = fun C1 C2 -> `A
let x = f C1 C2
let g : type a. a c1 -> a c2 -> a = fun C1 C2 -> `B
let y = g C1 C2

with the right type:
val y : [> `A | `B | `C ] = `B

However this does not work with `C:

let h : type a. a c1 -> a c2 -> a = fun C1 C2 -> `C;;
Error: This expression has type [> `C ]
       but an expression was expected of type a
       The second variant type does not allow tag(s) `C
TagsNo tags attached.
Attached Files

- Relationships
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0018154)
garrigue (manager)
2017-08-02 06:17

Incremental refinement of object and polymorphic variant types through GADTs is not supported yet.
(0018533)
xleroy (administrator)
2017-10-10 14:31

This reads like a feature wish. Decrementing severity.

- Issue History
Date Modified Username Field Change
2017-07-21 13:11 lavi New Issue
2017-08-02 06:17 garrigue Note Added: 0018154
2017-08-02 06:17 garrigue Assigned To => garrigue
2017-08-02 06:17 garrigue Status new => confirmed
2017-08-02 06:18 garrigue Relationship added child of 0005998
2017-10-10 14:31 xleroy Note Added: 0018533
2017-10-10 14:31 xleroy Severity minor => feature


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker