Re: [Caml-list] GADTs and Menhir

[Francois Pottier <Francois.Pottier@inria.fr>]

On Tue, Mar 31, 2015 at 03:16:32PM -0300, Andre Nathan wrote:
> value:
>   | i = INTEGER  { Int i }
>   | b = BOOL     { Bool b }

The problem lies here. What is the OCaml type of the symbol "value"? The OCaml
compiler complains that in one branch it seems to be int Foo.t, but in the
other branch it seems to be bool Foo.t. (The problem does not have anything to
do with Menhir, really.)

Usually, it is not advisable to try to perform parsing and type-checking in
one single phase. So, my advice would be to:

  1- perform parsing in the usual way,
     constructing ASTs in a normal algebraic data type "ast"
     (not a GADT);

  2- perform type-checking (or type inference).
     If you insist on using GADTs, you will probably need
     a GADT of terms (your type 'a Foo.t) and
     a GADT of type representations ('a ty)
     and the type-checking function will have type
     ast -> 'a ty -> 'a Foo.t option
     which means that, given an untyped term and
     a representation of an expected type, it
     either fails or succeeds and produces a typed term.

There are examples of this kind of thing online, e.g.
http://www.cs.ox.ac.uk/projects/gip/school/tc.hs
by Stephanie Weirich.

Hope this helps,

-- 
François Pottier
Francois.Pottier@inria.fr
http://gallium.inria.fr/~fpottier/