Rework annotation and Sort handling

16 files changed, 114 insertions, 87 deletions

diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index f91aa73..e4e2a5f 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -72,7 +72,7 @@ impl Hir {
 
     /// Typecheck the Hir.
     pub fn typecheck(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
-        type_with(env, self)
+        type_with(env, self, None)
     }
 
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 794edcf..a4ab31f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -24,13 +24,10 @@ pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(msg.to_string())))
 }
 
-pub fn mk_span_err<T, S: ToString>(
-    span: &Span,
-    msg: S,
-) -> Result<T, TypeError> {
+pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
     mkerr(
         ErrorBuilder::new(msg.to_string())
-            .span_err(span.clone(), msg.to_string())
+            .span_err(span, msg.to_string())
             .format(),
     )
 }
@@ -40,22 +37,25 @@ pub fn mk_span_err<T, S: ToString>(
 fn type_one_layer(
     env: &TyEnv,
     ekind: ExprKind<TyExpr>,
+    annot: Option<Type>,
     span: Span,
 ) -> Result<TyExpr, TypeError> {
-    let span_err = |msg: &str| mk_span_err(&span, msg);
+    let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with
+        ExprKind::Var(..)
+        | ExprKind::Const(Const::Sort)
+        | ExprKind::Annot(..) => unreachable!(), // Handled in type_with
 
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type_tyexpr(
                 &env.insert_type(&binder.clone(), annot.eval(env)),
             )?;
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
-            type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env)
+            type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.get_type()?.as_const() {
@@ -253,18 +253,6 @@ fn type_one_layer(
                 } // _ => span_err("NotARecord"),
             }
         }
-        ExprKind::Annot(x, t) => {
-            let t = t.eval(env);
-            let x_ty = x.get_type()?;
-            if x_ty != t {
-                return span_err(&format!(
-                    "annot mismatch: {} != {}",
-                    x_ty.to_expr_tyenv(env),
-                    t.to_expr_tyenv(env)
-                ));
-            }
-            x_ty
-        }
         ExprKind::Assert(t) => {
             let t = t.eval(env);
             match &*t.kind() {
@@ -365,7 +353,7 @@ fn type_one_layer(
                 x.get_type_tyexpr(env)?,
                 y.get_type_tyexpr(env)?,
             );
-            type_one_layer(env, ekind, span.clone())?.eval(env)
+            type_one_layer(env, ekind, None, span.clone())?.eval(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             fn check_rectymerge(
@@ -376,20 +364,25 @@ fn type_one_layer(
             ) -> Result<(), TypeError> {
                 let kts_x = match x.kind() {
                     ValueKind::RecordType(kts) => kts,
-                    _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"),
+                    _ => {
+                        return mk_span_err(
+                            span.clone(),
+                            "RecordTypeMergeRequiresRecordType",
+                        )
+                    }
                 };
                 let kts_y = match y.kind() {
                     ValueKind::RecordType(kts) => kts,
-                    _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"),
+                    _ => {
+                        return mk_span_err(
+                            span.clone(),
+                            "RecordTypeMergeRequiresRecordType",
+                        )
+                    }
                 };
                 for (k, tx) in kts_x {
                     if let Some(ty) = kts_y.get(k) {
-                        check_rectymerge(
-                            span,
-                            env,
-                            tx.clone(),
-                            ty.clone(),
-                        )?;
+                        check_rectymerge(span, env, tx.clone(), ty.clone())?;
                     }
                 }
                 Ok(())
@@ -717,30 +710,38 @@ fn type_one_layer(
             let ty_field_default = type_one_layer(
                 env,
                 ExprKind::Field(ty.clone(), "default".into()),
+                None,
                 span.clone(),
             )?;
             let ty_field_type = type_one_layer(
                 env,
                 ExprKind::Field(ty.clone(), "Type".into()),
+                None,
                 span.clone(),
             )?;
-            let merge = type_one_layer(
+            return type_one_layer(
                 env,
                 ExprKind::BinOp(
                     BinOp::RightBiasedRecordMerge,
                     ty_field_default,
                     compl.clone(),
                 ),
-                span.clone(),
-            )?;
-            return type_one_layer(
-                env,
-                ExprKind::Annot(merge, ty_field_type),
+                Some(ty_field_type.eval(env)),
                 span.clone(),
             );
         }
     };
 
+    if let Some(annot) = annot {
+        if ty != annot {
+            return span_err(&format!(
+                "annot mismatch: {} != {}",
+                ty.to_expr_tyenv(env),
+                annot.to_expr_tyenv(env)
+            ));
+        }
+    }
+
     Ok(TyExpr::new(
         HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
         Some(ty),
@@ -748,72 +749,78 @@ fn type_one_layer(
     ))
 }
 
-/// `type_with` typechecks an expressio in the provided environment.
-pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
-    let (tyekind, ty) = match hir.kind() {
-        HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))),
+/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
+/// to compare with.
+pub(crate) fn type_with(
+    env: &TyEnv,
+    hir: &Hir,
+    annot: Option<Type>,
+) -> Result<TyExpr, TypeError> {
+    match hir.kind() {
+        HirKind::Var(var) => Ok(TyExpr::new(
+            HirKind::Var(*var),
+            Some(env.lookup(var)),
+            hir.span(),
+        )),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-            (HirKind::Expr(ExprKind::Const(Const::Sort)), None)
+            mk_span_err(hir.span(), "Sort does not have a type")
+        }
+        HirKind::Expr(ExprKind::Annot(x, t)) => {
+            let t = match t.kind() {
+                HirKind::Expr(ExprKind::Const(Const::Sort)) => {
+                    Value::from_const(Const::Sort)
+                }
+                _ => type_with(env, t, None)?.eval(env),
+            };
+            type_with(env, x, Some(t))
         }
         HirKind::Expr(ekind) => {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
-                    let annot = type_with(env, annot)?;
+                    let annot = type_with(env, annot, None)?;
                     let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body)?;
+                    let body = type_with(&body_env, body, None)?;
                     ExprKind::Lam(binder.clone(), annot, body)
                 }
                 ExprKind::Pi(binder, annot, body) => {
-                    let annot = type_with(env, annot)?;
+                    let annot = type_with(env, annot, None)?;
                     let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body)?;
+                    let body = type_with(&body_env, body, None)?;
                     ExprKind::Pi(binder.clone(), annot, body)
                 }
                 ExprKind::Let(binder, annot, val, body) => {
-                    let val = if let Some(t) = annot {
-                        Hir::new(
-                            HirKind::Expr(ExprKind::Annot(
-                                val.clone(),
-                                t.clone(),
-                            )),
-                            t.span(),
-                        )
+                    let val_annot = if let Some(t) = annot {
+                        Some(type_with(env, t, None)?.eval(env))
                     } else {
-                        val.clone()
+                        None
                     };
-                    let val = type_with(env, &val)?;
+                    let val = type_with(env, &val, val_annot)?;
                     let val_ty = val.get_type()?;
                     let val_nf = val.eval(env);
                     let body_env = env.insert_value(&binder, val_nf, val_ty);
-                    let body = type_with(&body_env, body)?;
+                    let body = type_with(&body_env, body, None)?;
                     ExprKind::Let(binder.clone(), None, val, body)
                 }
-                _ => ekind.traverse_ref(|e| type_with(env, e))?,
+                _ => ekind.traverse_ref(|e| type_with(env, e, None))?,
             };
-            return type_one_layer(env, ekind, hir.span());
+            type_one_layer(env, ekind, annot, hir.span())
         }
-    };
-
-    Ok(TyExpr::new(tyekind, ty, hir.span()))
+    }
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(e: &Hir) -> Result<TyExpr, TypeError> {
-    let res = type_with(&TyEnv::new(), e)?;
-    // Ensure that the inferred type exists (i.e. this is not Sort)
-    res.get_type()?;
-    Ok(res)
+pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
+    type_with(&TyEnv::new(), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
-    let hir =
-        Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span());
-    typecheck(&hir)
+    let ty = typecheck(&ty)?.eval(&TyEnv::new());
+    type_with(&TyEnv::new(), hir, Some(ty))
 }
