fix the with regression as in dhall-lang/dhall-haskell#2597

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

@@ -604,7 +604,7 @@ object TypeCheck {
                   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,25 @@ object TypeCheck {
             }
 
           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)
+                    newWith.inferTypeWith(gamma.prependAndShift(newVar, t)).map(t1 => Expression(Application(Expression(ExprBuiltin(Builtin.Optional)), t1)))
 
-          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

@@ -525,16 +525,17 @@ class SimpleSemanticsTest extends DhallTest {
 
   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 = 2 }")
+    expect(result.unsafeGet.print == "Some { x = { y = 2 } }")
   }
 
-  test("fail `with` for Optional if it changes type, with deep record access") {
+  test("succeed `with` for Optional if it changes type, with deep record access") {
     val result = """(Some { x.y = 1 }) with ?.x.y = "hello"""".dhall.typeCheckAndBetaNormalize()
-    expect(
-      Try(
-        result.unsafeGet
-      ).failed.get.getMessage contains "Inferred type Text differs from the expected type { x : { y : Natural } }, expression under type inference: \"hello\""
-    )
+    expect(result.unsafeGet.print == "Some { x = { y = \"hello\" } }")
+//    expect(
+//      Try(
+//        result.unsafeGet
+//      ).failed.get.getMessage contains "Inferred type Text differs from the expected type { x : { y : Natural } }, expression under type inference: \"hello\""
+//    )
   }
 
 }

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: