Original bug ID: 5853
Reporter: electreg
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:43Z)
Resolution: not a bug
Priority: normal
Severity: minor
Platform: amd64
OS: Linux
OS Version: ubuntu-12.04
Version: 4.00.1
Category: typing
Related to: #5892
Child of: #5998

Bug description

Sometimes compiler gives "Warning 8: this pattern-matching is not exhaustive." when it is not true.
I tried to make Nat-indexed list:

module Nat = struct
type z
type 'a s
end

type (, 'l) iList =
| INil : (, Nat.z) iList
| ICons : 'a * ('a, 'n) iList -> ('a, 'n Nat.s) iList

and then write "safe head" function:

let hd : ('a, 'n Nat.s) iList -> 'a = fun (ICons(x, _)) -> x

So expression hd INil is ill-typed; however, compiler gives me "pattern-matching is not exhaustive" warning.

Steps to reproduce

Copy-paste code from description and try to run it.