From 7983c43210f5fcaa439fa1c6742e72252652e4f4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 20:50:57 +0200
Subject: Thread Typed through type_with

---
 dhall/src/typecheck.rs | 89 +++++++++++++++++++++++++++-----------------------
 1 file changed, 48 insertions(+), 41 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e63b032..f5dbbbf 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -2,6 +2,7 @@
 use std::collections::HashSet;
 use std::fmt;
 
+use crate::expr::*;
 use crate::normalize::normalize;
 use dhall_core;
 use dhall_core::context::Context;
@@ -10,6 +11,17 @@ use dhall_generator as dhall;
 
 use self::TypeMessage::*;
 
+impl Resolved {
+    pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
+        // let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
+        //     self.0.clone(),
+        // )?)));
+        // Ok(Typed(self.0, typ))
+        let typ = crate::typecheck::type_of(self.0.clone())?;
+        Ok(Typed(self.0, typ))
+    }
+}
+
 fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
@@ -199,13 +211,10 @@ where
 ///
 /// `type_with` normalizes the type since while type-checking. It expects the
 /// context to contain only normalized expressions.
-pub fn type_with<S>(
-    ctx: &Context<Label, SubExpr<S, X>>,
-    e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>>
-where
-    S: ::std::fmt::Debug + Clone,
-{
+pub fn type_with(
+    ctx: &Context<Label, SubExpr<X, X>>,
+    e: SubExpr<X, X>,
+) -> Result<Typed, TypeError<X>> {
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
     use dhall_core::Const::*;
@@ -228,19 +237,19 @@ where
             let ctx2 = ctx
                 .insert(x.clone(), t2.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, b.clone())?;
-            let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?;
+            let tB = type_with(&ctx2, b.clone())?.1;
+            let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1;
             Ok(Pi(x.clone(), t2, tB))
         }
         Pi(x, tA, tB) => {
-            let ttA = type_with(ctx, tA.clone())?;
+            let ttA = type_with(ctx, tA.clone())?.1;
             let tA = normalize(SubExpr::clone(tA));
             let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, tB.clone())?;
+            let tB = type_with(&ctx2, tB.clone())?.1;
             let kB = match tB.as_ref() {
                 Const(k) => *k,
                 _ => {
@@ -264,15 +273,15 @@ where
                 SubExpr::clone(r)
             };
 
-            let tR = type_with(ctx, r)?;
-            let ttR = type_with(ctx, tR.clone())?;
+            let tR = type_with(ctx, r)?.1;
+            let ttR = type_with(ctx, tR.clone())?.1;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
 
             let ctx2 = ctx.insert(f.clone(), tR.clone());
-            let tB = type_with(&ctx2, b.clone())?;
-            let ttB = type_with(ctx, tB.clone())?;
+            let tB = type_with(&ctx2, b.clone())?.1;
+            let ttB = type_with(ctx, tB.clone())?.1;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
@@ -285,7 +294,7 @@ where
         }
         _ => match e
             .as_ref()
-            .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))?
+            .traverse_ref_simple(|e| type_with(ctx, e.clone()))?
         {
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
@@ -295,10 +304,10 @@ where
                 Some(e) => Ok(e.unroll()),
                 None => Err(mkerr(UnboundVariable)),
             },
-            App((f, mut tf), args) => {
+            App(Typed(f, mut tf), args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                while let Some((a, ta)) = iter.next() {
+                while let Some(Typed(a, ta)) = iter.next() {
                     seen_args.push(a.clone());
                     let (x, tx, tb) = match tf.as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
@@ -321,18 +330,18 @@ where
                 }
                 Ok(tf.unroll())
             }
-            Annot((x, tx), (t, _)) => {
+            Annot(Typed(x, tx), Typed(t, _)) => {
                 let t = normalize(t.clone());
                 ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || {
                     AnnotMismatch(x.clone(), t.clone(), tx.clone())
                 })?;
                 Ok(t.unroll())
             }
-            BoolIf((x, tx), (y, ty), (z, tz)) => {
+            BoolIf(Typed(x, tx), Typed(y, ty), Typed(z, tz)) => {
                 ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || {
                     InvalidPredicate(x.clone(), tx.clone())
                 })?;
-                let tty = type_with(ctx, ty.clone())?;
+                let tty = type_with(ctx, ty.clone())?.1;
                 ensure_is_type(
                     tty.clone(),
                     IfBranchMustBeTerm(
@@ -343,7 +352,7 @@ where
                     ),
                 )?;
 
-                let ttz = type_with(ctx, tz.clone())?;
+                let ttz = type_with(ctx, tz.clone())?.1;
                 ensure_is_type(
                     ttz.clone(),
                     IfBranchMustBeTerm(
@@ -364,35 +373,35 @@ where
                 })?;
                 Ok(ty.unroll())
             }
-            EmptyListLit((t, tt)) => {
-                ensure_is_type(tt, InvalidListType(t.clone()))?;
-                let t = normalize(SubExpr::clone(t));
+            EmptyListLit(Typed(t, tt)) => {
+                ensure_is_type(tt.clone(), InvalidListType(t.clone()))?;
+                let t = Typed(t, tt).normalize().0;
                 Ok(dhall::expr!(List t))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
-                let (_, (_, t)) = iter.next().unwrap();
-                let s = type_with(ctx, t.clone())?;
+                let (_, Typed(_, t)) = iter.next().unwrap();
+                let s = type_with(ctx, t.clone())?.1;
                 ensure_is_type(s, InvalidListType(t.clone()))?;
-                for (i, (y, ty)) in iter {
+                for (i, Typed(y, ty)) in iter {
                     ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || {
                         InvalidListElement(i, t.clone(), y.clone(), ty.clone())
                     })?;
                 }
                 Ok(dhall::expr!(List t))
             }
-            EmptyOptionalLit((t, tt)) => {
+            EmptyOptionalLit(Typed(t, tt)) => {
                 ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
                 let t = normalize(t.clone());
                 Ok(dhall::expr!(Optional t))
             }
-            NEOptionalLit((_, t)) => {
-                let s = type_with(ctx, t.clone())?;
+            NEOptionalLit(Typed(_, t)) => {
+                let s = type_with(ctx, t.clone())?.1;
                 ensure_is_type(s, InvalidOptionalType(t.clone()))?;
                 Ok(dhall::expr!(Optional t))
             }
             RecordType(kts) => {
-                for (k, (t, tt)) in kts {
+                for (k, Typed(t, tt)) in kts {
                     ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
                 }
                 Ok(Const(Type))
@@ -400,15 +409,15 @@ where
             RecordLit(kvs) => {
                 let kts = kvs
                     .into_iter()
-                    .map(|(k, (v, t))| {
-                        let s = type_with(ctx, t.clone())?;
+                    .map(|(k, Typed(v, t))| {
+                        let s = type_with(ctx, t.clone())?.1;
                         ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
                         Ok((k.clone(), t))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RecordType(kts))
             }
-            Field((r, tr), x) => match tr.as_ref() {
+            Field(Typed(r, tr), x) => match tr.as_ref() {
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => Ok(e.unroll()),
                     None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
@@ -422,7 +431,7 @@ where
             DoubleLit(_) => Ok(Builtin(Double)),
             // TODO: check type of interpolations
             TextLit(_) => Ok(Builtin(Text)),
-            BinOp(o, (l, tl), (r, tr)) => {
+            BinOp(o, Typed(l, tl), Typed(r, tr)) => {
                 let t = Builtin(match o {
                     BoolAnd => Bool,
                     BoolOr => Bool,
@@ -448,17 +457,15 @@ where
             _ => panic!("Unimplemented typecheck case: {:?}", e),
         },
     }?;
-    Ok(rc(ret))
+    Ok(Typed(e, rc(ret)))
 }
 
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-pub fn type_of<S: ::std::fmt::Debug + Clone>(
-    e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>> {
+pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e) //.map(|e| e.into_owned())
+    type_with(&ctx, e).map(|e| e.1)
 }
 
 /// The specific type error
-- 
cgit v1.2.3


From c4438eb3d52b1a69c9022b12e8de135b8c9991c9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 21:54:55 +0200
Subject: Start taking Typed seriously

---
 dhall/src/typecheck.rs | 239 +++++++++++++++++++++++++++----------------------
 1 file changed, 133 insertions(+), 106 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f5dbbbf..d62fe5a 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -3,7 +3,6 @@ use std::collections::HashSet;
 use std::fmt;
 
 use crate::expr::*;
-use crate::normalize::normalize;
 use dhall_core;
 use dhall_core::context::Context;
 use dhall_core::*;
@@ -21,6 +20,16 @@ impl Resolved {
         Ok(Typed(self.0, typ))
     }
 }
+impl Typed {
+    pub fn get_type(&self) -> &Type {
+        &self.1
+    }
+}
+impl Normalized {
+    pub fn get_type(&self) -> &Type {
+        &self.1
+    }
+}
 
 fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::Const::*;
@@ -231,23 +240,29 @@ pub fn type_with(
             _ => Err(mkerr(msg)),
         };
 
+    enum Ret {
+        ErrRet(TypeError<X>),
+        OkNormalized(Normalized),
+        OkRet(Expr<X, X>),
+    }
+    use Ret::*;
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
-            let t2 = normalize(SubExpr::clone(t));
+            let t2 = type_with(ctx, t.clone())?.normalize();
             let ctx2 = ctx
-                .insert(x.clone(), t2.clone())
+                .insert(x.clone(), t2.0.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, b.clone())?.1;
             let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1;
-            Ok(Pi(x.clone(), t2, tB))
+            OkRet(Pi(x.clone(), t2.0, tB))
         }
         Pi(x, tA, tB) => {
-            let ttA = type_with(ctx, tA.clone())?.1;
-            let tA = normalize(SubExpr::clone(tA));
-            let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
+            let tA = type_with(ctx, tA.clone())?.normalize();
+            let kA =
+                ensure_const(tA.get_type(), InvalidInputType(tA.0.clone()))?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.clone())
+                .insert(x.clone(), tA.0.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, tB.clone())?.1;
             let kB = match tB.as_ref() {
@@ -262,8 +277,8 @@ pub fn type_with(
             };
 
             match rule(kA, kB) {
-                Err(()) => Err(mkerr(NoDependentTypes(tA.clone(), tB))),
-                Ok(_) => Ok(Const(kB)),
+                Err(()) => ErrRet(mkerr(NoDependentTypes(tA.0.clone(), tB))),
+                Ok(_) => OkRet(Const(kB)),
             }
         }
         Let(f, mt, r, b) => {
@@ -273,24 +288,33 @@ pub fn type_with(
                 SubExpr::clone(r)
             };
 
-            let tR = type_with(ctx, r)?.1;
-            let ttR = type_with(ctx, tR.clone())?.1;
+            let r = type_with(ctx, r)?;
+            let tr = type_with(ctx, r.get_type().clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
-            let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
+            let kR = ensure_const(
+                tr.get_type(),
+                InvalidInputType(r.get_type().clone()),
+            )?;
 
-            let ctx2 = ctx.insert(f.clone(), tR.clone());
-            let tB = type_with(&ctx2, b.clone())?.1;
-            let ttB = type_with(ctx, tB.clone())?.1;
+            let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
+            let b = type_with(&ctx2, b.clone())?;
+            let tb = type_with(ctx, b.get_type().clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
-            let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
+            let kB = ensure_const(
+                tb.get_type(),
+                InvalidOutputType(b.get_type().clone()),
+            )?;
 
             if let Err(()) = rule(kR, kB) {
-                return Err(mkerr(NoDependentLet(tR, tB)));
+                return Err(mkerr(NoDependentLet(
+                    r.get_type().clone(),
+                    b.get_type().clone(),
+                )));
             }
 
-            Ok(tB.unroll())
+            OkRet(b.get_type().unroll())
         }
         _ => match e
             .as_ref()
@@ -299,84 +323,85 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(c) => axiom(c).map(Const),
+            Const(c) => OkRet(Const(axiom(c)?)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
-                Some(e) => Ok(e.unroll()),
-                None => Err(mkerr(UnboundVariable)),
+                Some(e) => OkRet(e.unroll()),
+                None => ErrRet(mkerr(UnboundVariable)),
             },
-            App(Typed(f, mut tf), args) => {
+            App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
+                let mut tf = type_with(ctx, f.get_type().clone())?.normalize();
                 while let Some(Typed(a, ta)) = iter.next() {
                     seen_args.push(a.clone());
-                    let (x, tx, tb) = match tf.as_ref() {
+                    let (x, tx, tb) = match tf.0.as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(
-                                rc(App(f.clone(), seen_args)),
+                                rc(App(f.0.clone(), seen_args)),
                                 tf,
                             )));
                         }
                     };
                     ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || {
                         TypeMismatch(
-                            rc(App(f.clone(), seen_args.clone())),
+                            rc(App(f.0.clone(), seen_args.clone())),
                             tx.clone(),
                             a.clone(),
                             ta.clone(),
                         )
                     })?;
-                    tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb));
+                    tf =
+                        type_with(ctx, subst_shift(&V(x.clone(), 0), &a, &tb))?
+                            .normalize();
                 }
-                Ok(tf.unroll())
+                OkNormalized(tf)
             }
-            Annot(Typed(x, tx), Typed(t, _)) => {
-                let t = normalize(t.clone());
-                ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || {
-                    AnnotMismatch(x.clone(), t.clone(), tx.clone())
-                })?;
-                Ok(t.unroll())
+            Annot(x, t) => {
+                let t = t.normalize();
+                ensure_equal(
+                    t.0.as_ref(),
+                    x.get_type().as_ref(),
+                    mkerr,
+                    || AnnotMismatch(x.clone(), t.clone()),
+                )?;
+                OkNormalized(t)
             }
-            BoolIf(Typed(x, tx), Typed(y, ty), Typed(z, tz)) => {
-                ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || {
-                    InvalidPredicate(x.clone(), tx.clone())
-                })?;
-                let tty = type_with(ctx, ty.clone())?.1;
+            BoolIf(x, y, z) => {
+                ensure_equal(
+                    x.get_type().as_ref(),
+                    &Builtin(Bool),
+                    mkerr,
+                    || InvalidPredicate(x.clone()),
+                )?;
+                let ty = type_with(ctx, y.get_type().clone())?.normalize();
                 ensure_is_type(
-                    tty.clone(),
-                    IfBranchMustBeTerm(
-                        true,
-                        y.clone(),
-                        ty.clone(),
-                        tty.clone(),
-                    ),
+                    ty.get_type().clone(),
+                    IfBranchMustBeTerm(true, y.clone()),
                 )?;
 
-                let ttz = type_with(ctx, tz.clone())?.1;
+                let tz = type_with(ctx, z.get_type().clone())?.normalize();
                 ensure_is_type(
-                    ttz.clone(),
-                    IfBranchMustBeTerm(
-                        false,
-                        z.clone(),
-                        tz.clone(),
-                        ttz.clone(),
-                    ),
+                    tz.get_type().clone(),
+                    IfBranchMustBeTerm(false, z.clone()),
                 )?;
 
-                ensure_equal(ty.as_ref(), tz.as_ref(), mkerr, || {
-                    IfBranchMismatch(
-                        y.clone(),
-                        z.clone(),
-                        ty.clone(),
-                        tz.clone(),
-                    )
-                })?;
-                Ok(ty.unroll())
+                ensure_equal(
+                    y.get_type().as_ref(),
+                    z.get_type().as_ref(),
+                    mkerr,
+                    || IfBranchMismatch(y.clone(), z.clone()),
+                )?;
+
+                OkNormalized(ty)
             }
-            EmptyListLit(Typed(t, tt)) => {
-                ensure_is_type(tt.clone(), InvalidListType(t.clone()))?;
-                let t = Typed(t, tt).normalize().0;
-                Ok(dhall::expr!(List t))
+            EmptyListLit(t) => {
+                ensure_is_type(
+                    t.get_type().clone(),
+                    InvalidListType(t.0.clone()),
+                )?;
+                let t = t.normalize().0;
+                OkRet(dhall::expr!(List t))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
@@ -388,23 +413,26 @@ pub fn type_with(
                         InvalidListElement(i, t.clone(), y.clone(), ty.clone())
                     })?;
                 }
-                Ok(dhall::expr!(List t))
+                OkRet(dhall::expr!(List t))
             }
-            EmptyOptionalLit(Typed(t, tt)) => {
-                ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
-                let t = normalize(t.clone());
-                Ok(dhall::expr!(Optional t))
+            EmptyOptionalLit(t) => {
+                ensure_is_type(
+                    t.get_type().clone(),
+                    InvalidOptionalType(t.0.clone()),
+                )?;
+                let t = t.normalize().0;
+                OkRet(dhall::expr!(Optional t))
             }
             NEOptionalLit(Typed(_, t)) => {
                 let s = type_with(ctx, t.clone())?.1;
                 ensure_is_type(s, InvalidOptionalType(t.clone()))?;
-                Ok(dhall::expr!(Optional t))
+                OkRet(dhall::expr!(Optional t))
             }
             RecordType(kts) => {
                 for (k, Typed(t, tt)) in kts {
                     ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
                 }
-                Ok(Const(Type))
+                OkRet(Const(Type))
             }
             RecordLit(kvs) => {
                 let kts = kvs
@@ -415,23 +443,23 @@ pub fn type_with(
                         Ok((k.clone(), t))
                     })
                     .collect::<Result<_, _>>()?;
-                Ok(RecordType(kts))
+                OkRet(RecordType(kts))
             }
-            Field(Typed(r, tr), x) => match tr.as_ref() {
+            Field(r, x) => match r.get_type().as_ref() {
                 RecordType(kts) => match kts.get(&x) {
-                    Some(e) => Ok(e.unroll()),
-                    None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
+                    Some(e) => OkRet(e.unroll()),
+                    None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))),
                 },
-                _ => Err(mkerr(NotARecord(x.clone(), r.clone(), tr.clone()))),
+                _ => ErrRet(mkerr(NotARecord(x.clone(), r.clone()))),
             },
-            Builtin(b) => Ok(type_of_builtin(b)),
-            BoolLit(_) => Ok(Builtin(Bool)),
-            NaturalLit(_) => Ok(Builtin(Natural)),
-            IntegerLit(_) => Ok(Builtin(Integer)),
-            DoubleLit(_) => Ok(Builtin(Double)),
+            Builtin(b) => OkRet(type_of_builtin(b)),
+            BoolLit(_) => OkRet(Builtin(Bool)),
+            NaturalLit(_) => OkRet(Builtin(Natural)),
+            IntegerLit(_) => OkRet(Builtin(Integer)),
+            DoubleLit(_) => OkRet(Builtin(Double)),
             // TODO: check type of interpolations
-            TextLit(_) => Ok(Builtin(Text)),
-            BinOp(o, Typed(l, tl), Typed(r, tr)) => {
+            TextLit(_) => OkRet(Builtin(Text)),
+            BinOp(o, l, r) => {
                 let t = Builtin(match o {
                     BoolAnd => Bool,
                     BoolOr => Bool,
@@ -443,21 +471,25 @@ pub fn type_with(
                     _ => panic!("Unimplemented typecheck case: {:?}", e),
                 });
 
-                ensure_equal(tl.as_ref(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, l.clone(), tl.clone())
+                ensure_equal(l.get_type().as_ref(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, l.clone())
                 })?;
 
-                ensure_equal(tr.as_ref(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, r.clone(), tr.clone())
+                ensure_equal(r.get_type().as_ref(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, r.clone())
                 })?;
 
-                Ok(t)
+                OkRet(t)
             }
             Embed(p) => match p {},
             _ => panic!("Unimplemented typecheck case: {:?}", e),
         },
-    }?;
-    Ok(Typed(e, rc(ret)))
+    };
+    match ret {
+        OkRet(ret) => Ok(Typed(e, rc(ret))),
+        OkNormalized(ret) => Ok(Typed(e, ret.0)),
+        ErrRet(e) => Err(e),
+    }
 }
 
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
@@ -474,23 +506,18 @@ pub enum TypeMessage<S> {
     UnboundVariable,
     InvalidInputType(SubExpr<S, X>),
     InvalidOutputType(SubExpr<S, X>),
-    NotAFunction(SubExpr<S, X>, SubExpr<S, X>),
+    NotAFunction(SubExpr<S, X>, Normalized),
     TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
-    AnnotMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    AnnotMismatch(Typed, Normalized),
     Untyped,
     InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidListType(SubExpr<S, X>),
     InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidOptionalLiteral(usize),
     InvalidOptionalType(SubExpr<S, X>),
-    InvalidPredicate(SubExpr<S, X>, SubExpr<S, X>),
-    IfBranchMismatch(
-        SubExpr<S, X>,
-        SubExpr<S, X>,
-        SubExpr<S, X>,
-        SubExpr<S, X>,
-    ),
-    IfBranchMustBeTerm(bool, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidPredicate(Typed),
+    IfBranchMismatch(Typed, Typed),
+    IfBranchMustBeTerm(bool, Typed),
     InvalidField(Label, SubExpr<S, X>),
     InvalidFieldType(Label, SubExpr<S, X>),
     InvalidAlternative(Label, SubExpr<S, X>),
@@ -505,9 +532,9 @@ pub enum TypeMessage<S> {
     HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
     HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
     HandlerNotAFunction(Label, SubExpr<S, X>),
-    NotARecord(Label, SubExpr<S, X>, SubExpr<S, X>),
-    MissingField(Label, SubExpr<S, X>),
-    BinOpTypeMismatch(BinOp, SubExpr<S, X>, SubExpr<S, X>),
+    NotARecord(Label, Typed),
+    MissingField(Label, Typed),
+    BinOpTypeMismatch(BinOp, Typed),
     NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
     NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
 }
-- 
cgit v1.2.3


From f93aee4dcf71c85b826244b3b57949ffbdb820c4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 22:37:39 +0200
Subject: Add Sort type universe

---
 dhall/src/typecheck.rs | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index d62fe5a..5457701 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -36,16 +36,19 @@ fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::ExprF::*;
     match c {
         Type => Ok(Kind),
-        Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
+        Kind => Ok(Sort),
+        Sort => Err(TypeError::new(&Context::new(), rc(Const(Sort)), Untyped)),
     }
 }
 
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
     match (a, b) {
-        (Type, Kind) => Err(()),
+        (_, Type) => Ok(Type),
         (Kind, Kind) => Ok(Kind),
-        (Type, Type) | (Kind, Type) => Ok(Type),
+        (Sort, Sort) => Ok(Sort),
+        (Sort, Kind) => Ok(Sort),
+        _ => Err(()),
     }
 }
 
-- 
cgit v1.2.3


From b0eb080caab28196a09c5b60c5b6556846732563 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 23:07:30 +0200
Subject: Store the whole type hierarchy in a Type

---
 dhall/src/typecheck.rs | 260 ++++++++++++++++++++++++++++++-------------------
 1 file changed, 159 insertions(+), 101 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5457701..d0e1d44 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -16,8 +16,8 @@ impl Resolved {
         //     self.0.clone(),
         // )?)));
         // Ok(Typed(self.0, typ))
-        let typ = crate::typecheck::type_of(self.0.clone())?;
-        Ok(Typed(self.0, typ))
+        let typ = crate::typecheck::type_of_(self.0.clone())?;
+        Ok(typ)
     }
 }
 impl Typed {
@@ -30,14 +30,22 @@ impl Normalized {
         &self.1
     }
 }
-
-fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
-    use dhall_core::Const::*;
-    use dhall_core::ExprF::*;
-    match c {
-        Type => Ok(Kind),
-        Kind => Ok(Sort),
-        Sort => Err(TypeError::new(&Context::new(), rc(Const(Sort)), Untyped)),
+impl Type {
+    // pub fn as_expr(&self) -> &Normalized {
+    //     &*self.0
+    // }
+    pub fn as_expr(&self) -> &SubExpr<X, X> {
+        &self.as_normalized().0
+    }
+    pub fn as_normalized(&self) -> &Normalized {
+        use TypeInternal::*;
+        match &self.0 {
+            Expr(e) => &e,
+            Universe(_) => unimplemented!(),
+        }
+    }
+    pub fn get_type(&self) -> &Type {
+        self.as_normalized().get_type()
     }
 }
 
@@ -232,13 +240,15 @@ pub fn type_with(
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
-    let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
-    {
-        Const(k) => Ok(*k),
-        _ => Err(mkerr(msg)),
-    };
+    let ensure_const =
+        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref()
+        {
+            Const(k) => Ok(*k),
+            _ => Err(mkerr(msg)),
+        };
     let ensure_is_type =
-        |x: SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() {
+        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref()
+        {
             Const(Type) => Ok(()),
             _ => Err(mkerr(msg)),
         };
@@ -246,6 +256,7 @@ pub fn type_with(
     enum Ret {
         ErrRet(TypeError<X>),
         OkNormalized(Normalized),
+        OkType(crate::expr::Type),
         OkRet(Expr<X, X>),
     }
     use Ret::*;
@@ -255,9 +266,12 @@ pub fn type_with(
             let ctx2 = ctx
                 .insert(x.clone(), t2.0.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, b.clone())?.1;
-            let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1;
-            OkRet(Pi(x.clone(), t2.0, tB))
+            let b = type_with(&ctx2, b.clone())?;
+            let _ = type_with(
+                ctx,
+                rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())),
+            )?;
+            OkRet(Pi(x.clone(), t2.0, b.get_type().as_expr().clone()))
         }
         Pi(x, tA, tB) => {
             let tA = type_with(ctx, tA.clone())?.normalize();
@@ -267,20 +281,23 @@ pub fn type_with(
             let ctx2 = ctx
                 .insert(x.clone(), tA.0.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, tB.clone())?.1;
-            let kB = match tB.as_ref() {
+            let tB = type_with(&ctx2, tB.clone())?;
+            let kB = match tB.get_type().as_expr().as_ref() {
                 Const(k) => *k,
                 _ => {
                     return Err(TypeError::new(
                         &ctx2,
                         e.clone(),
-                        InvalidOutputType(tB),
+                        InvalidOutputType(tB.get_type().clone()),
                     ));
                 }
             };
 
             match rule(kA, kB) {
-                Err(()) => ErrRet(mkerr(NoDependentTypes(tA.0.clone(), tB))),
+                Err(()) => ErrRet(mkerr(NoDependentTypes(
+                    tA.0.clone(),
+                    tB.get_type().clone(),
+                ))),
                 Ok(_) => OkRet(Const(kB)),
             }
         }
@@ -292,32 +309,30 @@ pub fn type_with(
             };
 
             let r = type_with(ctx, r)?;
-            let tr = type_with(ctx, r.get_type().clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kR = ensure_const(
-                tr.get_type(),
-                InvalidInputType(r.get_type().clone()),
+                r.get_type().get_type(),
+                InvalidInputType(r.get_type().as_expr().clone()),
             )?;
 
-            let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
+            let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone());
             let b = type_with(&ctx2, b.clone())?;
-            let tb = type_with(ctx, b.get_type().clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(
-                tb.get_type(),
+                b.get_type().get_type(),
                 InvalidOutputType(b.get_type().clone()),
             )?;
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.get_type().clone(),
-                    b.get_type().clone(),
+                    r.get_type().as_expr().clone(),
+                    b.get_type().as_expr().clone(),
                 )));
             }
 
-            OkRet(b.get_type().unroll())
+            OkType(b.get_type().clone())
         }
         _ => match e
             .as_ref()
@@ -326,7 +341,9 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(c) => OkRet(Const(axiom(c)?)),
+            Const(Type) => OkRet(Const(Kind)),
+            Const(Kind) => OkRet(Const(Sort)),
+            Const(Sort) => ErrRet(mkerr(Untyped)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
                 Some(e) => OkRet(e.unroll()),
                 None => ErrRet(mkerr(UnboundVariable)),
@@ -334,9 +351,9 @@ pub fn type_with(
             App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                let mut tf = type_with(ctx, f.get_type().clone())?.normalize();
-                while let Some(Typed(a, ta)) = iter.next() {
-                    seen_args.push(a.clone());
+                let mut tf = f.get_type().as_normalized().clone();
+                while let Some(a) = iter.next() {
+                    seen_args.push(a.0.clone());
                     let (x, tx, tb) = match tf.0.as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
@@ -346,17 +363,23 @@ pub fn type_with(
                             )));
                         }
                     };
-                    ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || {
-                        TypeMismatch(
-                            rc(App(f.0.clone(), seen_args.clone())),
-                            tx.clone(),
-                            a.clone(),
-                            ta.clone(),
-                        )
-                    })?;
-                    tf =
-                        type_with(ctx, subst_shift(&V(x.clone(), 0), &a, &tb))?
-                            .normalize();
+                    ensure_equal(
+                        tx.as_ref(),
+                        a.get_type().as_expr().as_ref(),
+                        mkerr,
+                        || {
+                            TypeMismatch(
+                                rc(App(f.0.clone(), seen_args.clone())),
+                                tx.clone(),
+                                a.clone(),
+                            )
+                        },
+                    )?;
+                    tf = type_with(
+                        ctx,
+                        subst_shift(&V(x.clone(), 0), &a.0, &tb),
+                    )?
+                    .normalize();
                 }
                 OkNormalized(tf)
             }
