Phantom arguments in functions [Re: [Agda] another possible without-K problem]

[Guillaume Brunerie]

Thanks for the workaround!
It’s not optimal though, you have to give the silly [z] argument
everytime you use [fool] which is a bit annoying.
But this is easy to fix by making the argument [z] of [fool] an
instance argument instead of an implicit argument and by putting
somewhere in the context the following definition:

inhab-Phantom : {A : Set} {a : A} -> Phantom a Unit
inhab-Phantom = phantom unit

Then you can use [fool] just as you use [bla]:

same? : {x : Unit} → fool u1 x ≡ fool u2 x
same? = refl

gives the expected error.

Guillaume

2013/7/10 Andreas Abel <andreas.abel at ifi.lmu.de>:
> On 10.07.2013 16:54, Dan Licata wrote:
>>
>> Also, related to implementing higher inductives, but not to without-K:
>> is there a way to turn off/defeat the unused arguments analysis that is
>> new in 2.3.2.1?  It breaks some of the things I'm doing: I want a
>> function with a "phantom" parameter, where different values of the
>> phantom parameter do not automatically get equated.
>
>
> Data and record types still have phantom arguments, which can be exploited.
>
> Would this workaround help you?
>
> import Common.Level
> open import Common.Equality
>
> record Phantom {A : Set}(a : A)(B : Set) : Set where
>   constructor phantom
>   field
>     thePhantom : B
> open Phantom
>
> postulate
>   A      : Set
>   a      : A
>   Unused : Set
>   u1 u2  : Unused
>
> data Unit : Set where
>   unit : Unit
>
> bla : (u : Unused) → Unit → A
> bla u unit = a
>
> same : {x : Unit} → bla u1 x ≡ bla u2 x
> same = refl
>
> fool : (u : Unused){z : Phantom u Unit} → Unit  → A
> fool u {phantom unit} unit = a
>
> same? : ∀ {x : Unit}{y z} → fool u1 {y} x ≡ fool u2 {z} x
> same? = refl
>
> -- ERROR:
> -- u1 != u2 of type Unused
> -- when checking that the expression refl has type
> -- fool u1 .x ≡ fool u2 .x
>
>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda