Session types are broken in CBV mode

[thwfhk]

It seems that the safety of session types is broken due to the existence of Axiom K in the default call-by-value mode. We can write the following well-typed program

forkLinearWrapper : forall {s : Protocol} . () -> (LChan s -> ()) -> LChan (Dual s)
forkLinearWrapper () f = forkLinear f

test : forall {s : Protocol} . (LChan s -> ()) [] -> (LChan (Dual s)) []
test [f] = [forkLinearWrapper () f]

sender : LChan (Send Int End) -> ()
sender c =
  let c' = send c 42 in
  close c'

receiver : LChan (Recv Int End) -> Int
receiver c =
  let (i, c') = recv c in
  let () = close c' in
  i

main : Int
main = let [ch] = test [sender] in receiver ch + receiver ch

which gets stuck:

Granule> main
thread blocked indefinitely in an MVar operation

We can change the definition of test to the following still well-typed version

axiomk : forall {a : Type, b : Type} . (a -> b) [] -> a [] -> b []
axiomk [f] [x] = [f x]

test : forall {s : Protocol} . (LChan s -> ()) [] -> (LChan (Dual s)) []
test [f] = axiomk [forkLinearWrapper ()] [f]

which gives us a different runtime error:

Granule> main
Bug in Granule. Trying to fork: [\( internal1 : LChan (Send Int End)) -> 
    (case ((,) ())  internal1 of
      (,) _ c`0 -> let c'`1 = (send c`0) 42 in close c'`1)]
CallStack (from HasCallStack):
  error, called at src/Language/Granule/Interpreter/Eval.hs:787:15 in granule-interpreter-0.9.4.0-LnVThkA1TJl3beGnwGjlFQ:Language.Granule.Interpreter.Eval

Note that using forkLinearWrapper is necessary, because Granule has some existing mechanism to avoid the issue of Axiom K in CBV mode (probably the resourceAllocator predicate in the slides? I didn't find the corresponding paper). For instance, the following program is ill-typed.

test : forall {s : Protocol} . (LChan s -> ()) [] -> (LChan (Dual s)) []
test [f] = [forkLinear f]

Granule> :l axiomk.gr 
Unpromotable error: axiomk.gr:10:12:
Cannot promote a value of type `(LChan (Dual s)) [(0 : Ext Nat)..∞]` in call-by-value mode.

However, the existing mechanism is quite fragile; it can be easily broken by wrapping resourceAllocators in other functions.