summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-06 11:36:11 +0200
committerNadrieril2019-04-06 11:36:11 +0200
commite56b23ea05f7827c54187173eb86b31f7fe70422 (patch)
tree61ac6d43fabc9cd044c8ecd0f54cb0dec516e787 /dhall
parent3ce264fb88fb659f238601b70d6b7c5683a43aee (diff)
Normalize output of type inference
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/typecheck.rs8
1 files changed, 4 insertions, 4 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5184e72..a9b9d7d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -217,7 +217,7 @@ where
let ctx2 = ctx
.insert(x.clone(), tA.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
- let tB = type_with(&ctx2, b.clone())?;
+ let tB = normalized_type_with(&ctx2, b.clone())?;
let p = rc(Pi(x.clone(), tA.clone(), tB));
let _ = type_with(ctx, p.clone())?;
return Ok(p);
@@ -249,7 +249,7 @@ where
App(f, args) => {
// Recurse on args
let (a, tf) = match args.split_last() {
- None => return type_with(ctx, f.clone()),
+ None => return normalized_type_with(ctx, f.clone()),
Some((a, args)) => (
a,
normalized_type_with(
@@ -385,7 +385,7 @@ where
let kts = kvs
.iter()
.map(|(k, v)| {
- let t = type_with(ctx, v.clone())?;
+ let t = normalized_type_with(ctx, v.clone())?;
let s = normalized_type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
Ok((k.clone(), t))
@@ -458,7 +458,7 @@ pub fn type_of<S: ::std::fmt::Debug + Clone>(
e: SubExpr<S, X>,
) -> Result<SubExpr<S, X>, TypeError<S>> {
let ctx = Context::new();
- type_with(&ctx, e) //.map(|e| e.into_owned())
+ normalized_type_with(&ctx, e) //.map(|e| e.into_owned())
}
/// The specific type error