Commit Graph

37 Commits

Author SHA1 Message Date
bors
9ab0749ce3 Auto merge of #112875 - compiler-errors:negative-coherence-rework, r=lcnr
Rework negative coherence to properly consider impls that only partly overlap

This PR implements a modified negative coherence that handles impls that only have partial overlap.

It does this by:
1. taking both impl trait refs, instantiating them with infer vars
2. equating both trait refs
3. taking the equated trait ref (which represents the two impls' intersection), and resolving any vars
4. plugging all remaining infer vars with placeholder types

these placeholder-plugged trait refs can then be used normally with the new trait solver, since we no longer have to worry about the issue with infer vars in param-envs.

We use the **new trait solver** to reason correctly about unnormalized trait refs (due to deferred projection equality), since this avoid having to normalize anything under param-envs with infer vars in them.

This PR then additionally:
* removes the `FnPtr` knowable hack by implementing proper negative `FnPtr` trait bounds for rigid types.

---

An example:

Consider these two partially overlapping impls:

```
impl<T, U> PartialEq<&U> for &T where T: PartialEq<U> {}
impl<F> PartialEq<F> for F where F: FnPtr {}
```

Under the old algorithm, we would take one of these impls and replace it with infer vars, then try unifying it with the other impl under identity substitutions. This is not possible in either direction, since it either sets `T = U`, or tries to equate `F = &?0`.

Under the new algorithm, we try to unify `?0: PartialEq<?0>` with `&?1: PartialEq<&?2>`. This gives us `?0 = &?1 = &?2` and thus `?1 = ?2`. The intersection of these two trait refs therefore looks like: `&?1: PartialEq<&?1>`. After plugging this with placeholders, we get a trait ref that looks like `&!0: PartialEq<&!0>`, with the first impl having substs `?T = ?U = !0` and the second having substs `?F = &!0`[^1].

Then we can take the param-env from the first impl, and try to prove the negated where clause of the second.

We know that `&!0: !FnPtr` never holds, since it's a rigid type that is also not a fn ptr, we successfully detect that these impls may never overlap.

[^1]: For the purposes of this example, I just ignored lifetimes, since it doesn't really matter.
2023-10-26 10:57:21 +00:00
Oli Scherer
beaf46f7e5 Work around the fact that check_mod_type_wf may spuriously return ErrorGuaranteed, even if that error is only emitted by check_modwitem_types 2023-10-25 12:04:54 +00:00
Michael Goulet
0626f2e7d0 nits 2023-10-23 23:35:27 +00:00
Michael Goulet
e1edefc137 coherence doesn't like region constraints 2023-10-23 23:35:27 +00:00
Michael Goulet
1d99ddbfe8 Consider regions 2023-10-23 23:35:27 +00:00
Michael Goulet
8597bf1df7 Make things work by using the new solver 2023-10-23 23:35:27 +00:00
Oli Scherer
af93c20c06 Rename lots of files that had generator in their name 2023-10-20 21:14:02 +00:00
Oli Scherer
e96ce20b34 s/generator/coroutine/ 2023-10-20 21:14:01 +00:00
Oli Scherer
60956837cf s/Generator/Coroutine/ 2023-10-20 21:10:38 +00:00
Michael Goulet
973d589582 Bump COINDUCTIVE_OVERLAP_IN_COHERENCE 2023-10-18 18:54:11 +00:00
Michael Goulet
592163fb71 Extend impl's def_span to include where clauses 2023-10-09 11:47:02 +00:00
lcnr
8eade3aa71 update tests 2023-09-21 08:17:58 +02:00
Michael Goulet
30e6cea0ae Point out if a local trait has no implementations 2023-09-10 21:20:36 +00:00
Michael Goulet
4647aea7aa Don't record spans for predicates in coherence 2023-08-30 18:24:18 +00:00
Michael Goulet
0e20155662 more nits 2023-08-15 03:44:21 +00:00
Michael Goulet
d2a14df70e nits
Co-authored-by: lcnr <rust@lcnr.de>
2023-08-15 03:40:19 +00:00
Michael Goulet
56f5704ff8 Implement lint against coinductive impl overlap 2023-08-15 03:40:19 +00:00
nxya
a54a66830d moved note as unspanned note, moved note to the bottom of the msg 2023-07-18 21:53:34 -04:00
nxya
e6e8892051 added links as a note 2023-07-18 09:27:35 -04:00
nxya
f92a9f6808 add links to query documentation for E0391 2023-07-18 09:27:26 -04:00
nxya
bef91ee687 added links as a note 2023-07-18 09:20:25 -04:00
nxya
c429a72db9 add links to query documentation for E0391 2023-07-18 09:20:25 -04:00
Michael Goulet
8f178d1b0c Don't call predicate_must_hold during fulfillment in intercrate 2023-07-16 01:56:16 +00:00
lcnr
aa13288e22 remove unused revision 2023-05-30 12:40:35 +02:00
whtahy
21b9f5c3bb add known-bug test for unsound issue 74629 2023-04-26 22:34:39 -04:00
whtahy
232d685e61 add known-bug test for unsound issue 57893 2023-04-22 00:47:07 -04:00
Esteban Küber
9fadcc143a Special-case item attributes in the suggestion output 2023-04-12 22:50:10 +00:00
Esteban Küber
5b40aa5eb4 Tweak output for 'add line' suggestion 2023-04-12 22:50:10 +00:00
Matthias Krüger
031b528052
Rollup merge of #108884 - compiler-errors:tweak-illegal-copy-impl-message, r=WaffleLapkin
Tweak illegal `Copy` impl message

The phrase "may not" can both mean "is not able to" and "possibly does not". Disambiguate this by just using "cannot".
``@Lokathor`` expressed being annoyed by this [here](https://twitter.com/Lokathor/status/1633200313544089602?s=20).

Also drive-by fix for this extremely noisy message: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=6a37275bc810f7846bfe191845b7d11d.

r? diagnostics
2023-03-08 21:24:52 +01:00
Michael Goulet
8a99ffc344 Suppress copy impl error when post-normalized type references errors 2023-03-08 00:12:33 +00:00
Michael Goulet
a439c0293c may not => cannot 2023-03-08 00:00:18 +00:00
Mu42
23ba4ceb9e Bless the remaining ui tests 2023-03-06 21:05:35 +08:00
Michael Goulet
e20f6ff1dc Tighter spans for bad inherent impl types 2023-02-13 18:41:18 +00:00
David Tolnay
9e1c600f74
Disallow impl autotrait for trait object 2023-02-03 08:33:40 -08:00
Oli Scherer
42f1f54a5e Don't treat closures from other crates as local 2023-01-19 11:29:40 +00:00
Michael Goulet
2aabb0fd5d Point at impl self type for impl wf obligations 2023-01-12 20:44:47 +00:00
Albert Larsan
cf2dff2b1e
Move /src/test to /tests 2023-01-11 09:32:08 +00:00