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: 7181 Reporter:@chambart Assigned to:@garrigue Status: closed (set by @xavierleroy on 2017-09-24T15:32:09Z) Resolution: fixed Priority: normal Severity: minor Version: 4.03.0+dev / +beta1 Target version: 4.03.1+dev Fixed in version: 4.03.0+dev / +beta1 Category: typing Monitored by:@hcarty
Bug description
The example is
type 'a tree =
| Root : [>Root] tree | Leaf : [Root | Leaf] tree -> [>Leaf] tree
let rec root (type x) (tree : x tree) : [`Root] tree =
match tree with
| Root -> tree
| Leaf parent -> root parent
which fails with
| Root -> tree
^^^^
Error: This expression has type x tree but an expression was expected of type [ Root ] tree Type x = [> Root ] is not compatible with type [ `Root ]
The first variant type does not allow tag(s)
Additional information
By the way, I'm not completely certain that this type should not be accepted
The text was updated successfully, but these errors were encountered:
There is something fishy in trying to take an (exists 'r. [ Root | 'r ]) and turn it into a [ Root ]. In this case, you have no parameter to the Root constructor, so it seems harmless, but you could equally write the following which type-checks:
let rec root (type x) (tree : x tree) : [`Root] tree =
match tree with
| Root -> Root
| Leaf parent -> root parent
if you added a parameter in the Root case, if this parameter does not depend on 'a then you can reuse the trick above, and if it does then your version seems unsound:
type 'a tree =
| Root : ([> Root] as 'a) -> 'a tree | Leaf : [Root | Leaf] tree -> [>Leaf] tree
let rec root (type x) (tree : x tree) : [`Root] tree =
match tree with
| Root _ -> tree
| Leaf parent -> root parent
if I could type-check that I could use it to coerce (Root Leaf) into a ([Root] tree).
Indeed, the error message is confusing.
I suppose you should get something like
Type x = [> Root ] is not compatible with type [ Root ]
The second variant type does not allow tag(s) `AnyOtherTag
Here type x has an existential row, which means that it could contain
anything, so you cannot coerce it to just [`Root].
By the way this also cannot be coerced to [>`Root] for a different reason. The row variable will escape:
| Root -> tree
^^^^
Error: This expression has type x tree but an expression was expected of type
([> Root ] as 'a) tree Type x = [> Root ] is not compatible with type [> `Root ] as 'a
The type constructor $0 would escape its scope
Original bug ID: 7181
Reporter: @chambart
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:09Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.03.0+dev / +beta1
Target version: 4.03.1+dev
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Monitored by: @hcarty
Bug description
The example is
type 'a tree =
| Root : [>
Root] tree | Leaf : [
Root |Leaf] tree -> [>
Leaf] treelet rec root (type x) (tree : x tree) : [`Root] tree =
match tree with
| Root -> tree
| Leaf parent -> root parent
which fails with
| Root -> tree
^^^^
Error: This expression has type x tree but an expression was expected of type [
Root ] tree Type x = [>
Root ] is not compatible with type [ `Root ]The first variant type does not allow tag(s)
Additional information
By the way, I'm not completely certain that this type should not be accepted
The text was updated successfully, but these errors were encountered: