well-typed DeBrujin level

deb-lev.idr

module DBLev

import Data.List.Elem
import Decidable.Equality

%default total

-- from https://github.com/agda/agda/blob/master/test/Succeed/Issue985.agda

data Ty = A

data LupLev : Nat -> (g : List Ty) -> (a : Ty) -> Elem a g -> Type where
  LupZ :                   LupLev (length g) (a::g) a  Here
  LupS : LupLev x g a e -> LupLev x          (b::g) a (There e)

Uninhabited (LupLev x [] t e) where
  uninhabited LupZ impossible

record Lev (x : Nat) (g : List Ty) where
  constructor MkLev
  {ty : Ty}
  {el : Elem ty g}
  lev : LupLev x g ty el

Uninhabited (Lev x []) where
  uninhabited (MkLev lev) = uninhabited lev

weakLev : Lev x g -> Lev x (a::g)
weakLev (MkLev lev) = MkLev $ LupS lev

lookupLev : (x : Nat) -> (g : List Ty) -> Dec (Lev x g)
lookupLev x []     = No uninhabited
lookupLev x (a::g) = case decEq x (length g) of
  Yes Refl => Yes $ MkLev LupZ
  No ctra  => case lookupLev x g of
    Yes l    => Yes $ weakLev l
    No ctra2 => No $ \(MkLev l) => case l of
      LupZ    => ctra Refl
      LupS ll => ctra2 $ MkLev ll