Add weak kvars

[cole-k]

This PR adds support for weak, or external kvars. These are inference variables which fixpoint (usually) can't natively handle because they tend to appear only in either head position (meaning they can trivially be solved to true) or body position (meaning they can be trivially solved to false).

We generate weak kvars on function signatures, representing holes that can be filled in with refinements. The intended use for theses is for inferring function signatures to fix type errors.

There are some caveats to the code introduced here.

1. This code should not directly affect constraint generation. It will change constraints, because weak kvars are not completely elided when being emitted (they get turned into true). But these constraints should be equivalent to the constraints prior. Previously, we emitted weak kvars as UIFs (which should also not affect constraint generation in theory), but this was causing strange bugs in fixpoint.
2. The UIF generation is available as part of the code, and we do emit UIF definitions to fixpoint --- we just don't use the UIFs.
3. The UIF encoding is probably not necessary. Right now the only interaction fixpoint has with weak kvars is syntactically solving non-cut kvars to solutions which may contain weak kvars via the fusion algorithm. So if we depend upon fixpoint to solve these non-cut kvars, then we need to encode weak kvars as UIFs so that they can be "moved around" into the solutions of non-cut kvars. However, I have some code to implement fusion in Flux directly, which means we can skip this hacky encoding.
4. This is not presently gated behind a feature flag, but follow-up work will gate it as well as add a compilation flag. So if it makes sense, we could just merge one big PR or a stacked PR so we don't get an intermediate state where weak kvars are generated (but unused).

[cole-k]

@nilehmann I'm getting some failing tests relating to

https://github.com/flux-rs/flux/blob/ck-add-wkvars/crates/flux-infer/src/infer.rs#L1045-L1048

One of the compared sides has weak kvars added to its function signature and the other does not.

There are a couple possible answers I can imagine:

• NEITHER left nor right should have weak kvars, i.e. we shouldn't add weak kvars for FnPtrs ever (in which case, how do we avoid doing so?)
  • I don't actually think this is true --- I feel like we should be able to add more refinements onto them.
• BOTH left and right should have weak kvars, i.e. I'm missing a spot (in which case, where do you think this might be? I add weak kvars in queries and fhir)
• The refining is done correctly, but we should be subtyping by assuming the weak kvars are TRUE or something of that nature.
  • I tried "stripping" them by setting them to true but the comparison failed I think because it's syntactic.

Also the occurs check failure is occurring in tock now... I can't remember if I did anything or if it resolved itself. https://github.com/flux-rs/flux/blob/ck-add-wkvars/crates/flux-refineck/src/type_env.rs#L552-L555

Your thoughts?

[nilehmann]

@cole-k We should not add weak kvars to function pointers. It's theoretically possible to add refinement to function pointers, but we currently don't have the necessary checks, so the assumption is that function pointers never have refinements, hence the assertion.

[cole-k]

@cole-k We should not add weak kvars to function pointers. It's theoretically possible to add refinement to function pointers, but we currently don't have the necessary checks, so the assumption is that function pointers never have refinements, hence the assertion.

I just pushed a commit that lets you turn off wkvar adding wherever we call genv.fn_sig. Can you tell me which places I need to pass false to?

Or do I need to do something else to ensure FnPtrs don't get wkvars.

[nilehmann]

Function pointers don't go through the fn_sig query; they are a type. To avoid adding weak kvars, you need to stop the folder at BaseTy::FnSig.

[cole-k]

@nilehmann per our discussion I ignored BOTH ImplItem and TraitItem fhir Nodes. I'm not sure that removing Implitem is right but I had the same sort encoding bug where this time Adt1(Adt0) was getting encoded as Adt1(int) — and normalizing again didn't work (at least the attempts I made). It was failing for tests/tests/neg/extern_specs/extern_spec_iter00.rs.

This might break some of the tests in our benchmarks, but I think it's unlikely since most traits are things we are using not modifying.

EDIT: Also the occurs check is failing in tock too, so I'll take a look at that now…

[cole-k]

We think you can have wkvars in both TraitItem and ImplItem; the latter should be easier. But we don't know how to make it work for either yet.

[cole-k]

Circling back to this before I get busy because of other stuff.

I think we can do away with the wkvar UIF encoding, at least for this PR.

We can decide for the one that introduces and uses wick whether or not to add it. The good news is that I have some (perhaps untrustworthy) changes which (1) implement fusion in flux correctly and (2) avoid sending wkvars as UIFs off to fixpoint as a result --- they do depend on some changes in Haskell fixpoint, but we can discuss if they are reasonable or not at a later time.

So there is hope yet that we can do away with the UIF encoding in the limit.

Immediate next step is to open as a PR and add description.

Next step after merging this in is to rebase ck-refinement-suggestions on top (may be a bit messy).