[Agda] Instance arguments for parametrized modules

[Andreas Abel]

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 <mailto:andreas.abel at ifi.lmu.de>
>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>

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