sneaky fin cast rant

Stream: new members

[Alex Meiburg]

<rant> I can't believe this was allowed to compile.

def garbage : (Fin 10 → List ℕ) → List ℕ :=
  fun f => f 37

After a long while digging I learned that there's an implicit cast of 37 to Fin 10 using Fin.ofNat' which just uses 37 % 10. But that is very hidden, and unless you have used Fin.ofNat' deliberately before, that seems easy to miss!

While this isn't exactly a "bug", it seems like the kind of sneaky error that could easily lead to a bad theorem. That is... with a formal theorem prover, of course we should only have to trust the core + the theorem statement. But this kind of sneaky and surprising implicit cast seems like the kind of thing that could easily lead to an incorrect theorem statement.
</rant>

[Mario Carneiro]

It would be possible to have Fin numerals only compile if they were less than the max value. The problem is that we want Fin n to be a ring, and we want rings to have arbitrary numerals

[Kevin Buzzard]

Not everybody wants Fin n to be a ring! That's the point of ZMod n. Like Alex I think our design decisions here have been very weird. Note that Fin 0 isn't a ring, which makes things even more confusing.

[Kevin Buzzard]

Now numerals work completely differently we can have the thing that we actually want (3 : Fin 10 working) without having to also allow the thing that far fewer people seem to want (37 : Fin 10 working) and which drove the community to define an addition on Fin n in the first place.

[Eric Wieser]

Maybe the ring instance is used rarely enough that we can put it behind an open scoped?

[Eric Wieser]

When using Fin (2 ^ n) (docs#Std.BitVec, UInt64, etc) we definitely want it to be a ring, but those files could happily open the scope

[Joseph Myers]

Fin n is used for indices where informal mathematics would have indices from 1 to n, and it's very common in such informal mathematics for out-of-range indices to be considered mod n. I think allowing 37 in Fin 10, and having it at least be an additive group, is entirely consistent with this informal usage (this is nothing like the case of junk values from e.g. division by zero, which is not common in informal usage), even if the full ring structure is less common.