Enforce type information almost everywhere

5 files changed, 53 insertions, 63 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 7f98826..4a78b05 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -27,13 +27,14 @@ pub(crate) enum Form {
 }
 use Form::{Unevaled, NF, WHNF};
 
-#[derive(Debug)]
 /// Partially normalized value.
 /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
 /// Invariant: if `form` is `NF`, `value` must be fully normalized
+#[derive(Debug)]
 struct ValueInternal {
     form: Form,
     value: ValueF,
+    /// This is None if and only if `value` is `Sort` (which doesn't have a type)
     ty: Option<Value>,
 }
 
@@ -69,11 +70,15 @@ impl ValueInternal {
                 value: ValueF::Const(Const::Type),
                 ty: None,
             },
-            |vint| match &vint.form {
-                Unevaled => {
+            |vint| match (&vint.form, &vint.ty) {
+                (Unevaled, None) => ValueInternal {
+                    form: NF,
+                    value: ValueF::Const(Const::Sort),
+                    ty: None,
+                },
+                (Unevaled, Some(ty)) => {
                     let new_value =
-                        normalize_whnf(vint.value, vint.ty.as_ref())
-                            .into_whnf(vint.ty.as_ref());
+                        normalize_whnf(vint.value, &ty).into_whnf(&ty);
                     ValueInternal {
                         form: WHNF,
                         value: new_value,
@@ -81,7 +86,7 @@ impl ValueInternal {
                     }
                 }
                 // Already in WHNF
-                WHNF | NF => vint,
+                (WHNF, _) | (NF, _) => vint,
             },
         )
     }
@@ -103,10 +108,9 @@ impl ValueInternal {
     fn get_type(&self) -> Result<&Value, TypeError> {
         match &self.ty {
             Some(t) => Ok(t),
-            None => Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Untyped,
-            )),
+            None => {
+                Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+            }
         }
     }
 }
@@ -115,9 +119,13 @@ impl Value {
     pub(crate) fn new(value: ValueF, form: Form, ty: Option<Value>) -> Value {
         ValueInternal { form, value, ty }.into_value()
     }
+    // TODO: this is very wrong
     pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
         Value::new(v, Unevaled, None)
     }
+    pub(crate) fn const_sort() -> Value {
+        Value::new(ValueF::Const(Const::Sort), NF, None)
+    }
     pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
         Value::new(v, Unevaled, Some(t))
     }
@@ -225,27 +233,30 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let ty = self.get_type().ok();
-        let vovf = apply_any(self.clone(), v.clone(), ty.as_ref());
-        match self.as_internal().get_type() {
-            Err(_) => vovf.into_value_untyped(),
-            Ok(t) => match &*t.as_whnf() {
-                ValueF::Pi(x, _, e) => {
-                    let t = e.subst_shift(&x.into(), &v);
-                    vovf.into_value_with_type(t)
-                }
-                _ => unreachable!("Internal type error"),
-            },
+        let t = self.get_type_not_sort();
+        let vovf = apply_any(self.clone(), v.clone(), &t);
+        let t_borrow = t.as_whnf();
+        match &*t_borrow {
+            ValueF::Pi(x, _, e) => {
+                let t = e.subst_shift(&x.into(), &v);
+                vovf.into_value_with_type(t)
+            }
+            _ => unreachable!("Internal type error"),
         }
     }
 
     pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
         Ok(self.as_internal().get_type()?.clone())
     }
