Implicit Trait Constraints

[karthikbhargavan]

trafficstars

When adding a constraint of the form T: Copy, rustc always adds a second constraint T:Copy+Clone. Consequently, the generated typeclass in F* has both constraints (to be solved). However, the corresponding instance (trait implementation) in F* only solved the first constraint, leading to a lax-checking error.

[W95Psp]

Requires some investigation, marking it as small for now.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[W95Psp]

Seems like I can't reproduce any longer:

trait T: Clone {
    type U: Clone;    
}
impl T for () {
    type U = ();  
}

fn f<T: Clone>() {}

Open this code snippet in the playground

Let's keep this issue closed then!