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

[Sebastien Mondet <sebastien.mondet@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4544 bytes --]

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>


Is it intended?

Cheers
Seb





















On Tue, Jan 15, 2013 at 12:59 AM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

> Dear Camlers,
>
> It is a bit unusual, but this message is about changes in trunk.
>
> As you may be aware from past threads, since the introduction of GADTs
> in 4.00, some type information is propagated to pattern-matching, to allow
> it to refine types.
> More recently, types have started being used to disambiguate constructors
> and record fields, which means some more dependency on type information
> in pattern-matching.
>
> However, a weakness of this approach was that propagation was disabled
> as soon as a pattern contained polymorphic variants. The reason is that
> typing rules for polymorphic variants in patterns and expression are subtly
> different, and mixing information without care would lose principality.
>
> At long last I have removed this restriction on the presence of polymorphic
> variants, but this has some consequences on typing:
>
> * while type information is now propagated, information about possibly
>   present constructors still has to be discarded. For instance this means
> that
>   the following code will not be typed as you could expect:
>
>         let f (x : [< `A | `B]) = match x with `A -> 1 | _ -> 2;;
>         val f : [< `A | `B > `A ] -> int
>
>   What happens is that inside pattern-matching, only required constructors
>   are propagated, which reduces the type of x to [> ] (a polymorphic
> variant
>   type with any constructor…)
>   As before, to give an upper bound to the matched type, the type
> annotation
>   must be inside a pattern:
>
>         let f = function (`A : [< `A | `B]) -> 1 | _ -> 2;;
>         val f : [< `A | `B ] -> int = <fun>
>
> * the propagation of type information may lead to failure in some cases
> that
>   where typable before:
>
>         type ab = [ `A | `B ];;
>         let f (x : [`A]) = match x with #ab -> 1;;
>         Error: This pattern matches values of type [? `A | `B ]
>                but a pattern was expected which matches values of type [
> `A ]
>                The second variant type does not allow tag(s) `B
>
>   During pattern-matching it is not allowed to match on absent type
> constructors,
>   even though the type of the patterns would eventually be [< `A | `B],
> which allows
>   discarding `B. ([? `A | `B] denotes a type obeying the rules of
> pattern-matching)
>
> * for the sake of coherence, even if a type was not propagated because it
>   was not known when typing a pattern-matching, we are still going to fail
> if a
>   matched constructor appears to be absent after typing the whole function.
>   (This only applies to propagable types, i.e. polymorphic variant types
> that
>    contain only required constructors)
>
> In particular the last two points are important, because previously such
> uses
> would not have triggered even a warning.
>
> The idea is that allowing propagation of types is more important than
> keeping some not really useful corner cases, but if this is of concern
> to you, I'm interested in feedback.
>
>         Jacques Garrigue
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

[-- Attachment #2: Type: text/html, Size: 5741 bytes --]