Fixing the typechecking rule for Optional + with ? (#2650)

* Fixing the typesetting rule

* remove extraneous comment and refactor

* Revert "remove extraneous comment and refactor"

This reverts commit 215d4d1.

* revert refactor as it fails

* bump ci

* bump ci

* bump ci

* bump ci

Author: winitzki

dhall/src/Dhall/TypeCheck.hs

@@ -1314,12 +1314,21 @@ infer typer = loop
 
                   VOptional _O' -> do
                     case ks of
-                      WithQuestion  :| _ -> do
+
+                        -- (Some x) with ? = v is valid iff the type of x is the same as the type of v.
+                      WithQuestion :| [] -> do
                         tV' <- loop ctx v
                         if Eval.conv values _O' tV'
                           then return (VOptional _O')
                           else die OptionalWithTypeMismatch
 
+                        -- (Some x) with ?.a.b = v is valid iff the type of x.a.b is the same as the type of v.
+                      WithQuestion :| k₁ : ks' -> do
+                        tV' <- with _O' (k₁ :| ks') v
+                        if Eval.conv values _O' tV'
+                          then return (VOptional _O')
+                          else die OptionalWithTypeMismatch
+
                       WithLabel k :| _ -> die (NotAQuestionPath k)
 
                   _ -> die (NotWithARecord e₀ (quote names tE')) -- TODO: NotWithARecordOrOptional