-
Notifications
You must be signed in to change notification settings - Fork 1.2k
Typechecking bug in presence of constraints and polymorphic types #9603
Copy link
Copy link
Closed
Description
The relaxing of the handling of polymorphic type in #1132 has unearthed a bug in the handling of polymorphic type unification when constraints are involved.
For example, the following code fails
type 'p pair = 'a * 'b constraint 'p = < left:'a; right:'b>
let foo :
< m : 'left 'right. <left:'left; right:'right> pair >
-> < m : 'left 'right. <left:'left; right:'right> pair >
= fun x -> xfor OCaml version starting from at least version 4.01 .
With the heavier reliance on explicitly polymorphic type unification, the following code fails starting with 4.11 :
type 'p pair = 'a * 'b constraint 'p = < left:'a; right:'b>
let error: 'left 'right.
<left:'left; right:'right> pair -> <left:'right; right:'left> pair =
fun (x,y) -> (y,x)Note that this failure has been kind of observed in the wild, since it affects at least of my own library (and one that is not completely a toy): https://github.com/Octachron/orec/blob/master/src/namespace.ml#L307.
Reactions are currently unavailable