{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS -Wall -Wunticked-promoted-constructors #-}
module M where

data Val f env where
  VTop :: Val f '[]
  VPush :: f t -> Val f env -> Val f (t ': env)

data Idx env t where
  IZ :: Idx (t ': env) t
  IS :: Idx env t -> Idx (a ': env) t

prj1 :: Val f env -> Idx env t -> f t
prj1 (VPush x _) IZ = x
prj1 (VPush _ env) (IS i) = prj1 env i
prj1 VTop IZ = undefined                -- inaccessible right hand side
prj1 VTop (IS _) = undefined            -- inaccessible right hand side

prj2 :: Val f env -> Idx env t -> f t
prj2 (VPush x _) IZ = x
prj2 (VPush _ env) (IS i) = prj2 env i
prj2 VTop IZ = undefined                -- inaccessible right hand side

prj3 :: Val f env -> Idx env t -> f t
prj3 (VPush x _) IZ = x                 -- pattern match(es) are non-exhaustive
prj3 (VPush _ env) (IS i) = prj3 env i