Unsafe modification of val

[Theodus]

This program shows a modification to a val Array as if it was an iso reference.

class iso T
  var data: (Array[I64] val | Array[I64] iso) // iso <: val -> Array[I64] val

  new create() =>
    data = recover iso Array[I64] end

  new from(array: Array[I64] val) =>
    data = array

  fun ref push(v: I64) =>
    try
      (data as Array[I64] iso).push(v)
      @printf[None]("iso push\n".cstring())
    else
      data = recover iso data.clone() .> push(v) end
      @printf[None]("val push\n".cstring())
    end

actor Main
  new create(env: Env) =>
    let a = recover val [as I64: 1; 2; 3] end
    let t = T.from(a)
    t.push(4)
    t.push(5)
    env.out.print(a.size().string())
    env.out.print(t.data.size().string())

Expected output:

val push
iso push
3
5

Actual output:

iso push
iso push
5
5

http://pony-playpen.lietar.net/?gist=0f866ad477ff1e3131acc0ee72c9d637

[jemc]

Matches that are based only on capability are supposed to be disallowed - for exactly this reason, you're not supposed to be able to pattern-match on a (Foo val | Foo iso).

We need to find out why this safety mechanism is not kicking in - maybe it's because the example is using as instead of match, and is somehow bypassing that match check, or maybe the check is being bypassed for some other reason.

[Theodus]

The same thing happens when you replace var data: (Array[I64] val | Array[I64] iso) with
var data: Array[I64] val. Shouldn't it be possible to check if a val reference is actually iso?

[Praetonus]

This is coming from the as sugar.

c as C iso

The above expression is sugared to

try
  match c
  | let c': C iso! => consume ! c'
  else
    error
  end
end

The consume ! is a special construct allowed only in compiler sugar. It means that the operand unaliasing is "raw", e.g. iso! (tag) becomes iso, which is forbidden in a normal consume because tag -> iso is unsafe. The result type of the match is then C iso instead of C iso^ in a classic match/consume scheme.

I don't really see why as is behaving that way, since the resulting syntax can be convoluted (for example, to consume and match on an iso at the same time, consume c as C iso^ must be used instead of a more simple consume c as C iso). I think the solution for both the unsafeness and the strange syntax is to use a more straightforward sugar and to remove the consume ! rule altogether.

try
  match c
  | let c': C iso => consume c'
  else
    error
  end
end

[jemc]

Shouldn't it be possible to check if a val reference is actually iso?

Not at runtime. Capabilities don't exist at runtime (zero-cost abstraction), so you can't match on them. In this case we need a compile time error stopping you from doing any such matching at all, since matching is done at runtime.

[Theodus]

I see

[jemc]

@Theodus If you need to do something like this (support (Foo iso | Foo val) in your code), you should probably be using type parameters instead, so you can distinguish the two at compile time, using iftype.

Obviously this ticket is still a bug, but once it's fixed you still won't be able to do what you were trying to do, without moving to using type parameters.

[Theodus]

Yeah, I may end up needing to do that. Thanks!