From 77af0bbc171618f48531cc6b1d77e18089928885 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 13 Aug 2019 20:54:15 +0200
Subject: Stop tracking the absence of Embed values at the type level

---
 dhall/src/phase/typecheck.rs | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

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

diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index ecf9793..96ff246 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -2,7 +2,6 @@ use std::collections::HashMap;
 
 use dhall_syntax::{
     rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
-    X,
 };
 
 use crate::core::context::{NormalizationContext, TypecheckContext};
@@ -214,7 +213,7 @@ macro_rules! make_type {
     };
 }
 
-fn type_of_builtin(b: Builtin) -> Expr<X> {
+fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
     use dhall_syntax::Builtin::*;
     match b {
         Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -398,7 +397,7 @@ fn type_with(
 /// layer.
 fn type_last_layer(
     ctx: &TypecheckContext,
-    e: &ExprF<Typed, X>,
+    e: &ExprF<Typed, Normalized>,
 ) -> Result<Ret, TypeError> {
     use crate::error::TypeMessage::*;
     use dhall_syntax::BinOp::*;
@@ -598,9 +597,7 @@ fn type_last_layer(
             }
         }
         Const(c) => Ok(RetWhole(Typed::from_const(*c))),
-        Builtin(b) => {
-            Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?))
-        }
+        Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)),
         BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
         IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)),
@@ -1016,7 +1013,7 @@ pub fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
 
 pub fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
     let expr: SubExpr<_> = e.0;
-    let ty: SubExpr<_> = ty.to_expr().absurd();
+    let ty: SubExpr<_> = ty.to_expr();
     type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
 }
 pub fn skip_typecheck(e: Resolved) -> Typed {
-- 
cgit v1.2.3


From 51dbaa0b66089bca63aa9cf69a1e0ec59df053b9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 13 Aug 2019 21:10:59 +0200
Subject: Considerably simplify Embed handling

---
 dhall/src/phase/typecheck.rs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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

diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 96ff246..e8b2544 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -376,12 +376,11 @@ fn type_with(
                 e.as_ref().traverse_ref_with_special_handling_of_binders(
                     |e| type_with(ctx, e.clone()),
                     |_, _| unreachable!(),
-                    |_| unreachable!(),
                 )?;
             let ret = type_last_layer(ctx, &expr)?;
             match ret {
                 RetTypeOnly(typ) => {
-                    let expr = expr.map_ref_simple(|typed| typed.to_thunk());
+                    let expr = expr.map_ref(|typed| typed.to_thunk());
                     Typed::from_thunk_and_type(
                         Thunk::from_partial_expr(expr),
                         typ,
-- 
cgit v1.2.3


From 8d45d633dfa60e8d64c9e6e742de4e33496bf0fa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 13 Aug 2019 22:11:45 +0200
Subject: Store Imports in their own node instead of in Embed

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

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

diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index e8b2544..89e2da8 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -407,6 +407,9 @@ fn type_last_layer(
     let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg);
 
     match e {
+        Import(_) => unreachable!(
+            "There should remain no imports in a resolved expression"
+        ),
         Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
             unreachable!()
         }
-- 
cgit v1.2.3