How dangerous is trustMe?

Viewed 406

Here's what I understand about Relation.Binary.PropositionalEquality.TrustMe.trustMe: it seems to take an arbitrary x and y, and:

  • if x and y are genuinely equal, it becomes refl
  • if they are not, it behaves like postulate lie : x ≡ y.

Now, in the latter case it can easily make Agda inconsistent, but this in itself is not so much a problem: it just means that any proof using trustMe is a proof by appeal to authority. Moreover, though you can use such things to write coerce : {A B : Set} -> A -> B, it turns out to be the case that coerce {ℕ} {Bool} 0 doesn't reduce (at least, not according to C-c C-n), so it's really not analogous to, say, Haskell's semantic-stomping unsafeCoerce.

So what do I have to fear from trustMe? On the other hand, is there ever a reason to use it outside of implementing primitives?

1 Answers
Related