Dot product for matmul

[mstn]

Summary

Partial application

Notes

Generic Partial Application

The issue with generic partial.apply-left is that its type witness does not constrain the inlined generic type strongly enough.

We defined it roughly as:

partial.apply-left :
  ty(B) * A * (A * B => C) -> (B => C)

For matmul, we need:

B = ([.b] ix val)
A = lhs/rhs environment
C = f32

Conceptually this is correct. But after inlining, the checker does not use:

ty(([.b] ix val))

to force every generic B inside the inlined body to become:

([.b] ix val)

So the structural closure-building path ends up with fresh metavariables like:

Leaf(779)
Leaf(781)

instead of the concrete ix b.

The first symptom was that two helper closures inside partial.apply-left were instantiated at different fresh types:

closure.unit-left-intro : Leaf(779) => 1 * Leaf(779)
closure.identity        : Leaf(781) => Leaf(781)

Combining those helpers into one def fixed that part by making both use the same variable:

Leaf(779)

But it still did not connect that variable to the concrete type required by:

name.matmul-f32-product-at : ({lhs,rhs} * ix b) -> f32

So the remaining mismatch became:

{lhs,rhs} * Leaf(779)
vs
{lhs,rhs} * ix b

In short: ty(B) is currently just an object flowing through the graph. It is not treated by the checker as a singleton proof that unifies B with the concrete type carried by the witness. Once the generic helper is inlined, the intended relationship between the witness and the type parameter is lost or too weak.