[Agda] Instance arguments for parametrized modules

[Andreas Abel]

This issue is fixed now, the workaround is no longer needed...

On 07.07.12 9:21 AM, Andreas Abel wrote:
> A work around to open A tt seems to be
>
> module M = A tt
> open M
>
> However, module N = A {{ tt }} tt does not pass the scope checker.
>
> Cheers,
> Andreas
>
> On 06.07.12 4:36 PM, Guillaume Brunerie wrote:
>> 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
>> <mailto: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/