tupl-tufts / rdl

Types, type checking, and contracts for Ruby
BSD 3-Clause "New" or "Revised" License
602 stars 38 forks source link

`var_type :@ary, "Array"` prohibits any access to the instance variable #76

Closed mame closed 5 years ago

mame commented 6 years ago

What should I do?

require "rdl"

class Foo
  extend RDL::Annotate
  var_type :@ary, "Array"

  type "() -> %any", typecheck: :now
  def foo
    @ary = []
  end
end
Traceback (most recent call last):
    11: from t.rb:3:in `<main>'

*snip*

     1: from /home/mame/local/lib/ruby/gems/2.5.0/gems/rdl-2.1.0/lib/rdl/typecheck.rb:1079:in `tc_vasgn'
/home/mame/local/lib/ruby/gems/2.5.0/gems/rdl-2.1.0/lib/rdl/typecheck.rb:158:in `error':  (RDL::Typecheck::StaticTypeError)
t.rb:9:5: error: incompatible types: `[]' can't be assigned to variable of type `Array'
t.rb:9:     @ary = []
t.rb:9:     ^~~~~~~~~

Another case:

require "rdl"

class Foo
  extend RDL::Annotate
  var_type :@ary, "Array"

  type "() -> %any", typecheck: :now
  def foo
    @ary << 1
  end
end
$ ruby -Ilib t.rb 
Traceback (most recent call last):
    16: from t.rb:3:in `<main>'

*snip*

     1: from /home/mame/local/lib/ruby/gems/2.5.0/gems/rdl-2.1.0/lib/rdl/typecheck.rb:1261:in `tc_send_one_recv'
/home/mame/local/lib/ruby/gems/2.5.0/gems/rdl-2.1.0/lib/rdl/typecheck.rb:158:in `error':  (RDL::Typecheck::StaticTypeError)
t.rb:9:5: error: no type information for instance method `Array#<<'
t.rb:9:     @ary << 1
t.rb:9:     ^~~~~~~~~
mame commented 6 years ago

Sorry, I noticed that adding require "types/core" solves the latter case.

mame commented 6 years ago

I guess that in the former case, the array literal is considered as a type of 0-member tuple, but I have not found the solution yet.

mckaz commented 5 years ago

You are correct-- in the former case, the literal is considered as tuple type [], which for soundness reasons is not considered a subtype of Array (see issue #64 for a more detailed explanation). Currently, you can solve this issue by type casting [], i.e., @ary = RDL.type_cast([], "Array").

The comp-types branch of RDL uses type-level computations to bring a greater level of precision to various library types, including Arrays. It greatly reduces the need for type casts like the aforementioned one. We'll be merging that branch with master very shortly.