Thats interesting. I don't quite understand how that would work.

So can you work around that requirement by just going:

    if false 
    then <use my type> 
    else <do my things>

Technically it is used exactly once, but really it will never be used..

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

That wouldn't work, because the value must be used in all possible control paths. In this case, both the 'then' and 'else' branch would have to use the value.

Just curious, what is considered as 'using' the value?

Passing it as a parameter to a function or returning it

Or applying it if that value is a function. I believe the broader definition would be that it has to appear in an "evaluated" term.