Typeclass resolution interacts badly with dependent types

[andrew-appel]

Version 8.5, 8.6, 8.7.2, 8.8+beta1

Operating system: all

File: https://github.com/PrincetonUniversity/VST/blob/master/progs/bug83.v in any version of VST since commit b9396a780ea14d26542eed3181d154fc4c116673

This is not exactly a bug report: it is well known that, because Coq's typeclass resolution is performed after unification, there are some interactions of typeclasses with typechecking that Coq cannot resolve. See for example Gonthier et al., "How to make ad hoc proof automation less ad hoc", JFP 23 (4): 357–401, 2013.

Here I present a specific example, one that is quite troublesome for VST, which we have been living with for several years now. If someone wants to do research on better algorithms for doing typeclasses with dependent types in Coq, this could be a good test case.

The @data_at predicate is a dependently typed version of the separation-logic "maps-to" operator:

@data_at: forall (cs : compspecs) (sh: share) (t : type) (v: @reptype cs t) (p: val), mpred.

where the type of v depends on the values of cs and t. (See section 3 of Cao et al, VST-Floyd: A separation logic tool to verify correctness of C programs, JAR 2018)

The @exp predicate is an existential quantifier in (possibly lifted) separation logic (see Chapter 21 of Appel et al., Program Logics for Certified Compilers, 2014), using higher-order abstract syntax:

Class NatDed (A: Type) := mkNatDed {
  andp: A -> A -> A;
  exp: forall {T:Type}, (T -> A) -> A;
  . . . }.

The type mpred ("memory predicates") is way to instantiate the A parameter of the NatDed class, but we also have lifted instances of the typeclass,

Instance LiftNatDed (A B: Type) {ND: NatDed B} : NatDed (A -> B) :=
 mkNatDed (A -> B)
    (*andp*) (fun P Q x => andp (P x) (Q x))
    (*exp*) (fun {T} (F: T -> A -> B) (a: A) => exp (fun x => F x a))
   . . .  .

So therefore (environ->mpred) is also a way to instantiate the parameter of the NatDed class.

Finally, in the example file, we have SEPx: list mpred -> environ -> mpred.

And here is the example:

Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Fail Definition h : environ->mpred := 
 @exp _ _ _ (fun s : val => 
  SEPx (@data_at _ Tsh (Tstruct _tree noattr) (Vundef, (Vundef, (Vundef, Vundef))) Vundef :: nil)).

The problem is this: The cs parameter of @data_at is necessary to type-check that the value (Vundef, (Vundef, (Vundef, Vundef))) really belongs to @reptype cs (Tstruct _tree noattr), but unfortunately the typeclass resolution does not instantiate cs until too late.

What is interesting about this example is that if one instantiates the first underscore parameter of @exp, then typechecking succeeds! This is demonstrated in the file (Definition f), along with several other examples of how slight variations of definition h will successfully typecheck.

[lastland]

I have just played with your example. My understanding of the problem is a bit different.

I tried enabling type class debugging before executing your example:

Set Typeclasses Debug.

Now Coq gives me the following information:

Debug: 1: looking for (NatDed ?A) with backtracking
Debug: 1.1: exact Nveric on (NatDed ?A), 0 subgoal(s)
Debug: 1: looking for compspecs without backtracking
Debug: 1.1: exact CompSpecs on compspecs, 0 subgoal(s)
The command has indeed failed with message:
In environment
s : val
The term
 "SEP (data_at Tsh (Tstruct _tree noattr) (Vundef, (Vundef, (Vundef, Vundef)))
         Vundef)" has type "environ -> mpred" while it is expected to have type
 "mpred".

What happens is that Coq first performs a proof search for the NatDed instance. Since it has not yet type checked the lambda term (because it has not found an instance for compspecs), it does not know what the first parameter of @exp should be. It will greedily fill in the Nveric instance (which has type NatDed mpred) and make the first parameter mpred. This explains why Coq will give you such a bizarre error message: why it is expecting mpred rather than environ -> mpred.

If we force Coq to reverse the order it searches type class instances we can successfully define h:

Definition h : environ->mpred :=
  let t := (fun s : val => 
  SEPx (@data_at _ Tsh (Tstruct _tree noattr) (Vundef, (Vundef, (Vundef, Vundef))) Vundef :: nil)) in
 @exp _ _ _ t.

And now the proof search looks correct:

Debug: 1: looking for compspecs without backtracking
Debug: 1.1: exact CompSpecs on compspecs, 0 subgoal(s)
Debug: 1: looking for (NatDed (environ -> mpred)) without backtracking
Debug: 1.1: simple apply LiftNatDed' on (NatDed (environ -> mpred)), 1 subgoal(s)
Debug: 1.1-1 : (NatDed mpred)
Debug: 1.1-1: looking for (NatDed mpred) without backtracking
Debug: 1.1-1.1: exact Nveric on (NatDed mpred), 0 subgoal(s)
h is defined

[lastland]

I do not know why Coq cannot figure out the first parameter of @exp should be environ -> mpred by looking at the return type in the failed definition. If Coq can figure that out, we do not need to reverse the order of type class instance search.

Here is one way of forcing Coq to do that:

Definition h : environ->mpred.
  eapply (@exp _ _ _).
  exact (fun s : val => SEPx (@data_at _ Tsh (Tstruct _tree noattr) (Vundef, (Vundef, (Vundef, Vundef))) Vundef :: nil)).
Defined.

This definition should be equivalent to your failed definition. But this one works.

[lastland]

Here's a smaller example (with no dependency) that would exhibit the same bug:

Inductive AType := AConstr : AType.
Definition BType : Type := (bool * AType).

Section TC.
  Class Foo (A : Type).
  Class Bar := { flag : bool }.

  Instance aBar : Bar := { flag := true }.

  Axiom foo : forall A, Foo A -> A -> A.

  Definition rep (b : Bar) : Type :=
    if flag then AType else BType.

  Axiom bar : forall b : Bar, rep b -> nat.

  Instance natFoo : Foo nat.

  Instance boolFoo : Foo bool.

  Set Typeclasses Debug.
  Fail Definition f : nat := foo _ _ (bar _ AConstr).
  (* The command has indeed failed with message: The term "bar aBar
     AConstr" has type "nat" while it is expected to have type
     "bool". *)

  Definition g : nat := foo nat _ (bar _ AConstr).
  Definition h : nat := foo _ _ (bar aBar AConstr).

  Definition f : nat.
    eapply (foo _ _).
    exact (bar _ AConstr).
  Defined.
End TC.