Different behavior with identical types

Stream: new members

[Paul Nelson]

I'm curious why the first and second examples behave differently, given that the types on the right hand side seem to be the same.

import Mathlib
example (i : ℕ) : ℚ → (ℕ → ℚ) := fun r ↦ Pi.single i r  -- OK
example (i : ℕ) : ℚ → (ℕ → ℚ) := Pi.single i            -- fail
example : ℕ → ℚ → (ℕ → ℚ) := Pi.single                  -- OK
variable {i : ℕ}
#check Pi.single i             -- ?m.8 i → (j : ℕ) → ?m.8 j
#check (fun r ↦ Pi.single i r) -- ?m.1893 i → (j : ℕ) → ?m.1893 j

[Kevin Buzzard]

The reason example (i : ℕ) : ℚ → (ℕ → ℚ) := Pi.single i fails is that Lean 4 is failing to solve the unification problem. Giving it a hint fixes the problem:

example (i : ℕ) : ℚ → (ℕ → ℚ) := Pi.single i (f := fun _ ↦ ℚ)         -- now works

Unification is generally an undecidable problem but I have this gut feeling that Lean 3 used to do a much better job of it than Lean 4 does. In particular when you look at the error message

type mismatch
  Pi.single i
has type
  ?m.1133 i → (j : ℕ) → ?m.1133 j : Type ?u.1130
but is expected to have type
  ℚ → ℕ → ℚ : Type

Lean it saying "I can't think of a function which sends i to ℚ and j to ℚ" and to be quite frank I'm surprised that it can't muster up the idea of the function which sends everything to ℚ.

[Paul Nelson]

this makes sense (second example failing), but I'm surprised it then succeeds in the first example, despite the types all looking the same, which suggests to me that there's something more going on under the surface than just the way the types are presented via #check

[Paul Nelson]

to put it another way, without any type annotation, why should fun r ↦ Pi.single i r and Pi.single i ever behave differently?

[Kevin Buzzard]

If Pi.single were a plain function and you were supplying all, or all-but-one, of the inputs, then your instinct would be right. But Pi.single has all these inputs:

Pi.single.{u, v₁} {I : Type u} {f : I → Type v₁} [inst✝ : DecidableEq I] [inst✝¹ : (i : I) → Zero (f i)] (i : I)
  (x : f i) (j : I) : f j

so Lean has to figure out two universes, two inputs (I and f) by unification, and two further inputs (DecidableEq I and (i : I) → Zero (f i)) by typeclass inference. All this figuring out is going on internally in some order which I have no clue about, but what I do know is that the more explicit inputs you give Lean, the easier these problems are to solve. I'm not saying I can explain completely what's going on (indeed I cannot do this) but I am saying that this is somehow the core of the problem. If there were an algorithm which could always solve for these unknown inputs correctly then that would be the end of it, but this problem is undecidable in general so Lean resorts to heuristics and not supplying the input changes the heuristics. It is not at all uncommon to have to help Lean 4 out using this (f := ...) trick.

[Kevin Buzzard]

For some reason that r is making some heuristics apply in a different order, so Lean knows for sure that f i = ℚ and this pushes it into thinking that f _ = ℚ sufficiently early on to make everything else work, because that's the way the code was written. Without the r maybe Lean tries to solve [inst✝¹ : (i : I) → Zero (f i)] earlier (for all I know) and barfs on f _. People who can read the actual Lean code could tell you precisely why the failure was occurring, but I've managed to get this far just knowing the symptoms and how to fix them.