Not useful error message: "call expression requires function"

[sarsko]

Not super important, but might as well report(especially since it seems to be solvable in the parser).

The following

extern crate creusot_contracts;
use creusot_contracts::*;
use creusot_contracts::std::*;

#[predicate]
pub fn ex(v: Vec<usize>) -> bool {
    pearlite! {
        forall<i: Int> 0 <= i && i < (@v).len()
        true === true
    }
}

gives(due to lacking &&/==>)

error: unexpected token
 --> /home/sarek/master/sat-mirror/src/ex.rs:9:13
  |
9 |             true === true
  |             ^^^^

error: aborting due to previous error; 1 warning emitted

Which is a fine enough error message(could be better, but not terrible)

Whereas:

extern crate creusot_contracts;
use creusot_contracts::*;
use creusot_contracts::std::*;

#[predicate]
pub fn ex(v: Vec<usize>) -> bool {
    pearlite! {
        forall<i: Int> 0 <= i && i < (@v).len()
            (@v) === (@v)
    }
}

gives(again due to lacking &&/==>)

error[E0618]: expected function, found `creusot_contracts::Int`
  --> /home/sarek/master/sat-mirror/src/ex.rs:7:5
   |
7  | /     pearlite! {
8  | |         forall<i: Int> 0 <= i && i < (@v).len()
9  | |             (@v) === (@v)
10 | |     }
   | |_____^ call expression requires function
   |
   = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0308]: mismatched types
  --> /home/sarek/master/sat-mirror/src/ex.rs:7:5
   |
7  | /     pearlite! {
8  | |         forall<i: Int> 0 <= i && i < (@v).len()
9  | |             (@v) === (@v)
10 | |     }
   | |_____^ expected `bool`, found struct `creusot_contracts::Seq`
   |
   = note: expected type `bool`
            found struct `creusot_contracts::Seq<usize>`
   = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0283]: type annotations needed
  --> /home/sarek/master/sat-mirror/src/ex.rs:7:5
   |
7  | /     pearlite! {
8  | |         forall<i: Int> 0 <= i && i < (@v).len()
9  | |             (@v) === (@v)
10 | |     }
   | |_____^ cannot infer type for type `{integer}`
   |
   = note: multiple `impl`s satisfying `creusot_contracts::Int: std::convert::From<{integer}>` found in the `creusot_contracts` crate:
           - impl std::convert::From<i32> for creusot_contracts::Int;
           - impl std::convert::From<isize> for creusot_contracts::Int;
           - impl std::convert::From<u32> for creusot_contracts::Int;
           - impl std::convert::From<u8> for creusot_contracts::Int;
           and 1 more
   = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)

thread 'rustc' panicked at 'called `Result::unwrap()` on an `Err` value: CrErr', creusot/src/callbacks.rs:38:14
note: run with `RUST_BACKTRACE=1` environment variable to display a 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/xldenis/creusot/issues/new

error: aborting due to 3 previous errors

Some errors have detailed explanations: E0283, E0308, E0618.
For more information about an error, try `rustc --explain E0283`.

Which is not very helpful + a panic.

[xldenis]

Brutal, I wonder why that second expression parses, it shouldn't just like the first..

[xldenis]

I just had an idea: we can use a lint to check this !