Merge pull request #102 from Nadrieril/inline-headers

Implement inline headers parsing 

8 files changed, 101 insertions, 98 deletions

diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index c18014e..7c5c537 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
 use std::cell::{Ref, RefCell};
 use std::rc::Rc;
 
-use dhall_syntax::{Const, ExprF, X};
+use dhall_syntax::{Const, ExprF};
 
 use crate::core::context::{NormalizationContext, TypecheckContext};
 use crate::core::value::Value;
@@ -12,7 +12,7 @@ use crate::phase::normalize::{
     apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
 };
 use crate::phase::typecheck::type_of_const;
-use crate::phase::{NormalizedSubExpr, Type, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
 
 #[derive(Debug, Clone, Copy)]
 enum Marker {
@@ -30,7 +30,7 @@ enum ThunkInternal {
     /// Partially normalized value whose subexpressions have been thunked (this is returned from
     /// typechecking). Note that this is different from `Value::PartialExpr` because there is no
     /// requirement of WHNF here.
-    PartialExpr(ExprF<Thunk, X>),
+    PartialExpr(ExprF<Thunk, Normalized>),
     /// Partially normalized value.
     /// Invariant: if the marker is `NF`, the value must be fully normalized
     Value(Marker, Value),
@@ -123,7 +123,7 @@ impl Thunk {
         ThunkInternal::Value(WHNF, v).into_thunk()
     }
 
-    pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk {
+    pub fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
         ThunkInternal::PartialExpr(e).into_thunk()
     }
 
@@ -309,7 +309,6 @@ impl Shift for ThunkInternal {
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
                     |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
-                    |x| Ok(X::clone(x)),
                 )?,
             ),
             ThunkInternal::Value(m, v) => {
@@ -356,7 +355,6 @@ impl Subst<Typed> for ThunkInternal {
                             &val.under_binder(x),
                         )
                     },
-                    X::clone,
                 ),
             ),
             ThunkInternal::Value(_, v) => {
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 8486d6e..20a6021 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,7 +2,7 @@ use std::collections::HashMap;
 
 use dhall_syntax::{
     rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural, X,
+    NaiveDouble, Natural,
 };
 
 use crate::core::thunk::{Thunk, TypedThunk};
@@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::normalize::{
     apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
 };
-use crate::phase::Typed;
+use crate::phase::{Normalized, Typed};
 
 /// A semantic value. The invariants ensure this value represents a Weak-Head
 /// Normal Form (WHNF). This means that this first constructor is the first constructor of the
@@ -59,7 +59,7 @@ pub enum Value {
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
     Equivalence(TypedThunk, TypedThunk),
     // Invariant: this must not contain a value captured by one of the variants above.
-    PartialExpr(ExprF<Thunk, X>),
+    PartialExpr(ExprF<Thunk, Normalized>),
 }
 
 impl Value {
@@ -243,7 +243,7 @@ impl Value {
                 y.normalize_to_expr_maybe_alpha(alpha),
             )),
             Value::PartialExpr(e) => {
-                rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
+                rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
             }
         }
     }
@@ -333,8 +333,8 @@ impl Value {
                 y.normalize_mut();
             }
             Value::PartialExpr(e) => {
-                // TODO: need map_mut_simple
-                e.map_ref_simple(|v| {
+                // TODO: need map_mut
+                e.map_ref(|v| {
                     v.normalize_nf();
                 });
             }
@@ -475,7 +475,6 @@ impl Shift for Value {
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
                     |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
-                    |x| Ok(X::clone(x)),
                 )?,
             ),
         })
@@ -500,7 +499,6 @@ impl Subst<Typed> for Value {
                             &val.under_binder(x),
                         )
                     },
-                    X::clone,
                 ))
             }
             // Retry normalizing since substituting may allow progress
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 3626d96..8f6ff51 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -4,7 +4,7 @@ use dhall_syntax::{BinOp, Import, Label, ParseError, V};
 
 use crate::core::context::TypecheckContext;
 use crate::phase::resolve::ImportStack;
