Fixes for typeclasses

[mtzguido]

Most importantly, trying to defer the execution of meta-args until their environment and goal are fully defined. This reduces the order dependency observed in #3130, but it's not completely eliminated. In particular, we F* can still try to run a meta-arg in a partially-unresolved context, but maybe we should remove that possibility altogether.

[mtzguido]

but maybe we should remove that possibility altogether.

I've now done this, turns out everything works fine without it given the other changes! This means we are essentially forcing typeclasses (meta args in general) to run in topological order of dependencies, and we will never attempt a problem that is not fully defined, so we should not see anything unexpected.

This doesn't solve #2602 though, @@resolve_implicits is a different beast.

[TWal]

This one fails now. It's a bit strange, it doesn't use a fancy typeclass dependency.

class ord_leq (a:eqtype) =
  { leq: a -> a -> bool
  ; trans: (x:a) -> (y:a) -> (z:a) -> Lemma (x `leq` y /\ y `leq` z ==> x `leq` z)
  }

let transitivity {| ord_leq 'a |} (x y z : 'a)
  : Lemma (x `leq` y /\ y `leq` z ==> x `leq` z)
  [SMTPat (x `leq` y); SMTPat (x `leq` z)]
  = trans x y z

let transitivity_forall #a {| ord_leq a |} unit
  : Lemma (forall (x y z : a). x `leq` y /\ y `leq` z ==> x `leq` z )
= ()

[TWal]

(looks like typeclass resolution is bamboozled by the unit, which is misleading: I guess the intent was for it to be (), but it is in fact a variable named unit of unknown type ; removing this extra argument or replacing it with () works fine.)

[mtzguido]

Ah, yes, the typeclass tactic will now not run in contexts with unresolved types in them, so this unit:_ is to blame. But the error is pretty bad, and could also expect for the unit:_ to be generalized into unit:b for some fresh b, and only then try to solve the constraints.

I'll try to at least make it clear that the tcresolve tactic is not running.

[TWal]

I agree, the code looks a bit fishy and should probably be fixed! Although in that case I would indeed expect to have unit:b for some fresh b.

Here is something else that works with master but not this PR (from Comparse tests):

class bytes_like (bytes:Type0) = {
  x:unit;
}

assume val t: bytes:Type0 -> {|bytes_like bytes|} -> a:Type -> Type

irreducible let with_parser (#bytes:Type0) {|bytes_like bytes|} (#a:Type0) (x:t bytes a) = ()

assume val test_dep_nat_e: bytes:Type0 -> {|bytes_like bytes|} -> nat -> Type0

assume val ps_test_dep_nat_e: #bytes:Type0 -> {|bytes_like bytes|} -> n:nat -> t bytes (test_dep_nat_e bytes n)

assume val ps_option: #bytes:Type0 -> {|bytes_like bytes|} -> #a:Type -> t bytes a -> t bytes (option a)

noeq type test_with_parser (bytes:Type0) {|bytes_like bytes|} = {
  [@@@ with_parser #bytes (ps_option (ps_test_dep_nat_e 256))]
  f2: option (test_dep_nat_e bytes 256);
  [@@@ with_parser #bytes (ps_option (ps_test_dep_nat_e 256))]
  f3: option (test_dep_nat_e bytes 256);
}

[mtzguido]

I updated the branch. The example with the extra unit:_ argument now works by generalizing it before typeclass resolution.

The other snippet also works after a fix to the checking of binder attributes.

I have one more tiny regression, which I'm still looking at.

[mtzguido]

I think everything should work now, still with the restriction of not running meta args in any open context/type. Turns out we did rely on it in one place (FStarLang/steel#127) but I think we can just set a compat option for now.

Maybe the right thing to do is add a marker to the tactic specifying it "accepts" being called in unresolved contexts. We could even do that for typeclasses in order to introduce functional dependencies, allowing tcresolve and the unifier to interoperate in a single common loop. But I think this PR can go in already.

[TWal]

Hmm, this files still fails with me: https://github.com/TWal/comparse/blob/main/src/Comparse.Bytes.Typeclass.fsti .
It seemed like you added it in F* tests in commit 8e9f09a but I don't see it anymore, did you remove it?

[mtzguido]

It's still there, just in my fork mtzguido@8e9f09a. And I just downloaded that file and it passes for me.

Are you sure you're on bbbcff1? I did have to bump the checked file version, so maybe a make clean would be needed...

[TWal]

Hmm, sorry I did the test between two meetings and completely messed-up my git-fu.
Everything works well for me!

[nikswamy]

I just had a look through it. It look good to me.

Note to self. I see the main semantic changes are:

• Rel.fst: is should_run_meta_arg to block unless the ctx uvars are empty; and to skip solving such main cases in the main resolve_implicits loop, unless the compat flag is set.
• The change in generalize to skip past variables that the meta attribute set

Also, great to see the more widespread use of show etc. throughout.

Thanks!

[mtzguido]

Everything works well for me!

Awesome! Thanks for the all the examples, they were super helpful.