From db3ca819283f9bd99d197de464717f0b58b52fe4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 17:07:11 +0200
Subject: Instead of possibly nonexistent Type, treat Sort specially

---
 dhall/src/expr.rs                | 158 +++++++++++++++++-----
 dhall/src/normalize.rs           |  50 +++----
 dhall/src/tests.rs               |   9 +-
 dhall/src/traits/deserialize.rs  |   2 +-
 dhall/src/traits/dynamic_type.rs |  24 +---
 dhall/src/traits/static_type.rs  |   8 +-
 dhall/src/typecheck.rs           | 273 +++++++++++++++++----------------------
 7 files changed, 282 insertions(+), 242 deletions(-)

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index a753ffd..4d55f4a 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,4 +1,5 @@
 use crate::imports::ImportRoot;
+use crate::normalize::{Thunk, Value};
 use dhall_core::*;
 use std::marker::PhantomData;
 
@@ -36,23 +37,23 @@ pub(crate) struct Resolved<'a>(
 );
 derive_other_traits!(Resolved);
 
+pub(crate) use self::typed::TypedInternal;
+
 #[derive(Debug, Clone)]
 pub(crate) struct Typed<'a>(
-    pub(crate) crate::normalize::Thunk,
-    pub(crate) Option<Type<'static>>,
+    pub(crate) TypedInternal,
     pub(crate) PhantomData<&'a ()>,
 );
 
 #[derive(Debug, Clone)]
 pub(crate) struct Normalized<'a>(
-    pub(crate) crate::normalize::Thunk,
-    pub(crate) Option<Type<'static>>,
+    pub(crate) TypedInternal,
     pub(crate) PhantomData<&'a ()>,
 );
 
 impl<'a> std::cmp::PartialEq for Normalized<'a> {
     fn eq(&self, other: &Self) -> bool {
-        self.0.normalize_to_expr() == other.0.normalize_to_expr()
+        self.to_expr() == other.to_expr()
     }
 }
 
@@ -60,7 +61,110 @@ impl<'a> std::cmp::Eq for Normalized<'a> {}
 
 impl<'a> std::fmt::Display for Normalized<'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.0.normalize_to_expr().fmt(f)
+        self.to_expr().fmt(f)
+    }
+}
+
+mod typed {
+    use super::{Type, Typed};
+    use crate::normalize::{Thunk, Value};
+    use crate::typecheck::{
+        TypeError, TypeInternal, TypeMessage, TypecheckContext,
+    };
+    use dhall_core::{Const, Label, SubExpr, V, X};
+    use std::borrow::Cow;
+    use std::marker::PhantomData;
+
+    #[derive(Debug, Clone)]
+    pub(crate) enum TypedInternal {
+        // The `Sort` higher-kinded type doesn't have a type
+        Sort,
+        // Any other value, along with its type
+        Value(Thunk, Option<Type<'static>>),
+    }
+
+    impl TypedInternal {
+        pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+            TypedInternal::Value(th, Some(t))
+        }
+
+        pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+            TypedInternal::Value(th, None)
+        }
+
+        // TODO: Avoid cloning if possible
+        pub(crate) fn to_value(&self) -> Value {
+            match self {
+                TypedInternal::Value(th, _) => th.normalize_whnf().clone(),
+                TypedInternal::Sort => Value::Const(Const::Sort),
+            }
+        }
+
+        pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+            self.to_value().normalize_to_expr()
+        }
+
+        pub(crate) fn to_thunk(&self) -> Thunk {
+            match self {
+                TypedInternal::Value(th, _) => th.clone(),
+                TypedInternal::Sort => {
+                    Thunk::from_whnf(Value::Const(Const::Sort))
+                }
+            }
+        }
+
+        pub(crate) fn to_type(&self) -> Type<'static> {
+            match self {
+                TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)),
+                TypedInternal::Value(th, _) => match &*th.normalize_whnf() {
+                    Value::Const(c) => Type(TypeInternal::Const(*c)),
+                    _ => Type(TypeInternal::Typed(Box::new(Typed(
+                        self.clone(),
+                        PhantomData,
+                    )))),
+                },
+            }
+        }
+
+        pub(crate) fn get_type(
+            &self,
+        ) -> Result<Cow<'_, Type<'static>>, TypeError> {
+            match self {
+                TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
+                TypedInternal::Value(_, None) => Err(TypeError::new(
+                    &TypecheckContext::new(),
+                    TypeMessage::Untyped,
+                )),
+                TypedInternal::Sort => Err(TypeError::new(
+                    &TypecheckContext::new(),
+                    TypeMessage::Sort,
+                )),
+            }
+        }
+
+        pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+            match self {
+                TypedInternal::Value(th, t) => TypedInternal::Value(
+                    th.shift(delta, var),
+                    t.as_ref().map(|x| x.shift(delta, var)),
+                ),
+                TypedInternal::Sort => TypedInternal::Sort,
+            }
+        }
+
+        pub(crate) fn subst_shift(
+            &self,
+            var: &V<Label>,
+            val: &Typed<'static>,
+        ) -> Self {
+            match self {
+                TypedInternal::Value(th, t) => TypedInternal::Value(
+                    th.subst_shift(var, val),
+                    t.as_ref().map(|x| x.subst_shift(var, val)),
+                ),
+                TypedInternal::Sort => TypedInternal::Sort,
+            }
+        }
     }
 }
 