-use crate::phase::{Normalized, Type, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
 
 pub type Result<T> = std::result::Result<T, Error>;
 
@@ -21,9 +21,9 @@ pub enum Error {
 
 #[derive(Debug)]
 pub enum ImportError {
-    Recursive(Import, Box<Error>),
-    UnexpectedImport(Import),
-    ImportCycle(ImportStack, Import),
+    Recursive(Import<NormalizedSubExpr>, Box<Error>),
+    UnexpectedImport(Import<NormalizedSubExpr>),
+    ImportCycle(ImportStack, Import<NormalizedSubExpr>),
 }
 
 #[derive(Debug)]
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 3292617..36dd471 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -4,13 +4,12 @@ use std::iter::FromIterator;
 
 use dhall_syntax::map::DupTreeMap;
 use dhall_syntax::{
-    rc, ExprF, FilePrefix, Hash, Import, ImportHashed, ImportLocation,
-    ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, SubExpr,
-    URL, V,
+    rc, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode, Integer,
+    InterpolatedText, Label, Natural, Scheme, SubExpr, URL, V,
 };
 
 use crate::error::{DecodeError, EncodeError};
-use crate::phase::{DecodedSubExpr, ParsedSubExpr};
+use crate::phase::DecodedSubExpr;
 
 pub fn decode(data: &[u8]) -> Result<DecodedSubExpr, DecodeError> {
     match serde_cbor::de::from_slice(data) {
@@ -19,8 +18,7 @@ pub fn decode(data: &[u8]) -> Result<DecodedSubExpr, DecodeError> {
     }
 }
 
-//TODO: encode normalized expression too
-pub fn encode(expr: &ParsedSubExpr) -> Result<Vec<u8>, EncodeError> {
+pub fn encode<E>(expr: &SubExpr<E>) -> Result<Vec<u8>, EncodeError> {
     serde_cbor::ser::to_vec(&Serialize::Expr(expr))
         .map_err(|e| EncodeError::CBORError(e))
 }
@@ -261,20 +259,12 @@ fn cbor_value_to_dhall(
                         };
                         let headers = match rest.next() {
                             Some(Null) => None,
-                            // TODO
-                            // Some(x) => {
-                            //     match cbor_value_to_dhall(&x)?.as_ref() {
-                            //         Embed(import) => Some(Box::new(
-                            //             import.location_hashed.clone(),
-                            //         )),
-                            //         _ => Err(DecodeError::WrongFormatError(
-                            //             "import/remote/headers".to_owned(),
-                            //         ))?,
-                            //     }
-                            // }
+                            Some(x) => {
+                                let x = cbor_value_to_dhall(&x)?;
+                                Some(x)
+                            }
                             _ => Err(DecodeError::WrongFormatError(
-                                "import/remote/headers is unimplemented"
-                                    .to_owned(),
+                                "import/remote/headers".to_owned(),
                             ))?,
                         };
                         let authority = match rest.next() {
@@ -340,9 +330,10 @@ fn cbor_value_to_dhall(
                         "import/type".to_owned(),
                     ))?,
                 };
-                Embed(Import {
+                Import(dhall_syntax::Import {
                     mode,
-                    location_hashed: ImportHashed { hash, location },
+                    hash,
+                    location,
                 })
             }
             [U64(25), bindings..] => {
@@ -424,11 +415,11 @@ where
         .collect::<Result<_, _>>()
 }
 
-enum Serialize<'a> {
-    Expr(&'a ParsedSubExpr),
+enum Serialize<'a, E> {
+    Expr(&'a SubExpr<E>),
     CBOR(cbor::Value),
-    RecordMap(&'a DupTreeMap<Label, ParsedSubExpr>),
-    UnionMap(&'a DupTreeMap<Label, Option<ParsedSubExpr>>),
+    RecordMap(&'a DupTreeMap<Label, SubExpr<E>>),
+    UnionMap(&'a DupTreeMap<Label, Option<SubExpr<E>>>),
 }
 
 macro_rules! count {
@@ -448,7 +439,7 @@ macro_rules! ser_seq {
     }};
 }
 
-fn serialize_subexpr<S>(ser: S, e: &ParsedSubExpr) -> Result<S::Ok, S::Error>
+fn serialize_subexpr<S, E>(ser: S, e: &SubExpr<E>) -> Result<S::Ok, S::Error>
 where
     S: serde::ser::Serializer,
 {
@@ -458,21 +449,14 @@ where
     use std::iter::once;
 
     use self::Serialize::{RecordMap, UnionMap};
-    fn expr(x: &ParsedSubExpr) -> self::Serialize<'_> {
+    fn expr<E>(x: &SubExpr<E>) -> self::Serialize<'_, E> {
         self::Serialize::Expr(x)
     }
-    fn cbor<'a>(v: cbor::Value) -> self::Serialize<'a> {
-        self::Serialize::CBOR(v)
-    }
-    fn tag<'a>(x: u64) -> self::Serialize<'a> {
-        cbor(U64(x))
-    }
-    fn null<'a>() -> self::Serialize<'a> {
-        cbor(cbor::Value::Null)
-    }
-    fn label<'a>(l: &Label) -> self::Serialize<'a> {
-        cbor(cbor::Value::String(l.into()))
-    }
+    let cbor =
+        |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) };
+    let tag = |x: u64| cbor(U64(x));
+    let null = || cbor(cbor::Value::Null);
+    let label = |l: &Label| cbor(cbor::Value::String(l.into()));
 
     match e.as_ref() {
         Const(c) => ser.serialize_str(&c.to_string()),
@@ -573,18 +557,24 @@ where
                 .chain(once(expr(x)))
                 .chain(ls.iter().map(label)),
         ),
-        Embed(import) => serialize_import(ser, import),
+        Import(import) => serialize_import(ser, import),
+        Embed(_) => unimplemented!(
+            "An expression with resolved imports cannot be binary-encoded"
+        ),
     }
 }
 
-fn serialize_import<S>(ser: S, import: &Import) -> Result<S::Ok, S::Error>
+fn serialize_import<S, E>(
+    ser: S,
+    import: &Import<SubExpr<E>>,
+) -> Result<S::Ok, S::Error>
 where
     S: serde::ser::Serializer,
 {
     use cbor::Value::{Bytes, Null, U64};
     use serde::ser::SerializeSeq;
 
-    let count = 4 + match &import.location_hashed.location {
+    let count = 4 + match &import.location {
         ImportLocation::Remote(url) => 3 + url.path.len(),
         ImportLocation::Local(_, path) => path.len(),
         ImportLocation::Env(_) => 1,
@@ -594,7 +584,7 @@ where
 
     ser_seq.serialize_element(&U64(24))?;
 
-    let hash = match &import.location_hashed.hash {
+    let hash = match &import.hash {
         None => Null,
         Some(Hash::SHA256(h)) => {
             let mut bytes = vec![18, 32];
@@ -611,7 +601,7 @@ where
     };
     ser_seq.serialize_element(&U64(mode))?;
 
-    let scheme = match &import.location_hashed.location {
+    let scheme = match &import.location {
         ImportLocation::Remote(url) => match url.scheme {
             Scheme::HTTP => 0,
             Scheme::HTTPS => 1,
@@ -627,16 +617,13 @@ where
     };
     ser_seq.serialize_element(&U64(scheme))?;
 
-    match &import.location_hashed.location {
+    match &import.location {
         ImportLocation::Remote(url) => {
             match &url.headers {
                 None => ser_seq.serialize_element(&Null)?,
-                Some(location_hashed) => ser_seq.serialize_element(
-                    &self::Serialize::Expr(&rc(ExprF::Embed(Import {
-                        mode: ImportMode::Code,
-                        location_hashed: location_hashed.as_ref().clone(),
-                    }))),
-                )?,
+                Some(e) => {
+                    ser_seq.serialize_element(&self::Serialize::Expr(e))?
+                }
             };
             ser_seq.serialize_element(&url.authority)?;
             for p in &url.path {
@@ -661,7 +648,7 @@ where
     ser_seq.end()
 }
 
-impl<'a> serde::ser::Serialize for Serialize<'a> {
+impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
     fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error>
     where
         S: serde::ser::Serializer,
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 8c93889..b73597c 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
 use std::fmt::Display;
 use std::path::Path;
 
-use dhall_syntax::{Const, Import, SubExpr, X};
+use dhall_syntax::{Const, SubExpr, Void};
 
 use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
@@ -17,15 +17,17 @@ pub(crate) mod parse;
 pub(crate) mod resolve;
 pub(crate) mod typecheck;
 
-pub type ParsedSubExpr = SubExpr<Import>;
-pub type DecodedSubExpr = SubExpr<Import>;
+pub type ParsedSubExpr = SubExpr<Void>;
+pub type DecodedSubExpr = SubExpr<Void>;
 pub type ResolvedSubExpr = SubExpr<Normalized>;
-pub type NormalizedSubExpr = SubExpr<X>;
+pub type NormalizedSubExpr = SubExpr<Normalized>;
 
 #[derive(Debug, Clone)]
 pub struct Parsed(ParsedSubExpr, ImportRoot);
 
 /// An expression where all imports have been resolved
+///
+/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
 #[derive(Debug, Clone)]
 pub struct Resolved(ResolvedSubExpr);
 
@@ -155,6 +157,10 @@ impl Typed {
 }
 
 impl Normalized {
+    pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
+        crate::phase::binary::encode(&self.to_expr())
+    }
+
     #[allow(dead_code)]
     pub fn to_expr(&self) -> NormalizedSubExpr {
         self.0.to_expr()
@@ -218,6 +224,18 @@ derive_traits_for_wrapper_struct!(Parsed);
 derive_traits_for_wrapper_struct!(Resolved);
 derive_traits_for_wrapper_struct!(Normalized);
 
+impl std::hash::Hash for Normalized {
+    fn hash<H>(&self, state: &mut H)
+    where
+        H: std::hash::Hasher,
+    {
+        match self.encode() {
+            Ok(vec) => vec.hash(state),
+            Err(_) => {}
+        }
+    }
+}
+
 impl Eq for Typed {}
 impl PartialEq for Typed {
     fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 644f98c..adbcb02 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -2,14 +2,14 @@ use std::collections::HashMap;
 
 use dhall_syntax::{
     BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents,
-    NaiveDouble, X,
+    NaiveDouble,
 };
 
 use crate::core::context::NormalizationContext;
 use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
 use crate::core::var::Subst;
-use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
 
 pub type InputSubExpr = ResolvedSubExpr;
 pub type OutputSubExpr = NormalizedSubExpr;
@@ -86,7 +86,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                     // Empty string literal.
                     [] => {
                         // Printing InterpolatedText takes care of all the escaping
-                        let txt: InterpolatedText<X> =
+                        let txt: InterpolatedText<Normalized> =
                             std::iter::empty().collect();
                         let s = txt.to_string();
                         Ok((
@@ -98,10 +98,11 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                     // interpolations, there is a single Text item) in the literal.
                     [InterpolatedTextContents::Text(s)] => {
                         // Printing InterpolatedText takes care of all the escaping
-                        let txt: InterpolatedText<X> = std::iter::once(
-                            InterpolatedTextContents::Text(s.clone()),
-                        )
-                        .collect();
+                        let txt: InterpolatedText<Normalized> =
+                            std::iter::once(InterpolatedTextContents::Text(
+                                s.clone(),
+                            ))
+                            .collect();
                         let s = txt.to_string();
                         Ok((
                             r,
@@ -376,11 +377,10 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
     }
 
     // Thunk subexpressions
-    let expr: ExprF<Thunk, X> =
+    let expr: ExprF<Thunk, Normalized> =
         expr.as_ref().map_ref_with_special_handling_of_binders(
             |e| Thunk::new(ctx.clone(), e.clone()),
             |x, e| Thunk::new(ctx.skip(x), e.clone()),
-            |_| unreachable!(),
         );
 
     normalize_one_layer(expr)
@@ -391,7 +391,7 @@ enum Ret<'a> {
     Value(Value),
     Thunk(Thunk),
     ThunkRef(&'a Thunk),
-    Expr(ExprF<Thunk, X>),
+    Expr(ExprF<Thunk, Normalized>),
 }
 
 /// Performs an intersection of two HashMaps.
@@ -636,7 +636,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
     })
 }
 
-pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
+pub fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
     use Value::{
         AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
         NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -644,6 +644,9 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
     };
 
     let ret = match expr {
+        ExprF::Import(_) => unreachable!(
+            "There should remain no imports in a resolved expression"
+        ),
         ExprF::Embed(_) => unreachable!(),
         ExprF::Var(_) => unreachable!(),
         ExprF::Annot(x, _) => Ret::Thunk(x),
diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs
index abcee7e..52353e4 100644
--- a/dhall/src/phase/resolve.rs
+++ b/dhall/src/phase/resolve.rs
@@ -1,10 +1,10 @@
 use std::collections::HashMap;
 use std::path::{Path, PathBuf};
 
-use dhall_syntax::Import;
-
 use crate::error::{Error, ImportError};
-use crate::phase::{Normalized, Parsed, Resolved};
+use crate::phase::{Normalized, NormalizedSubExpr, Parsed, Resolved};
+
+type Import = dhall_syntax::Import<NormalizedSubExpr>;
 
 /// A root from which to resolve relative imports.
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -28,7 +28,7 @@ fn resolve_import(
     let cwd = match root {
         LocalDir(cwd) => cwd,
     };
-    match &import.location_hashed.location {
+    match &import.location {
         Local(prefix, path) => {
             let path: PathBuf = path.iter().cloned().collect();
             let path = match prefix {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index ecf9793..89e2da8 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),
@@ -377,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,
@@ -398,7 +396,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::*;
@@ -409,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!()
         }
@@ -598,9 +599,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 +1015,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 {