Coq: why do I need to manually unfold a value even though it has a `Hint Unfold` on it?

Question

I've come up with the following toy proof script:

Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Unfold myValue.

Example test: myProp myValue.
Proof.
  auto 1000. (* does nothing *)
  unfold myValue.
  trivial.
Qed.

Why do I need to manually unfold myValue here? Shouldn't the hint suffice?

Answer 1

That's because (see refman)

This [Hint Unfold <qualid>] adds the tactic unfold qualid to the hint list that will only be used when the head constant of the goal is ident.

And the goal myProp myValue has myProp in the head position, not myValue.

There are several ways of dealing with this:

Hint Extern 4 => constructor.   (* change 4 with a cost of your choice *)

or

Hint Extern 4 => unfold myValue.

or even

Hint Extern 1 =>
  match goal with
  | [ |- context [myValue]] => unfold myValue
  end.