Creusot panic on model where ShallowModelTy is a tuple with a Seq.

[sarsko]

The following code

use creusot_contracts::*;

pub struct Formula {
    vec: Vec<usize>,
    b: bool,
}

impl ShallowModel for Formula {
    type ShallowModelTy = (Seq<usize>, bool);

    #[logic]
    #[open]
    fn shallow_model(self) -> Self::ShallowModelTy {
        (self.vec.shallow_model(), self.b)
    }
}

impl Formula {
    #[ensures(self@ == self@)] // Just here for the model access
    fn love_and_hope(&self) {}
}

Gives the following panic:

thread 'rustc' panicked at creusot/src/backend/clone_map/elaborator.rs:272:13:
Could not find Type(creusot_contracts::Seq<usize>) -> Type(creusot_contracts::Seq<usize>)
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: creusot::backend::clone_map::elaborator::SymNamer::get
   3: <creusot::backend::clone_map::elaborator::SymNamer as creusot::backend::clone_map::Namer>::ty
   4: creusot::backend::ty::translate_ty_inner
   5: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
   6: creusot::backend::ty::translate_ty_inner
   7: creusot::backend::signature::sig_to_why3
   8: creusot::backend::clone_map::elaborator::SymbolElaborator::build_clone
   9: creusot::backend::clone_map::CloneMap::to_clones
  10: creusot::backend::interface::interface_for
  11: creusot::backend::Why3Generator::translate
  12: creusot::translation::after_analysis
  13: rustc_middle::ty::context::GlobalCtxt::enter
  14: <creusot::callbacks::ToWhy as rustc_driver_impl::Callbacks>::after_expansion
  15: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#0}::{closure#0}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  16: rustc_span::set_source_map::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#0}>::{closure#0}::{closure#0}>
  17: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::util::run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#0}>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>
  18: rustc_span::create_session_globals_then::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::util::run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#0}>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>::{closure#0}>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/creusot-rs/creusot/issues/new

query stack during panic:
end of query stack
warning: `vt2024` (lib) generated 1 warning
error: could not compile `vt2024` (lib); 1 warning emitted

Some notes:

1. Model type has to be a tuple as far as I can tell.
2. One of the model fields has to be a Seq (may be it fails with other composite types as well, didn't think of one readily)
3. Opacity does not seem to matter
4. The issue seems to arise from calling @ in a spec.

[sarsko]

Can be worked around by creating a struct instead of a tuple, as in:

pub struct FormulaModel {
    pub clauses: Seq<usize>,
    pub num_vars: Int
}

impl ShallowModel for Formula {
    type ShallowModelTy = FormulaModel;

    #[logic]
    #[open]
    fn shallow_model(self) -> Self::ShallowModelTy {
        FormulaModel { clauses: self.clauses.shallow_model(), num_vars: self.num_vars.shallow_model() }
    }
}

pub struct Formula {
    clauses: Vec<usize>,
    num_vars: usize,
}