Bug with higher order List

Stream: lean4

[Paul Mure]

This following minimum example crashes Lean4:

def listify (tys : List Type) : List Type :=
  tys.map (λ ty => List ty)

I think this should type check just fine. But Lean gave the following error:

Lean (version 4.0.0, commit ec941735c80d, 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 List.{0}

[Eric Wieser]

It works fine if you add noncomputable (i.e., the crash is in the compiler, but I guess you can see that in the message)

[Henrik Böving]

  7 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7f746091743e]
  8 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normLetValueImp+0x110)[0x7f745ff7ef00]
  9 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Internalize_internalizeLetDecl+0x1aa)[0x7f745ff4b7aa]
 10 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Internalize_internalizeCode+0x6f)[0x7f745ff4c95f]
 11 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Internalize_internalizeCode___spec__3+0x277)[0x7f745ff4f397]
 12 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Internalize_internalizeCode+0x1719)[0x7f745ff4e009]
 13 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go+0xcb7)[0x7f74600df007]
 14 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_mkSpecDecl+0x2ea)[0x7f74600e046a]
 15 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3+0x652)[0x7f74600e72f2]
 16 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__4+0xc67)[0x7f74600e9047]
 17 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5+0x720)[0x7f74600e98b0]
 18 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__6+0x715)[0x7f74600ea225]
 19 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__7+0x25b)[0x7f74600eac5b]
 20 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f+0x26d)[0x7f74600eb17d]
 21 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_visitCode+0x17a)[0x7f74600e3dda]
 22 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Specialize_main+0x4c9)[0x7f74600ef989]
 23 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_Decl_specialize+0x111)[0x7f74600f0b81]
 24 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_specialize___elambda__1___spec__1+0x1a0)[0x7f74600f1030]
 25 /home/nix/.elan/toolchains/leanprover--lean4---4.0.0/bin/../lib/lean/libleanshared.so(l_Lean_Compiler_LCNF_specialize___elambda__1+0x245)[0x7f74600f1595]

it's a bug in the specializer

[Henrik Böving]

def listify (tys : List Type) : List Type :=
  tys.map id

Further minimised

[Paul Mure]

Does anyone know if there is an existing issue filed already?

[Paul Mure]

Looks like it is alredy an active issue.