0005736: Support GADTs in or-patterns

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005736

OCaml

OCaml typing

public

2012-08-22 23:12

2013-04-23 02:52

Reporter

omion

Assigned To

garrigue

Priority

normal

Severity

feature

Reproducibility

always

Status

confirmed

Resolution

open

Platform

OS Version

Product Version

4.00.0

Target Version

Fixed in Version

Summary

0005736: Support GADTs in or-patterns

Description

Currently, 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.

Tags

No tags attached.

Attached Files

Relationships

child of

0005998

assigned

garrigue

GADT typing and exhaustiveness bugs

Notes
(0007975) 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.

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