partial def inf loops

Stream: lean4

[James Gallicchio]

I am encountering some weirdness with partial defs that I'm not sure is really a bug but could definitely use better error messages for.

MWE:

set_option trace.compiler.ir.result true in
partial def test : StateM Unit Unit := do
  let () ← test

The IR optimizes test to a single unreachable call, which is accurate only to the extent that test does not return... it is certainly a surprise to #eval test and crash the server instead of infinitely loop.

[James Gallicchio]

If the compiler is detecting the infinite loop and inserting unreachable, then perhaps it should be another symbol that is more descriptive than unreachable. Even a standard non-internal panic! would be much more helpful for debugging.

[Henrik Böving]

This seems to be a mis-analysis of the elim dead branches pass that does indeed not ocur in the rewrite of elim dead branches in the new code generator!

Old:

[init]
def test (x_1 : obj) : obj :=
  let x_2 : obj := test x_1;
  case x_2 : obj of
  Prod.mk →
    let x_3 : obj := proj[1] x_2;
    let x_4 : obj := ctor_0[PUnit.unit];
    let x_5 : obj := ctor_0[Prod.mk] x_4 x_3;
    ret x_5
[elim_dead_branches]
def test (x_1 : obj) : obj :=
  let x_2 : obj := test x_1;
  case x_2 : obj of
  Prod.mk →
    ⊥

New:

[Compiler.elimDeadBranches] size: 5
    def test._redArg : PUnit × PUnit :=
      let _x.1 := test._redArg;
      cases _x.1 : PUnit × PUnit
      | Prod.mk fst.2 snd.3 =>
        let _x.4 := PUnit.unit;
        let _x.5 := Prod.mk _ _ _x.4 snd.3;
        return _x.5
[Compiler.elimDeadBranches] size: 1
    def test a.1 : PUnit × PUnit :=
      let _x.2 := test._redArg;
      return _x.2

current end result of new:

[Compiler.result] size: 5
    def test._redArg : PUnit × PUnit :=
      let _x.1 := test._redArg;
      cases _x.1 : PUnit × PUnit
      | Prod.mk fst.2 snd.3 =>
        let _x.4 := PUnit.unit;
        let _x.5 := Prod.mk _ _ _x.4 snd.3;
        return _x.5
[Compiler.result] size: 1 def test a.1 : PUnit × PUnit := let _x.2 := test._redArg; return _x.2

[Henrik Böving]

I cannot tell for sure from the top of my head but I would guess that the abstract interpreter of the old pass somehow got the idea that the return value of test is bot and thus decided to eliminate the Prod.mk branch which was then later turned into just a single unreachable instrruction because "Hey there is a single branch here and we do not use its data, might as well not branch" and so on.