[maemre]

Linear type systems often enforce that requirement by saying both branches need to use exactly the same linear values (or consume the same resources). So your example would be rejected by the type system. For example, the following function would not type check in a linearly-typed language because then branch is using x while else branch is not using x.

    -- Using Haskell-like syntax, '-o' is linear arrow, i.e. lollipop
    foo : Int -o Int -o Int
    foo x y = if y < 0 then x else 0