diff options
Diffstat (limited to 'dhall')
16 files changed, 114 insertions, 87 deletions
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs index f91aa73..e4e2a5f 100644 --- a/dhall/src/semantics/hir.rs +++ b/dhall/src/semantics/hir.rs @@ -72,7 +72,7 @@ impl Hir { /// Typecheck the Hir. pub fn typecheck(&self, env: &TyEnv) -> Result<TyExpr, TypeError> { - type_with(env, self) + type_with(env, self, None) } /// Eval the Hir. It will actually get evaluated only as needed on demand. diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 794edcf..a4ab31f 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -24,13 +24,10 @@ pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> { Err(TypeError::new(TypeMessage::Custom(msg.to_string()))) } -pub fn mk_span_err<T, S: ToString>( - span: &Span, - msg: S, -) -> Result<T, TypeError> { +pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> { mkerr( ErrorBuilder::new(msg.to_string()) - .span_err(span.clone(), msg.to_string()) + .span_err(span, msg.to_string()) .format(), ) } @@ -40,22 +37,25 @@ pub fn mk_span_err<T, S: ToString>( fn type_one_layer( env: &TyEnv, ekind: ExprKind<TyExpr>, + annot: Option<Type>, span: Span, ) -> Result<TyExpr, TypeError> { - let span_err = |msg: &str| mk_span_err(&span, msg); + 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::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with + ExprKind::Var(..) + | ExprKind::Const(Const::Sort) + | ExprKind::Annot(..) => unreachable!(), // Handled in type_with ExprKind::Lam(binder, annot, body) => { let body_ty = body.get_type_tyexpr( &env.insert_type(&binder.clone(), annot.eval(env)), )?; let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); - type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env) + type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env) } ExprKind::Pi(_, annot, body) => { let ks = match annot.get_type()?.as_const() { @@ -253,18 +253,6 @@ fn type_one_layer( } // _ => span_err("NotARecord"), } } - ExprKind::Annot(x, t) => { - let t = t.eval(env); - let x_ty = x.get_type()?; - if x_ty != t { - return span_err(&format!( - "annot mismatch: {} != {}", - x_ty.to_expr_tyenv(env), - t.to_expr_tyenv(env) - )); - } - x_ty - } ExprKind::Assert(t) => { let t = t.eval(env); match &*t.kind() { @@ -365,7 +353,7 @@ fn type_one_layer( x.get_type_tyexpr(env)?, y.get_type_tyexpr(env)?, ); - type_one_layer(env, ekind, span.clone())?.eval(env) + type_one_layer(env, ekind, None, span.clone())?.eval(env) } ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { fn check_rectymerge( @@ -376,20 +364,25 @@ fn type_one_layer( ) -> Result<(), TypeError> { let kts_x = match x.kind() { ValueKind::RecordType(kts) => kts, - _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"), + _ => { + return mk_span_err( + span.clone(), + "RecordTypeMergeRequiresRecordType", + ) + } }; let kts_y = match y.kind() { ValueKind::RecordType(kts) => kts, - _ => return mk_span_err(span, "RecordTypeMergeRequiresRecordType"), + _ => { + return mk_span_err( + span.clone(), + "RecordTypeMergeRequiresRecordType", + ) + } }; for (k, tx) in kts_x { if let Some(ty) = kts_y.get(k) { - check_rectymerge( - span, - env, - tx.clone(), - ty.clone(), - )?; + check_rectymerge(span, env, tx.clone(), ty.clone())?; } } Ok(()) @@ -717,30 +710,38 @@ fn type_one_layer( 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(), )?; - let merge = type_one_layer( + return type_one_layer( env, ExprKind::BinOp( BinOp::RightBiasedRecordMerge, ty_field_default, compl.clone(), ), - span.clone(), - )?; - return type_one_layer( - env, - ExprKind::Annot(merge, ty_field_type), + Some(ty_field_type.eval(env)), span.clone(), ); } }; + if let Some(annot) = annot { + if ty != annot { + return span_err(&format!( + "annot mismatch: {} != {}", + ty.to_expr_tyenv(env), + annot.to_expr_tyenv(env) + )); + } + } + Ok(TyExpr::new( HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())), Some(ty), @@ -748,72 +749,78 @@ fn type_one_layer( )) } -/// `type_with` typechecks an expressio in the provided environment. -pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> { - let (tyekind, ty) = match hir.kind() { - HirKind::Var(var) => (HirKind::Var(*var), Some(env.lookup(var))), +/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation +/// to compare with. +pub(crate) fn type_with( + env: &TyEnv, + hir: &Hir, + annot: Option<Type>, +) -> Result<TyExpr, TypeError> { + match hir.kind() { + HirKind::Var(var) => Ok(TyExpr::new( + HirKind::Var(*var), + Some(env.lookup(var)), + hir.span(), + )), HirKind::Expr(ExprKind::Var(_)) => { unreachable!("Hir should contain no unresolved variables") } HirKind::Expr(ExprKind::Const(Const::Sort)) => { - (HirKind::Expr(ExprKind::Const(Const::Sort)), None) + mk_span_err(hir.span(), "Sort does not have a type") + } + HirKind::Expr(ExprKind::Annot(x, t)) => { + let t = match t.kind() { + HirKind::Expr(ExprKind::Const(Const::Sort)) => { + Value::from_const(Const::Sort) + } + _ => type_with(env, t, None)?.eval(env), + }; + type_with(env, x, Some(t)) } HirKind::Expr(ekind) => { let ekind = match ekind { ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot)?; + let annot = type_with(env, annot, None)?; let annot_nf = annot.eval(env); let body_env = env.insert_type(binder, annot_nf); - let body = type_with(&body_env, body)?; + let body = type_with(&body_env, body, None)?; ExprKind::Lam(binder.clone(), annot, body) } ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot)?; + let annot = type_with(env, annot, None)?; let annot_nf = annot.eval(env); let body_env = env.insert_type(binder, annot_nf); - let body = type_with(&body_env, body)?; + let body = type_with(&body_env, body, None)?; ExprKind::Pi(binder.clone(), annot, body) } ExprKind::Let(binder, annot, val, body) => { - let val = if let Some(t) = annot { - Hir::new( - HirKind::Expr(ExprKind::Annot( - val.clone(), - t.clone(), - )), - t.span(), - ) + let val_annot = if let Some(t) = annot { + Some(type_with(env, t, None)?.eval(env)) } else { - val.clone() + None }; - let val = type_with(env, &val)?; + let val = type_with(env, &val, val_annot)?; let val_ty = val.get_type()?; let val_nf = val.eval(env); let body_env = env.insert_value(&binder, val_nf, val_ty); - let body = type_with(&body_env, body)?; + let body = type_with(&body_env, body, None)?; ExprKind::Let(binder.clone(), None, val, body) } - _ => ekind.traverse_ref(|e| type_with(env, e))?, + _ => ekind.traverse_ref(|e| type_with(env, e, None))?, }; - return type_one_layer(env, ekind, hir.span()); + type_one_layer(env, ekind, annot, hir.span()) } - }; - - Ok(TyExpr::new(tyekind, ty, hir.span())) + } } /// Typecheck an expression and return the expression annotated with types if type-checking /// succeeded, or an error if type-checking failed. -pub(crate) fn typecheck(e: &Hir) -> Result<TyExpr, TypeError> { - let res = type_with(&TyEnv::new(), e)?; - // Ensure that the inferred type exists (i.e. this is not Sort) - res.get_type()?; - Ok(res) +pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> { + type_with(&TyEnv::new(), hir, None) } /// Like `typecheck`, but additionally checks that the expression's type matches the provided type. pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> { - let hir = - Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span()); - typecheck(&hir) + let ty = typecheck(&ty)?.eval(&TyEnv::new()); + type_with(&TyEnv::new(), hir, Some(ty)) } diff --git a/dhall/tests/type-inference/failure/SortInLet.txt b/dhall/tests/type-inference/failure/SortInLet.txt index 5b88ff7..19bd26d 100644 --- a/dhall/tests/type-inference/failure/SortInLet.txt +++ b/dhall/tests/type-inference/failure/SortInLet.txt @@ -1 +1,6 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type + --> <current file>:1:8 + | +1 | let x = Sort in 0 + | ^^^^ Sort does not have a type + | diff --git a/dhall/tests/type-inference/failure/hurkensParadox.txt b/dhall/tests/type-inference/failure/hurkensParadox.txt index 6b99615..5aacb80 100644 --- a/dhall/tests/type-inference/failure/hurkensParadox.txt +++ b/dhall/tests/type-inference/failure/hurkensParadox.txt @@ -1,15 +1,15 @@ Type error: error: wrong type of function argument - --> <current file>:6:23 + --> <current file>:6:15 | 1 | let bottom : Type = ∀(any : Type) → any 2 | 3 | in let not : Type → Type = λ(p : Type) → p → bottom 4 | ... + 9 | in let tau 10 | : pow (pow U) → U -11 | = λ(t : pow (pow U)) - | ^^^ this expects an argument of type: Kind - | ^ but this has type: Sort + | ^^^ this expects an argument of type: Kind + | ^ but this has type: Sort | = note: expected type `Kind` found type `Sort` diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt index 5b88ff7..a5d2465 100644 --- a/dhall/tests/type-inference/failure/recordOfKind.txt +++ b/dhall/tests/type-inference/failure/recordOfKind.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt index 01a1f32..a39a0fb 100644 --- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt +++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: { x : Natural } != { y : Natural } --> <current file>:1:0 | 1 | { x = 1 } : { y : Natural } - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural } + | ^^^^^^^^^ annot mismatch: { x : Natural } != { y : Natural } | diff --git a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt index 5c10467..9ecc2a4 100644 --- a/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt +++ b/dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: { x : Natural } != { x : Text } --> <current file>:1:0 | 1 | { x = 1 } : { x : Text } - | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text } + | ^^^^^^^^^ annot mismatch: { x : Natural } != { x : Text } | diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt index 5b88ff7..6f26607 100644 --- a/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt +++ b/dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt @@ -1 +1,6 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type + --> <current file>:1:7 + | +1 | Kind → Sort + | ^^^^ Sort does not have a type + | diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt index 5b88ff7..169014b 100644 --- a/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt +++ b/dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt @@ -1 +1,6 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type + --> <current file>:1:7 + | +1 | Type → Sort + | ^^^^ Sort does not have a type + | diff --git a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt index 2f75196..51279f2 100644 --- a/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt +++ b/dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt @@ -1,6 +1,6 @@ Type error: error: annot mismatch: Bool != Natural - --> <current file>:1:8 + --> <current file>:1:18 | 1 | let x : Natural = True in True - | ^^^^^^^ annot mismatch: Bool != Natural + | ^^^^ annot mismatch: Bool != Natural | diff --git a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt index 066e4a3..0cc4bba 100644 --- a/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt +++ b/dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: List Natural != Optional Natural --> <current file>:1:0 | 1 | [ 1 ] : Optional Natural - | ^^^^^^^^^^^^^^^^^^^^^^^^ annot mismatch: List Natural != Optional Natural + | ^^^^^ annot mismatch: List Natural != Optional Natural | diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt index 5b88ff7..a5d2465 100644 --- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt index 5b88ff7..a5d2465 100644 --- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt +++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt index 5b88ff7..a5d2465 100644 --- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt @@ -1 +1 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type diff --git a/dhall/tests/type-inference/failure/unit/Sort.txt b/dhall/tests/type-inference/failure/unit/Sort.txt index 5b88ff7..e402127 100644 --- a/dhall/tests/type-inference/failure/unit/Sort.txt +++ b/dhall/tests/type-inference/failure/unit/Sort.txt @@ -1 +1,6 @@ -Type error: Unhandled error: Sort +Type error: error: Sort does not have a type + --> <current file>:1:0 + | +1 | Sort + | ^^^^ Sort does not have a type + | diff --git a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt index e203d22..dffadb1 100644 --- a/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt +++ b/dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt @@ -2,5 +2,5 @@ Type error: error: annot mismatch: Natural != Bool --> <current file>:1:0 | 1 | 1 : Bool - | ^^^^^^^^ annot mismatch: Natural != Bool + | ^ annot mismatch: Natural != Bool | |