title: Compilation error while implementing extensible record
body: <p>I'm playing around with idris and was trying to implement extensible records. </p>
  
  <p>The main goal is to guarantee that the record's keys are unique.</p>
  
  <p>For example </p>
  
  <pre><code>("Year" := 1998) +: rnil
  </code></pre>
  
  <p>is legal</p>
  
  <pre><code>("Title" := "test") +: ("Year" := 1998) +: rnil
  </code></pre>
  
  <p>also works, but</p>
  
  <pre><code>("Year" := "test") +: ("Year" := 1998) +: rnil
  </code></pre>
  
  <p>Should fail to compile.</p>
  
  <p>I came up with the following implementation which compiles fine:</p>
  
  <pre><code>{-
  See: http://lpaste.net/104020
    and https://github.com/gonzaw/extensible-records
  -}
  module Record
  
  import Data.List
  
  %default total
  
  data HList : List Type -&gt; Type where
    Nil : HList []
    (::) : a -&gt; HList xs -&gt; HList (a :: xs)
  
  infix 5 :=
  
  data Field : lbl -&gt; Type -&gt; Type where
    (:=) : (label : lbl) -&gt;
            (value : b) -&gt; Field label b
  
  labelsOf : List (lbl, Type) -&gt; List lbl
  labelsOf [] = []
  labelsOf ((label, _) :: xs) = label :: labelsOf xs
  
  toFields : List (lbl, Type) -&gt; List Type
  toFields [] = []
  toFields ((l, t) :: xs) = (Field l t) :: toFields xs
  
  data IsSet : List t -&gt; Type where
    IsSetNil : IsSet []
    IsSetCons : Not (Elem x xs) -&gt; IsSet xs -&gt; IsSet (x :: xs)
  
  data Record : List (lty, Type) -&gt; Type where
    MkRecord : IsSet (labelsOf ts) -&gt; HList (toFields ts) -&gt;
                                      Record ts
  
  infixr 6 +:
  
  rnil : Record []
  rnil = MkRecord IsSetNil []
  
  prepend : { label : lbl,
            xs : List (lbl, Type),
            prf : Not (Elem label (labelsOf xs))
          } -&gt;
          Field label t -&gt;
          Record xs -&gt;
          Record ((label, t) :: xs)
  prepend {prf} f (MkRecord isSet fs) = MkRecord (IsSetCons prf isSet) (f :: fs)
  
  data IsNo : Dec prop -&gt; Type where
    ItIsNo : IsNo (No y)
  
  (+:) : DecEq lbl =&gt;
    { label : lbl, xs : List (lbl, Type) } -&gt;
    Field label t -&gt;
    Record xs -&gt;
    { auto isno : IsNo (isElem label $ labelsOf xs) } -&gt;
    Record ((label, t) :: xs)
  
  (+:) {label} {xs} f r with (isElem label $ labelsOf xs)
      (+:) { isno = ItIsNo } _ _ | (Yes _) impossible
      (+:) f r | (No no) = prepend {prf = no} f r
  </code></pre>
  
  <p>The interesting bit is</p>
  
  <pre><code>  { auto isno : IsNo (isElem label $ labelsOf xs) } -&gt;
  </code></pre>
  
  <p>The idea is that if the keys are unique, the compiler will trivialy find an instance of <code>IsNo</code> while it won't if keys are not unique and therefore fail to compile.</p>
  
  <p>This works well with for those example</p>
  
  <pre><code>("Year" := 1998) +: rnil                       -- Compiles fine
  ("Year" := "test") +: ("Year" := 1998) +: rnil -- fails to compile as expected
  </code></pre>
  
  <p>But </p>
  
  <pre><code>("Title" := "test") +: ("Year" := 1998) +: rnil
  </code></pre>
  
  <p>fails to compile with the following error:</p>
  
  <pre><code>    (input):Type mismatch between
          ("Title" = "Year") -&gt; "Title" = "Year"
  and
          ("Title" = "Year") -&gt; Void
  </code></pre>
  
  <p>I must admit that this error baffles me. Can anyone explain what's happening here ?</p>