Type unification error

issue.idr.hs

module Issue

data Env : (t: Type) -> (iR: t -> Type) -> (xs: Vect t n) -> Type where
   Empty : {iR: t -> Type} -> (Env t iR Vect.Nil)
   Extend : {r:t} -> {iR: t -> Type} -> {xs: Vect t n} ->
                (res: (iR r)) -> (Env t iR xs) -> (Env t iR (r::xs))

data ElemAtIs : (i: Fin n) -> a -> Vect a n -> Type where
  ElemAtIsHere : {x: a} -> {xs : Vect a n} -> ElemAtIs fO x (x::xs)
  ElemAtIsThere : {i : Fin n} -> {x: a} -> {xs : Vect a n} ->
                    ElemAtIs i x xs -> ElemAtIs (fS i) x (y::xs)

data ResState = RState Nat Type

data Resource : ResState -> Type where
     resource : (l: Nat) -> (r:ty) -> (Resource (RState l ty))

REnv : (xs:Vect ResState n) -> Type
REnv xs = Env ResState Resource xs

envRead : {rsin: Vect ResState n} -> (REnv rsin) ->
    (ElemAtIs i (RState (S k) ty) rsin) -> ty
envRead (Extend (resource l val) rsin) ElemAtIsHere = val
envRead (Extend r rsin) (ElemAtIsThere foo) = envRead rsin foo

Failure:

*Issue> :reload
Type checking ./Issue.idr
Issue.idr:23:Can't unify ElemAtIs (fO) x (Prelude.Vect.:: x xs) with
ElemAtIs i (RState (S k) A) (Prelude.Vect.:: (RState l ty) xs)

Specifically:
        Can't unify l with S k
*Issue> :set showimplicits
*Issue> :reload
Type checking ./Issue.idr
Issue.idr:23:Can't unify ElemAtIs {n = S {n1000}} {a = {a1000}} (fO {k = {n1000}}) {x1000}
(Prelude.Vect.:: {a = {a1000}} {n = {n1000}} {x1000} {xs1001}) with
ElemAtIs {n = S {n1001}} {a = ResState} {i1000} (RState (S {k1000}) {A0})
(Prelude.Vect.:: {a = ResState} {n = {n1001}} (RState l {ty1000}) {xs1000})

Specifically:
        Can't unify l with S {k1000}