@@ -364,91 +387,103 @@ pub fn type_with(
                 let t = t.normalize();
                 ensure_equal(
                     t.0.as_ref(),
-                    x.get_type().as_ref(),
+                    x.get_type().as_expr().as_ref(),
                     mkerr,
                     || AnnotMismatch(x.clone(), t.clone()),
                 )?;
-                OkNormalized(t)
+                OkType(x.get_type().clone())
             }
             BoolIf(x, y, z) => {
                 ensure_equal(
-                    x.get_type().as_ref(),
+                    x.get_type().as_expr().as_ref(),
                     &Builtin(Bool),
                     mkerr,
                     || InvalidPredicate(x.clone()),
                 )?;
-                let ty = type_with(ctx, y.get_type().clone())?.normalize();
                 ensure_is_type(
-                    ty.get_type().clone(),
+                    y.get_type().get_type(),
                     IfBranchMustBeTerm(true, y.clone()),
                 )?;
 
-                let tz = type_with(ctx, z.get_type().clone())?.normalize();
                 ensure_is_type(
-                    tz.get_type().clone(),
+                    z.get_type().get_type(),
                     IfBranchMustBeTerm(false, z.clone()),
                 )?;
 
                 ensure_equal(
-                    y.get_type().as_ref(),
-                    z.get_type().as_ref(),
+                    y.get_type().as_expr().as_ref(),
+                    z.get_type().as_expr().as_ref(),
                     mkerr,
                     || IfBranchMismatch(y.clone(), z.clone()),
                 )?;
 
-                OkNormalized(ty)
+                OkType(y.get_type().clone())
             }
             EmptyListLit(t) => {
-                ensure_is_type(
-                    t.get_type().clone(),
-                    InvalidListType(t.0.clone()),
-                )?;
+                ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?;
                 let t = t.normalize().0;
                 OkRet(dhall::expr!(List t))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
-                let (_, Typed(_, t)) = iter.next().unwrap();
-                let s = type_with(ctx, t.clone())?.1;
-                ensure_is_type(s, InvalidListType(t.clone()))?;
-                for (i, Typed(y, ty)) in iter {
-                    ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || {
-                        InvalidListElement(i, t.clone(), y.clone(), ty.clone())
-                    })?;
+                let (_, x) = iter.next().unwrap();
+                ensure_is_type(
+                    x.get_type().get_type(),
+                    InvalidListType(x.get_type().as_expr().clone()),
+                )?;
+                for (i, y) in iter {
+                    ensure_equal(
+                        x.get_type().as_expr().as_ref(),
+                        y.get_type().as_expr().as_ref(),
+                        mkerr,
+                        || {
+                            InvalidListElement(
+                                i,
+                                x.get_type().as_expr().clone(),
+                                y.clone(),
+                            )
+                        },
+                    )?;
                 }
+                let t = x.get_type().as_expr().clone();
                 OkRet(dhall::expr!(List t))
             }
             EmptyOptionalLit(t) => {
-                ensure_is_type(
-                    t.get_type().clone(),
-                    InvalidOptionalType(t.0.clone()),
-                )?;
+                ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?;
                 let t = t.normalize().0;
                 OkRet(dhall::expr!(Optional t))
             }
-            NEOptionalLit(Typed(_, t)) => {
-                let s = type_with(ctx, t.clone())?.1;
-                ensure_is_type(s, InvalidOptionalType(t.clone()))?;
+            NEOptionalLit(x) => {
+                ensure_is_type(
+                    x.get_type().get_type(),
+                    InvalidOptionalType(x.get_type().as_expr().clone()),
+                )?;
+                let t = x.get_type().as_expr().clone();
                 OkRet(dhall::expr!(Optional t))
             }
             RecordType(kts) => {
-                for (k, Typed(t, tt)) in kts {
-                    ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
+                for (k, t) in kts {
+                    ensure_is_type(
+                        t.get_type(),
+                        InvalidFieldType(k.clone(), t.clone()),
+                    )?;
                 }
                 OkRet(Const(Type))
             }
             RecordLit(kvs) => {
                 let kts = kvs
                     .into_iter()
-                    .map(|(k, Typed(v, t))| {
-                        let s = type_with(ctx, t.clone())?.1;
-                        ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
-                        Ok((k.clone(), t))
+                    .map(|(k, v)| {
+                        ensure_is_type(
+                            v.get_type().get_type(),
+                            InvalidField(k.clone(), v.clone()),
+                        )?;
+                        Ok((k.clone(), v.get_type().as_expr().clone()))
                     })
                     .collect::<Result<_, _>>()?;
                 OkRet(RecordType(kts))
             }
-            Field(r, x) => match r.get_type().as_ref() {
+            Field(r, x) => match r.get_type().as_expr().as_ref() {
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => OkRet(e.unroll()),
                     None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))),
@@ -474,13 +509,19 @@ pub fn type_with(
                     _ => panic!("Unimplemented typecheck case: {:?}", e),
                 });
 
-                ensure_equal(l.get_type().as_ref(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, l.clone())
-                })?;
+                ensure_equal(
+                    l.get_type().as_expr().as_ref(),
+                    &t,
+                    mkerr,
+                    || BinOpTypeMismatch(o, l.clone()),
+                )?;
 
-                ensure_equal(r.get_type().as_ref(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, r.clone())
-                })?;
+                ensure_equal(
+                    r.get_type().as_expr().as_ref(),
+                    &t,
+                    mkerr,
+                    || BinOpTypeMismatch(o, r.clone()),
+                )?;
 
                 OkRet(t)
             }
@@ -489,8 +530,20 @@ pub fn type_with(
         },
     };
     match ret {
-        OkRet(ret) => Ok(Typed(e, rc(ret))),
-        OkNormalized(ret) => Ok(Typed(e, ret.0)),
+        OkRet(Const(Sort)) => {
+            Ok(Typed(e, crate::expr::Type(TypeInternal::Universe(3))))
+        }
+        OkRet(ret) => Ok(Typed(
+            e,
+            crate::expr::Type(TypeInternal::Expr(Box::new(
+                type_with(ctx, rc(ret))?.normalize(),
+            ))),
+        )),
+        OkNormalized(ret) => Ok(Typed(
+            e,
+            crate::expr::Type(TypeInternal::Expr(Box::new(ret))),
+        )),
+        OkType(ret) => Ok(Typed(e, ret)),
         ErrRet(e) => Err(e),
     }
 }
@@ -500,7 +553,12 @@ pub fn type_with(
 /// will fail.
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e).map(|e| e.1)
+    type_with(&ctx, e).map(|e| e.get_type().as_expr().clone())
+}
+
+pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
+    let ctx = Context::new();
+    type_with(&ctx, e)
 }
 
 /// The specific type error
@@ -508,12 +566,12 @@ pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
 pub enum TypeMessage<S> {
     UnboundVariable,
     InvalidInputType(SubExpr<S, X>),
-    InvalidOutputType(SubExpr<S, X>),
+    InvalidOutputType(crate::expr::Type),
     NotAFunction(SubExpr<S, X>, Normalized),
-    TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, Typed),
     AnnotMismatch(Typed, Normalized),
     Untyped,
-    InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidListElement(usize, SubExpr<S, X>, Typed),
     InvalidListType(SubExpr<S, X>),
     InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidOptionalLiteral(usize),
@@ -521,8 +579,8 @@ pub enum TypeMessage<S> {
     InvalidPredicate(Typed),
     IfBranchMismatch(Typed, Typed),
     IfBranchMustBeTerm(bool, Typed),
-    InvalidField(Label, SubExpr<S, X>),
-    InvalidFieldType(Label, SubExpr<S, X>),
+    InvalidField(Label, Typed),
+    InvalidFieldType(Label, Typed),
     InvalidAlternative(Label, SubExpr<S, X>),
     InvalidAlternativeType(Label, SubExpr<S, X>),
     DuplicateAlternative(Label),
@@ -539,7 +597,7 @@ pub enum TypeMessage<S> {
     MissingField(Label, Typed),
     BinOpTypeMismatch(BinOp, Typed),
     NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
-    NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
+    NoDependentTypes(SubExpr<S, X>, crate::expr::Type),
 }
 
 /// A structured type error that includes context
@@ -571,7 +629,7 @@ impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
             InvalidInputType(_) => "Invalid function input",
             InvalidOutputType(_) => "Invalid function output",
             NotAFunction(_, _) => "Not a function",
-            TypeMismatch(_, _, _, _) => "Wrong type of function argument",
+            TypeMismatch(_, _, _) => "Wrong type of function argument",
             _ => "Unhandled error",
         }
     }
@@ -583,13 +641,13 @@ impl<S> fmt::Display for TypeMessage<S> {
             UnboundVariable => {
                 f.write_str(include_str!("errors/UnboundVariable.txt"))
             }
-            TypeMismatch(e0, e1, e2, e3) => {
+            TypeMismatch(e0, e1, e2) => {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
                     .replace("$txt0", &format!("{}", e0))
                     .replace("$txt1", &format!("{}", e1))
-                    .replace("$txt2", &format!("{}", e2))
-                    .replace("$txt3", &format!("{}", e3));
+                    .replace("$txt2", &format!("{}", e2.0))
+                    .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
                 f.write_str(&s)
             }
             _ => f.write_str("Unhandled error message"),
-- 
cgit v1.2.3


From 2e29ffcff718db2f95372c6f5258338df92ea213 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 23:41:32 +0200
Subject: More improvements to typecheck

---
 dhall/src/typecheck.rs | 247 +++++++++++++++++++++++--------------------------
 1 file changed, 114 insertions(+), 133 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index d0e1d44..0ebc67e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -21,6 +21,9 @@ impl Resolved {
     }
 }
 impl Typed {
+    fn as_expr(&self) -> &SubExpr<X, X> {
+        &self.0
+    }
     pub fn get_type(&self) -> &Type {
         &self.1
     }
@@ -29,15 +32,18 @@ impl Normalized {
     pub fn get_type(&self) -> &Type {
         &self.1
     }
+    fn into_type(self) -> Type {
+        crate::expr::Type(TypeInternal::Expr(Box::new(self)))
+    }
 }
 impl Type {
     // pub fn as_expr(&self) -> &Normalized {
     //     &*self.0
     // }
-    pub fn as_expr(&self) -> &SubExpr<X, X> {
+    fn as_expr(&self) -> &SubExpr<X, X> {
         &self.as_normalized().0
     }
-    pub fn as_normalized(&self) -> &Normalized {
+    fn as_normalized(&self) -> &Normalized {
         use TypeInternal::*;
         match &self.0 {
             Expr(e) => &e,
@@ -49,6 +55,9 @@ impl Type {
     }
 }
 
+const TYPE_OF_SORT: crate::expr::Type =
+    crate::expr::Type(TypeInternal::Universe(4));
+
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
     match (a, b) {
@@ -209,8 +218,8 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
 }
 
 fn ensure_equal<'a, S, F1, F2>(
-    x: &'a Expr<S, X>,
-    y: &'a Expr<S, X>,
+    x: &'a Type,
+    y: &'a Type,
     mkerr: F1,
     mkmsg: F2,
 ) -> Result<(), TypeError<S>>
@@ -219,7 +228,7 @@ where
     F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
     F2: FnOnce() -> TypeMessage<S>,
 {
-    if prop_equal(x, y) {
+    if prop_equal(x.as_expr().as_ref(), y.as_expr().as_ref()) {
         Ok(())
     } else {
         Err(mkerr(mkmsg()))
@@ -253,33 +262,40 @@ pub fn type_with(
             _ => Err(mkerr(msg)),
         };
 
+    let mktype =
+        |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
+
     enum Ret {
-        ErrRet(TypeError<X>),
-        OkNormalized(Normalized),
-        OkType(crate::expr::Type),
-        OkRet(Expr<X, X>),
+        RetType(crate::expr::Type),
+        RetExpr(Expr<X, X>),
     }
     use Ret::*;
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
-            let t2 = type_with(ctx, t.clone())?.normalize();
+            let t2 = mktype(ctx, t.clone())?;
             let ctx2 = ctx
-                .insert(x.clone(), t2.0.clone())
+                .insert(x.clone(), t2.as_expr().clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let b = type_with(&ctx2, b.clone())?;
             let _ = type_with(
                 ctx,
                 rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())),
             )?;
-            OkRet(Pi(x.clone(), t2.0, b.get_type().as_expr().clone()))
+            Ok(RetExpr(Pi(
+                x.clone(),
+                t2.as_expr().clone(),
+                b.get_type().as_expr().clone(),
+            )))
         }
         Pi(x, tA, tB) => {
-            let tA = type_with(ctx, tA.clone())?.normalize();
-            let kA =
-                ensure_const(tA.get_type(), InvalidInputType(tA.0.clone()))?;
+            let tA = mktype(ctx, tA.clone())?;
+            let kA = ensure_const(
+                tA.get_type(),
+                InvalidInputType(tA.as_expr().clone()),
+            )?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.0.clone())
+                .insert(x.clone(), tA.as_expr().clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, tB.clone())?;
             let kB = match tB.get_type().as_expr().as_ref() {
@@ -294,11 +310,11 @@ pub fn type_with(
             };
 
             match rule(kA, kB) {
-                Err(()) => ErrRet(mkerr(NoDependentTypes(
-                    tA.0.clone(),
+                Err(()) => Err(mkerr(NoDependentTypes(
+                    tA.as_expr().clone(),
                     tB.get_type().clone(),
                 ))),
-                Ok(_) => OkRet(Const(kB)),
+                Ok(k) => Ok(RetExpr(Const(k))),
             }
         }
         Let(f, mt, r, b) => {
@@ -332,7 +348,7 @@ pub fn type_with(
                 )));
             }
 
-            OkType(b.get_type().clone())
+            Ok(RetType(b.get_type().clone()))
         }
         _ => match e
             .as_ref()
@@ -341,20 +357,20 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(Type) => OkRet(Const(Kind)),
-            Const(Kind) => OkRet(Const(Sort)),
-            Const(Sort) => ErrRet(mkerr(Untyped)),
+            Const(Type) => Ok(RetExpr(Const(Kind))),
+            Const(Kind) => Ok(RetExpr(Const(Sort))),
+            Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
-                Some(e) => OkRet(e.unroll()),
-                None => ErrRet(mkerr(UnboundVariable)),
+                Some(e) => Ok(RetExpr(e.unroll())),
+                None => Err(mkerr(UnboundVariable)),
             },
             App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                let mut tf = f.get_type().as_normalized().clone();
+                let mut tf = f.get_type().clone();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.0.clone());
-                    let (x, tx, tb) = match tf.0.as_ref() {
+                    let (x, tx, tb) = match tf.as_expr().as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(
@@ -363,40 +379,29 @@ pub fn type_with(
                             )));
                         }
                     };
-                    ensure_equal(
-                        tx.as_ref(),
-                        a.get_type().as_expr().as_ref(),
-                        mkerr,
-                        || {
-                            TypeMismatch(
-                                rc(App(f.0.clone(), seen_args.clone())),
-                                tx.clone(),
-                                a.clone(),
-                            )
-                        },
-                    )?;
-                    tf = type_with(
-                        ctx,
-                        subst_shift(&V(x.clone(), 0), &a.0, &tb),
-                    )?
-                    .normalize();
+                    let tx = mktype(ctx, tx.clone())?;
+                    ensure_equal(&tx, a.get_type(), mkerr, || {
+                        TypeMismatch(
+                            rc(App(f.0.clone(), seen_args.clone())),
+                            tx.clone(),
+                            a.clone(),
+                        )
+                    })?;
+                    tf = mktype(ctx, subst_shift(&V(x.clone(), 0), &a.0, &tb))?;
                 }
-                OkNormalized(tf)
+                Ok(RetType(tf))
             }
             Annot(x, t) => {
-                let t = t.normalize();
-                ensure_equal(
-                    t.0.as_ref(),
-                    x.get_type().as_expr().as_ref(),
-                    mkerr,
-                    || AnnotMismatch(x.clone(), t.clone()),
-                )?;
-                OkType(x.get_type().clone())
+                let t = t.normalize().into_type();
+                ensure_equal(&t, x.get_type(), mkerr, || {
+                    AnnotMismatch(x.clone(), t.clone())
+                })?;
+                Ok(RetType(x.get_type().clone()))
             }
             BoolIf(x, y, z) => {
                 ensure_equal(
-                    x.get_type().as_expr().as_ref(),
-                    &Builtin(Bool),
+                    x.get_type(),
+                    &mktype(ctx, rc(Builtin(Bool)))?,
                     mkerr,
                     || InvalidPredicate(x.clone()),
                 )?;
@@ -410,19 +415,16 @@ pub fn type_with(
                     IfBranchMustBeTerm(false, z.clone()),
                 )?;
 
-                ensure_equal(
-                    y.get_type().as_expr().as_ref(),
-                    z.get_type().as_expr().as_ref(),
-                    mkerr,
-                    || IfBranchMismatch(y.clone(), z.clone()),
-                )?;
+                ensure_equal(y.get_type(), z.get_type(), mkerr, || {
+                    IfBranchMismatch(y.clone(), z.clone())
+                })?;
 
-                OkType(y.get_type().clone())
+                Ok(RetType(y.get_type().clone()))
             }
             EmptyListLit(t) => {
                 ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?;
                 let t = t.normalize().0;
-                OkRet(dhall::expr!(List t))
+                Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
@@ -432,26 +434,21 @@ pub fn type_with(
                     InvalidListType(x.get_type().as_expr().clone()),
                 )?;
                 for (i, y) in iter {
-                    ensure_equal(
-                        x.get_type().as_expr().as_ref(),
-                        y.get_type().as_expr().as_ref(),
-                        mkerr,
-                        || {
-                            InvalidListElement(
-                                i,
-                                x.get_type().as_expr().clone(),
-                                y.clone(),
-                            )
-                        },
-                    )?;
+                    ensure_equal(x.get_type(), y.get_type(), mkerr, || {
+                        InvalidListElement(
+                            i,
+                            x.get_type().as_expr().clone(),
+                            y.clone(),
+                        )
+                    })?;
                 }
                 let t = x.get_type().as_expr().clone();
-                OkRet(dhall::expr!(List t))
+                Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?;
                 let t = t.normalize().0;
-                OkRet(dhall::expr!(Optional t))
+                Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
@@ -459,7 +456,7 @@ pub fn type_with(
                     InvalidOptionalType(x.get_type().as_expr().clone()),
                 )?;
                 let t = x.get_type().as_expr().clone();
-                OkRet(dhall::expr!(Optional t))
+                Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
                 for (k, t) in kts {
@@ -468,7 +465,7 @@ pub fn type_with(
                         InvalidFieldType(k.clone(), t.clone()),
                     )?;
                 }
-                OkRet(Const(Type))
+                Ok(RetExpr(Const(Type)))
             }
             RecordLit(kvs) => {
                 let kts = kvs
@@ -481,70 +478,54 @@ pub fn type_with(
                         Ok((k.clone(), v.get_type().as_expr().clone()))
                     })
                     .collect::<Result<_, _>>()?;
-                OkRet(RecordType(kts))
+                Ok(RetExpr(RecordType(kts)))
             }
             Field(r, x) => match r.get_type().as_expr().as_ref() {
                 RecordType(kts) => match kts.get(&x) {
-                    Some(e) => OkRet(e.unroll()),
-                    None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))),
+                    Some(e) => Ok(RetExpr(e.unroll())),
+                    None => Err(mkerr(MissingField(x.clone(), r.clone()))),
                 },
-                _ => ErrRet(mkerr(NotARecord(x.clone(), r.clone()))),
+                _ => Err(mkerr(NotARecord(x.clone(), r.clone()))),
             },
-            Builtin(b) => OkRet(type_of_builtin(b)),
-            BoolLit(_) => OkRet(Builtin(Bool)),
-            NaturalLit(_) => OkRet(Builtin(Natural)),
-            IntegerLit(_) => OkRet(Builtin(Integer)),
-            DoubleLit(_) => OkRet(Builtin(Double)),
+            Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
+            BoolLit(_) => Ok(RetExpr(Builtin(Bool))),
+            NaturalLit(_) => Ok(RetExpr(Builtin(Natural))),
+            IntegerLit(_) => Ok(RetExpr(Builtin(Integer))),
+            DoubleLit(_) => Ok(RetExpr(Builtin(Double))),
             // TODO: check type of interpolations
-            TextLit(_) => OkRet(Builtin(Text)),
+            TextLit(_) => Ok(RetExpr(Builtin(Text))),
             BinOp(o, l, r) => {
-                let t = Builtin(match o {
-                    BoolAnd => Bool,
-                    BoolOr => Bool,
-                    BoolEQ => Bool,
-                    BoolNE => Bool,
-                    NaturalPlus => Natural,
-                    NaturalTimes => Natural,
-                    TextAppend => Text,
-                    _ => panic!("Unimplemented typecheck case: {:?}", e),
-                });
-
-                ensure_equal(
-                    l.get_type().as_expr().as_ref(),
-                    &t,
-                    mkerr,
-                    || BinOpTypeMismatch(o, l.clone()),
+                let t = mktype(
+                    ctx,
+                    rc(Builtin(match o {
+                        BoolAnd => Bool,
+                        BoolOr => Bool,
+                        BoolEQ => Bool,
+                        BoolNE => Bool,
+                        NaturalPlus => Natural,
+                        NaturalTimes => Natural,
+                        TextAppend => Text,
+                        _ => panic!("Unimplemented typecheck case: {:?}", e),
+                    })),
                 )?;
 
-                ensure_equal(
-                    r.get_type().as_expr().as_ref(),
-                    &t,
-                    mkerr,
-                    || BinOpTypeMismatch(o, r.clone()),
-                )?;
+                ensure_equal(l.get_type(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, l.clone())
+                })?;
 
-                OkRet(t)
+                ensure_equal(r.get_type(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, r.clone())
+                })?;
+
+                Ok(RetType(t))
             }
             Embed(p) => match p {},
             _ => panic!("Unimplemented typecheck case: {:?}", e),
         },
-    };
+    }?;
     match ret {
-        OkRet(Const(Sort)) => {
-            Ok(Typed(e, crate::expr::Type(TypeInternal::Universe(3))))
-        }
-        OkRet(ret) => Ok(Typed(
-            e,
-            crate::expr::Type(TypeInternal::Expr(Box::new(
-                type_with(ctx, rc(ret))?.normalize(),
-            ))),
-        )),
-        OkNormalized(ret) => Ok(Typed(
-            e,
-            crate::expr::Type(TypeInternal::Expr(Box::new(ret))),
-        )),
-        OkType(ret) => Ok(Typed(e, ret)),
-        ErrRet(e) => Err(e),
+        RetExpr(ret) => Ok(Typed(e, mktype(ctx, rc(ret))?)),
+        RetType(typ) => Ok(Typed(e, typ)),
     }
 }
 
