compiler IR check failed

Stream: lean4

[Michael Stoll]

import Mathlib.RingTheory.AdjoinRoot
import Mathlib.RingTheory.IntegrallyClosed

open Polynomial AdjoinRoot

noncomputable
def test {F R : Type*} [CommRing F] [IsDomain F] [IsIntegrallyClosed F]
    [CommRing R] [IsDomain R] [Algebra F R] [NoZeroSMulDivisors F R] {x : R} (hx : IsIntegral F x) :
    Algebra.adjoin F ({x} : Set R) ≃ₐ[F] AdjoinRoot (minpoly F x) := by
  refine AlgEquiv.symm <| AlgEquiv.ofBijective (Minpoly.toAdjoin F x) ?_
  sorry

#check minpoly

Commenting out noncomputable gives the error

compiler IR check failed at 'test._rarg', error: unknown declaration 'minpoly'

I think there should be the usual error message suggesting to mark the definition as noncomputable, so it appears that this is a bug.

[Kevin Buzzard]

Is this lean4#1785 ?

[Michael Stoll]

Very likely, minpoly is noncomputable...

[Shaopeng]

Yet another instance involving FirstOrder.Language.Formula.varFreeFinset and Finset.toList, the latter of which is noncomputable. Will comment at lean4#1785 as well.

import Mathlib.ModelTheory.Basic
import Mathlib.ModelTheory.Syntax
import Mathlib.Data.Finset.Basic
set_option linter.unusedVariables false

open FirstOrder List Finset
def freeVarFinset_Equal_Min {𝓛: Language}(β : Type ut)[DecidableEq β](φ: 𝓛.Formula β)(t1 t2: 𝓛.Term β)
  : 𝓛.Formula (β)
  :=
  match φ.freeVarFinset.toList with
    | nil => Language.Term.equal t1 t2
    | List.cons a l => Language.Term.equal t2 t1

/- cf. Weirdly the following works. Note the only diff is the order of terms in the last line,
    making the match essentially uniform. -/
def freeVarFinset_Equal_Min2 {𝓛: Language}(β : Type ut)[DecidableEq β](φ: 𝓛.Formula β)(t1 t2: 𝓛.Term β)
  : 𝓛.Formula (β)
  :=
  match φ.freeVarFinset.toList with
    | nil => Language.Term.equal t1 t2
    | List.cons a l => Language.Term.equal t1 t2