Metavariable suddenly appears from nowhere?

[lovely-error]

In the code I've written, a metavariable suddenly appears after application.
You can witness the problem yourself on the playground

[nomeata]

Thanks for the report. Is there a reason you deviated from the issue template? It is helpful if the bug report includes an ideally minimal example, and it's clear without guessing where the behavior doesn't match your expectations, and what you expected instead. It's preferable to include the code in the bug report.

[lovely-error]

Hello. If you go through the link, you will land on a web lean playground where the code is present. There are two versions, one which errors and one which doesn't. They are functionally identical, so I expect that both work.

[Rob23oba]

The error here is that OEq has two universe parameters: one for the outer Sort _ and one for the inner Sort _ and similarly is_contr has two universe parameters. oeq_is_eq only works though if the second universe is 0, i.e. ∀ (P : A → Prop), P a → P b is used. Because of using oeq_is_eq, contr_to_contr_fun_sp then also restricts itself to the second universe variable being 0. In contr_sp_fun_irrel however it expects it to work for all pairs of universe variables but contr_to_contr_fun_sp doesn't allow for that. The "match contains meta-variables" error masks the actual error which is (on the latest version):

Application type mismatch: In the application
  contr_to_contr_fun_sp c
the argument
  c
has type
  is_contr.{u_1, u_2} T : Sort (max (max 1 u_1) (imax u_1 (max u_1 (u_2 + 1)) u_2))
but is expected to have type
  is_contr.{?u.593, 0} ?m.594 : Sort (max 1 ?u.593)

Here you can see that c is is_contr with an arbitrary second universe parameter but contr_to_contr_fun_sp only accepts it with the second universe variable being 0. You can fix this problem by using A → Prop explicitly in OEq.
(Note: the confusion may come from the fact that you'd expect OEq in your form to mean "for all universes u and P : A → Sort u, P a → P b" while it actually means "for every universe u make a variant of OEq that looks like ∀ (P : A → Sort u), P a → P b". In other words, you have many different OEq a bs for every universe level)

[Rob23oba]

Regarding the question this issue is about: Lean uses meta-variables all the time to find out implicit parameters (in this case T). When writing contr_to_contr_fun_sp, it uses a meta-variable to fill T: is_contr ?m → is_contr (?m → ?m). Because the type of c didn't match up because of universe problems, it then doesn't gain any information and infers the type of the application as is_contr (?m → ?m). Because is_contr T is defined as (cc : T) ×' ∀ i, OEq i cc, this type is equivalent to (cc : ?m → ?m) ×' ∀ i, OEq i cc. You then match on this value implicitly using the let (a) := b tactic (which expands to match b with | a => ?_) and cc now has type ?m → ?m. However, we don't want to have meta-variables in types of local declarations which is why it then complains about the existence of meta-variables (the additional number part is to make sure that different meta-variables can be distinguished).