[Agda] Type Mismatch in with

[effectfully]

In

... with x
... | y

`x' and `y' must be of the same type (i.e. (x y : A) and not (x : y))
— just like with `case' in Haskell. Agda correctly protests that (Dec
_) is in `Set', while (yes _) and (no _) are not.

It's not possible to meaningfully define your function with this type
signature, because you can't check for equality elements of an
arbitrary type — that type must be decidable. You can either provide a
function of type (Decidable (_≡_ {A = A})) like this:

  lookupelem : { A : Set } -> Decidable (_≡_ {A = A}) -> ( a : A ) →
List' A → Maybe A
  lookupelem eq a [] = nothing
  lookupelem eq a ( x :: xs ) with eq a x
  lookupelem eq a ( x :: xs ) | yes _ = just a
  lookupelem eq a ( x :: xs ) | no _ = lookupelem eq a xs

or use instance arguments:

record DecEq {α} (A : Set α) : Set α where
  infix 5 _≟_ _==_
  field _≟_ : Decidable (_≡_ {A = A})

  _==_ : A -> A -> Bool
  n == m = ⌊ n ≟ m ⌋
open DecEq {{...}} public

lookup-for : ∀ {α β} {A : Set α} {B : Set β} {{_ : DecEq A}}
           -> A -> List (A × B) -> Maybe B
lookup-for x  []            = nothing
lookup-for x ((y , z) ∷ xs) = if x == y then just z else lookup-for x xs