Original bug ID: 6673
Reporter: @fpottier
Assigned to: @garrigue
Status: acknowledged (set by @garrigue on 2014-12-18T01:17:40Z)
Resolution: duplicate
Priority: normal
Severity: minor
Version: 4.01.0
Category: typing
Has duplicate: #7483
Related to: #6569
Monitored by: @ygrek

Bug description

This is accepted:
let f : 'a . 'a -> 'a = fun x -> x;;

And this is accepted too:
let f = fun (x : 'a) -> x;;

But this is rejected:
let f : 'a . 'a -> 'a = fun (x : 'a) -> x;;
Error: This definition has type 'a -> 'a which is less general than
'a0. 'a0 -> 'a0

This behavior seems inconsistent to me, and somewhat unplesant.
(I have teaching in mind.) Is it a bug and could it be fixed?

Thanks
Francois.

File attachments

• poly.patch
• poly2.patch
• poly3.patch