[Agda] Instance arguments for parametrized modules

[Guillaume Brunerie]

Thanks Andreas, recompiling the latest version of Agda fixed the first
problem.

And thanks for reporting the other problems, I forgot there is a bug
tracker, I'll try to remember it.

Guillaume
Le 5 juil. 2012 08:37, "Andreas Abel" <andreas.abel at ifi.lmu.de> a écrit :

> Hi Guillaume,
>
> On 04.07.12 11:10 PM, Guillaume Brunerie wrote:
>
>> Are instance arguments supposed to work as arguments of parametrized
>> modules?
>>
>
> I'd say yes.
>
>  I’m asking because I just had a bug saying
>>
>>  An internal error has occurred. Please report this as a bug.
>>> Location of the error: src/full/Agda/TypeChecking/**Conversion.hs:406
>>>
>>
> Mmh, this could be related to the closed issue 670
>
>   http://code.google.com/p/agda/**issues/detail?id=670<http://code.google.com/p/agda/issues/detail?id=670>
>
> Is it possible to reconstruct this internal error?
>
>  I was trying to find a minimal example, but I got another error
>> instead which also looks like a bug in Agda.
>> The code for the second error is
>>
>>  record unit : Set where
>>>    constructor tt
>>>
>>> module A ⦃ t : unit ⦄ (i : unit) where
>>>    id : unit → unit
>>>    id x = x
>>>
>>> open A tt
>>>
>>
>> And the error message is
>>
>>  Panic: Unbound name: Bug._.id [0,8,9]@69078460
>>> when checking that tt are valid arguments to a function of type
>>> {{t : unit}} → unit → Prop
>>>
>>
>>
>>
>> Also another problem is that it does not seem possible to specify
>> explicitely instance arguments of modules. In the previous example, if
>> I replace
>>
>>  open A tt
>>>
>>
>> by
>>
>>  open A ⦃ tt ⦄ tt
>>>
>>
>> I now get the following error message:
>>
>>  {{tt}} cannot appear by itself. It needs to be the argument to a
>>> function expecting an instance argument.
>>> when scope checking {{tt}}
>>>
>>
> I reported these bugs as issue 674 on the bug tracker:
>
>   http://code.google.com/p/agda/**issues/detail?id=674<http://code.google.com/p/agda/issues/detail?id=674>
>
>  PS : I’m using Agda 2.3.1 compiled a few weeks ago
>>
>
> You might want to update to see if the fix for 670 makes a difference for
> you.
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120706/ae6671c3/attachment.html