Ambiguous constructors [Re: [Agda] import Data.Maybe.Core X import Data.Maybe]

[Andreas Abel]

Hi Carlos,

this is indeed puzzling, but it is not a bug.

Module Data.Maybe defines constructor 4 times: in data types Maybe, Eq, 
Any, and All, so we have 4 constructors

   Maybe.just
   Eq.just
   Any.just
   All.just

If you import (just) from Data.Maybe you get an ambiguous constructor, 
which agda cannot resolve, since your use gives not enough hints.  While 
Eq.just can be ruled out, the other three constructors are possible 
resolves of ambiguous constructor just.

To see what goes wrong, replace the definition line by

   invJust refl = ?

The file then type-checks, but the type (just n ≡ just m) is yellow, 
which indicates unresolved meta-variables.

With unresolved constructors, Agda then cannot unify  just n == just m 
and gives the error you see.

A solution is to manually disambiguate:

  open import Data.Maybe                 using (Maybe; just)
  open import Relation.Binary.Core       using (refl; _≡_)

  invJust : ∀ {A : Set} {n m : A} → (Maybe.just n ≡ just m) → n ≡ m
  invJust {A} {n} {.n} refl = refl

Cheers,
Andreas

On 01.07.13 9:30 PM, Carlos Camarao wrote:
> Hi. Is the following ok, or a bug?
>
> Compiling M.agda below with "import Data.Maybe.Core using (just)" is ok
> (no error is detected), but
> compiling with "import Data.Maybe using (just)" causes an error.
>
> The error is: "Failed to infer the value of dotted pattern
>                      when checking that the pattern .n has type A"
>
> I am using agda version 2.3.0.1, on Ubuntu 12.04 LTS.
>
> Carlos
>
> =============
> module M where
>
> open import Data.Maybe.Core            using (just) -- line 1
> -- open import Data.Maybe                 using (just) -- error
> (commenting line 1)
> open import Relation.Binary.Core       using (refl; _≡_)
>
> invJust : ∀ {A : Set} {n : A} {m : A} → (just n ≡ just m) → n ≡ m
> invJust {A} {n} {.n} refl = refl
>
> =============
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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