Engine: F*: open modules providing trait impls #676
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The PR fixes 667.
Consider the following Rust module:
The point here is that the type
MyType
, the traitMyTrait
, the impl ofMyTrait
forMyType
and the call tomy_method
are in four different modules.Thus, in the module
use_type
, the moduleimpl_type
is never explicitly mentioned: in F* this results in the moduleimpl_type
to not be loaded at all by F*, which in turn, implies that the instance (the impl) is not in scope. Thus, the F* mechanism for resolving the instance of the typeclassMyTrait
fails.With this PR, extracting this crate, you will get the following for module
use_type
: