[Agda] Defining a module by pattern matching

[Dr. ERDI Gergo]

On Wed, 15 May 2013, Guillaume Brunerie wrote:

> This looks like a good idea but I don’t see how to make it work with
> pattern matching on the identity type instead.
> The issue is that the identity type is an inductive family, so when
> pattern matching against it it will change one of the endpoints (which
> is another module argument) so Agda does not like it.

Is your equality type a valid EQUALITY built-in? Because I was able to get 
this working via 'rewrite', which requires _≡_ (or in your case, _==_) to 
be marked as the EQUALITY:

module Guillaume where

open import Relation.Binary.PropositionalEquality

module FunctionArguments where
   same-same : {A : Set} {x y : A} {P : A → Set} → x ≡ y → P x → P y
   same-same refl Px = Px

module ModuleArguments {A : Set} {x y : A} {eq : x ≡ y} where
   same-same : {P : A → Set} → P x → P y
   same-same Px rewrite eq = Px


-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
2B or not 2B, that is 0xff