## Stream: lean4

### Topic: design decisions around type inference and elaboration

#### Jason Gross (Mar 22 2021 at 21:08):

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 (Mar 22 2021 at 21:42):

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 (Mar 22 2021 at 21:55):

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

#### Jason Gross (Mar 22 2021 at 21:58):

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 (Mar 22 2021 at 21:58):

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

Last updated: May 07 2021 at 12:15 UTC