summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-02-13 20:45:42 +0000
committerNadrieril2020-02-13 20:45:42 +0000
commite25b67906ce68e8726e8139c1d1855f3ab2518ce (patch)
tree706e8873e371f9bbedd8ab1315dcfa7ef34ccaa7 /dhall
parentf29a40fb55b898b3a3cc51f198e8522eaecf0777 (diff)
Rework annotation and Sort handling
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/hir.rs2
-rw-r--r--dhall/src/semantics/tck/typecheck.rs143
-rw-r--r--dhall/tests/type-inference/failure/SortInLet.txt7
-rw-r--r--dhall/tests/type-inference/failure/hurkensParadox.txt8
-rw-r--r--dhall/tests/type-inference/failure/recordOfKind.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldName.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/AnnotationRecordWrongFieldType.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeKindSort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeTypeSort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/LetWithWrongAnnotation.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/OptionalDeprecatedSyntaxPresent.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/Sort.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/TypeAnnotationWrong.txt2
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
|