Compiler IR Check Failed vs Failed to compile Definition

Stream: mathlib4

[Gareth Ma]

These two codes give different error messages but I think they should give the same? Or is there something imported that changes the error. If so, I don't understand why :/

import Mathlib.NumberTheory.Divisors
/- To show it exists -/
example : (Finset.Ico 3 5).toList = (Finset.Icc 3 4).toList := rfl

#check Finset.toList
#check (Finset.Ico 3 5).toList
#eval (Finset.Ico 3 5).toList
/-
▶ 9:1-9:30: error:
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Finset.toList', and it does not have executable code
-/

vs

import Mathlib.Data.Nat.Interval
/- To show it exists -/
example : (Finset.Ico 3 5).toList = (Finset.Icc 3 4).toList := rfl

#check Finset.toList
#check (Finset.Ico 3 5).toList
#eval (Finset.Ico 3 5).toList
/-
▶ 9:1-9:30: error:
compiler IR check failed at '_eval', error: unknown declaration 'Finset.toList'
-/

[Damiano Testa]

I am not sure why this is happening, but this is a slight minimisation:

import Mathlib.NumberTheory.Divisors

-- comment this instance to change the error in the `#eval` below
instance : LocallyFiniteOrder ℕ := inferInstance

#eval (Finset.Ico 3 4).toList