Re: [Caml-list] problem to use gadt

[Gabriel Scherer <gabriel.scherer@gmail.com>]

The typing rule for Or is rather weird: any type can be used as the
result type, which is non-standard. You could define a dummy type
"any"

  type any = Any

  [...]

  | Or : _ t * _ t -> any t

and the output type of Or wouldn't be polymorphic anymore, so the
value restriction (
http://caml.inria.fr/resources/doc/faq/core.en.html#weak-type-variables
) wouldn't be a problem anymore.

On Sun, Feb 15, 2015 at 2:35 PM, Nicolas Boulay <nicolas@boulay.name> wrote:
> I try to define my own type system using gadt. But it seems that is complex
> to mix both type system : mine and the ocaml one.
>
> This tiny example did not compile:
>
> type _ t =
>  | Or: _ t * _ t -> _ t
>  | Int : int t
>  | Float : float t
>
> let a = Or (Int, Float)  (*is ok*)
>
> let (||)  a b = Or (a, b)
>
> let aa = Int || Float (*Error: '_a t, contains type variable that cannot be
> generalized*)
>
> Using an operator make a difference. But how to exprime "don't care" if a
> choice between 2 types is not possible to be define.  It could be nice if
> "('a | 'b) t" worked :) Should i use normal sum type, and make all type
> check by a function ?
>
> Nicolas Boulay