Using derived `decEq` on inductive datatypes fails

[rvs314]

I'm trying to derive a DecEq instance on an inductive datatype, but it seems to fail (it causes the Idris2 process to eat all of my ram and get killed by the OS). Here is the code I used:

import Decidable.Equality
import Generics.Derive

%language ElabReflection
      
data Term = Zero | Next Term

%runElab derive "Term" [Generic, DecEq]

Running this isn't an issue, but trying to run decEq Zero Zero is what causes the failure. Is this an error on my part, or can this be recreated?

[jmanuel1]

Does it work if you add Meta to the list [Generic, DecEq]?