inhabited_value doesn't really work well

[andrew-appel]

Ltac inhabited_value, in floyd/deadvars.v, does not work well.

1. The failure message doesn't work, because Ltac does not allow mixing of failure messages with returning constr results, in some cases. The behavior is that instead of the failure message, we get Expression does not evaluate to a tactic (got a constr).
   This can be fixed by replacing

let t := eval unfold T in T in
         tryif constr_eq t T 
         then fail 3 "cannot prove that type" T "is inhabited... "
         else inhabited_value t

with simply fail 3 "cannot prove.." , but then the extra functionality of unfolding definitions is lost. It's probably worth making the change, though, because otherwise the error message from deadvars is inscrutable.

2. The tactic really should look up type T to see whether there is anything of type Inhabitant T in the typeclass_instances database, but I don't know how to do that in Ltac. Perhaps it's possible in Ltac2 ?