Oddities with Base kind

[ranjitjhala]

          This is still odd, but now I understand the problem. Turns out that implementing this is a bit more involved. 

In this test

fn make_eq_hash() -> impl Eq + Hash
    0
}

fn id<T as base>(x: T) -> T[x] {
    x
}


fn test00() {
    let z = mk_eq_hash();
    id(z);
}

At the point we call id we have λ. impl Eq + Hash as the generic argument, i.e., a lambda with no parameters. That's already wrong at many levels. Arguments of kind base should be a lambda with exactly one parameter. So there's a problem when we generate the instantiation here https://github.com/flux-rs/flux/blob/main/crates/flux-middle/src/global_env.rs#L341. I think we need to do this check before we instantiate the arguments or make the instantiation itself check it.

We can ponder this later though. The change is a bit orthogonal to the rest of the changes in the PR. I would revert the changes and remove the associated tests, so we can tackle it later.

Originally posted by @nilehmann in #542 (comment)

[nilehmann]

Fixed in #622