summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs851
1 files changed, 436 insertions, 415 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 8f3fcb2..28d08b9 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -66,206 +66,263 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
)
}
-/// When all sub-expressions have been typed, check the remaining toplevel
-/// layer.
-fn type_one_layer(
+fn type_of_binop(
env: &TyEnv,
- ekind: ExprKind<Tir<'_>>,
span: Span,
+ op: BinOp,
+ l: &Tir<'_>,
+ r: &Tir<'_>,
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+ use BinOp::*;
+ use NirKind::{ListType, RecordType};
- let ty = match &ekind {
- ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => {
- unreachable!("This case should have been handled in resolution")
- }
- ExprKind::Var(..)
- | ExprKind::Const(Const::Sort)
- | ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
- | ExprKind::Annot(..) => {
- unreachable!("This case should have been handled in type_with")
- }
+ Ok(match op {
+ RightBiasedRecordMerge => {
+ let x_type = l.ty();
+ let y_type = r.ty();
- 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);
- typecheck(&t_hir)?.eval_to_type(env)?
- }
- ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
- ExprKind::Num(NumKind::Natural(_)) => {
- Type::from_builtin(Builtin::Natural)
- }
- ExprKind::Num(NumKind::Integer(_)) => {
- Type::from_builtin(Builtin::Integer)
- }
- ExprKind::Num(NumKind::Double(_)) => {
- Type::from_builtin(Builtin::Double)
+ // Extract the LHS record type
+ let kts_x = match x_type.kind() {
+ RecordType(kts) => kts,
+ _ => return span_err("MustCombineRecord"),
+ };
+ // Extract the RHS record type
+ let kts_y = match y_type.kind() {
+ RecordType(kts) => kts,
+ _ => return span_err("MustCombineRecord"),
+ };
+
+ // Union the two records, prefering
+ // the values found in the RHS.
+ let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone());
+
+ let u = max(l.ty().ty(), r.ty().ty());
+ Nir::from_kind(RecordType(kts)).to_type(u)
}
- ExprKind::TextLit(interpolated) => {
- let text_type = Type::from_builtin(Builtin::Text);
- for contents in interpolated.iter() {
- use InterpolatedTextContents::Expr;
- if let Expr(x) = contents {
- if *x.ty() != text_type {
- return span_err("InvalidTextInterpolation");
- }
- }
- }
- text_type
+ RecursiveRecordMerge => {
+ check_rectymerge(&span, env, l.ty().to_nir(), r.ty().to_nir())?;
+
+ let hir = Hir::new(
+ HirKind::Expr(ExprKind::Op(OpKind::BinOp(
+ RecursiveRecordTypeMerge,
+ l.ty().to_hir(env.as_varenv()),
+ r.ty().to_hir(env.as_varenv()),
+ ))),
+ span.clone(),
+ );
+ let x_u = l.ty().ty();
+ let y_u = r.ty().ty();
+ Type::new(hir.eval(env), max(x_u, y_u))
}
- ExprKind::EmptyListLit(t) => {
- let t = t.eval_to_type(env)?;
- match t.kind() {
- NirKind::ListType(..) => {}
- _ => return span_err("InvalidListType"),
- };
- t
+ RecursiveRecordTypeMerge => {
+ check_rectymerge(&span, env, l.eval(env), r.eval(env))?;
+
+ // A RecordType's type is always a const
+ let xk = l.ty().as_const().unwrap();
+ let yk = r.ty().as_const().unwrap();
+ Type::from_const(max(xk, yk))
}
- ExprKind::NEListLit(xs) => {
- let mut iter = xs.iter();
- let x = iter.next().unwrap();
- for y in iter {
- if x.ty() != y.ty() {
- return span_err("InvalidListElement");
- }
+ ListAppend => {
+ match l.ty().kind() {
+ ListType(..) => {}
+ _ => return span_err("BinOpTypeMismatch"),
}
- if x.ty().ty().as_const() != Some(Const::Type) {
- return span_err("InvalidListType");
+
+ if l.ty() != r.ty() {
+ return span_err("BinOpTypeMismatch");
}
- let t = x.ty().to_nir();
- Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
+ l.ty().clone()
}
- ExprKind::SomeLit(x) => {
- if x.ty().ty().as_const() != Some(Const::Type) {
- return span_err("InvalidOptionalType");
+ Equivalence => {
+ if l.ty() != r.ty() {
+ return span_err("EquivalenceTypeMismatch");
+ }
+ if l.ty().ty().as_const() != Some(Const::Type) {
+ return span_err("EquivalenceArgumentsMustBeTerms");
}
- let t = x.ty().to_nir();
- Nir::from_builtin(Builtin::Optional)
- .app(t)
- .to_type(Const::Type)
+ Type::from_const(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()) {
- Entry::Occupied(_) => {
- return span_err("RecordTypeDuplicateField")
- }
- Entry::Vacant(e) => e.insert(v.ty().to_nir()),
- };
+ op => {
+ let t = Type::from_builtin(match op {
+ BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool,
+ NaturalPlus | NaturalTimes => Builtin::Natural,
+ TextAppend => Builtin::Text,
+ ListAppend
+ | RightBiasedRecordMerge
+ | RecursiveRecordMerge
+ | RecursiveRecordTypeMerge
+ | Equivalence => unreachable!(),
+ ImportAlt => unreachable!("ImportAlt leftover in tck"),
+ });
- // Check that the fields have a valid kind
- match v.ty().ty().as_const() {
- Some(c) => k = max(k, c),
- None => return span_err("InvalidFieldType"),
- }
+ if *l.ty() != t {
+ return span_err("BinOpTypeMismatch");
}
- Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
+ if *r.ty() != t {
+ return span_err("BinOpTypeMismatch");
+ }
+
+ t
}
- ExprKind::RecordType(kts) => {
- use std::collections::hash_map::Entry;
- let mut seen_fields = HashMap::new();
- // An empty record type has type Type
- let mut k = Const::Type;
+ })
+}
- for (x, t) in kts {
- // Check for duplicated entries
- match seen_fields.entry(x.clone()) {
- Entry::Occupied(_) => {
- return span_err("RecordTypeDuplicateField")
- }
- Entry::Vacant(e) => e.insert(()),
- };
+fn type_of_merge(
+ env: &TyEnv,
+ span: Span,
+ record: &Tir<'_>,
+ scrut: &Tir<'_>,
+ type_annot: Option<&Tir<'_>>,
+) -> Result<Type, TypeError> {
+ let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+ use NirKind::{OptionalType, PiClosure, RecordType, UnionType};
- // Check the type is a Const and compute final type
- match t.ty().as_const() {
- Some(c) => k = max(k, c),
- None => return span_err("InvalidFieldType"),
- }
- }
+ let record_type = scrut.ty();
+ let handlers = match record_type.kind() {
+ RecordType(kts) => kts,
+ _ => return span_err("Merge1ArgMustBeRecord"),
+ };
- Type::from_const(k)
+ let scrut_type = scrut.ty();
+ let variants = match scrut_type.kind() {
+ UnionType(kts) => Cow::Borrowed(kts),
+ OptionalType(ty) => {
+ let mut kts = HashMap::new();
+ kts.insert("None".into(), None);
+ kts.insert("Some".into(), Some(ty.clone()));
+ Cow::Owned(kts)
}
- ExprKind::UnionType(kts) => {
- use std::collections::hash_map::Entry;
- let mut seen_fields = HashMap::new();
- // Check that all types are the same const
- let mut k = None;
- for (x, t) in kts {
- if let Some(t) = t {
- match (k, t.ty().as_const()) {
- (None, Some(k2)) => k = Some(k2),
- (Some(k1), Some(k2)) if k1 == k2 => {}
- _ => return span_err("InvalidFieldType"),
- }
- }
- match seen_fields.entry(x) {
- Entry::Occupied(_) => {
- return span_err("UnionTypeDuplicateField")
- }
- Entry::Vacant(e) => e.insert(()),
- };
- }
+ _ => return span_err("Merge2ArgMustBeUnionOrOptional"),
+ };
- // An empty union type has type Type;
- // an union type with only unary variants also has type Type
- let k = k.unwrap_or(Const::Type);
+ let mut inferred_type = None;
+ for (x, handler_type) in handlers {
+ let handler_return_type: Type = match variants.get(x) {
+ // Union alternative with type
+ Some(Some(variant_type)) => match handler_type.kind() {
+ PiClosure { closure, annot, .. } => {
+ if variant_type != annot {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Wrong handler input type"
+ ))
+ .span_err(
+ span,
+ format!("in this merge expression",),
+ )
+ .span_err(
+ record.span(),
+ format!(
+ "the handler for `{}` expects a value of \
+ type: `{}`",
+ x,
+ annot.to_expr_tyenv(env)
+ ),
+ )
+ .span_err(
+ scrut.span(),
+ format!(
+ "but the corresponding variant has type: \
+ `{}`",
+ variant_type.to_expr_tyenv(env)
+ ),
+ )
+ .format(),
+ );
+ }
- Type::from_const(k)
- }
- ExprKind::Op(OpKind::Field(scrut, x)) => {
- match scrut.ty().kind() {
- NirKind::RecordType(kts) => match kts.get(&x) {
- Some(val) => Type::new_infer_universe(env, val.clone())?,
- None => return span_err("MissingRecordField"),
- },
- NirKind::Const(_) => {
- let scrut = scrut.eval_to_type(env)?;
- match scrut.kind() {
- NirKind::UnionType(kts) => match kts.get(x) {
- // Constructor has type T -> < x: T, ... >
- Some(Some(ty)) => {
- Nir::from_kind(NirKind::PiClosure {
- binder: Binder::new(x.clone()),
- annot: ty.clone(),
- closure: Closure::new_constant(
- scrut.to_nir(),
- ),
- })
- .to_type(scrut.ty())
- }
- Some(None) => scrut,
- None => return span_err("MissingUnionField"),
- },
- _ => return span_err("NotARecord"),
+ // TODO: this actually doesn't check anything yet
+ match closure.remove_binder() {
+ Ok(v) => Type::new_infer_universe(env, v.clone())?,
+ Err(()) => {
+ return span_err("MergeReturnTypeIsDependent")
+ }
}
}
- _ => return span_err("NotARecord"),
+ _ => {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "merge handler is not a function"
+ ))
+ .span_err(span, format!("in this merge expression"))
+ .span_err(
+ record.span(),
+ format!(
+ "the handler for `{}` has type: `{}`",
+ x,
+ handler_type.to_expr_tyenv(env)
+ ),
+ )
+ .span_help(
+ scrut.span(),
+ format!(
+ "the corresponding variant has type: `{}`",
+ variant_type.to_expr_tyenv(env)
+ ),
+ )
+ .help(format!(
+ "a handler for this variant must be a function \
+ that takes an input of type: `{}`",
+ variant_type.to_expr_tyenv(env)
+ ))
+ .format(),
+ )
+ }
+ },
+ // Union alternative without type
+ Some(None) => Type::new_infer_universe(env, handler_type.clone())?,
+ None => return span_err("MergeHandlerMissingVariant"),
+ };
+ match &inferred_type {
+ None => inferred_type = Some(handler_return_type),
+ Some(t) => {
+ if t != &handler_return_type {
+ return span_err("MergeHandlerTypeMismatch");
+ }
}
}
- ExprKind::Assert(t) => {
- let t = t.eval_to_type(env)?;
- match t.kind() {
- NirKind::Equivalence(x, y) if x == y => {}
- NirKind::Equivalence(..) => return span_err("AssertMismatch"),
- _ => return span_err("AssertMustTakeEquivalence"),
+ }
+ for x in variants.keys() {
+ if !handlers.contains_key(x) {
+ return span_err("MergeVariantMissingHandler");
+ }
+ }
+
+ let type_annot = type_annot
+ .as_ref()
+ .map(|t| t.eval_to_type(env))
+ .transpose()?;
+ Ok(match (inferred_type, type_annot) {
+ (Some(t1), Some(t2)) => {
+ if t1 != t2 {
+ return span_err("MergeAnnotMismatch");
}
- t
+ t1
}
- ExprKind::Op(OpKind::App(f, arg)) => {
+ (Some(t), None) => t,
+ (None, Some(t)) => t,
+ (None, None) => return span_err("MergeEmptyNeedsAnnotation"),
+ })
+}
+
+fn type_of_operation(
+ env: &TyEnv,
+ span: Span,
+ opkind: &OpKind<Tir<'_>>,
+) -> Result<Type, TypeError> {
+ let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+ use NirKind::{ListType, PiClosure, RecordType, UnionType};
+ use OpKind::*;
+
+ Ok(match opkind {
+ App(f, arg) => {
match f.ty().kind() {
// TODO: store Type in closure
- NirKind::PiClosure { annot, closure, .. } => {
+ PiClosure { annot, closure, .. } => {
if arg.ty().as_nir() != annot {
return mkerr(
ErrorBuilder::new(format!(
@@ -310,7 +367,8 @@ fn type_one_layer(
),
}
}
- ExprKind::Op(OpKind::BoolIf(x, y, z)) => {
+ BinOp(o, l, r) => type_of_binop(env, span, *o, l, r)?,
+ BoolIf(x, y, z) => {
if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
@@ -323,245 +381,16 @@ fn type_one_layer(
y.ty().clone()
}
- ExprKind::Op(OpKind::BinOp(BinOp::RightBiasedRecordMerge, x, y)) => {
- let x_type = x.ty();
- let y_type = y.ty();
-
- // Extract the LHS record type
- let kts_x = match x_type.kind() {
- NirKind::RecordType(kts) => kts,
- _ => return span_err("MustCombineRecord"),
- };
- // Extract the RHS record type
- let kts_y = match y_type.kind() {
- NirKind::RecordType(kts) => kts,
- _ => return span_err("MustCombineRecord"),
- };
-
- // Union the two records, prefering
- // the values found in the RHS.
- let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone());
-
- let u = max(x.ty().ty(), y.ty().ty());
- Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
+ Merge(record, scrut, type_annot) => {
+ type_of_merge(env, span, record, scrut, type_annot.as_ref())?
}
- ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => {
- check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
-
- let hir = Hir::new(
- HirKind::Expr(ExprKind::Op(OpKind::BinOp(
- BinOp::RecursiveRecordTypeMerge,
- x.ty().to_hir(env.as_varenv()),
- y.ty().to_hir(env.as_varenv()),
- ))),
- span.clone(),
- );
- let x_u = x.ty().ty();
- let y_u = y.ty().ty();
- Type::new(hir.eval(env), max(x_u, y_u))
- }
- ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y)) => {
- 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();
- let yk = y.ty().as_const().unwrap();
- Type::from_const(max(xk, yk))
- }
- ExprKind::Op(OpKind::BinOp(BinOp::ListAppend, l, r)) => {
- match l.ty().kind() {
- NirKind::ListType(..) => {}
- _ => return span_err("BinOpTypeMismatch"),
- }
-
- if l.ty() != r.ty() {
- return span_err("BinOpTypeMismatch");
- }
-
- l.ty().clone()
- }
- ExprKind::Op(OpKind::BinOp(BinOp::Equivalence, l, r)) => {
- if l.ty() != r.ty() {
- return span_err("EquivalenceTypeMismatch");
- }
- if l.ty().ty().as_const() != Some(Const::Type) {
- return span_err("EquivalenceArgumentsMustBeTerms");
- }
-
- Type::from_const(Const::Type)
- }
- ExprKind::Op(OpKind::BinOp(o, l, r)) => {
- let t = Type::from_builtin(match o {
- BinOp::BoolAnd
- | BinOp::BoolOr
- | BinOp::BoolEQ
- | BinOp::BoolNE => Builtin::Bool,
- BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural,
- BinOp::TextAppend => Builtin::Text,
- BinOp::ListAppend
- | BinOp::RightBiasedRecordMerge
- | BinOp::RecursiveRecordMerge
- | BinOp::RecursiveRecordTypeMerge
- | BinOp::Equivalence => unreachable!(),
- BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
- });
-
- if *l.ty() != t {
- return span_err("BinOpTypeMismatch");
- }
-
- if *r.ty() != t {
- return span_err("BinOpTypeMismatch");
- }
-
- t
- }
- ExprKind::Op(OpKind::Merge(record, union, type_annot)) => {
- let record_type = record.ty();
- let handlers = match record_type.kind() {
- NirKind::RecordType(kts) => kts,
- _ => return span_err("Merge1ArgMustBeRecord"),
- };
-
- let union_type = union.ty();
- let variants = match union_type.kind() {
- NirKind::UnionType(kts) => Cow::Borrowed(kts),
- NirKind::OptionalType(ty) => {
- let mut kts = HashMap::new();
- kts.insert("None".into(), None);
- kts.insert("Some".into(), Some(ty.clone()));
- Cow::Owned(kts)
- }
- _ => return span_err("Merge2ArgMustBeUnionOrOptional"),
- };
-
- let mut inferred_type = None;
- for (x, handler_type) in handlers {
- let handler_return_type: Type = match variants.get(x) {
- // Union alternative with type
- Some(Some(variant_type)) => match handler_type.kind() {
- NirKind::PiClosure { closure, annot, .. } => {
- if variant_type != annot {
- return mkerr(
- ErrorBuilder::new(format!(
- "Wrong handler input type"
- ))
- .span_err(
- span,
- format!("in this merge expression",),
- )
- .span_err(
- record.span(),
- format!(
- "the handler for `{}` expects a \
- value of type: `{}`",
- x,
- annot.to_expr_tyenv(env)
- ),
- )
- .span_err(
- union.span(),
- format!(
- "but the corresponding variant \
- has type: `{}`",
- variant_type.to_expr_tyenv(env)
- ),
- )
- .format(),
- );
- }
-
- // TODO: this actually doesn't check anything yet
- match closure.remove_binder() {
- Ok(v) => {
- Type::new_infer_universe(env, v.clone())?
- }
- Err(()) => {
- return span_err(
- "MergeReturnTypeIsDependent",
- )
- }
- }
- }
- _ => {
- return mkerr(
- ErrorBuilder::new(format!(
- "merge handler is not a function"
- ))
- .span_err(
- span,
- format!("in this merge expression"),
- )
- .span_err(
- record.span(),
- format!(
- "the handler for `{}` has type: `{}`",
- x,
- handler_type.to_expr_tyenv(env)
- ),
- )
- .span_help(
- union.span(),
- format!(
- "the corresponding variant has type: \
- `{}`",
- variant_type.to_expr_tyenv(env)
- ),
- )
- .help(format!(
- "a handler for this variant must be a \
- function that takes an input of type: \
- `{}`",
- variant_type.to_expr_tyenv(env)
- ))
- .format(),
- )
- }
- },
- // Union alternative without type
- Some(None) => {
- Type::new_infer_universe(env, handler_type.clone())?
- }
- None => return span_err("MergeHandlerMissingVariant"),
- };
- match &inferred_type {
- None => inferred_type = Some(handler_return_type),
- Some(t) => {
- if t != &handler_return_type {
- return span_err("MergeHandlerTypeMismatch");
- }
- }
- }
- }
- for x in variants.keys() {
- if !handlers.contains_key(x) {
- return span_err("MergeVariantMissingHandler");
- }
- }
-
- 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 {
- return span_err("MergeAnnotMismatch");
- }
- t1
- }
- (Some(t), None) => t,
- (None, Some(t)) => t,
- (None, None) => return span_err("MergeEmptyNeedsAnnotation"),
- }
- }
- ExprKind::Op(OpKind::ToMap(record, annot)) => {
+ ToMap(record, annot) => {
if record.ty().ty().as_const() != Some(Const::Type) {
return span_err("`toMap` only accepts records of type `Type`");
}
let record_t = record.ty();
let kts = match record_t.kind() {
- NirKind::RecordType(kts) => kts,
+ RecordType(kts) => kts,
_ => {
return span_err("The argument to `toMap` must be a record")
}
@@ -581,11 +410,11 @@ fn type_one_layer(
let err_msg = "The type of `toMap x` must be of the form \
`List { mapKey : Text, mapValue : T }`";
let arg = match annot_val.kind() {
- NirKind::ListType(t) => t,
+ ListType(t) => t,
_ => return span_err(err_msg),
};
let kts = match arg.kind() {
- NirKind::RecordType(kts) => kts,
+ RecordType(kts) => kts,
_ => return span_err(err_msg),
};
if kts.len() != 2 {
@@ -614,7 +443,7 @@ fn type_one_layer(
kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
kts.insert("mapValue".into(), entry_type);
let output_type: Type = Nir::from_builtin(Builtin::List)
- .app(Nir::from_kind(NirKind::RecordType(kts)))
+ .app(Nir::from_kind(RecordType(kts)))
.to_type(Const::Type);
if let Some(annot) = annot {
let annot_val = annot.eval_to_type(env)?;
@@ -625,10 +454,36 @@ fn type_one_layer(
output_type
}
}
- ExprKind::Op(OpKind::Projection(record, labels)) => {
+ Field(scrut, x) => {
+ match scrut.ty().kind() {
+ RecordType(kts) => match kts.get(&x) {
+ Some(val) => Type::new_infer_universe(env, val.clone())?,
+ None => return span_err("MissingRecordField"),
+ },
+ NirKind::Const(_) => {
+ let scrut = scrut.eval_to_type(env)?;
+ match scrut.kind() {
+ UnionType(kts) => match kts.get(x) {
+ // Constructor has type T -> < x: T, ... >
+ Some(Some(ty)) => Nir::from_kind(PiClosure {
+ binder: Binder::new(x.clone()),
+ annot: ty.clone(),
+ closure: Closure::new_constant(scrut.to_nir()),
+ })
+ .to_type(scrut.ty()),
+ Some(None) => scrut,
+ None => return span_err("MissingUnionField"),
+ },
+ _ => return span_err("NotARecord"),
+ }
+ }
+ _ => return span_err("NotARecord"),
+ }
+ }
+ Projection(record, labels) => {
let record_type = record.ty();
let kts = match record_type.kind() {
- NirKind::RecordType(kts) => kts,
+ RecordType(kts) => kts,
_ => return span_err("ProjectionMustBeRecord"),
};
@@ -648,21 +503,18 @@ fn type_one_layer(
};
}
- Type::new_infer_universe(
- env,
- Nir::from_kind(NirKind::RecordType(new_kts)),
- )?
+ Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))?
}
- ExprKind::Op(OpKind::ProjectionByExpr(record, selection)) => {
+ ProjectionByExpr(record, selection) => {
let record_type = record.ty();
let rec_kts = match record_type.kind() {
- NirKind::RecordType(kts) => kts,
+ RecordType(kts) => kts,
_ => return span_err("ProjectionMustBeRecord"),
};
let selection_val = selection.eval_to_type(env)?;
let sel_kts = match selection_val.kind() {
- NirKind::RecordType(kts) => kts,
+ RecordType(kts) => kts,
_ => return span_err("ProjectionByExprTakesRecordType"),
};
@@ -679,13 +531,182 @@ fn type_one_layer(
selection_val
}
- };
+ Completion(..) => {
+ unreachable!("This case should have been handled in resolution")
+ }
+ })
+}
- Ok(ty)
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
+fn type_one_layer(
+ env: &TyEnv,
+ ekind: ExprKind<Tir<'_>>,
+ span: Span,
+) -> Result<Type, TypeError> {
+ let span_err = |msg: &str| mk_span_err(span.clone(), msg);
+
+ Ok(match &ekind {
+ ExprKind::Import(..) => {
+ unreachable!("This case should have been handled in resolution")
+ }
+ 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::Const(Const::Type) => Type::from_const(Const::Kind),
+ ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
+ ExprKind::Num(num) => Type::from_builtin(match num {
+ NumKind::Bool(_) => Builtin::Bool,
+ NumKind::Natural(_) => Builtin::Natural,
+ NumKind::Integer(_) => Builtin::Integer,
+ NumKind::Double(_) => Builtin::Double,
+ }),
+ ExprKind::Builtin(b) => {
+ let t_hir = type_of_builtin(*b);
+ typecheck(&t_hir)?.eval_to_type(env)?
+ }
+ ExprKind::TextLit(interpolated) => {
+ let text_type = Type::from_builtin(Builtin::Text);
+ for contents in interpolated.iter() {
+ use InterpolatedTextContents::Expr;
+ if let Expr(x) = contents {
+ if *x.ty() != text_type {
+ return span_err("InvalidTextInterpolation");
+ }
+ }
+ }
+ text_type
+ }
+ ExprKind::SomeLit(x) => {
+ if x.ty().ty().as_const() != Some(Const::Type) {
+ return span_err("InvalidOptionalType");
+ }
+
+ let t = x.ty().to_nir();
+ Nir::from_builtin(Builtin::Optional)
+ .app(t)
+ .to_type(Const::Type)
+ }
+ ExprKind::EmptyListLit(t) => {
+ let t = t.eval_to_type(env)?;
+ match t.kind() {
+ NirKind::ListType(..) => {}
+ _ => return span_err("InvalidListType"),
+ };
+ t
+ }
+ ExprKind::NEListLit(xs) => {
+ let mut iter = xs.iter();
+ let x = iter.next().unwrap();
+ for y in iter {
+ if x.ty() != y.ty() {
+ return span_err("InvalidListElement");
+ }
+ }
+ if x.ty().ty().as_const() != Some(Const::Type) {
+ return span_err("InvalidListType");
+ }
+
+ let t = x.ty().to_nir();
+ Nir::from_builtin(Builtin::List).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()) {
+ Entry::Occupied(_) => {
+ return span_err("RecordTypeDuplicateField")
+ }
+ Entry::Vacant(e) => e.insert(v.ty().to_nir()),
+ };
+
+ // Check that the fields have a valid kind
+ match v.ty().ty().as_const() {
+ Some(c) => k = max(k, c),
+ None => return span_err("InvalidFieldType"),
+ }
+ }
+
+ Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
+ }
+ ExprKind::RecordType(kts) => {
+ use std::collections::hash_map::Entry;
+ let mut seen_fields = HashMap::new();
+ // An empty record type has type Type
+ let mut k = Const::Type;
+
+ for (x, t) in kts {
+ // Check for duplicated entries
+ match seen_fields.entry(x.clone()) {
+ Entry::Occupied(_) => {
+ return span_err("RecordTypeDuplicateField")
+ }
+ Entry::Vacant(e) => e.insert(()),
+ };
+
+ // Check the type is a Const and compute final type
+ match t.ty().as_const() {
+ Some(c) => k = max(k, c),
+ None => return span_err("InvalidFieldType"),
+ }
+ }
+
+ Type::from_const(k)
+ }
+ ExprKind::UnionType(kts) => {
+ use std::collections::hash_map::Entry;
+ let mut seen_fields = HashMap::new();
+ // Check that all types are the same const
+ let mut k = None;
+ for (x, t) in kts {
+ if let Some(t) = t {
+ match (k, t.ty().as_const()) {
+ (None, Some(k2)) => k = Some(k2),
+ (Some(k1), Some(k2)) if k1 == k2 => {}
+ _ => return span_err("InvalidFieldType"),
+ }
+ }
+ match seen_fields.entry(x) {
+ Entry::Occupied(_) => {
+ return span_err("UnionTypeDuplicateField")
+ }
+ Entry::Vacant(e) => e.insert(()),
+ };
+ }
+
+ // An empty union type has type Type;
+ // an union type with only unary variants also has type Type
+ let k = k.unwrap_or(Const::Type);
+
+ Type::from_const(k)
+ }
+ ExprKind::Op(op) => type_of_operation(env, span, op)?,
+ ExprKind::Assert(t) => {
+ let t = t.eval_to_type(env)?;
+ match t.kind() {
+ NirKind::Equivalence(x, y) if x == y => {}
+ NirKind::Equivalence(..) => return span_err("AssertMismatch"),
+ _ => return span_err("AssertMustTakeEquivalence"),
+ }
+ t
+ }
+ })
}
/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
/// to compare with.
+// We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use
+// it to handle the annotations in merge/toMap/etc. uniformly.
pub fn type_with<'hir>(
env: &TyEnv,
hir: &'hir Hir,
@@ -781,7 +802,7 @@ pub fn type_with<'hir>(
Ok(tir)
}
-/// Typecheck an expression and return the expression annotated with types if type-checking
+/// Typecheck an expression and return the expression annotated with its type if type-checking
/// succeeded, or an error if type-checking failed.
pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
type_with(&TyEnv::new(), hir, None)
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-16 18:24:11 +0000