Add support for updating dependent records

[eugene536]

I tried to compile this simple program, but I have an error. If I create a new Record with new fields, it works fine, but why I can't update (or set new values) two fields simultaneously? (Is it a bug or I misunderstand something?)

import Data.Vect

record DataStore where
  constructor MkData
  size   : Nat
  items  : Vect size Nat

addToStore : (store : DataStore) -> Nat -> DataStore
-- Why does this line not compile?
addToStore store x = record {size $= (1+), items $= (x::)} store
-- addToStore store x = MkData (1 + (size store)) (x :: (items store))

temp.idr:10:12:When checking right hand side of addToStore with expected type
        DataStore

No such variable set_items
Holes: Main.addToStore

[ahmadsalim]

Thanks for the bug report. Unfortunately, Idris does not currently support generating record setters for dependent records (as suggested by the feature request in #644).

I will convert your issue into a feature request.

[edwinb]

This is, unfortunately, rather hard, because there's a dependency between the two updates that means they both must be done at once. This is incompatible with the current meaning of record updates, which does one at a time.

If you make size implicit, it's fine:

record DataStore where
  constructor MkData
  items  : Vect size Nat

addToStore : (store : DataStore) -> Nat -> DataStore
addToStore store x = record { items $= (x::) } store

When you create a record, Idris builds update functions with types of the following form:

set_items : Vect size Nat -> DataStore -> DataStore

If there are fields that can't be updated because of dependencies on others, the setters don't get generated, because the setters only update one field. If size is implicit, building the setters works because the generated code doesn't mention the implicit fields.

There might be a better way to do this that identifies dependencies and builds setters in a more clever way. I'm very unlikely to do this any time soon, though, sorry. If somebody wants to step up and have a go, great.