PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding

Stream: lean4

[Siddharth Bhat]

Here's a test case where the compiler emits PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding expected on being invoked. I don't know if this is considered a bug since the input program should not compile due to syntax errors. I reduced the test case to a minimal example in case Lean has a policy of never panicking on malformed input.

The full error log:

/home/bollu/temp/lean-gap$ leanpkg build
configuring gap 0.1
> LEAN_PATH=././build /home/bollu/work/lean4/build/stage1/bin/lean -o build/GAP/P.olean -c build/temp/GAP/P.c ./GAP/P.lean
> LEAN_PATH=././build /home/bollu/work/lean4/build/stage1/bin/lean -o build/GAP/AST.olean -c build/temp/GAP/AST.c ./GAP/AST.lean
PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding expected
PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding expected
./GAP/AST.lean:5:29: error: unknown identifier 'Expr'
./GAP/AST.lean:7:21: error: unknown identifier 'Expr'
./GAP/AST.lean:5:6: error: fail to show termination for
  GAP.AST.parse_expr_logical
  GAP.AST.parse_expr
with errors
structural recursion does not handle mutually recursive functions

unexpected bound variable #0
external command exited with status 1
Build failed.

The minimal test case

/home/bollu/temp/lean-gap$ tree
.
├── GAP
│   ├── AST.lean
│   └── P.lean
├── GAP.lean
└── leanpkg.toml

with file contents:

-- GAP.lean
import GAP.P
import GAP.AST

-- GAP/P.lean
namespace GAP.P
structure P (a: Type) where
   runP: a
instance : Monad P := {
  pure := fun a => { runP := a },
  bind := fun a => fun a2mb => a2mb (a.runP)
}

-- GAP/AST.lean
  import GAP.P
  open GAP.P
  namespace GAP.AST
  mutual
  def parse_expr_logical : P Expr := do
    let l <- parse_expr
  def parse_expr : P Expr := parse_expr_logical
  end

# leanpkg.toml
[package]
name = "gap"
version = "0.1"
lean_version = "leanprover/lean4:master"

Link to Gist

Click here for a gist, formatted as a Lean issue

[Leonardo de Moura]

Thanks for reporting the problem. I pushed a fix for this issue.