fix(typing) Type soundness bug for match expressions #645

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>

examples/opttest/contract.json

@@ -0,0 +1,3 @@
+{
+  "$class": "org.accordproject.opttest.TemplateModel"
+}

examples/opttest/logic.ergo

@@ -0,0 +1,44 @@
+/*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+namespace org.accordproject.opttest
+
+contract OptTest over TemplateModel {
+  // Simple Clause
+  clause test(request : Request) : Response {
+		let foo : Nothing? =   // This should fail
+      match request
+		  with let x : Request then some(1)
+		  else none;
+
+		let foo : Nothing? =   // This should fail
+      match some(request)
+		  with let? x : Request then some(1)
+		  else none;
+
+		let foo : Nothing? =   // This should fail
+      match request
+		  with let x then some(1)
+		  else none;
+
+		let foo : Nothing? =   // This should fail
+      match some(request)
+		  with let? x then some(1)
+		  else none;
+
+    return Response{
+		  test1:1
+		}
+  }
+}

examples/opttest/model.cto

@@ -0,0 +1,29 @@
+/*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+namespace org.accordproject.opttest
+
+transaction Request {
+}
+
+transaction Response {
+  o Integer test1
+}
+
+/**
+ * The template model
+ */
+@AccordTemplateModel("opttest")
+concept TemplateModel {
+}

examples/opttest/request.json

@@ -0,0 +1,3 @@
+{
+    "$class": "org.accordproject.opttest.Request"
+}

examples/opttest/state.json

@@ -0,0 +1,2 @@
+{ "$class": "org.accordproject.cicero.contract.AccordContractState",
+  "stateId" : "1" }

mechanization/ErgoC/Lang/ErgoCTypecheck.v

@@ -249,6 +249,19 @@ Section ErgoCTypecheck.
                               ((CaseLet (prov,sofart) name None,eT)::fst sofarT, sofart))
                            sofarT
                            (ergoc_typecheck_expr nsctxt (type_context_update_local_env ctxt name t0) res)
+                  | (CaseLet prov name (Some b), res) =>
+                    elift2 (fun sofarT eT =>
+                              let et := exprct_type_annot eT in
+                              let sofart := ergoc_type_join et (snd sofarT) in
+                              ((CaseLet (prov,sofart) name (Some b), eT)::fst sofarT, sofart))
+                           sofarT
+                           (ergoc_typecheck_expr
+                              nsctxt
+                              (type_context_update_local_env
+                                 ctxt
+                                 name
+                                 (tbrand (b::nil)))
+                              res)
                   | (CaseLetOption prov name None, res) =>
                     match unteither t0 with
                     | None =>
@@ -267,7 +280,8 @@ Section ErgoCTypecheck.
                       case_option_not_on_either_error prov
                     | Some (st, ft) =>
                       elift2 (fun sofarT eT =>
-                                let sofart := snd sofarT in
+                                let et := exprct_type_annot eT in
+                                let sofart := ergoc_type_join et (snd sofarT) in
                                 ((CaseLetOption (prov,sofart) name (Some b), eT)::fst sofarT, sofart))
                              sofarT
                              (ergoc_typecheck_expr
@@ -283,18 +297,6 @@ Section ErgoCTypecheck.
                               ((CaseWildcard (prov,sofart) (Some b), eT)::fst sofarT, sofart))
                            sofarT
                            (ergoc_typecheck_expr nsctxt ctxt res)
-                  | (CaseLet prov name (Some b), res) =>
-                    elift2 (fun sofarT eT =>
-                              let sofart := snd sofarT in
-                              ((CaseLet (prov,sofart) name (Some b), eT)::fst sofarT, sofart))
-                           sofarT
-                           (ergoc_typecheck_expr
-                              nsctxt
-                              (type_context_update_local_env
-                                 ctxt
-                                 name
-                                 (tbrand (b::nil)))
-                              res)
                   end)
                (esuccess (nil, dt) nil)
                pes))

packages/ergo-engine/test/workload.json

@@ -51,6 +51,20 @@
       }
     }
   },
+  {
+    "name": "opttest",
+    "dir": "examples/opttest",
+    "ergo": ["logic.ergo"],
+    "models": ["model.cto"],
+    "contract": "contract.json",
+    "request": "request.json",
+    "state": "state.json",
+    "contractName": "org.accordproject.opttest.OptTest",
+    "currentTime": null,
+    "expected": {
+      "error": "Type error (at file examples/opttest/logic.ergo line 20 col 2). The let type annotation `Nothing?' for the name `foo' does not match the actual type `Integer?'.\n  let foo : Nothing? =   // This should fail\n  ^                                         "
+    }
+  },
   {
     "name": "helloworldstate",
     "dir": "examples/helloworldstate",