Exact not matching

Stream: new members

[Guilherme Espada]

Does anyone have any idea on why the following terms wouldn't be considered matchable by exact?

invalid type ascription, term has type
  typ ctx (subst 0 t_t2 ev_t12_t1) (a_T11.ty_func T)
but is expected to have type
  typ ctx (subst 0 t_t2 ev_t12_t1) (?m_1.ty_func T)

I've manually confirmed that ?m_1 and a_T11 have the same type.

Thanks

[Guilherme Espada]

Additionally: doing sorry says

exact tactic failed, failed to assign
  sorry
to metavariable ?m_2 (possible cause: occurs check failed)

[Guilherme Espada]

I got it: the relevant metavar comes from outside the current goal