[WIP] Dependent field updates?

[samuelgruetter]

Currently, in RecordSetTests.DependentExample, we can't typecheck

Definition setA(x: X)(a: T x) := x <|A := a|>.

because set only accepts non-dependent projections (proj: R -> T). This PR makes set accept projections with a dependent return type, (proj: forall r: R, T r), so that setA above now typechecks.

It requires changing the argument order of set (the record needs to come before the field updater), because the type of the field updater depends on the record.

Also, I haven't figured out yet how to fix the recursive notation for nested updates...

Thoughts?

[JasonGross]

Also, I haven't figured out yet how to fix the recursive notation for nested updates...

I think you want

--- a/src/RecordSet.v
+++ b/src/RecordSet.v
@@ -90,9 +90,9 @@ Module RecordSetNotations.
   Notation "x <| proj  :=  v |>" := (set proj x (fun _ => v))
                                     (at level 12, left associativity) : record_set.
   Notation "x <| proj1 ; proj2 ; .. ; projn ::= f |>" :=
-    (set proj1 (set proj2 .. (set projn f) ..) x)
+    (set proj1 x (set proj2 x .. (set projn x f) ..))
     (at level 12, f at next level, left associativity) : record_set.
   Notation "x <| proj1 ; proj2 ; .. ; projn := v |>" :=
-    (set proj1 (set proj2 .. (set projn (fun _ => v)) ..) x)
+    (set proj1 x (set proj2 x .. (set projn x (fun _ => v)) ..))
     (at level 12, left associativity) : record_set.
 End RecordSetNotations.

Edit: Nevermind, this doesn't work

[JasonGross]

@samuelgruetter I fixed it for you: https://github.com/samuelgruetter/coq-record-update/pull/1

However, the nested syntax might not work correctly when we really need set : forall r : R, (T r -> T r) -> R rather than having a version that is set : (forall r, T r -> T r) -> (R -> R) (i.e. when typechecking the updated nested value depends on the particular record you are updating); you should add some tests maybe.