@@ -567,9 +548,9 @@ pub enum TypeMessage<S> {
     UnboundVariable,
     InvalidInputType(SubExpr<S, X>),
     InvalidOutputType(crate::expr::Type),
-    NotAFunction(SubExpr<S, X>, Normalized),
-    TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, Typed),
-    AnnotMismatch(Typed, Normalized),
+    NotAFunction(SubExpr<S, X>, crate::expr::Type),
+    TypeMismatch(SubExpr<S, X>, crate::expr::Type, Typed),
+    AnnotMismatch(Typed, crate::expr::Type),
     Untyped,
     InvalidListElement(usize, SubExpr<S, X>, Typed),
     InvalidListType(SubExpr<S, X>),
@@ -645,8 +626,8 @@ impl<S> fmt::Display for TypeMessage<S> {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
                     .replace("$txt0", &format!("{}", e0))
-                    .replace("$txt1", &format!("{}", e1))
-                    .replace("$txt2", &format!("{}", e2.0))
+                    .replace("$txt1", &format!("{}", e1.as_expr()))
+                    .replace("$txt2", &format!("{}", e2.as_expr()))
                     .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
                 f.write_str(&s)
             }
-- 
cgit v1.2.3


From 0ce048e4d95b08e50dec0f2e0f6736f3c5b646f2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 00:24:34 +0200
Subject: More typecheck

---
 dhall/src/typecheck.rs | 164 ++++++++++++++++++++++++++-----------------------
 1 file changed, 86 insertions(+), 78 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 0ebc67e..29ad6d4 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,5 +1,4 @@
 #![allow(non_snake_case)]
-use std::collections::HashSet;
 use std::fmt;
 
 use crate::expr::*;
@@ -12,10 +11,6 @@ use self::TypeMessage::*;
 
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
-        // let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
-        //     self.0.clone(),
-        // )?)));
-        // Ok(Typed(self.0, typ))
         let typ = crate::typecheck::type_of_(self.0.clone())?;
         Ok(typ)
     }
@@ -24,11 +19,23 @@ impl Typed {
     fn as_expr(&self) -> &SubExpr<X, X> {
         &self.0
     }
+    fn into_expr(self) -> SubExpr<X, X> {
+        self.0
+    }
+    pub fn into_type(self) -> Type {
+        self.1
+    }
     pub fn get_type(&self) -> &Type {
         &self.1
     }
 }
 impl Normalized {
+    fn as_expr(&self) -> &SubExpr<X, X> {
+        &self.0
+    }
+    fn into_expr(self) -> SubExpr<X, X> {
+        self.0
+    }
     pub fn get_type(&self) -> &Type {
         &self.1
     }
@@ -37,11 +44,8 @@ impl Normalized {
     }
 }
 impl Type {
-    // pub fn as_expr(&self) -> &Normalized {
-    //     &*self.0
-    // }
     fn as_expr(&self) -> &SubExpr<X, X> {
-        &self.as_normalized().0
+        &self.as_normalized().as_expr()
     }
     fn as_normalized(&self) -> &Normalized {
         use TypeInternal::*;
@@ -50,13 +54,24 @@ impl Type {
             Universe(_) => unimplemented!(),
         }
     }
+    fn into_expr(self) -> SubExpr<X, X> {
+        use TypeInternal::*;
+        match self.0 {
+            Expr(e) => e.into_expr(),
+            Universe(_) => unimplemented!(),
+        }
+    }
     pub fn get_type(&self) -> &Type {
-        self.as_normalized().get_type()
+        use TypeInternal::*;
+        match &self.0 {
+            Expr(e) => e.get_type(),
+            Universe(_) => unimplemented!(),
+            // Universe(n) => &Type(Universe(n+1)),
+        }
     }
 }
 
-const TYPE_OF_SORT: crate::expr::Type =
-    crate::expr::Type(TypeInternal::Universe(4));
+const TYPE_OF_SORT: Type = Type(TypeInternal::Universe(4));
 
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
@@ -89,11 +104,7 @@ fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
 }
 
 // Takes normalized expressions as input
-fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
-where
-    S: ::std::fmt::Debug,
-    T: ::std::fmt::Debug,
-{
+fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
     use dhall_core::ExprF::*;
     fn go<S, T>(
         ctx: &mut Vec<(Label, Label)>,
@@ -149,8 +160,16 @@ where
             (_, _) => false,
         }
     }
-    let mut ctx = vec![];
-    go::<S, T>(&mut ctx, eL0, eR0)
+    match (&eL0.0, &eR0.0) {
+        (TypeInternal::Universe(l), TypeInternal::Universe(r)) if r == l => {
+            true
+        }
+        (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
+            let mut ctx = vec![];
+            go(&mut ctx, l.as_expr().as_ref(), r.as_expr().as_ref())
+        }
+        _ => false,
+    }
 }
 
 fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
@@ -228,18 +247,17 @@ where
     F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
     F2: FnOnce() -> TypeMessage<S>,
 {
-    if prop_equal(x.as_expr().as_ref(), y.as_expr().as_ref()) {
+    if prop_equal(x, y) {
         Ok(())
     } else {
         Err(mkerr(mkmsg()))
     }
 }
 
-/// Type-check an expression and return the expression's type if type-checking
-/// succeeds or an error if type-checking fails
+/// Type-check an expression and return the expression alongside its type
+/// if type-checking succeeded, or an error if type-checking failed
 ///
-/// `type_with` normalizes the type since while type-checking. It expects the
-/// context to contain only normalized expressions.
+/// `type_with` expects the context to contain only normalized expressions.
 pub fn type_with(
     ctx: &Context<Label, SubExpr<X, X>>,
     e: SubExpr<X, X>,
@@ -284,15 +302,12 @@ pub fn type_with(
             Ok(RetExpr(Pi(
                 x.clone(),
                 t2.as_expr().clone(),
-                b.get_type().as_expr().clone(),
+                b.into_type().into_expr(),
             )))
         }
         Pi(x, tA, tB) => {
             let tA = mktype(ctx, tA.clone())?;
-            let kA = ensure_const(
-                tA.get_type(),
-                InvalidInputType(tA.as_expr().clone()),
-            )?;
+            let kA = ensure_const(tA.get_type(), InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.as_expr().clone())
@@ -311,7 +326,7 @@ pub fn type_with(
 
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
-                    tA.as_expr().clone(),
+                    tA.clone(),
                     tB.get_type().clone(),
                 ))),
                 Ok(k) => Ok(RetExpr(Const(k))),
@@ -329,7 +344,7 @@ pub fn type_with(
             // message because this should never happen anyway
             let kR = ensure_const(
                 r.get_type().get_type(),
-                InvalidInputType(r.get_type().as_expr().clone()),
+                InvalidInputType(r.get_type().clone()),
             )?;
 
             let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone());
@@ -343,8 +358,8 @@ pub fn type_with(
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.get_type().as_expr().clone(),
-                    b.get_type().as_expr().clone(),
+                    r.into_type(),
+                    b.into_type(),
                 )));
             }
 
@@ -369,25 +384,31 @@ pub fn type_with(
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
                 let mut tf = f.get_type().clone();
                 while let Some(a) = iter.next() {
-                    seen_args.push(a.0.clone());
+                    seen_args.push(a.as_expr().clone());
                     let (x, tx, tb) = match tf.as_expr().as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
-                            return Err(mkerr(NotAFunction(
-                                rc(App(f.0.clone(), seen_args)),
+                            return Err(mkerr(NotAFunction(Typed(
+                                rc(App(f.into_expr(), seen_args)),
                                 tf,
-                            )));
+                            ))));
                         }
                     };
                     let tx = mktype(ctx, tx.clone())?;
                     ensure_equal(&tx, a.get_type(), mkerr, || {
                         TypeMismatch(
-                            rc(App(f.0.clone(), seen_args.clone())),
+                            Typed(
+                                rc(App(f.as_expr().clone(), seen_args.clone())),
+                                tf.clone(),
+                            ),
                             tx.clone(),
                             a.clone(),
                         )
                     })?;
-                    tf = mktype(ctx, subst_shift(&V(x.clone(), 0), &a.0, &tb))?;
+                    tf = mktype(
+                        ctx,
+                        subst_shift(&V(x.clone(), 0), &a.as_expr(), &tb),
+                    )?;
                 }
                 Ok(RetType(tf))
             }
@@ -422,8 +443,9 @@ pub fn type_with(
                 Ok(RetType(y.get_type().clone()))
             }
             EmptyListLit(t) => {
-                ensure_is_type(t.get_type(), InvalidListType(t.0.clone()))?;
-                let t = t.normalize().0;
+                let t = t.normalize().into_type();
+                ensure_is_type(t.get_type(), InvalidListType(t.clone()))?;
+                let t = t.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
@@ -431,31 +453,28 @@ pub fn type_with(
                 let (_, x) = iter.next().unwrap();
                 ensure_is_type(
                     x.get_type().get_type(),
-                    InvalidListType(x.get_type().as_expr().clone()),
+                    InvalidListType(x.get_type().clone()),
                 )?;
                 for (i, y) in iter {
                     ensure_equal(x.get_type(), y.get_type(), mkerr, || {
-                        InvalidListElement(
-                            i,
-                            x.get_type().as_expr().clone(),
-                            y.clone(),
-                        )
+                        InvalidListElement(i, x.get_type().clone(), y.clone())
                     })?;
                 }
-                let t = x.get_type().as_expr().clone();
+                let t = x.into_type().into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
-                ensure_is_type(t.get_type(), InvalidOptionalType(t.0.clone()))?;
-                let t = t.normalize().0;
+                let t = t.normalize().into_type();
+                ensure_is_type(t.get_type(), InvalidOptionalType(t.clone()))?;
+                let t = t.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
                     x.get_type().get_type(),
-                    InvalidOptionalType(x.get_type().as_expr().clone()),
+                    InvalidOptionalType(x.get_type().clone()),
                 )?;
-                let t = x.get_type().as_expr().clone();
+                let t = x.into_type().into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
@@ -475,7 +494,7 @@ pub fn type_with(
                             v.get_type().get_type(),
                             InvalidField(k.clone(), v.clone()),
                         )?;
-                        Ok((k.clone(), v.get_type().as_expr().clone()))
+                        Ok((k.clone(), v.into_type().into_expr()))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
@@ -534,7 +553,7 @@ pub fn type_with(
 /// will fail.
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e).map(|e| e.get_type().as_expr().clone())
+    type_with(&ctx, e).map(|e| e.into_type().into_expr())
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -546,39 +565,28 @@ pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(SubExpr<S, X>),
-    InvalidOutputType(crate::expr::Type),
-    NotAFunction(SubExpr<S, X>, crate::expr::Type),
-    TypeMismatch(SubExpr<S, X>, crate::expr::Type, Typed),
-    AnnotMismatch(Typed, crate::expr::Type),
+    InvalidInputType(Type),
+    InvalidOutputType(Type),
+    NotAFunction(Typed),
+    TypeMismatch(Typed, Type, Typed),
+    AnnotMismatch(Typed, Type),
     Untyped,
-    InvalidListElement(usize, SubExpr<S, X>, Typed),
-    InvalidListType(SubExpr<S, X>),
-    InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
-    InvalidOptionalLiteral(usize),
-    InvalidOptionalType(SubExpr<S, X>),
+    InvalidListElement(usize, Type, Typed),
+    InvalidListType(Type),
+    InvalidOptionalType(Type),
     InvalidPredicate(Typed),
     IfBranchMismatch(Typed, Typed),
     IfBranchMustBeTerm(bool, Typed),
     InvalidField(Label, Typed),
     InvalidFieldType(Label, Typed),
-    InvalidAlternative(Label, SubExpr<S, X>),
-    InvalidAlternativeType(Label, SubExpr<S, X>),
     DuplicateAlternative(Label),
-    MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
     FieldCollision(Label),
-    MustMergeARecord(SubExpr<S, X>, SubExpr<S, X>),
-    MustMergeUnion(SubExpr<S, X>, SubExpr<S, X>),
-    UnusedHandler(HashSet<Label>),
-    MissingHandler(HashSet<Label>),
-    HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
-    HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
-    HandlerNotAFunction(Label, SubExpr<S, X>),
     NotARecord(Label, Typed),
     MissingField(Label, Typed),
     BinOpTypeMismatch(BinOp, Typed),
-    NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
-    NoDependentTypes(SubExpr<S, X>, crate::expr::Type),
+    NoDependentLet(Type, Type),
+    NoDependentTypes(Type, Type),
+    MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
 }
 
 /// A structured type error that includes context
@@ -609,7 +617,7 @@ impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
             UnboundVariable => "Unbound variable",
             InvalidInputType(_) => "Invalid function input",
             InvalidOutputType(_) => "Invalid function output",
-            NotAFunction(_, _) => "Not a function",
+            NotAFunction(_) => "Not a function",
             TypeMismatch(_, _, _) => "Wrong type of function argument",
             _ => "Unhandled error",
         }
@@ -625,7 +633,7 @@ impl<S> fmt::Display for TypeMessage<S> {
             TypeMismatch(e0, e1, e2) => {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
-                    .replace("$txt0", &format!("{}", e0))
+                    .replace("$txt0", &format!("{}", e0.as_expr()))
                     .replace("$txt1", &format!("{}", e1.as_expr()))
                     .replace("$txt2", &format!("{}", e2.as_expr()))
                     .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
-- 
cgit v1.2.3


From da9937f623f2698adec50718e1e703958e837c85 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 01:08:02 +0200
Subject: Put a Cow in Type

---
 dhall/src/typecheck.rs | 148 ++++++++++++++++++++++++++-----------------------
 1 file changed, 78 insertions(+), 70 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 29ad6d4..a703821 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,6 +6,7 @@ use dhall_core;
 use dhall_core::context::Context;
 use dhall_core::*;
 use dhall_generator as dhall;
+use std::borrow::Cow;
 
 use self::TypeMessage::*;
 
@@ -22,11 +23,8 @@ impl Typed {
     fn into_expr(self) -> SubExpr<X, X> {
         self.0
     }
-    pub fn into_type(self) -> Type {
-        self.1
-    }
-    pub fn get_type(&self) -> &Type {
-        &self.1
+    pub fn get_type<'a>(&'a self) -> Type<'a> {
+        self.1.reborrow()
     }
 }
 impl Normalized {
@@ -36,42 +34,47 @@ impl Normalized {
     fn into_expr(self) -> SubExpr<X, X> {
         self.0
     }
-    pub fn get_type(&self) -> &Type {
-        &self.1
+    pub fn get_type<'a>(&'a self) -> Type<'a> {
+        self.1.reborrow()
     }
-    fn into_type(self) -> Type {
-        crate::expr::Type(TypeInternal::Expr(Box::new(self)))
+    fn into_type(self) -> Type<'static> {
+        crate::expr::Type(Cow::Owned(TypeInternal::Expr(Box::new(self))))
     }
 }
-impl Type {
-    fn as_expr(&self) -> &SubExpr<X, X> {
-        &self.as_normalized().as_expr()
+impl<'a> Type<'a> {
+    fn into_owned(self) -> Type<'static> {
+        Type(Cow::Owned(self.0.into_owned()))
     }
-    fn as_normalized(&self) -> &Normalized {
-        use TypeInternal::*;
+    fn reborrow<'b>(&'b self) -> Type<'b> {
         match &self.0 {
-            Expr(e) => &e,
+            Cow::Owned(x) => crate::expr::Type(Cow::Borrowed(x)),
+            Cow::Borrowed(x) => crate::expr::Type(Cow::Borrowed(x)),
+        }
+    }
+    fn as_expr(&'a self) -> &'a SubExpr<X, X> {
+        use TypeInternal::*;
+        match self.0.as_ref() {
+            Expr(e) => e.as_expr(),
             Universe(_) => unimplemented!(),
         }
     }
     fn into_expr(self) -> SubExpr<X, X> {
         use TypeInternal::*;
-        match self.0 {
+        match self.0.into_owned() {
             Expr(e) => e.into_expr(),
             Universe(_) => unimplemented!(),
         }
     }
-    pub fn get_type(&self) -> &Type {
+    pub fn get_type<'b>(&'b self) -> Type<'b> {
         use TypeInternal::*;
-        match &self.0 {
+        match self.0.as_ref() {
             Expr(e) => e.get_type(),
-            Universe(_) => unimplemented!(),
-            // Universe(n) => &Type(Universe(n+1)),
+            Universe(n) => crate::expr::Type(Cow::Owned(Universe(n + 1))),
         }
     }
 }
 
-const TYPE_OF_SORT: Type = Type(TypeInternal::Universe(4));
+const TYPE_OF_SORT: Type<'static> = Type(Cow::Owned(TypeInternal::Universe(4)));
 
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
@@ -160,7 +163,7 @@ fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
             (_, _) => false,
         }
     }
-    match (&eL0.0, &eR0.0) {
+    match (&*eL0.0, &*eR0.0) {
         (TypeInternal::Universe(l), TypeInternal::Universe(r)) if r == l => {
             true
         }
@@ -237,8 +240,8 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
 }
 
 fn ensure_equal<'a, S, F1, F2>(
-    x: &'a Type,
-    y: &'a Type,
+    x: &Type<'a>,
+    y: &Type<'a>,
     mkerr: F1,
     mkmsg: F2,
 ) -> Result<(), TypeError<S>>
@@ -284,7 +287,7 @@ pub fn type_with(
         |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
 
     enum Ret {
-        RetType(crate::expr::Type),
+        RetType(crate::expr::Type<'static>),
         RetExpr(Expr<X, X>),
     }
     use Ret::*;
@@ -302,12 +305,13 @@ pub fn type_with(
             Ok(RetExpr(Pi(
                 x.clone(),
                 t2.as_expr().clone(),
-                b.into_type().into_expr(),
+                b.get_type().into_expr(),
             )))
         }
         Pi(x, tA, tB) => {
             let tA = mktype(ctx, tA.clone())?;
-            let kA = ensure_const(tA.get_type(), InvalidInputType(tA.clone()))?;
+            let kA =
+                ensure_const(&tA.get_type(), InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.as_expr().clone())
@@ -319,7 +323,7 @@ pub fn type_with(
                     return Err(TypeError::new(
                         &ctx2,
                         e.clone(),
-                        InvalidOutputType(tB.get_type().clone()),
+                        InvalidOutputType(tB.get_type().into_owned()),
                     ));
                 }
             };
@@ -327,7 +331,7 @@ pub fn type_with(
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
                     tA.clone(),
-                    tB.get_type().clone(),
+                    tB.get_type().into_owned(),
                 ))),
                 Ok(k) => Ok(RetExpr(Const(k))),
             }
