Report some simple inference errors

Author: hrutvik

typing/pure_inferencePropsScript.sml

@@ -1371,9 +1371,6 @@ Proof
   recInduct infer'_ind >> rw[infer'_def, infer_def] >>
   rw[infer'_prim_def |> DefnBase.one_line_ify NONE] >>
   simp[apply_foldr_def, FOLDR_MAP] >> gvs[NULL_EQ]
-  >- ( (* Prim - no arguments *)
-    TOP_CASE_TAC >> rw[infer_def]
-    )
   >- ( (* Prim *)
     TOP_CASE_TAC >> rw[infer_def]
     >- foldr_eq_tac
@@ -1394,8 +1391,8 @@ Proof
     pairarg_tac >> gvs[] >> rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >> rw[FUN_EQ_THM] >>
     last_x_assum drule >> rw[]
     ) >>
-  qmatch_goalsub_abbrev_tac `case css of [] => _ | _::_ => foo` >>
-  `(case css of [] => fail (Unknown d) | _::_ => foo) = foo` by (
+  qmatch_goalsub_abbrev_tac `case css of [] => err | _::_ => foo` >>
+  `(case css of [] => err | _::_ => foo) = foo` by (
     Cases_on `css` >> gvs[]) >>
   pop_assum SUBST_ALL_TAC >> unabbrev_all_tac >> rw[LAMBDA_PROD, FUN_EQ_THM] >>
   ntac 2 (rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >> rw[FUN_EQ_THM]) >>
@@ -1419,8 +1416,8 @@ Proof
     ntac 2 (TOP_CASE_TAC >> gvs[]) >> pairarg_tac >> gvs[] >>
     simp[return_def] >> rw[] >> simp[oreturn_def, return_def]
     ) >>
-  simp[return_def, infer_bind_def] >> rename1 `oreturn _ _ n` >>
-  qsuff_tac `oreturn (Unknown d) (oHD tys) n = OK (HD tys, n)` >> simp[] >>
+  simp[return_def, infer_bind_def] >> rename1 `oreturn err _ n` >>
+  qsuff_tac `oreturn err (oHD tys) n = OK (HD tys, n)` >> simp[] >>
   qsuff_tac `LENGTH tys = LENGTH css`
   >- (rw[] >> Cases_on `tys` >> gvs[oreturn_def, return_def]) >>
   qpat_x_assum `FOLDR _ _ _ _ = _` mp_tac >> rpt $ pop_assum kall_tac >>