Inline signatures vs signatures in let bindings

Stream: lean4

[cognivore]

@Arthur Paulino has encouraged me to report this: https://github.com/cognivore/FuncDep.lean/commit/55c9a46fd9fb94874861e3fe8ef7c7c9080f765e#r77932527

[cognivore]

It should work because $\text{instCountParts\_String.}\alpha$ is $\mathbb{N}$ .

[Arthur Paulino]

Oh, what about let n₂' := ((FuncDep.CountParts_.φ "Tarmogoyf" 'o') : Nat)?

[Arthur Paulino]

(just to make sure we're helping Lean with the right term)

[cognivore]

It won't work. Or do you assume that : is right-associative and 'o' : Nat would typecheck? :D

[cognivore]

I'll try, one sec.

[cognivore]

Arthur Paulino said:

Oh, what about let n₂' := ((FuncDep.CountParts_.φ "Tarmogoyf" 'o') : Nat)?

Same error.

[Arthur Paulino]

Here's a more distilled #mwe:

class CountParts_ (S : Type u) where
  μ : Type v
  α : Type w
  φ : S → μ → α

instance : CountParts_ String where
  μ := Char
  α := Nat
  φ haystack needle := haystack.foldl (fun acc x => acc + if x == needle then 1 else 0) 0

class CountParts (S : Type u) (μ : Type v) (α : Type w) where
  φ : S → μ → α

/- Somehow, Lean manages to see `Nat ~ CountParts_.α String` in the instance declaration! -/
instance : CountParts String Char Nat where
  φ haystack needle :=
    let y : Nat := instCountParts_String.φ haystack needle
    y + 1

instance : CountParts String Char Nat where
  φ haystack needle := (instCountParts_String.φ haystack needle) + 1
-- failed to synthesize instance
--   HAdd (CountParts_.α String) Nat ?m.4026

instance : CountParts String Char Nat where
  φ haystack needle := ((instCountParts_String.φ haystack needle) : Nat) + 1
-- failed to synthesize instance
--   HAdd (CountParts_.α String) Nat ?m.4098

We were trying to understand why the first instance typechecks and the others don't
We're on nightly from 2022-05-29 btw

[Arthur Paulino]

I just tested on a more recent version (leanprover/lean4:nightly-2022-07-04) and the same error occurs

[Mac]

If I understand correctly, the difference is that (x : T) doesn't actually assign type T to x (it just hints at it) whereas let y : T := x actually does.

[Mac]

Here is an old thread with a part by @Mario Carneiro on the topic: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/OptionM.20and.20DecEq/near/236380370

[Sebastian Ullrich]

The underlying cause is that class projections are not reducible. It works with

attribute [reducible] CountParts_.α

[cognivore]

Wow, thank you, Sebastian! That's an interesting thing to learn about for me as a beginner :bow: