Env.idr

module Env
import Data.List

||| Proof that the list doesn't contain the element
data NotElem : k -> List k -> Type where
  NotElemNil : NotElem k []
  NotElemCons : (k = k' -> Void) -> NotElem k ks -> NotElem k (k' :: ks)

-- just to check ourselves...
proveNotElem : NotElem k ks -> Elem k ks -> Void
proveNotElem (NotElemCons f x) Here = f Refl
proveNotElem (NotElemCons f x) (There z) = proveNotElem x z

data Env : {kt:Type} -> List kt -> (a : Type) -> Type where
  Empty : Env [] a
  Insert : (k:kt) -> a ->
           {auto notElemProof : NotElem k ks} ->
           Env ks a -> Env (k::ks) a

myenv : Env ["b"] Int
myenv = Insert "b" 1 Empty

myenv2 : Env ["a", "b"] Int
myenv2 = Insert "a" 2 $ Insert "b" 1 Empty
{-
Error:
Can't solve goal NotElem "a" ["b"]
-}