@@ -88,10 +192,7 @@ 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"),
-        }
+        self.to_normalized().fmt(f)
     }
 }
 
@@ -115,39 +216,38 @@ impl<'a> From<SubExpr<X, X>> for SimpleType<'a> {
 #[doc(hidden)]
 impl<'a> From<Normalized<'a>> for Typed<'a> {
     fn from(x: Normalized<'a>) -> Typed<'a> {
-        Typed(x.0, x.1, x.2)
+        Typed(x.0, x.1)
     }
 }
 
 impl<'a> Normalized<'a> {
+    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+        Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+    }
     // Deprecated
     pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
-        self.0.normalize_to_expr()
+        self.0.to_expr()
     }
     pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
-        self.0.normalize_to_expr()
+        self.0.to_expr()
     }
-    pub(crate) fn to_value(&self) -> crate::normalize::Value {
-        self.0.normalize_nf().clone()
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
     }
     #[allow(dead_code)]
     pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
-        Normalized(self.0, self.1, PhantomData)
+        Normalized(self.0, PhantomData)
     }
 }
 
-#[doc(hidden)]
-impl<'a> Type<'a> {
-    pub(crate) fn unnote<'b>(self) -> Type<'b> {
-        // use TypeInternal::*;
-        // Type(match self.0 {
-        //     Expr(e) => Expr(Box::new(e.unnote())),
-        //     Pi(ctx, c, x, t, e) => Pi(ctx, c, x, t, e),
-        //     Const(c) => Const(c),
-        //     SuperType => SuperType,
-        // })
-
-        // Yes, this is positively horrible. Please forgive me.
-        unsafe { std::mem::transmute::<Type<'a>, Type<'b>>(self) }
+impl<'a> Typed<'a> {
+    pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+        Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+    }
+    pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+        Typed(TypedInternal::from_thunk_untyped(th), PhantomData)
+    }
+    pub(crate) fn const_sort() -> Self {
+        Typed(TypedInternal::Sort, PhantomData)
     }
 }
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 390911a..a023d38 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_core::{
 };
 use dhall_generator as dhall;
 
-use crate::expr::{Normalized, Type, Typed};
+use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
 type InputSubExpr = SubExpr<X, Normalized<'static>>;
 type OutputSubExpr = SubExpr<X, X>;
@@ -25,11 +25,17 @@ impl<'a> Typed<'a> {
     /// leave ill-typed sub-expressions unevaluated.
     ///
     pub fn normalize(self) -> Normalized<'a> {
-        // TODO: stupid but needed for now
-        let thunk = Thunk::from_normalized_expr(self.0.normalize_to_expr());
-        // let thunk = self.0;
-        thunk.normalize_nf();
-        Normalized(thunk, self.1, self.2)
+        let internal = match self.0 {
+            TypedInternal::Sort => TypedInternal::Sort,
+            TypedInternal::Value(thunk, t) => {
+                // TODO: stupid but needed for now
+                let thunk =
+                    Thunk::from_normalized_expr(thunk.normalize_to_expr());
+                thunk.normalize_nf();
+                TypedInternal::Value(thunk, t)
+            }
+        };
+        Normalized(internal, self.1)
     }
 
     pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
