Re: [Caml-list] GADT in an optional parameter

[oleg@okmij.org]

> Now, in my woolly way, I thought that the default value for an optional
> parameter behaved /almost/ like syntactic sugar, but clearly not. Is there a
> way to annotate this to achieve what I'm after? 

Actually a default parameter is syntactic sugar. When the type checker
sees

        fun ?(p=v) -> body

it essentially macro-expands the expression to the following

   fun xxOpt -> let p = match xxOpt with
                         | Some xxSth -> xxSth
                         | None       -> v
                in body
and then type checks the resulting macro-expansion. Here xxOpt and
xxSth are internally generated identifiers with funky names (the type
checker is fond of generating funny identifiers, especially when
dealing with objects). You can see this expansion process for yourself,
typing/typecore.ml; search for the line

  | Pexp_function (l, Some default, [spat, sbody]) ->

If you apply this expansion to your function

> let find : type s t . 
>     ?mode:(s, t) wrap -> string -> s Map.Make(String).t -> t = 
>  fun ?(mode = Exn) key map ->

you will see the error right away. Let's take a simpler GADT for clarity

    type _ g = 
      | Int : int -> int g 
      | Str : string -> string g
    ;;

and write a consumer of GADT values (which pattern-matches on them)

    let g_consumer : type a. a g -> string = function
      | Int x -> string_of_int x
      | Str x -> x
    ;;

This is a polymorphic function: it can handle data of the type
[int g] and [string g]:

    g_consumer (Int 1);;
    g_consumer (Str "str");;

Let us attempt to write a producer:

let g_producer1 : type a. a g = Int 1;;

we immediately get an error:

  let g_producer1 : type a. a g = Int 1;;
                                  ^^^^^
Error: This expression has type int g but an expression was expected of type
         a g


Although we may consume either [int g] or [string g], we can produce
only one of them. Likewise,
        fun x -> match x with
                   true ->  Int 1
                 | false -> Str "str"
;;
fails similarly.


If we desugar the original example with the optional parameter, we get
something like

        let mode = match xxOpt with
                 | Some x -> x
                 | None   -> Int 1

the parameter mode is supposed to be polymorphic, [a g], but the match
expression, which produces GADT, cannot produce the polymorphic GADT
type. If we see Int 1, then result must be [int g]. 

Again, a function that pattern-matches on GADT can be polymorphic. A
function/expression that _produces_ GADT (that is, uses GADT
constructors to produce values) cannot be polymorphic in the resulting
GADT.