Add missing symmetric rules for field selection normalization (#682)

Follow-up to #664.

standard/beta-normalization.md

@@ -970,57 +970,50 @@ If the argument is a record projection, select from the contained record.
     t₀.x ⇥ v
 
 
-If the argument is a right-biased record merge, first inspect the right operand.
-If it is a record literal that contains the field, select it:
+If the argument is a right-biased record merge and one of the operands is a
+record literal, we can simplify further:
 
 
-    t₀ ⇥ t₁ ⫽ { x = v, … }
-    ──────────────────────
-    t₀.x ⇥ v
-
-
-If it is a record literal that doesn't contain the field, select from the left
-operand:
+    t₀ ⇥ { x = v, … } ⫽ t₁
+    ─────────────────────────
+    t₀.x ⇥ ({ x = v } ⫽ t₁).x
 
 
-    t₀ ⇥ t₁ ⫽ { xs… }   t₁.x ⇥ v
+    t₀ ⇥ { xs… } ⫽ t₁   t₁.x ⇥ v
     ──────────────────────────── ; x ∉ xs
     t₀.x ⇥ v
 
 
-If the left operand is a record literal that doesn't contain the field, select
-from the right operand.
+    t₀ ⇥ t₁ ⫽ { x = v, … }
+    ──────────────────────
+    t₀.x ⇥ v
 
 
-    t₀ ⇥ { xs… } ⫽ t₁   t₁.x ⇥ v
+    t₀ ⇥ t₁ ⫽ { xs… }   t₁.x ⇥ v
     ──────────────────────────── ; x ∉ xs
     t₀.x ⇥ v
 
 
-If the argument is a recursive record merge, first inspect the right operand.
-If it is a record literal that contains the field, simplify this right operand by
-restricting it to this field:
+If the argument is a recursive record merge and one of the operands is a record
+literal, we can simplify it similarly:
 
 
-    t₀ ⇥ t₁ ∧ { x = v, … }
+    t₀ ⇥ { x = v, … } ∧ t₁
     ─────────────────────────
-    t₀.x ⇥ (t₁ ∧ { x = v }).x
+    t₀.x ⇥ ({ x = v } ∧ t₁).x
 
 
-If it is a record literal that doesn't contain the field, select from the left
-operand:
-
-
-    t₀ ⇥ t₁ ∧ { xs… }   t₁.x ⇥ v
+    t₀ ⇥ { xs… } ∧ t₁   t₁.x ⇥ v
     ──────────────────────────── ; x ∉ xs
     t₀.x ⇥ v
 
 
-If the left operand is a record literal that doesn't contain the field, select
-from the right operand.
+    t₀ ⇥ t₁ ∧ { x = v, … }
+    ─────────────────────────
+    t₀.x ⇥ (t₁ ∧ { x = v }).x
 
 
-    t₀ ⇥ { xs… } ∧ t₁   t₁.x ⇥ v
+    t₀ ⇥ t₁ ∧ { xs… }   t₁.x ⇥ v
     ──────────────────────────── ; x ∉ xs
     t₀.x ⇥ v
 

tests/normalization/success/unit/RecursiveRecordMergeWithinFieldSelection3A.dhall

@@ -0,0 +1 @@
+({ a = 0, b = 1 } ∧ x).a

tests/normalization/success/unit/RecursiveRecordMergeWithinFieldSelection3B.dhall

@@ -0,0 +1 @@
+({ a = 0 } ∧ x).a

tests/normalization/success/unit/RightBiasedMergeWithinFieldSelection3A.dhall

@@ -0,0 +1 @@
+({ a = 0, b = 1 } ⫽ x).a

tests/normalization/success/unit/RightBiasedMergeWithinFieldSelection3B.dhall

@@ -0,0 +1 @@
+({ a = 0 } ⫽ x).a