Idris扩展记录编译错误：合法非重复键组合触发类型不匹配

Let's break down exactly what's happening here, and why your valid record is triggering that confusing error.

First, what the error is saying #

That type mismatch boils down to one critical issue: when you try to add a new key-value pair to your record, your code expects a proof that the new key is NOT equal to existing keys (that's the ("Title" = "Year") -> Void part—Void means this equality can never be true). But instead, your implementation is producing a useless identity function type (("Title" = "Year") -> "Title" = "Year") which doesn't prove anything about inequality.

Why this is happening #

For unique-key records in Idris, we rely on dependent types to track which keys already exist (usually via a type-level list of keys). When adding a new key k, you need a constraint that proves k isn't already in that list.

Your mistake is almost certainly in how you've defined that constraint, or how your +: operator enforces it:

• Maybe you accidentally asked for a proof of equality instead of inequality in your type signature.
• Or your "key not present" type is incorrectly structured, so Idris can't derive the right proof for non-duplicate keys.

How to fix it #

Let's walk through a corrected approach to ground this:

First, define a type to represent "a key is not in a list of existing keys":

data NotElem : String -> List String -> Type where
  NotNil : NotElem k []
  NotCons : (keyNeqHead : k ≠ h) -> NotElem k tail -> NotElem k (h :: tail)

This type builds a proof recursively: a key isn't in an empty list, and it isn't in a non-empty list if it's not equal to the head AND not in the tail.

Next, define your record type and +: operator with the right constraint. We'll use auto to let Idris automatically derive the proof when possible (since String implements DecEq, Idris can check if two strings are equal/unequal for us):

-- Basic record type, tracking keys at the type level
data Record : List String -> Type where
  RNil : Record []
  RCons : (k : String) -> (valType : Type) -> Record ks -> Record (k :: ks)

-- Key-value pair helper
data (:=) : String -> Type -> Type where
  (:=) : (k : String) -> (v : Type) -> k := v

-- The extended cons operator, with unique-key enforcement
infixr 5 +:
(+:) : {k : String} -> {v : Type} -> {ks : List String} ->
       (k := v) -> Record ks -> {auto keyNotIn : NotElem k ks} -> Record (k :: ks)
(+:) (k := v) rec = RCons k v rec

With this setup:

• Your valid record ("Title" := String) +: ("Year" := Nat) +: RNil will compile automatically—Idris uses DecEq to prove "Title" ≠ "Year" and builds the NotElem proof for you.
• A duplicate key like ("Year" := String) +: ("Year" := Nat) +: RNil will fail to compile, exactly as you want, because Idris can't produce a ("Year" ≠ "Year") -> Void proof (since that equality is true).

Recapping your original issue #

Your code was asking for the wrong kind of proof. Instead of requiring evidence that the new key doesn't match any existing ones, it was somehow expecting a proof of equality (or generating an identity function instead of an inequality proof). Double-check your +: operator's type signature and any custom "key not present" types you defined—you likely mixed up equality vs. inequality in the constraints.

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