@@ -343,8 +347,8 @@ pub fn type_with(
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kR = ensure_const(
-                r.get_type().get_type(),
-                InvalidInputType(r.get_type().clone()),
+                &r.get_type().get_type(),
+                InvalidInputType(r.get_type().into_owned()),
             )?;
 
             let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone());
@@ -352,18 +356,18 @@ pub fn type_with(
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(
-                b.get_type().get_type(),
-                InvalidOutputType(b.get_type().clone()),
+                &b.get_type().get_type(),
+                InvalidOutputType(b.get_type().into_owned()),
             )?;
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.into_type(),
-                    b.into_type(),
+                    r.get_type().into_owned(),
+                    b.get_type().into_owned(),
                 )));
             }
 
-            Ok(RetType(b.get_type().clone()))
+            Ok(RetType(b.get_type().into_owned()))
         }
         _ => match e
             .as_ref()
@@ -382,7 +386,7 @@ pub fn type_with(
             App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                let mut tf = f.get_type().clone();
+                let mut tf = f.get_type().into_owned();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.as_expr().clone());
                     let (x, tx, tb) = match tf.as_expr().as_ref() {
@@ -395,7 +399,7 @@ pub fn type_with(
                         }
                     };
                     let tx = mktype(ctx, tx.clone())?;
