apply_fun doesn't handle dependent functions

[jeremysalwen]

In lean3, apply_fun works fine with dependent functions:

import tactic.apply_fun

lemma foo {α} (a b: list α) (P: a = b): a = a := by
  apply_fun list.length at P

However, with mathlib4, this gives us an error:

import Std.Data.List.Basic
import Mathlib.Tactic.applyFun

open Lean

lemma foo (a b: List α) (P: a = b): True := by
  apply_fun List.length at P
  -- Error: Can not use `apply_fun` with a dependently typed function.

[semorrison]

The problem here is that Lean.Meta.mkCongrArg treats List.length as having type {α : Type _} → List α → ℕ, whereas we would really like it to first fill in the implicit argument α with a metavariable before handing it to congrArg. I can change applyFun to do this, but arguably Lean.Meta.mkCongrArg might want to handle this.