Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005736OCamltypingpublic2012-08-22 23:122017-02-18 17:23
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.00.0 
Target VersionlaterFixed in Version 
Summary0005736: Support GADTs in or-patterns
DescriptionCurrently, if you have a GADT with multiple branches sharing the same type, eg:
type _ gadt =
| Float : float -> float gadt
| Float2 : float -> float gadt
| Int : int -> int gadt

then try to use Float and Float2 in one branch of a function:
let type_of_gadt : type t. t gadt -> string = function
| Float _ | Float2 _ -> "float"
| Int _ -> "int"

this will not pass the type checker, even though Float and Float2 have the same type:
Error: This pattern matches values of type float gadt
       but a pattern was expected which matches values of type t gadt

You would have to have each variant:
let type_of_gadt : type t. t gadt -> string = function
| Float _ -> "float"
| Float2 _ -> "float"
| Int _ -> "int"

or, matching with the default "_" will work since it's not an or-pattern, but this only works well if there is only one type in the GADT that has the problem:
let type_of_gadt : type t. t gadt -> string = function
| Int _ -> "int"
| _ -> "float"

It would be handy to be able to combine the branches for GADT constructors that refer to the same types.
TagsNo tags attached.
Attached Files

- Relationships
related to 0007319acknowledged Provide a way to ignore existentials in GADT pattern matching 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
garrigue (manager)
2012-08-23 01:27

This one is a long-term goal.
To do that, one would need to know that the branches are equivalent,
but in the current implementation of GADTs there is no way to check that.
That is, we end up with two environments, we need to compare them,
and worse, we need to drop one of the two and still be safe for that branch...
Maybe we could use the summary, but this is still going to be difficult,
particularly if we are creating fresh skolem variables in both patterns.
xleroy (administrator)
2017-02-18 17:23

Moving to "later" based on @garrigue's comment.

- Issue History
Date Modified Username Field Change
2012-08-22 23:12 omion New Issue
2012-08-23 01:19 garrigue Assigned To => garrigue
2012-08-23 01:19 garrigue Status new => assigned
2012-08-23 01:27 garrigue Note Added: 0007975
2012-08-23 01:27 garrigue Status assigned => confirmed
2013-04-23 02:52 garrigue Relationship added child of 0005998
2016-08-04 15:04 yallop Relationship added related to 0007319
2016-09-07 16:49 shinwell Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2017-02-18 17:23 xleroy Note Added: 0017335
2017-02-18 17:23 xleroy Target Version 4.05.0 +dev/beta1/beta2/beta3/rc1 => later
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker