Hi,

just fixing up some GADT code. I came across this:

I have a module M with module type T:

module type T = sig
  type p
  val p_type : p Ztypes.ztype
  val output : float -> p
end

Now, Ztypes.ztype is a GADT like

type _ ztype =
  | Zstring : string ztype
  | Zfloat : float ztype
  | ...

In a function calling M.output I cannot assume that p=float unless I
check it explicitly. So I wrote

let f() =
  let m_output =
    match M.p_type with
      | Ztypes.Zfloat -> (M.output : float -> float)
      | _ -> assert false in
 ...

This doesn't type-check. Funnily, you can fix it by simply adding a
newtype to the function:

let f : type t = fun() ->
  let m_output =
    match M.p_type with
      |
Ztypes.Zfloat -> (M.output : float -> float)
      | _ -> assert false
in
 ...

It is just the presence of t that makes it type-check. This type is not in any way bound to the type parameter of ztype, and this is somewhat unexpected. From a user's perspective it is very comfy that the newtype works like a configuration switch for the type checker. Nevertheless, I wonder why it is like that.

Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------