Improve some error messages

[sonmarcho]

This PR improves the error messages generated when detecting mixed groups of mutually recursive declarations: we now list the involved declarations, and if some of them are external we list the spans which (transitively) refer to those declarations.

For instance, we now generate this kind of error messages when detecting mixed groups of declarations :

[Error] Detected groups of mixed mutually recursive definitions (such as a type mutually recursive with a function, or a function mutually recursive with a trait implementation):

Group:
# Group:
- trait decl(Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 39:0-39:18): core::iter::traits::iterator::Iterator
- trait decl(Source: '/rustc/library/core/src/iter/traits/collect.rs', lines 318:0-318:22): core::iter::traits::collect::IntoIterator
- type decl(Source: '/rustc/library/core/src/iter/adapters/intersperse.rs', lines 10:0-10:35): core::iter::adapters::intersperse::Intersperse
- type decl(Source: '/rustc/library/core/src/iter/adapters/intersperse.rs', lines 91:0-91:32): core::iter::adapters::intersperse::IntersperseWith
- type decl(Source: '/rustc/library/core/src/iter/adapters/peekable.rs', lines 17:0-17:32): core::iter::adapters::peekable::Peekable
- type decl(Source: '/rustc/library/core/src/iter/adapters/flatten.rs', lines 17:0-17:41): core::iter::adapters::flatten::FlatMap
- type decl(Source: '/rustc/library/core/src/iter/adapters/flatten.rs', lines 254:0-254:51): core::iter::adapters::flatten::Flatten
- type decl(Source: '/rustc/library/core/src/iter/adapters/map_windows.rs', lines 11:0-11:53): core::iter::adapters::map_windows::MapWindows
- trait decl(Source: '/rustc/library/core/src/iter/traits/collect.rs', lines 134:0-134:32): core::iter::traits::collect::FromIterator
- trait decl(Source: '/rustc/library/core/src/iter/traits/collect.rs', lines 431:0-431:19): core::iter::traits::collect::Extend
- trait decl(Source: '/rustc/library/core/src/iter/traits/double_ended.rs', lines 41:0-41:39): core::iter::traits::double_ended::DoubleEndedIterator
- trait decl(Source: '/rustc/library/core/src/iter/traits/exact_size.rs', lines 86:0-86:37): core::iter::traits::exact_size::ExactSizeIterator
- type decl(Source: '/rustc/library/core/src/iter/adapters/array_chunks.rs', lines 19:0-19:51): core::iter::adapters::array_chunks::ArrayChunks
- trait decl(Source: '/rustc/library/core/src/iter/traits/accum.rs', lines 17:0-17:30): core::iter::traits::accum::Sum
- trait decl(Source: '/rustc/library/core/src/iter/traits/accum.rs', lines 38:0-38:34): core::iter::traits::accum::Product
- trait decl(Source: '/rustc/library/core/src/iter/adapters/zip.rs', lines 593:0-593:51): core::iter::adapters::zip::TrustedRandomAccessNoCoerce

The declarations in this group are (transitively) used at the following location(s):
Source: '/rustc/library/core/src/macros/mod.rs', lines 51:84-51:112
Source: 'src/misc.rs', lines 7:0-12:1
Source: 'src/misc.rs', lines 8:14-8:21
Source: 'src/misc.rs', lines 16:12-16:36
...

[sonmarcho]

This PR depends on AeneasVerif/charon#479