The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

I don't accept Patrick's answer "What gets you confused is probably
...  the difference between opaque and transparent constants."

Consider the following examples, where "reflexive" is transparent in
both examples:

  Reset Initial.
  Variables A:Set; R:A->A->Prop.
  Definition reflexive : Prop := (a:A)(R a a).

  Lemma test: (refl:reflexive)(a:A)(R a a).
  Intros.
  Apply refl.

We get "Subtree proved!".  On the other hand:

  Reset Initial.
  Variables A:Set; R:A->A->Prop.
  Definition reflexive : Prop := (a:A)(R a a).

  Record Setoid : Type := { refl: reflexive }.

  Lemma test: (S:Setoid)(a:A)(R a a).
  Intros.
  Apply refl.        (* fails *)

This fails with

  test < Apply refl.
  Error during interpretation of command:
  Apply refl.
  Error: Impossible to unify reflexive with (R a a)

However if we define an type-expanded version of "refl"

  Definition refl_unfolded: Setoid->(a:A)(R a a) := refl.
  Apply refl_unfolded.

This works.  In this case, instead of defining "refl_unfolded" we
could also use "Apply (refl S)."  (Why??) 

But we can't make "(refl S)" a Hint, because "S" is local to the lemma
and is not known at top-level.

So my question still stands how to avoid this ugly expanded-version
trick?

Randy