The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I don't have an explanation, but here's a smaller example:

Axiom SProp : Set.

Axiom sp : SProp.

(* If we hardcode valueType := nat, it goes through *)

Class StateIs := {

  valueType : Type;

  stateIs : valueType -> SProp

}.

Instance NatStateIs : StateIs := {

  valueType := nat;

  stateIs := fun _ => sp

}.

Class LogicOps F := { land: F -> F }.

Instance : LogicOps SProp. Admitted.

Instance : LogicOps Prop. Admitted.

Set Printing All.

Parameter (n : nat).

(* If this is a [Definition], the resolution goes through fine. *)

Notation vn := (@stateIs _ n).

(* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)

Definition BAD : SProp :=

  @land _ _ vn.

Perhaps there's a bug in typeclass resolution when the instance we're picking out is determined by a field of the class?  Maybe this should be reported on the bug tracker?

-Jason

On Tue, May 13, 2014 at 4:05 PM, Andrew Kennedy <akenn AT microsoft.com> wrote:

Hello

I'm puzzled by a failure of type class resolution in my Coq code; unless I am completely explicit and supply the full instance information the code does not type check, even though it seems to me that it is unambiguous. I have boiled it down to a smallish fragment, shown below. Note that the "StateIs" class uses T to determine both a type (the type associated with the "variable" type T) and an "variable-is" predicate.

Any help much appreciated!

Cheers
Andrew.

Inductive BoolVar :=  IsRaining | IsSunny.
Inductive NatVar := Year | Month | Day.

Inductive State :=
| mkState (nats: NatVar -> nat) (bools: BoolVar -> bool).

Definition eqState s1 s2 :=
  match s1, s2 with
  | mkState n1 b1, mkState n2 b2 => forall v, n1 v = n2 v /\ forall v, b1 v = b2 v
  end.

Inductive SProp :=
| mkSProp (st: State -> Prop).

Class StateIs T := {
  valueType : Type;
  stateIs : T -> valueType -> SProp
}.

Notation "x ~ y" := (stateIs x y) (at level 10).

Instance NatStateIs : StateIs NatVar := {
  valueType := nat;
  stateIs x v := mkSProp (fun s => match s with mkState n b => n x = v end)
}.

Instance BoolStateIs : StateIs BoolVar := {
  valueType := bool;
  stateIs x v := mkSProp (fun s => match s with mkState n b => b x = v end)
}.

Class LogicOps F := {
  land: F -> F -> F
}.

Notation "x //\\ y" := (land x y) (at level 40).

Instance SPropLogicOps : LogicOps SProp := { land := fun P Q =>
  match P, Q with mkSProp SP, mkSProp SQ => mkSProp (fun s => SP s /\ SQ s) end }.

Instance PropLogicOps : LogicOps Prop := { land := and }.

(* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
Definition BAD (v: NatVar) (n: nat) : SProp :=
  v ~ n //\\ Year ~ 2014.