[Agda] Trust me regarding Dan Licata's trick

[Guillaume Brunerie]

(resending without the irrelevant citations given that the Agda list
doesn’t like long emails and I don’t know if my previous email has
been sent)

On Jun 7, 2013 5:40 AM, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:
> On 06/06/13 19:57, Guillaume Brunerie wrote:
>>
>> This is a natural number which should normalise to 0 if you have
>> canonicity, but it doesn't, even if you use primTrustMe.
>> (on the other hand if you *compile* it, then it will compute to 0,
>
>
> It is a bit disturbing that the normalization for type checking is different from the normalization given by compilation for running terms.

One difference between normalization and compilation is that when you
run a program you are guaranteed to be in the empty context whereas
normalization also happens in non empty contexts.

>> but
>> combining that with univalence you can easily get a segfault)
>
>
> I want to understand this more precisely, because univalence is compatible with hpropositional truncation. Perhaps you are just saying that we cannot have all points of the truncation to be definitionally equal under univalence: the type checking is right (because it doesn't believe me when I ask to be trusted), but the compilation is wrong (for univalent foundations).

Univalence is compatible with truncation but not with primTrustMe.
PrimTrustMe is based on the fact that in the empty context the only
proof of equality should be refl, which is not compatible with
univalence.

Here is how I think you can get a segfault using the interval (I
haven't managed to actually get the segfault because I don't
understand how to compile an Agda program yet). You can probably adapt
it to truncations if you want.

Assuming univalence, the types Unit and Unit -> Unit are equivalent.
Hence there is a dependent type over I whose fiber over 0 is Unit and
whose fiber over 1 is Unit -> Unit.
Then you can take the canonical element tt of Unit, transport it along
the path of the interval (so that you get a function of type Unit ->
Unit) and apply it to tt.
What I think will happen if you try to compile it is that the path of
the interval will be compiled to refl, hence the transport is just the
identity so the program will try to apply the "function" tt to the
argument tt, which is obviously problematic.

> Anyway, if trustMe does work as a postulate as claimed earlier, why is it needed/useful at all?

My impression is that it can be used to get some unsafe coercion
between arbitrary types, like Obj.magic in OCaml.

Guillaume