[Agda] Instance arguments for parametrized modules

[Andreas Abel]

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

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

> 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/