The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Is it possible in Coq for an evar instance to exist in a goal such that 
it is "trapped" under binders?  Meaning that after all possible intros 
are done, the evar instance still can't be found using Ltac's context[] 
construct (as in [match .. with context[?V] => is_evar V ...], but 
has_evar senses it)?  Any case of an evar instance "trapped" under 
binders would seem to require that its type depends on bound variables.  
I can construct such cases within the conclusion of a goal, but they 
would become untrapped by doing sufficient intros, at which point 
context[] can find them.  I can't seem to construct any cases in 
hypotheses (trapped under vars bound in the hypothesis), however.  But, 
that's certainly not proof that it isn't possible.

If such trapped evar instances are possible, can anyone come up with an 
example?

-- Jonathan