The Coq mailing list

[Kathrin Stark <kathrin.stark AT rz-online.de>]

Hello,

I have a question concerning the "Typeclasses Filtered Unification" 
option.

Using the typeclasses eauto tactic, I would like to unify a pattern of 
the form
Test 0 ?n with another pattern of the form Test ?m ?m
 - however, Coq complains that the patterns do not match:
pattern (Test ?META158 ?META158) on (Test 0 ?n) failed with: pattern 
does not match

I don't understand why - I would have guessed it could unify ?META158 
with ?n with 0.
(Without the above option activated, it works out of course.)
So I wondered how exactly the pattern matching algorithm works? - 
Unfortunately I didn't find an answer to that.

The minimal code example can be found below.

Thank you very much!

Best,
Kathrin S.


------------------------------------------------------
Class Test (x y : nat) := testeqn : x = y.

Unset Typeclasses Filtered Unification.
Instance: forall n, Test n n.
Proof. reflexivity. Qed.
Set Typeclasses Filtered Unification.

Set Typeclasses Debug Verbosity 2.

Goal True.
  evar (n : nat).
  assert (Test 0 ?n). try typeclasses eauto.
 (* Here we get:
 simple apply Test_instance_0 with pattern (Test ?META158 ?META158) on 
(Test 0 ?n) failed with: pattern does not match *)
Abort.