Inconsistent behaviour of linear quantity on function definitions

[buzden]

Steps to Reproduce

Consider the following function:

1 f : (1 _ : Nat) -> Nat
f x = S x

It doesn't really matter what exactly it is doing, the important thing is that it's declared with 1-quantity.

We can successfully pass this function to other functions requiring linear context:

fi : (1 f : (1 _ : Nat) -> Nat) -> Nat -> Nat
fi f x = let fx = f x in fx

fi_f : Nat -> Nat
fi_f = fi f -- Typechecks

But we can't pass this function when the outer context is not linear:

fj : (f : (1 _ : Nat) -> Nat) -> Nat -> Nat
fj f x = let fx = f x in fx

fj_f : Nat -> Nat
fj_f = fj f -- Does not typecheck

This fails with

Error: While processing right hand side of fj_f. Trying to use linear name Main.f in non-linear context.

.../Function1.idr:37:11--37:12
    |
 37 | fj_f = fj f
    |           ^

Well, why not, f is declared with 1.

But at the same time we can use this f twice in the same function:

useTwice : Nat -> Nat -> Nat
useTwice x y = let fx = f x
                   fy = f y
               in ?whatever

And when we ask for the type of the hole, we see that 1-quantity of f gave its quantity to the results of f invocations.

   y : Nat
   x : Nat
 1 fx : Nat
 1 fy : Nat
------------------------------
whatever : Nat

So, function f defined with 1-quantity behaves as if we can use it as many times as we want (from zero to infinity) but if we use it, we must use its results exactly once. That is, as if 1-quantity belongs to the result of this function but not to the definition itself.

By the way, I personally consider nice to be able to express such property for functions that produce some resources, modeled with linear types.

However, if we do let ff = f in ?foo and look to the context of ?foo hole, we'll see

 1 ff : Nat -> Nat
------------------------------

i.e. that we must use ff exactly once. That is, this rule above applies not to the result of this function but to anything it's influences on.

This, by the way, regards not only to top-level definitions. Consider this definition:

local : Nat -> Nat
local x = let 1 foj : (1 _ : Nat) -> Nat
              foj x = S x in
          let 1 foy : (1 _ : Nat) -> Nat
              foy = foj in
          --let 1 fox = foj in
          x
  where
    1 foo : (1 _ : Nat) -> Nat
    foo x = S x

This definition typechecks. However if we uncomment the commented line, it does not typecheck, because linear fox is not used. But the fact that local functions are defined with 1-quantity does not make them to be used exactly once, this regards only to their usages.

Expected Behavior

Linear quantity of the argument means (afaik) that this argument is used exactly once if the result of the function is used exactly once. But it's unclear to me what are conditions of usage for top-level definitions. And it's unclear why local functions are treated differently when they are defined at full function definition or as an alias to partially applied functions.

I'd expect only one thing to hold: either quantity of a top-level function relates to the definition itself or to its result.

In the first case I would expect inability to use f function twice. And in this case it's unclear for me what would be the space on where it's counted -- function, module or the whole program? In either cases, there's a question of using such function exactly once. However, the behaviour is that when we have fx = f x, fx variable gets 1-quantity leads to the thought

In the second case it is okay that when doing let fx = f x, fx variable gets 1-quantity, but also I would expect an ability to use f in a non-linear context like passing to the fj_f function.

Observed Behavior

Functions defined with 1-quantity (no matter where they are defined) can be used as many times as we want for applying them, but their values and results of application must be used in only a linear context.

[gallais]

I am not sure what the point of top level functions with quantity 1 is but this does appear to be inconsistent.

[joelberkeley]

I'd have thought top level functions with quantity 1 should only be possible if private, and used exactly once in the module (though I can't imagine why you'd want one). If they're public, there's no way for the compiler to know how many times it's used, so it should balk.

[joelberkeley]

I think this means that a top-level linear object can only be used within the same module as a non-exported main function.