Compiler inserts `instDecidableCoprime`?

Stream: lean4

[Eric Wieser]

I'm noticing something weird here:

import Batteries.Data.Nat.Gcd

set_option trace.compiler true

def test (a b : Nat) : Nat :=
  let g := a.gcd b
  if hg : g = 1 then
    g + 1
  else
    g

this emits a trace of

[compiler.input] >> test
fun a b =>
  let g := a.gcd b;
  if hg : g = 1 then g + 1 else g
[compiler.eta_expand] >> test
fun a b =>
  let g := a.gcd b;
  if hg : g = 1 then g + 1 else g
[compiler.lcnf] >> test
fun a b =>
  let _x_1 := a.gcd b;
  let _x_2 := a.instDecidableCoprime b;
  Decidable.casesOn _x_2 (fun hg => _x_1) fun hg =>
    let _x_3 := instHAdd;
    let _x_4 := _x_3.1;
    let _x_5 := instOfNatNat 1;
    let _x_6 := _x_5.1;
    _x_4 _x_1 _x_6

This seems pretty strange, because docs#instDecidableCoprime works by computing the gcd, and so here it gets computed twice.

[Henrik Böving]

I'm assuming that the tc synthesis comes up with that decidable procedure for the hg condition because it peeks into the definition of g. Not much the compiler itself can do about this.

[Eric Wieser]

Nice catch, this is not the compiler's fault after all

[Eric Wieser]

I guess the fix is perhaps to mark instDecidableCoprime @[inline}?

[Eric Wieser]

Yep, that fixes it

[Henrik Böving]

How does the output of the compiler look in the end from the old example?

[Henrik Böving]

I would have assumed it might inline the decision procedure on it's own and notice this but maybe the old compiler isn't smart enough for that

[Eric Wieser]

The final output is

def test (x_1 : @& obj) (x_2 : @& obj) : obj :=
  let x_3 : obj := Nat.gcd x_1 x_2;
  let x_4 : u8 := Nat.instDecidableCoprime x_1 x_2;
  case x_4 : u8 of
  Bool.false →
    ret x_3
  Bool.true →
    let x_5 : obj := 1;
    let x_6 : obj := Nat.add x_3 x_5;
    dec x_3;
    ret x_6

before, and

def test (x_1 : @& obj) (x_2 : @& obj) : obj :=
  let x_3 : obj := Nat.gcd x_1 x_2;
  let x_4 : obj := 1;
  let x_5 : u8 := Nat.decEq x_3 x_4;
  case x_5 : u8 of
  Bool.false →
    ret x_3
  Bool.true →
    let x_6 : obj := Nat.add x_3 x_4;
    dec x_3;
    ret x_6

after

[Henrik Böving]

Right, I'm not quite sure if this is the right fix, maybe working the instance such that this ends up resolving to just dec eq on Nat works

[Eric Wieser]

I think inlining the instance is still a good move; because it means

def test (a b : Nat) : Nat :=
  let g := a.gcd b
  if a.Coprime b then
    g + 1
  else
    g

compiles to the optimal version

[Eric Wieser]

I think I'd go as far as saying that every decidable instance of the form instance : Decidable Foo := inferInstanceAs <| Decidable Bar should be @[inline]

[Kyle Miller]

Eric Wieser said:

I guess the fix is perhaps to mark instDecidableCoprime @[inline}?

I think the fix is instead to delete Nat.instDecidableCoprime because Nat.Coprime is @[reducible], so the instance is actually Decidable (m.gcd n = 1), which is completely unnecessary.

[Kyle Miller]

Another workaround here is, but then hg needs a little work to put into a better form.

def test (a b : Nat) : Nat :=
  let g := a.gcd b
  if hg : g == 1 then
    g + 1
  else
    g

[Eric Wieser]

Ah, I missed that coprime was reducible. That explains why this is happening.

[Eric Wieser]

Inserting an id in the let is another workaround

[Eric Wieser]

Alternatively, perhaps Coprime should not be reducible

[Kyle Miller]

I'm not sure whether or not to report this as a Lean issue. Just in case, here's a Lean-only mwe.

def expensive : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * expensive n

abbrev IsExpensiveZero (n : Nat) : Prop := expensive n = 0

instance : DecidablePred IsExpensiveZero := inferInstance

set_option trace.compiler true

def f (n : Nat) : Nat :=
  let m := expensive n
  if m = 0 then
    m + 1
  else
    m + 2

/-
[compiler.lambda_pure] >> f := fun _x_1 =>
  let _x_2 := expensive _x_1;
  let _x_3 := instDecidablePredNatIsExpensiveZero _x_1;
  Bool.casesOn _x_3
    (let _x_4 := 2;
    let _x_5 := Nat.add _x_2 _x_4;
    _x_5)
    (let _x_6 := 1;
    let _x_7 := Nat.add _x_2 _x_6;
    _x_7)
-/

[Eric Wieser]

I think probably Lean itself is not to blame here, and rather it's the user's fault for creating a non-inlinable instance about an inlineable def

[Mac Malone]

The odd part here is why does one need to mark theseinstances @[inline] in the first place? Instances are supposed to be inlined by default and inferInstance / inferInstanceAs are abbrev and thus marked @[inline]. What is making the commpiler think it does not need to inline it?

[Eric Wieser]

Is there a reference for the "inlined by default" claim?

[Eric Wieser]

(the reducibility of inferInstanceAs is a distraction here, it's the decl generated by instance which doesn't reduce)

[Eric Wieser]

I've created batteries#1036 to fix this