[Agda] Instance arguments for parametrized modules

Andreas Abel andreas.abel at ifi.lmu.de
Thu Jul 5 08:37:42 CEST 2012

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


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:


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


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

More information about the Agda mailing list