[Agda] rewriting and parameterized modules

[Jesper Cockx]

... aaaaaaand fixed. Have fun with rewriting.

-- Jesper

On Fri, Jun 16, 2017 at 5:47 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> This is a bug in Agda, I've added it to the issue tracker:
> https://github.com/agda/agda/issues/2606
>
> Working on a fix...
>
> -- Jesper
>
> On Fri, Jun 16, 2017 at 5:19 PM, Ambrus Kaposi <kaposi.ambrus at gmail.com>
> wrote:
>
>> 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 β #-}
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170616/cf466298/attachment.html>