Type inference problem

Stream: lean4

[Michał Staromiejski]

Hi, I'm getting the following error:

application type mismatch
  assoc' (Term.op mul)
argument
  Term.op mul
has type
  (Fin (?m.1535 mul) → Term ?m.1535 ?m.1536) → Term ?m.1535 ?m.1536 : Type (max ?u.1532 0)
but is expected to have type
  (Fin 2 → Term arity ℕ) → Term arity ℕ : Type

where arity : Ops → ℕ is explicitly defined for mul : Ops as 2. Looking at meta-variables it should be easy to deduce

?m.1535 = arity
?m.1536 = ℕ

so I guess the problem is with ?u.1532. But why is it not deduced to 0 after other deductions are made? And why is there this meta-variable, is it because the domain type of ?m.1535 is not yet known?

[Kevin Buzzard]

#mwe ?

[Michał Staromiejski]

@Kevin Buzzard tried to create one and it was not easy. Will try to port to lean web and post a link here.

[Michał Staromiejski]

But anyway, it's a question about why those specific type "instances" cannot trigger proper inference.

[Kevin Buzzard]

My answer to these questions is usually "I don't have any understanding of how unification works so let me just add more hints" and this usually solves it.

[Kevin Buzzard]

i.e. type (assoc (Term.op mul) : [the type you want it to be]) somehow

[Kevin Buzzard]

With a MWE I'd try and do this for you.

[Michał Staromiejski]

With hints it works (enough to specify Term.op (s := arity) mul), I already know it :) But I want to understand this case...
The link to a "nsmwe" (not-so-minimal-...): here

[Michał Staromiejski]

Oh, just realised my question got "merged" with another similar one. Will go through the answer as well, maybe it would clarify more.

[Kevin Buzzard]

52 lines is perfectly minimal enough! I don't know how the unification algorithm works though, you're asking an interesting question, perhaps I'll learn something too.

[Jovan Gerbscheid]

Michał Staromiejski said:

application type mismatch
  assoc' (Term.op mul)
argument
  Term.op mul
has type
  (Fin (?m.1535 mul) → Term ?m.1535 ?m.1536) → Term ?m.1535 ?m.1536 : Type (max ?u.1532 0)
but is expected to have type
  (Fin 2 → Term arity ℕ) → Term arity ℕ : Type

Unfortunately, the unification algorithm here works from left to right, so it starts with 2 =?= ?m.1535 mul, and there it gets stuck and throws an error.

[Jovan Gerbscheid]

Generally, higher order unification is hard (i.e. there are metavariables that are functions). In this case it got the unification order the wrong way around to do manage the higher order unificaiton.

[Kevin Buzzard]

it's not just hard, it's undecidable right? Thanks for the explanation!