[Agda] What to do when Rewrite fails?

[Joey Eremondi]

I'm in a situation where I'm using "agda --without k", and I'm working with
a with decidable equality.

In my proofs, a bunch of normalizations are stuck on "decEq i i". I have a
proof of the form "uipDec : \forall i -> decEq i i \equiv yes refl", but
when I try to "rewrite uipDec", I get:

decEq i i != lhs of type Dec (i ≡ i)
when checking that the type decEq i i != lhs of type Dec (i ≡ i)
when checking that the type ... of the generated with function is
well-formed

I'm wondering, is there a way to manually do the rewrite? The problem is
that "decEq i i" doesn't actually appear in the type, it's just what the
evaluation gets stuck on, so I don't think I can use subst. Basically,
other than rewrite (which is failing), I don't know how to tell Agda the
value of a term that normalization is stuck on.

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200306/c434df95/attachment.html>