[Caml-list] Funny name for a type variable in the output: should this be filed on the BTS?

[Roberto Di Cosmo <roberto@dicosmo.org>]

I was playing around some more with GADTs, preparing my next course
on functional programming, and came across an example on
which the type checker outputs a type containing a funny name
for a type variable. 

I do not know if this qualifies as a bug, so before filing it, I'd
love some feedback.

Here we are: I am writing an example to show how one can code
a well typed length function for empty/nonempty list; we start
with the type definition

 type empty
 type nonempty

 type ('a, 'b) l =
     Nil : (empty, 'b) l
   | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;;

then we move on to the length function

 let rec length : type a b. (a,b) l -> 'a = function 
   | Nil -> 0 
   | (Cons (_,r)) -> 1+ (length r);;

Hey, you say, the natural type to declare for length should be

   type a b. (a,b) l -> int

but as you see, for some mysterious reason I ended
up writing something silly (dont ask why, I am just
very well known to step on strange bugs as easily
as I breath)

   type a b. (a,b) l -> 'a

The type checker is happy anyway: 'a will be instantiated
to int, and the declaration of length is accepted... but now
look at the output type

   val length : ('a1, 'b) l -> int = <fun>

Why do we get 'a1, and not 'a, in the type?

Well, probably, since 'a is instantiated to int during
type checking, it may be the case that 'a, as type name, is
still marked as taken during the type output, so we get ('a1,'b)

The type is perfectly sound... it is just 'surprising' for
a regular user... do you think this should be considered a bug?

--Roberto
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 6C08 (6th floor)
175, rue du Chevaleret, XIII
Metro Chevaleret, ligne 6
------------------------------------------------------------------