From f47f60503929a1c5cef9913736a381be2c90e2e5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Apr 2021 22:17:29 -0700 Subject: [PATCH] fix: remove incorrect test It had two problems: - It was preventing coercions from being applied. - It was compromising error recovery. The body of the lambda was not being elaborated when the exception was thrown. The new error message is more verbose and potentially confusing, but it is better than the one produced this morning. --- src/Lean/Elab/Binders.lean | 5 +- src/Lean/Elab/Term.lean | 49 +++++++++++-------- .../mulcommErrorMessage.lean.expected.out | 30 ++++++++++-- 3 files changed, 55 insertions(+), 29 deletions(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index f01583cc0b..ed92845871 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -313,10 +313,7 @@ private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) : let b := b.instantiate1 fvar pure { s with expectedType? := some b } | _ => - if expectedType.getAppFn.isMVar then - pure { s with expectedType? := none } - else - throwError "expected type is not a function type{indentExpr expectedType}" + pure { s with expectedType? := none } private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat) (s : State) : TermElabM State := do if h : i < binderViews.size then diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 3c21d04d64..6984161da3 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -932,20 +932,10 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed (← saveContext)) pure mvar -private def decorateErrorMessageWithLambdaImplicitVars (ref : Syntax) (msg : MessageData) (impFVars : Array Expr) : TermElabM Exception := do - if impFVars.isEmpty then - return Exception.error ref msg - else - let mut msg := m!"{msg}\nthe following variables have been introduced by the implicit lamda feature" - for impFVar in impFVars do - msg := m!"{msg}{indentD m!"{impFVar} : {← inferType impFVar}"}" - msg := m!"{msg}\nyou can disable implict lambdas using `@` or writing a lambda expression with `\{}` or `[]` binder annotations." - return Exception.error ref msg - /- Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or an error is found. -/ -private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) (impFVars : Array Expr) +private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : List TermElab → TermElabM Expr | [] => do throwError "unexpected syntax{indentD stx}" | (elabFn::elabFns) => do @@ -953,7 +943,6 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : elabFn stx expectedType? catch ex => match ex with | Exception.error ref msg => - let ex ← decorateErrorMessageWithLambdaImplicitVars ref msg impFVars if (← read).errToSorry then exceptionToSorry ex expectedType? else @@ -963,7 +952,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : exceptionToSorry ex expectedType? else if id == unsupportedSyntaxExceptionId then s.restore - elabUsingElabFnsAux s stx expectedType? catchExPostpone impFVars elabFns + elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns else if catchExPostpone && id == postponeExceptionId then /- If `elab` threw `Exception.postpone`, we reset any state modifications. For example, we want to make sure pending synthetic metavariables created by `elab` before @@ -984,12 +973,12 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : else throw ex -private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) (impFVars : Array Expr): TermElabM Expr := do +private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : TermElabM Expr := do let s ← saveState let table := termElabAttribute.ext.getState (← getEnv) |>.table let k := stx.getKind match table.find? k with - | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone impFVars elabFns + | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns | none => throwError "elaboration function for '{k}' has not been implemented{indentD stx}" instance : MonadMacroAdapter TermElabM where @@ -1064,12 +1053,30 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te | _ => pure none | _ => pure none +private def decorateErrorMessageWithLambdaImplicitVars (ex : Exception) (impFVars : Array Expr) : TermElabM Exception := do + match ex with + | Exception.error ref msg => + if impFVars.isEmpty then + return Exception.error ref msg + else + let mut msg := m!"{msg}\nthe following variables have been introduced by the implicit lamda feature" + for impFVar in impFVars do + let auxMsg := m!"{impFVar} : {← inferType impFVar}" + let auxMsg ← addMessageContext auxMsg + msg := m!"{msg}{indentD auxMsg}" + msg := m!"{msg}\nyou can disable implict lambdas using `@` or writing a lambda expression with `\{}` or `[]` binder annotations." + return Exception.error ref msg + | _ => return ex + private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (impFVars : Array Expr) : TermElabM Expr := do - let body ← elabUsingElabFns stx expectedType catchExPostpone impFVars - let body ← ensureHasType expectedType body - let r ← mkLambdaFVars impFVars body - trace[Elab.implicitForall] r - pure r + let body ← elabUsingElabFns stx expectedType catchExPostpone + try + let body ← ensureHasType expectedType body + let r ← mkLambdaFVars impFVars body + trace[Elab.implicitForall] r + pure r + catch ex => + throw (← decorateErrorMessageWithLambdaImplicitVars ex impFVars) private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) (type : Expr) : TermElabM Expr := loop type #[] @@ -1103,7 +1110,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : let implicit? ← if implicitLambda && (← read).implicitLambda then useImplicitLambda? stx expectedType? else pure none match implicit? with | some expectedType => elabImplicitLambda stx catchExPostpone expectedType - | none => elabUsingElabFns stx expectedType? catchExPostpone (impFVars := #[]) + | none => elabUsingElabFns stx expectedType? catchExPostpone def addTermInfo (stx : Syntax) (e : Expr) : TermElabM Unit := do if (← getInfoState).enabled then diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out index 83c5363b26..8b3daf9bd3 100644 --- a/tests/lean/mulcommErrorMessage.lean.expected.out +++ b/tests/lean/mulcommErrorMessage.lean.expected.out @@ -1,12 +1,34 @@ -mulcommErrorMessage.lean:8:17-8:18: error: expected type is not a function type - a✝ * b✝ = b✝ * a✝ +mulcommErrorMessage.lean:8:13-13:25: error: type mismatch + fun (a : ?m) (b : ?m a) => ?m a b +has type + (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u) +but is expected to have type + a✝ * b✝ = b✝ * a✝ : Prop the following variables have been introduced by the implicit lamda feature a✝ : Bool b✝ : Bool you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations. -mulcommErrorMessage.lean:16:5-16:6: error: expected type is not a function type - a✝ * b✝ = b✝ * a✝ +mulcommErrorMessage.lean:11:22-11:25: error: type mismatch + rfl +has type + true = true : Prop +but is expected to have type + true = false : Prop +mulcommErrorMessage.lean:16:3-17:47: error: type mismatch + fun (a b : Bool) => Bool.casesOn a (?m a b) (?m a b) +has type + (a b : Bool) → ?m a b a : Sort (imax 1 1 ?u) +but is expected to have type + a✝ * b✝ = b✝ * a✝ : Prop the following variables have been introduced by the implicit lamda feature a✝ : Bool b✝ : Bool you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations. +mulcommErrorMessage.lean:16:12-17:47: error: application type mismatch + Bool.casesOn a ?m (Bool.casesOn b ?m ?m) +argument + Bool.casesOn b ?m ?m +has type + ?m a b b : Sort ?u +but is expected to have type + ?m a b true : Sort ?u