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: 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.
The text was updated successfully, but these errors were encountered:
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 incompatibleAnd:
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 ] -> unitTypes 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.
The text was updated successfully, but these errors were encountered: