Embrace TypeInternal as a semantic value

4 files changed, 25 insertions, 9 deletions

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 03aa966..44d1612 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -72,6 +72,15 @@ pub(crate) use crate::typecheck::TypeInternal;
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct Type<'a>(pub(crate) TypeInternal<'a>);
 
+impl<'a> std::fmt::Display for Type<'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+        match self.0.clone().into_normalized() {
+            Ok(e) => e.fmt(f),
+            Err(_) => write!(f, "SuperType"),
+        }
+    }
+}
+
 // Exposed for the macros
 #[doc(hidden)]
 impl<'a> From<SimpleType<'a>> for SubExpr<X, X> {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f092c4d..7aa8686 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -322,6 +322,7 @@ enum WHNF {
         (NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
     ),
     TextLit(Vec<InterpolatedTextContents<Now>>),
+    /// This must not contain a value captured by one of the variants above.
     Expr(OutputSubExpr),
 }
 
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 7f85b5c..c945b23 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -140,7 +140,7 @@ pub fn run_test(
                 TypeInference => {
                     let expr = expr.typecheck()?;
                     let ty = expr.get_type()?;
-                    assert_eq_display!(ty.as_normalized()?.as_ref(), &expected);
+                    assert_eq_display!(ty.as_ref(), &expected.into_type());
                 }
                 Normalization => {
                     let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 99fb003..b0ea63e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -61,9 +61,7 @@ impl Normalized<'static> {
     }
 }
 impl<'a> Type<'a> {
-    pub(crate) fn as_normalized(
-        &self,
-    ) -> Result<Cow<Normalized<'a>>, TypeError> {
+    fn as_normalized(&self) -> Result<Cow<Normalized<'a>>, TypeError> {
         match &self.0 {
             TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)),
             TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))),
@@ -84,6 +82,9 @@ impl<'a> Type<'a> {
             Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
         }
     }
+    fn internal(&self) -> &TypeInternal {
+        &self.0
+    }
     fn shift0(&self, delta: isize, label: &Label) -> Self {
         use TypeInternal::*;
         Type(match &self.0 {
@@ -109,16 +110,21 @@ impl Type<'static> {
     }
 }
 
+/// A semantic type. This is partially redundant with `dhall_core::Expr`, on purpose. `TypeInternal` should
+/// be limited to syntactic expressions: either written by the user or meant to be printed.
+/// The rule is the following: we must _not_ construct values of type `Expr` while typechecking,
+/// but only construct `TypeInternal`s.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum TypeInternal<'a> {
-    Expr(Box<Normalized<'a>>),
-    Const(dhall_core::Const),
+    Const(Const),
     /// The type of `Sort`
     SuperType,
+    /// This must not contain a value captured by one of the variants above.
+    Expr(Box<Normalized<'a>>),
 }
 
 impl<'a> TypeInternal<'a> {
-    fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
+    pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
         match self {
             TypeInternal::Expr(e) => Ok(*e),
             TypeInternal::Const(c) => Ok(const_to_normalized(c)),
@@ -348,8 +354,8 @@ macro_rules! ensure_simple_type {
 
 macro_rules! ensure_is_const {
     ($x:expr, $err:expr $(,)*) => {
-        match $x.unroll_ref()?.as_ref() {
-            Const(k) => *k,
+        match $x.internal() {
+            TypeInternal::Const(k) => *k,
             _ => return Err($err),
         }
     };