changing reducibility for type class inference

Stream: lean4

[Rob Lewis]

We're facing an issue where semireducible List functions in the library are blocking type class inference, similar to this MWE:

@[reducible]
def myLength : List Nat → Nat
| [] => 0
| _::t => 1 + myLength t

#check (1 : Fin 2) -- works
#check  (1 :  Fin (myLength [3, 4])) -- works
#check  (1 :  Fin (List.length [3, 4])) -- fails

In Lean 3 I would have locally changed the reducibility of List.length but Lean 4 doesn't allow this. Is there a canonical workaround, outside of redefining the relevant functions with @[reducible]?

[Adam Topaz]

In this case you could introduce something like the following (possibly inline in the problematic decl):

instance {i} : OfNat (Fin (List.length (x :: xs))) i :=
  show OfNat (Fin (Nat.succ _)) _ from inferInstance

[Adam Topaz]

Of course that doesn't answer the actual question.

[Eric Wieser]

For this specific case you can also fix things with:

instance : NeZero (List.length <| .cons x xs) := ⟨by simp⟩

(with import Mathlib.Data.Fin.Basic)

[Rob Lewis]

Thanks. Unfortunately I'm not sure either of these translate to our actual use case :sad: We have a large class of these problems, some too long to reasonably unfold by hand, and they show up in definitions theorem statements that we expect users to write.

[Eric Wieser]

Does no_index help at all here?

[Rob Lewis]

I can't actually find any documentation about no_index, but if I understand correctly what it does, then no. (The Nat in this mwe isn't relevant.)

[Mario Carneiro]

This came up in iris-lean and it was addressed by just copy pasting all the list defs as reducible

[Jannis Limperg]

Is it even allowed to make recursive definitions reducible? I think Gabriel once told me that Lean assumes only nonrecursive definitions are reducible. The question came up in a discussion about discrimination trees, so maybe discrimination tree indexing relies on this invariant for correctness.

[Mario Carneiro]

you can put @[reducible] def on a recursive def, but not abbrev IIRC

[Gabriel Ebner]

Yes, iirc the discrimination tree module eagerly unfolds reducible definitions. So if you declare an instance for NeZero (a :: b).lengthReducible, then it wouldn't apply to NeZero (a :: b :: c).lengthReducible because the two are reduced to NeZero a.lengthReducible.succ and NeZero c.lengthReducible.succ.succ as a preprocessing step.