simps sometimes gets types confused

[eric-wieser]

mwe:

import Mathlib.Tactic
import Mathlib.Logic.Equiv.Basic

@[simps]
def univRefl : (Set.univ : Set ℕ) ≃ (Set.univ : Set ℕ) where
  toFun x := x 
  invFun x := x
  left_inv _ := rfl
  right_inv _ := rfl

@[simps!]
def subtypeTrueRefl : Subtype (⊤ : ℕ → Prop) ≃ Subtype (⊤ : ℕ → Prop) where
  __ := univRefl

#check subtypeTrueRefl_apply
/-
subtypeTrueRefl_apply (a✝ : ↑Set.univ) : ↑subtypeTrueRefl a✝ = a✝
-/

The result has a binder a : Set.univ, but this is poorly-typed and should be a : Subtype ⊤

EDIT by Floris: Zulip

[eric-wieser]

This patch seems to fix the problem:

--- a/Mathlib/Tactic/Simps/Basic.lean
+++ b/Mathlib/Tactic/Simps/Basic.lean
@@ -1094,7 +1094,7 @@ partial def addProjections (nm : Name) (type lhs rhs : Expr)
   if let idx :: rest := toApply then
     let some ⟨newRhs, _⟩ := projInfo[idx]?
       | throwError "unreachable: index of composite projection is out of bounds."
-    let newType ← inferType newRhs
+    let newType ← inferType lhsAp
     trace[simps.debug] "Applying a custom composite projection. Todo: {toApply}. Current lhs:{
       indentExpr lhsAp}"
     return ← addProjections nm newType lhsAp newRhs newArgs false cfg todo rest

but results in a kernel error near the end of the simps tests

[fpvandoorn]

Yeah, simps is using the rhs to infer the type, which indeed unfolds definitions sometimes. lhsAp cannot be used: a user-projection could be a composite of multiple projections.

7707 attempts to fix this.

[fpvandoorn]

This issue is linked in various places of the library, but for many of these occurrences, this issue doesn't solve them. There are a couple of other issues for some of the linked:

• Definitions stated in a way such that the types are not in simp-normal form --> We can fix the statement of these definitions
• Lemmas (unrelated to simps) stated in a way that doesn't satisfy the linter. --> We can just remove the simp attribute
• Sometimes, a definition makes sense, but simps produces a lemma where the type of one of the new arguments to that lemma is not in simp normal form. E.g. it is some functor applied to an object, and we have a dsimp rule that this simplifies. I had not considered this before (because this was not relevant before). Probably this requires a new feature to simps that we dsimp the type of all new arguments.

[fpvandoorn]

A few of the occurrences are fixed in #7707 and #7929, I didn't check all occurrences