0005553: Type checker output contains type variable with suprising name in 3.13.0+dev11

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005553

OCaml

OCaml typing

public

2012-03-22 20:20

2012-03-23 03:19

Reporter

rdicosmo

Assigned To

garrigue

Priority

low

Severity

minor

Reproducibility

always

Status

resolved

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

4.00.0+dev

Summary

0005553: Type checker output contains type variable with suprising name in 3.13.0+dev11

Description

In 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 Reproduce

Just 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 Information

If 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 :).

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

Relationships