<p>Thanks Andreas, recompiling the latest version of Agda fixed the first problem.</p>
<p>And thanks for reporting the other problems, I forgot there is a bug tracker, I'll try to remember it.</p>
<p>Guillaume</p>
<div class="gmail_quote">Le 5 juil. 2012 08:37, "Andreas Abel" <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> a écrit :<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Guillaume,<br>
<br>
On 04.07.12 11:10 PM, Guillaume Brunerie wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Are instance arguments supposed to work as arguments of parametrized modules?<br>
</blockquote>
<br>
I'd say yes.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I’m asking because I just had a bug saying<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
An internal error has occurred. Please report this as a bug.<br>
Location of the error: src/full/Agda/TypeChecking/<u></u>Conversion.hs:406<br>
</blockquote></blockquote>
<br>
Mmh, this could be related to the closed issue 670<br>
<br>
<a href="http://code.google.com/p/agda/issues/detail?id=670" target="_blank">http://code.google.com/p/agda/<u></u>issues/detail?id=670</a><br>
<br>
Is it possible to reconstruct this internal error?<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I was trying to find a minimal example, but I got another error<br>
instead which also looks like a bug in Agda.<br>
The code for the second error is<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
record unit : Set where<br>
constructor tt<br>
<br>
module A ⦃ t : unit ⦄ (i : unit) where<br>
id : unit → unit<br>
id x = x<br>
<br>
open A tt<br>
</blockquote>
<br>
And the error message is<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Panic: Unbound name: Bug._.id [0,8,9]@69078460<br>
when checking that tt are valid arguments to a function of type<br>
{{t : unit}} → unit → Prop<br>
</blockquote>
<br>
<br>
<br>
Also another problem is that it does not seem possible to specify<br>
explicitely instance arguments of modules. In the previous example, if<br>
I replace<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
open A tt<br>
</blockquote>
<br>
by<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
open A ⦃ tt ⦄ tt<br>
</blockquote>
<br>
I now get the following error message:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
{{tt}} cannot appear by itself. It needs to be the argument to a<br>
function expecting an instance argument.<br>
when scope checking {{tt}}<br>
</blockquote></blockquote>
<br>
I reported these bugs as issue 674 on the bug tracker:<br>
<br>
<a href="http://code.google.com/p/agda/issues/detail?id=674" target="_blank">http://code.google.com/p/agda/<u></u>issues/detail?id=674</a><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
PS : I’m using Agda 2.3.1 compiled a few weeks ago<br>
</blockquote>
<br>
You might want to update to see if the fix for 670 makes a difference for you.<br>
<br>
Cheers,<br>
Andreas<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</blockquote></div>