[Agda] question about with

[Dan Licata]

I have a question about refining goals using with.  Consider the
following example:

  data Nat : Set where
    Z : Nat
    S : Nat -> Nat

  plus : Nat -> Nat -> Nat
  plus n Z = n
  plus n (S m) = S (plus n m)

  data Id : Nat -> Nat -> Set where
    Refl : {n : Nat} -> Id n n

  plus-lh-z : (n : Nat) -> Id (plus Z n) n
  plus-lh-z Z = Refl
  plus-lh-z (S n) with (plus Z n) | plus-lh-z n 
  ...                | .n         | Refl = Refl

This works fine.  Here, I'm using the with to replace instances of 
(plus Z n) with n in the context and goal, which is justified by the 
recursive call.  After this replacement, the goal is easy to prove.  

However, suppose I wanted to go the other way:

  plus-lh-z' : (n : Nat) -> Id (plus Z n) n
  plus-lh-z' Z = Refl
  plus-lh-z' (S n) with n           | plus-lh-z' n 
  ...                 | .(plus Z n) | Refl = ?

In this case, agda complains that 

  w != plus Z w of type Nat
  when checking that the pattern Refl has type Id (plus Z w) w

I don't understand why this refinement fails, when the above one
succeeded.

Of course, the second refinement isn't actually helpful in this case,
but I have an analogous example where this is the direction I want to go
(i.e., the goal type has the simple expression (analogous to n) but the
term I want to write has the complicated expression (analogous to (plus
Z n)) in its type, so I want to replace simple with complicated in the
goal).  I also ran into an example where neither option worked.  Both of
these are buried in a somewhat large development, but I can provide a
tar if that would be helpful.

I know how to work around this using a helper function (e.g., subst)
instead, but is there a way to do this using with?

Thanks!
-Dan