summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/nze/normalize.rs2
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs117
-rw-r--r--dhall/src/semantics/tck/typecheck.rs263
-rw-r--r--dhall/src/syntax/ast/expr.rs7
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt4
-rw-r--r--tests_buffer1
7 files changed, 218 insertions, 180 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 0e09511..c2d2dc2 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -471,7 +471,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
closure: Closure::new(env, body.clone()),
}
}
- HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
+ HirKind::Expr(ExprKind::Let(_, _, val, body)) => {
let val = val.eval(env);
body.eval(env.insert_value(val, ())).kind().clone()
}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 4999899..3c47a81 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,12 @@
-use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
use crate::syntax::{Builtin, Const, Span};
use crate::{NormalizedExpr, ToExprOptions};
+/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub(crate) struct Universe(u8);
+
/// An expression representing a type
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) struct Type {
@@ -16,12 +20,64 @@ pub(crate) struct TyExpr {
ty: Type,
}
+impl Universe {
+ pub fn from_const(c: Const) -> Self {
+ Universe(match c {
+ Const::Type => 0,
+ Const::Kind => 1,
+ Const::Sort => 2,
+ })
+ }
+ pub fn as_const(self) -> Option<Const> {
+ match self.0 {
+ 0 => Some(Const::Type),
+ 1 => Some(Const::Kind),
+ 2 => Some(Const::Sort),
+ _ => None,
+ }
+ }
+ pub fn next(self) -> Self {
+ Universe(self.0 + 1)
+ }
+ pub fn previous(self) -> Option<Self> {
+ if self.0 == 0 {
+ None
+ } else {
+ Some(Universe(self.0 - 1))
+ }
+ }
+}
+
impl Type {
+ pub fn new(val: Value, _u: Universe) -> Self {
+ Type { val }
+ }
pub fn from_const(c: Const) -> Self {
- Value::from_const(c).into()
+ Self::new(Value::from_const(c), c.to_universe().next())
}
pub fn from_builtin(b: Builtin) -> Self {
- Value::from_builtin(b).into()
+ use Builtin::*;
+ match b {
+ Bool | Natural | Integer | Double | Text => {}
+ _ => unreachable!("this builtin is not a type: {}", b),
+ }
+
+ Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+ }
+
+ /// Get the type of this type
+ // TODO: avoid recomputing so much
+ pub fn ty(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
+ Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const())
+ }
+ /// Get the type of this type
+ // TODO: avoid recomputing so much
+ pub fn ty_univ(&self, env: &TyEnv) -> Result<Universe, TypeError> {
+ Ok(match self.ty(env)? {
+ Some(c) => c.to_universe(),
+ // TODO: hack, might explode
+ None => Const::Sort.to_universe().next(),
+ })
}
pub fn to_value(&self) -> Value {
@@ -49,9 +105,9 @@ impl Type {
}
impl TyExpr {
- pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
+ pub fn from_hir(hir: &Hir, ty: Type) -> Self {
TyExpr {
- hir: Hir::new(kind, span),
+ hir: hir.clone(),
ty,
}
}
@@ -62,16 +118,6 @@ impl TyExpr {
pub fn ty(&self) -> &Type {
&self.ty
}
- /// Get the kind (the type of the type) of this value
- // TODO: avoid recomputing so much
- pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
- Ok(self
- .ty()
- .to_hir(env.as_varenv())
- .typecheck(env)?
- .ty()
- .as_const())
- }
pub fn to_hir(&self) -> Hir {
self.as_hir().clone()
@@ -79,18 +125,51 @@ impl TyExpr {
pub fn as_hir(&self) -> &Hir {
&self.hir
}
- /// Converts a value back to the corresponding AST expression.
+ /// Converts a closed expression back to the corresponding AST expression.
pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
self.as_hir().to_expr(opts)
}
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ self.as_hir().to_expr_tyenv(env)
+ }
/// Eval the TyExpr. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
self.as_hir().eval(env.into())
}
+ pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+ if self.ty().as_const().is_none() {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Expected a type, found: `{}`",
+ self.to_expr_tyenv(env),
+ ))
+ .span_err(
+ self.span(),
+ format!(
+ "this has type: `{}`",
+ self.ty().to_expr_tyenv(env)
+ ),
+ )
+ .help(format!(
+ "An expression in type position must have type `Type`, \
+ `Kind` or `Sort`",
+ ))
+ .format(),
+ );
+ }
+ Ok(())
+ }
/// Evaluate to a Type.
- pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
- self.eval(env).into()
+ pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+ self.ensure_is_type(env)?;
+ Ok(Type::new(
+ self.eval(env),
+ self.ty()
+ .as_const()
+ .expect("case handled in ensure_is_type")
+ .to_universe(),
+ ))
}
/// Eval a closed TyExpr (i.e. without free variables). 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 dd996ae..1281045 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -15,8 +15,8 @@ use crate::syntax::{
fn check_rectymerge(
span: &Span,
env: &TyEnv,
- x: Type,
- y: Type,
+ x: Value,
+ y: Value,
) -> Result<(), TypeError> {
let kts_x = match x.kind() {
ValueKind::RecordType(kts) => kts,
@@ -39,7 +39,7 @@ fn check_rectymerge(
for (k, tx) in kts_x {
if let Some(ty) = kts_y.get(k) {
// TODO: store Type in RecordType ?
- check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?;
+ check_rectymerge(span, env, tx.clone(), ty.clone())?;
}
}
Ok(())
@@ -70,9 +70,8 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
fn type_one_layer(
env: &TyEnv,
ekind: ExprKind<TyExpr>,
- annot: Option<Type>,
span: Span,
-) -> Result<TyExpr, TypeError> {
+) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
let ty = match &ekind {
@@ -81,84 +80,19 @@ fn type_one_layer(
}
ExprKind::Var(..)
| ExprKind::Const(Const::Sort)
+ | ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..)
| ExprKind::Annot(..) => {
unreachable!("This case should have been handled in type_with")
}
- ExprKind::Lam(binder, annot, body) => {
- if annot.ty().as_const().is_none() {
- return mkerr(
- ErrorBuilder::new(format!(
- "Invalid input type: `{}`",
- annot.ty().to_expr_tyenv(env),
- ))
- .span_err(
- annot.span(),
- format!(
- "this has type: `{}`",
- annot.ty().to_expr_tyenv(env)
- ),
- )
- .help(format!(
- "The input type of a function must have type `Type`, \
- `Kind` or `Sort`",
- ))
- .format(),
- );
- }
- let body_env = env.insert_type(&binder, annot.eval_to_type(env));
- if body.get_kind(&body_env)?.is_none() {
- return span_err("Invalid output type");
- }
- Hir::new(
- HirKind::Expr(ExprKind::Pi(
- binder.clone(),
- annot.to_hir(),
- body.ty().to_hir(body_env.as_varenv()),
- )),
- span.clone(),
- )
- .eval_to_type(env)
- }
- ExprKind::Pi(_, annot, body) => {
- let ks = match annot.ty().as_const() {
- Some(k) => k,
- _ => {
- return mkerr(
- ErrorBuilder::new(format!(
- "Invalid input type: `{}`",
- annot.ty().to_expr_tyenv(env),
- ))
- .span_err(
- annot.span(),
- format!(
- "this has type: `{}`",
- annot.ty().to_expr_tyenv(env)
- ),
- )
- .help(format!(
- "The input type of a function must have type \
- `Type`, `Kind` or `Sort`",
- ))
- .format(),
- );
- }
- };
- let kt = match body.ty().as_const() {
- Some(k) => k,
- _ => return span_err("Invalid output type"),
- };
-
- Type::from_const(function_check(ks, kt))
- }
- ExprKind::Let(_, _, _, body) => body.ty().clone(),
-
ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
ExprKind::Builtin(b) => {
let t_hir = type_of_builtin(*b);
let t_tyexpr = typecheck(&t_hir)?;
- t_tyexpr.eval_to_type(env)
+ t_tyexpr.eval_to_type(env)?
}
ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
ExprKind::Lit(LitKind::Natural(_)) => {
@@ -183,7 +117,7 @@ fn type_one_layer(
text_type
}
ExprKind::EmptyListLit(t) => {
- let t = t.eval_to_type(env);
+ let t = t.eval_to_type(env)?;
match t.kind() {
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
@@ -202,7 +136,7 @@ fn type_one_layer(
return span_err("InvalidListElement");
}
}
- if x.get_kind(env)? != Some(Const::Type) {
+ if x.ty().ty(env)? != Some(Const::Type) {
return span_err("InvalidListType");
}
@@ -210,7 +144,7 @@ fn type_one_layer(
Value::from_builtin(Builtin::List).app(t).to_type()
}
ExprKind::SomeLit(x) => {
- if x.get_kind(env)? != Some(Const::Type) {
+ if x.ty().ty(env)? != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
@@ -230,7 +164,7 @@ fn type_one_layer(
};
// Check that the fields have a valid kind
- match v.get_kind(env)? {
+ match v.ty().ty(env)? {
Some(_) => {}
None => return span_err("InvalidFieldType"),
}
@@ -297,7 +231,7 @@ fn type_one_layer(
},
// TODO: branch here only when scrut.ty() is a Const
_ => {
- let scrut_nf = scrut.eval_to_type(env);
+ let scrut_nf = scrut.eval(env);
match scrut_nf.kind() {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
@@ -305,13 +239,11 @@ fn type_one_layer(
Value::from_kind(ValueKind::PiClosure {
binder: Binder::new(x.clone()),
annot: ty.clone(),
- closure: Closure::new_constant(
- scrut_nf.into_value(),
- ),
+ closure: Closure::new_constant(scrut_nf),
})
.to_type()
}
- Some(None) => scrut_nf,
+ Some(None) => scrut_nf.to_type(),
None => return span_err("MissingUnionField"),
},
_ => return span_err("NotARecord"),
@@ -320,7 +252,7 @@ fn type_one_layer(
}
}
ExprKind::Assert(t) => {
- let t = t.eval_to_type(env);
+ let t = t.eval_to_type(env)?;
match t.kind() {
ValueKind::Equivalence(x, y) if x == y => {}
ValueKind::Equivalence(..) => {
@@ -382,7 +314,7 @@ fn type_one_layer(
if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
- if y.get_kind(env)? != Some(Const::Type) {
+ if y.ty().ty(env)? != Some(Const::Type) {
return span_err("IfBranchMustBeTerm");
}
if y.ty() != z.ty() {
@@ -415,25 +347,22 @@ fn type_one_layer(
Value::from_kind(ValueKind::RecordType(kts)).to_type()
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
- check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
+ check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
- Hir::new(
+ let hir = Hir::new(
HirKind::Expr(ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
x.ty().to_hir(env.as_varenv()),
y.ty().to_hir(env.as_varenv()),
)),
span.clone(),
- )
- .eval_to_type(env)
+ );
+ let x_u = x.ty().ty_univ(env)?;
+ let y_u = y.ty().ty_univ(env)?;
+ Type::new(hir.eval(env), max(x_u, y_u))
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
- check_rectymerge(
- &span,
- env,
- x.eval_to_type(env),
- y.eval_to_type(env),
- )?;
+ check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
// A RecordType's type is always a const
let xk = x.ty().as_const().unwrap();
@@ -459,7 +388,7 @@ fn type_one_layer(
if l.ty() != r.ty() {
return span_err("EquivalenceTypeMismatch");
}
- if l.get_kind(env)? != Some(Const::Type) {
+ if l.ty().ty(env)? != Some(Const::Type) {
return span_err("EquivalenceArgumentsMustBeTerms");
}
@@ -614,7 +543,10 @@ fn type_one_layer(
}
}
- let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env));
+ let type_annot = type_annot
+ .as_ref()
+ .map(|t| t.eval_to_type(env))
+ .transpose()?;
match (inferred_type, type_annot) {
(Some(t1), Some(t2)) => {
if t1 != t2 {
@@ -628,7 +560,7 @@ fn type_one_layer(
}
}
ExprKind::ToMap(record, annot) => {
- if record.get_kind(env)? != Some(Const::Type) {
+ if record.ty().ty(env)? != Some(Const::Type) {
return span_err("`toMap` only accepts records of type `Type`");
}
let record_t = record.ty();
@@ -648,7 +580,7 @@ fn type_one_layer(
annotation",
);
};
- let annot_val = annot.eval_to_type(env);
+ let annot_val = annot.eval_to_type(env)?;
let err_msg = "The type of `toMap x` must be of the form \
`List { mapKey : Text, mapValue : T }`";
@@ -693,7 +625,7 @@ fn type_one_layer(
.app(Value::from_kind(ValueKind::RecordType(kts)))
.to_type();
if let Some(annot) = annot {
- let annot_val = annot.eval_to_type(env);
+ let annot_val = annot.eval_to_type(env)?;
if output_type != annot_val {
return span_err("Annotation mismatch");
}
@@ -733,7 +665,7 @@ fn type_one_layer(
_ => return span_err("ProjectionMustBeRecord"),
};
- let selection_val = selection.eval_to_type(env);
+ let selection_val = selection.eval_to_type(env)?;
let sel_kts = match selection_val.kind() {
ValueKind::RecordType(kts) => kts,
_ => return span_err("ProjectionByExprTakesRecordType"),
@@ -754,22 +686,7 @@ fn type_one_layer(
}
};
- if let Some(annot) = annot {
- if ty != annot {
- return span_err(&format!(
- "annot mismatch: {} != {}",
- ty.to_expr_tyenv(env),
- annot.to_expr_tyenv(env)
- ));
- }
- }
-
- // TODO: avoid retraversing
- Ok(TyExpr::new(
- HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
- ty,
- span,
- ))
+ Ok(ty)
}
/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
@@ -779,59 +696,93 @@ pub(crate) fn type_with(
hir: &Hir,
annot: Option<Type>,
) -> Result<TyExpr, TypeError> {
- match hir.kind() {
- HirKind::Var(var) => {
- Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span()))
- }
+ let tyexpr = match hir.kind() {
+ HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)),
HirKind::Expr(ExprKind::Var(_)) => {
unreachable!("Hir should contain no unresolved variables")
}
HirKind::Expr(ExprKind::Const(Const::Sort)) => {
- mk_span_err(hir.span(), "Sort does not have a type")
+ return 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)) => {
Type::from_const(Const::Sort)
}
- _ => type_with(env, t, None)?.eval_to_type(env),
+ _ => type_with(env, t, None)?.eval_to_type(env)?,
};
- type_with(env, x, Some(t))
+ type_with(env, x, Some(t))?
}
- HirKind::Expr(ekind) => {
- let ekind = match ekind {
- ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot, None)?;
- let annot_nf = annot.eval_to_type(env);
- let body_env = env.insert_type(binder, annot_nf);
- 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, None)?;
- let annot_val = annot.eval_to_type(env);
- let body_env = env.insert_type(binder, annot_val);
- let body = type_with(&body_env, body, None)?;
- ExprKind::Pi(binder.clone(), annot, body)
- }
- ExprKind::Let(binder, annot, val, body) => {
- let val_annot = if let Some(t) = annot {
- Some(type_with(env, t, None)?.eval_to_type(env))
- } else {
- None
- };
- let val = type_with(env, &val, val_annot)?;
- let val_nf = val.eval(env);
- let body_env =
- env.insert_value(&binder, val_nf, val.ty().clone());
- let body = type_with(&body_env, body, None)?;
- ExprKind::Let(binder.clone(), None, val, body)
- }
- _ => ekind.traverse_ref(|e| type_with(env, e, None))?,
+
+ HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+ let annot = type_with(env, annot, None)?;
+ let annot_nf = annot.eval_to_type(env)?;
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body, None)?;
+
+ let u_annot = annot.ty().as_const().unwrap();
+ let u_body = match body.ty().ty(&body_env)? {
+ Some(k) => k,
+ _ => return mk_span_err(hir.span(), "Invalid output type"),
};
- type_one_layer(env, ekind, annot, hir.span())
+ let u = function_check(u_annot, u_body).to_universe();
+ let ty_hir = Hir::new(
+ HirKind::Expr(ExprKind::Pi(
+ binder.clone(),
+ annot.to_hir(),
+ body.ty().to_hir(body_env.as_varenv()),
+ )),
+ hir.span(),
+ );
+ let ty = Type::new(ty_hir.eval(env), u);
+
+ TyExpr::from_hir(hir, ty)
+ }
+ HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ let annot = type_with(env, annot, None)?;
+ let annot_val = annot.eval_to_type(env)?;
+ let body_env = env.insert_type(binder, annot_val);
+ let body = type_with(&body_env, body, None)?;
+ body.ensure_is_type(env)?;
+
+ let ks = annot.ty().as_const().unwrap();
+ let kt = body.ty().as_const().unwrap();
+ let ty = Type::from_const(function_check(ks, kt));
+ TyExpr::from_hir(hir, ty)
+ }
+ HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
+ let val_annot = annot
+ .as_ref()
+ .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?))
+ .transpose()?;
+ let val = type_with(env, &val, val_annot)?;
+ let val_nf = val.eval(env);
+ let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
+ let body = type_with(&body_env, body, None)?;
+ let ty = body.ty().clone();
+ TyExpr::from_hir(hir, ty)
+ }
+ HirKind::Expr(ekind) => {
+ let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
+ let ty = type_one_layer(env, ekind, hir.span())?;
+ TyExpr::from_hir(hir, ty)
+ }
+ };
+
+ if let Some(annot) = annot {
+ if *tyexpr.ty() != annot {
+ return mk_span_err(
+ hir.span(),
+ &format!(
+ "annot mismatch: {} != {}",
+ tyexpr.ty().to_expr_tyenv(env),
+ annot.to_expr_tyenv(env)
+ ),
+ );
}
}
+
+ Ok(tyexpr)
}
/// Typecheck an expression and return the expression annotated with types if type-checking
@@ -842,6 +793,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
/// 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 ty = typecheck(&ty)?.eval_to_type(&TyEnv::new());
+ let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
type_with(&TyEnv::new(), hir, Some(ty))
}
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 18ec9fd..a479b53 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,3 +1,4 @@
+use crate::semantics::Universe;
use crate::syntax::map::{DupTreeMap, DupTreeSet};
use crate::syntax::visitor;
use crate::syntax::*;
@@ -18,6 +19,12 @@ pub enum Const {
Sort,
}
+impl Const {
+ pub(crate) fn to_universe(self) -> Universe {
+ Universe::from_const(self)
+ }
+}
+
/// Bound variable
///
/// The `Label` field is the variable's name (i.e. \"`x`\").
diff --git a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
index e84eb15..ca5bbcd 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `1`
--> <current file>:1:6
|
1 | λ(_ : 1) → _
| ^ this has type: `Natural`
|
- = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
index 4aa0f4f..168ebb9 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `2`
--> <current file>:1:0
|
1 | 2 → _
| ^ this has type: `Natural`
|
- = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/tests_buffer b/tests_buffer
index e8eb3d7..1c814ff 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -52,6 +52,7 @@ success/
(λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
failure/
\(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+ unit/FunctionTypeOutputTypeNotAType Bool -> 1
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 16:21:14 +0000