Hi Andreas, thanks for the clarifying explanation.<br><br>Cheers,<br><br>Carlos<br><br><div class="gmail_quote">On Mon, Jul 1, 2013 at 7:29 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Carlos,<br>
<br>
this is indeed puzzling, but it is not a bug.<br>
<br>
Module Data.Maybe defines constructor 4 times: in data types Maybe, Eq, Any, and All, so we have 4 constructors<br>
<br>
Maybe.just<br>
Eq.just<br>
Any.just<br>
All.just<br>
<br>
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.<br>
<br>
To see what goes wrong, replace the definition line by<br>
<br>
invJust refl = ?<br>
<br>
The file then type-checks, but the type (just n ≡ just m) is yellow, which indicates unresolved meta-variables.<br>
<br>
With unresolved constructors, Agda then cannot unify just n == just m and gives the error you see.<br>
<br>
A solution is to manually disambiguate:<br>
<br>
open import Data.Maybe using (Maybe; just)<br>
open import Relation.Binary.Core using (refl; _≡_)<br>
<br>
invJust : ∀ {A : Set} {n m : A} → (Maybe.just n ≡ just m) → n ≡ m<br>
invJust {A} {n} {.n} refl = refl<br>
<br>
Cheers,<br>
Andreas<br>
<br>
On 01.07.13 9:30 PM, Carlos Camarao wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi. Is the following ok, or a bug?<br>
<br>
Compiling M.agda below with "import Data.Maybe.Core using (just)" is ok<br>
(no error is detected), but<br>
compiling with "import Data.Maybe using (just)" causes an error.<br>
<br>
The error is: "Failed to infer the value of dotted pattern<br>
when checking that the pattern .n has type A"<br>
<br>
I am using agda version 2.3.0.1, on Ubuntu 12.04 LTS.<br>
<br>
Carlos<br>
<br>
=============<br>
module M where<br>
<br>
open import Data.Maybe.Core using (just) -- line 1<br>
-- open import Data.Maybe using (just) -- error<br>
(commenting line 1)<br>
open import Relation.Binary.Core using (refl; _≡_)<br>
<br>
invJust : ∀ {A : Set} {n : A} {m : A} → (just n ≡ just m) → n ≡ m<br>
invJust {A} {n} {.n} refl = refl<br>
<br>
=============<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br>