Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005553OCamlOCaml typingpublic2012-03-22 20:202013-08-31 12:48
Reporterrdicosmo 
Assigned Togarrigue 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.00.0+dev 
Summary0005553: Type checker output contains type variable with suprising name in 3.13.0+dev11
DescriptionIn the following example code, the type of the lengthIn the following example code, the type of the length
function contains a type variable with a surprising name:

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

Indeed, in 3.13.0+dev11 (2012-01-26), we get

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

The 'a1 in the type is quite puzzling, and it would
be better to print 'a in place of it
function contains a type variable with a surprising name:

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

Indeed, in 3.13.0+dev11 (2012-01-26), we get

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

The 'a1 in the type is quite puzzling, and it would
be better to print 'a in place of it.
Steps To ReproduceJust type

 type ('a, 'b) l =
 Nil : ('a, 'b) l
 | Cons : 'b * ('a, 'b) l -> ('a, 'b) l;;
 
 let rec length : type a b. (a,b) l -> 'a = function
 | Nil -> 0
 | (Cons (_,r)) -> 1+ (length r);;
Additional InformationIf we use different names for the type variables in the GADT,
the problem does not show up

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

 val length : ('d, 'e) l -> int = <fun>

Here is what Jonathan hinted at as a potential explanation

> Jacques Garrigue recently implemented a patch that tries to keep user-provided
> type names when printing out types, and also when giving error
> messages. In your
> example, there probably is an internal variable that's called "a" because of the
> type name you provided. Some wizardry happens with GADTs, so another type
> variable is generated. The other one ends up being printed, and because it's
> called "a" too, the type-checker has to find another suitable name.
>
> Or something like that. Maybe change type a b. to type foo bar. will give
> different results :).
 
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0007132)
garrigue (manager)
2012-03-23 03:19

Fixed by not allowing a type variable to have the same name as a local type in the "type a b. <typexp>" syntactic sugar.

- Issue History
Date Modified Username Field Change
2012-03-22 20:20 rdicosmo New Issue
2012-03-23 03:14 garrigue Assigned To => garrigue
2012-03-23 03:14 garrigue Status new => assigned
2012-03-23 03:19 garrigue Note Added: 0007132
2012-03-23 03:19 garrigue Status assigned => resolved
2012-03-23 03:19 garrigue Fixed in Version => 4.00.0+dev
2012-03-23 03:19 garrigue Resolution open => fixed
2013-08-31 12:48 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker