You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 5553 Reporter: rdicosmo Assigned to:@garrigue Status: closed (set by @xavierleroy on 2013-08-31T10:48:50Z) Resolution: fixed Priority: low Severity: minor Fixed in version: 4.00.0+dev Category: typing
Bug 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 =
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 =
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 =
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 :).
The text was updated successfully, but these errors were encountered:
Original bug ID: 5553
Reporter: rdicosmo
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2013-08-31T10:48:50Z)
Resolution: fixed
Priority: low
Severity: minor
Fixed in version: 4.00.0+dev
Category: typing
Bug 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 =
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 =
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 =
Here is what Jonathan hinted at as a potential explanation
The text was updated successfully, but these errors were encountered: