Ooopps

1 - record.idr

module Record

import Data.List

%default total

data IsSet : List t -> Type where
  IsSetNil : IsSet []
  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)

data HList : List Type -> Type where
  Nil : HList []
  (::) : a -> HList xs -> HList (a :: xs)

infix 5 :=

data Field : lbl -> Type -> Type where
  (:=) : (label : lbl) ->
          (value : b) -> Field label b

labelsOf : List (lbl, Type) -> List lbl
labelsOf = map fst

Record : (xs : List (lbl, Type)) -> IsSet (labelsOf xs) -> Type
Record xs prf =
  let toField = \(label, t) => Field label t
      types = map toField xs in
      HList types

rnil : Record [] IsSetNil
rnil = Nil

infixr 6 +:

(+:) : Field lbl t ->
  Record xs xsIsSet ->
  (prf : Not (Elem lbl (labelsOf xs))) ->
  Record ((lbl, t) :: xs) (IsSetCons prf xsIsSet)
(+:) f rec _ = f :: rec

-- foo : Record [('Book, String), ('Year, Integer)]
-- foo = ('Book := "yolo") +: ('Year := 1234) +: rnil

2 - compiler_error.txt

Idris> :l record.idr
Type checking ./record.idr
record.idr:43:18-19:
   |
43 | (+:) f rec _ = f :: rec
   |                  ~~
When checking right hand side of +: with expected type
        Record ((lbl, t) :: xs) (IsSetCons prf xsIsSet)

When checking an application of constructor Record.:::
        Type mismatch between
                Record xs xsIsSet (Type of rec)
        and
                HList (Prelude.List.List implementation of Prelude.Functor.Functor, method map (\lamp => case lamp of   (label, t) => Field label t) xs) (Expected type)

        Specifically:
                Type mismatch between
                        Prelude.List.List implementation of Prelude.Functor.Functor, method map (\lamp => case lamp of   (label, t) => Field label t) xs
                and
                        Prelude.List.List implementation of Prelude.Functor.Functor, method map (\lamp => case lamp of   (label, t) => Field label t) xs

Holes: Record.+: