From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <francois.pottier@inria.fr>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 023997FCE0
	for <caml-list@sympa.inria.fr>; Tue, 31 Mar 2015 21:45:32 +0200 (CEST)
X-IronPort-AV: E=Sophos;i="5.11,503,1422918000"; 
   d="scan'208";a="130961162"
Received: from yquem.inria.fr ([128.93.8.37])
  by mail2-relais-roc.national.inria.fr with ESMTP; 31 Mar 2015 21:45:31 +0200
Received: by yquem.inria.fr (Postfix, from userid 18965)
	id E4CD0E199F; Tue, 31 Mar 2015 21:45:31 +0200 (CEST)
Date: Tue, 31 Mar 2015 21:45:31 +0200
From: Francois Pottier <Francois.Pottier@inria.fr>
To: Andre Nathan <andre@digirati.com.br>
Cc: caml users <caml-list@inria.fr>
Message-ID: <20150331194531.GA12168@yquem.inria.fr>
Reply-To: Francois.Pottier@inria.fr
References: <551AE480.1000008@digirati.com.br>
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <551AE480.1000008@digirati.com.br>
User-Agent: Mutt/1.5.21 (2010-09-15)
Subject: Re: [Caml-list] GADTs and Menhir

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/