Skip to content

another broken GADT exhaustiveness check #6403

@vicuna

Description

@vicuna

Original bug ID: 6403
Reporter: @gasche
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:14:46Z)
Resolution: fixed
Priority: low
Severity: minor
Version: 4.02.0+dev
Target version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Has duplicate: #6801
Related to: #6437 #6598
Child of: #5998
Monitored by: @yallop

Bug description

OCaml version 4.02.0+dev5-2014-04-29

type (_, _) eq = Refl : ('a, 'a) eq;;

type empty = { bottom : 'a . 'a };;

type ('a, 'b) sum = Left of 'a | Right of 'b;;

let notequal : ((int, bool) eq, empty) sum -> empty = function

| Right empty -> empty;;  

Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Left _
val notequal : ((int, bool) eq, empty) sum -> empty =

File attachments

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions