Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PANIC at Lean.Expr.fvarId! Lean.Expr:1068:14: fvar expected #1705

Closed
dwrensha opened this issue Oct 7, 2022 · 0 comments
Closed

PANIC at Lean.Expr.fvarId! Lean.Expr:1068:14: fvar expected #1705

dwrensha opened this issue Oct 7, 2022 · 0 comments

Comments

@dwrensha
Copy link
Contributor

dwrensha commented Oct 7, 2022

lean panics on the following input:

class S (R : T u) M : R
$ ~/src/lean4/build/release/stage1/bin/lean panic.lean
PANIC at Lean.Expr.fvarId! Lean.Expr:1068:14: fvar expected
backtrace:
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x32e9dac)[0x7f42f7ae9dac]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0xc4)[0x7f42f7aea114]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6+0x3b)[0x7f42f645828b]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__3+0x261d)[0x7f42f645dded]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__4+0x103e)[0x7f42f645f02e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_5+0xe93)[0x7f42f7afcae3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLCtx___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__3___rarg+0x47)[0x7f42f69b01c7]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__5+0xa8f)[0x7f42f643aa8f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xc39)[0x7f42f7b02239]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0xb88)[0x7f42f7b03c28]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg+0x34)[0x7f42f641e554]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView+0x8ac)[0x7f42f646074c]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__2+0x467)[0x7f42f64650e7]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__2___boxed+0xf7)[0x7f42f6465e97]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xfe0)[0x7f42f7b025e0]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb6a)[0x7f42f7b0216a]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBindersAux_loop___rarg___boxed+0x25)[0x7f42f69c6eb5]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb27)[0x7f42f7b02127]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xc39)[0x7f42f7b02239]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_6+0xcc2)[0x7f42f7afe5e2]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__3___rarg+0x92)[0x7f42f62bd862]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBinderViews_loop___rarg+0x64a)[0x7f42f69c386a]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBindersAux___rarg+0x2f)[0x7f42f69c6f1f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7f42f7b00515]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg+0xac)[0x7f42f629a0fc]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x93d)[0x7f42f7b000cd]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0x143)[0x7f42f62bdda3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb6a)[0x7f42f7b0216a]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_6+0xcc2)[0x7f42f7afe5e2]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__3___rarg+0x92)[0x7f42f62bd862]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0xa2e)[0x7f42f62be68e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit___rarg+0x35f)[0x7f42f62bf60f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7f42f7b00569]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withLevelNames___rarg+0x1c1)[0x7f42f62b6441]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__3___boxed+0xe3)[0x7f42f64679d3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x10d7)[0x7f42f7b00867]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__4___boxed+0xe3)[0x7f42f6467ed3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x10d7)[0x7f42f7b00867]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xc5e)[0x7f42f7b003ee]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runTermElabM___rarg___lambda__1___boxed+0x21)[0x7f42f63ea6c1]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0xae7)[0x7f42f7b03b87]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runTermElabM___rarg___lambda__2___boxed+0x21)[0x7f42f63eb5b1]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0x9e4)[0x7f42f7b01fe4]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7f42f7b00515]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg+0xac)[0x7f42f629a0fc]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x93d)[0x7f42f7b000cd]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0x143)[0x7f42f62bdda3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit___rarg+0x35f)[0x7f42f62bf60f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7f42f7b00569]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withSaveInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__1___rarg+0x2c0)[0x7f42f63e4f00]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1+0x1b)[0x7f42f63e5f2b]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7f42f7b00569]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_TermElabM_run___rarg+0x257)[0x7f42f62990e7]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_liftTermElabM___rarg+0x49c)[0x7f42f63e669c]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure___lambda__7+0x125)[0x7f42f6469385]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabStructure+0x8b7)[0x7f42f646a447]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x110e)[0x7f42f7af926e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Command_withMacroExpansion___spec__1___rarg+0x1fe)[0x7f42f63d091e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing+0x222)[0x7f42f63d1f02]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x10c6)[0x7f42f7af9226]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x10ee)[0x7f42f7af924e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2+0x57)[0x7f42f63d5497]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabCommandTopLevel___lambda__2+0x340)[0x7f42f63ddc60]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend+0x1f5)[0x7f42f6558585]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed+0x16)[0x7f42f6559076]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x13c7)[0x7f42f7af59e7]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0x14)[0x7f42f56f6c44]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0x11)[0x7f42f56f6d91]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x1268)[0x7f42f7af5888]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_profileit+0x9f)[0x7f42f7a08b2f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x59)[0x7f42f56f6e29]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommand+0xc0d)[0x7f42f655be6d]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommands+0x5e)[0x7f42f655ccbe]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_IO_processCommands+0xf6)[0x7f42f655d1e6]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_runFrontend___lambda__2+0x33)[0x7f42f655e623]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_run_frontend+0x4de)[0x7f42f655fa5e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x3196823)[0x7f42f7996823]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_main+0x29c5)[0x7f42f799a1b5]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90)[0x7f42f4429d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80)[0x7f42f4429e40]
/home/dwrensha/src/lean4/build/release/stage1/bin/lean(_start+0x25)[0x560b9c666095]
panic.lean:1:13: error: function expected at
  T
term has type
  ?m.3
panic.lean:1:18: error: expected command
$ ~/src/lean4/build/release/stage1/bin/lean --version
Lean (version 4.0.0, commit 5c7cf7657580, Release)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant