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: 1757 Reporter: administrator Status: closed Resolution: fixed Priority: normal Severity: minor Category: ~DO NOT USE (was: OCaml general)
Bug description
Full_Name: Jacek Chrzaszcz
Version: 3.06
OS: Linux
Submission from: dhcp17.labri.fr (147.210.9.112)
Hello,
By doing some experiments and looking at the type-checker's code I discovered
that
the subtyping of functor types is too restrictive!
In the papers of X.Leroy the rule is
E |- M_1' <: M_1 E,X:M_1' |- M_2 <: M_2'
E |- functor(X:M_1)M_2 <: functor(X:M_1')M_2'
while in the implementation, its right premise is
E,X:M_1 |- M_2 <: M_2'
^
no ' here
Consequently correct functor subtyping might be rejected. For example:
module type SUBTYPE = functor(X:sig type t end) -> sig type t=X.t end
module type SUPERTYPE = functor(X:sig type t type u=t end) -> sig type t=X.u
end
module S : SUBTYPE =
functor(X:sig type t end) -> struct type t=X.t end
module Tester(Y:SUPERTYPE) = struct end
module Test=Tester(S)
Is it a forgotten subtlety or is it on purpose, motivated by some subtle
compilation issues that I do not see?
Best regards to the Caml Team
Jacek
The text was updated successfully, but these errors were encountered:
By doing some experiments and looking at the type-checker's code I
discovered that the subtyping of functor types is too restrictive!
[...]
Is it a forgotten subtlety or is it on purpose, motivated by some subtle
compilation issues that I do not see?
You are correct. It's an oversight: there are no compilation issues
or otherwise that require the more restrictive rule currently
implemented. Actually, the bug has been there since the very
beginning (1995); it's a good thing that it only causes the
type-checker to err on the safe side.
I'll put the "real" functor subtyping rule for the next release.
Original bug ID: 1757
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)
Bug description
Full_Name: Jacek Chrzaszcz
Version: 3.06
OS: Linux
Submission from: dhcp17.labri.fr (147.210.9.112)
Hello,
By doing some experiments and looking at the type-checker's code I discovered
that
the subtyping of functor types is too restrictive!
In the papers of X.Leroy the rule is
E |- M_1' <: M_1 E,X:M_1' |- M_2 <: M_2'
E |- functor(X:M_1)M_2 <: functor(X:M_1')M_2'
while in the implementation, its right premise is
E,X:M_1 |- M_2 <: M_2'
^
no ' here
Consequently correct functor subtyping might be rejected. For example:
module type SUBTYPE = functor(X:sig type t end) -> sig type t=X.t end
module type SUPERTYPE = functor(X:sig type t type u=t end) -> sig type t=X.u
end
module S : SUBTYPE =
functor(X:sig type t end) -> struct type t=X.t end
module Tester(Y:SUPERTYPE) = struct end
module Test=Tester(S)
Is it a forgotten subtlety or is it on purpose, motivated by some subtle
compilation issues that I do not see?
Best regards to the Caml Team
Jacek
The text was updated successfully, but these errors were encountered: