[Agda] skipped ambiguity?

[Serge D. Mechveliani]

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

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

Changing  Carrier  to  Semigroup.Carrier  in the last line makes it work.
So the impression is that the name  `Carrier'  is ambiguous. 
Then, why the checker does not report of this?
May be, it sets silently some other value for Carrier?

Thanks,
Sergei.