+    /// When we know the value isn't `Sort`, this gets the type directly
+    pub(crate) fn get_type_not_sort(&self) -> Value {
+        self.get_type()
+            .expect("Internal type error: value is `Sort` but shouldn't be")
+    }
 }
 
 impl VoVF {
-    pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF {
+    pub(crate) fn into_whnf(self, ty: &Value) -> ValueF {
         match self {
             VoVF::ValueF {
                 val,
@@ -256,7 +267,7 @@ impl VoVF {
             VoVF::Value(v) => {
                 let v_ty = v.get_type().ok();
                 debug_assert_eq!(
-                    ty,
+                    Some(ty),
                     v_ty.as_ref(),
                     "The type recovered from normalization doesn't match the stored type."
                 );
@@ -264,12 +275,6 @@ impl VoVF {
             }
         }
     }
-    pub(crate) fn into_value_untyped(self) -> Value {
-        match self {
-            VoVF::Value(v) => v,
-            VoVF::ValueF { val, form } => Value::new(val, form, None),
-        }
-    }
     pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
         match self {
             VoVF::Value(v) => {
@@ -288,7 +293,8 @@ impl VoVF {
     pub(crate) fn app(self, x: Value) -> VoVF {
         VoVF::Value(match self {
             VoVF::Value(v) => v.app(x),
-            VoVF::ValueF { val, .. } => val.into_value_untyped().app(x),
+            // TODO: this is very wrong
+            VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x),
         })
     }
 }
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 42606a9..5638078 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -47,9 +47,6 @@ pub(crate) enum ValueF {
 }
 
 impl ValueF {
-    pub(crate) fn into_value_untyped(self) -> Value {
-        Value::from_valuef_untyped(self)
-    }
     pub(crate) fn into_value_with_type(self, t: Value) -> Value {
         Value::from_valuef_and_type(self, t)
     }
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13a9d7e..2ddaf3d 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -54,7 +54,6 @@ pub(crate) enum TypeMessage {
     NotAFunction(Value),
     TypeMismatch(Value, Value, Value),
     AnnotMismatch(Value, Value),
-    Untyped,
     InvalidListElement(usize, Value, Value),
     InvalidListType(Value),
     InvalidOptionalType(Value),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index fe99696..9837a8b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -46,7 +46,7 @@ macro_rules! make_closure {
         let var: AlphaLabel = Label::from(stringify!($var)).into();
         let ty = make_closure!($($ty)*);
         let body = make_closure!($($body)*);
-        let body_ty = body.get_type().expect("Internal type error");
+        let body_ty = body.get_type_not_sort();
         let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
             .into_value_with_type(Value::from_const(Type));
         ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
@@ -60,7 +60,7 @@ macro_rules! make_closure {
     };
     (Some($($rest:tt)*)) => {{
         let v = make_closure!($($rest)*);
-        let v_type = v.get_type().expect("Internal type error");
+        let v_type = v.get_type_not_sort();
         let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
         ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
     }};
@@ -79,7 +79,7 @@ macro_rules! make_closure {
     ([ $($head:tt)* ] # $($tail:tt)*) => {{
         let head = make_closure!($($head)*);
         let tail = make_closure!($($tail)*);
-        let list_type = tail.get_type().expect("Internal type error");
+        let list_type = tail.get_type_not_sort();
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
             ValueF::NEListLit(vec![head])
@@ -90,11 +90,7 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(
-    b: Builtin,
-    args: Vec<Value>,
-    _ty: Option<&Value>,
-) -> VoVF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
     use dhall_syntax::Builtin::*;
     use ValueF::*;
 
@@ -251,9 +247,7 @@ pub(crate) fn apply_builtin(
                     // Extract the type of the list elements
                     let t = match &*l_whnf {
                         EmptyListLit(t) => t.clone(),
-                        NEListLit(xs) => {
-                            xs[0].get_type().expect("Internal type error")
-                        }
+                        NEListLit(xs) => xs[0].get_type_not_sort(),
                         _ => unreachable!(),
                     };
 
@@ -429,7 +423,7 @@ pub(crate) fn apply_builtin(
     }
 }
 
-pub(crate) fn apply_any(f: Value, a: Value, ty: Option<&Value>) -> VoVF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF {
     let fallback = |f: Value, a: Value| {
         ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
     };
@@ -524,7 +518,7 @@ fn apply_binop<'a>(
     o: BinOp,
     x: &'a Value,
     y: &'a Value,
-    ty: Option<&Value>,
+    ty: &Value,
 ) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
@@ -618,7 +612,6 @@ fn apply_binop<'a>(
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let ty = ty.expect("Internal type error");
             let ty_borrow = ty.as_whnf();
             let kts = match &*ty_borrow {
                 RecordType(kts) => kts,
@@ -647,7 +640,7 @@ fn apply_binop<'a>(
 
 pub(crate) fn normalize_one_layer(
     expr: ExprF<Value, Normalized>,
-    ty: Option<&Value>,
+    ty: &Value,
 ) -> VoVF {
     use ValueF::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
@@ -808,7 +801,7 @@ pub(crate) fn normalize_one_layer(
 }
 
 /// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: Option<&Value>) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF {
     match v {
         ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
         ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 270191a..ef2018a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-fn type_of_const(c: Const) -> Result<Value, TypeError> {
-    match c {
-        Const::Type => Ok(const_to_value(Const::Kind)),
-        Const::Kind => Ok(const_to_value(Const::Sort)),
-        Const::Sort => {
-            Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
-        }
-    }
-}
-
 pub(crate) fn const_to_value(c: Const) -> Value {
     let v = ValueF::Const(c);
-    match type_of_const(c) {
-        Ok(t) => Value::from_valuef_and_type(v, t),
-        Err(_) => Value::from_valuef_untyped(v),
+    match c {
+        Const::Type => {
+            Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+        }
+        Const::Kind => {
+            Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+        }
+        Const::Sort => Value::const_sort(),
     }
 }