Re: Typing of patterns

[Patrick M Doane <patrick@watson.org>]

On Mon, 5 Jun 2000, Pierre Weis wrote:

> However, we get a strange difference in typing since, as you
> mentioned, the explicit ``as clause'' does not set up a typing
> connection between input and output :
> 
> let (ensure_nil : 'a pliste -> 'b pliste) = function
>   | `Cons (x, l) -> failwith "Not nil"
>   | `Nil as l -> l;;
> val ensure_nil : 'a pliste -> 'b pliste = <fun>
> 
> Jacques may explain us if the above suggested generalization scheme is
> used for identifiers bound in as clauses of patterns (and if not,
> which scheme is used ?)...

This discussion seems related to a recent typing difficulty I have had
with polymorphic variants.

I want to change the data associated to a particular constructor of a
variant and leave the others unmodified:

     # let f = function `A -> `A () | _ as t -> t;;
     Characters 41-42:
     This expression has type [< `A | ..] but is here used with type
       [> `A of unit]

Notice that the type for '_' includes `A when it obviously cannot. One
could include every possible expected type in place of '_' but that
removes one of the advantages of polymorphic variants: that the type can 
be refined and extended easily.


While further exploring this issue I managed to get an uncaught exception
from the type checker:

     # let f = function `A true -> () | `A 5 -> ();; 
     Uncaught exception: File "typing/parmmatch.ml", ...

Taking the conjuction of 'unit' and 'int' does seem to work however,

     # let f = function `A -> () | `A 5 -> ();;
     val f : [< `A of & int] -> unit = <fun>

but it prints the type without mentioning 'unit'.

Patrick Doane