[Agda] another possible without-K problem

[Andreas Abel]

On 10.07.2013 11:56, Altenkirch Thorsten wrote:
> This looks like a bug – please add it to the bug tracker.

I added this as issue 881.

> We really need to understand what we are doing when checking wether
> pattern satisfy the —without-K condition. It seems that Conor's work on
> translating pattern matching to eliminators (with J and K) would be a
> good starting point.

Could not agree more!

> At the same time we know that many types support UIP by structure.
> Michael Hedberg showed that all types with a decidable equality support
> UIP and it is not hard to see that this can be extended to stable
> equality (non-not closed). (Little puzzle: without extensionality – are
> there any types which have stable but not decidable equality ?)

What was "non-not closed" again?

> We also want to quantify over all HSets (I.e. types with UIP) and so on.

> From: Jason Reed <jcreed at gmail.com <mailto:jcreed at gmail.com>>
> Date: Tue, 9 Jul 2013 16:31:22 +0100
> To: "agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>"
> <agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>>
> Subject: [Agda] another possible without-K problem
>
>     I'm experiencing something that I think is a violation of the intent
>     of the --without-K flag, similar to what Thorsten was talking about
>     in https://lists.chalmers.se/pipermail/agda/2012/004104.html.
>
>     The following file checks fine for me under current darcs Agda:
>
>     <<<begin>>>
>     {-# OPTIONS --without-K #-}
>
>     module Test where
>
>     data S1 : Set where
>          base : S1
>
>     module test where
>         data _≡_ {A : Set} (a : A) : A → Set where
>          refl : a ≡ a
>
>         bad : (p q : base ≡ base) -> p ≡ q
>         bad refl refl = refl
>
>     module test2 where
>         data _≡_ {A : Set} : A → A → Set where
>             refl : {x : A} → x ≡ x
>
>         bad : (p q : base ≡ base) -> p ≡ q
>         bad refl refl = refl
>     <<<end>>>
>
>     Note that this covers both the possible definitions of the identity
>     type mentioned by Guillaume in
>     https://lists.chalmers.se/pipermail/agda/2012/004105.html
>
>     Any ideas what should be done here? Does the K-check need to be
>     further strengthened when there aren't parameters around? Am I
>     misunderstanding something trivial?
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete
> it.   Please do not use, copy or disclose the information contained in
> this message or in any attachment.  Any views or opinions expressed by
> the author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
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/