[Agda] Postulated computing quotients are unsound

[Dan Licata]

Oh, good catch!  I hadn't thought about absurd patterns.  The root of
the issue seems to be that Agda won't let me *not* export the fact that
the constructors are provably disjoint.  

On the other hand, computing quotients are pretty convenient, at least
for Homotopy Type Theory stuff, and Agda seems close to supporting them.
(E.g., your counterexample doesn't apply to higher-inductive types with
only one base point, like the spheres.)

I can imagine a few ways solving this problem, in the short run:

- A heavy solution would be to add a flag --no-absurd-patterns.
  A quick grep suggests that my homotopy type theory code would compile
  with this flag.    

- A better solution would be to disable absurd patterns on a type by
  type basis.  From a certain point of view, Agda already does this, but
  only for Set---otherwise univalence would allow a similar
  counterexample.  Essentially, you only want unification failures
  between hSets to allow absurd patterns.  I'm not sure how hard this
  would be to implement, though.  Thoughts?  

Of course, I'd ultimately like primitive support for univalence and
higher inductive types. But in the short run another flag along the
lines of --without-K might be a good fix.   

Thoughts?  
-Dan

On May16, Nils Anders Danielsson wrote:
> Hi,
> 
> At the last AIM Thorsten Altenkirch, James Chapman and I experimented
> with postulated, computing quotients, perhaps inspired by Dan Licata's
> "Running Circles Around (In) Your Proof Assistant; or, Quotients that
> Compute":
> 
>   http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
> 
> We were not sure if this hack was sound or not. Now, thanks to Dan Doel,
> I know that it isn't.
> 
> 
> Quotients were defined in the following way:
> 
>   data Quotient {c ℓ} (A : Setoid c ℓ) : Set (c ⊔ ℓ) where
>     box : (x : Setoid.Carrier A) → Quotient A
> 
> To avoid direct pattern matching we didn't export the constructor, but
> only a function [_] = box. We also exported an eliminator that allowed
> you to "pattern match" as long as you proved that you respected the
> relation, as well as the following postulate, which states that [_]
> respects the relation:
> 
>   postulate
>     [_]-cong : ∀ {c ℓ} {A : Setoid c ℓ} {a₁ a₂} → let open 
>     Setoid A in
>                a₁ ≈ a₂ → _≡_ {A = Quotient A} [ a₁ ] [ a₂ ]
> 
> 
> Dan Doel pointed out [1] that certain hacks intended to emulate "higher
> inductive types" (as in Dan Licata's post mentioned above) are
> suspicious:
> 
> * Even if you hide the constructors the absurd pattern is still
>   available.
> 
> * The exported constructors compute to the real ones, also in
>   equalities. For instance, [ true ] ≡ [ false ] computes to box true ≡
>   box false.
> 
> 
> Given these observations it is easy to prove that the postulate above is
> unsound:
> 
> * Quotient Bool by the trivial relation.
> 
> * Use [_]-cong to prove that [ true ] and [ false ] are equal. Denote
>   the proof by p.
> 
> * Prove that the empty type is inhabited by using an absurd pattern:
> 
>     bad : ⊥
>     bad with p
>     ... | ()
> 
> 
> A similar approach can be used to prove that Dan Licata's encoding of
> the interval is unsound.
> 
> 
> [1] The #agda IRC channel, 2012-05-15
>     (http://agda.orangesquash.org.uk/2012/May/16.html); Dan Doel's nick
>     is dolio.
>