[Agda] Agda Observational equality using primUnsafeTrustMe?

[Conor McBride]

On 9 Jan 2011, at 02:51, Dan Doel wrote:

> On Friday 07 January 2011 7:04:49 pm Conor McBride wrote:
>> On 7 Jan 2011, at 17:05, Thorsten Altenkirch wrote:
>>> Hi Dominique,
>>>
>>> I have been thinking about something like this but didn't realize it
>>> could be done so easily. I think this is an interesting idea.
>>>
>>> It certainly breaks a number of things, e.g. subject reduction. But
>>> does it break termination?
>>
>> Since it now is tomorrow, I can confirm that, yes, it does
>> break termination.
>
> To elaborate slightly on Conor's answer, the question is roughly the  
> same as
> asking, "is it safe to erase/be lazy in equality proofs?" And the  
> answer to
> that, for open terms, is "no."

Let me give some more clues. Firstly, the condition that all  
postulates are
consistent is no talisman against error. One need merely *hypothesize* a
lie to create trouble. The world of open terms is a dangerous place  
where
all lies are true and functions from the empty type can be persuaded to
return canonical values. In that setting, an excess of trust is lethal.

All the best

Conor