[Agda] trustMe and make my coercion go

[Benja Fallenstein]

Hi all,

It occurs to me that the function

> compute-dammit! : {X : Set} → {x y : X} → x == y → x == y
> compute-dammit! _ = primTrustMe

could be used to make stuck coercions go -- contrived example:

> postulate foo : Nat == Nat
>
> test : coerce (compute-dammit! foo) zero == zero
> test = refl

(I'm using --type-in-type there because Agda doesn't let me use
primTrustMe on higher levels, but that seems like a detail.)

Now I'm wondering what effect introducing compute-dammit! would have
on the metatheory: Does it destroy normalization? Consistency? It
seems like consistency should be preserved, because in a
set-theoretical model, compute-dammit! should just be the identity,
right?

Thanks,
- Benja