Bogus error in beta and nightly: recursive type has infinite size

[jorendorff]

trait Front {
    type Back;
}

impl<T> Front for Vec<T> {
    type Back = Vec<T>;
}

struct PtrBack<T: Front>(*mut T::Back);

struct M(PtrBack<Vec<M>>);

fn main() {
    println!("{}", std::mem::size_of::<M>());
}

This program prints 8 in Stable (1.5.0), but in Beta and Nightly compilation fails with:

<anon>:11:1: 11:27 error: recursive type `M` has infinite size [E0072]
<anon>:11 struct M(PtrBack<Vec<M>>);
          ^~~~~~~~~~~~~~~~~~~~~~~~~~
<anon>:11:1: 11:27 help: see the detailed explanation for E0072
<anon>:11:1: 11:27 help: insert indirection (e.g., a `Box`, `Rc`, or `&`) at some point to make `M` representable
<anon>:11:1: 11:27 note: type `M` is embedded within `PtrBack<collections::vec::Vec<M>>`...
<anon>:11:1: 11:27 note: ...which in turn is embedded within `PtrBack<collections::vec::Vec<M>>`...
<anon>:11:1: 11:27 note: ...which in turn is embedded within `M`, completing the cycle.

From 8 bytes to infinity would seem to be a serious memory usage regression.

[jorendorff]

Same error if I change the pointer to a Box.

[jonas-schievink]

cc @nikomatsakis since I think he touched that code last

[arielb1]

Mini (no Vec needed - Vec is quite internally complex for some reason):

trait Front { type Back; }
impl<T> Front for T { type Back = T; }
struct PtrBack<T: Front>(*mut T::Back);
struct M(PtrBack<M>);

fn main() {
    println!("{}", std::mem::size_of::<M>());
}

[arielb1]

This is fallout from inductiveness

In the OC, the problem is that:

*) M: Sized if (sized)
*) PtrBack<M>: Sized if (sized)
*) *mut <M as Front>::Back: Sized if (sized)
*) M: Front if (impl)
*) M: Sized 

This could potentially be fixed by lazy normalization.

A harder case is:

trait Front { type Back; }
impl<T> Front for T { type Back = *mut T; /* note *mut is here */ }
struct PtrBack<T: Front>(T::Back);
struct M(PtrBack<M>);

fn main() {
    println!("{}", std::mem::size_of::<M>());
}

The cycle is similar:

*) M: Sized if (sized)
*) PtrBack<M>: Sized if (sized)
*) <M as Front>::Back: Sized if (sized)
*) M: Front if (impl)
*) M: Sized 

However, not even lazy normalization can save us here.

I admit the infinite type detection here is just plain wrong.

[Aatch]

@arielb1 those sequences are kinda hard to understand. However, I'm not sure why Sized is that relevant here. Unless the "infinite sized type" error is just a red herring and it's mis-reporting the recursive dependency for Sized vs. non-Sized?

[nikomatsakis]

@Aatch the message is basically a special-cased variant targeting the case where computing whether T: Sized is implemented requires that we recursively compute T: Sized. That usually (but not always) means an infinitely sized type, hence the message.

This is pretty related to how we can formalize auto traits. I'd been debating about a formalization that basically inserted one (automatically generated) impl for each auto trait, but those impls worked the same way as all other impls (this is not how it works today, but how it works today is unsound). However, I realized that this could fail, and my example was exactly the one that @jorendorff gives here -- one where the recursion arises through a projection. In the Obligation Forest PR, I considered whether to make Sized co-inductive, but @aturon and I decided we could avoid it. This may not have been correct.

So it may be that the correct fix is to have auto traits have a more complex, co-inductive proving semantics and -- since Sized is entirely builtin -- also give it those same semantics.

[Aatch]

@nikomatsakis so to be clear, the error message is wrong here, the problem is that we have "T meets Sized if T meets Sized" being reported as "T has infinite size". Makes sense given that in the absence of projection the only way that recursion could happen is if T contained T without indirection. Just want to make sure there's a version of this problem written in language understandable to those not super-familiar with the compiler's type-system internals.

[nikomatsakis]

@Aatch I agree the message is wrong, I didn't consider this case when phrasing it -- but I think ideally we wouldn't be reporting an error here at all. I guess the question is if there is a way to achieve that.

[arielb1]

auto trait = OIBIT right?

I'd been debating about a formalization that basically inserted one (automatically generated) impl for each auto trait

What's the difference between that and what we have today? That auto traits are coinductive?

If we forbid coinductive traits from having supertraits and associated types/constants we should be fine, as they can only be inputs of trait selection and not outputs.

[nikomatsakis]

triage: P-high