diff options
author | Nadrieril | 2020-02-15 19:10:52 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-15 19:15:32 +0000 |
commit | 5057144ed99bc4e1a76a0840dd39fc1bd862665c (patch) | |
tree | 89b3a5b6bed6732668df9001d5267db503186038 /dhall/src/semantics/tck | |
parent | d65d639ff93691adbf0a208edb99736003bc64bd (diff) |
Desugar Completion during resolution
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 34 |
1 files changed, 6 insertions, 28 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a8a2d95..36f7173 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -75,12 +75,14 @@ fn type_one_layer( let span_err = |msg: &str| mk_span_err(span.clone(), msg); let ty = match &ekind { - ExprKind::Import(..) => unreachable!( - "There should remain no imports in a resolved expression" - ), + ExprKind::Import(..) | ExprKind::Completion(..) => { + unreachable!("This case should have been handled in resolution") + } ExprKind::Var(..) | ExprKind::Const(Const::Sort) - | ExprKind::Annot(..) => unreachable!(), // Handled in type_with + | ExprKind::Annot(..) => { + unreachable!("This case should have been handled in type_with") + } ExprKind::Lam(binder, annot, body) => { if annot.ty().as_const().is_none() { @@ -739,30 +741,6 @@ fn type_one_layer( selection_val } - ExprKind::Completion(ty, compl) => { - let ty_field_default = type_one_layer( - env, - ExprKind::Field(ty.clone(), "default".into()), - None, - span.clone(), - )?; - let ty_field_type = type_one_layer( - env, - ExprKind::Field(ty.clone(), "Type".into()), - None, - span.clone(), - )?; - return type_one_layer( - env, - ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - ty_field_default, - compl.clone(), - ), - Some(ty_field_type.eval(env)), - span.clone(), - ); - } }; if let Some(annot) = annot { |