~q pattern match does not respect return

[Vtec234]

Consider the snippet below. I would expect the two functions foo₁ and foo₂ to be equivalent and both to work, however foo₁ fails to elaborate with a type error.

import Lean
import Qq

open Lean Meta
open Qq

def foo₁ (T : Q(Type)) (t : Q($T)) : MetaM Q($T) := do
  if let ~q(Prop) := T then
    /- type mismatch
      q(True)
    has type
      Q(Prop) : Type
    but is expected to have type
      PUnit : Type -/
    return q(True)
  return q($t)

def foo₂ (T : Q(Type)) (t : Q($T)) : MetaM Q($T) := do
  match T with
  | ~q(Prop) => return q(True)
  | _ => return q($t)

[eric-wieser]

I think the return is operating at the wrong scope:

def foo₁ (T : Q(Type)) : MetaM Bool := do
  if let ~q(Prop) := T then
    return ()
  return true

It's returning from the inner macro, not the outer do block

[eric-wieser]

Here's a slightly more damning example:

import Qq
open Qq Lean

def foo₂ (T : Q(Type)) : MetaM Bool := do
  let x : Unit ← match T with
    | ~q(Prop) => return true
    | _ => return true
  return false

#eval foo₂ q(Nat)  -- false
#eval foo₂ q(Int)  -- false

[eric-wieser]

I added a lot of test-cases in #27

[eric-wieser]

A possible solution is discussed at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Converting.20from.20doSeq.20to.20doSeqItem/near/402223969