diff options
author | Nadrieril | 2019-04-06 11:36:11 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-06 11:36:11 +0200 |
commit | e56b23ea05f7827c54187173eb86b31f7fe70422 (patch) | |
tree | 61ac6d43fabc9cd044c8ecd0f54cb0dec516e787 /dhall | |
parent | 3ce264fb88fb659f238601b70d6b7c5683a43aee (diff) |
Normalize output of type inference
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/typecheck.rs | 8 |
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 |