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?

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