Potential bug in error reporting

I observed that removing the predicate from the following example triggers no error, but the definition is not listed in the output.

define mulOne : forall a, Equality a (mul a (successor Zero)) where
      case mulOne { Zero } => reflexivity
      case mulOne { successor p } =>
        substitute { P = (x => Equality (successor p) x) } Addition.addSuccessor (
          substitute { P = (x => Equality (successor p) (successor x)) } Addition.addZero (
            congruence successor (mulOne { p })))