`maximum recursion depth` error

[javra]

This causes an error

import Mathlib.Data.ZMod.Basic
open Qq

example (x : Q(ZMod <| 2^249)) : Q(Prop) := q($x = $x)

[gebner]

This is a bug in Lean itself. Qq-free MWE:

def ZMod : Nat → Type
  | 0 => Int
  | n+1 => Fin n

example (x : ZMod (2^300)) : Prop :=
  x = x -- maximum recursion depth has been reached

[gebner]

Also, I was positively surprised that I could debug this in GDB using rbreak throwMaxRecDepthAt.

[javra]

Oof, sorry, I'll post it there then. Seems like a unification problem then.