Unexpected linearity constraint and unification failure in dependent case results

[spcfox]

Steps to Reproduce

The following code fails to compile. The compiler incorrectly infers a linear quantity for the argument w

foo : (u : ()) -> case u of () => (w : Unit) -> ()
foo () w = ()

Attempting to fix this by explicitly setting a quantity (e.g., 0) also fails:

bar : (u : ()) -> case u of () => (0 w : Unit) -> ()
bar () w = ()

Expected Behavior

Successful typecheck

Observed Behavior

Error: While processing right hand side of foo. There are 0 uses of linear name w. 

Main:2:12--2:14
 1 | foo : (u : ()) -> case u of () => (w : Unit) -> ()
 2 | foo () w = ()
                ^^

Suggestion: linearly bounded variables must be used exactly once.
Error: While processing left hand side of bar. When unifying:
    (0 _ : ()) -> ()
and:
    ?argTy -> ?retTy
Mismatch between: (0 _ : ()) -> () and ?argTy -> ?retTy.

Main:5:1--5:9
 1 | foo : (u : ()) -> case u of () => (w : Unit) -> ()
 2 | foo () w = ()
 3 | 
 4 | bar : (u : ()) -> case u of () => (0 w : Unit) -> ()
 5 | bar () w = ()
     ^^^^^^^^