Skip to content

Typechecking bug in presence of constraints and polymorphic types #9603

@Octachron

Description

@Octachron

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 -> x

for 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions