error: failed to unify

Stream: general

[Johan Commelin]

I am at a stage where I am currently hitting errors of the following type

invalid apply tactic, failed to unify
  p.fst = q.fst
with
  ?m_2 = ?m_3

I have no clue why Lean can't unify those... probably there are some hidden metavariables somewhere... how do I get more info?

[Johannes Hölzl]

can you try to use set_option pp.all true and inspect the term again

[Johan Commelin]

Thanks, the response by Lean was a little bit overwhelming. But it solved my problem!