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

[Carlos Camarao]

Hi Andreas, thanks for the clarifying explanation.

Cheers,

Carlos

On Mon, Jul 1, 2013 at 7:29 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> 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<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/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130702/52430da3/attachment.html