diff options
Diffstat (limited to 'dhall')
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 + | |