Linearity

Linearity.md

In Granule (the base calculus is linear) these two tests violate linearity:

data Foo a = Bar a

test1 : Foo Int -> (Int , Int)
test1 (Bar mustUseOnce) = (mustUseOnce, mustUseOnce)

test2 : Foo Int -> Int
test2 (Bar mustUseOnce) = 42

yields

Linearity error: sandbox/access.gr:73:27:
Linear variable `mustUseOnce` is used more than once.

Linearity error: sandbox/access.gr:76:1:
Linear variable `mustUseOnce` is never used.

However in Idris, this violation of linearity is not caught by the type checker?

data Foo : (a : Type) -> Type where 
     Bar : (1 x : a) -> Foo a
    
test1 : Foo Int -> (Int,Int) 
test1 (Bar mustUseOnce) = (mustUseOnce, mustUseOnce)

test2 : Foo Int -> Int
test2 (Bar mustUseOnce) = 42

yields no error even though linearity is violated?

The Granule code can equally be expressed as (using modal boxing/unboxing):

data Foo a = Bar (a[1])

test1 : Foo Int -> (Int , Int)
test1 (Bar [mustUseOnce]) = (mustUseOnce, mustUseOnce)

test2 : Foo Int -> Int
test2 (Bar [mustUseOnce]) = 42

yields

Falsifiable theorem: sandbox/access.gr:82:1:
  When checking `test1`, expected 1 uses, but instead there are (2 : Nat) actual uses.

Falsifiable theorem: sandbox/access.gr:85:1:
  When checking `test2`, expected 1 uses, but instead there are (0 : Nat) actual uses.

In idris by default the function space is unrestricted.
You meant to write:

test1 : (1 _ : Foo Int) -> (Int,Int)
test1 (Bar mustUseOnce) = (mustUseOnce, mustUseOnce)

test2 : (1 _ : Foo Int) -> Int
test2 (Bar mustUseOnce) = 42