Instance synthesis fails with a match expression

[lzy0505]

/-- error: (match ?b with
  | true => ?Q
  | false => ?Q) ⊢
  ?Q is not an entailment -/
#guard_msgs in
example [BI PROP] (Q : PROP) : Q ⊢ Q := by
  iintro HQ
  have H: (∀ b (Q: PROP), (match b with | true => iprop(Q) | false => iprop(Q)) ⊢ Q) := by sorry
  iapply H

This example failed at iapply H.
But the iapply works if I replace the match expression with (if b == true then iprop(Q) else iprop(Q)).

The problem seems to be at this line:

iris-lean/src/Iris/ProofMode/SynthInstance.lean

Line 86 in 1bed579

let instances ← SynthInstance.getInstances mvarType

Is this an upstream bug?

cc @MackieLoeffel

[MackieLoeffel]

This part of the IPM synthesis is taken from the standard type class search. I think this is a limitation of the standard lean TC synthesis implementation (not sure if a bug or on purpose).

See this example:

class Test (n : Nat)

instance : Test 1 := ⟨⟩

variable (n : Nat)
-- works
#synth Test 1
-- fails
#synth Test (match n with | 0 => 1 | _ => 1)
-- fails
#synth Test (if n == 0 then 1 else 1)

[lzy0505]

I think this example reproduces the issue better:

class Test (n : Nat)

instance {n} : Test (n) := ⟨⟩

-- works
#synth Test 1
-- fails
#synth Test (match ?_ with | 0 => 1 | _ => 1)
-- works
#synth Test (if ?_ == 0 then 1 else 1)

[btj-h]

I bumped into this as well. I created an upstream issue.