Comments (14)
This would make a good first bug. The idea would be to modify src/solve/test.rs
and add a new test looking something like the existing #[test]
entries. This test would include two overlapping impls (e.g., impl<T: Foo> Marker for T
and impl<T: Bar> Marker for T
) and check that we can prove X: Marker
for types that implement both Foo and Bar.
Bonus points would be to add some cases to show that inference holds back from decided types if there are more than one applicable impl. For example:
impl<T: Foo> Marker<u32> for T
and
impl<T: Bar> Marker<i32> for T
would result in ambiguity on exists<?A> X: Marker<?A>
if X: Foo + Bar
. But if would succeed with either X: Marker<u32>
or X: Marker<i32>
.
from chalk.
@nikomatsakis I started working on this. First, I started with a simple_overlap
test in exactly the way you describe. Easy peasy.
I got more confident and created a maybe_overlap
test much like an example from @aturon's recent Chalk blog post. The test was something like this:
program {
struct Unit { }
trait MyTrait { }
trait Error { }
impl<T: Error> MyTrait for T { }
impl MyTrait for Unit { }
}
goal {
Unit: !Error
} yields {
"Solution: { successful: Maybe"
}
which failed because chalk
apparently doesn't implement negative reasoning yet (??).
Then I "accidentally" started implementing support for WhereClause::NotImplemented
, but got a bit overwhelmed 😁.
Do you have any pointers here?
from chalk.
@mrhota, you're right that negative reasoning is not well-supported right now, and the current forms for negation are going to be removed, in favor of a more general purpose system of negation.
However, you should be able to add this test without using negation. @nikomatsakis's comment lays out one particular strategy for doing so. Did that comment make sense to you?
from chalk.
@aturon after stepping away for a few days, I think I understand the second part of that comment better. I admit I'm rather out of my depth, but the code is pretty straightforward, so that helps!
from chalk.
@nikomatsakis did I understand you right? Here is a test I came up with:
trait Foo {}
trait Bar {}
trait Marker {}
impl<T> Marker for T where T: Foo {}
impl<T> Marker for T where T: Bar {}
struct i32 {}
impl Foo for i32 {}
impl Bar for i32 {}
// Goals
// forall<T> { if(T: Foo, T: Bar) { T: Marker }}
// i32: Marker
Unfortunately, when I load the program into chalki, it says error: overlapping impls of trait "Marker"
from chalk.
@mikeyhew No, those impls actually overlap, because you can use two different impls to prove i32: Marker
. The type parameter on the example in @nikomatsakis's post was necessary, because it meant that the impls were not actually overlapping.
from chalk.
@withoutboats I'm confused. I thought the impls were supposed to overlap? Niko said to "check that we can prove X: Marker
for types that implement both Foo and Bar". So I made i32 implement Foo and Bar and checked that i32: Marker
. Which type parameter are you referring to, X
?
from chalk.
@withoutboats @nikomatsakis Is this what you meant?
trait Foo {}
trait Bar {}
trait Marker {}
impl<T> Marker for T where T: Foo {}
impl<T> Marker for T where T: Bar {}
// goal: forall<X> { if(X: Foo, X: Bar) { X: Marker }}
// result: Unique; substitution [], lifetime constraints []
from chalk.
Niko spoke unprecisely when he said the two impls overlap. What he means is that if the parameter is not known, they both could apply.
It was like this:
trait Foo {}
trait Bar {}
trait Marker<T> {}
impl<T> Marker<u32> for T where T: Foo {}
impl<T> Marker<i32> for T where T: Bar {}
If T: Foo + Bar
, and you don't know what the ?
in Marker<?>
is, its uncertain whether ?
is i32
or u32
(as opposed to incorrectly picking one at random).
These impls don't actually overlap, in the sense of the overlapping impl check, because the type parameter on Marker
is different in both cases.
from chalk.
No, those impls actually overlap, because you can use two different impls to prove i32: Marker. The type parameter on the example in @nikomatsakis's post was necessary, because it meant that the impls were not actually overlapping.
Well, actually, due to RFC 1268, marker traits (those with zero items) are allowed to overlap. So that may be a bug that @mikeyhew has uncovered, actually.
from chalk.
A little annoying for chalk since nearly all of our tests use marker traits.
from chalk.
A little annoying for chalk since nearly all of our tests use marker traits.
True. =) Maybe we should make marker traits more explicit with #[marker]
?
from chalk.
@withoutboats I agree with @nikomatsakis. One of the unresolved question on RFC 1268, anyway, is whether to use a #[marker_trait]
attribute, to avoid accidentally creating a marker trait and breaking backward compatibility when you add an associated item. In either case, it would probably make sense for rustc to tell chalk that a trait is a marker trait, rather than have chalk infer it.
from chalk.
I wrote up the steps to add #[marker]
in #62. I'm going to close this now that we landed @mikeyhew's PR.
from chalk.
Related Issues (20)
- CI Publish job using Mac runner HOT 2
- When Rust 1.55 hits stable, replace `ControlFlow` with std version
- Recursive solver reports ambiguity HOT 7
- Idea: rework how SLG solver uses the environment
- Auto traits are not handled for generic closures HOT 8
- Consider removing unused field
- Clean up coherence chapter in the Chalk book HOT 1
- Ambiguity through unrelated env clauses because of implied bounds HOT 1
- reconcile SLG/recursive solver's attempts to merge multiple results
- book: hard to read mermaid diagram in dark themes
- Lowered command panics with auto trait HOT 1
- Recursive solver hangs on cyclic traits HOT 3
- mdbook-mermaid needs updating
- Unable to deduce projection types of dyn types from supertrait bounds
- ICE: negative subgoal had delayed_subgoals HOT 2
- any progress and roadmap? HOT 1
- Automatic releases have been failing for a couple of months
- Branch protection prevents automatic releases from updating the version number on the `master` branch
- Recursive Solver fails to solve recursive associated type with GAT
- Fails to solve some existential clause HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from chalk.