Fwd: Agda refers to things not in scope [Re: [Agda] [ANNOUNCE] Agda 2.5.1]

[Andrew Pitts]

Andreas says

> On 19 Apr 2016, at 10:49, Andreas Abel <abela at chalmers.se> wrote:
>
> Andy, Haskell is no better:
>
….
>
> With dependent types, you need to refer to things which are not in scope (unless you force the user to reimport recursively everything that is mentioned in any imported type).
>
> Or what would be your suggestion?

and Thorsten says

> On 19 Apr 2016, at 11:14, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>
> On 19/04/2016, 08:54, "agda-bounces at lists.chalmers.se on behalf of Andrew
> Pitts" <agda-bounces at lists.chalmers.se on behalf of
> Andrew.Pitts at cl.cam.ac.uk> wrote:
>
>> Thanks for that explanation. I can¹t say I find this aspect of Agda¹s
>> behaviour desirable.
>
> Maybe I misunderstand you but it seems completely reasonable that you can
> define a module without opening it. You just need to use the qualified
> names instead of merging the name space. Not only Agda is doing this.

and Andy replies:

I don’t disagree with either of those comments. But what I meant is
that the few definitions in Agda.Primitive are so, well, primitive to
the rest of Agda, that I was expecting their names (Level, lzero, lsuc
and _⊔_) to be available to me automatically without having to
remember the incantation “open import Agda.Primitive”. But I can live
with it!

(The other issue is that despite some years using Agda, I had not got
my head around exactly where one can and where one cannot use “{arg}”
instead of “{arg:_}”.)

Andy