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

[Andreas Abel]

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/