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: 6007 Reporter:@fpottier Assigned to:@garrigue Status: closed (set by @xavierleroy on 2015-12-11T18:18:50Z) Resolution: not a bug Priority: normal Severity: minor Platform: Linux, MacOS Version: 4.00.1 Category: typing Child of:#5343 Monitored by:@gasche
Bug description
This problem concerns ocamlc -rectypes. If I define a cyclic type
abbreviation foo as follows, it is accepted:
type 'a foo = 'a foo list (* accepted *)
However, I wish to abstract away the type list, so I place this
definition in the body of a functor, which expects list as an
argument. Then, the definition is rejected by ocaml 4.00.1:
module M (X : sig type 'a list end) = struct
type 'a foo = 'a foo X.list
(* accepted by ocaml 3.11.2; rejected by ocaml 4.00.1 *)
end
Is this a bug or is there a good reason to reject this definition?
Thanks!
Francois.
There is indeed a good reason: we don't know whether X.list is contractive,
and if it were not, foo would not be well-founded (leading to a potential
unsoundness).
See #5343 for details.
Hi Jacques,
I have looked at #5343. I understand. Indeed, unless we allow declaring
that an unknown type constructor is contractive, I do not see how
to allow this code. Too bad... Thanks for the quick reply.
Original bug ID: 6007
Reporter: @fpottier
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:50Z)
Resolution: not a bug
Priority: normal
Severity: minor
Platform: Linux, MacOS
Version: 4.00.1
Category: typing
Child of: #5343
Monitored by: @gasche
Bug description
This problem concerns ocamlc -rectypes. If I define a cyclic type
abbreviation foo as follows, it is accepted:
type 'a foo = 'a foo list (* accepted *)
However, I wish to abstract away the type list, so I place this
definition in the body of a functor, which expects list as an
argument. Then, the definition is rejected by ocaml 4.00.1:
module M (X : sig type 'a list end) = struct
type 'a foo = 'a foo X.list
(* accepted by ocaml 3.11.2; rejected by ocaml 4.00.1 *)
end
Is this a bug or is there a good reason to reject this definition?
Thanks!
Francois.
File attachments
The text was updated successfully, but these errors were encountered: