Add support for ad-hoc variables in refinement types

[bvssvni]

For example:

fn add(a: any, b: any) -> any { ... }
    all T { (T f64, T f64) -> T f64 }

This is needed since addition on ad-hoc types is only valid for the same ad-hoc type.

A "none ad-hoc type" is a type f64 which ad-hoc type is T f64.

The all quantifier uses the semantics that "none ad-hoc type" is quantified over. This way, one only needs to write a single rule for all ad-hoc types plus the default case. The normal ad-hoc rule is not involved, since one can simply leave out the case e.g. (f64, f64) -> f64 and use all T { (T f64, T f64) -> T f64 } instead.

The "none ad-hoc type" of the previous arguments is lifted to T. This means that for binary operators, you can leave out ad-hoc type of the left argument and still pass the type check.

fn km(a: f64) -> km f64 {return clone(a)}

fn main() {
    println(2 + km(4)) // Works fine.
    println(km(4) + 2) // ERROR
}