diff --git a/dhall/tests/type-inference/failure/SortInLet.txt b/dhall/tests/type-inference/failure/SortInLet.txt
index 5b88ff7..19bd26d 100644
--- a/dhall/tests/type-inference/failure/SortInLet.txt
+++ b/dhall/tests/type-inference/failure/SortInLet.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:8
+  |
+1 | let x = Sort in 0
+  |         ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/hurkensParadox.txt b/dhall/tests/type-inference/failure/hurkensParadox.txt
index 6b99615..5aacb80 100644
--- a/dhall/tests/type-inference/failure/hurkensParadox.txt
+++ b/dhall/tests/type-inference/failure/hurkensParadox.txt
@@ -1,15 +1,15 @@
 Type error: error: wrong type of function argument
-  --> <current file>:6:23
+  --> <current file>:6:15
    |
  1 |     let bottom : Type = ∀(any : Type) → any
  2 | 
  3 | in  let not : Type → Type = λ(p : Type) → p → bottom
  4 | 
 ...
+ 9 | in  let tau
 10 |         : pow (pow U) → U
-11 |         =   λ(t : pow (pow U))
-   |                        ^^^ this expects an argument of type: Kind
-   |                            ^ but this has type: Sort
+   |                ^^^ this expects an argument of type: Kind
+   |                    ^ but this has type: Sort
    |
    = note: expected type `Kind`
               found type `Sort`
diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt
index 5b88ff7..a5d2465 100644
--- a/dhall/tests/type-inference/failure/recordOfKind.txt
+++ b/dhall/tests/type-inference/failure/recordOfKind.txt
@@ -1 +1 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
index 01a1f32..a39a0fb 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt
@@ -2,5 +2,5 @@ Type error: error: annot mismatch: { x : Natural } != { y : Natural }
  --> <current file>:1:0
   |
 1 | { x = 1 } : { y : Natural }
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural }
+  | ^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural }
   |
diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
index 5c10467..9ecc2a4 100644
--- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
+++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt
@@ -2,5 +2,5 @@ Type error: error: annot mismatch: { x : Natural } != { x : Text }
  --> <current file>:1:0
   |
 1 | { x = 1 } : { x : Text }
-  | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text }
+  | ^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text }
   |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
index 5b88ff7..6f26607 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+  |
+1 | Kind → Sort
+  |        ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
index 5b88ff7..169014b 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:7
+  |
+1 | Type → Sort
+  |        ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
index 2f75196..51279f2 100644
--- a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
+++ b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt
@@ -1,6 +1,6 @@
 Type error: error: annot mismatch: Bool != Natural
- --> <current file>:1:8
+ --> <current file>:1:18
   |
 1 | let x : Natural = True in True
-  |         ^^^^^^^ annot mismatch: Bool != Natural
+  |                   ^^^^ annot mismatch: Bool != Natural
   |
diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
index 066e4a3..0cc4bba 100644
--- a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
+++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -2,5 +2,5 @@ Type error: error: annot mismatch: List Natural != Optional Natural
  --> <current file>:1:0
   |
 1 | [ 1 ] : Optional Natural
-  | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: List Natural != Optional Natural
+  | ^^^^^ annot mismatch: List Natural != Optional Natural
   |
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
index 5b88ff7..a5d2465 100644
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -1 +1 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
index 5b88ff7..a5d2465 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -1 +1 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
index 5b88ff7..a5d2465 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -1 +1 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
diff --git a/dhall/tests/type-inference/failure/unit/Sort.txt b/dhall/tests/type-inference/failure/unit/Sort.txt
index 5b88ff7..e402127 100644
--- a/dhall/tests/type-inference/failure/unit/Sort.txt
+++ b/dhall/tests/type-inference/failure/unit/Sort.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: Sort
+Type error: error: Sort does not have a type
+ --> <current file>:1:0
+  |
+1 | Sort
+  | ^^^^ Sort does not have a type
+  |
diff --git a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
index e203d22..dffadb1 100644
--- a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
+++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt
@@ -2,5 +2,5 @@ Type error: error: annot mismatch: Natural != Bool
  --> <current file>:1:0
   |
 1 | 1 : Bool
-  | ^^^^^^^^ annot mismatch: Natural != Bool
+  | ^ annot mismatch: Natural != Bool
   |