Universe inconsistency issue

Sets.idr

module Sets

data Index : (xs : List a) -> Type where
  Z : Index (x :: xs)
  S : Index xs -> Index (x :: xs)

Uninhabited (Index []) where
  uninhabited (Z) impossible
  uninhabited (S _) impossible

total nth : {list:List a} -> Index list -> a
nth {list = []} Z impossible
nth {list = []} (S _) impossible
nth {list = (a :: _)} Z = a
nth {list = (_ :: xs)} (S x) = nth {list=xs} x

total top : Index (x::xs)
top = Z

total bot : Index (x::xs)
bot {xs = []} = Z
bot {xs = (x :: zs)} = S (bot {xs=zs})

data Enum : (t:Type) -> (t -> Type) -> Type where
  All : (xs : List t)
    -> ((x:t) -> p x -> (i:Index xs ** x = nth i))
    -> ((x:t) -> (i:Index xs ** x = nth i) -> p x)
    -> Enum t p

K : a -> Type
K _ = ()

index_first : Index (x::xs)
index_first = Z

index_weaken : Index xs -> Index (x::xs)
index_weaken = S

-- Obtaining universe inconsistency here
--        Old domain: (5,5)
--        New domain: (5,4)
htht : {xs:List a} -> (p : Index xs -> Type)
  -> (prf : p q)
  -> (g : (is : Index ss) -> p (nth is))
  -> (v : Index (q :: ss)) -> p (nth v)
htht p prf g Z = ?htht_rhs_1
htht p prf g (S x) = ?htht_rhs_2

lemma_select : {xs:List a} -> (ys:List a)
  -> (p:Index xs -> Type)
  -> ((x:Index xs) -> Dec (p x))
  -> (s:Index ys -> Index xs)
  -> (ss:List (Index xs))
  -> ((x:Index xs) -> p x -> Either (i : Index ss ** x = nth i) (y:Index ys ** x = (s y)))
  -> ((is:Index ss) -> p (nth is)) 
  -> Enum  (Index xs) p

lemma_select [] p f s ss eh g = All ss
  (\s, ps => case eh s ps of
    Left a => a
    Right (iy**p) => absurd iy)
  (\_, (is ** pf) => rewrite pf in g is)
lemma_select (j :: js) p f s ss eh g = case f (s Z) of
  (Yes prf) => lemma_select js p f (s . S) (s Z::ss)
    (\ix, px => case eh ix px of
      Left (xx**Refl) => Left (index_weaken xx ** Refl)
      Right (Z**ya) => Left (index_first ** ya)
      Right (S k**ya) => Right (k**ya))
    (htht p prf g)
  (No contra) => lemma_select js p f (s . S) ss ?fotuht ?fooo_2

select : (xs:List a)
  -> (p:Index xs -> Type)
  -> ((x:Index xs) -> Dec (p x))
  -> Enum (Index xs) p

-- select xs p f = lemma_select xs p f id [] (\x => absurd x)
--select [] p f = All [] (\x => absurd x) (\x => absurd x)
--select (x :: xs) p f = lemma_select id p f