[Agda] skipped ambiguity?

[Andreas Abel]

On 06.11.2012 12:04, Serge D. Mechveliani wrote:
> People,
> the checker (in  Agda-2.3.0.1, MAlonzo, lib-0.6)
> reports a strange thing for the program
>
> ------------------------------------------------------------------------
> open import Algebra
>       using ( Semigroup; module Semigroup;   Monoid; module Monoid;
>               CommutativeMonoid; module CommutativeMonoid;
>               CommutativeRing;   module CommutativeRing;
>               Semiring; module Semiring;
>               CommutativeSemiring; module CommutativeSemiring
>             )
> ...
> record LeftQuotient {c l : Level} (H : Semigroup c l)
>                      (a b : Semigroup.Carrier H) :  Set (max c l)
>    where
>    open Semigroup {{...}}
>    field quot      : Semigroup.Carrier H
>          quotProof : (quot * b) \~~ a
>
> data MbDivideLeft {c l : Level} (H : Semigroup c l)
>                    (a : Semigroup.Carrier H) (b : Semigroup.Carrier H) :
>                                                             Set (max c l)
>    where
>    quot       : LeftQuotient H a b -> MbDivideLeft H a b
>    noQuotient :
>             let open Semigroup {{...}}
>             in
>             (x : Carrier H) -> \neg ((x * b) \~~ a) -> MbDivideLeft H a b
> ------------------------------------------------------------------------

Since you have not attached the complete source, I cannot try it, but

   (x : Carrier {{ H }})

should also work, or maybe even

   (x : Carrier)

> Here I replace the math symbols as   Level.\sqcup -> max,  \. -> *,
>
> It reports on the _last line_:
>
>    Set c  should be a function type, but it isn't
>    when checking that  H  are valid arguments to a function of type
>    Set c

Set c is the type of Carrier {{_}}, it cannot be applied to H.

> Changing  Carrier  to  Semigroup.Carrier  in the last line makes it work.
> So the impression is that the name  `Carrier'  is ambiguous.

No, the "let open" statement has the effect of defining

   Carrier {{H}} = Semigroup.Carrier H

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/