improve error messages

1 files changed, 21 insertions, 19 deletions

diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml
index ba1da02..f40076d 100644
--- a/src/elaborator/Elaborator.ml
+++ b/src/elaborator/Elaborator.ml
@@ -5,8 +5,6 @@ module A = Ast
 module S = NbE.Syntax
 module D = NbE.Domain
 
-(* TODO: REALLY improve error messages *)
-
 (* invariant: `tps`, `tms` and `names` all have length `size` *)
 type env = {
   tps : D.env;
@@ -48,19 +46,23 @@ let eval tm = NbE.eval ~env:(Eff.read()).tms tm
 (* TODO: this is kind of inelegant, can we do better? *)
 let eval_at arg = NbE.eval ~env:((Eff.read()).tms <: arg)
 
-let quote v = NbE.quote ~size:(Eff.read()).size v
-
 (** Pretty-printing helpers *)
 
-let pp () = let names = (Eff.read()).names in fun fmt tm -> 
-    Pretty.pp ~names fmt tm
+let pp_tm () =
+  let names = (Eff.read()).names in
+  fun fmt tm -> Pretty.pp ~names fmt tm
+
+let pp_val () =
+  let size = (Eff.read()).size in
+  let pp_tm = pp_tm () in
+  fun fmt v -> pp_tm fmt (NbE.quote ~size v)
 
 (** Main algorithm *)
 
 type connective = [ `Pi | `Sigma ]
 
 let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
-  Error.tracef ?loc:tm.loc "when checking against the type @[%a@]" (pp()) (quote tp) @@ fun () ->
+  Error.tracef ?loc:tm.loc "when checking against the type @[%a@]" (pp_val()) tp @@ fun () ->
   match tm.value with
   | A.Pi ((name, base), fam) -> check_connective `Pi ~name:name.value ~base ~fam ~tp
   | A.Fun (base, fam) -> check_connective `Pi ~name:None ~base ~fam ~tp
@@ -70,7 +72,7 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
           let fib = NbE.inst_clo fam arg in
           check ~tm:body ~tp:fib in
         S.Lam (name.value, body)
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (pp()) (quote tp)
+      | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "a Pi type"
     end
   | A.Sg ((name, base), fam) -> check_connective `Sigma ~name:name.value ~base ~fam ~tp
   | A.Prod (base, fam) -> check_connective `Sigma ~name:None ~base ~fam ~tp
@@ -80,28 +82,28 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
         let fib = NbE.inst_clo fam (eval fst) in
         let snd = check ~tm:snd ~tp:fib in
         S.Pair (fst, snd)
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (pp()) (quote tp)
+      | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "a Sigma type"
     end
   | A.Type -> begin match tp with (* TODO type-in-type *)
       | D.Type -> S.Type
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
+      | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type"
     end
   | A.Bool -> begin match tp with
       | D.Type -> S.Bool
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
+      | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type"
     end
   | A.True -> begin match tp with
       | D.Bool -> S.True
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
+      | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "bool"
     end
   | A.False -> begin match tp with
       | D.Bool -> S.False
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
+      | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "bool"
     end
   | _ -> let (inferred_tp, tm) = infer tm in begin
       try NbE.equate ~size:((Eff.read()).size) inferred_tp tp with
       | NbE.Unequal ->
-        Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" (pp()) (quote tp) (pp()) (quote inferred_tp)
+        Error.type_mismatch (pp_val()) tp (pp_val()) inferred_tp
     end;
     tm
 
@@ -114,7 +116,7 @@ and check_connective connective ~(name : Ident.local) ~(base : A.expr) ~(fam : A
       | `Pi -> S.Pi (name, base, fam)
       | `Sigma -> S.Sg (name, base, fam)
     end
-  | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
+  | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type"
 
 and infer (tm : A.expr) : D.t * S.t =
   Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
@@ -130,18 +132,18 @@ and infer (tm : A.expr) : D.t * S.t =
         let tp = NbE.inst_clo fam (eval arg) in
         let tm = S.App (fn, arg) in
         (tp, tm)
-      | _ -> Error.fatalf Error.Message.IllTyped "cannot apply this term because it is not a function"
+      | (tp, _) -> Error.type_mismatch ?loc:fn.loc Fmt.string "a Pi type" (pp_val()) tp
     end
   | A.Fst p -> begin match infer p with
       | (D.Sg (_, base, _), p) -> (base, S.Fst p)
-      | _ -> Error.fatalf Error.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type"
+      | (tp, _) -> Error.type_mismatch ?loc:p.loc Fmt.string "a Sigma type" (pp_val()) tp
     end
   | A.Snd p -> begin match infer p with
       | (D.Sg (_, _, fam), p) ->
         let tp = NbE.inst_clo fam (eval (S.Fst p)) in
         let tm = S.Snd p in
         (tp, tm)
-      | _ -> Error.fatalf Error.Message.IllTyped "cannot apply second projection to this term because it is of sigma type"
+      | (tp, _) -> Error.type_mismatch ?loc:p.loc Fmt.string "a Sigma type" (pp_val()) tp
     end
   | A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
     let scrut = check ~tm:scrut ~tp:D.Bool in
@@ -154,7 +156,7 @@ and infer (tm : A.expr) : D.t * S.t =
     let false_case = check ~tm:false_case ~tp:motive_false in
     let tm = S.BoolElim { motive_var = motive_var.value; motive; true_case; false_case; scrut } in
     (motive_scrut, tm)
-  | _ -> Error.fatalf Error.Message.CannotInferType "cannot infer type"
+  | _ -> Error.not_inferable ()
 
 let empty_env : env = {
   tps = Emp;