Widen types if they are used in typeclass constraints

[nikswamy]

Consider this program:

class eq a = {
    deq : a -> a -> bool
}
instance eq_int : eq int = {
    deq = ( = )
}
let test4 (x:int{x > 0}) (y:int{y > x}) = deq x y

This fails typeclass resolution since type inference gets constraints of the form:

x:int{x > 0} <: ?u
y:int{y > x} <: ?u

and solves ?u to the meet x:int{ x > 0 \/ y > x} . Typeclass instantiation then fails to find an instance at this refined type.

There are some ways to workaround this, e.g., by adding explicit instances for refined types

instance eq_refine (#a:Type) {| d : eq a |} (p:a -> Type) : eq (x:a { p x }) = {
  deq = fun (x y: (x:a { p x } )) -> d.deq x y
}

But, this requires the programmer to provide these additional instances.

In this patch, I am changing type inference so that if a variable ?u appears in a goal that is to be solved by typeclass resolution, then when computing the meet of types in a solution of ?u, I widen the meet to the nearest common named type.

With this patch, we now have the following behavior:

This works, resolving to int:

let test4 (x:int{x > 0}) (y:int{y > x}) = deq x y

This fails since there is no instance on nat (since widening goes to the nearest common named type, in this case nat)

let test6 (x:nat) (y:nat) = deq x y

But, this works:

instance eq_nat : eq nat = {
    deq = ( = )
}

let pos = x:nat { x > 0}
//also works in master with nat
let test7 (x:nat) (y:pos { y > 17 }) = deq x y
//fails in master, works here at nat
let test8 (x:nat{ x > 2 }) (y:pos { y > 17 }) = deq x y

Note, it also works in the unary case, i.e., it widens a type even when there is no meet of two types to take.

class neg a = {
    dneg : a -> a
}

instance neg_bool : neg bool = {
    dneg = fun x -> not x
}

let tneg (x:bool) = dneg x
//fails in master
let tneg2 (x:bool { x = true }) = dneg x

[mtzguido]

Looks good! I confirmed it doesn't break the secure IO repo.

[TWal]

This definitely looks useful because typeclass resolution on refined types is one of the major pain points of using typeclasses in F* code!

However, I'm a bit concerned that this is only a partial step to solving this problem.
I feel like test6 should succeed: nats are ints, which means we could use the int typeclass instantiation.

The workaround of adding an instantiation for subtypes doesn't work in most cases. Here it works because in eq a, all the a are at the left of arrows. But if your typeclass looks like this:

class eq_monoid (a:Type) = {
  deq: a -> a -> bool;
  zero: a;
  add: a -> a -> a;
}

Then it not possible to do a workaround such as eq_refine. The only workaround is to do

let test6' (x:nat) (y:nat) = deq (x <: int) (y <: int)

which is not very convenient.
The only real solution would be to change how F* calls the typeclass resolution meta-program:
if the typeclass resolution fails, then try to widen the type by removing one refinement, until it succeeds or you can't widen the type anymore.

In test6, it means that we would try to do typeclass resolution on nat, which would fail. Because nat = n:int{0 <= n}, then we would try on int and it would succeed.

Do you think it would be possible to integrate this mechanism? If you do, this would solve most of the issues I have with typeclasses in F*!

[nikswamy]

hi @TWal

I agree with your remark.
And yes, certainly this:

The workaround of adding an instantiation for subtypes doesn't work in most cases. Here it works because in eq a, all the a are at the left of arrows.

I see this widening as a step towards further improvement.

I plan to investigate adding backtracking: that is, once the unifier picks a candidate solution, we run the typeclass instance resolver to see if it it can find a solution too; if not, backtrack, widen further (e.g., unfolding definitions and widening nat to int) and try again.