diff --git a/Gemfile b/Gemfile index ff77e12ef..1dfea64bf 100644 --- a/Gemfile +++ b/Gemfile @@ -12,3 +12,6 @@ end gem 'minitest-slow_test' gem "debug", require: false, platform: :mri + +# gem "rbs", path: File.join(__dir__, "../rbs") +# gem "rbs", path: "../rbs" diff --git a/lib/steep/subtyping/check.rb b/lib/steep/subtyping/check.rb index 5dff60815..263254152 100644 --- a/lib/steep/subtyping/check.rb +++ b/lib/steep/subtyping/check.rb @@ -783,18 +783,21 @@ def check_generic_method_type(name, relation) def check_constraints(relation, variables:, variance:) checker = Check.new(builder: builder) - constraints.solution( - checker, + context = Constraints::Context.new( variance: variance, - variables: variables, self_type: self_type, instance_type: instance_type, class_type: class_type ) - Success(relation) - rescue Constraints::UnsatisfiableConstraint => error - Failure(relation, Result::Failure::UnsatisfiedConstraints.new(error)) + solution = Constraints.solve(constraints, checker, context) + + case solution + when Interface::Substitution + Success(relation) + else + Failure(relation, Result::Failure::UnsatisfiedConstraints.new(solution)) + end end def check_method_type(name, relation) diff --git a/lib/steep/subtyping/constraints.rb b/lib/steep/subtyping/constraints.rb index 4da9bfa36..4f1bb541f 100644 --- a/lib/steep/subtyping/constraints.rb +++ b/lib/steep/subtyping/constraints.rb @@ -73,14 +73,14 @@ def initialize(var:, sub_type:, super_type:, result:) end attr_reader :dictionary - attr_reader :vars + attr_reader :generics_upper_bounds def initialize(unknowns:) @dictionary = {} - @vars = Set.new + @generics_upper_bounds = {} unknowns.each do |var| - dictionary[var] = [Set.new, Set.new, Set.new] + dictionary[var] = [Set.new, Set.new] end end @@ -88,21 +88,12 @@ def self.empty new(unknowns: []) end - def add_var(*vars) - vars.each do |var| - self.vars << var - end - - unless Set.new(vars).disjoint?(unknowns) - raise UnsatisfiedInvariantError.new( - reason: UnsatisfiedInvariantError::VariablesUnknownsNotDisjoint.new(vars: vars), - constraints: self - ) - end + def add_generics_upper_bound(var, type) + generics_upper_bounds[var] = type end - def add(var, sub_type: nil, super_type: nil, skip: false) - subs, supers, skips = dictionary[var] + def add(var, sub_type: nil, super_type: nil) + subs, supers = dictionary[var] if sub_type.is_a?(AST::Types::Logic::Base) sub_type = AST::Builtin.bool_type @@ -115,13 +106,11 @@ def add(var, sub_type: nil, super_type: nil, skip: false) if super_type && !super_type.is_a?(AST::Types::Top) type = eliminate_variable(super_type, to: AST::Types::Top.new) supers << type - skips << type if skip end if sub_type && !sub_type.is_a?(AST::Types::Bot) type = eliminate_variable(sub_type, to: AST::Types::Bot.new) subs << type - skips << type if skip end super_fvs = supers.each_with_object(Set.new) do |type, fvs| @@ -164,10 +153,10 @@ def eliminate_variable(type, to:) AST::Types::Intersection.build(types: types) end when AST::Types::Var - if vars.member?(type.name) - to - else + if unknown?(type.name) type + else + to end when AST::Types::Tuple AST::Types::Tuple.new( @@ -204,12 +193,8 @@ def empty? dictionary.keys.empty? end - def upper_bound(var, skip: false) - if skip - upper_bound = upper_bound_types(var) - else - _, upper_bound, _ = dictionary[var] - end + def upper_bound(var) + upper_bound = upper_bound_types(var) case upper_bound.size when 0 @@ -221,7 +206,7 @@ def upper_bound(var, skip: false) end end - def lower_bound(var, skip: false) + def lower_bound(var) lower_bound = lower_bound_types(var) case lower_bound.size @@ -236,73 +221,118 @@ def lower_bound(var, skip: false) Context = _ = Struct.new(:variance, :self_type, :instance_type, :class_type, keyword_init: true) - def solution(checker, variance: nil, variables:, self_type: nil, instance_type: nil, class_type: nil, context: nil) - if context - raise if variance - raise if self_type - raise if instance_type - raise if class_type - - variance = context.variance - self_type = context.self_type - instance_type = context.instance_type - class_type = context.class_type + def self.solve!(constraints, checker, context) + solution = solve(constraints, checker, context) + + if solution.is_a?(Interface::Substitution) + solution + else + raise solution + end + end + + def self.solve(constraints, checker, context) + subst = Interface::Substitution.empty + + double_end_constraints = {} #: Hash[Symbol, Array[Relation[AST::Types::t]]] + no_constraints = [] #: Array[Symbol] + + constraints.dictionary.each_key do |var| + constraint = constraints.constraint(var) + + case constraint + when Array + double_end_constraints[var] = constraint + when nil + no_constraints << var + else + type = constraint.subst(subst) + subst.add!(var, type) + end end - vars = [] #: Array[Symbol] - types = [] #: Array[AST::Types::t] - - dictionary.each_key do |var| - if variables.include?(var) - if has_constraint?(var) - relation = Relation.new( - sub_type: lower_bound(var, skip: false), - super_type: upper_bound(var, skip: false) - ) - - checker.check(relation, self_type: self_type, instance_type: instance_type, class_type: class_type, constraints: self.class.empty).yield_self do |result| - if result.success? - vars << var - - upper_bound = upper_bound(var, skip: true) - lower_bound = lower_bound(var, skip: true) - - type = - case - when variance.contravariant?(var) - upper_bound - when variance.covariant?(var) - lower_bound - else - if lower_bound.level.join > upper_bound.level.join - upper_bound - else - lower_bound - end - end - - types << type - else - raise UnsatisfiableConstraint.new( - var: var, - sub_type: result.relation.sub_type, - super_type: result.relation.super_type, - result: result - ) - end + if double_end_constraints.empty? + untyped_subst = Interface::Substitution.build(no_constraints, no_constraints.map { AST::Types::Any.new}) + return subst.merge!(untyped_subst) + end + + additional_relations = {} #: Hash[Symbol, Array[Relation[AST::Types::t]]] + double_end_constraints.each do |var, relations| + additional_relations[var] = relations.map do |rel| + rel.map {|ty| ty.subst(subst) } + end + end + + fvs = additional_relations.each_with_object(Set.new) do |(var, relations), fvs| #$ Set[Symbol] + relations.each do |relation| + relation.sub_type.free_variables.each do |fv| + fvs << fv if fv.is_a?(Symbol) + end + relation.super_type.free_variables.each do |fv| + fvs << fv if fv.is_a?(Symbol) + end + end + end + + fvs = fvs & no_constraints + + cs = Constraints.new(unknowns: fvs) + additional_relations.each do |var, relations| + relations.each do |relation| + checker.check(relation, self_type: context.self_type, instance_type: context.instance_type, class_type: context.class_type, constraints: cs).yield_self do |result| + unless result.success? + return UnsatisfiableConstraint.new( + var: var, + sub_type: result.relation.sub_type, + super_type: result.relation.super_type, + result: result + ) end - else - vars << var - types << AST::Types::Any.new end end end - Interface::Substitution.build(vars, types) + solution = solve(cs, checker, context) + if solution.is_a?(Interface::Substitution) + subst.merge!(solution) + + additional_relations.each do |var, relations| + lowest = relations[0].sub_type + upest = relations[-1].super_type + + type = + case + when context.variance.contravariant?(var) + upest + when context.variance.covariant?(var) + lowest + else + if lowest.level.join > upest.level.join + upest + else + lowest + end + end + + subst.add!(var, type.subst(solution)) + end + + subst + else + solution + end end def has_constraint?(var) - !upper_bound_types(var).empty? || !lower_bound_types(var).empty? + constraint(var) ? true : false + end + + def each_unknown_variable(&block) + if block + dictionary.each_key(&block) + else + enum_for :each_unknown_variable + end end def each @@ -317,10 +347,47 @@ def each def to_s strings = each.map do |var, lower_bound, upper_bound| - "#{lower_bound} <: #{var} <: #{upper_bound}" + if ub = generics_upper_bounds.fetch(var, nil) + "#{lower_bound} <: #{var} <: #{upper_bound} (<: #{ub})" + else + "#{lower_bound} <: #{var} <: #{upper_bound}" + end end - "#{unknowns.to_a.join(",")}/#{vars.to_a.join(",")} |- { #{strings.join(", ")} }" + "#{unknowns.to_a.join(",")} |- { #{strings.join(", ")} }" + end + + def constraint(var_name) + upper_bound = upper_bound(var_name) + lower_bound = lower_bound(var_name) + generics_bound = generics_upper_bounds.fetch(var_name, nil) + + if generics_bound + case + when upper_bound.is_a?(AST::Types::Top) && lower_bound.is_a?(AST::Types::Bot) + generics_bound + when upper_bound.is_a?(AST::Types::Top) + [Relation.new(sub_type: lower_bound, super_type: generics_bound)] + when lower_bound.is_a?(AST::Types::Bot) + [Relation.new(sub_type: upper_bound, super_type: generics_bound)] + else + [ + Relation.new(sub_type: lower_bound, super_type: upper_bound), + Relation.new(sub_type: upper_bound, super_type: generics_bound) + ] + end + else + case + when upper_bound.is_a?(AST::Types::Top) && lower_bound.is_a?(AST::Types::Bot) + nil + when upper_bound.is_a?(AST::Types::Top) + lower_bound + when lower_bound.is_a?(AST::Types::Bot) + upper_bound + else + [Relation.new(sub_type: lower_bound, super_type: upper_bound)] + end + end end def lower_bound_types(var_name) @@ -329,16 +396,8 @@ def lower_bound_types(var_name) end def upper_bound_types(var_name) - _, upper, skips = dictionary[var_name] - - case - when upper.empty? - skips - when skips.empty? - upper - else - upper - skips - end + _, upper = dictionary[var_name] + upper end end end diff --git a/lib/steep/type_construction.rb b/lib/steep/type_construction.rb index e854ea8ab..99455076a 100644 --- a/lib/steep/type_construction.rb +++ b/lib/steep/type_construction.rb @@ -3928,7 +3928,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: type_params.each do |param| if ub = param.upper_bound - constraints.add(param.name, super_type: ub, skip: true) + constraints.add_generics_upper_bound(param.name, ub) upper_bounds[param.name] = ub end end @@ -3970,7 +3970,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: if hint.free_variables.subset?(self_type.free_variables) if check_relation(sub_type: method_type.type.return_type, super_type: hint, constraints: constraints).success? method_type, solved, s = apply_solution(errors, node: node, method_type: method_type) do - constraints.solution(checker, variables: fvs, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) end end @@ -4043,7 +4043,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: fvs_.merge(method_type.type.params.free_variables) if method_type.type.params fvs_.merge(method_type.block.type.params.free_variables) if method_type.block.type.params - constraints.solution(checker, variables: fvs_, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type.block or raise @@ -4085,7 +4085,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: if result.success? # Successfully type checked the body method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) do - constraints.solution(checker, variables: type_param_names, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) end method_type = eliminate_vars(method_type, type_param_names) unless solved @@ -4124,7 +4124,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: ) method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) { - constraints.solution(checker, variables: type_param_names, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type = eliminate_vars(method_type, type_param_names) unless solved @@ -4200,7 +4200,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: if nil_given # nil is given ==> no block arg node is given method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) { - constraints.solution(checker, variables: method_type.free_variables, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type = eliminate_vars(method_type, type_param_names) unless solved @@ -4221,14 +4221,14 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: end method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) { - constraints.solution(checker, variables: method_type.free_variables, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type = eliminate_vars(method_type, type_param_names) unless solved end else # Block is not given method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) { - constraints.solution(checker, variables: method_type.free_variables, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type = eliminate_vars(method_type, type_param_names) unless solved end @@ -4238,7 +4238,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: when arg.block_missing? # Block is required but not given method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) { - constraints.solution(checker, variables: method_type.free_variables, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type = eliminate_vars(method_type, type_param_names) unless solved @@ -4255,7 +4255,7 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, arguments: arg.node or raise method_type, solved, _ = apply_solution(errors, node: node, method_type: method_type) { - constraints.solution(checker, variables: method_type.free_variables, context: ccontext) + Subtyping::Constraints.solve!(constraints, checker, ccontext) } method_type = eliminate_vars(method_type, type_param_names) unless solved return_type = method_type.type.return_type @@ -4891,7 +4891,6 @@ def semantically_arrayish_type?(type) var = AST::Types::Var.fresh(:Elem) array = AST::Builtin::Array.instance_type(var) constraints = Subtyping::Constraints.new(unknowns: []) - constraints.add_var(var.name) if (result = check_relation(sub_type: type, super_type: array, constraints: constraints)).success? context = Subtyping::Constraints::Context.new( @@ -4900,14 +4899,7 @@ def semantically_arrayish_type?(type) instance_type: module_context.instance_type, class_type: module_context.module_type ) - - variables = (type.free_variables + [var.name]).filter_map do |name| - case name - when Symbol - name - end - end - subst = constraints.solution(checker, variables: variables, context: context) + subst = Subtyping::Constraints.solve!(constraints, checker, context) type.subst(subst) end diff --git a/sig/steep/subtyping/constraints.rbs b/sig/steep/subtyping/constraints.rbs index b54103c21..56dd8dab9 100644 --- a/sig/steep/subtyping/constraints.rbs +++ b/sig/steep/subtyping/constraints.rbs @@ -56,7 +56,7 @@ module Steep end class Context - attr_reader variance: untyped + attr_reader variance: VariableVariance attr_reader self_type: AST::Types::t @@ -64,20 +64,26 @@ module Steep attr_reader class_type: AST::Types::t - def initialize: (variance: untyped, self_type: AST::Types::t, instance_type: AST::Types::t, class_type: AST::Types::t) -> void + def initialize: (variance: VariableVariance, self_type: AST::Types::t, instance_type: AST::Types::t, class_type: AST::Types::t) -> void end - attr_reader dictionary: Hash[Symbol, [Set[AST::Types::t], Set[AST::Types::t], Set[AST::Types::t]]] + attr_reader dictionary: Hash[Symbol, [Set[AST::Types::t], Set[AST::Types::t]]] - attr_reader vars: Set[Symbol] + attr_reader generics_upper_bounds: Hash[Symbol, AST::Types::t] def initialize: (unknowns: _Each[Symbol]) -> void def self.empty: () -> Constraints - def add_var: (*Symbol vars) -> void + # Add a constraint on type variable + # + # Because the upperbound is truly a constraint which shouldn't include the result type, we have the flag. + # + def add: (Symbol var, ?sub_type: AST::Types::t?, ?super_type: AST::Types::t?) -> void - def add: (Symbol var, ?sub_type: AST::Types::t?, ?super_type: AST::Types::t?, ?skip: bool) -> void + # Add a constraint on type variable as a generics upper bound + # + def add_generics_upper_bound: (Symbol var, AST::Types::t type) -> void def eliminate_variable: (AST::Types::t `type`, to: AST::Types::t) -> AST::Types::t @@ -89,20 +95,42 @@ module Steep def empty?: () -> bool - def upper_bound: (Symbol var, ?skip: bool) -> AST::Types::t + # Returns the upper bound of the variable + # + # If the variable is not constrained, it returns `top` type. + # + def upper_bound: (Symbol var) -> AST::Types::t - def lower_bound: (Symbol var, ?skip: bool) -> AST::Types::t + # Returs the lower bound of the variable + # + # If the variable is not constrained, it returns `bot` type. + # + def lower_bound: (Symbol var) -> AST::Types::t - def solution: (Check checker, variables: Enumerable[AST::Types::variable], variance: VariableVariance, self_type: AST::Types::t, instance_type: AST::Types::t, class_type: AST::Types::t) -> Interface::Substitution - | (Check checker, variables: Enumerable[AST::Types::variable], context: Context) -> Interface::Substitution + def self.solve: (Constraints constraints, Check, Context) -> (Interface::Substitution | UnsatisfiableConstraint) + + def self.solve!: (Constraints constraints, Check, Context) -> Interface::Substitution def has_constraint?: (Symbol var) -> bool + def each_unknown_variable: () { (Symbol) -> void } -> void + | () -> Enumerator[Symbol, void] + + # Yields a tuple of variable name, its lower bound, and its upper_bound + # def each: () { ([Symbol, AST::Types::t, AST::Types::t]) -> void } -> void | () -> Enumerator[[Symbol, AST::Types::t, AST::Types::t], void] def to_s: () -> ::String + # Returns a constraint for the variable + # + # If the variable is not constrained, it returns `nil`. + # If the variable is constrained by one side, it returns the type. + # If the variable is constrained by both sides, it returns a pair of types -- the lower bound and the upper bound. + # + def constraint: (Symbol var_name) -> (Array[Relation[AST::Types::t]] | AST::Types::t | nil) + private def lower_bound_types: (Symbol var_name) -> Set[AST::Types::t] diff --git a/test/constraints_test.rb b/test/constraints_test.rb index e42685e2d..2564b9cd7 100644 --- a/test/constraints_test.rb +++ b/test/constraints_test.rb @@ -7,41 +7,6 @@ class ConstraintsTest < Minitest::Test include FactoryHelper include SubtypingHelper - BUILTIN = <<-EOB -class BasicObject -end - -class Object < BasicObject - def class: () -> class -end - -class Class - def new: (*untyped) -> untyped -end - -class Module -end - -class String - def to_str: -> String - def self.try_convert: (untyped) -> String -end - -class Integer - def to_int: -> Integer - def self.sqrt: (Integer) -> Integer -end - -class Array[A] - def []: (Integer) -> A - def []=: (Integer, A) -> A -end - -interface _Indexable[T] - def []: (Integer) -> T -end - EOB - def test_bounds with_factory do constraints = Subtyping::Constraints.new(unknowns: [:a, :b, :c]) @@ -82,14 +47,8 @@ def test_subst contravariants: Set.new([:b, :c]) ) - subst = constraints.solution( - checker, - self_type: AST::Types::Self.new, - instance_type: AST::Types::Instance.new, - class_type: AST::Types::Class.new, - variance: variance, - variables: Set.new([:a, :b, :c]) - ) + context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance) + subst = Subtyping::Constraints.solve(constraints, checker, context) assert_equal string, subst[:a] assert_equal integer, subst[:b] @@ -97,22 +56,19 @@ def test_subst end end - def test_subst_with_skip_constraints - with_checker do |checker| + def test_subst_with_generics_upper_bound + with_checker(<<~RBS) do |checker| + interface _Indexable[T] + def []: (Integer) -> T + end + RBS constraints = Subtyping::Constraints.new(unknowns: [:X]) - constraints.add(:X, super_type: parse_type("::_Indexable[::Integer]"), skip: true) - constraints.add(:X, super_type: parse_type("::Array[::Integer]"), skip: false) + constraints.add_generics_upper_bound(:X, parse_type("::_Indexable[::Integer]")) + constraints.add(:X, super_type: parse_type("::Array[::Integer]")) variance = Subtyping::VariableVariance.new(covariants: Set[], contravariants: Set[]) - - subst = constraints.solution( - checker, - self_type: AST::Types::Self.new, - instance_type: AST::Types::Instance.new, - class_type: AST::Types::Class.new, - variance: variance, - variables: Set[:X] - ) + context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance) + subst = Subtyping::Constraints.solve(constraints, checker, context) assert_equal parse_type("::Array[::Integer]"), subst[:X] end @@ -133,25 +89,17 @@ def test_subst2 covariants: Set.new([:a, :c]), contravariants: Set.new([:b, :c]) ) - - subst = constraints.solution( - checker, - self_type: AST::Types::Self.new, - instance_type: AST::Types::Instance.new, - class_type: AST::Types::Class.new, - variance: variance, - variables: Set.new([:a, :b]) - ) + context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance) + subst = Subtyping::Constraints.solve(constraints, checker, context) assert_equal string, subst[:a] assert_equal integer, subst[:b] - refute_operator subst, :key?, :c + assert_equal object, subst[:c] end end def test_variable_elimination - constraints = Subtyping::Constraints.new(unknowns: []) - constraints.add_var(:a, :b) + constraints = Subtyping::Constraints.new(unknowns: [:x]) assert_equal AST::Types::Var.new(name: :x), constraints.eliminate_variable(AST::Types::Var.new(name: :x), to: AST::Types::Top.new) @@ -175,4 +123,62 @@ def test_variable_elimination args: [AST::Types::Var.new(name: :a)]), to: AST::Types::Top.new) end + + def test_solve__with_nested_type_variable + with_checker(<<~RBS) do |checker| + interface _Indexable[T] + def []: (Integer) -> T + end + RBS + # { Array[Integer] <: A <: Array[B], B } + constraints = Subtyping::Constraints.new(unknowns: [:A, :B]) + constraints.add(:A, sub_type: parse_type("::Array[::Integer]"), super_type: parse_type("::_Indexable[B]", variables: [:B])) + + variance = Subtyping::VariableVariance.new(covariants: Set[], contravariants: Set[]) + context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance) + subst = Subtyping::Constraints.solve(constraints, checker, context) + + assert_instance_of Interface::Substitution, subst + + assert_equal parse_type("::Array[::Integer]"), subst[:A] + assert_equal parse_type("::Integer"), subst[:B] + end + end + + def test_solve__with_nested_type_variable__generics_upper_bound + with_checker(<<~RBS) do |checker| + interface _Indexable[T] + def []: (Integer) -> T + end + RBS + + constraints = Subtyping::Constraints.new(unknowns: [:A, :B]) + constraints.add(:A, sub_type: parse_type("::Array[::Integer]")) + constraints.add_generics_upper_bound(:A, parse_type("::_Indexable[B]", variables: [:B])) + + variance = Subtyping::VariableVariance.new(covariants: Set[], contravariants: Set[]) + context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance) + subst = Subtyping::Constraints.solve(constraints, checker, context) + + assert_instance_of Interface::Substitution, subst + + assert_equal parse_type("::Array[::Integer]"), subst[:A] + assert_equal parse_type("::Integer"), subst[:B] + end + end + + def test_solve__fail_by_generics_upper_bound + with_checker(<<~RBS) do |checker| + RBS + constraints = Subtyping::Constraints.new(unknowns: [:A, :B]) + constraints.add(:A, sub_type: parse_type("::String")) + constraints.add_generics_upper_bound(:A, parse_type("::Integer")) + + variance = Subtyping::VariableVariance.new(covariants: Set[], contravariants: Set[]) + context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance) + subst = Subtyping::Constraints.solve(constraints, checker, context) + + assert_instance_of Subtyping::Constraints::UnsatisfiableConstraint, subst + end + end end diff --git a/test/subtyping_test.rb b/test/subtyping_test.rb index 739be661e..8f6d515af 100644 --- a/test/subtyping_test.rb +++ b/test/subtyping_test.rb @@ -684,14 +684,13 @@ def set: (String) -> self assert_equal "::String", constraints.lower_bound(:T).to_s variance = Subtyping::VariableVariance.new(covariants: Set[:T], contravariants: Set[:T]) - s = constraints.solution( - checker, + context = Constraints::Context.new( variance: variance, - variables: Set[:T], self_type: parse_type("self", checker: checker), instance_type: parse_type("instance", checker: checker), class_type: parse_type("class", checker: checker) ) + s = Constraints.solve(constraints, checker, context) assert_equal "::String", s[:T].to_s end end @@ -1124,4 +1123,72 @@ def test_selfq assert_success_check(checker, "self | nil", "self | nil") end end + + def test_coerce_float + with_checker(<<~RBS) do |checker| + class Float + end + + class Integer + end + + interface _Plus[T, S] + def +: (T) -> S + end + + class Num + def +: (::Integer) -> ::Integer + | (::Float) -> ::Float + end + RBS + + Subtyping::Constraints.new(unknowns: [:O, :S, :R]).tap do |constraints| + constraints.add( + :O, + sub_type: parse_type("::Num", checker: checker), + super_type: parse_type("::_Plus[S, R]", variables: [:S, :R], checker: checker) + ) + constraints.add( + :S, + sub_type: parse_type("::Float", checker: checker) + ) + + variance = Subtyping::VariableVariance.new(covariants: Set[:S, :O], contravariants: Set[:T, :O]) + context = Constraints::Context.new(variance: variance, self_type: 1, instance_type: 1, class_type: 1) + solution = Constraints.solve(constraints, checker, context) + assert_instance_of Interface::Substitution, solution + pp solution.to_s + end + end + end + + # def test_bounded_method_parameter + # with_checker(<<~RBS) do |checker| + # class Foo < Object + # end + + # class Bar < Foo + # end + # RBS + + # Subtyping::Constraints.new(unknowns: [:X]).tap do |constraints| + # constraints.add( + # :X, + # super_type: parse_type("::Foo", checker: checker), + # skip: true + # ) + # constraints.add( + # :X, + # sub_type: parse_type("::Bar", checker: checker) + # ) + + # variance = Subtyping::VariableVariance.new(covariants: Set[:X], contravariants: Set[:X]) + # context = Constraints::Context.new(variance: variance, self_type: 1, instance_type: 1, class_type: 1) + + # solution = Constraints.solve(constraints, checker, context) + # assert_instance_of Interface::Substitution, solution + # pp solution.to_s + # end + # end + # end end diff --git a/test/type_check_test.rb b/test/type_check_test.rb index 99310de85..76779a61f 100644 --- a/test/type_check_test.rb +++ b/test/type_check_test.rb @@ -16,10 +16,10 @@ class TypeCheckTest < Minitest::Test include Steep - def run_type_check_test(signatures: {}, code: {}, expectations: nil) + def run_type_check_test(signatures: {}, code: {}, expectations: nil, nostdlib: false) typings = {} - with_factory(signatures, nostdlib: false) do |factory| + with_factory(signatures, nostdlib: nostdlib) do |factory| builder = Interface::Builder.new(factory) subtyping = Subtyping::Check.new(builder: builder) @@ -2103,4 +2103,605 @@ def foo(x) #: Integer YAML ) end + + def test_numeric_plus__single + run_type_check_test( + signatures: { + "a.rbs" => <<~RBS + class BasicObject + def initialize: () -> void + end + + module Kernel : BasicObject + end + + class Object < BasicObject + include Kernel + end + + class Module + end + + class Class < Module + def new: () -> untyped + end + + class Numeric + def coerce: (self) -> [self, self] + | (untyped) -> [Float, Float] + + def to_r: () -> Rational + + def to_c: () -> Complex + end + + interface _Add[Other, Return] + def +: (Other) -> Return + end + + interface _Coerce[Other, ConvertedOther, ConvertedSelf] + def coerce: (Other) -> [ConvertedOther, ConvertedSelf] + end + + class Integer < Numeric + def coerce: ... + + def +: (Integer) -> Integer + | [O < _Add[S, R], S, R] (_Coerce[Integer, O, S] other) -> R + end + + class Float < Numeric + def coerce: (untyped) -> [Float, Float] + + def +: (Float) -> Float + | (Integer) -> Float + | [O < _Add[S, R], S, R] (_Coerce[Float, O, S] other) -> R + end + + class Rational < Numeric + def coerce: (Integer) -> [Rational, Rational] + | (Float) -> [Float, Float] + | (Rational) -> [Rational, Rational] + | (Complex) -> ([Rational, Rational] | [Complex, Complex]) + + def +: (Integer) -> Rational + | (Float) -> Float + | (Rational) -> Rational + | [O < _Add[S, R], S, R] (_Coerce[Rational, O, S] other) -> R + end + + class Complex < Numeric + def coerce: (untyped) -> [Complex, Complex] + + def +: (Integer) -> Complex + | (Float) -> Complex + | (Rational) -> Complex + | (Complex) -> Complex + | [O < _Add[S, R], S, R] (_Coerce[Complex, O, S] other) -> R + end + RBS + }, + nostdlib: true, + code: { + "a.rb" => <<~RUBY + (1 + 1).integer! + (1 + 1.0).float! + (1 + 1.to_r).rational! + (1 + 1.to_c).complex! + + (1.0 + 1).float! + (1.0 + 1.0).float! + (1.0 + 1.to_r).float! + (1.0 + 1.to_c).complex! + + (1.to_r + 1).rational! + (1.to_r + 1.0).float! + (1.to_r + 1.to_r).rational! + (1.to_r + 1.to_c).complex! + + (1.to_c + 1).complex! + (1.to_c + 1.0).complex! + (1.to_c + 1.to_r).complex! + (1.to_c + 1.to_c).complex! + RUBY + }, + expectations: <<~YAML + --- + - file: a.rb + diagnostics: + - range: + start: + line: 1 + character: 8 + end: + line: 1 + character: 16 + severity: ERROR + message: Type `::Integer` does not have method `integer!` + code: Ruby::NoMethod + - range: + start: + line: 2 + character: 10 + end: + line: 2 + character: 16 + severity: ERROR + message: Type `::Float` does not have method `float!` + code: Ruby::NoMethod + - range: + start: + line: 3 + character: 13 + end: + line: 3 + character: 22 + severity: ERROR + message: Type `::Rational` does not have method `rational!` + code: Ruby::NoMethod + - range: + start: + line: 4 + character: 13 + end: + line: 4 + character: 21 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + - range: + start: + line: 6 + character: 10 + end: + line: 6 + character: 16 + severity: ERROR + message: Type `::Float` does not have method `float!` + code: Ruby::NoMethod + - range: + start: + line: 7 + character: 12 + end: + line: 7 + character: 18 + severity: ERROR + message: Type `::Float` does not have method `float!` + code: Ruby::NoMethod + - range: + start: + line: 8 + character: 15 + end: + line: 8 + character: 21 + severity: ERROR + message: Type `::Float` does not have method `float!` + code: Ruby::NoMethod + - range: + start: + line: 9 + character: 15 + end: + line: 9 + character: 23 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + - range: + start: + line: 11 + character: 13 + end: + line: 11 + character: 22 + severity: ERROR + message: Type `::Rational` does not have method `rational!` + code: Ruby::NoMethod + - range: + start: + line: 12 + character: 15 + end: + line: 12 + character: 21 + severity: ERROR + message: Type `::Float` does not have method `float!` + code: Ruby::NoMethod + - range: + start: + line: 13 + character: 18 + end: + line: 13 + character: 27 + severity: ERROR + message: Type `::Rational` does not have method `rational!` + code: Ruby::NoMethod + - range: + start: + line: 14 + character: 18 + end: + line: 14 + character: 26 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + - range: + start: + line: 16 + character: 13 + end: + line: 16 + character: 21 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + - range: + start: + line: 17 + character: 15 + end: + line: 17 + character: 23 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + - range: + start: + line: 18 + character: 18 + end: + line: 18 + character: 26 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + - range: + start: + line: 19 + character: 18 + end: + line: 19 + character: 26 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + YAML + ) + end + + def test_numeric_plus__union + run_type_check_test( + signatures: { + "a.rbs" => <<~RBS + class BasicObject + def initialize: () -> void + end + + module Kernel : BasicObject + end + + class Object < BasicObject + include Kernel + end + + class Module + end + + class Class < Module + def new: () -> untyped + end + + class Numeric + def coerce: (self) -> [self, self] + | (untyped) -> [Float, Float] + + def to_r: () -> Rational + + def to_c: () -> Complex + end + + interface _Add[Other, Return] + def +: (Other) -> Return + end + + interface _Coerce[Other, Converted] + def coerce: (Other) -> [Converted, Converted] + end + + class Integer < Numeric + def coerce: ... + + def +: (Integer) -> Integer + | [O < _Add[O, R], R] (_Coerce[self, O] other) -> R + end + + class Float < Numeric + def coerce: (untyped) -> [Float, Float] + + def +: (Float) -> Float + | (Integer) -> Float + | [O < _Add[O, R], R] (_Coerce[Float, O] other) -> R + end + + class Rational < Numeric + def coerce: (Integer) -> [Rational, Rational] + | (Float) -> [Float, Float] + | (Rational) -> [Rational, Rational] + | (Complex) -> ([Rational, Rational] | [Complex, Complex]) + + def +: (Integer) -> Rational + | (Float) -> Float + | (Rational) -> Rational + | [O < _Add[S, R], S, R] (_Coerce[self, O] other) -> R + end + + class Complex < Numeric + def coerce: (untyped) -> [Complex, Complex] + + def +: (Integer) -> Complex + | (Float) -> Complex + | (Rational) -> Complex + | (Complex) -> Complex + | [O < _Add[S, R], S, R] (_Coerce[self, O] other) -> R + end + RBS + }, + nostdlib: true, + code: { + "a.rb" => <<~RUBY + ( + 1 + + 1 #: Integer | Float | Rational | Complex + ).type_int_float_rational_complex? + + ( + 1.1 + + 1 #: Integer | Float | Rational | Complex + ).type_float_or_complex? + + ( + 1.to_r + + 1 #: Integer | Float | Rational | Complex + ).type_float_or_rational? + + ( + 1.to_c + + 1 #: Integer | Float | Rational | Complex + ).type_complex? + RUBY + }, + expectations: <<~YAML + --- + - file: a.rb + diagnostics: + - range: + start: + line: 4 + character: 2 + end: + line: 4 + character: 34 + severity: ERROR + message: Type `(::Integer | ::Float | ::Rational | ::Complex)` does not have method + `type_int_float_rational_complex?` + code: Ruby::NoMethod + - range: + start: + line: 9 + character: 2 + end: + line: 9 + character: 24 + severity: ERROR + message: Type `(::Float | ::Complex)` does not have method + `type_float_or_complex?` + code: Ruby::NoMethod + - range: + start: + line: 14 + character: 2 + end: + line: 14 + character: 25 + severity: ERROR + message: Type `(::Float | ::Rational)` does not have method + `type_float_or_rational?` + code: Ruby::NoMethod + - range: + start: + line: 19 + character: 2 + end: + line: 19 + character: 15 + severity: ERROR + message: Type `::Complex` does not have method + `type_complex?` + code: Ruby::NoMethod + YAML + ) + end + + def test_numeric_plus__testtest + run_type_check_test( + signatures: { + "a.rbs" => <<~RBS + class BasicObject + def initialize: () -> void + end + + module Kernel : BasicObject + end + + class Object < BasicObject + include Kernel + end + + class Module + end + + class Class < Module + def new: () -> untyped + end + + class Numeric + def coerce: (self) -> [self, self] + | (untyped) -> [Float, Float] + + def to_r: () -> Rational + + def to_c: () -> Complex + end + + interface _Add[Other, Return] + def +: (Other) -> Return + end + + interface _Coerce[Other, ConvertedOther, ConvertedSelf] + def coerce: (Other) -> [ConvertedOther, ConvertedSelf] + end + + class Integer < Numeric + def coerce: ... + + def +: (Integer) -> Integer + | [O < _Add[S, R], S, R] (_Coerce[Integer, O, S] other) -> R + end + + class Float < Numeric + def coerce: (untyped) -> [Float, Float] + + def +: (Float) -> Float + | (Integer) -> Float + | [O < _Add[S, R], S, R] (_Coerce[Float, O, S] other) -> R + end + + class Rational < Numeric + def coerce: (Integer) -> [Rational, Rational] + | (Float) -> [Float, Float] + | (Rational) -> [Rational, Rational] + | (Complex) -> ([Rational, Rational] | [Complex, Complex]) + + def +: (Integer) -> Rational + | (Float) -> Float + | (Rational) -> Rational + | [O < _Add[S, R], S, R] (_Coerce[Rational, O, S] other) -> R + end + + class Complex < Numeric + def coerce: (untyped) -> [Complex, Complex] + + def +: (Integer) -> Complex + | (Float) -> Complex + | (Rational) -> Complex + | (Complex) -> Complex + | [O < _Add[S, R], S, R] (_Coerce[Complex, O, S] other) -> R + end + RBS + }, + nostdlib: true, + code: { + "a.rb" => <<~RUBY + (1 + 1).integer! + (1 + 1.0).float! + (1 + 1.to_r).rational! + (1 + 1.to_c).complex! + RUBY + }, + expectations: <<~YAML + --- + - file: a.rb + diagnostics: + - range: + start: + line: 1 + character: 8 + end: + line: 1 + character: 16 + severity: ERROR + message: Type `::Integer` does not have method `integer!` + code: Ruby::NoMethod + - range: + start: + line: 2 + character: 10 + end: + line: 2 + character: 16 + severity: ERROR + message: Type `::Float` does not have method `float!` + code: Ruby::NoMethod + - range: + start: + line: 3 + character: 1 + end: + line: 3 + character: 11 + severity: ERROR + message: Type `::Rational` does not have method `rational!` + code: Ruby::NoMethod + - range: + start: + line: 4 + character: 1 + end: + line: 4 + character: 11 + severity: ERROR + message: Type `::Complex` does not have method `complex!` + code: Ruby::NoMethod + YAML + ) + end + + def test_generic_method_call__1 + run_type_check_test( + signatures: { + "a.rbs" => <<~RBS + class Hello + def f: [A] () { () -> A } -> A + end + RBS + }, + code: { + "a.rb" => <<~RUBY + hello = Hello.new() + + a = hello.f() { 1 } + a.is_integer + RUBY + }, + expectations: <<~YAML + --- + - file: a.rb + diagnostics: + - range: + start: + line: 5 + character: 4 + end: + line: 5 + character: 7 + severity: ERROR + message: Type `::String` does not have method `foo` + code: Ruby::NoMethod + - range: + start: + line: 6 + character: 4 + end: + line: 6 + character: 7 + severity: ERROR + message: Type `::Integer` does not have method `bar` + code: Ruby::NoMethod + YAML + ) + end end