@@ -37,11 +43,7 @@ impl<'a> Typed<'a> {
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        Typed(
-            self.0.shift(delta, var),
-            self.1.as_ref().map(|x| x.shift(delta, var)),
-            self.2,
-        )
+        Typed(self.0.shift(delta, var), self.1)
     }
 
     pub(crate) fn subst_shift(
@@ -49,19 +51,15 @@ impl<'a> Typed<'a> {
         var: &V<Label>,
         val: &Typed<'static>,
     ) -> Self {
-        Typed(
-            self.0.subst_shift(var, val),
-            self.1.as_ref().map(|x| x.subst_shift(var, val)),
-            self.2,
-        )
+        Typed(self.0.subst_shift(var, val), self.1)
     }
 
-    pub(crate) fn normalize_whnf(&self) -> std::cell::Ref<Value> {
-        self.0.normalize_whnf()
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
     }
 
-    pub(crate) fn as_thunk(&self) -> Thunk {
-        self.0.clone()
+    pub(crate) fn to_thunk(&self) -> Thunk {
+        self.0.to_thunk()
     }
 }
 
@@ -278,7 +276,7 @@ impl EnvItem {
     ) -> Self {
         match self {
             EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
-            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()),
+            EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
             EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
         }
     }
@@ -695,7 +693,10 @@ impl Value {
 
         match self {
             Value::Lam(x, _, e) => {
-                let val = Typed(th, None, std::marker::PhantomData);
+                let val = Typed(
+                    TypedInternal::Value(th, None),
+                    std::marker::PhantomData,
+                );
                 e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
             }
             Value::AppliedBuiltin(b, mut args) => {
@@ -867,7 +868,7 @@ impl Value {
                 t.subst_shift(var, val),
                 e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
             ),
-            Value::Var(v) if v == var => val.normalize_whnf().clone(),
+            Value::Var(v) if v == var => val.to_value().clone(),
             Value::Var(v) => Value::Var(v.shift(-1, var)),
             Value::Const(c) => Value::Const(*c),
             Value::BoolLit(b) => Value::BoolLit(*b),
@@ -1163,8 +1164,7 @@ impl TypeThunk {
     pub(crate) fn normalize_nf(&self) -> Value {
         match self {
             TypeThunk::Thunk(th) => th.normalize_nf().clone(),
-            // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
+            TypeThunk::Type(t) => t.to_value().normalize(),
         }
     }
 
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index ebca256..ecd6e43 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -134,15 +134,12 @@ pub fn run_test(
                     assert_eq_display!(expr, expected);
                 }
                 Typecheck => {
-                    expr.typecheck_with(&expected.into_type()?)?;
+                    expr.typecheck_with(&expected.to_type())?;
                 }
                 TypeInference => {
                     let expr = expr.typecheck()?;
-                    let ty = expr.get_type()?;
-                    assert_eq_display!(
-                        ty.as_normalized()?.as_expr(),
-                        expected.into_type()?.as_normalized()?.as_expr()
-                    );
+                    let ty = expr.get_type()?.into_owned();
+                    assert_eq_display!(ty.to_normalized(), expected);
                 }
                 Normalization => {
                     let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs
index 9cc2147..99ca5ee 100644
--- a/dhall/src/traits/deserialize.rs
+++ b/dhall/src/traits/deserialize.rs
@@ -48,6 +48,6 @@ impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> {
 
 impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> {
     fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> {
-        Ok(Normalized::from_str(s, ty)?.into_type()?)
+        Ok(Normalized::from_str(s, ty)?.to_type())
     }
 }
diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs
index c15b277..74c2e0a 100644
--- a/dhall/src/traits/dynamic_type.rs
+++ b/dhall/src/traits/dynamic_type.rs
@@ -1,9 +1,7 @@
 use crate::expr::*;
 use crate::traits::StaticType;
 #[allow(unused_imports)]
-use crate::typecheck::{
-    type_of_const, TypeError, TypeMessage, TypecheckContext,
-};
+use crate::typecheck::{TypeError, TypeMessage, TypecheckContext};
 #[allow(unused_imports)]
 use dhall_core::{Const, ExprF};
 use std::borrow::Cow;
@@ -20,32 +18,18 @@ impl<T: StaticType> DynamicType for T {
 
 impl<'a> DynamicType for Type<'a> {
     fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
-        Ok(Cow::Owned(
-            self.clone().into_normalized()?.get_type()?.into_owned(),
-        ))
+        self.get_type()
     }
 }
 
 impl<'a> DynamicType for Normalized<'a> {
     fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
-        match &self.1 {
-            Some(t) => Ok(Cow::Borrowed(t)),
-            None => Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Untyped,
-            )),
-        }
+        self.0.get_type()
     }
 }
 
 impl<'a> DynamicType for Typed<'a> {
     fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
-        match &self.1 {
-            Some(t) => Ok(Cow::Borrowed(t)),
-            None => Err(TypeError::new(
-                &TypecheckContext::new(),
-                TypeMessage::Untyped,
-            )),
-        }
+        self.0.get_type()
     }
 }
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index 4dd9961..df6a177 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -38,15 +38,13 @@ fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> {
 
 impl<T: SimpleStaticType> StaticType for T {
     fn get_static_type() -> Type<'static> {
-        crate::expr::Normalized(
+        crate::expr::Normalized::from_thunk_and_type(
             crate::normalize::Thunk::from_normalized_expr(
                 T::get_simple_static_type().into(),
             ),
-            Some(Type::const_type()),
-            std::marker::PhantomData,
+            Type::const_type(),
         )
-        .into_type()
-        .unwrap()
+        .to_type()
     }
 }
 
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8afbb2b..582930b 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -3,7 +3,6 @@ use std::borrow::Borrow;
 use std::borrow::Cow;
 use std::collections::BTreeMap;
 use std::fmt;
-use std::marker::PhantomData;
 
 use crate::expr::*;
 use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value};
@@ -24,71 +23,52 @@ impl<'a> Resolved<'a> {
         ty: &Type,
     ) -> Result<Typed<'static>, TypeError> {
         let expr: SubExpr<_, _> = self.0.unnote();
-        let ty: SubExpr<_, _> = ty.clone().unnote().embed()?;
-        type_of(dhall::subexpr!(expr: ty))
+        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd();
+        type_of(rc(ExprF::Annot(expr, ty)))
     }
     /// Pretends this expression has been typechecked. Use with care.
     #[allow(dead_code)]
     pub fn skip_typecheck(self) -> Typed<'a> {
-        Typed(
-            Thunk::new(NormalizationContext::new(), self.0.unnote()),
-            None,
-            PhantomData,
-        )
+        Typed::from_thunk_untyped(Thunk::new(
+            NormalizationContext::new(),
+            self.0.unnote(),
+        ))
     }
 }
+
 impl<'a> Typed<'a> {
-    fn get_type_move(self) -> Result<Type<'static>, TypeError> {
-        self.1.ok_or_else(|| {
-            TypeError::new(&TypecheckContext::new(), TypeMessage::Untyped)
-        })
+    fn to_type(&self) -> Type<'a> {
+        match &self.to_value() {
+            Value::Const(c) => Type(TypeInternal::Const(*c)),
+            _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
+        }
     }
 }
+
 impl<'a> Normalized<'a> {
     fn shift0(&self, delta: isize, label: &Label) -> Self {
         self.shift(delta, &V(label.clone(), 0))
     }
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        Normalized(
-            self.0.shift(delta, var),
-            self.1.as_ref().map(|t| t.shift(delta, var)),
-            self.2,
-        )
+        Normalized(self.0.shift(delta, var), self.1)
     }
-    pub(crate) fn into_type(self) -> Result<Type<'a>, TypeError> {
-        let typed: Typed = self.into();
-        Ok(typed.to_type())
-    }
-    fn get_type_move(self) -> Result<Type<'static>, TypeError> {
-        self.1.ok_or_else(|| {
-            TypeError::new(&TypecheckContext::new(), TypeMessage::Untyped)
-        })
-    }
-}
-impl Normalized<'static> {
-    fn embed<N>(self) -> SubExpr<N, Normalized<'static>> {
-        rc(ExprF::Embed(self))
-    }
-}
-impl<'a> Typed<'a> {
-    fn to_type(&self) -> Type<'a> {
-        match &*self.normalize_whnf() {
-            Value::Const(c) => Type(TypeInternal::Const(*c)),
-            _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
-        }
+    pub(crate) fn to_type(self) -> Type<'a> {
+        self.0.to_type()
     }
 }
+
 impl<'a> Type<'a> {
-    pub(crate) fn as_normalized(
-        &self,
-    ) -> Result<Cow<Normalized<'a>>, TypeError> {
-        Ok(Cow::Owned(self.0.clone().into_normalized()?))
+    pub(crate) fn to_normalized(&self) -> Normalized<'a> {
+        self.0.to_normalized()
+    }
+    pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+        self.0.to_expr()
     }
-    pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
-        self.0.into_normalized()
+    pub(crate) fn to_value(&self) -> Value {
+        self.0.to_value()
     }
