Env.idr

module Env
import Data.List

%default total

||| 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

data Elem : k -> a -> Env ks a -> Type where
  Here : Elem k a (Insert k a e)
  There : Elem k a e -> Elem k a (Insert k' a' e)

keys : {ks : List kt} -> Env ks a -> List kt
keys {ks} _ = ks

stg.idr

module Env
import Data.List

%default total

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

data Elem : k -> a -> Env ks a -> Type where
  Here : Elem k a (Insert k a e)
  There : Elem k a e -> Elem k a (Insert k' a' e)

keys : {ks : List kt} -> Env ks a -> List kt
keys {ks} _ = ks

ldelete : Eq k => k -> List k -> List k
ldelete x [] = []
ldelete x (y :: xs) with (x == y)
  ldelete x (y :: xs) | False = y :: ldelete x xs
  ldelete x (y :: xs) | True = ldelete x xs

-- This compiles
delete : Eq kt => (k:kt) -> Env ks a -> Env (ldelete k ks) a
delete k Empty = Empty
delete k (Insert k' v e) with (k == k')
  delete k (Insert k' v e) | False = Insert k' v (delete k e)
  delete k (Insert k' v e) | True = delete k e

-- This doesn't compile
delete' : Eq kt => (k:kt) -> Env ks a -> Env (filter (/= k) ks) a
delete' k Empty = Empty
delete' k (Insert k' v e) with (k == k')
  delete' k (Insert k' v e) | False = Insert k' v (delete' k e)
  delete' k (Insert k' v e) | True = delete' k e
{-
Can't unify
        Env (k' :: filter (\{ARG1000} => ARG /= k) ks) a
with
        Env (boolElim (k' /= k)
                      (Delay (k' :: filter (\{ARG1000} => ARG /= k) ks))
                      (Delay (filter (\{ARG1000} => ARG /= k) ks)))
            a

Specifically:
        Can't unify
                k' :: filter (\{ARG1000} => ARG /= k) ks
        with
                boolElim (k' /= k)
                         (Delay (k' :: filter (\{ARG1000} => ARG /= k) ks))
                         (Delay (filter (\{ARG1000} => ARG /= k) ks))
-}