<div dir="ltr"><div>... aaaaaaand fixed. Have fun with rewriting.<br><br></div>-- Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jun 16, 2017 at 5:47 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>This is a bug in Agda, I've added it to the issue tracker: <a href="https://github.com/agda/agda/issues/2606" target="_blank">https://github.com/agda/agda/<wbr>issues/2606</a><br><br></div>Working on a fix...<span class="HOEnZb"><font color="#888888"><br><br></font></span></div><span class="HOEnZb"><font color="#888888">-- Jesper<br></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jun 16, 2017 at 5:19 PM, Ambrus Kaposi <span dir="ltr"><<a href="mailto:kaposi.ambrus@gmail.com" target="_blank">kaposi.ambrus@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Agda Developers,<br>
<br>
I don't understand why the following module doesn't typecheck. The error is<br>
<br>
β  is not a legal rewrite rule, since the left-hand side  f a  reduces<br>
to  f a  when checking the pragma REWRITE β<br>
<br>
If I remove the X parameters from the m1 and m2 modules, it works. It<br>
also works when m1 and m2 are merged. But I'd like to use separate<br>
parameterised modules.<br>
<br>
What is the explanation for this behaviour?<br>
<br>
Many thanks,<br>
Ambrus<br>
<br>
<br>
<br>
<br>
{-# OPTIONS --rewriting #-}<br>
<br>
module a where<br>
<br>
postulate<br>
  _~_ : {A : Set} → A → A → Set<br>
<br>
{-# BUILTIN REWRITE _~_ #-}<br>
<br>
module m1 (X : Set) where<br>
<br>
  postulate<br>
    A B : Set<br>
    a : A<br>
    b : B<br>
    f : A → B<br>
<br>
module m2 (X : Set) where<br>
<br>
  open m1 X<br>
<br>
  postulate<br>
    β : f a ~ b<br>
<br>
  {-# REWRITE β #-}<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>