Idris实现SafeMap时为何类型参数k被判定为Type类型

核心问题是未显式声明的泛型参数被Idris默认推断为Type种类（kind），和你实际传入的字符串值不匹配：

• 你最初定义data SafeMap : (keys : List k) -> Type -> Type时，k是未提前绑定的自由变量，Idris会自动将其识别为隐式泛型参数，默认种类为Type，等价于写了data SafeMap : {k : Type} -> (keys : List k) -> Type -> Type。这时候keys是元素为类型的列表，要求传入的键本身是类型，而不是普通值。
• 对应的add函数签名里的k也继承了这个隐式约束，第一个参数要求传入种类为Type的值（也就是需要传一个类型），但你实际传入的"test"是String类型的普通值，和要求的Type种类完全无法统一，就抛出了你看到的错误。
• 错误信息里的元变量?k就是这个未被正确指定的隐式参数，编译器默认假设它是Type，直到发现传入了String值，两边匹配失败。

另外你最初的(::)构造器还有笔误：返回类型里写的newKey在参数列表里根本不存在，应该替换成参数里的k，正确写法是(::) : Pair k v -> SafeMap ks v -> SafeMap (k :: ks) v。

当你把定义改为data SafeMap : (keys : List String) -> Type -> Type时，相当于显式指定键列表的元素类型是String（存储字符串值）：

• add的第一个参数明确要求传入String类型的值
• 类型签名里的["test"]是合法的List String值，和键列表的类型要求完全匹配
• 传入"test"作为键符合所有类型约束，自然不会报错。

如果要让SafeMap支持任意键类型而非固定为String，正确的泛型写法需要显式声明键类型参数，避免编译器默认将其推断为Type种类：

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

empty : SafeMap k [] v
empty = Nil

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

-- 使用时自动推断键类型为String，无类型错误
myDict : SafeMap String ["test"] Nat
myDict = add "test" 234 Nil

内容的提问来源于stack exchange，提问作者Aron