Anonymous | Login | Signup for a new account 2017-05-23 07:07 CEST
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005553OCamltypingpublic2012-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 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. " 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 2017-02-23 16:45 doligez Category OCaml typing => typing

 Copyright © 2000 - 2011 MantisBT Group