The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

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.