[Agda] primes

[Ruben Henner Zilibowitz]

Hi. I'm using Agda 2.2.4 on Emacs. Here is a module I wrote:

-------------

module Test where

open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation
open import Data.Fin using (fromℕ≤)
open import Relation.Nullary
open import Data.Product

-- Prime m is inhabited iff m is a prime number.
Prime : (m : ℕ) → Set
Prime 0 = ⊥
Prime 1 = ⊥
Prime m = forall {i} → i < m → i ∣ m → i ≡ 1

sn≢0 : ∀ {n} → (suc n) ≢ 0
sn≢0 ()

2-prime : Prime 2
2-prime (s≤s z≤n) 0|2 = contradiction (0∣0 0|2) sn≢0
2-prime (s≤s (s≤s z≤n)) _ = refl

exPrimes : ∃ Prime
exPrimes = 2 , 2-prime

-------------

It chokes on the last line with the error:

/Users/rhz/Documents/dev/Agda/Test.agda:26,16-23
(_27 < suc (suc 0) → _27 ∣ suc (suc 0) → _27 ≡ 1) !=
({i : ℕ} → i < suc (suc 0) → i ∣ suc (suc 0) → i ≡ 1)  
because one
is an implicit function type and the other is an explicit function
type
when checking that the expression 2-prime has type Prime 2

Could someone explain this error to me?

Thanks,

Ruben