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