Constraint Integral ([n]a) should imply a = Bit

[brianhuffman]

Cryptol infers what I consider to be a too-general type for expressions involving shift/indexing operators:

Cryptol> :t \x -> 0b01 << [x]
(\x -> 0b01 << [x]) : {a} (Integral ([1]a)) => a -> [2]
Cryptol> :t \x -> 0b01 @ [x]
(\x -> 0b01 @ [x]) : {a} (Integral ([1]a)) => a -> Bit

I would expect that the constraint Integral ([n]a) should improve to the type equality a = Bool, and then be discharged.

[robdockins]

This requires closed world assumptions about the class instances, which is pretty different from how I usually think about class inference. Do we do inference of this sort elsewhere in Cryptol already?

[brianhuffman]

This seems similar to #265. Maybe there are reasons to infer such a general type, but it doesn't seem very user-friendly to me.

[brianhuffman]

I don't think this actually requires a closed-world assumption. We just need to have a single Integral class instance rule for the list type, which is basically instance (fin n, a ~ Bool) => Integral ([n]a). So this situation is actually simpler than we had for #265, because when we see Integral ([n]a), there is exactly one instance rule that applies. (In #265, we couldn't simplify Arith ([n]a) because we have two overlapping instance rules Arith a => Arith ([n]a) and (fin n, a ~ Bool) => Arith ([n]a).)

[robdockins]

Well, I guess that's true, you don't have any confluence, etc. issues if you phrase the instance that way.

However, I don't think we have a type equality constraint, even internally. It seems like it might be a pretty big change to add one.

[yav]

We have equality on numeric types, and it wouldn't be hard to add it to value types too. It's not there because (1) we didn't really need it in the past, and (2) it allows you to write odd type schemes like:

{a} (a = Bool) => [8]a

which complicates typechecking.

My vote would be to add an equality predicate on value types, but to treat it as a bit of a 2nd class citizen, in that it should never end up in type schemes. In particular, users shouldn't be allowed to write them, and they should never end up in type schemes (i.e., trying to unify bound variables of kind * would result in an error just like it does now, rather than producing a delayed equality constraint).

[brianhuffman]

Adding type equalities to the class system is probably too big of a change to be worth it just for this feature.