[Caml-list] GADT magic

[Rodolphe Lepigre <rodolphe.lepigre@univ-savoie.fr>]

Dear list,

I am using a GADT and some phantom types to implement an abstract syntax
tree for some functional programming language, say the λ-calculus.

My first type definition was something like:

==========
type valu =
  | LVar of string
  | LAbs of valu -> term
and  term =
  | Valu of valu
  | Appl of term * term
==========

This works fine, but it is annoying to work with because of the coercion
constructor "Valu". Then I decided to be to smarter and use some GADT and
phantom types:

==========
type v
type t

type _ expr =
  | LVar : string              -> 'a expr
  | LAbs : (v expr -> 'b expr) -> 'a expr
  | Appl : 'a expr * 'b expr   ->  t expr

type term = t expr
type valu = v expr
==========

This definition is much more convenient since the type "valu" is (kind of)
a subtype of the type "term". It is not a real subtype since I had to
define a function with the type:

==========
val expr_to_term : type a. a expr -> term
==========

This function is exactly the identity function, but for the type checker
to accept it I need to be quite explicit:

==========
let expr_to_term : type a. a expr -> term = function
  | LVar(x)   -> LVar(x)
  | LAbs(f)   -> LAbs(f)
  | Appl(t,u) -> Appl(t,u)
==========

Of course, a better and more efficient implementation for this function
is "Obj.magic", but this is not the question here. I was expecting the
following definition to work:

==========
let expr_to_term : type a. a expr -> term = function
  | LVar(x)   -> LVar(x)
  | LAbs(f)   -> LAbs(f)
  | t         -> t
==========

But it does not type check. This is weird because all remaining patterns
captured by the "t" have type "term"...

Is this normal behaviour? Is this a bug?

Rodolphe
-- 
Rodolphe Lepigre
LAMA, Université Savoie Mont Blanc, FRANCE
http://lama.univ-smb.fr/~lepigre/