impl<A: Copy> Copy for Tracked<A>

[tjhance]

No description provided.

[Chris-Hawblitzel]

I guess we could already do this indirectly anyway:

fn d<A: Copy>(Tracked(x): Tracked<A>) -> (Tracked<A>, Tracked<A>) {
    (Tracked(x), Tracked(x))
}

so there's no harm in also allowing it directly.

[Chris-Hawblitzel]

Could this be A: Clone, to be more flexible?

[tjhance]

We don't actually supported Tracked::clone at all right now. If we did support it, how do you think it should work? We either treat it like a 'copy' (in which we case we do need the A: Copy bound here, as I wrote) or we treat it like Tracked(a.borrow.clone()). Even defining Clone for a tracked object when it's not Copy is already a pretty unusual operation. My inclination is to continue not supporting Tracked::clone, in which case it doesn't really matter what this bound is.

[Chris-Hawblitzel]

I guess Clone::clone wouldn't work on the A value anyway, because it's an exec function taking an exec argument, not a proof function taking a tracked argument.

[tjhance]

If anyone is wondering about the status of this, I decided to wait until my other work on the Clone trait is done.