design decisions around type inference and elaboration

Stream: lean4

[Jason Gross]

It seems very strange to me that I keep having to do by { exact foo } rather than foo and

let foo' := foo
foo'

rather than foo in order to get the type inferencer to accept my code. Is this a sign that I'm doing something wrong? Is this a deliberate design decision, to make let x := y in x and by { exact y } be treated differently from y?

[Kevin Buzzard]

In Lean 3, by exact X and X were elaborated in slightly different ways, meaning that sometimes one would not work but the other would. There are around 87 occurrences of by exact in mathlib, which I guess is rare given that it's now half a million lines of code.

[Mario Carneiro]

Could you say more precisely in what context foo is showing up, such that this difference is visible?

[Jason Gross]

def compose (C : Procat) {a b c : C.Obj} (f : a ~> b) (g : b ~> c) : a ~> c :=
  let f' : 1 ≈> (a ~>₁ b) := by { exact f }
  let g' : 1 ≈> (b ~>₁ c) := by { exact g }
  let f'g' := f' * g'
  let f'g'c := f'g' ⨾ C.compose
  f'g'c

works fine. Inlining f'g' into f'g'c breaks things. Inlining f'g'c breaks things. I suppose this also works:

def compose (C : Procat) {a b c : C.Obj} (f : a ~> b) (g : b ~> c) : a ~> c :=
  let f'g' := (by { exact f } : 1 ≈> (a ~>₁ b)) * (by { exact g } : 1 ≈> (b ~>₁ c))
  let f'g'c := f'g' ⨾ C.compose
  f'g'c

Replacing by { exact f } with f (and similarly for g) breaks things.

[Jason Gross]

I strongly suspect this is about typeclass resolution, perhaps around the order in which default instances are tried.