Zulip Chat Archive
Stream: lean4
Topic: (kernel) unknown constant
Sébastien Michelland (May 24 2022 at 14:09):
I have this error, which looks like a Lean bug. It seems that the double-nested dependency is required, the class parameter (specifically a class) is required as well, and the mutual recursion in the string functions is also needed.
class Class where
instance empty: Class := {}
mutual
inductive T (δ: Class) where
| mk (ss: List (S δ))
inductive S (δ: Class) where
| mk (ts: List (T δ))
end
mutual
partial def str_T: T δ → String
| .mk ss => "\n".intercalate (ss.map str_S)
partial def str_S: S δ → String
| .mk ts => "\n".intercalate (ts.map str_T)
end
def error := str_T (T.mk (δ := empty) [])
-- (kernel) unknown constant 'str_T._at.error._spec_1'
Cc @Siddharth Bhat
Sébastien Michelland (May 24 2022 at 16:12):
Temporary workaround for us: make the str_*
functions total by not using map
.
Leonardo de Moura (May 26 2022 at 03:39):
Pushed a fix for this.
Jovan Gerbscheid (Sep 25 2024 at 11:51):
I got a similar error, which I have minimized here. It seems to be due to a problem with specializing in a mutual recursive definition. Using a single monad instead of a stack like ReaderT Unit (ReaderT Unit Id)
does work fine.
variable {m : Type → Type} [Monad m]
mutual
partial def A : m Unit := do
pure ()
B
partial def B : m Unit := do
pure ()
A
end
def oops : ReaderT Unit (ReaderT Unit Id) Unit := A
-- (kernel) unknown constant 'A._at.oops._spec_1'
From copying the implementation of ReaderT
, it seems this problem can be solved by modifying the @[inline]
annotations in the ReaderT
implementation: either add @[inline] to the instance Monad (ReaderT ρ m)
, or remove it from ReaderT.bind
.
Jovan Gerbscheid (Sep 25 2024 at 11:55):
My temporary workaround is to add the inlined instance
@[inline]
instance {m : Type → Type} {ρ : Type} [Monad m] : Monad (ReaderT ρ m) where
bind := ReaderT.bind
Kim Morrison (Sep 26 2024 at 00:47):
@Jovan Gerbscheid, could you please create an issue for this one?
Jovan Gerbscheid (Oct 08 2024 at 12:07):
Sorry for the delay, here is the issue: lean4#5651
Last updated: May 02 2025 at 03:31 UTC