A function like `closeFile` will consume the linear value but not produce a new linear value - it returns `Unit`. It does this via a destructuring assignment (For example, File would be a record type with a field named handle).

    function closeFile (file : File) : Unit is
        let { handle } := file;    (* This consumes the file *)
        fclose(handle);
        return nil;
    end;

A module will usually provide opaque types, with the actual definitions encapsulated by an implementation file, similar to how C and C++ do it. Users of this library don't know what is in the type `File`, so they're unable to use the destructuring assignment themselves - so their only option is to call `closeFile`, or the compiler will complain that the linear value is not consumed.

You can of course, call `closeFile` from `g`, and then it's fine to make `g` return Unit.

    function g (file : File) : Unit is
        let file0 := (* do something with file *);
        return closeFile(file0);
    end;

The compiler actually enforces this. If g takes a `file` argument and returns Unit, then it MUST call `closeFile`. Failure to do so won't compile.

For a real example, check how the RootCapability type is defined in `builtin/Pervasive`[1]. It's declared as an opaque type in the .aui file, along with `surrenderRoot`. This is all the user of the type knows about it.

    type RootCapability : Linear;

    function surrenderRoot(cap: RootCapability): Unit;

In the .aum file both the type and surrenderRoot are actually defined.

    record RootCapability: Linear is
        value: Unit;
    end;

    function surrenderRoot(cap: RootCapability): Unit is
        let { value: Unit } := cap;
        return nil;
    end;

[1]:https://github.com/austral/austral/tree/master/lib/builtin