Linear "types" are completely unsound

[jaens]

Linear types are generally attached to a value, not separate proof objects.

Otherwise, you get trivial unsoundness like:

1. You can free an object with the proof from another object.
2. You can consume the proof but still access the object afterwards.

Example:

from pythoc import compile, linear, consume, void, ptr, i8, i32, struct
from pythoc.libc.stdlib import malloc, free

# Allocator returns resource + linear proof
@compile
def lmalloc(size: i32) -> struct[ptr[i8], linear]:
    print("Allocating", size)
    return malloc(size), linear()

# Only the paired deallocator can consume the proof
@compile
def lfree(ptr: ptr[i8], prf: linear) -> void:
    print("Freeing", ptr)
    consume(prf)  # Proof consumed - resource NOT released
    free(ptr)

@compile
def safe_usage() -> void:
    mem, prf = lmalloc(100)
    mem2, prf2 = lmalloc(200)
    print("Hello from safe_usage")
    lfree(mem, prf2)
    lfree(mem2, prf) # Freeing with the wrong proof
    # NO compile error
    print("Done")

safe_usage()

Also this seems to be very miscompiled and outputs:

Allocating ValueRef(kind=address, type=i32, +addr)
Freeing ValueRef(kind=address, type=ptr[i8], +addr)
Hello from safe_usage
Done

so it's missing the prints from the second malloc and the prints are in the wrong order?