Passing literal Symbol/Integer as generic fails static type check

[andrew-cc]

require 'rdl'
require 'types/core'

class A
  extend RDL::Annotate

  type '(Array<Symbol>) -> nil', typecheck: :later
  def f(xs)
  end

  type '() -> nil', typecheck: :later
  def g
    f(%i[bar])
  end
end

RDL.do_typecheck :later
A.new.g

Gives error:

/usr/local/bundle/gems/rdl-2.1.0/lib/rdl/typecheck.rb:158:in `error':  (RDL::Typecheck::StaticTypeError)
tmp.rb:43:5: error: argument type error for instance method `A#f'
Method type:
        (Array<Symbol>) -> nil
Actual arg type:
      (Array<:bar>)
tmp.rb:43:     f(%i[bar])
tmp.rb:43:     ^~~~~~~~~~

This also happens with Integer. It doesn’t, however, happen with literal Strings, nor does it happen when unwrapping the generic (i.e. if the method was (Symbol) -> nil and called accordingly). Additionally, Array<%any> never appears to work. This is also likewise an issue for Hash value (but not key) generic.

If static checking is skipped, runtime checking has no issues.

If RDL’s types/core is not required and instead do RDL.type_params Array, [:t], :all?, variance: [:+], then it works. This seems odd, since :bar is an instance of Symbol, not a subtype. (I’m also unsure how to implement this workaround concisely as I cannot require types/core and re-call type_params with a different variance.)

This was tested on both v2.1.0 and the latest dev branch.

Is there something I’m missing here? As-is, it seems not possible to statically check a function which takes a Array<Symbol> or Array<Integer>.

[jeffrey-s-foster]

Right, this is the same issue as #41, but for arrays instead of hashes. RDL works this way to be sound (meaning, RDL will not accept any program with type errors), but it can be annoying in practice. The solution is to change the variance, as you did. Probably RDL should have a global configuration option to enable the unsound behavior for arrays and hashes. Does that sound reasonable?

To see the soundness issue, suppose a has type Array<:bar> and b has type Array<Symbol>. Then suppose we set b = a, which is only allowed with covariant subtyping (:+). Then the problem is that we could set b[0] = :foo. But now a[0] == :foo and yet a[0] has type :bar.

In the particular example you have above, f does not write to its argument so the issue can't happen. But RDL can't tell that from the types. (We could add a const annotation to RDL to capture this case but that would have pervasive effects and would probably be hard to work with.)