-    pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> {
-        Ok(self.0.normalize_whnf()?)
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
+        self.0.get_type()
     }
     fn as_const(&self) -> Option<Const> {
         self.0.as_const()
@@ -96,7 +76,7 @@ impl<'a> Type<'a> {
     fn internal(&self) -> &TypeInternal<'a> {
         &self.0
     }
-    fn internal_whnf(&self) -> Option<std::cell::Ref<Value>> {
+    fn internal_whnf(&self) -> Option<Value> {
         self.0.whnf()
     }
     pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
@@ -123,14 +103,9 @@ impl<'a> Type<'a> {
         Type(TypeInternal::Const(Const::Type))
     }
 }
-impl Type<'static> {
-    fn embed<N>(self) -> Result<SubExpr<N, Normalized<'static>>, TypeError> {
-        Ok(self.into_normalized()?.embed())
-    }
-}
 
 impl TypeThunk {
-    fn normalize_to_type(
+    fn to_type(
         &self,
         ctx: &TypecheckContext,
     ) -> Result<Type<'static>, TypeError> {
@@ -138,10 +113,7 @@ impl TypeThunk {
             TypeThunk::Type(t) => Ok(t.clone()),
             TypeThunk::Thunk(th) => {
                 // TODO: rule out statically
-                mktype(
-                    ctx,
-                    th.normalize_whnf().normalize_to_expr().embed_absurd(),
-                )
+                mktype(ctx, th.normalize_to_expr().embed_absurd())
             }
         }
     }
@@ -154,29 +126,30 @@ impl TypeThunk {
 #[derive(Debug, Clone)]
 pub(crate) enum TypeInternal<'a> {
     Const(Const),
-    /// The type of `Sort`
-    SuperType,
-    /// This must not contain Const value.
+    /// This must not contain a Const value.
     Typed(Box<Typed<'a>>),
 }
 
 impl<'a> TypeInternal<'a> {
-    pub(crate) fn into_normalized(&self) -> Result<Normalized<'a>, TypeError> {
-        Ok(self.as_typed()?.normalize())
+    fn to_typed(&self) -> Typed<'a> {
+        match self {
+            TypeInternal::Typed(e) => e.as_ref().clone(),
+            TypeInternal::Const(c) => const_to_typed(*c),
+        }
+    }
+    fn to_normalized(&self) -> Normalized<'a> {
+        self.to_typed().normalize()
     }
-    fn normalize_whnf(&self) -> Result<Value, TypeError> {
-        Ok(self.as_typed()?.normalize_whnf().clone())
+    fn to_expr(&self) -> SubExpr<X, X> {
+        self.to_normalized().to_expr()
     }
-    fn as_typed(&self) -> Result<Typed<'a>, TypeError> {
+    fn to_value(&self) -> Value {
+        self.to_typed().to_value().clone()
+    }
+    pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
         Ok(match self {
-            TypeInternal::Typed(e) => e.as_ref().clone(),
-            TypeInternal::Const(c) => const_to_typed(*c),
-            TypeInternal::SuperType => {
-                return Err(TypeError::new(
-                    &TypecheckContext::new(),
-                    TypeMessage::Untyped,
-                ))
-            }
+            TypeInternal::Typed(e) => e.get_type()?,
+            TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?),
         })
     }
     fn as_const(&self) -> Option<Const> {
@@ -185,9 +158,9 @@ impl<'a> TypeInternal<'a> {
             _ => None,
         }
     }
-    fn whnf(&self) -> Option<std::cell::Ref<Value>> {
+    fn whnf(&self) -> Option<Value> {
         match self {
-            TypeInternal::Typed(e) => Some(e.normalize_whnf()),
+            TypeInternal::Typed(e) => Some(e.to_value()),
             _ => None,
         }
     }
@@ -199,7 +172,6 @@ impl<'a> TypeInternal<'a> {
         match self {
             Typed(e) => Typed(Box::new(e.shift(delta, var))),
             Const(c) => Const(*c),
-            SuperType => SuperType,
         }
     }
     fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
@@ -207,7 +179,6 @@ impl<'a> TypeInternal<'a> {
         match self {
             Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
             Const(c) => Const(*c),
-            SuperType => SuperType,
         }
     }
 }
