Handling integer/float variables

[flodiebold]

Integer literals of unspecified type like e.g. 1 get assigned an 'integer type' variable in Rust, which is for most uses like a normal type variable, but we know it can only be one of the integer types. The same goes for float literals. Chalk mostly doesn't care about this, but it can lead us to a non-ambiguous solution because in some cases, only one solution actually is an integer type. The most notable example (I think) happens when indexing into an array or slice:

let x: &[u32];
let i = 1;
x[i]

i gets inferred to usize here because that's the only integer type for which Index is implemented in this case, as far as I understand. Chalk currently can't do this.

There was already some discussion about this in a Zulip stream a while ago; I thought I'd open a ticket to keep track of the problem.

[jackh726]

So, I'm a little confused about this. Why would/does it matter that there can multiple "integer types" vs. usize, u32, etc.? i here should get inferred to being usize here since that's the only matching type for Index, right?

[flodiebold]

From Chalk's view, i is of completely unknown type at that point, and there are more implementations of Index than just for usize (e.g. for ranges as well). But we know these other implementations can't apply because none of them are for an integer type.

[flodiebold]

(An additional complication is that we in general don't want to enumerate a potentially completely open set of types for solutions, but in this case the actual set of possible types that the variable can take is very constrained from the outset.)

[flodiebold]

Actually, it might be possible to model this using a hidden enumerable Integer trait 🤔

[jackh726]

Yes, I was thinking about that as a solution (it was my first thought).

[nikomatsakis]

I used to favor an integer trait, but these days I'm thinking we will regret trying to be too clever, and we should just add more entries to VariableKind for "integer type variable" and "float type variable", and basically model how rustc handles this.

[nikomatsakis]

I feel like it's not that much complexity to add and somehow I think we are going to find that using a special trait is going to be more trouble than it's worth.

[flodiebold]

The trait solution wouldn't work in the recursive solver anyway, at least.

[AzureMarker]

I'm interested in working on this, it looks like the design is thought-out enough to start experimenting with the implementation?

I don't see it mentioned yet, but following rustc we would have an Int and UInt variable kind? As for the AST, it looks like we would represent integer/float variable kinds with special prefixes, in order to distinguish between the kinds? So similar to const N, we would have int N, uint N, and float N. I'm a little concerned if it's necessary, since it's a departure from normal Rust syntax, but I would imagine that since it's just for tests it doesn't matter, and additionally downstream libraries like RA would want to have integer/float variable kinds in their queries (they would know if the variable should be an integer/float, as in this issue's example).

[jackh726]

Indeed, I think if we just go with the rustc way of approaching this, it should be fairly straightforward to implement.

There wouldn't be a different Int and Uint. The idea is if you have

let x = 0;
x.foo();

and there is a foo on both usize and something else, we know that x is a usize. You can also imagine any other scenario where x is a different type of int/uint.

Floats are distinguished from ints because we actually know that from parsing. 0 vs 0.0. So we could have the same example above between usize and f32.

[AzureMarker]

So to transform that example into a test, it would look something like this?

test! {
    program {
        trait Foo {}
        struct Bar {}
        
        impl Foo for usize {}
        impl Foo for Bar {}
    }
    
    goal {
        exists<int N> {
            N: Foo
        }
    } yields {
        "Unique; substitution [?0 := usize]"
    }
}

[jackh726]

Yes, that looks right

[AzureMarker]

@rustbot claim

I've got a working implementation of integer kinded variables (:tada:), and after I extend it to floats I'll open a PR.