Incomprensible type for hole

[freddi301]

type at ?h4 is with block in has i conArg item item _ [] = True

namespace SetBehaviour
  public export
  interface SetBehaviour s i where
    empty : s
    has : i -> s -> Bool
    add : i -> s -> s
    rem : i -> s -> s

    has_empty : (item : i) -> (has item empty) = False
    has_add : (item : i) -> (set : s) -> has item (add item set) = True
    has_rem : (item : i) -> (set : s) -> has item (rem item set) = False

namespace MapBehaviour
  interface MapBehaviour m k v where
    empty : m
    get : k -> m -> Maybe v
    set : k -> v -> m -> m
    rem : k -> m -> m

    get_empty : (key : k) -> (get key empty) = Nothing
    get_set : (key : k) -> (value : v) -> (map : m) -> get key (set key value map) = Just value
    get_rem : (key : k) -> (map : m) -> get key (rem key map) = Nothing

    -- has : k -> m -> Bool
    -- has key map = case get key map of
    --   Just _ => True
    --   Nothing => False

Eq i => SetBehaviour.SetBehaviour (List i) i where
  empty = []
  has item [] = False
  has item (head :: tail) with (item == head)
    _ | True = True
    _ | False = has item tail
  add item list = item :: list
  rem item [] = []
  rem item (head :: tail) with (item == head)
    _ | True = tail
    _ | False = head :: (rem item tail)

  has_empty item = Refl
  has_add item [] with (item == item)
    _ | _ = ?h4
  has_add item (head :: tail) with (item == item)
    _ | _ = ?h6
  has_rem item [] = Refl
  has_rem item (head :: tail) with (item == head)
    _ | True = ?h20
    _ | False = ?h21