Issue3067.agda:25,27-45
Refusing to invert pattern matching of A-false because the maximum
depth (50) has been reached. Most likely this means you have an
unsatisfiable constraint, but it could also mean that you need to
increase the maximum depth using the flag --inversion-max-depth=N
when checking that the expression p _ (eternity _ n) has type
P (A-on-Nat a (suc n))
Failed to solve the following constraints:
  A-false _b_178 = a : A (blocked on _b_178)
Unsolved metas at the following locations:
  Issue3067.agda:25,27-45
