Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

strange behavior of GADT with plymorphic variants #7592

Closed
vicuna opened this issue Jul 21, 2017 · 3 comments
Closed

strange behavior of GADT with plymorphic variants #7592

vicuna opened this issue Jul 21, 2017 · 3 comments
Assignees
Labels
feature-wish Stale typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Jul 21, 2017

Original bug ID: 7592
Reporter: lavi
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2017-08-02T04:17:38Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.05.0
Category: typing
Child of: #5998

Bug description

This 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
@vicuna
Copy link
Author

vicuna commented Aug 2, 2017

Comment author: @garrigue

Incremental refinement of object and polymorphic variant types through GADTs is not supported yet.

@vicuna
Copy link
Author

vicuna commented Oct 10, 2017

Comment author: @xavierleroy

This reads like a feature wish. Decrementing severity.

@github-actions
Copy link

github-actions bot commented May 7, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 7, 2020
@Octachron Octachron added the typing-GADTS GADT typing and exhaustiveness bugs label May 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature-wish Stale typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants