Type Inference Conditions #60
Description
Since we added type class instance erasure, I was always unsure about whether type class specialization (TCS) was still necessary. I've since come to conclude that we don't need TCS... if we introduce what I'll call "type inference conditions".
Background
My canonical example for TCS is the theorem
(app (app (app (app (app (app (const "HMul.hMul" ?u ?u ?u) ?A) ?A) ?A) (inst (app (app (app (const "HMul" ?u ?u ?u) ?A) ?A) ?A))) (app (app (app (const "OfNat.ofNat" ?u) ?A) (lit 1)) (inst (app (app (const "OfNat" ?u) ?A) (lit 1))))) ?a)
=>
?a
if
(inst (app (const "Group" ?u) ?A))
You can see that the type ?A and the universe ?u only appear in the LHS and not the RHS. Also, the type class condition requires us to figure out what ?A and ?u are before we can run synthesis. Thus, as is, the rewrite is only applicable in the forward direction. To obtain the backward direction, we currently perform TCS. That is, we try to generate a rewrite where all occurrences of type class instances in the rewrite are already instantiated. In this case, if we have some type G with an instance inst : Group G in our context, we'd generate a rewrite where the type class condition is "filled in" by inst. As a result ?u and ?A also get resolved. Thus, the only remaining variable on both sides is ?a, and the rewrite can be applied in both directions.
Historical Changes
You might have noticed in the example above, that it's kind of weird that we're instantiating a type class instance, because the body of the rewrite doesn't contain any type class instances in the first place (because we do type class instance erasure). This phenomenon is due to historical reasons. Before we had type class instance erasure, type class instances could appear in the rewrite's body, and TCS instantiated those instances. Nowadays, type class instances don't actually appear anywhere - their only remnant are type class instance conditions. But type class instance conditions can be synthesized during equality saturation, so there's not much value in filling them in beforehand either. What we actually want nowadays is something like "type specialization". That is, in order to enable the backward direction for the given rewrite above, we want to know what ?A is (and ?u, but that's more of a technical detail).
Type Inference Conditions
In order to allow us to obtain ?A when matching on the RHS, I propose adding a way to run type inference during equality saturation. Just as we have type class conditions which run type class synthesis, there should be "inference conditions" which run type inference.
TO BE CONTINUED...