summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/nze/value.rs6
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs49
-rw-r--r--dhall/src/semantics/tck/typecheck.rs73
-rw-r--r--dhall/tests/type-inference/failure/recordOfKind.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt7
7 files changed, 97 insertions, 59 deletions
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index f31fd6c..7084af6 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use crate::semantics::nze::lazy;
use crate::semantics::{
apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
- BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv,
+ BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -139,8 +139,8 @@ impl Value {
self.0.kind()
}
- pub(crate) fn to_type(&self) -> Type {
- self.clone().into()
+ pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+ Type::new(self.clone(), u.into())
}
/// Converts a value back to the corresponding AST expression.
pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 3c47a81..f6591ba 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -11,6 +11,7 @@ pub(crate) struct Universe(u8);
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) struct Type {
val: Value,
+ univ: Universe,
}
/// A hir expression plus its inferred type.
@@ -39,18 +40,28 @@ impl Universe {
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 new(val: Value, univ: Universe) -> Self {
+ Type { val, univ }
+ }
+ /// Creates a new Type and infers its universe by re-typechecking its value.
+ /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
+ /// PiClosure.
+ pub fn new_infer_universe(
+ env: &TyEnv,
+ val: Value,
+ ) -> Result<Self, TypeError> {
+ let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
+ let u = match c {
+ Some(c) => c.to_universe(),
+ None => unreachable!(
+ "internal type error: this is not a type: {:?}",
+ val
+ ),
+ };
+ Ok(Type::new(val, u))
}
pub fn from_const(c: Const) -> Self {
Self::new(Value::from_const(c), c.to_universe().next())
@@ -66,18 +77,8 @@ impl 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 ty(&self) -> Universe {
+ self.univ
}
pub fn to_value(&self) -> Value {
@@ -184,8 +185,8 @@ impl TyExpr {
}
}
-impl From<Value> for Type {
- fn from(x: Value) -> Type {
- Type { val: x }
+impl From<Const> for Universe {
+ fn from(x: Const) -> Universe {
+ Universe::from_const(x)
}
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1281045..45b3168 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -136,24 +136,30 @@ fn type_one_layer(
return span_err("InvalidListElement");
}
}
- if x.ty().ty(env)? != Some(Const::Type) {
+ if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidListType");
}
let t = x.ty().to_value();
- Value::from_builtin(Builtin::List).app(t).to_type()
+ Value::from_builtin(Builtin::List)
+ .app(t)
+ .to_type(Const::Type)
}
ExprKind::SomeLit(x) => {
- if x.ty().ty(env)? != Some(Const::Type) {
+ if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
let t = x.ty().to_value();
- Value::from_builtin(Builtin::Optional).app(t).to_type()
+ Value::from_builtin(Builtin::Optional)
+ .app(t)
+ .to_type(Const::Type)
}
ExprKind::RecordLit(kvs) => {
use std::collections::hash_map::Entry;
let mut kts = HashMap::new();
+ // An empty record type has type Type
+ let mut k = Const::Type;
for (x, v) in kvs {
// Check for duplicated entries
match kts.entry(x.clone()) {
@@ -164,13 +170,13 @@ fn type_one_layer(
};
// Check that the fields have a valid kind
- match v.ty().ty(env)? {
- Some(_) => {}
+ match v.ty().ty().as_const() {
+ Some(c) => k = max(k, c),
None => return span_err("InvalidFieldType"),
}
}
- Value::from_kind(ValueKind::RecordType(kts)).to_type()
+ Value::from_kind(ValueKind::RecordType(kts)).to_type(k)
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
@@ -226,29 +232,31 @@ fn type_one_layer(
ExprKind::Field(scrut, x) => {
match scrut.ty().kind() {
ValueKind::RecordType(kts) => match kts.get(&x) {
- Some(val) => val.clone().to_type(),
+ Some(val) => Type::new_infer_universe(env, val.clone())?,
None => return span_err("MissingRecordField"),
},
- // TODO: branch here only when scrut.ty() is a Const
- _ => {
- let scrut_nf = scrut.eval(env);
- match scrut_nf.kind() {
+ ValueKind::Const(_) => {
+ let scrut = scrut.eval_to_type(env)?;
+ match scrut.kind() {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
Value::from_kind(ValueKind::PiClosure {
binder: Binder::new(x.clone()),
annot: ty.clone(),
- closure: Closure::new_constant(scrut_nf),
+ closure: Closure::new_constant(
+ scrut.to_value(),
+ ),
})
- .to_type()
+ .to_type(scrut.ty())
}
- Some(None) => scrut_nf.to_type(),
+ Some(None) => scrut,
None => return span_err("MissingUnionField"),
},
_ => return span_err("NotARecord"),
}
- } // _ => span_err("NotARecord"),
+ }
+ _ => return span_err("NotARecord"),
}
}
ExprKind::Assert(t) => {
@@ -295,7 +303,7 @@ fn type_one_layer(
}
let arg_nf = arg.eval(env);
- closure.apply(arg_nf).to_type()
+ Type::new_infer_universe(env, closure.apply(arg_nf))?
}
_ => return mkerr(
ErrorBuilder::new(format!(
@@ -314,7 +322,7 @@ fn type_one_layer(
if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
- if y.ty().ty(env)? != Some(Const::Type) {
+ if y.ty().ty().as_const() != Some(Const::Type) {
return span_err("IfBranchMustBeTerm");
}
if y.ty() != z.ty() {
@@ -344,7 +352,8 @@ fn type_one_layer(
Ok(r_t.clone())
})?;
- Value::from_kind(ValueKind::RecordType(kts)).to_type()
+ let u = max(x.ty().ty(), y.ty().ty());
+ Value::from_kind(ValueKind::RecordType(kts)).to_type(u)
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
@@ -357,8 +366,8 @@ fn type_one_layer(
)),
span.clone(),
);
- let x_u = x.ty().ty_univ(env)?;
- let y_u = y.ty().ty_univ(env)?;
+ let x_u = x.ty().ty();
+ let y_u = y.ty().ty();
Type::new(hir.eval(env), max(x_u, y_u))
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
@@ -388,7 +397,7 @@ fn type_one_layer(
if l.ty() != r.ty() {
return span_err("EquivalenceTypeMismatch");
}
- if l.ty().ty(env)? != Some(Const::Type) {
+ if l.ty().ty().as_const() != Some(Const::Type) {
return span_err("EquivalenceArgumentsMustBeTerms");
}
@@ -480,8 +489,11 @@ fn type_one_layer(
);
}
+ // TODO: this actually doesn't check anything yet
match closure.remove_binder() {
- Ok(v) => v.to_type(),
+ Ok(v) => {
+ Type::new_infer_universe(env, v.clone())?
+ }
Err(()) => {
return span_err(
"MergeReturnTypeIsDependent",
@@ -525,7 +537,9 @@ fn type_one_layer(
}
},
// Union alternative without type
- Some(None) => handler_type.clone().to_type(),
+ Some(None) => {
+ Type::new_infer_universe(env, handler_type.clone())?
+ }
None => return span_err("MergeHandlerMissingVariant"),
};
match &inferred_type {
@@ -560,7 +574,7 @@ fn type_one_layer(
}
}
ExprKind::ToMap(record, annot) => {
- if record.ty().ty(env)? != Some(Const::Type) {
+ if record.ty().ty().as_const() != Some(Const::Type) {
return span_err("`toMap` only accepts records of type `Type`");
}
let record_t = record.ty();
@@ -623,7 +637,7 @@ fn type_one_layer(
kts.insert("mapValue".into(), entry_type);
let output_type: Type = Value::from_builtin(Builtin::List)
.app(Value::from_kind(ValueKind::RecordType(kts)))
- .to_type();
+ .to_type(Const::Type);
if let Some(annot) = annot {
let annot_val = annot.eval_to_type(env)?;
if output_type != annot_val {
@@ -656,7 +670,10 @@ fn type_one_layer(
};
}
- Value::from_kind(ValueKind::RecordType(new_kts)).to_type()
+ Type::new_infer_universe(
+ env,
+ Value::from_kind(ValueKind::RecordType(new_kts)),
+ )?
}
ExprKind::ProjectionByExpr(record, selection) => {
let record_type = record.ty();
@@ -721,7 +738,7 @@ pub(crate) fn type_with(
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)? {
+ let u_body = match body.ty().ty().as_const() {
Some(k) => k,
_ => return mk_span_err(hir.span(), "Invalid output type"),
};
diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt
index a5d2465..653fe0b 100644
--- a/dhall/tests/type-inference/failure/recordOfKind.txt
+++ b/dhall/tests/type-inference/failure/recordOfKind.txt
@@ -1 +1,6 @@
-Type error: error: Sort does not have a type
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+ |
+1 | { a = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
index a5d2465..146018f 100644
--- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: error: Sort does not have a type
+Type error: error: InvalidFieldType
+ --> <current file>:1:0
+ |
+1 | { x = Type, y = Kind }
+ | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
index a5d2465..521ae05 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -1 +1,6 @@
-Type error: error: Sort does not have a type
+Type error: error: InvalidFieldType
+ --> <current file>:1:15
+ |
+1 | { x = Bool } ⫽ { x = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |
diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
index a5d2465..3abf62c 100644
--- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
+++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -1 +1,6 @@
-Type error: error: Sort does not have a type
+Type error: error: InvalidFieldType
+ --> <current file>:1:14
+ |
+1 | { x = {=} } ⫽ { x = Kind }
+ | ^^^^^^^^^^^^ InvalidFieldType
+ |