Re: [Caml-list] Propagating types to pattern-matching

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/02/12, at 0:31, Sebastien Mondet <sebastien.mondet@gmail.com> wrote:

> Hi Jacques
> 
> I don't know if this directly related, or if it is actually intended, but this looks like a regression to me:
> 
> 
> With OCaml version 4.00.1+dev2_2012-08-06  (4.00.1+short-types in Opam):
> 
> # let f = function 0 -> `zero | 1 -> `one | _ -> `some;;
> val f : int -> [> `one | `some | `zero ] = <fun>
> 
> # let g x = match f x with `one -> 1 | `zero -> 0;;
> Error: This pattern matches values of type [< `one | `zero ]
>        but a pattern was expected which matches values of type
>          [> `one | `some | `zero ]
>        The first variant type does not allow tag(s) `some
> 
> which is the nice behavior we were used to,
> but with OCaml version 4.01.0+dev10-2012-10-16  (a.k.a.  4.01.0dev+short-paths), the error has been downgraded to a warning:
> 
> # let f = function 0 -> `zero | 1 -> `one | _ -> `some;;
> val f : int -> [> `one | `some | `zero ] = <fun>
> 
> # let g x = match f x with `one -> 1 | `zero -> 0;;
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> `some
> val g : int -> int = <fun>
> 

This is related, and this is the intended behavior.
For polymorphic variants, you get a warning if the type was known early enough,
and a hard error otherwise.
Actually, I see it as a progress, since the warning gives you a counter-example,
whereas the error message only gives you a discrepancy between types.

For me the only sane handling of partial matching is to see it as an error,
so use at least -warn-error P. (Or at least watch for warnings)

	Jacques Garrigue