diff options
author | Nadrieril | 2019-12-24 21:46:29 +0000 |
---|---|---|
committer | Nadrieril | 2019-12-24 21:46:29 +0000 |
commit | f5a588defc0ad22ce2f0d3b32ef8f0e22e43e672 (patch) | |
tree | 405bcef717b1a7ab0ec8de898ca5264698c39362 /dhall/src/semantics/phase/typecheck.rs | |
parent | 611d4ced3a5ffca8b9765971001995a216dbbb54 (diff) |
Ensure inferred type is always in normal form
Diffstat (limited to 'dhall/src/semantics/phase/typecheck.rs')
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index e9836e8..3960146 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -315,6 +315,7 @@ fn type_with( Ok(match e.as_ref() { Lam(var, annot, body) => { let annot = type_with(ctx, annot.clone())?; + annot.normalize_nf(); let ctx2 = ctx.insert_type(var, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; @@ -401,7 +402,9 @@ fn type_last_layer( return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } - RetTypeOnly(tb.subst_shift(&x.into(), a)) + let ret = tb.subst_shift(&x.into(), a); + ret.normalize_nf(); + RetTypeOnly(ret) } Annot(x, t) => { if &x.get_type()? != t { |