Hi. Is the following ok, or a bug?<br><br>Compiling M.agda below with &quot;import Data.Maybe.Core using (just)&quot; is ok (no error is detected), but <br>compiling with &quot;import Data.Maybe using (just)&quot; causes an error. <br>
<br>The error is: &quot;Failed to infer the value of dotted pattern<br>                    when checking that the pattern .n has type A&quot;<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 (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>