Update Aeneas to remove the marker traits

[sonmarcho]

Today, we have to call Charon with the option --hide-marker-traits, which is quite annoying and error prone.

[R1kM]

Without this option, extracting code such as the following fails:

pub enum CList<T> {
    CCons(T, Box<CList<T>>),
    CNil,
}

This is due to the translation of trait instance ids:

aeneas/compiler/SymbolicToPure.ml

Line 462 in 6377992

craise_opt_span __FILE__ __LINE__ span "Unreachable"

The solution would be to add a prepass to remove these, similarly to what is done in Charon.

[Nadrieril]

I'd prefer if aeneas called charon by itself

[sonmarcho]

Yes that makes sense. I opened an issue: #349