diff options
| -rw-r--r-- | dhall/src/error/builder.rs | 169 | ||||
| -rw-r--r-- | dhall/src/error/mod.rs | 9 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 3 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/env.rs | 6 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 204 | ||||
| -rw-r--r-- | dhall/tests/type-errors/hurkensParadox.txt | 4 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/AssertAlphaTrap.txt | 7 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 4 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt | 8 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt | 8 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 4 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 4 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt | 7 | ||||
| -rw-r--r-- | dhall/tests/type-errors/unit/VariableFree.txt | 7 | ||||
| -rw-r--r-- | tests_buffer | 2 |
15 files changed, 272 insertions, 174 deletions
diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs index e293220..22b0d77 100644 --- a/dhall/src/error/builder.rs +++ b/dhall/src/error/builder.rs @@ -4,97 +4,162 @@ use annotate_snippets::{ snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation}, }; -use crate::syntax::Span; +use crate::syntax::{ParsedSpan, Span}; -#[derive(Debug, Clone)] +#[derive(Debug, Clone, Default)] pub struct ErrorBuilder { + title: FreeAnnotation, + annotations: Vec<SpannedAnnotation>, + footer: Vec<FreeAnnotation>, + /// Inducate that the current builder has already been consumed and consuming it again should + /// panic. + consumed: bool, +} + +#[derive(Debug, Clone)] +struct SpannedAnnotation { + span: ParsedSpan, message: String, annotation_type: AnnotationType, - annotations: Vec<BuilderAnnotation>, } #[derive(Debug, Clone)] -struct BuilderAnnotation { - span: Span, +struct FreeAnnotation { message: String, annotation_type: AnnotationType, } +impl SpannedAnnotation { + fn into_annotation(self) -> SourceAnnotation { + SourceAnnotation { + label: self.message, + annotation_type: self.annotation_type, + range: self.span.as_char_range(), + } + } +} + +impl FreeAnnotation { + fn into_annotation(self) -> Annotation { + Annotation { + label: Some(self.message), + id: None, + annotation_type: self.annotation_type, + } + } +} + /// A builder that uses the annotate_snippets library to display nice error messages about source /// code locations. impl ErrorBuilder { - pub fn new(message: String) -> Self { + pub fn new(message: impl ToString) -> Self { ErrorBuilder { - message, - annotation_type: AnnotationType::Error, + title: FreeAnnotation { + message: message.to_string(), + annotation_type: AnnotationType::Error, + }, annotations: Vec::new(), + footer: Vec::new(), + consumed: false, } } - pub fn span_err(span: &Span, message: String) -> Self { + pub fn new_span_err(span: &Span, message: impl ToString) -> Self { + let message = message.to_string(); let mut builder = Self::new(message.clone()); - builder.annotate_err(span, message); + builder.span_err(span, message); builder } - pub fn annotate_err(&mut self, span: &Span, message: String) { - self.annotations.push(BuilderAnnotation { + pub fn span_err( + &mut self, + span: &Span, + message: impl ToString, + ) -> &mut Self { + // Ignore spans not coming from a source file + let span = match span { + Span::Parsed(span) => span, + _ => return self, + }; + self.annotations.push(SpannedAnnotation { span: span.clone(), - message, + message: message.to_string(), annotation_type: AnnotationType::Error, - }) + }); + self } - pub fn annotate_info(&mut self, span: &Span, message: String) { - self.annotations.push(BuilderAnnotation { + pub fn span_help( + &mut self, + span: &Span, + message: impl ToString, + ) -> &mut Self { + // Ignore spans not coming from a source file + let span = match span { + Span::Parsed(span) => span, + _ => return self, + }; + self.annotations.push(SpannedAnnotation { span: span.clone(), - message, + message: message.to_string(), + annotation_type: AnnotationType::Help, + }); + self + } + pub fn help(&mut self, message: impl ToString) -> &mut Self { + self.footer.push(FreeAnnotation { + message: message.to_string(), annotation_type: AnnotationType::Help, - }) + }); + self } // TODO: handle multiple files - pub fn format(self) -> String { - let mut input = None; - let annotations = self - .annotations - .into_iter() - .filter_map(|annot| { - let span = match annot.span { - Span::Parsed(span) => span, - _ => return None, - }; - if input.is_none() { - input = Some(span.to_input()); - } - Some(SourceAnnotation { - label: annot.message, - annotation_type: annot.annotation_type, - range: span.as_char_range(), - }) - }) - .collect(); - - let input = match input { - Some(input) => input, - None => return format!("[unknown location] {}", self.message), - }; + pub fn format(&mut self) -> String { + if self.consumed { + panic!("tried to format the same ErrorBuilder twice") + } + let this = std::mem::replace(self, ErrorBuilder::default()); + self.consumed = true; + drop(self); // Get rid of the self reference so we don't use it by mistake. - let snippet = Snippet { - title: Some(Annotation { - label: Some(self.message), - id: None, - annotation_type: self.annotation_type, - }), - footer: vec![], - slices: vec![Slice { + let slices = if this.annotations.is_empty() { + Vec::new() + } else { + let input = this.annotations[0].span.to_input(); + let annotations = this + .annotations + .into_iter() + .map(|annot| annot.into_annotation()) + .collect(); + vec![Slice { source: input, line_start: 1, // TODO origin: Some("<current file>".to_string()), fold: true, annotations, - }], + }] + }; + let footer = this + .footer + .into_iter() + .map(|annot| annot.into_annotation()) + .collect(); + + let snippet = Snippet { + title: Some(this.title.into_annotation()), + slices, + footer, }; let dl = DisplayList::from(snippet); let dlf = DisplayListFormatter::new(true, false); format!("{}", dlf.format(&dl)) } } + +impl Default for FreeAnnotation { + fn default() -> Self { + FreeAnnotation { + message: String::new(), + annotation_type: AnnotationType::Error, + } + } +} diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 5b7693e..6ea7d0c 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,7 +1,6 @@ use std::io::Error as IOError; use crate::semantics::resolve::ImportStack; -use crate::semantics::Value; use crate::syntax::{Import, ParseError}; use crate::NormalizedExpr; @@ -49,8 +48,6 @@ pub struct TypeError { #[derive(Debug)] pub(crate) enum TypeMessage { // UnboundVariable(Span), - InvalidInputType(Value), - InvalidOutputType(Value), // NotAFunction(Value), // TypeMismatch(Value, Value, Value), // AnnotMismatch(Value, Value), @@ -100,12 +97,6 @@ impl std::fmt::Display for TypeError { use TypeMessage::*; let msg = match &self.message { // UnboundVariable(var) => var.error("Type error: Unbound variable"), - InvalidInputType(v) => { - v.span().error("Type error: Invalid function input") - } - InvalidOutputType(v) => { - v.span().error("Type error: Invalid function output") - } // NotAFunction(v) => v.span().error("Type error: Not a function"), // TypeMismatch(x, y, z) => { // x.span() diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d97b8c4..bb3e3c0 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -174,9 +174,6 @@ impl Value { _ => None, } } - pub(crate) fn span(&self) -> Span { - self.0.span.clone() - } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 812ca7a..1fc711c 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value}; +use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value}; use crate::syntax::{Label, V}; /// Environment for indexing variables. @@ -116,9 +116,9 @@ impl TyEnv { items: self.items.insert_value(e), } } - pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> { + pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> { let var = self.names.unlabel_var(var)?; let ty = self.items.lookup_ty(&var); - Some((TyExprKind::Var(var), ty)) + Some((var, ty)) } } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a652663..e642b8f 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -35,19 +35,6 @@ fn function_check(a: Const, b: Const) -> Const { } } -fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> { - let ks = match src.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))), - }; - let kt = match tgt.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))), - }; - - Ok(Value::from_const(function_check(ks, kt))) -} - fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> { Err(TypeError::new(TypeMessage::Custom(x.to_string()))) } @@ -64,12 +51,55 @@ fn type_one_layer( "There should remain no imports in a resolved expression" ), ExprKind::Var(..) - | ExprKind::Lam(..) - | ExprKind::Pi(..) - | ExprKind::Let(..) | ExprKind::Const(Const::Sort) | ExprKind::Embed(..) => unreachable!(), // Handled in type_with + ExprKind::Lam(binder, annot, body) => { + let body_ty = body.get_type()?; + let body_ty = body_ty.to_tyexpr(env.as_varenv().insert()); + let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty); + let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?; + let ty = TyExpr::new( + TyExprKind::Expr(pi_ekind), + Some(pi_ty), + Span::Artificial, + ); + ty.eval(env.as_nzenv()) + } + ExprKind::Pi(_, annot, body) => { + let ks = match annot.get_type()?.as_const() { + Some(k) => k, + _ => { + return mkerr( + ErrorBuilder::new(format!( + "Invalid input type: `{}`", + annot.get_type()?.to_expr_tyenv(env), + )) + .span_err( + &annot.span(), + format!( + "this has type: `{}`", + annot.get_type()?.to_expr_tyenv(env) + ), + ) + .help( + format!( + "The input type of a function must have type `Type`, `Kind` or `Sort`", + ), + ) + .format(), + ); + } + }; + let kt = match body.get_type()?.as_const() { + Some(k) => k, + _ => return mkerr("Invalid output type"), + }; + + Value::from_const(function_check(ks, kt)) + } + ExprKind::Let(_, _, _, body) => body.get_type()?, + ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), ExprKind::Builtin(b) => { @@ -202,10 +232,12 @@ fn type_one_layer( ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { - let pi_ty = type_of_function( - ty.get_type()?, - scrut.get_type()?, - )?; + // Can't fail because uniontypes must have type Const(_). + let kt = scrut.get_type()?.as_const().unwrap(); + // The type of the field must be Const smaller than `kt`, thus the + // function type has type `kt`. + let pi_ty = Value::from_const(kt); + Value::from_kind_and_type( ValueKind::PiClosure { binder: Binder::new(x.clone()), @@ -256,25 +288,27 @@ fn type_one_layer( ExprKind::App(f, arg) => match f.get_type()?.kind() { ValueKind::PiClosure { annot, closure, .. } => { if arg.get_type()? != *annot { - let mut builder = ErrorBuilder::span_err( - &span, - format!("function annot mismatch",), - ); - builder.annotate_info( - &f.span(), - format!( - "this expects an argument of type: {}", - annot.to_expr_tyenv(env), - ), + return mkerr( + ErrorBuilder::new_span_err( + &span, + format!("Wrong type of function argument"), + ) + .span_help( + &f.span(), + format!( + "this expects an argument of type: {}", + annot.to_expr_tyenv(env), + ), + ) + .span_help( + &arg.span(), + format!( + "but this has type: {}", + arg.get_type()?.to_expr_tyenv(env), + ), + ) + .format(), ); - builder.annotate_info( - &arg.span(), - format!( - "but this has type: {}", - arg.get_type()?.to_expr_tyenv(env), - ), - ); - return mkerr(builder.format()); } let arg_nf = arg.eval(env.as_nzenv()); @@ -534,62 +568,15 @@ pub(crate) fn type_with( ) -> Result<TyExpr, TypeError> { let (tyekind, ty) = match expr.as_ref() { ExprKind::Var(var) => match env.lookup(&var) { - Some((k, ty)) => (k, Some(ty)), - None => return mkerr("unbound variable"), + Some((v, ty)) => (TyExprKind::Var(v), Some(ty)), + None => { + return mkerr( + ErrorBuilder::new(format!("unbound variable `{}`", var)) + .span_err(&expr.span(), "not found in this scope") + .format(), + ) + } }, - ExprKind::Lam(binder, annot, body) => { - let annot = type_with(env, annot)?; - let annot_nf = annot.eval(env.as_nzenv()); - let body_env = env.insert_type(&binder, annot_nf.clone()); - let body = type_with(&body_env, body)?; - let body_ty = body.get_type()?; - let ty = TyExpr::new( - TyExprKind::Expr(ExprKind::Pi( - binder.clone(), - annot.clone(), - body_ty.to_tyexpr(body_env.as_varenv()), - )), - Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?), - Span::Artificial, - ); - let ty = ty.eval(env.as_nzenv()); - ( - TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), - Some(ty), - ) - } - ExprKind::Pi(binder, annot, body) => { - let annot = type_with(env, annot)?; - let annot_nf = annot.eval(env.as_nzenv()); - let body = - type_with(&env.insert_type(binder, annot_nf.clone()), body)?; - let ty = type_of_function(annot.get_type()?, body.get_type()?)?; - ( - TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), - Some(ty), - ) - } - ExprKind::Let(binder, annot, val, body) => { - let val = if let Some(t) = annot { - t.rewrap(ExprKind::Annot(val.clone(), t.clone())) - } else { - val.clone() - }; - - let val = type_with(env, &val)?; - let val_nf = val.eval(&env.as_nzenv()); - let body = type_with(&env.insert_value(&binder, val_nf), body)?; - let body_ty = body.get_type().ok(); - ( - TyExprKind::Expr(ExprKind::Let( - binder.clone(), - None, - val, - body, - )), - body_ty, - ) - } ExprKind::Const(Const::Sort) => { (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None) } @@ -597,7 +584,36 @@ pub(crate) fn type_with( return Ok(p.clone().into_value().to_tyexpr_noenv()) } ekind => { - let ekind = ekind.traverse_ref(|e| type_with(env, e))?; + let ekind = match ekind { + ExprKind::Lam(binder, annot, body) => { + let annot = type_with(env, annot)?; + let annot_nf = annot.eval(env.as_nzenv()); + let body_env = env.insert_type(binder, annot_nf); + let body = type_with(&body_env, body)?; + ExprKind::Lam(binder.clone(), annot, body) + } + ExprKind::Pi(binder, annot, body) => { + let annot = type_with(env, annot)?; + let annot_nf = annot.eval(env.as_nzenv()); + let body_env = env.insert_type(binder, annot_nf); + let body = type_with(&body_env, body)?; + ExprKind::Pi(binder.clone(), annot, body) + } + ExprKind::Let(binder, annot, val, body) => { + let val = if let Some(t) = annot { + t.rewrap(ExprKind::Annot(val.clone(), t.clone())) + } else { + val.clone() + }; + let val = type_with(env, &val)?; + let val_nf = val.eval(&env.as_nzenv()); + let body_env = env.insert_value(&binder, val_nf); + let body = type_with(&body_env, body)?; + ExprKind::Let(binder.clone(), None, val, body) + } + _ => ekind.traverse_ref(|e| type_with(env, e))?, + }; + let ty = type_one_layer(env, &ekind, expr.span())?; (TyExprKind::Expr(ekind), Some(ty)) } diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 10bb9a4..e06c4b2 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1,4 +1,4 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> <current file>:6:23 | 1 | let bottom : Type = ∀(any : Type) → any @@ -8,7 +8,7 @@ Type error: Unhandled error: error: function annot mismatch ... 10 | : pow (pow U) → U 11 | = λ(t : pow (pow U)) - | ^^^^^ function annot mismatch + | ^^^^^ Wrong type of function argument | --- help: this expects an argument of type: Kind | - help: but this has type: Sort | diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt index 87cf48e..e4584f5 100644 --- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt +++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable ``_`` + --> <current file>:1:46 + | +1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _) + | ^ not found in this scope + | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 7aa2281..776b14e 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1,8 +1,8 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> <current file>:1:1 | 1 | (λ(_ : Natural) → _) True - | ^^^^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ^^^^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument | ------------------ help: this expects an argument of type: Natural | ---- help: but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index a13fb3a..3fc1652 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1 +1,7 @@ -[unknown location] Type error: Invalid function input +Type error: Unhandled error: error: Invalid input type: `Natural` + --> <current file>:1:6 + | +1 | λ(_ : 1) → _ + | ^ this has type: `Natural` + | + = help: The input type of a function must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index a13fb3a..948c6c7 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1 +1,7 @@ -[unknown location] Type error: Invalid function input +Type error: Unhandled error: error: Invalid input type: `Natural` + --> <current file>:1:0 + | +1 | 2 → _ + | ^ this has type: `Natural` + | + = help: The input type of a function must have type `Type`, `Kind` or `Sort` diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 3673338..125cc87 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1,8 +1,8 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> <current file>:1:5 | 1 | [] : List Type - | ^^^^^^^^^ function annot mismatch + | ^^^^^^^^^ Wrong type of function argument | ---- help: this expects an argument of type: Type | ---- help: but this has type: Kind | diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 795c97c..5ee2a11 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1,8 +1,8 @@ -Type error: Unhandled error: error: function annot mismatch +Type error: Unhandled error: error: Wrong type of function argument --> <current file>:1:0 | 1 | Natural/subtract True True - | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ^^^^^^^^^^^^^^^^^^^^^ Wrong type of function argument | ---------------- help: this expects an argument of type: Natural | ---- help: but this has type: Bool | diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt index 87cf48e..a234f9f 100644 --- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt +++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable `constructors` + --> <current file>:1:0 + | +1 | constructors < Left : Natural | Right : Bool > + | ^^^^^^^^^^^^ not found in this scope + | diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt index 87cf48e..52baa7f 100644 --- a/dhall/tests/type-errors/unit/VariableFree.txt +++ b/dhall/tests/type-errors/unit/VariableFree.txt @@ -1 +1,6 @@ -Type error: Unhandled error: unbound variable +Type error: Unhandled error: error: unbound variable `x` + --> <current file>:1:0 + | +1 | x + | ^ not found in this scope + | diff --git a/tests_buffer b/tests_buffer index 34210a9..87d73ef 100644 --- a/tests_buffer +++ b/tests_buffer @@ -51,6 +51,8 @@ success/ let X = 0 in λ(T : Type) → λ(x : T) → 1 (λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T failure/ + \(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _) + \(x: let x = 1 in Sort) -> 0 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 |