0d7e76ea88
This PR fixes a compiler panic when a structure constructor receives a noncomputable instance as an instance-implicit argument. The LCNF translation first visits the instance in an irrelevant position (type parameter) where `ignoreNoncomputable` is `true`, caches the result, and then reuses that cached entry in a relevant position, bypassing `checkComputable`. Adding `ignoreNoncomputable` to the cache key ensures the two contexts do not share cache entries. Fixes #13371
13 lines
543 B
Text
13 lines
543 B
Text
-- Regression test for https://github.com/leanprover/lean4/issues/13371
|
|
-- The LCNF cache must distinguish entries cached in irrelevant positions
|
|
-- (where noncomputable uses are tolerated) from those in relevant positions.
|
|
structure Hom [Inhabited Unit] where
|
|
toFun : Unit
|
|
|
|
noncomputable instance inst : Inhabited Unit := ⟨Classical.choice ⟨()⟩⟩
|
|
|
|
/--
|
|
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'inst', which is 'noncomputable'
|
|
-/
|
|
#guard_msgs in
|
|
def test : Hom := ⟨default⟩
|