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: 5242 Reporter: SpiceGuid Assigned to:@garrigue Status: closed (set by @xavierleroy on 2013-08-31T10:43:54Z) Resolution: not a bug Priority: normal Severity: minor Version: 3.11.0 Fixed in version: 3.12.0 Category: ~DO NOT USE (was: OCaml general)
Bug description
It seems to me the compiler assumes a recursive type to be regular even when told otherwise. The consequence is restricted generality, even when full generality is explicited.
type ('a, 'b) bijective_map =
| Nil
| Cons of 'a * 'b * ('b, 'a) bijective_map
let rec connected : ('a -> 'b -> bool) -> ('a, 'b) bijective_map -> bool =
fun r -> function
| Nil -> false
| Cons(a,b,l) -> r a b or connected (fun x y -> r y x) l;;
val connected : ('a -> 'a -> bool) -> ('a, 'a) bijective_map -> bool =
Additional information
Untested with 3.12.0
The text was updated successfully, but these errors were encountered:
There is a misunderstanding here.
The problem is not with the type definition, which does not have to be
regular for datatypes (only type abbreviations are restricted).
The problem is just that your expected type requires polymorphic
recursion, which is known to be undecidable.
Moreover your type annotation is misleading, since in ocaml type variables
appearing in annotations may be freely instantiated by the typechecker.
Since 3.12, polymorphic recursion is allowed, using a new form of type
annotation, which makes polymorphism requirements explicit.
The following code will give you the expected type.
let rec connected : 'a 'b. ('a -> 'b -> bool) -> ('a, 'b) bijective_map -> bool
fun r -> function
| Nil -> false
| Cons(a,b,l) -> r a b or connected (fun x y -> r y x) l;;
Original bug ID: 5242
Reporter: SpiceGuid
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2013-08-31T10:43:54Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 3.11.0
Fixed in version: 3.12.0
Category: ~DO NOT USE (was: OCaml general)
Bug description
It seems to me the compiler assumes a recursive type to be regular even when told otherwise. The consequence is restricted generality, even when full generality is explicited.
type ('a, 'b) bijective_map =
| Nil
| Cons of 'a * 'b * ('b, 'a) bijective_map
let rec connected : ('a -> 'b -> bool) -> ('a, 'b) bijective_map -> bool =
fun r -> function
| Nil -> false
| Cons(a,b,l) -> r a b or connected (fun x y -> r y x) l;;
val connected : ('a -> 'a -> bool) -> ('a, 'a) bijective_map -> bool =
Additional information
Untested with 3.12.0
The text was updated successfully, but these errors were encountered: