Panic on a noncomputable definition

[sonmarcho]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean panics on the following definition:

import Lean

def mk_arrow (x : Type × Type) : Type := x.fst → x.snd

-- Panics here
def mk_arrows (xs : List (Type × Type)) : List Type :=
  xs.map (fun x => x.fst → x.snd)

We get the following error (on Ubuntu):

Lean (version 4.0.0-nightly-2023-06-07, commit d5348dfac847, Release)
PANIC at _private.Lean.Compiler.LCNF.CompilerM.0.Lean.Compiler.LCNF.normFVarImp Lean.Compiler.LCNF.CompilerM:236:6: invalid LCNF substitution of free variable with expression fun (x : Prod.{1, 1} Type Type) => lcErased -> lcErased

Changing the definition to the following one makes the error disappear:

noncomputable def mk_arrows (xs : List (Type × Type)) : List Type :=
  xs.map (fun x => x.fst → x.snd)

[hargoniX]

@bollu and I investigated this a little bit. A note first though: This is not a panic on a noncomputable definition, this is a panic of the code generator on a funky function and you can fix it by saying that it is noncomputable which will prevent the code generator from runnning, this is why it was suggested to you.

Now to our results:

1. The stack trace of this goes into the specializer which is sadly a phase in the new code generator that I am not very familiar with it so I won't be able to pull a fix from the top of my head
2. One can construct a second issue from this that manifests a lot earlier, it is unclear to Sid and me whether this issue actually related to this one but I'll paste the example regardless:

def mk_arrows (xs : Option Type) : Option Type :=
   xs.map id

this already triggers a bug in the simplifier, namely:

[cse] size: 1
      def mk_arrows xs : Option Type :=
        let _x.1 := @Option.map _ _ _ xs;
        return _x.1 
  [] new compiler phase: base, pass: simp 
  [simp] size: 5
      def mk_arrows xs : Option Type :=
        cases xs : Option Type
        | Option.none =>
          return xs
        | Option.some val.1 =>
          let _x.2 := [anonymous] val.1;
          let _x.3 := @some _ _x.2;
          return _x.3 

after inlining the id and the Option.some it has basically forgotten about the fact that it is supposed to use id to apply that to the value inside of the some. I conjecture this is because the simplifier has noticed that the function parameter to Option.map is doing a type operation here and should thus be ignored which causes it to forget about the inlined value of id. I am again uncertain about how to precisely fix this in the simplifier since I am too not very familiar with it.

CC @leodemoura can you take a look?