Idris can't fill in obvious implicit argument

Map.idr

module Map

%access public export
%default total

||| A Map structured basically as an association list
data Map : (key : Type) -> (value : Type) -> Type where
    Empty  : Map k v
    Insert : k -> v -> Map k v -> Map k v

||| A datatype for wittnesses that a given key is in a given map
data HasKey : k -> Map k v -> Type where
    Here : HasKey key (Insert key val map)
    Next : HasKey key map -> HasKey key (Insert key' val map)

||| It doesn't make sense to have a HasKey wittness for an empty map that doesn't have any keys
implementation Uninhabited (HasKey {k} x Empty) where
    uninhabited Here impossible
    uninhabited (Next p) impossible

empty : Map k v
empty = Empty

||| A Proof that, if we search for a key and can't find it in 'map', we won't be able
||| to find it in the same map, after we inserted a key 'irrelevantKey' that is not
||| the key searched for.
insertIrrelevant : { searchKey, irrelevantKey : k } -> { map : Map k v }
    -> Not (HasKey searchKey map) -- given, that a key is not in the map
    -> Not (searchKey = irrelevantKey) -- and we have a key that is not what we're looking for
    -> Not (HasKey searchKey (Insert irrelevantKey value map)) -- the key is not gonna be here after inserting an irrelevant key
insertIrrelevant searchKeyNotInMap irrelevantKeyNeqSearchKey Here = irrelevantKeyNeqSearchKey Refl
insertIrrelevant searchKeyNotInMap irrelevantKeyNeqSearchKey (Next keyInRest) = searchKeyNotInMap keyInRest

||| Find out whether a given key is in a given map
||| If the key is included, provide a HasKey wittness,
||| If not, provide a proof that a HasKey wittness is impossible
findKey : DecEq k => (key : k) -> (map : Map k v) -> Dec (HasKey key map)
findKey key Empty = No absurd
findKey key (Insert key' value map) with (decEq key key')
    findKey key (Insert key value map)    | Yes Refl = Yes Here
    findKey key (Insert notKey value map) | No keysNeq with (findKey key map)
        | Yes elsewhere = Yes (Next elsewhere)
        | No nowhere = No (insertIrrelevant nowhere keysNeq)

||| Insert a key into the map _only_ when the given key is not included
insert : (key : k) 
    -> (value : v) 
    -> (map : Map k v )
    -> { auto keyNotIncluded : Not (HasKey key map) }
    -> Map k v
insert key value map = Insert key value map

||| Update a key in a map with a function f, only when it is included
updateKey : (key : k)
    -> (f : v -> v)
    -> (map : Map k v)
    -> { auto keyIncluded : HasKey key map }
    -> Map k v
updateKey key f (Insert _ value map) {keyIncluded} with (keyIncluded)
    updateKey key f (Insert key value map)    | Here   = Insert key (f value) map
    updateKey key f (Insert notKey value map) | Next p = updateKey key f map {keyIncluded=p}
updateKey key f Empty {keyIncluded} = absurd keyIncluded

||| Remove a given key from a map that is proven to have the given key
removeKey : (key : k)
    -> (map : Map k v)
    -> { auto keyIncluded : HasKey key map }
    -> (Map k v, v)
removeKey key map {keyIncluded} with (keyIncluded)
    removeKey key (Insert key value map)    | Here   = (map, value)
    removeKey key (Insert notKey value map) | Next p =
        let (newMap, removedValue) = removeKey key map {keyIncluded = p}
        in (Insert notKey value newMap, removedValue)
removeKey key Empty impossible

testError.idr

module TestError

import Map

%default total

data Ty 
    = TyUnit
    | TyRecord (Map String Ty)

data Val : (a : Ty) -> Type where
    ValUnit : Val TyUnit
    ValRecord   : (name : String)
                -> Val t
                -> Val (TyRecord map)
                -> { auto addedUniqueName : Not (Map.HasKey name map) }
                -> Val (TyRecord (Map.insert name t map)) -- Doesn't work
                -- -> Val (TyRecord (Map.insert name t map {keyNotIncluded=addedUniqueName})) -- Works