Qq doesn't know that two things have the same type

Stream: mathlib4

[Heather Macbeth]

I'm trying to write a positivity extension (cc @David Renshaw) and using Qq for the first time. Here is what I have:

import Mathlib.Algebra.Order.Hom.Basic

open Lean Meta Qq Mathlib Meta Positivity

/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
@[positivity _]
def evalMap : PositivityExt where eval {u₃ β} zβ pβ e := do
  let .app (.app _coe f') a' ← withReducible (whnf e) | throwError "not NonnegHomClass"
  let ⟨u₂, α, a⟩ ← inferTypeQ' a'
  let ⟨u₁, F, f⟩ ← inferTypeQ' f'
  let _a ← synthInstanceQ (q(NonnegHomClass $F $α $β) : Q(Type max (max u₁ u₂) u₃))
  pure (.nonnegative q(map_nonneg $f $a)) -- error here

[Heather Macbeth]

The error message is:

type mismatch
  map_nonneg «$f» «$a»
has type
  0 ≤ ↑«$f» «$a» : Prop
but is expected to have type
  0 ≤ «$e» : Prop

[Heather Macbeth]

On other positivity extensions, these error messages are solved by lines like

let _e_eq : $e =Q $c $f $a := ⟨⟩

I can't do this here because the _coe, which should be of type Q($F → $α → $β), is not known to be of this type by Lean. How can I tell it?

[Thomas Murrills]

Does have coe : Q($F → $α → $β) := coe (as a means of telling it the type) before the =Q line work? (Apologies if you’ve tried this, just checking)

[David Renshaw]

cop-out answer (no Qq):

  pure (.nonnegative (← mkAppM ``map_nonneg #[f', a']))

[Heather Macbeth]

David Renshaw said:

cop-out answer (no Qq):

  pure (.nonnegative (← mkAppM ``map_nonneg #[f', a']))

I know, I know ... I'm trying to learn how to use Qq though :)

[Heather Macbeth]

@Thomas Murrills Thanks for the suggestion. Maybe it helped? With your suggestion I was able to add a few more lines of copy-pasta without getting errors, but I still do reach an error near the end.

import Mathlib.Algebra.Order.Hom.Basic

open Lean Meta Qq Mathlib Meta Positivity

/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
@[positivity _]
def evalMap : PositivityExt where eval {u₃ β} zβ pβ e := do
  let .app (.app c' f') a' ← withReducible (whnf e) | throwError "not NonnegHomClass"
  let ⟨u₂, α, a⟩ ← inferTypeQ' a'
  let ⟨u₁, F, f⟩ ← inferTypeQ' f'
  have c : Q($F → $α → $β) := c'
  let _e_eq : $e =Q $c $f $a := ⟨⟩
  let _a ← synthInstanceQ (q(NonnegHomClass $F $α $β) : Q(Type max (max u₁ u₂) u₃))
  assertInstancesCommute
  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ c q(FunLike.coe) -- error here
  pure (.nonnegative q(map_nonneg $f $a))

[Heather Macbeth]

The error is

invalid match-expression, type of pattern variable '_f_eq' contains metavariables
  «$c» =Q FunLike.coe

[Thomas Murrills]

Hmm, I played around with it for a while—I was able to resolve the metavariable error (I suspected outparams) by synthesizingQ an instance of FunLike $F $α (fun a => $β), haveing them into the context as above, and giving arguments explicitly to FunLike.coe, but at the cost of recovering the original error! 🙃

[Heather Macbeth]

Following Thomas' idea that the outparams might be causing extra complications, I tried to write a positivity extension for a situation where there is a similar "guess-the-type" Qq problem but there are no outparams. This still fails:

import Mathlib.Topology.MetricSpace.Basic

theorem dist_nonneg'' [PseudoMetricSpace α] (x y : α) : 0 ≤ dist x y := dist_nonneg
-- convenience version with arguments explicit

open Lean Meta Qq Function Mathlib Meta Positivity

/-- Extension for the `positivity` tactic: distances are nonnegative. -/
@[positivity Dist.dist _ _]
def evalDist : PositivityExt where eval {_ _} _zα _pα e := do
  let .app (.app f a') b ← withReducible (whnf e) | throwError "not dist · ·"
  let ⟨u, α, a⟩ ← inferTypeQ' a'
  let _a ← synthInstanceQ (q(PseudoMetricSpace $α) : Q(Type u))
  let _b ← synthInstanceQ (q(Dist $α) : Q(Type u))
  have b : Q($α) := b
  have f : Q($α → $α → ℝ) := f
  have e : Q(ℝ) := e
  let _e_eq : $e =Q $f $a $b := ⟨⟩
  assumeInstancesCommute
  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u) f q(@Dist.dist $α $_b)
  pure (.nonnegative q(dist_nonneg'' $a $b))