Original bug ID: 6437
Reporter: mqtthiqs
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:16:34Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.01.0
Target version: 4.03.0+dev / +beta1
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Related to: #6403 #6801
Child of: #5998
Parent of: #6220
Monitored by: @gasche @yallop @alainfrisch

Bug description

This code:

type ('a, 'b) ctx =
| Nil : (unit, unit) ctx
| Cons : ('a, 'b) ctx -> ('a * unit, 'b * unit) ctx

type 'a var =
| O : ('a * unit) var
| S : 'a var -> ('a * unit) var

let rec f : type g1 g2. (g1, g2) ctx * g1 var -> g2 var = function
| Cons g, O -> O
| Cons g, S n -> S (f (g, n))
(* | Nil, _ -> (assert false) *)

reports a warning for non-exhaustive pattern-matching, whereas (I think) it should not, since the last commented case is impossible.
Or am I missing something?

File attachments

• type_pat_cps.diff
• type_pat_cps2.diff
• type_pat_cps3.diff