Something wrong with my dependent types

Even.idr

data Even = E Nat
data Odd = O Nat

data Num = Ev Nat | Od Nat

NumType : Num -> Type
NumType (Ev k) = Even
NumType (Od k) = Odd

mkEven : Nat -> Num
mkEven x =  case (x `mod` 2) == 0 of
                 True => Ev x
                 False => Od x

thing : Nat -> Type
thing = NumType . mkEven

isEven: (x : Nat) -> thing x -> String
isEven Z y = "even"
isEven (S k) y = ?isEven_rhs_1