-                    ensure_equal(&tx, a.get_type(), mkerr, || {
+                    ensure_equal(&tx, &a.get_type(), mkerr, || {
                         TypeMismatch(
                             Typed(
                                 rc(App(f.as_expr().clone(), seen_args.clone())),
@@ -414,37 +418,37 @@ pub fn type_with(
             }
             Annot(x, t) => {
                 let t = t.normalize().into_type();
-                ensure_equal(&t, x.get_type(), mkerr, || {
+                ensure_equal(&t, &x.get_type(), mkerr, || {
                     AnnotMismatch(x.clone(), t.clone())
                 })?;
-                Ok(RetType(x.get_type().clone()))
+                Ok(RetType(x.get_type().into_owned()))
             }
             BoolIf(x, y, z) => {
                 ensure_equal(
-                    x.get_type(),
+                    &x.get_type(),
                     &mktype(ctx, rc(Builtin(Bool)))?,
                     mkerr,
                     || InvalidPredicate(x.clone()),
                 )?;
                 ensure_is_type(
-                    y.get_type().get_type(),
+                    &y.get_type().get_type(),
                     IfBranchMustBeTerm(true, y.clone()),
                 )?;
 
                 ensure_is_type(
-                    z.get_type().get_type(),
+                    &z.get_type().get_type(),
                     IfBranchMustBeTerm(false, z.clone()),
                 )?;
 
-                ensure_equal(y.get_type(), z.get_type(), mkerr, || {
+                ensure_equal(&y.get_type(), &z.get_type(), mkerr, || {
                     IfBranchMismatch(y.clone(), z.clone())
                 })?;
 
-                Ok(RetType(y.get_type().clone()))
+                Ok(RetType(y.get_type().into_owned()))
             }
             EmptyListLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type(t.get_type(), InvalidListType(t.clone()))?;
+                ensure_is_type(&t.get_type(), InvalidListType(t.clone()))?;
                 let t = t.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
@@ -452,35 +456,39 @@ pub fn type_with(
                 let mut iter = xs.into_iter().enumerate();
                 let (_, x) = iter.next().unwrap();
                 ensure_is_type(
-                    x.get_type().get_type(),
-                    InvalidListType(x.get_type().clone()),
+                    &x.get_type().get_type(),
+                    InvalidListType(x.get_type().into_owned()),
                 )?;
                 for (i, y) in iter {
-                    ensure_equal(x.get_type(), y.get_type(), mkerr, || {
-                        InvalidListElement(i, x.get_type().clone(), y.clone())
+                    ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
+                        InvalidListElement(
+                            i,
+                            x.get_type().into_owned(),
+                            y.clone(),
+                        )
                     })?;
                 }
-                let t = x.into_type().into_expr();
+                let t = x.get_type().into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type(t.get_type(), InvalidOptionalType(t.clone()))?;
+                ensure_is_type(&t.get_type(), InvalidOptionalType(t.clone()))?;
                 let t = t.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
-                    x.get_type().get_type(),
-                    InvalidOptionalType(x.get_type().clone()),
+                    &x.get_type().get_type(),
+                    InvalidOptionalType(x.get_type().into_owned()),
                 )?;
-                let t = x.into_type().into_expr();
+                let t = x.get_type().into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
                 for (k, t) in kts {
                     ensure_is_type(
-                        t.get_type(),
+                        &t.get_type(),
                         InvalidFieldType(k.clone(), t.clone()),
                     )?;
                 }
@@ -491,10 +499,10 @@ pub fn type_with(
                     .into_iter()
                     .map(|(k, v)| {
                         ensure_is_type(
-                            v.get_type().get_type(),
+                            &v.get_type().get_type(),
                             InvalidField(k.clone(), v.clone()),
                         )?;
-                        Ok((k.clone(), v.into_type().into_expr()))
+                        Ok((k.clone(), v.get_type().into_expr()))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
@@ -528,11 +536,11 @@ pub fn type_with(
                     })),
                 )?;
 
-                ensure_equal(l.get_type(), &t, mkerr, || {
+                ensure_equal(&l.get_type(), &t, mkerr, || {
                     BinOpTypeMismatch(o, l.clone())
                 })?;
 
-                ensure_equal(r.get_type(), &t, mkerr, || {
+                ensure_equal(&r.get_type(), &t, mkerr, || {
                     BinOpTypeMismatch(o, r.clone())
                 })?;
 
@@ -553,7 +561,7 @@ pub fn type_with(
 /// will fail.
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e).map(|e| e.into_type().into_expr())
+    type_with(&ctx, e).map(|e| e.get_type().into_expr())
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -565,15 +573,15 @@ pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(Type),
-    InvalidOutputType(Type),
+    InvalidInputType(Type<'static>),
+    InvalidOutputType(Type<'static>),
     NotAFunction(Typed),
-    TypeMismatch(Typed, Type, Typed),
-    AnnotMismatch(Typed, Type),
+    TypeMismatch(Typed, Type<'static>, Typed),
+    AnnotMismatch(Typed, Type<'static>),
     Untyped,
-    InvalidListElement(usize, Type, Typed),
-    InvalidListType(Type),
-    InvalidOptionalType(Type),
+    InvalidListElement(usize, Type<'static>, Typed),
+    InvalidListType(Type<'static>),
+    InvalidOptionalType(Type<'static>),
     InvalidPredicate(Typed),
     IfBranchMismatch(Typed, Typed),
     IfBranchMustBeTerm(bool, Typed),
@@ -584,8 +592,8 @@ pub enum TypeMessage<S> {
     NotARecord(Label, Typed),
     MissingField(Label, Typed),
     BinOpTypeMismatch(BinOp, Typed),
-    NoDependentLet(Type, Type),
-    NoDependentTypes(Type, Type),
+    NoDependentLet(Type<'static>, Type<'static>),
+    NoDependentTypes(Type<'static>, Type<'static>),
     MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
 }
 
-- 
cgit v1.2.3


From b96f187dfc6373b6e2faee01e085d7e3dff893ca Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 01:18:31 +0200
Subject: Handle universe error properly

---
 dhall/src/typecheck.rs | 84 +++++++++++++++++++++++++++++---------------------
 1 file changed, 49 insertions(+), 35 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index a703821..becabbd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -51,18 +51,26 @@ impl<'a> Type<'a> {
             Cow::Borrowed(x) => crate::expr::Type(Cow::Borrowed(x)),
         }
     }
-    fn as_expr(&'a self) -> &'a SubExpr<X, X> {
+    fn as_expr(&'a self) -> Result<&'a SubExpr<X, X>, TypeError<X>> {
         use TypeInternal::*;
         match self.0.as_ref() {
-            Expr(e) => e.as_expr(),
-            Universe(_) => unimplemented!(),
+            Expr(e) => Ok(e.as_expr()),
+            Universe(_) => Err(TypeError::new(
+                &Context::new(),
+                rc(ExprF::Const(Const::Sort)),
+                TypeMessage::Untyped,
+            )),
         }
     }
-    fn into_expr(self) -> SubExpr<X, X> {
+    fn into_expr(self) -> Result<SubExpr<X, X>, TypeError<X>> {
         use TypeInternal::*;
         match self.0.into_owned() {
-            Expr(e) => e.into_expr(),
-            Universe(_) => unimplemented!(),
+            Expr(e) => Ok(e.into_expr()),
+            Universe(_) => Err(TypeError::new(
+                &Context::new(),
+                rc(ExprF::Const(Const::Sort)),
+                TypeMessage::Untyped,
+            )),
         }
     }
     pub fn get_type<'b>(&'b self) -> Type<'b> {
@@ -270,18 +278,20 @@ pub fn type_with(
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
-    let ensure_const =
-        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref()
-        {
-            Const(k) => Ok(*k),
-            _ => Err(mkerr(msg)),
-        };
-    let ensure_is_type =
-        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref()
-        {
-            Const(Type) => Ok(()),
-            _ => Err(mkerr(msg)),
-        };
+    let ensure_const = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
+        .as_expr()?
+        .as_ref()
+    {
+        Const(k) => Ok(*k),
+        _ => Err(mkerr(msg)),
+    };
+    let ensure_is_type = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
+        .as_expr()?
+        .as_ref()
+    {
+        Const(Type) => Ok(()),
+        _ => Err(mkerr(msg)),
+    };
 
     let mktype =
         |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
@@ -295,17 +305,17 @@ pub fn type_with(
         Lam(x, t, b) => {
             let t2 = mktype(ctx, t.clone())?;
             let ctx2 = ctx
-                .insert(x.clone(), t2.as_expr().clone())
+                .insert(x.clone(), t2.as_expr()?.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let b = type_with(&ctx2, b.clone())?;
             let _ = type_with(
                 ctx,
-                rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())),
+                rc(Pi(x.clone(), t.clone(), b.get_type().as_expr()?.clone())),
             )?;
             Ok(RetExpr(Pi(
                 x.clone(),
-                t2.as_expr().clone(),
-                b.get_type().into_expr(),
+                t2.as_expr()?.clone(),
+                b.get_type().into_expr()?,
             )))
         }
         Pi(x, tA, tB) => {
@@ -314,10 +324,10 @@ pub fn type_with(
                 ensure_const(&tA.get_type(), InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.as_expr().clone())
+                .insert(x.clone(), tA.as_expr()?.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, tB.clone())?;
-            let kB = match tB.get_type().as_expr().as_ref() {
+            let kB = match tB.get_type().as_expr()?.as_ref() {
                 Const(k) => *k,
                 _ => {
                     return Err(TypeError::new(
@@ -351,7 +361,7 @@ pub fn type_with(
                 InvalidInputType(r.get_type().into_owned()),
             )?;
 
-            let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone());
+            let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr()?.clone());
             let b = type_with(&ctx2, b.clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
@@ -389,7 +399,7 @@ pub fn type_with(
                 let mut tf = f.get_type().into_owned();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.as_expr().clone());
-                    let (x, tx, tb) = match tf.as_expr().as_ref() {
+                    let (x, tx, tb) = match tf.as_expr()?.as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(Typed(
@@ -449,7 +459,7 @@ pub fn type_with(
             EmptyListLit(t) => {
                 let t = t.normalize().into_type();
                 ensure_is_type(&t.get_type(), InvalidListType(t.clone()))?;
-                let t = t.into_expr();
+                let t = t.into_expr()?;
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
@@ -468,13 +478,13 @@ pub fn type_with(
                         )
                     })?;
                 }
-                let t = x.get_type().into_expr();
+                let t = x.get_type().into_expr()?;
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 let t = t.normalize().into_type();
                 ensure_is_type(&t.get_type(), InvalidOptionalType(t.clone()))?;
-                let t = t.into_expr();
+                let t = t.into_expr()?;
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
@@ -482,7 +492,7 @@ pub fn type_with(
                     &x.get_type().get_type(),
                     InvalidOptionalType(x.get_type().into_owned()),
                 )?;
-                let t = x.get_type().into_expr();
+                let t = x.get_type().into_expr()?;
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
@@ -502,12 +512,12 @@ pub fn type_with(
                             &v.get_type().get_type(),
                             InvalidField(k.clone(), v.clone()),
                         )?;
-                        Ok((k.clone(), v.get_type().into_expr()))
+                        Ok((k.clone(), v.get_type().into_expr()?))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
             }
-            Field(r, x) => match r.get_type().as_expr().as_ref() {
+            Field(r, x) => match r.get_type().as_expr()?.as_ref() {
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => Ok(RetExpr(e.unroll())),
                     None => Err(mkerr(MissingField(x.clone(), r.clone()))),
@@ -561,7 +571,8 @@ pub fn type_with(
 /// will fail.
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e).map(|e| e.get_type().into_expr())
+    let e = type_with(&ctx, e)?;
+    e.get_type().into_expr()
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -642,9 +653,12 @@ impl<S> fmt::Display for TypeMessage<S> {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
                     .replace("$txt0", &format!("{}", e0.as_expr()))
-                    .replace("$txt1", &format!("{}", e1.as_expr()))
+                    .replace("$txt1", &format!("{}", e1.as_expr().unwrap()))
                     .replace("$txt2", &format!("{}", e2.as_expr()))
-                    .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
+                    .replace(
+                        "$txt3",
+                        &format!("{}", e2.get_type().as_expr().unwrap()),
+                    );
                 f.write_str(&s)
             }
             _ => f.write_str("Unhandled error message"),
-- 
cgit v1.2.3


From 619290e208f59bb15fc4f9d4b6dae2c19bb7b711 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 01:41:08 +0200
Subject: Augment stack size for typecheck tests

---
 dhall/src/typecheck.rs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index becabbd..fe9f68c 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -17,40 +17,50 @@ impl Resolved {
     }
 }
 impl Typed {
+    #[inline(always)]
     fn as_expr(&self) -> &SubExpr<X, X> {
         &self.0
     }
+    #[inline(always)]
     fn into_expr(self) -> SubExpr<X, X> {
         self.0
     }
+    #[inline(always)]
     pub fn get_type<'a>(&'a self) -> Type<'a> {
         self.1.reborrow()
     }
 }
 impl Normalized {
+    #[inline(always)]
     fn as_expr(&self) -> &SubExpr<X, X> {
         &self.0
     }
+    #[inline(always)]
     fn into_expr(self) -> SubExpr<X, X> {
         self.0
     }
+    #[inline(always)]
     pub fn get_type<'a>(&'a self) -> Type<'a> {
         self.1.reborrow()
     }
+    #[inline(always)]
     fn into_type(self) -> Type<'static> {
         crate::expr::Type(Cow::Owned(TypeInternal::Expr(Box::new(self))))
     }
 }
 impl<'a> Type<'a> {
+    #[inline(always)]
     fn into_owned(self) -> Type<'static> {
         Type(Cow::Owned(self.0.into_owned()))
     }
+    #[inline(always)]
     fn reborrow<'b>(&'b self) -> Type<'b> {
         match &self.0 {
             Cow::Owned(x) => crate::expr::Type(Cow::Borrowed(x)),
             Cow::Borrowed(x) => crate::expr::Type(Cow::Borrowed(x)),
         }
     }
+    #[inline(always)]
     fn as_expr(&'a self) -> Result<&'a SubExpr<X, X>, TypeError<X>> {
         use TypeInternal::*;
         match self.0.as_ref() {
@@ -62,6 +72,7 @@ impl<'a> Type<'a> {
             )),
         }
     }
+    #[inline(always)]
     fn into_expr(self) -> Result<SubExpr<X, X>, TypeError<X>> {
         use TypeInternal::*;
         match self.0.into_owned() {
@@ -73,6 +84,7 @@ impl<'a> Type<'a> {
             )),
         }
     }
+    #[inline(always)]
     pub fn get_type<'b>(&'b self) -> Type<'b> {
         use TypeInternal::*;
         match self.0.as_ref() {
-- 
cgit v1.2.3


From 354ccf95ff03fa39b8812e6b138db2b1993a981e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 01:54:16 +0200
Subject: Store Normalized in type error

---
 dhall/src/typecheck.rs | 112 +++++++++++++++++++++++++++++--------------------
 1 file changed, 66 insertions(+), 46 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index fe9f68c..3815f9f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -61,10 +61,10 @@ impl<'a> Type<'a> {
         }
     }
     #[inline(always)]
-    fn as_expr(&'a self) -> Result<&'a SubExpr<X, X>, TypeError<X>> {
+    fn as_expr(&'a self) -> Result<&'a Normalized, TypeError<X>> {
         use TypeInternal::*;
         match self.0.as_ref() {
-            Expr(e) => Ok(e.as_expr()),
+            Expr(e) => Ok(e),
             Universe(_) => Err(TypeError::new(
                 &Context::new(),
                 rc(ExprF::Const(Const::Sort)),
@@ -73,10 +73,10 @@ impl<'a> Type<'a> {
         }
     }
     #[inline(always)]
-    fn into_expr(self) -> Result<SubExpr<X, X>, TypeError<X>> {
+    fn into_expr(self) -> Result<Normalized, TypeError<X>> {
         use TypeInternal::*;
         match self.0.into_owned() {
-            Expr(e) => Ok(e.into_expr()),
+            Expr(e) => Ok(*e),
             Universe(_) => Err(TypeError::new(
                 &Context::new(),
                 rc(ExprF::Const(Const::Sort)),
@@ -292,6 +292,7 @@ pub fn type_with(
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
     let ensure_const = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
         .as_expr()?
+        .as_expr()
         .as_ref()
     {
         Const(k) => Ok(*k),
@@ -299,6 +300,7 @@ pub fn type_with(
     };
     let ensure_is_type = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
         .as_expr()?
+        .as_expr()
         .as_ref()
     {
         Const(Type) => Ok(()),
@@ -317,43 +319,51 @@ pub fn type_with(
         Lam(x, t, b) => {
             let t2 = mktype(ctx, t.clone())?;
             let ctx2 = ctx
-                .insert(x.clone(), t2.as_expr()?.clone())
+                .insert(x.clone(), t2.as_expr()?.as_expr().clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let b = type_with(&ctx2, b.clone())?;
             let _ = type_with(
                 ctx,
-                rc(Pi(x.clone(), t.clone(), b.get_type().as_expr()?.clone())),
+                rc(Pi(
+                    x.clone(),
+                    t.clone(),
+                    b.get_type().as_expr()?.as_expr().clone(),
+                )),
             )?;
             Ok(RetExpr(Pi(
                 x.clone(),
-                t2.as_expr()?.clone(),
-                b.get_type().into_expr()?,
+                t2.as_expr()?.as_expr().clone(),
+                b.get_type().into_expr()?.into_expr(),
             )))
         }
         Pi(x, tA, tB) => {
             let tA = mktype(ctx, tA.clone())?;
-            let kA =
-                ensure_const(&tA.get_type(), InvalidInputType(tA.clone()))?;
+            let kA = ensure_const(
+                &tA.get_type(),
+                InvalidInputType(tA.clone().into_expr()?),
+            )?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.as_expr()?.clone())
+                .insert(x.clone(), tA.as_expr()?.as_expr().clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, tB.clone())?;
-            let kB = match tB.get_type().as_expr()?.as_ref() {
+            let kB = match tB.get_type().as_expr()?.as_expr().as_ref() {
                 Const(k) => *k,
                 _ => {
                     return Err(TypeError::new(
                         &ctx2,
                         e.clone(),
-                        InvalidOutputType(tB.get_type().into_owned()),
+                        InvalidOutputType(
+                            tB.get_type().into_owned().into_expr()?,
+                        ),
                     ));
                 }
             };
 
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
-                    tA.clone(),
-                    tB.get_type().into_owned(),
+                    tA.clone().into_expr()?,
+                    tB.get_type().into_owned().into_expr()?,
                 ))),
                 Ok(k) => Ok(RetExpr(Const(k))),
             }
@@ -370,22 +380,23 @@ pub fn type_with(
             // message because this should never happen anyway
             let kR = ensure_const(
                 &r.get_type().get_type(),
-                InvalidInputType(r.get_type().into_owned()),
+                InvalidInputType(r.get_type().into_owned().into_expr()?),
             )?;
 
-            let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr()?.clone());
+            let ctx2 = ctx
+                .insert(f.clone(), r.get_type().as_expr()?.as_expr().clone());
             let b = type_with(&ctx2, b.clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(
                 &b.get_type().get_type(),
-                InvalidOutputType(b.get_type().into_owned()),
+                InvalidOutputType(b.get_type().into_owned().into_expr()?),
             )?;
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.get_type().into_owned(),
-                    b.get_type().into_owned(),
+                    r.get_type().into_owned().into_expr()?,
+                    b.get_type().into_owned().into_expr()?,
                 )));
             }
 
@@ -411,7 +422,7 @@ pub fn type_with(
                 let mut tf = f.get_type().into_owned();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.as_expr().clone());
-                    let (x, tx, tb) = match tf.as_expr()?.as_ref() {
+                    let (x, tx, tb) = match tf.as_expr()?.as_expr().as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(Typed(
@@ -427,7 +438,7 @@ pub fn type_with(
                                 rc(App(f.as_expr().clone(), seen_args.clone())),
                                 tf.clone(),
                             ),
-                            tx.clone(),
+                            tx.clone().into_expr().unwrap(),
                             a.clone(),
                         )
                     })?;
@@ -441,7 +452,7 @@ pub fn type_with(
             Annot(x, t) => {
                 let t = t.normalize().into_type();
                 ensure_equal(&t, &x.get_type(), mkerr, || {
-                    AnnotMismatch(x.clone(), t.clone())
+                    AnnotMismatch(x.clone(), t.clone().into_expr().unwrap())
                 })?;
                 Ok(RetType(x.get_type().into_owned()))
             }
@@ -470,8 +481,11 @@ pub fn type_with(
             }
             EmptyListLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type(&t.get_type(), InvalidListType(t.clone()))?;
-                let t = t.into_expr()?;
+                ensure_is_type(
+                    &t.get_type(),
+                    InvalidListType(t.clone().into_expr()?),
+                )?;
+                let t = t.into_expr()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
@@ -479,32 +493,35 @@ pub fn type_with(
                 let (_, x) = iter.next().unwrap();
                 ensure_is_type(
                     &x.get_type().get_type(),
-                    InvalidListType(x.get_type().into_owned()),
+                    InvalidListType(x.get_type().into_owned().into_expr()?),
                 )?;
                 for (i, y) in iter {
                     ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
                         InvalidListElement(
                             i,
-                            x.get_type().into_owned(),
+                            x.get_type().into_owned().into_expr().unwrap(),
                             y.clone(),
                         )
                     })?;
                 }
-                let t = x.get_type().into_expr()?;
+                let t = x.get_type().into_expr()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type(&t.get_type(), InvalidOptionalType(t.clone()))?;
-                let t = t.into_expr()?;
+                ensure_is_type(
+                    &t.get_type(),
+                    InvalidOptionalType(t.clone().into_expr()?),
+                )?;
+                let t = t.into_expr()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
                     &x.get_type().get_type(),
-                    InvalidOptionalType(x.get_type().into_owned()),
+                    InvalidOptionalType(x.get_type().into_owned().into_expr()?),
                 )?;
-                let t = x.get_type().into_expr()?;
+                let t = x.get_type().into_expr()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
@@ -524,12 +541,12 @@ pub fn type_with(
                             &v.get_type().get_type(),
                             InvalidField(k.clone(), v.clone()),
                         )?;
-                        Ok((k.clone(), v.get_type().into_expr()?))
+                        Ok((k.clone(), v.get_type().into_expr()?.into_expr()))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
             }
-            Field(r, x) => match r.get_type().as_expr()?.as_ref() {
+            Field(r, x) => match r.get_type().as_expr()?.as_expr().as_ref() {
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => Ok(RetExpr(e.unroll())),
                     None => Err(mkerr(MissingField(x.clone(), r.clone()))),
@@ -584,7 +601,7 @@ pub fn type_with(
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
     let e = type_with(&ctx, e)?;
-    e.get_type().into_expr()
+    Ok(e.get_type().into_expr()?.into_expr())
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -596,15 +613,15 @@ pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(Type<'static>),
-    InvalidOutputType(Type<'static>),
+    InvalidInputType(Normalized),
+    InvalidOutputType(Normalized),
     NotAFunction(Typed),
-    TypeMismatch(Typed, Type<'static>, Typed),
-    AnnotMismatch(Typed, Type<'static>),
+    TypeMismatch(Typed, Normalized, Typed),
+    AnnotMismatch(Typed, Normalized),
     Untyped,
-    InvalidListElement(usize, Type<'static>, Typed),
-    InvalidListType(Type<'static>),
-    InvalidOptionalType(Type<'static>),
+    InvalidListElement(usize, Normalized, Typed),
+    InvalidListType(Normalized),
+    InvalidOptionalType(Normalized),
     InvalidPredicate(Typed),
     IfBranchMismatch(Typed, Typed),
     IfBranchMustBeTerm(bool, Typed),
@@ -615,8 +632,8 @@ pub enum TypeMessage<S> {
     NotARecord(Label, Typed),
     MissingField(Label, Typed),
     BinOpTypeMismatch(BinOp, Typed),
-    NoDependentLet(Type<'static>, Type<'static>),
-    NoDependentTypes(Type<'static>, Type<'static>),
+    NoDependentLet(Normalized, Normalized),
+    NoDependentTypes(Normalized, Normalized),
     MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
 }
 
@@ -665,11 +682,14 @@ impl<S> fmt::Display for TypeMessage<S> {
                 let template = include_str!("errors/TypeMismatch.txt");
                 let s = template
                     .replace("$txt0", &format!("{}", e0.as_expr()))
-                    .replace("$txt1", &format!("{}", e1.as_expr().unwrap()))
+                    .replace("$txt1", &format!("{}", e1.as_expr()))
                     .replace("$txt2", &format!("{}", e2.as_expr()))
                     .replace(
                         "$txt3",
-                        &format!("{}", e2.get_type().as_expr().unwrap()),
+                        &format!(
+                            "{}",
+                            e2.get_type().as_expr().unwrap().as_expr()
+                        ),
                     );
                 f.write_str(&s)
             }
-- 
cgit v1.2.3


From c461548c32f8cb3ee2db5ade88ae4f91b3838ab5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 11:09:57 +0200
Subject: Avoid constructing exprs manually when possible

---
 dhall/src/typecheck.rs | 38 ++++++++++++++++++++------------------
 1 file changed, 20 insertions(+), 18 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 3815f9f..5be43cf 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -370,7 +370,9 @@ pub fn type_with(
         }
         Let(f, mt, r, b) => {
             let r = if let Some(t) = mt {
-                rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
+                let r = SubExpr::clone(r);
+                let t = SubExpr::clone(t);
+                dhall::subexpr!(r: t)
             } else {
                 SubExpr::clone(r)
             };
@@ -409,8 +411,8 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(Type) => Ok(RetExpr(Const(Kind))),
-            Const(Kind) => Ok(RetExpr(Const(Sort))),
+            Const(Type) => Ok(RetExpr(dhall::expr!(Kind))),
+            Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
             Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
                 Some(e) => Ok(RetExpr(e.unroll())),
@@ -531,7 +533,7 @@ pub fn type_with(
                         InvalidFieldType(k.clone(), t.clone()),
                     )?;
                 }
-                Ok(RetExpr(Const(Type)))
+                Ok(RetExpr(dhall::expr!(Type)))
             }
             RecordLit(kvs) => {
                 let kts = kvs
@@ -554,25 +556,25 @@ pub fn type_with(
                 _ => Err(mkerr(NotARecord(x.clone(), r.clone()))),
             },
             Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
-            BoolLit(_) => Ok(RetExpr(Builtin(Bool))),
-            NaturalLit(_) => Ok(RetExpr(Builtin(Natural))),
-            IntegerLit(_) => Ok(RetExpr(Builtin(Integer))),
-            DoubleLit(_) => Ok(RetExpr(Builtin(Double))),
+            BoolLit(_) => Ok(RetExpr(dhall::expr!(Bool))),
+            NaturalLit(_) => Ok(RetExpr(dhall::expr!(Natural))),
+            IntegerLit(_) => Ok(RetExpr(dhall::expr!(Integer))),
+            DoubleLit(_) => Ok(RetExpr(dhall::expr!(Double))),
             // TODO: check type of interpolations
-            TextLit(_) => Ok(RetExpr(Builtin(Text))),
+            TextLit(_) => Ok(RetExpr(dhall::expr!(Text))),
             BinOp(o, l, r) => {
                 let t = mktype(
                     ctx,
-                    rc(Builtin(match o {
-                        BoolAnd => Bool,
-                        BoolOr => Bool,
-                        BoolEQ => Bool,
-                        BoolNE => Bool,
-                        NaturalPlus => Natural,
-                        NaturalTimes => Natural,
-                        TextAppend => Text,
+                    match o {
+                        BoolAnd => dhall::subexpr!(Bool),
+                        BoolOr => dhall::subexpr!(Bool),
+                        BoolEQ => dhall::subexpr!(Bool),
+                        BoolNE => dhall::subexpr!(Bool),
+                        NaturalPlus => dhall::subexpr!(Natural),
+                        NaturalTimes => dhall::subexpr!(Natural),
+                        TextAppend => dhall::subexpr!(Text),
                         _ => panic!("Unimplemented typecheck case: {:?}", e),
-                    })),
+                    },
                 )?;
 
                 ensure_equal(&l.get_type(), &t, mkerr, || {
-- 
cgit v1.2.3


From b1906923a59e9313c4c9e32f37e4c86f2040cc1f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 12:04:53 +0200
Subject: More typecheck

---
 dhall/src/typecheck.rs | 155 ++++++++++++++++++++++++++++---------------------
 1 file changed, 89 insertions(+), 66 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5be43cf..f380448 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -47,6 +47,16 @@ impl Normalized {
     fn into_type(self) -> Type<'static> {
         crate::expr::Type(Cow::Owned(TypeInternal::Expr(Box::new(self))))
     }
+    // Expose the outermost constructor
+    #[inline(always)]
+    fn unroll_ref(&self) -> &Expr<X, X> {
+        self.as_expr().as_ref()
+    }
+    #[inline(always)]
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        // shift the type too ?
+        Normalized(shift(delta, var, &self.0), self.1.clone())
+    }
 }
 impl<'a> Type<'a> {
     #[inline(always)]
@@ -61,7 +71,7 @@ impl<'a> Type<'a> {
         }
     }
     #[inline(always)]
-    fn as_expr(&'a self) -> Result<&'a Normalized, TypeError<X>> {
+    fn as_normalized(&'a self) -> Result<&'a Normalized, TypeError<X>> {
         use TypeInternal::*;
         match self.0.as_ref() {
             Expr(e) => Ok(e),
@@ -73,7 +83,7 @@ impl<'a> Type<'a> {
         }
     }
     #[inline(always)]
-    fn into_expr(self) -> Result<Normalized, TypeError<X>> {
+    fn into_normalized(self) -> Result<Normalized, TypeError<X>> {
         use TypeInternal::*;
         match self.0.into_owned() {
             Expr(e) => Ok(*e),
@@ -84,6 +94,11 @@ impl<'a> Type<'a> {
             )),
         }
     }
+    // Expose the outermost constructor
+    #[inline(always)]
+    fn unroll_ref(&'a self) -> Result<&'a Expr<X, X>, TypeError<X>> {
+        Ok(self.as_normalized()?.unroll_ref())
+    }
     #[inline(always)]
     pub fn get_type<'b>(&'b self) -> Type<'b> {
         use TypeInternal::*;
@@ -92,6 +107,15 @@ impl<'a> Type<'a> {
             Universe(n) => crate::expr::Type(Cow::Owned(Universe(n + 1))),
         }
     }
+    #[inline(always)]
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        use TypeInternal::*;
+        crate::expr::Type(Cow::Owned(match self.reborrow().0 {
+            Cow::Borrowed(Expr(e)) => Expr(Box::new(e.shift(delta, var))),
+            Cow::Borrowed(Universe(n)) => Universe(*n),
+            Cow::Owned(_) => unreachable!(),
+        }))
+    }
 }
 
 const TYPE_OF_SORT: Type<'static> = Type(Cow::Owned(TypeInternal::Universe(4)));
@@ -189,7 +213,7 @@ fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
         }
         (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
             let mut ctx = vec![];
-            go(&mut ctx, l.as_expr().as_ref(), r.as_expr().as_ref())
+            go(&mut ctx, l.unroll_ref(), r.unroll_ref())
         }
         _ => false,
     }
@@ -279,10 +303,8 @@ where
 
 /// Type-check an expression and return the expression alongside its type
 /// if type-checking succeeded, or an error if type-checking failed
-///
-/// `type_with` expects the context to contain only normalized expressions.
 pub fn type_with(
-    ctx: &Context<Label, SubExpr<X, X>>,
+    ctx: &Context<Label, Type<'static>>,
     e: SubExpr<X, X>,
 ) -> Result<Typed, TypeError<X>> {
     use dhall_core::BinOp::*;
@@ -290,22 +312,16 @@ pub fn type_with(
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
-    let ensure_const = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
-        .as_expr()?
-        .as_expr()
-        .as_ref()
-    {
-        Const(k) => Ok(*k),
-        _ => Err(mkerr(msg)),
-    };
-    let ensure_is_type = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
-        .as_expr()?
-        .as_expr()
-        .as_ref()
-    {
-        Const(Type) => Ok(()),
-        _ => Err(mkerr(msg)),
-    };
+    let ensure_const =
+        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.unroll_ref()? {
+            Const(k) => Ok(*k),
+            _ => Err(mkerr(msg)),
+        };
+    let ensure_is_type =
+        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.unroll_ref()? {
+            Const(Type) => Ok(()),
+            _ => Err(mkerr(msg)),
+        };
 
     let mktype =
         |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
@@ -317,44 +333,39 @@ pub fn type_with(
     use Ret::*;
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
-            let t2 = mktype(ctx, t.clone())?;
+            let t = mktype(ctx, t.clone())?;
             let ctx2 = ctx
-                .insert(x.clone(), t2.as_expr()?.as_expr().clone())
-                .map(|e| shift(1, &V(x.clone(), 0), e));
+                .insert(x.clone(), t.clone())
+                .map(|e| e.shift(1, &V(x.clone(), 0)));
             let b = type_with(&ctx2, b.clone())?;
-            let _ = type_with(
+            Ok(RetType(mktype(
                 ctx,
                 rc(Pi(
                     x.clone(),
-                    t.clone(),
-                    b.get_type().as_expr()?.as_expr().clone(),
+                    t.into_normalized()?.into_expr(),
+                    b.get_type().into_normalized()?.into_expr(),
                 )),
-            )?;
-            Ok(RetExpr(Pi(
-                x.clone(),
-                t2.as_expr()?.as_expr().clone(),
-                b.get_type().into_expr()?.into_expr(),
-            )))
+            )?))
         }
         Pi(x, tA, tB) => {
             let tA = mktype(ctx, tA.clone())?;
             let kA = ensure_const(
                 &tA.get_type(),
-                InvalidInputType(tA.clone().into_expr()?),
+                InvalidInputType(tA.clone().into_normalized()?),
             )?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.as_expr()?.as_expr().clone())
-                .map(|e| shift(1, &V(x.clone(), 0), e));
+                .insert(x.clone(), tA.clone())
+                .map(|e| e.shift(1, &V(x.clone(), 0)));
             let tB = type_with(&ctx2, tB.clone())?;
-            let kB = match tB.get_type().as_expr()?.as_expr().as_ref() {
+            let kB = match tB.get_type().unroll_ref()? {
                 Const(k) => *k,
                 _ => {
                     return Err(TypeError::new(
                         &ctx2,
                         e.clone(),
                         InvalidOutputType(
-                            tB.get_type().into_owned().into_expr()?,
+                            tB.get_type().into_owned().into_normalized()?,
                         ),
                     ));
                 }
@@ -362,8 +373,8 @@ pub fn type_with(
 
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
-                    tA.clone().into_expr()?,
-                    tB.get_type().into_owned().into_expr()?,
+                    tA.clone().into_normalized()?,
+                    tB.get_type().into_owned().into_normalized()?,
                 ))),
                 Ok(k) => Ok(RetExpr(Const(k))),
             }
@@ -382,23 +393,22 @@ pub fn type_with(
             // message because this should never happen anyway
             let kR = ensure_const(
                 &r.get_type().get_type(),
-                InvalidInputType(r.get_type().into_owned().into_expr()?),
+                InvalidInputType(r.get_type().into_owned().into_normalized()?),
             )?;
 
-            let ctx2 = ctx
-                .insert(f.clone(), r.get_type().as_expr()?.as_expr().clone());
+            let ctx2 = ctx.insert(f.clone(), r.get_type().into_owned());
             let b = type_with(&ctx2, b.clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(
                 &b.get_type().get_type(),
-                InvalidOutputType(b.get_type().into_owned().into_expr()?),
+                InvalidOutputType(b.get_type().into_owned().into_normalized()?),
             )?;
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.get_type().into_owned().into_expr()?,
-                    b.get_type().into_owned().into_expr()?,
+                    r.get_type().into_owned().into_normalized()?,
+                    b.get_type().into_owned().into_normalized()?,
                 )));
             }
 
@@ -415,7 +425,7 @@ pub fn type_with(
             Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
             Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
-                Some(e) => Ok(RetExpr(e.unroll())),
+                Some(e) => Ok(RetType(e.clone())),
                 None => Err(mkerr(UnboundVariable)),
             },
             App(f, args) => {
@@ -424,7 +434,7 @@ pub fn type_with(
                 let mut tf = f.get_type().into_owned();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.as_expr().clone());
-                    let (x, tx, tb) = match tf.as_expr()?.as_expr().as_ref() {
+                    let (x, tx, tb) = match tf.unroll_ref()? {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(Typed(
@@ -440,7 +450,7 @@ pub fn type_with(
                                 rc(App(f.as_expr().clone(), seen_args.clone())),
                                 tf.clone(),
                             ),
-                            tx.clone().into_expr().unwrap(),
+                            tx.clone().into_normalized().unwrap(),
                             a.clone(),
                         )
                     })?;
@@ -454,7 +464,10 @@ pub fn type_with(
             Annot(x, t) => {
                 let t = t.normalize().into_type();
                 ensure_equal(&t, &x.get_type(), mkerr, || {
-                    AnnotMismatch(x.clone(), t.clone().into_expr().unwrap())
+                    AnnotMismatch(
+                        x.clone(),
+                        t.clone().into_normalized().unwrap(),
+                    )
                 })?;
                 Ok(RetType(x.get_type().into_owned()))
             }
@@ -485,9 +498,9 @@ pub fn type_with(
                 let t = t.normalize().into_type();
                 ensure_is_type(
                     &t.get_type(),
-                    InvalidListType(t.clone().into_expr()?),
+                    InvalidListType(t.clone().into_normalized()?),
                 )?;
-                let t = t.into_expr()?.into_expr();
+                let t = t.into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
@@ -495,35 +508,42 @@ pub fn type_with(
                 let (_, x) = iter.next().unwrap();
                 ensure_is_type(
                     &x.get_type().get_type(),
-                    InvalidListType(x.get_type().into_owned().into_expr()?),
+                    InvalidListType(
+                        x.get_type().into_owned().into_normalized()?,
+                    ),
                 )?;
                 for (i, y) in iter {
                     ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
                         InvalidListElement(
                             i,
-                            x.get_type().into_owned().into_expr().unwrap(),
+                            x.get_type()
+                                .into_owned()
+                                .into_normalized()
+                                .unwrap(),
                             y.clone(),
                         )
                     })?;
                 }
-                let t = x.get_type().into_expr()?.into_expr();
+                let t = x.get_type().into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 let t = t.normalize().into_type();
                 ensure_is_type(
                     &t.get_type(),
-                    InvalidOptionalType(t.clone().into_expr()?),
+                    InvalidOptionalType(t.clone().into_normalized()?),
                 )?;
-                let t = t.into_expr()?.into_expr();
+                let t = t.into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
                 ensure_is_type(
                     &x.get_type().get_type(),
-                    InvalidOptionalType(x.get_type().into_owned().into_expr()?),
+                    InvalidOptionalType(
+                        x.get_type().into_owned().into_normalized()?,
+                    ),
                 )?;
-                let t = x.get_type().into_expr()?.into_expr();
+                let t = x.get_type().into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
@@ -543,12 +563,15 @@ pub fn type_with(
                             &v.get_type().get_type(),
                             InvalidField(k.clone(), v.clone()),
                         )?;
-                        Ok((k.clone(), v.get_type().into_expr()?.into_expr()))
+                        Ok((
+                            k.clone(),
+                            v.get_type().into_normalized()?.into_expr(),
+                        ))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
             }
-            Field(r, x) => match r.get_type().as_expr()?.as_expr().as_ref() {
+            Field(r, x) => match r.get_type().unroll_ref()? {
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => Ok(RetExpr(e.unroll())),
                     None => Err(mkerr(MissingField(x.clone(), r.clone()))),
@@ -603,7 +626,7 @@ pub fn type_with(
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
     let e = type_with(&ctx, e)?;
-    Ok(e.get_type().into_expr()?.into_expr())
+    Ok(e.get_type().into_normalized()?.into_expr())
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -642,14 +665,14 @@ pub enum TypeMessage<S> {
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<S> {
-    pub context: Context<Label, SubExpr<S, X>>,
+    pub context: Context<Label, Type<'static>>,
     pub current: SubExpr<S, X>,
     pub type_message: TypeMessage<S>,
 }
 
 impl<S> TypeError<S> {
     pub fn new(
-        context: &Context<Label, SubExpr<S, X>>,
+        context: &Context<Label, Type<'static>>,
         current: SubExpr<S, X>,
         type_message: TypeMessage<S>,
     ) -> Self {
@@ -690,7 +713,7 @@ impl<S> fmt::Display for TypeMessage<S> {
                         "$txt3",
                         &format!(
                             "{}",
-                            e2.get_type().as_expr().unwrap().as_expr()
+                            e2.get_type().as_normalized().unwrap().as_expr()
                         ),
                     );
                 f.write_str(&s)
-- 
cgit v1.2.3


From d454d31ea07b70ff6d3f8d4d1014d37d954241dd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 12:29:48 +0200
Subject: Universe hierarchy is overkill

---
 dhall/src/typecheck.rs | 132 ++++++++++++++++++++++---------------------------
 1 file changed, 59 insertions(+), 73 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f380448..9eead93 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,6 @@ use dhall_core;
 use dhall_core::context::Context;
 use dhall_core::*;
 use dhall_generator as dhall;
-use std::borrow::Cow;
 
 use self::TypeMessage::*;
 
@@ -26,8 +25,12 @@ impl Typed {
         self.0
     }
     #[inline(always)]
-    pub fn get_type<'a>(&'a self) -> Type<'a> {
-        self.1.reborrow()
+    pub fn get_type(&self) -> &Type {
+        &self.1
+    }
+    #[inline(always)]
+    fn get_type_move(self) -> Type {
+        self.1
     }
 }
 impl Normalized {
@@ -40,12 +43,12 @@ impl Normalized {
         self.0
     }
     #[inline(always)]
-    pub fn get_type<'a>(&'a self) -> Type<'a> {
-        self.1.reborrow()
+    pub fn get_type(&self) -> &Type {
+        &self.1
     }
     #[inline(always)]
-    fn into_type(self) -> Type<'static> {
-        crate::expr::Type(Cow::Owned(TypeInternal::Expr(Box::new(self))))
+    fn into_type(self) -> Type {
+        crate::expr::Type(TypeInternal::Expr(Box::new(self)))
     }
     // Expose the outermost constructor
     #[inline(always)]
@@ -58,24 +61,13 @@ impl Normalized {
         Normalized(shift(delta, var, &self.0), self.1.clone())
     }
 }
-impl<'a> Type<'a> {
-    #[inline(always)]
-    fn into_owned(self) -> Type<'static> {
-        Type(Cow::Owned(self.0.into_owned()))
-    }
-    #[inline(always)]
-    fn reborrow<'b>(&'b self) -> Type<'b> {
-        match &self.0 {
-            Cow::Owned(x) => crate::expr::Type(Cow::Borrowed(x)),
-            Cow::Borrowed(x) => crate::expr::Type(Cow::Borrowed(x)),
-        }
-    }
+impl Type {
     #[inline(always)]
-    fn as_normalized(&'a self) -> Result<&'a Normalized, TypeError<X>> {
+    fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
         use TypeInternal::*;
-        match self.0.as_ref() {
+        match &self.0 {
             Expr(e) => Ok(e),
-            Universe(_) => Err(TypeError::new(
+            Untyped => Err(TypeError::new(
                 &Context::new(),
                 rc(ExprF::Const(Const::Sort)),
                 TypeMessage::Untyped,
@@ -85,9 +77,9 @@ impl<'a> Type<'a> {
     #[inline(always)]
     fn into_normalized(self) -> Result<Normalized, TypeError<X>> {
         use TypeInternal::*;
-        match self.0.into_owned() {
+        match self.0 {
             Expr(e) => Ok(*e),
-            Universe(_) => Err(TypeError::new(
+            Untyped => Err(TypeError::new(
                 &Context::new(),
                 rc(ExprF::Const(Const::Sort)),
                 TypeMessage::Untyped,
@@ -96,29 +88,28 @@ impl<'a> Type<'a> {
     }
     // Expose the outermost constructor
     #[inline(always)]
-    fn unroll_ref(&'a self) -> Result<&'a Expr<X, X>, TypeError<X>> {
+    fn unroll_ref(&self) -> Result<&Expr<X, X>, TypeError<X>> {
         Ok(self.as_normalized()?.unroll_ref())
     }
     #[inline(always)]
-    pub fn get_type<'b>(&'b self) -> Type<'b> {
+    pub fn get_type(&self) -> &Type {
         use TypeInternal::*;
-        match self.0.as_ref() {
+        match &self.0 {
             Expr(e) => e.get_type(),
-            Universe(n) => crate::expr::Type(Cow::Owned(Universe(n + 1))),
+            Untyped => &UNTYPE,
         }
     }
     #[inline(always)]
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         use TypeInternal::*;
-        crate::expr::Type(Cow::Owned(match self.reborrow().0 {
-            Cow::Borrowed(Expr(e)) => Expr(Box::new(e.shift(delta, var))),
-            Cow::Borrowed(Universe(n)) => Universe(*n),
-            Cow::Owned(_) => unreachable!(),
-        }))
+        crate::expr::Type(match &self.0 {
+            Expr(e) => Expr(Box::new(e.shift(delta, var))),
+            Untyped => Untyped,
+        })
     }
 }
 
-const TYPE_OF_SORT: Type<'static> = Type(Cow::Owned(TypeInternal::Universe(4)));
+const UNTYPE: Type = Type(TypeInternal::Untyped);
 
 fn rule(a: Const, b: Const) -> Result<Const, ()> {
     use dhall_core::Const::*;
@@ -207,10 +198,8 @@ fn prop_equal(eL0: &Type, eR0: &Type) -> bool {
             (_, _) => false,
         }
     }
-    match (&*eL0.0, &*eR0.0) {
-        (TypeInternal::Universe(l), TypeInternal::Universe(r)) if r == l => {
-            true
-        }
+    match (&eL0.0, &eR0.0) {
+        (TypeInternal::Untyped, TypeInternal::Untyped) => false,
         (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
             let mut ctx = vec![];
             go(&mut ctx, l.unroll_ref(), r.unroll_ref())
@@ -283,9 +272,9 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
     }
 }
 
-fn ensure_equal<'a, S, F1, F2>(
-    x: &Type<'a>,
-    y: &Type<'a>,
+fn ensure_equal<S, F1, F2>(
+    x: &Type,
+    y: &Type,
     mkerr: F1,
     mkmsg: F2,
 ) -> Result<(), TypeError<S>>
@@ -304,7 +293,7 @@ where
 /// Type-check an expression and return the expression alongside its type
 /// if type-checking succeeded, or an error if type-checking failed
 pub fn type_with(
-    ctx: &Context<Label, Type<'static>>,
+    ctx: &Context<Label, Type>,
     e: SubExpr<X, X>,
 ) -> Result<Typed, TypeError<X>> {
     use dhall_core::BinOp::*;
@@ -327,7 +316,7 @@ pub fn type_with(
         |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
 
     enum Ret {
-        RetType(crate::expr::Type<'static>),
+        RetType(crate::expr::Type),
         RetExpr(Expr<X, X>),
     }
     use Ret::*;
@@ -343,7 +332,7 @@ pub fn type_with(
                 rc(Pi(
                     x.clone(),
                     t.into_normalized()?.into_expr(),
-                    b.get_type().into_normalized()?.into_expr(),
+                    b.get_type_move().into_normalized()?.into_expr(),
                 )),
             )?))
         }
@@ -365,7 +354,7 @@ pub fn type_with(
                         &ctx2,
                         e.clone(),
                         InvalidOutputType(
-                            tB.get_type().into_owned().into_normalized()?,
+                            tB.get_type_move().into_normalized()?,
                         ),
                     ));
                 }
@@ -374,7 +363,7 @@ pub fn type_with(
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
                     tA.clone().into_normalized()?,
-                    tB.get_type().into_owned().into_normalized()?,
+                    tB.get_type_move().into_normalized()?,
                 ))),
                 Ok(k) => Ok(RetExpr(Const(k))),
             }
@@ -393,26 +382,26 @@ pub fn type_with(
             // message because this should never happen anyway
             let kR = ensure_const(
                 &r.get_type().get_type(),
-                InvalidInputType(r.get_type().into_owned().into_normalized()?),
+                InvalidInputType(r.get_type().clone().into_normalized()?),
             )?;
 
-            let ctx2 = ctx.insert(f.clone(), r.get_type().into_owned());
+            let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
             let b = type_with(&ctx2, b.clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(
                 &b.get_type().get_type(),
-                InvalidOutputType(b.get_type().into_owned().into_normalized()?),
+                InvalidOutputType(b.get_type().clone().into_normalized()?),
             )?;
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
-                    r.get_type().into_owned().into_normalized()?,
-                    b.get_type().into_owned().into_normalized()?,
+                    r.get_type_move().into_normalized()?,
+                    b.get_type_move().into_normalized()?,
                 )));
             }
 
-            Ok(RetType(b.get_type().into_owned()))
+            Ok(RetType(b.get_type_move()))
         }
         _ => match e
             .as_ref()
@@ -423,7 +412,7 @@ pub fn type_with(
             Let(_, _, _, _) => unreachable!(),
             Const(Type) => Ok(RetExpr(dhall::expr!(Kind))),
             Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))),
-            Const(Sort) => Ok(RetType(TYPE_OF_SORT)),
+            Const(Sort) => Ok(RetType(UNTYPE)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
                 Some(e) => Ok(RetType(e.clone())),
                 None => Err(mkerr(UnboundVariable)),
@@ -431,7 +420,7 @@ pub fn type_with(
             App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                let mut tf = f.get_type().into_owned();
+                let mut tf = f.get_type().clone();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.as_expr().clone());
                     let (x, tx, tb) = match tf.unroll_ref()? {
@@ -469,7 +458,7 @@ pub fn type_with(
                         t.clone().into_normalized().unwrap(),
                     )
                 })?;
-                Ok(RetType(x.get_type().into_owned()))
+                Ok(RetType(x.get_type_move()))
             }
             BoolIf(x, y, z) => {
                 ensure_equal(
@@ -492,7 +481,7 @@ pub fn type_with(
                     IfBranchMismatch(y.clone(), z.clone())
                 })?;
 
-                Ok(RetType(y.get_type().into_owned()))
+                Ok(RetType(y.get_type_move()))
             }
             EmptyListLit(t) => {
                 let t = t.normalize().into_type();
@@ -508,23 +497,18 @@ pub fn type_with(
                 let (_, x) = iter.next().unwrap();
                 ensure_is_type(
                     &x.get_type().get_type(),
-                    InvalidListType(
-                        x.get_type().into_owned().into_normalized()?,
-                    ),
+                    InvalidListType(x.get_type().clone().into_normalized()?),
                 )?;
                 for (i, y) in iter {
                     ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
                         InvalidListElement(
                             i,
-                            x.get_type()
-                                .into_owned()
-                                .into_normalized()
-                                .unwrap(),
+                            x.get_type().clone().into_normalized().unwrap(),
                             y.clone(),
                         )
                     })?;
                 }
-                let t = x.get_type().into_normalized()?.into_expr();
+                let t = x.get_type_move().into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
@@ -540,10 +524,10 @@ pub fn type_with(
                 ensure_is_type(
                     &x.get_type().get_type(),
                     InvalidOptionalType(
-                        x.get_type().into_owned().into_normalized()?,
+                        x.get_type().clone().into_normalized()?,
                     ),
                 )?;
-                let t = x.get_type().into_normalized()?.into_expr();
+                let t = x.get_type_move().into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
@@ -565,7 +549,7 @@ pub fn type_with(
                         )?;
                         Ok((
                             k.clone(),
-                            v.get_type().into_normalized()?.into_expr(),
+                            v.get_type_move().into_normalized()?.into_expr(),
                         ))
                     })
                     .collect::<Result<_, _>>()?;
@@ -624,14 +608,16 @@ pub fn type_with(
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
 pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
-    let ctx = Context::new();
-    let e = type_with(&ctx, e)?;
-    Ok(e.get_type().into_normalized()?.into_expr())
+    let e = type_of_(e)?;
+    Ok(e.get_type_move().into_normalized()?.into_expr())
 }
 
 pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e)
+    let e = type_with(&ctx, e)?;
+    // Ensure the inferred type isn't UNTYPE
+    e.get_type().as_normalized()?;
+    Ok(e)
 }
 
 /// The specific type error
@@ -665,14 +651,14 @@ pub enum TypeMessage<S> {
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<S> {
-    pub context: Context<Label, Type<'static>>,
+    pub context: Context<Label, Type>,
     pub current: SubExpr<S, X>,
     pub type_message: TypeMessage<S>,
 }
 
 impl<S> TypeError<S> {
     pub fn new(
-        context: &Context<Label, Type<'static>>,
+        context: &Context<Label, Type>,
         current: SubExpr<S, X>,
         type_message: TypeMessage<S>,
     ) -> Self {
-- 
cgit v1.2.3


From 0f5b69ac599a4b6979de465cf520ff5c283cfdbd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 14:17:38 +0200
Subject: Use macros in typecheck; much cleaner

---
 dhall/src/typecheck.rs | 257 ++++++++++++++++++++++++-------------------------
 1 file changed, 125 insertions(+), 132 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 9eead93..a0782f8 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -272,22 +272,33 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
     }
 }
 
-fn ensure_equal<S, F1, F2>(
-    x: &Type,
-    y: &Type,
-    mkerr: F1,
-    mkmsg: F2,
-) -> Result<(), TypeError<S>>
-where
-    S: std::fmt::Debug,
-    F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
-    F2: FnOnce() -> TypeMessage<S>,
-{
-    if prop_equal(x, y) {
-        Ok(())
-    } else {
-        Err(mkerr(mkmsg()))
-    }
+macro_rules! ensure_equal {
+    ($x:expr, $y:expr, $err:expr $(,)*) => {
+        if !prop_equal(&$x, &$y) {
+            return Err($err);
+        }
+    };
+}
+
+macro_rules! ensure_matches {
+    ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => {
+        match $x.unroll_ref()? {
+            $pat => $branch,
+            _ => return Err($err),
+        }
+    };
+}
+
+macro_rules! ensure_is_type {
+    ($x:expr, $err:expr $(,)*) => {
+        ensure_matches!($x, Const(Type) => {}, $err)
+    };
+}
+
+macro_rules! ensure_is_const {
+    ($x:expr, $err:expr $(,)*) => {
+        ensure_matches!($x, Const(k) => *k, $err)
+    };
 }
 
 /// Type-check an expression and return the expression alongside its type
@@ -301,16 +312,6 @@ pub fn type_with(
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
-    let ensure_const =
-        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.unroll_ref()? {
-            Const(k) => Ok(*k),
-            _ => Err(mkerr(msg)),
-        };
-    let ensure_is_type =
-        |x: &crate::expr::Type, msg: TypeMessage<_>| match x.unroll_ref()? {
-            Const(Type) => Ok(()),
-            _ => Err(mkerr(msg)),
-        };
 
     let mktype =
         |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
@@ -338,27 +339,23 @@ pub fn type_with(
         }
         Pi(x, tA, tB) => {
             let tA = mktype(ctx, tA.clone())?;
-            let kA = ensure_const(
+            let kA = ensure_is_const!(
                 &tA.get_type(),
-                InvalidInputType(tA.clone().into_normalized()?),
-            )?;
+                mkerr(InvalidInputType(tA.into_normalized()?)),
+            );
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.clone())
                 .map(|e| e.shift(1, &V(x.clone(), 0)));
             let tB = type_with(&ctx2, tB.clone())?;
-            let kB = match tB.get_type().unroll_ref()? {
-                Const(k) => *k,
-                _ => {
-                    return Err(TypeError::new(
-                        &ctx2,
-                        e.clone(),
-                        InvalidOutputType(
-                            tB.get_type_move().into_normalized()?,
-                        ),
-                    ));
-                }
-            };
+            let kB = ensure_is_const!(
+                &tB.get_type(),
+                TypeError::new(
+                    &ctx2,
+                    e.clone(),
+                    InvalidOutputType(tB.get_type_move().into_normalized()?),
+                ),
+            );
 
             match rule(kA, kB) {
                 Err(()) => Err(mkerr(NoDependentTypes(
@@ -380,19 +377,19 @@ pub fn type_with(
             let r = type_with(ctx, r)?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
-            let kR = ensure_const(
+            let kR = ensure_is_const!(
                 &r.get_type().get_type(),
-                InvalidInputType(r.get_type().clone().into_normalized()?),
-            )?;
+                mkerr(InvalidInputType(r.get_type_move().into_normalized()?)),
+            );
 
             let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
             let b = type_with(&ctx2, b.clone())?;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
-            let kB = ensure_const(
+            let kB = ensure_is_const!(
                 &b.get_type().get_type(),
-                InvalidOutputType(b.get_type().clone().into_normalized()?),
-            )?;
+                mkerr(InvalidOutputType(b.get_type_move().into_normalized()?)),
+            );
 
             if let Err(()) = rule(kR, kB) {
                 return Err(mkerr(NoDependentLet(
@@ -423,26 +420,23 @@ pub fn type_with(
                 let mut tf = f.get_type().clone();
                 while let Some(a) = iter.next() {
                     seen_args.push(a.as_expr().clone());
-                    let (x, tx, tb) = match tf.unroll_ref()? {
+                    let (x, tx, tb) = ensure_matches!(tf,
                         Pi(x, tx, tb) => (x, tx, tb),
-                        _ => {
-                            return Err(mkerr(NotAFunction(Typed(
-                                rc(App(f.into_expr(), seen_args)),
-                                tf,
-                            ))));
-                        }
-                    };
+                        mkerr(NotAFunction(Typed(
+                            rc(App(f.into_expr(), seen_args)),
+                            tf,
+                        )))
+                    );
                     let tx = mktype(ctx, tx.clone())?;
-                    ensure_equal(&tx, &a.get_type(), mkerr, || {
-                        TypeMismatch(
-                            Typed(
-                                rc(App(f.as_expr().clone(), seen_args.clone())),
-                                tf.clone(),
-                            ),
-                            tx.clone().into_normalized().unwrap(),
-                            a.clone(),
-                        )
-                    })?;
+                    ensure_equal!(
+                        tx,
+                        a.get_type(),
+                        mkerr(TypeMismatch(
+                            Typed(rc(App(f.into_expr(), seen_args)), tf),
+                            tx.into_normalized()?,
+                            a,
+                        ))
+                    );
                     tf = mktype(
                         ctx,
                         subst_shift(&V(x.clone(), 0), &a.as_expr(), &tb),
@@ -452,90 +446,93 @@ pub fn type_with(
             }
             Annot(x, t) => {
                 let t = t.normalize().into_type();
-                ensure_equal(&t, &x.get_type(), mkerr, || {
-                    AnnotMismatch(
-                        x.clone(),
-                        t.clone().into_normalized().unwrap(),
-                    )
-                })?;
+                ensure_equal!(
+                    t,
+                    x.get_type(),
+                    mkerr(AnnotMismatch(x, t.into_normalized()?))
+                );
                 Ok(RetType(x.get_type_move()))
             }
             BoolIf(x, y, z) => {
-                ensure_equal(
-                    &x.get_type(),
-                    &mktype(ctx, rc(Builtin(Bool)))?,
-                    mkerr,
-                    || InvalidPredicate(x.clone()),
-                )?;
-                ensure_is_type(
-                    &y.get_type().get_type(),
-                    IfBranchMustBeTerm(true, y.clone()),
-                )?;
+                ensure_equal!(
+                    x.get_type(),
+                    mktype(ctx, rc(Builtin(Bool)))?,
+                    mkerr(InvalidPredicate(x)),
+                );
+                ensure_is_type!(
+                    y.get_type().get_type(),
+                    mkerr(IfBranchMustBeTerm(true, y)),
+                );
 
-                ensure_is_type(
-                    &z.get_type().get_type(),
-                    IfBranchMustBeTerm(false, z.clone()),
-                )?;
+                ensure_is_type!(
+                    z.get_type().get_type(),
+                    mkerr(IfBranchMustBeTerm(false, z)),
+                );
 
-                ensure_equal(&y.get_type(), &z.get_type(), mkerr, || {
-                    IfBranchMismatch(y.clone(), z.clone())
-                })?;
+                ensure_equal!(
+                    y.get_type(),
+                    z.get_type(),
+                    mkerr(IfBranchMismatch(y, z))
+                );
 
                 Ok(RetType(y.get_type_move()))
             }
             EmptyListLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type(
-                    &t.get_type(),
-                    InvalidListType(t.clone().into_normalized()?),
-                )?;
+                ensure_is_type!(
+                    t.get_type(),
+                    mkerr(InvalidListType(t.into_normalized()?)),
+                );
                 let t = t.into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
                 let (_, x) = iter.next().unwrap();
-                ensure_is_type(
-                    &x.get_type().get_type(),
-                    InvalidListType(x.get_type().clone().into_normalized()?),
-                )?;
+                ensure_is_type!(
+                    x.get_type().get_type(),
+                    mkerr(InvalidListType(
+                        x.get_type_move().into_normalized()?
+                    )),
+                );
                 for (i, y) in iter {
-                    ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
-                        InvalidListElement(
+                    ensure_equal!(
+                        x.get_type(),
+                        y.get_type(),
+                        mkerr(InvalidListElement(
                             i,
-                            x.get_type().clone().into_normalized().unwrap(),
-                            y.clone(),
-                        )
-                    })?;
+                            x.get_type_move().into_normalized()?,
+                            y
+                        ))
+                    );
                 }
                 let t = x.get_type_move().into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(List t)))
             }
             EmptyOptionalLit(t) => {
                 let t = t.normalize().into_type();
-                ensure_is_type(
-                    &t.get_type(),
-                    InvalidOptionalType(t.clone().into_normalized()?),
-                )?;
+                ensure_is_type!(
+                    t.get_type(),
+                    mkerr(InvalidOptionalType(t.into_normalized()?)),
+                );
                 let t = t.into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             NEOptionalLit(x) => {
-                ensure_is_type(
-                    &x.get_type().get_type(),
-                    InvalidOptionalType(
-                        x.get_type().clone().into_normalized()?,
-                    ),
-                )?;
-                let t = x.get_type_move().into_normalized()?.into_expr();
+                let tx = x.get_type_move();
+                ensure_is_type!(
+                    tx.get_type(),
+                    mkerr(InvalidOptionalType(tx.into_normalized()?,)),
+                );
+                let t = tx.into_normalized()?.into_expr();
                 Ok(RetExpr(dhall::expr!(Optional t)))
             }
             RecordType(kts) => {
                 for (k, t) in kts {
-                    ensure_is_type(
-                        &t.get_type(),
-                        InvalidFieldType(k.clone(), t.clone()),
-                    )?;
+                    ensure_is_type!(
+                        t.get_type(),
+                        mkerr(InvalidFieldType(k, t)),
+                    );
                 }
                 Ok(RetExpr(dhall::expr!(Type)))
             }
@@ -543,25 +540,25 @@ pub fn type_with(
                 let kts = kvs
                     .into_iter()
                     .map(|(k, v)| {
-                        ensure_is_type(
-                            &v.get_type().get_type(),
-                            InvalidField(k.clone(), v.clone()),
-                        )?;
+                        ensure_is_type!(
+                            v.get_type().get_type(),
+                            mkerr(InvalidField(k, v)),
+                        );
                         Ok((
-                            k.clone(),
+                            k,
                             v.get_type_move().into_normalized()?.into_expr(),
                         ))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RetExpr(RecordType(kts)))
             }
-            Field(r, x) => match r.get_type().unroll_ref()? {
+            Field(r, x) => ensure_matches!(r.get_type(),
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => Ok(RetExpr(e.unroll())),
-                    None => Err(mkerr(MissingField(x.clone(), r.clone()))),
+                    None => Err(mkerr(MissingField(x, r))),
                 },
-                _ => Err(mkerr(NotARecord(x.clone(), r.clone()))),
-            },
+                mkerr(NotARecord(x, r))
+            ),
             Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
             BoolLit(_) => Ok(RetExpr(dhall::expr!(Bool))),
             NaturalLit(_) => Ok(RetExpr(dhall::expr!(Natural))),
@@ -584,13 +581,9 @@ pub fn type_with(
                     },
                 )?;
 
-                ensure_equal(&l.get_type(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, l.clone())
-                })?;
+                ensure_equal!(l.get_type(), t, mkerr(BinOpTypeMismatch(o, l)));
 
-                ensure_equal(&r.get_type(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, r.clone())
-                })?;
+                ensure_equal!(r.get_type(), t, mkerr(BinOpTypeMismatch(o, r)));
 
                 Ok(RetType(t))
             }
-- 
cgit v1.2.3


From 4bebcd96b6e76b9b8ae7877af91d2ae571e617a9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 16:45:30 +0200
Subject: Restrict public API

Closes #20
---
 dhall/src/typecheck.rs | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index a0782f8..babfad0 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -11,8 +11,11 @@ use self::TypeMessage::*;
 
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
-        let typ = crate::typecheck::type_of_(self.0.clone())?;
-        Ok(typ)
+        type_of_(self.0.clone())
+    }
+    /// Pretends this expression has been typechecked. Use with care.
+    pub fn skip_typecheck(self) -> Typed {
+        Typed(self.0, UNTYPE)
     }
 }
 impl Typed {
@@ -63,7 +66,7 @@ impl Normalized {
 }
 impl Type {
     #[inline(always)]
-    fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
+    pub fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
         use TypeInternal::*;
         match &self.0 {
             Expr(e) => Ok(e),
-- 
cgit v1.2.3