Forget this message.

Gerd

Am Freitag, den 26.08.2016, 00:33 +0200 schrieb Gerd Stolpmann:
> 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
------------------------------------------------------------