@@ -215,12 +186,7 @@ impl<'a> TypeInternal<'a> {
 impl<'a> Eq for TypeInternal<'a> {}
 impl<'a> PartialEq for TypeInternal<'a> {
     fn eq(&self, other: &Self) -> bool {
-        let self_nzed = self.clone().into_normalized();
-        let other_nzed = other.clone().into_normalized();
-        match (self_nzed, other_nzed) {
-            (Ok(x), Ok(y)) => x == y,
-            _ => false,
-        }
+        self.to_normalized() == other.to_normalized()
     }
 }
 
@@ -369,17 +335,14 @@ where
         }
     }
     match (eL0.borrow().internal(), eR0.borrow().internal()) {
-        (TypeInternal::SuperType, TypeInternal::SuperType) => true,
-        (TypeInternal::SuperType, _) => false,
-        (_, TypeInternal::SuperType) => false,
         // (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
         // (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
         _ => {
             let mut ctx = vec![];
             go(
                 &mut ctx,
-                &eL0.borrow().as_normalized().unwrap().to_expr(),
-                &eR0.borrow().as_normalized().unwrap().to_expr(),
+                &eL0.borrow().to_expr(),
+                &eR0.borrow().to_expr(),
             )
         }
         // _ => false,
@@ -387,22 +350,29 @@ where
 }
 
 fn const_to_typed<'a>(c: Const) -> Typed<'a> {
-    Typed(
-        Value::Const(c).into_thunk(),
-        Some(type_of_const(c)),
-        PhantomData,
-    )
+    match c {
+        Const::Sort => Typed::const_sort(),
+        _ => Typed::from_thunk_and_type(
+            Value::Const(c).into_thunk(),
+            type_of_const(c).unwrap(),
+        ),
+    }
 }
 
 fn const_to_type<'a>(c: Const) -> Type<'a> {
     Type(TypeInternal::Const(c))
 }
 
-pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> {
+fn type_of_const<'a>(c: Const) -> Result<Type<'a>, TypeError> {
     match c {
-        Const::Type => Type::const_kind(),
-        Const::Kind => Type::const_sort(),
-        Const::Sort => Type(TypeInternal::SuperType),
+        Const::Type => Ok(Type::const_kind()),
+        Const::Kind => Ok(Type::const_sort()),
+        Const::Sort => {
+            return Err(TypeError::new(
+                &TypecheckContext::new(),
+                TypeMessage::Sort,
+            ))
+        }
     }
 }
 
@@ -512,7 +482,7 @@ impl TypeIntermediate {
                     _ => {
                         return Err(mkerr(
                             ctx,
-                            InvalidInputType(ta.clone().into_normalized()?),
+                            InvalidInputType(ta.clone().to_normalized()),
                         ))
                     }
                 };
@@ -524,9 +494,9 @@ impl TypeIntermediate {
                             &ctx2,
                             InvalidOutputType(
                                 tb.clone()
-                                    .into_normalized()?
-                                    .get_type_move()?
-                                    .into_normalized()?,
+                                    .to_normalized()
+                                    .get_type()?
+                                    .to_normalized(),
                             ),
                         ))
                     }
@@ -538,25 +508,24 @@ impl TypeIntermediate {
                         return Err(mkerr(
                             ctx,
                             NoDependentTypes(
-                                ta.clone().into_normalized()?,
+                                ta.clone().to_normalized(),
                                 tb.clone()
-                                    .into_normalized()?
-                                    .get_type_move()?
-                                    .into_normalized()?,
+                                    .to_normalized()
+                                    .get_type()?
+                                    .to_normalized(),
                             ),
                         ))
                     }
                 };
 
