sharable mode annotation might be broken for arrow types

[kikofernandez]

In the current development version of Encore, I keep getting the error:

"test.enc" (line 13, column 5)
Cannot use linear type 'X' as type argument. Type parameter 'a' requires the type to have sharable mode
In expression: 
  appl(fun (var y : X) => consume y, consume x)

For something that I think should typecheck. The minimum code to reproduce this errors is given below:

import ParT.ParT

fun appl[sharable a, sharable b](fn : a -> b, x: a): b
  fn(consume x)
end

linear class X
end

active class Main
  def main(): unit
    var x = new X
    appl(fun (var y: X) => consume y, consume x)
  end
end

Am I doing something wrong or did I find a bug?

[kikofernandez]

It seems like nested types have problems with the sharable too. For instance, the next example throws the error:

"test.enc" (line 14, column 5)
Cannot use linear type 'X' as type argument. Type parameter 'a' requires the type to have sharable mode
In expression: 
  appl(consume x)

when I thought that it would work. Find the code below:

fun appl[sharable a](x: Maybe[Maybe[a]]): Maybe[a]
  match x with
    case Nothing => Nothing
    case Just(y) => y
  end
end

linear class X
end

active class Main
  def main(): unit
    var x = Just(Just(new X))
    appl(consume x)
  end
end

[kikofernandez]

I also saw that an option type that wraps a linear type doesn't seem to play at all with the match expression, i.e. I am not allowed to extract one of the values to treat the value linearly.

A test case that proves this is given below:

fun foo[linear t](var x: t): unit
  ()
end

fun appl(var x: Maybe[X]): unit
  match x with
    case Nothing => ()
    case Just(y) => foo(consume y)
  end
end

linear class X
end

active class Main
  def main(): unit
    ()
  end
end

I get the error:

"test.enc" (line 8, column 25)
Cannot consume immutable variable 'y'
In expression: 
  consume y
In expression: 
  foo(consume y)
In function 'appl' of type 'unit'

[EliasC]

Am I doing something wrong or did I find a bug?

This is not a bug. The sharable mode abstracts over active and read (locked would be included here as well if we had it). You are sending it something linear (note that the error is in main, not in appl), which could break linearity if the function duplicated it:

fun dup[sharable t](x : t) : (t, t)
  (x, x)
end

fun app[sharable t](fn : t -> (t, t), x) : (t, t)
  fn(x)
end

app(dup, new X)

Your second example has the same problem, and your last example is related to #770. The latter could be fixed by supporting non-destructive consumes (i.e. by statically checking that we don't duplicate a linear thing).

[kikofernandez]

You are right. I think the message mislead me to believe there was something wrong:

Cannot use linear type 'X' as type argument. Type parameter 'a' requires the type to have sharable mode

when I read the Type parameter 'a' ... I thought it was related to the function.