Why does Idris think my type parameter k is of type Type?

Question

Sorry I couldn't think of a less confusing way to put this.

I'm trying to build something like a map that can be safely accessed without returning a maybe, because all of its keys are contained in its type and querying for a key that isn't contained in its list of keys will throw a type error.

data SafeMap : (keys : List k) -> Type -> Type where
    Nil : SafeMap [] v
    (::) : Pair k v -> SafeMap ks v -> SafeMap (newKey :: ks) v

empty : SafeMap Nil v
empty = Nil

add : k -> v -> SafeMap ks v -> SafeMap (k :: ks) v
add k v l = (k,v) :: l

myDict : SafeMap ["test"] Nat
myDict = add "test" 234 Nil
--       ^^^^^^^^^^^^^^^^^^^ error here

The error message is

While processing right hand side of myDict. When unifying:
    SafeMap [?k] Nat
and:
    SafeMap [fromString "test"] Nat
Mismatch between: Type and String.

Why does it think that ?k is of type Type?

By contrast, if I replace k with an explicit String everything works and there's no type error.

data SafeMap : (keys : List String) -> Type -> Type where
--                          ^^^^^^ changed here
    Nil : SafeMap [] v
    (::) : Pair k v -> SafeMap ks v -> SafeMap (newKey :: ks) v

empty : SafeMap Nil v
empty = Nil

add : (k : String) -> v -> SafeMap ks v -> SafeMap (k :: ks) v
--         ^^^^^^ and here
add k v l = (k,v) :: l


myDict : SafeMap ["test"] Nat
myDict = add "test" 234 Nil
-- No error here! ^

Answer 1

Your mistake is here:

add : k -> v -> SafeMap ks v -> SafeMap (k :: ks) v

You want:

add : (k : _) -> v -> SafeMap ks v -> SafeMap (k :: ks) v

In (v : t) ->, v is the name of an argument of type t.