confilct with the conclusion: &mut T is invariant On T

[zylthinking]

the code below can be compiled, but it should be rejected because of &mut T is invariant On T;
Is there anything I misunderstand?

impl Animal for Cat1 {
    fn snuggle(&self) {
    }

    fn eat(&mut self) {
        println!("cat {}", self.data);
    }
}

impl Cat for Cat1 {
    fn meow(&self) {}
}

fn love(pet: &mut Animal) {
}

fn change() {
    let mut z: Cat1 = Cat1 {
        data: 8
    };
    love(&mut z);
}

[JOE1994]

I see your point ! Below is a minimal buildable code expanded from your example (link to playground). Code builds sucessfully with rustc stable 1.41.0.

trait Animal {
    fn snuggle(&self);
    fn eat(&self);
}

struct Cat1 { data: i32 }
impl Animal for Cat1 {
    fn snuggle(&self) {}
    fn eat(&self) { println!("cat {}", self.data); }
}

trait Cat: Animal { fn meow(&self); }
impl Cat for Cat1 { fn meow(&self) {} }

fn love(pet: &mut Animal) { pet.snuggle(); }

fn change() {
    let mut z: Cat1 = Cat1 { data: 8 };
    // Cat1 <: Cat
    // Cat <: Animal
    
    // Since `&mut` has invariance, 
    // `&mut Cat` and `&mut Animal` has no subtype relations
    
    love(&mut z); // Yet works!
}

From the explanation of the subtyping and variance chapter, it seems that the compiler should refuse to compile the above program, but yet it works.

[Gankra]

traits do not engage in subtyping, only lifetimes are used for subtyping. You are demonstrating coercions.

Cat/Dog/Animal is used as an abstraction to provide a simple inheritance relationship for the reader to understand the basic issues before delving into the concrete case of lifetimes.

[JOE1994]

traits do not engage in subtyping, only lifetimes are used for subtyping. You are demonstrating coercions.

If traits don't engage in subtyping, having the highlighted column in the below chart (from the chapter Subtyping and Variance) seems totally pointless to me.. (please correct me if I'm wrong)
Besides traits, I can't think of other types that allow reasoning of subtyping for the T column of the table.

[Gankra]

because T may be something that contains a lifetime like &'b X

&'a mut &'b X is invariant over 'b because &mut T is invariant over T