GADT type information is not used to detect unused match cases

[vicuna]

Original bug ID: 6220
Reporter: @lpw25
Assigned to: @garrigue
Status: closed (set by @garrigue on 2015-12-04T00:46:13Z)
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
Child of: #5998 #6437
Monitored by: @gasche @hcarty

Bug description

It seems that warning 11 ("this match case is unused") does not take account of the type information of GADTs.

For example:

type 'a t = I : int t | F : float t;;

type 'a t = I : int t | F : float t

let f : int t -> int = function

  I -> 1;;
val f : int t -> int = <fun>

let f : int t -> int = function

  I -> 1
| _ -> 2;;
  val f : int t -> int = <fun>

I would have expected the second declaration of f to raise warning 11, but it does not.

[vicuna]

Comment author: @garrigue

Indeed, the refined information is not used here.
Not completely clear how to do it, as inclusion is not easy in presence of gadts.

[vicuna]

Comment author: @alainfrisch

Now we get warning 56 ("this match case is unreachable"). Is this considered ok (or should warning 11 be raised) ? I did not follow the discussion about "_ -> ." clauses, but I don't see offhand why this should be a different warning number.

[vicuna]

Comment author: @garrigue

Solved together with its parent.

This has to be a different warning, because if a case is only unreachable (rather than unused), you cannot just remove it, but have to replace it by a refutation case.
Note that 56 is a subcase of 11: you only get warning 56 if both 11 and 56 are turned on.