0005332: pattern matching problem with GADT

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005332

OCaml

OCaml general

public

2011-08-09 14:35

2011-08-09 16:01

Reporter

dim

Assigned To

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

3.13.0+dev

Summary

0005332: pattern matching problem with GADT

Description

I was playing with the svn version of ocaml and get the following error:

type ('env, 'a) var =
  | Zero : ('a * 'env, 'a) var
  | Succ : ('env, 'a) var -> ('b * 'env, 'a) var

type ('env, 'a) typ =
  | Tint : ('env, int) typ
  | Tbool : ('env, bool) typ
  | Tvar : ('env, 'a) var -> ('env, 'a) typ

let f : type env a. (env, a) typ -> (env, a) typ -> int = fun ta tb ->
  match ta, tb with
    | Tint, Tint -> 0
    | Tbool, Tbool -> 1
    | Tvar var, tb -> 2

let x = f Tint (Tvar Zero)

Here i get no warning when defining f, and x is evaluated to 0. If i remove the Tbool constructor, then i get a warning and a Match_failure exception.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0006086) garrigue (manager) 2011-08-09 16:01	Stupid bug in the auxiliary function Parmatch.combinations. Thanks for your report.

Issue History
Date Modified	Username	Field	Change
2011-08-09 14:35	dim	New Issue
2011-08-09 16:01	garrigue	Note Added: 0006086
2011-08-09 16:01	garrigue	Status	new => closed
2011-08-09 16:01	garrigue	Resolution	open => fixed
2011-08-09 16:01	garrigue	Fixed in Version	=> 3.13.0+dev