Typeclass resolution don't work with typeclass that depend on others

[TWal]

See the following example:

class tc1 (a:Type) = {
  tc1_method: unit;
}

class tc2 (a:Type) {|tc1 a|} (b:Type)= {
  //This function use the methods of tc1 to do its computation
  tc2_method: b -> a;
}

assume val test_type: Type
instance test_instance_tc2 (a:Type) {|tc1 a|}: tc2 a test_type = magic()

val test_function: #a:Type -> {|tc1 a|} -> test_type -> a
let test_function #a #pf1 x =
  tc2_method x
  //Workaround:
  //tc2_method #a #pf1 x

F* is able to infer the #a, and should be able to infer #pf1 using the typeclass resolution tactic.

[nikswamy]

Thanks for the example.

I was confronting something similar in the graded monad example here and worked around it by using a slightly different indexing structure: http://fstar-lang.org/tutorial/book/part3/part3_typeclasses.html#beyond-monads-with-do-notation

But my workaround is a bit unsatisfactory and not always applicable.

The problem is that in tcresolve we have

and trywith (seen:list term) (fuel:int) (t:term) : Tac unit =
    debug ("Trying to apply hypothesis/instance: " ^ term_to_string t);
    (fun () -> apply_noinst t) `seq` (fun () -> tcresolve' seen (fuel-1))

where the apply_noinst is requires a typeclass instance to match the goal but without instantiating any uvars in the goal.

This restriction is similar to Haskell's behavior on typeclass resolution, where metavariables in constraints that do not appear in the generalized type of the term are not solved. A classic example is Haskell refusing to solve show [] : Show a => string since the choice on instantiation of a can result in different results (e.g., a = char, produces "" while any other choice would produce [])

In this particular example, the goal is

tc2 a #(*?u1*) _ test_type

where ?u1 : tc1 a

Now, we may be able to relax this restriction in F*.

The simplest patch would be to allow instantiations of uvars here by just using apply instead of apply_noinst.

A more subtle patch would be something like allowing the instantiation of only certain kinds of uvars, e.g., in this case ?u1 is uvar for a typeclass instance, so it may be okay to instantiate.

@mtzguido , any thoughts about this?

[TWal]

Thank you for the interesting and detailed answer! My feeling was that since ?u1 is a Q_Meta tcresolve argument of tc2, then it could be instantiated with another invocation of tcresolve. In a way, the second argument of tc2 is deduced from its first argument via tcresolve, so there should be no ambiguity. Maybe this is too naïve?

[mtzguido]

I took a look at this, I think crux of the problem here is that the meta qualifiers of the tc2 class are lost in its projectors (and just turned into regular implicits). This means the methods inherit the meta-less implicits, and therefore there is no way to solve for the tc1 a needed to call test_method2. I have a patch to retain these, which makes this example work. If everest comes back green I will merge it.

I also removed Nik's workaround for the graded monad, it works sensibly now.

The more fundamental of problem of the order of resolution stands, though.