ZMod maximum recursion depth

Stream: mathlib4

[Jakob von Raumer]

Has anybody come across this issue yet?

import Mathlib.Data.ZMod.Basic

example (x : ZMod 128) : ZMod (2^256) :=  x.cast  -- gives maximum recursion depth error

There's a workaround by evaulating 2^256 first, but this is pretty annoying

[Kevin Buzzard]

It's not the cast:

import Mathlib.Data.ZMod.Basic

example (x : ℕ) : ZMod (2^256) := x -- max recursion

[Jakob von Raumer]

Yes, it's the modulus

[Jakob von Raumer]

But since the issue doesn't occur when replacing ZMod by Fin, I assume that to evaluate the cast (from Nat or from wherever) it needs to evaluate the modulus to determine whether it is 0, which in turn causes the issue

[Matthew Ballard]

def Bar : Nat →  Type
  | 0 => Unit
  | _ => Unit

def foo : Bar (2^256) := .unit  -- max recursion