flux-rs / flux

Refinement Types for Rust
MIT License
660 stars 21 forks source link

A bit of function subtyping for `ReifyFnPointer` #874

Closed ranjitjhala closed 1 week ago

ranjitjhala commented 3 weeks ago

Fixes #859

ranjitjhala commented 2 weeks ago

ping @nilehmann

ranjitjhala commented 2 weeks ago

I'd prefer if we do the subtyping when we check the cast (ReifyFnPointer).

that would indeed be preferable but I don’t see how that’s possible since at that point we don’t know what the “super-type” is supposed to be?

ranjitjhala commented 2 weeks ago

At best one can imagine

  1. generating a KVAR template at the cast site and creating a subtyping constraint there and
  2. then generating a subtyping between the template and the actual super type at the actual usage site

but that seems rather overkill to me and really what the FnDef is avoiding.

ranjitjhala commented 2 weeks ago

So I’d say what we’re “gaining” is avoiding this redundant indirection through Kvars, unless you see some other way to do it?

nilehmann commented 2 weeks ago

We do know the type because it's unrefined. When checking a cast we have the rust target type (which in this case should be a FnPtr). We need the default refinement for that type and then check against it.

ranjitjhala commented 2 weeks ago

Ah yes of course, we do now but (hopefully soon) we'll want to refine the FnPtr and then we won't have that info, so why paint into a corner?

nilehmann commented 2 weeks ago

I'm not convinced this is the best way to support refined function pointers. If we want the function pointer to be polymorphic we could instead put some refinement parameters (the ones not mentioned in clauses) as part of Binder instead of EarlyBinder. Also, storing a function in a variable and then using it multiple times is rare so I'm not even convinced we need it to be polymorphic, at which point this is just an optimization (to avoid extra kvars).

ranjitjhala commented 1 week ago

Ok @nilehmann have moved the subtyping to the cast site.