apply instance check fails at reducible transparency

Stream: lean4

[Jannis Limperg]

This is an MWE (well, sort of minimal) extracted from an Aesop failure at #7909:

import Mathlib.Topology.Category.TopCat.Basic

universe u

example (X : TopCat) : X ⟶ TopCat.of PUnit.{u + 1} := by
  exists fun _ => PUnit.unit
  with_reducible apply continuous_const -- tactic 'apply' failed, failed to assign synthesized instance

The with_reducible apply fails even though the target unifies with the conclusion of continuous_const at reducible transparency. The issue seems to be that apply checks here whether some synthesised instances are defeq to inferred instances. In the above example, this check succeeds at default or instances transparency, but fails at reducible.

What would be a good solution to this in the context of Aesop rules that should be applied with reducible transparency? Change apply such that it performs this defeq check with at least default transparency (or maybe instances)? Turn off the check for Aesop's version of apply?

[Eric Wieser]

I think this suggests that there is some API missing to translate between raw functions and morphisms

[Eric Wieser]

This works:

import Mathlib.Topology.Category.TopCat.Basic

universe u

/-- type-cast between the underlying map and the categorical spelling -/
def TopCat.mkHom {X Y : TopCat} (f : ContinuousMap X Y) : X ⟶ Y := f

example (X : TopCat) : X ⟶ TopCat.of PUnit.{u + 1} := by
  refine TopCat.mkHom ?_
  exists fun _ => PUnit.unit
  with_reducible apply continuous_const --success

[Jannis Limperg]

I don't mind this solution because it means less work for me. ;)

Still, the user experience is very suboptimal: a lemma reducibly matches the target yet with_reducible apply fails to apply it. Does anyone have an intuition as to what would break if the check were performed at instances or default transparency? I'm guessing not much since the check should succeed in the vast majority of cases, but maybe I'm wrong.