[Agda] A different implementation of --without-K

[Nils Anders Danielsson]

On 2013-11-22 13:34, Jesper Cockx wrote:
> Lately I have been working on a proof of correctness for the
> --without-K flag in Agda (someone should do it, right?).

Right.

> What I'd like you to do, is:
> 1. Try out my modification on your favorite examples,

My examples are accepted. However, several of the examples under
test/fail are also accepted, for instance test/fail/WithoutK9.agda:

   module WithoutK9 where

   module Eq {A : Set} (x : A) where

     data _≡_ : A → Set where
       refl : _≡_ x

   open Eq

   module Bad {A : Set} {x : A} where

     module E = Eq x

     weak-K : {y : A} (p q : E._≡_ y) (α β : p ≡ q) → α ≡ β
     weak-K refl .refl refl refl = refl

The problem is presumably that Agda doesn't store constructor
parameters. I fixed this problem for my implementation of --without-K by
reconstructing constructor parameters (see
Agda.TypeChecking.Rules.LHS.Split.wellFormedIndices).

-- 
/NAD