[Agda] rewriting and parameterized modules

[Ambrus Kaposi]

Hi Agda Developers,

I don't understand why the following module doesn't typecheck. The error is

β  is not a legal rewrite rule, since the left-hand side  f a  reduces
to  f a  when checking the pragma REWRITE β

If I remove the X parameters from the m1 and m2 modules, it works. It
also works when m1 and m2 are merged. But I'd like to use separate
parameterised modules.

What is the explanation for this behaviour?

Many thanks,
Ambrus




{-# OPTIONS --rewriting #-}

module a where

postulate
  _~_ : {A : Set} → A → A → Set

{-# BUILTIN REWRITE _~_ #-}

module m1 (X : Set) where

  postulate
    A B : Set
    a : A
    b : B
    f : A → B

module m2 (X : Set) where

  open m1 X

  postulate
    β : f a ~ b

  {-# REWRITE β #-}