-                Typed(
+                Typed::from_thunk_and_type(
                     Value::Pi(
                         x.clone(),
                         TypeThunk::from_type(ta.clone()),
                         TypeThunk::from_type(tb.clone()),
                     )
                     .into_thunk(),
-                    Some(const_to_type(k)),
-                    PhantomData,
+                    const_to_type(k),
                 )
             }
             TypeIntermediate::RecordType(ctx, kts) => {
@@ -577,7 +546,7 @@ impl TypeIntermediate {
                 // An empty record type has type Type
                 let k = k.unwrap_or(dhall_core::Const::Type);
 
-                Typed(
+                Typed::from_thunk_and_type(
                     Value::RecordType(
                         kts.iter()
                             .map(|(k, t)| {
@@ -586,8 +555,7 @@ impl TypeIntermediate {
                             .collect(),
                     )
                     .into_thunk(),
-                    Some(const_to_type(k)),
-                    PhantomData,
+                    const_to_type(k),
                 )
             }
             TypeIntermediate::UnionType(ctx, kts) => {
@@ -612,7 +580,7 @@ impl TypeIntermediate {
                 // an union type with only unary variants also has type Type
                 let k = k.unwrap_or(dhall_core::Const::Type);
 
-                Typed(
+                Typed::from_thunk_and_type(
                     Value::UnionType(
                         kts.iter()
                             .map(|(k, t)| {
@@ -626,37 +594,31 @@ impl TypeIntermediate {
                             .collect(),
                     )
                     .into_thunk(),
-                    Some(const_to_type(k)),
-                    PhantomData,
+                    const_to_type(k),
                 )
             }
             TypeIntermediate::ListType(ctx, t) => {
                 ensure_simple_type!(
                     t,
-                    mkerr(ctx, InvalidListType(t.clone().into_normalized()?)),
+                    mkerr(ctx, InvalidListType(t.clone().to_normalized())),
                 );
-                Typed(
+                Typed::from_thunk_and_type(
                     Value::from_builtin(Builtin::List)
-                        .app(t.normalize_whnf()?)
+                        .app(t.to_value())
                         .into_thunk(),
-                    Some(const_to_type(Const::Type)),
-                    PhantomData,
+                    const_to_type(Const::Type),
                 )
             }
             TypeIntermediate::OptionalType(ctx, t) => {
                 ensure_simple_type!(
                     t,
-                    mkerr(
-                        ctx,
-                        InvalidOptionalType(t.clone().into_normalized()?)
-                    ),
+                    mkerr(ctx, InvalidOptionalType(t.clone().to_normalized())),
                 );
-                Typed(
+                Typed::from_thunk_and_type(
                     Value::from_builtin(Builtin::Optional)
-                        .app(t.normalize_whnf()?)
+                        .app(t.to_value())
                         .into_thunk(),
-                    Some(const_to_type(Const::Type)),
-                    PhantomData,
+                    const_to_type(Const::Type),
                 )
             }
         })
@@ -701,7 +663,7 @@ fn type_with(
             let tx = mktype(ctx, t.clone())?;
             let ctx2 = ctx.insert_type(x, tx.clone());
             let b = type_with(&ctx2, b.clone())?;
-            let tb = b.get_type_move()?;
+            let tb = b.get_type()?.into_owned();
             Ok(RetType(
                 TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
                     .typecheck()?
@@ -727,7 +689,7 @@ fn type_with(
             let v = type_with(ctx, v)?.normalize();
             let e = type_with(&ctx.insert_value(x, v.clone()), e.clone())?;
 
-            Ok(RetType(e.get_type_move()?))
+            Ok(RetType(e.get_type()?.into_owned()))
         }
         OldOptionalLit(None, t) => {
             let t = t.clone();
@@ -749,15 +711,13 @@ fn type_with(
         ),
     }?;
     Ok(match ret {
-        RetExpr(ret) => Typed(
+        RetExpr(ret) => Typed::from_thunk_and_type(
             Thunk::new(ctx.to_normalization_ctx(), e),
-            Some(mktype(ctx, rc(ret))?),
-            PhantomData,
+            mktype(ctx, rc(ret))?,
         ),
-        RetType(typ) => Typed(
+        RetType(typ) => Typed::from_thunk_and_type(
             Thunk::new(ctx.to_normalization_ctx(), e),
-            Some(typ),
-            PhantomData,
+            typ,
         ),
         RetTyped(tt) => tt,
     })
@@ -787,7 +747,7 @@ fn type_last_layer(
         App(f, a) => {
             let tf = f.get_type()?;
             let tf_internal = tf.internal_whnf();
-            let (x, tx, tb) = match tf_internal.deref() {
+            let (x, tx, tb) = match &tf_internal {
                 Some(Value::Pi(
                     x,
                     TypeThunk::Type(tx),
@@ -799,7 +759,7 @@ fn type_last_layer(
                 _ => return Err(mkerr(NotAFunction(f.clone()))),
             };
             ensure_equal!(a.get_type()?, tx, {
-                mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a))
+                mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
             });
 
             Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
@@ -809,9 +769,9 @@ fn type_last_layer(
             ensure_equal!(
                 &t,
                 x.get_type()?,
-                mkerr(AnnotMismatch(x, t.into_normalized()?))
+                mkerr(AnnotMismatch(x, t.to_normalized()))
             );
-            Ok(RetType(x.get_type_move()?))
+            Ok(RetType(x.get_type()?.into_owned()))
         }
         BoolIf(x, y, z) => {
             ensure_equal!(
@@ -836,7 +796,7 @@ fn type_last_layer(
                 mkerr(IfBranchMismatch(y, z))
             );
 
-            Ok(RetType(y.get_type_move()?))
+            Ok(RetType(y.get_type()?.into_owned()))
         }
         EmptyListLit(t) => {
             let t = t.to_type();
@@ -855,12 +815,12 @@ fn type_last_layer(
                     y.get_type()?,
                     mkerr(InvalidListElement(
                         i,
-                        x.get_type_move()?.into_normalized()?,
+                        x.get_type()?.to_normalized(),
                         y
                     ))
                 );
             }
-            let t = x.get_type_move()?;
+            let t = x.get_type()?.into_owned();
             Ok(RetType(
                 TypeIntermediate::ListType(ctx.clone(), t)
                     .typecheck()?
@@ -868,7 +828,7 @@ fn type_last_layer(
             ))
         }
         SomeLit(x) => {
-            let t = x.get_type_move()?;
+            let t = x.get_type()?.into_owned();
             Ok(RetType(
                 TypeIntermediate::OptionalType(ctx.clone(), t)
                     .typecheck()?
@@ -904,7 +864,7 @@ fn type_last_layer(
         RecordLit(kvs) => {
             let kts = kvs
                 .into_iter()
-                .map(|(x, v)| Ok((x, v.get_type_move()?)))
+                .map(|(x, v)| Ok((x, v.get_type()?.into_owned())))
                 .collect::<Result<_, _>>()?;
             Ok(RetType(
                 TypeIntermediate::RecordType(ctx.clone(), kts)
@@ -923,7 +883,7 @@ fn type_last_layer(
                     Ok((x, t))
                 })
                 .collect::<Result<_, _>>()?;
-            let t = v.get_type_move()?;
+            let t = v.get_type()?.into_owned();
             kts.insert(x, Some(t));
             Ok(RetType(
                 TypeIntermediate::UnionType(ctx.clone(), kts)
@@ -934,12 +894,12 @@ fn type_last_layer(
         Field(r, x) => {
             let tr = r.get_type()?;
             let tr_internal = tr.internal_whnf();
-            match tr_internal.deref() {
+            match &tr_internal {
                 Some(Value::RecordType(kts)) => match kts.get(&x) {
                     Some(tth) => {
                         let tth = tth.clone();
                         drop(tr_internal);
-                        Ok(RetType(tth.normalize_to_type(ctx)?))
+                        Ok(RetType(tth.to_type(ctx)?))
                     },
                     None => Err(mkerr(MissingRecordField(x, r.clone()))),
                 },
@@ -947,7 +907,7 @@ fn type_last_layer(
                 _ => {
                     let r = r.to_type();
                     let r_internal = r.internal_whnf();
-                    match r_internal.deref() {
+                    match &r_internal {
                         Some(Value::UnionType(kts)) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
                             // TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
@@ -958,7 +918,7 @@ fn type_last_layer(
                                     TypeIntermediate::Pi(
                                         ctx.clone(),
                                         x.clone(),
-                                        t.normalize_to_type(ctx)?,
+                                        t.to_type(ctx)?,
                                         r,
                                     )
                                     .typecheck()?
@@ -973,7 +933,7 @@ fn type_last_layer(
                                 drop(r_internal);
                                 Err(mkerr(MissingUnionField(
                                     x,
-                                    r.into_normalized()?,
+                                    r.to_normalized(),
                                 )))
                             },
                         },
@@ -981,18 +941,18 @@ fn type_last_layer(
                             drop(r_internal);
                             Err(mkerr(NotARecord(
                                 x,
-                                r.into_normalized()?
+                                r.to_normalized()
                             )))
                         },
                     }
                 }
                 // _ => Err(mkerr(NotARecord(
                 //     x,
-                //     r.to_type()?.into_normalized()?,
+                //     r.to_type()?.to_normalized(),
                 // ))),
             }
         }
-        Const(c) => Ok(RetType(type_of_const(c))),
+        Const(c) => Ok(RetTyped(const_to_typed(c))),
         Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
         BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
@@ -1001,7 +961,7 @@ fn type_last_layer(
         // TODO: check type of interpolations
         TextLit(_) => Ok(RetType(builtin_to_type(Text)?)),
         BinOp(o @ ListAppend, l, r) => {
-            match l.get_type()?.internal_whnf().deref() {
+            match l.get_type()?.internal_whnf() {
                 Some(Value::AppliedBuiltin(List, _)) => {}
                 _ => return Err(mkerr(BinOpTypeMismatch(o, l.clone()))),
             }
@@ -1045,8 +1005,8 @@ fn type_of(
 ) -> Result<Typed<'static>, TypeError> {
     let ctx = TypecheckContext::new();
     let e = type_with(&ctx, e)?;
-    // Ensure the inferred type isn't SuperType
-    e.get_type()?.as_normalized()?;
+    // Ensure `e` has a type (i.e. `e` is not `Sort`)
+    e.get_type()?;
     Ok(e)
 }
 
@@ -1072,6 +1032,7 @@ pub(crate) enum TypeMessage<'a> {
     MissingUnionField(Label, Normalized<'a>),
     BinOpTypeMismatch(BinOp, Typed<'a>),
     NoDependentTypes(Normalized<'a>, Normalized<'a>),
+    Sort,
     Unimplemented,
 }
 
-- 
cgit v1.2.3