Rejection of erased irrefutable patterns after with

[spcfox]

Steps to Reproduce

data Y : Bool -> Type where
  T : Y True
  F : Y False

failing "While processing left hand side of with block in foo. Can't match on T (Erased argument)"
  foo : {f : _} -> (b : Bool) -> (0 _ : Y (f b)) -> ()
  foo b y with (f b)
    foo b T | True = ()
    foo b F | False = ()

But it works with a nested function:

foo : {f : _} -> (b : Bool) -> (0 _ : Y (f b)) -> ()
foo b y = go (f b) y
  where
    go : (b : Bool) -> (0 _ : Y b) -> ()
    go True T = ()
    go False F = ()

The types in context are correct:

foo : {f : _} -> (b : Bool) -> (0 _ : Y (f b)) -> ()
foo b y with (f b)
  foo b y | True = ?hole
  foo b y | False = ()

Main> :t hole
   f : Bool -> Bool
 0 y : Y True
   b : Bool
------------------------------
hole : ()

Expected Behavior

Successful compilation

Observed Behavior

Error: While processing left hand side of with block in foo. Can't match on T (Erased argument).

Main:7:9--7:10
 3 |   F : Y False
 4 | 
 5 | foo : {f : _} -> (b : Bool) -> (0 _ : Y (f b)) -> ()
 6 | foo b y with (f b)
 7 |   foo b T | True = ()
             ^