add failing tests

scall-core/src/main/scala/io/chymyst/dhall/TypeCheck.scala

@@ -604,7 +604,7 @@
                   typeError(
                     s"Expression `assert` failed: Unequal sides, ${lop.alphaNormalized.betaNormalized.print} does not equal ${rop.alphaNormalized.betaNormalized.print}, in ${exprN.print}"
                   )
-              case other                                               => typeError(s"An `assert` expression must have an equality type but has ${other.print}")
+              case other                                               => typeError(s"An `assert` expression must have an equality type but has type ${other.print}")
             }
           case errors   => errors
         }
@@ -630,11 +630,27 @@
             }
 
           case tt @ Expression(Application(Expression(ExprBuiltin(Builtin.Optional)), t)) =>
-            if (pathComponents.head.isOptionalLabel) {
-              validate(gamma, body, t).map(_ => tt)
-            } else typeError(s"An Optional value must be updated with `?` but instead found ${pathComponents.head}")
+            pathComponents.head match {
+              case PathComponent.Label(fieldName) =>
+                typeError(s"An Optional value must be updated with `?` but instead found ${fieldName}")
+              case PathComponent.DescendOptional  =>
+                pathComponents.tail match {
+                  case Seq() => // The expression is (Some x) with ? = body. The type of this expression is Optional Y where body : Y.
+                    // We use `validate` to impose the constraint that body's type is `t`. See https://github.com/dhall-lang/dhall-haskell/issues/2597
+                    validate(gamma, body, t).map(_ => tt)
+                  case tail  => // The expression is (Some x) with ?.a.b = body. The type of this expression is Optional Y where Y is the type of `x with a.b = body`. Here, `x` is a new variable that should not be free in `body`.
+                    val newVar   = VarName("check_type_of_with")
+                    val newBody  = Semantics.shift(positive = true, newVar, BigInt(0), body)
+                    val newWith  = With(Expression(Variable(newVar, BigInt(0))), tail, newBody)
+                    val newGamma = gamma.prependAndShift(newVar, t)
+//                    newWith.inferTypeWith(newGamma).map(t1 => Expression(Application(Expression(ExprBuiltin(Builtin.Optional)), t1))) // This would allow changing types after `with`.
+                    validate(newGamma, newWith, t).map(_ => tt)
 
-          case other => typeError(s"A `with` expression's arg must have record type, but instead found ${other.print}")
+                }
+
+            }
+
+          case other => typeError(s"A `with` expression's argument must have record type or Optional type, but instead found type ${other.print}")
         }
 
       case DoubleLiteral(_)  => Builtin.Double

scall-core/src/test/scala/io/chymyst/dhall/unit/SimpleSemanticsTest.scala

@@ -370,7 +370,6 @@ class SimpleSemanticsTest extends DhallTest {
 
   test("failure in eta expansion with two curried arguments") {
     val failure = "λ(f : Bool → Bool → Bool) → assert : f === (λ(x : Bool) → λ(y : Bool) → f y x)".dhall.inferTypeWith(KnownVars.empty)
-    println(failure)
     expect(failure match {
       case TypecheckResult.Invalid(errors) => errors exists (_ contains "Unequal sides, f does not equal λ(_ : Bool) → λ(_ : Bool) → f _ _@1")
     })
@@ -383,15 +382,13 @@ class SimpleSemanticsTest extends DhallTest {
 
   test("failure 1 with f x in eta expansion with free occurrences of external bound variable") {
     val failure = "λ(f : Bool → Bool → Bool) → λ(x : Bool) → assert : f x === (λ(x : Bool) → f x x)".dhall.inferTypeWith(KnownVars.empty)
-    println(failure)
     expect(failure match {
       case TypecheckResult.Invalid(errors) => errors exists (_ contains "Unequal sides, f x does not equal λ(_ : Bool) → f _ _, in f x ≡ (λ(x : Bool) → f x x)")
     })
   }
 
   test("failure 2 with f x in eta expansion with free occurrences of external bound variable") {
     val failure = "λ(f : Bool → Bool → Bool) → λ(x : Bool) → assert : f === (λ(x : Bool) → f x x)".dhall.inferTypeWith(KnownVars.empty)
-    println(failure)
     expect(failure match {
       case TypecheckResult.Invalid(errors) =>
         errors exists (_ contains "Types of two sides of `===` are not equivalent: ∀(_ : Bool) → ∀(_ : Bool) → Bool and ∀(x : Bool) → Bool")
@@ -512,4 +509,29 @@ class SimpleSemanticsTest extends DhallTest {
     expect(!Semantics.equivalent(x, y))
   }
 
+  test("`with` for Optional works if it does not change type") { // https://github.com/dhall-lang/dhall-haskell/issues/2597
+    val result = "(Some 1) with ? = 2".dhall.typeCheckAndBetaNormalize()
+    expect(result.unsafeGet.print == "Some 2")
+  }
+
+  test("fail `with` for Optional if it changes type") {
+    val result = """(Some 1) with ? = "hello"""".dhall.typeCheckAndBetaNormalize()
+    expect(
+      Try(
+        result.unsafeGet
+      ).failed.get.getMessage contains "Inferred type Text differs from the expected type Natural, expression under type inference: \"hello\""
+    )
+  }
+
+  test("`with` for Optional works if it does not change type, with deep record access") { // https://github.com/dhall-lang/dhall-haskell/issues/2597
+    val result = "(Some { x.y = 1 }) with ?.x.y = 2".dhall.typeCheckAndBetaNormalize()
+    expect(result.unsafeGet.print == "Some { x = { y = 2 } }")
+  }
+
+  test("fail `with` for Optional if it changes type, with deep record access") {
+    val result = """(Some { x.y = 1 }) with ?.x.y = "hello"""".dhall.typeCheckAndBetaNormalize()
+//    expect(result.unsafeGet.print == "Some { x = { y = \"hello\" } }")
+    expect(Try(result.unsafeGet).failed.get.getMessage contains "Inferred type { x : { y : Text } } differs from the expected type { x : { y : Natural } }")
+  }
+
 }

tutorial/programming_dhall.md

@@ -90,6 +90,9 @@ Identifiers may be arbitrary characters (even keywords or whitespace) if escaped
 3
 ```
 
+The standalone underscore character `_` in Haskell and Scala is a syntax for a special "unused" variable.
+But in Dhall, the variable named `_` is a variable like any other.
+
 ### Primitive types
 
 Integers must have a sign (`+1` or `-1`) while `Natural` numbers may not have a sign (`123`).
@@ -7027,6 +7030,7 @@ p G unfixf (fmap_K T G (unfold T cT) kt)
 as long as the precondition of the law holds:
 
 `fmap_F T G (unfold T cT) (cT x) === unfixf (unfold T cT x)`
+
 This equation (after setting `R = T` and `rfr = cT`) was derived in Statement 2 in the section "Properties of co-inductive types".
 
 This allows us to complete the proof of item 2: