uninterpolated error message: unecessary generalizing

Stream: lean4

[Siddharth Bhat]

In a somewhat complex mathlib development that's difficult to MWE, I was able to produce the error message:

unnecessary 'generalizing' argument,
variable '{mkFVar v}' is generalized automatically

which is strange, since one would assume that {mkFVar v} would have been interpolated.
In debugging this, I see that the offending line is:

-- Lean/Elab/Tactic/Induction.lean
-- process `generalizingVars` subterm of induction Syntax `stx`.
private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) : TacticM (Nat × MVarId) :=
     ...
      if forbidden.contains userFVarId then
        throwError "variable cannot be generalized because target depends on it{indentExpr (mkFVar userFVarId)}"
      if s.contains userFVarId then
        throwError "unnecessary 'generalizing' argument, variable '{mkFVar userFVarId}' is generalized automatically"

the definition of throwError says:

-- src/Lean/Exception.lean
macro_rules
  | `(throwError $msg:interpolatedStr) => `(Lean.throwError (m! $msg))
  | `(throwError $msg:term)            => `(Lean.throwError $msg)

how does throwError actually figure out that the $msg is an interpolatedStr? I'd be happy to fix this, but I'm not sure what the right fix is!

[Patrick Massot]

Siddharth Bhat said:

how does throwError actually figure out that the $msg is an interpolatedStr?is!

I guess it looks for s! in the input syntax.

[Kyle Miller]

That's weird -- if you open up that definition in VS Code it highlights like an interpolated string.

One way to force it to be one is putting m! right in front of the string, but that's not necessary here. In fact, if you #print generalizeVars you can see that it's been interpolated:

                Lean.throwError
                    (toMessageData "unnecessary 'generalizing' argument, variable '" ++
                        toMessageData (mkFVar userFVarId) ++
                      toMessageData "' is generalized automatically")

Could you try making a mwe?

[Siddharth Bhat]

The way to reproduce this is by uncommenting the "-- generalizing i" at this PR: https://github.com/leanprover-community/mathlib4/pull/5920/files#diff-f6a569804f7aec89a2a69cc9f1c115b1da9ff00349ebd8df8845b35c85b3acb5R406

[Siddharth Bhat]

Aha, I think I am looking at induction instead of induction'.

[Siddharth Bhat]

https://github.com/leanprover-community/mathlib4/blob/ec3e666d5e8dca12efcea13b028c27413d3f4bda/Mathlib/Tactic/Cases.lean#L81-L82

elab (name := induction') "induction' " tgts:(Parser.Tactic.casesTarget,+)
  ...
          throwError ("unnecessary 'generalizing' argument, " ++
            "variable '{mkFVar v}' is generalized automatically")

[Siddharth Bhat]

OK, I'll make a PR for this.

[Siddharth Bhat]

What's the ideal fix? do I remove the ++? call m! on both strings and keep the ++?

[Kyle Miller]

          throwError "variable cannot be generalized {""
            }because target depends on it{indentExpr (mkFVar v)}"

[Kyle Miller]

This is a bit of a hack, but hopefully we'll have proper line continuations for strings at some point, and then we can look for all {"" and ""}

[Siddharth Bhat]

PRd at https://github.com/leanprover-community/mathlib4/pull/8132

[Siddharth Bhat]

I also audited the other uses of throwError, and we have some uses that look like this:

Relation/Trans.lean:      | none => throwError "transitivity lemmas only apply to FLAG
Relation/Trans.lean-        binary relations, not {indentExpr tgt}"

Does this introduce a newline in the error message? Is this something we should also change to the {""} style?

[Kyle Miller]

Yeah, that introduces a newline and probably a bunch of whitespace too. That should be fixed.