Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

requiring item bounds for coinduction may be breaking #80

Open
lcnr opened this issue Dec 20, 2023 · 2 comments
Open

requiring item bounds for coinduction may be breaking #80

lcnr opened this issue Dec 20, 2023 · 2 comments

Comments

@lcnr
Copy link
Contributor

lcnr commented Dec 20, 2023

our current plan to soundly support coinductive traits is to require proving the item bounds of a trait when using an implementation. Afaict this should break the following example:

trait WithSuper<T>: Copy {}

trait WithAliasBound {
    type Assoc: Copy;
}

// With our approach to coinduction, using this impl should require
// proving `<T as WithAliasBound>::Assoc: Copy`
impl<T: WithAliasBound> WithSuper<T> for <T as WithAliasBound>::Assoc {}

fn impls_with_super<T: WithSuper<U>, U>() {}

fn item_bounds_not_checked<T: WithAliasBound<Assoc = U>, U>() {
    impls_with_super::<U, T>();
    // This uses the impl and would fail to prove `U: Copy`.
}

related issues

@lcnr lcnr changed the title requiring item bounds for coinduction is breaking requiring item bounds for coinduction may be breaking Dec 20, 2023
@compiler-errors
Copy link
Member

would this be fixed if we auto-elaborated item bounds, i.e. elaborate U: Copy from T: WithAliasBound<Assoc = U>?

@lcnr
Copy link
Contributor Author

lcnr commented Dec 20, 2023

yes it would, had the same convo with @BoxyUwU rn 😆 doing so is non-trivial however.

Instead of T: WithAliasBound<Assoc = U> you can have T: WithIntoIteratorAliasBound<Assoc = Vec<U>>. So if you now add Vec<u32>: IntoIterator into the environment it probably shadows the actual impl, preventing you from normalizing <Vec<u32> as IntoIterator>::Item. We probably want param env Trait-candidates to prevent normalizing via impls due to #76/#12

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants