Strange error on `congr` macro

Stream: mathlib4

[Jz Pan]

import Mathlib.Tactic.CongrM

def T1 (A : Nat → Type) := ∀ n, A n
def T2 (A : Nat → Type) := { f : ∀ n, A n // f = f }

example {A : Nat → Type} (f g : ∀ n, A n) (h : f = g) (n : Nat) : f n = g n := by
  have := congr($h n) -- works (1)
  exact this

example {A : Nat → Type} (f g : T1 A) (h : f = g) (n : Nat) : f n = g n := by
  have := congr($h n) -- works (2)
  exact this

example {A : Nat → Type} (f g : T2 A) (h : f = g) (n : Nat) : f.1 n = g.1 n := by
  have := congr($h.1 n) -- does not work (3)
  sorry

example {A : Nat → Type} (f g : T2 A) (h : f = g) (n : Nat) : f.1 n = g.1 n := by
  have hh := congr($h.1) -- works
  have := congr($hh n) -- does not work (4)
  sorry

I have no idea why (3) and (4) does not work. I think the (4) is exactly the same as in (1).

[Aaron Liu]

example 3 I can see how that error message could happen, example 4 I have no idea

[Kyle Miller]

They're both cases of "overapplication" of Subtype.val. The specific values of the arguments make it possible to use it as a function of more arguments than you can see from the type of Subtype.val itself.

This oversight happens a frequently in congruence code.

It won't be too hard to fix.

[Kyle Miller]

@Jz Pan Fixed in #25851.

I ended up rewriting a good portion of the app congruence generator, and made things more efficient. The proof terms are more efficient as well. It used to always create these large HEq casting terms, but now it utilizes congrArg/congrFun/congr if it can. That was enough to handle your example:

example {A : Nat → Type} (f g : T2 A) (h : f = g) (n : Nat) : f.1 n = g.1 n := by?
  have := congr($h.1 n) -- (3)
  exact this
/-
Try this: have this := id (congrArg (fun x => x.val n) h);
this
-/

It also handles overapplication in more complicated cases.

[Jz Pan]

Kyle Miller said:

Jz Pan Fixed in #25851.

I ended up rewriting a good portion of the app congruence generator, and made things more efficient. The proof terms are more efficient as well. It used to always create these large HEq casting terms, but now it utilizes congrArg/congrFun/congr if it can. That was enough to handle your example:

example {A : Nat → Type} (f g : T2 A) (h : f = g) (n : Nat) : f.1 n = g.1 n := by?
  have := congr($h.1 n) -- (3)
  exact this
/-
Try this: have this := id (congrArg (fun x => x.val n) h);
this
-/

It also handles overapplication in more complicated cases.

Thank you very much!

[Kyle Miller]

Following up, these examples all work now.

Please let me know if you run into any other congr() issues!