Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixed conjunctive polymorphic variant tags do not unify with themselves #7496

Closed
vicuna opened this issue Feb 27, 2017 · 1 comment
Closed
Assignees

Comments

@vicuna
Copy link

vicuna commented Feb 27, 2017

Original bug ID: 7496
Reporter: @lpw25
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-03-14T02:59:21Z)
Resolution: fixed
Priority: low
Severity: minor
Version: 4.04.0
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing

Bug description

This is the unification version of the complaint in #5927. Fixed polymorphic variant types with conjunctions do not unify with themselves. For example:

let f (x : < m: 'a. ([< Foo of int & float] as 'a) -> unit>) : < m: 'a. ([< Foo of int & float] as 'a) -> unit> = x;;

Characters 127-128:
: < m: 'a. ([< Foo of int & float] as 'a) -> unit> = x;; ^ Error: This expression has type < m : 'a. ([< Foo of int & float ] as 'a) -> unit >
but an expression was expected of type
< m : 'b. ([< Foo of int & float ] as 'b) -> unit > Types for tag Foo are incompatible

And:

type t = { x : 'a. ([< `Foo of int & float] as 'a) -> unit };;

type t = { x : 'a. ([< `Foo of int & float ] as 'a) -> unit; }

let f t = { x = t.x };;

Characters 16-19:
let f t = { x = t.x };;
^^^
Error: This expression has type [< Foo of int & float ] -> unit but an expression was expected of type [< Foo of int & float ] -> unit
Types for tag `Foo are incompatible

I appreciate that these types are not meant to be actively used in practice. However, I think it is a mistake to have them break basic properties like the reflexivity of equality and the idempotence of unification. These properties are somewhat relied upon by other parts of the type-checker for sane behaviour.

For example, my patch for #6673 fails on the new test case for #7269. Not because there is anything wrong with the patch but because it happens to introduce an additional idempotent unification which fails for the conjunctive tags in that test.

@vicuna
Copy link
Author

vicuna commented Mar 14, 2017

Comment author: @garrigue

Fixed Ctype.unify_row_field in commit 1c97fde.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants