Removing redundant extern specs causes type checking failure in Why3

[jhjourdan]

See #562.

[xldenis]

A quick inspection appears to show that the issue is that associated types are improperly normalized for inherited specifications. This can be confirmed by removing https://github.com/xldenis/creusot/blob/master/creusot-contracts/src/std/slice.rs#L336-L356 and looking at the output of 03_std_iterators.

Which goes from:

module Core_Slice_Iter_Impl181_Next_Interface
  type t
  use prelude.Borrow
  use seq.Seq
  clone Core_Slice_Iter_Impl181_Item_Type as Item0 with type t = t
  use Core_Slice_Iter_Iter_Type as Core_Slice_Iter_Iter_Type
  clone CreusotContracts_Std1_Iter_IteratorSpec_Produces_Interface as Produces0 with type self = Core_Slice_Iter_Iter_Type.t_iter t,
  type Item0.item = Item0.item
  clone CreusotContracts_Std1_Iter_IteratorSpec_Completed_Interface as Completed0 with type self = Core_Slice_Iter_Iter_Type.t_iter t
  use Core_Option_Option_Type as Core_Option_Option_Type
  val next [@cfg:stackify] (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : Core_Option_Option_Type.t_option t
    ensures { match (result) with
      | Core_Option_Option_Type.C_None -> Completed0.completed self
      | Core_Option_Option_Type.C_Some v -> Produces0.produces ( * self) (Seq.singleton v) ( ^ self)
      end }
    
end

to:

module Core_Slice_Iter_Impl181_Next_Interface
  type t
  use prelude.Borrow
  use seq.Seq
  use Core_Option_Option_Type as Core_Option_Option_Type
  use Core_Slice_Iter_Iter_Type as Core_Slice_Iter_Iter_Type
  clone Core_Iter_Traits_Iterator_Iterator_Item_Type as Item0 with type self = Core_Slice_Iter_Iter_Type.t_iter t
  clone CreusotContracts_Std1_Iter_IteratorSpec_Produces_Interface as Produces0 with type self = Core_Slice_Iter_Iter_Type.t_iter t,
  type Item0.item = Item0.item
  clone CreusotContracts_Std1_Iter_IteratorSpec_Completed_Interface as Completed0 with type self = Core_Slice_Iter_Iter_Type.t_iter t
  val next [@cfg:stackify] (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : Core_Option_Option_Type.t_option t
    ensures { match (result) with
      | Core_Option_Option_Type.C_None -> Completed0.completed self
      | Core_Option_Option_Type.C_Some v -> Produces0.produces ( * self) (Seq.singleton v) ( ^ self)
      end }
    
end

The only thing which changes is the associated type.