[Agda] Re: wait whaaat

[Dan Licata]

I think the relevant question is "what should without-K do when the indices are
constructors?".  Note that Agda won't accept "bad" if you replace S1 and
base with a postulate or variable or make them abstract.

However, this is an important question, since we use (private) constructors to
implement higher inductive types with definitional computation rules.
I would prefer that without-K did not allow this match.  

However, even at present, a workaround is to implement higher inductives
using the "pair with (unit -> unit)"
trick that I proposed when Nisse noticed that Agda still lets you do 
an absurd match on private datatypes.  This also blocks your example.
I've attached a sample below.

BTW, did --without-K always allow matching on constructors?
I've been using an old version of Agda (2.3.0 I think) until just this week, but I
no longer have the old version or the ghc that it compiled on to test.

-Dan

{-# OPTIONS --without-K #-}                                                                                                                                                    
                                                                                                                                                                               
module Test where                                                                                                                                                              
               
record Unit : Set where
  constructor <>

data Void : Set where

data _≡_ {A : Set} (a : A) : A → Set where                                                                                                                                  
  refl : a ≡ a                                                                                                                                                               

-- simplification of how we implement HITs
module Interval where
  private 
    data I' : Set where                                                                                                                                                            
     zero' : I'
     one'  : I'

  I : Set
  I = I'

  zero : I 
  zero = zero' 

  one : I 
  one = one' 

module Bad where
  
  open Interval

  -- Agda allows a disjointness match, even though I don't want it.
  bad1 : (zero ≡ one) → Void
  bad1 ()

  -- Agda allows UIP, even though I don't want it.
  bad2 : (p : one ≡ one) → p ≡ refl
  bad2 refl = refl

module IntervalFn where
  private 
    data I' : Set where                                                                                                                                                            
     zero' : I'
     one'  : I'

    data I'' : Set where
     i'' : I' -> (Unit -> Unit) -> I''

  I : Set
  I = I''

  zero : I 
  zero = i'' zero' _

  one : I 
  one = i'' one' _

module Good where
  
  -- The presence of the function defeats the "constructors (or
  -- literals) applied to variables" check:

  open IntervalFn

  {-
  good1 : (zero ≡ one) → Void
  good1 ()
  Fails with error message
      /Users/drl/tmp/Test.agda:63,3-11
      The indices
        .Test.IntervalFn.I''.i'' .Test.IntervalFn.I'.one' (λ _ → <>)
      are not constructors (or literals) applied to variables (note that
      parameters count as constructor arguments)
      when checking that the clause good1 () has type zero ≡ one → Void
  -}

  {-
  good2 : (p : one ≡ one) → p ≡ refl
  good2 refl = refl
  Fails with error message
        /Users/drl/tmp/Test.agda:75,9-13
        The indices
          .Test.IntervalFn.I''.i'' .Test.IntervalFn.I'.one' (λ _ → <>)
        are not constructors (or literals) applied to variables (note that
        parameters count as constructor arguments)
        when checking that the pattern refl has type one ≡ one
  -}


On Jul09, Jason Reed wrote:
> 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?
> 
> 
> On Tue, Jul 9, 2013 at 11:06 AM, Jason Reed <jcreed at gmail.com> wrote:
> 
> > Nope, that doesn't help me.
> >
> > The following checks for me in fresh-from-darcs Agda 2.3.3, I'd be curious
> > if you observe anything different:
> >
> > {-# 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
> >
> >
> >
> > On Tue, Jul 9, 2013 at 11:01 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> >
> >> Also, IIRC, if you use the
> >>
> >>   data Id {A : Set} (a : A) : A -> Set where
> >>      refl : Id a a
> >>
> >> definition, no one was able to trip this bug.  It was related to
> >> the parameter/index disctinction.
> >>
> >> -Dan
> >>
> >
> >