From 1666659c1b55a930acdc19ef5aaa25c49eca3538 Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Fri, 5 Jul 2024 13:40:43 +0900
Subject: [PATCH 1/7] Add test

---
 test/type_check_test.rb | 426 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 424 insertions(+), 2 deletions(-)

diff --git a/test/type_check_test.rb b/test/type_check_test.rb
index 99310de85..570a72165 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,426 @@ 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
 end

From efa46f9f58a5170d970df1eeaef5b77f4fdb63f0 Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Thu, 11 Jul 2024 10:48:39 +0900
Subject: [PATCH 2/7] Subtyping test

---
 Gemfile                             |   2 +
 Gemfile.lock                        |   9 +-
 lib/steep/subtyping/constraints.rb  | 103 +++++++++++++--------
 sig/steep/subtyping/constraints.rbs |   7 ++
 test/subtyping_test.rb              |  42 +++++++++
 test/type_check_test.rb             | 134 ++++++++++++++++++++++++++++
 6 files changed, 256 insertions(+), 41 deletions(-)

diff --git a/Gemfile b/Gemfile
index ff77e12ef..6013622b1 100644
--- a/Gemfile
+++ b/Gemfile
@@ -12,3 +12,5 @@ end
 gem 'minitest-slow_test'
 
 gem "debug", require: false, platform: :mri
+
+gem "rbs", path: "../rbs"
diff --git a/Gemfile.lock b/Gemfile.lock
index 5f1f7f0fe..fae1b2c4e 100644
--- a/Gemfile.lock
+++ b/Gemfile.lock
@@ -1,3 +1,9 @@
+PATH
+  remote: ../rbs
+  specs:
+    rbs (3.5.1)
+      logger
+
 PATH
   remote: .
   specs:
@@ -71,8 +77,6 @@ GEM
     rb-fsevent (0.11.2)
     rb-inotify (0.11.1)
       ffi (~> 1.0)
-    rbs (3.5.1)
-      logger
     rdoc (6.7.0)
       psych (>= 4.0.0)
     reline (0.5.9)
@@ -96,6 +100,7 @@ DEPENDENCIES
   minitest-hooks
   minitest-slow_test
   rake
+  rbs!
   stackprof
   steep!
 
diff --git a/lib/steep/subtyping/constraints.rb b/lib/steep/subtyping/constraints.rb
index 4da9bfa36..93e0a760b 100644
--- a/lib/steep/subtyping/constraints.rb
+++ b/lib/steep/subtyping/constraints.rb
@@ -237,6 +237,8 @@ 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)
+        pp self.to_s
+        
         if context
           raise if variance
           raise if self_type
@@ -249,56 +251,79 @@ def solution(checker, variance: nil, variables:, self_type: nil, instance_type:
           class_type = context.class_type
         end
 
-        vars = [] #: Array[Symbol]
-        types = [] #: Array[AST::Types::t]
+        subst = Interface::Substitution.empty
+
+        single_side_constraint_vars = [] #: Array[Symbol]
+        double_side_constraint_vars = [] #: Array[Symbol]
+        no_constraint_vars = [] #: Array[Symbol]
 
         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)
-              )
+            lower_bound_types = lower_bound_types(var)
+            upper_bound_types = upper_bound_types(var)
+
+            case
+            when !lower_bound_types.empty? && !upper_bound_types.empty?
+              double_side_constraint_vars << var
+            when lower_bound_types.empty? && upper_bound_types.empty?
+              no_constraint_vars << var
+            else
+              single_side_constraint_vars << var
+            end
+          end
+        end
+
+        single_side_constraint_vars.each do |var|
+          resolve = lower_bound(var)
+          if resolve.is_a?(AST::Types::Bot)
+            resolve = upper_bound(var)
+          end
 
-              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
+          subst.add!(var, resolve)
+        end
+
+        double_side_constraint_vars.each do |var|
+          lower = lower_bound(var).subst(subst)
+          upper = upper_bound(var).subst(subst)
+
+          relation = Relation.new(sub_type: lower, super_type: upper)
+
+          checker.check(relation, self_type: self_type, instance_type: instance_type, class_type: class_type, constraints: self).yield_self do |result|
+            if result.success?
+              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
-                  raise UnsatisfiableConstraint.new(
-                    var: var,
-                    sub_type: result.relation.sub_type,
-                    super_type: result.relation.super_type,
-                    result: result
-                  )
+                  if lower_bound.level.join > upper_bound.level.join
+                    upper_bound
+                  else
+                    lower_bound
+                  end
                 end
-              end
+
+              subst.add!(var, type)
             else
-              vars << var
-              types << AST::Types::Any.new
+              raise UnsatisfiableConstraint.new(
+                var: var,
+                sub_type: result.relation.sub_type,
+                super_type: result.relation.super_type,
+                result: result
+              )
             end
           end
         end
 
-        Interface::Substitution.build(vars, types)
+        no_constraint_vars.each do |var|
+          subst.add!(var, AST::Types::Any.new)
+        end
+
+        subst
       end
 
       def has_constraint?(var)
diff --git a/sig/steep/subtyping/constraints.rbs b/sig/steep/subtyping/constraints.rbs
index b54103c21..21be7cef3 100644
--- a/sig/steep/subtyping/constraints.rbs
+++ b/sig/steep/subtyping/constraints.rbs
@@ -77,6 +77,11 @@ module Steep
 
       def add_var: (*Symbol vars) -> void
 
+      # Add a constraint on type variable
+      #
+      # `skip:` is for generics upper bounds.
+      # 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?, ?skip: bool) -> void
 
       def eliminate_variable: (AST::Types::t `type`, to: AST::Types::t) -> AST::Types::t
@@ -89,6 +94,8 @@ module Steep
 
       def empty?: () -> bool
 
+      def sub_constraints: () -> Constraints
+
       def upper_bound: (Symbol var, ?skip: bool) -> AST::Types::t
 
       def lower_bound: (Symbol var, ?skip: bool) -> AST::Types::t
diff --git a/test/subtyping_test.rb b/test/subtyping_test.rb
index 739be661e..5bf912858 100644
--- a/test/subtyping_test.rb
+++ b/test/subtyping_test.rb
@@ -1124,4 +1124,46 @@ 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])
+        constraints.solution(
+          checker,
+          variance: variance,
+          variables: [:O, :S, :R],
+          self_type: 1,
+          instance_type: 1,
+          class_type: 1
+        )
+      end
+    end
+  end
 end
diff --git a/test/type_check_test.rb b/test/type_check_test.rb
index 570a72165..655015c9f 100644
--- a/test/type_check_test.rb
+++ b/test/type_check_test.rb
@@ -2525,4 +2525,138 @@ def +: (Integer) -> Complex
       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
 end

From 9c2dc26ec5072d698e34249da8244e38a8c9cbdb Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Fri, 12 Jul 2024 13:09:53 +0900
Subject: [PATCH 3/7] Extract `Constraints.solve` method

---
 lib/steep/subtyping/check.rb        |  15 ++--
 lib/steep/subtyping/constraints.rb  | 127 +++++++++++-----------------
 sig/steep/subtyping/constraints.rbs |  24 +++++-
 test/subtyping_test.rb              |  10 +--
 4 files changed, 86 insertions(+), 90 deletions(-)

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 93e0a760b..762af0850 100644
--- a/lib/steep/subtyping/constraints.rb
+++ b/lib/steep/subtyping/constraints.rb
@@ -236,98 +236,57 @@ 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)
-        pp self.to_s
-        
-        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
-        end
-
+      def self.solve(constraints, checker, context)
         subst = Interface::Substitution.empty
 
-        single_side_constraint_vars = [] #: Array[Symbol]
-        double_side_constraint_vars = [] #: Array[Symbol]
-        no_constraint_vars = [] #: Array[Symbol]
-
-        dictionary.each_key do |var|
-          if variables.include?(var)
-            lower_bound_types = lower_bound_types(var)
-            upper_bound_types = upper_bound_types(var)
-
-            case
-            when !lower_bound_types.empty? && !upper_bound_types.empty?
-              double_side_constraint_vars << var
-            when lower_bound_types.empty? && upper_bound_types.empty?
-              no_constraint_vars << var
-            else
-              single_side_constraint_vars << var
-            end
-          end
-        end
+        constraints.dictionary.each_key do |var|
+          constraint = constraints.constraint(var)
 
-        single_side_constraint_vars.each do |var|
-          resolve = lower_bound(var)
-          if resolve.is_a?(AST::Types::Bot)
-            resolve = upper_bound(var)
-          end
+          case constraint
+          when Array
+            relation = Relation.new(sub_type: constraint[0], super_type: constraint[1])
 
-          subst.add!(var, resolve)
-        end
+            checker.check(relation, self_type: context.self_type, instance_type: context.instance_type, class_type: context.class_type, constraints: Constraints.empty).yield_self do |result|
+              if result.success?
+                upper_bound = constraints.upper_bound(var, skip: true)
+                lower_bound = constraints.lower_bound(var, skip: true)
 
-        double_side_constraint_vars.each do |var|
-          lower = lower_bound(var).subst(subst)
-          upper = upper_bound(var).subst(subst)
-
-          relation = Relation.new(sub_type: lower, super_type: upper)
-
-          checker.check(relation, self_type: self_type, instance_type: instance_type, class_type: class_type, constraints: self).yield_self do |result|
-            if result.success?
-              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
+                type =
+                  case
+                  when context.variance.contravariant?(var)
                     upper_bound
-                  else
+                  when context.variance.covariant?(var)
                     lower_bound
+                  else
+                    if lower_bound.level.join > upper_bound.level.join
+                      upper_bound
+                    else
+                      lower_bound
+                    end
                   end
-                end
-
-              subst.add!(var, type)
-            else
-              raise UnsatisfiableConstraint.new(
-                var: var,
-                sub_type: result.relation.sub_type,
-                super_type: result.relation.super_type,
-                result: result
-              )
+
+                subst.add!(var, type)
+              else
+                return UnsatisfiableConstraint.new(
+                  var: var,
+                  sub_type: result.relation.sub_type,
+                  super_type: result.relation.super_type,
+                  result: result
+                )
+              end
             end
+          when nil
+            subst.add!(var, AST::Types::Any.new())
+          else
+            subst.add!(var, constraint)
           end
         end
 
-        no_constraint_vars.each do |var|
-          subst.add!(var, AST::Types::Any.new)
-        end
-
         subst
       end
 
       def has_constraint?(var)
-        !upper_bound_types(var).empty? || !lower_bound_types(var).empty?
+        constraint(var) ? true : false
       end
 
       def each
@@ -348,6 +307,22 @@ def to_s
         "#{unknowns.to_a.join(",")}/#{vars.to_a.join(",")} |- { #{strings.join(", ")} }"
       end
 
+      def constraint(var_name)
+        upper_bound = upper_bound(var_name)
+        lower_bound = lower_bound(var_name)
+
+        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
+          [lower_bound, upper_bound]
+        end
+      end
+
       def lower_bound_types(var_name)
         lower, _, _ = dictionary[var_name]
         lower
diff --git a/sig/steep/subtyping/constraints.rbs b/sig/steep/subtyping/constraints.rbs
index 21be7cef3..8e0fe2153 100644
--- a/sig/steep/subtyping/constraints.rbs
+++ b/sig/steep/subtyping/constraints.rbs
@@ -96,20 +96,40 @@ module Steep
 
       def sub_constraints: () -> Constraints
 
+      # Returns the upper bound of the variable
+      #
+      # If the variable is not constrained, it returns `top` type.
+      # If `skip: true` is given, it ignores the generics upper-bound constraints.
+      #
       def upper_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, ?skip: bool) -> 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 has_constraint?: (Symbol var) -> bool
 
+      # 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.
+      #
+      # The `skip` constraints are included in the result.
+      #
+      def constraint: (Symbol var_name) -> ([AST::Types::t, AST::Types::t] | AST::Types::t | nil)
+
       private
 
       def lower_bound_types: (Symbol var_name) -> Set[AST::Types::t]
diff --git a/test/subtyping_test.rb b/test/subtyping_test.rb
index 5bf912858..c86f928c7 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
@@ -1155,14 +1154,13 @@ def +: (::Integer) -> ::Integer
         )
 
         variance = Subtyping::VariableVariance.new(covariants: Set[:S, :O], contravariants: Set[:T, :O])
-        constraints.solution(
-          checker,
+        context = Constraints::Context.new(
           variance: variance,
-          variables: [:O, :S, :R],
           self_type: 1,
           instance_type: 1,
           class_type: 1
         )
+        assert_instance_of Interface::Substitution, Constraints.solve(constraints, checker, context)
       end
     end
   end

From 4c23fdda5b79ec5b6d202deab9597eea5804ee92 Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Fri, 12 Jul 2024 15:51:11 +0900
Subject: [PATCH 4/7] Fix constraint solver

---
 lib/steep/subtyping/constraints.rb  | 133 ++++++++++++++++------------
 sig/steep/subtyping/constraints.rbs |  13 ++-
 test/constraints_test.rb            |  21 +----
 test/subtyping_test.rb              |  41 +++++++--
 4 files changed, 121 insertions(+), 87 deletions(-)

diff --git a/lib/steep/subtyping/constraints.rb b/lib/steep/subtyping/constraints.rb
index 762af0850..42f8bc374 100644
--- a/lib/steep/subtyping/constraints.rb
+++ b/lib/steep/subtyping/constraints.rb
@@ -80,7 +80,7 @@ def initialize(unknowns:)
         @vars = Set.new
 
         unknowns.each do |var|
-          dictionary[var] = [Set.new, Set.new, Set.new]
+          dictionary[var] = [Set.new, Set.new]
         end
       end
 
@@ -102,7 +102,7 @@ def add_var(*vars)
       end
 
       def add(var, sub_type: nil, super_type: nil, skip: false)
-        subs, supers, skips = dictionary[var]
+        subs, supers = dictionary[var]
 
         if sub_type.is_a?(AST::Types::Logic::Base)
           sub_type = AST::Builtin.bool_type
@@ -115,13 +115,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|
@@ -204,12 +202,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 +215,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
@@ -239,50 +233,87 @@ def lower_bound(var, skip: false)
       def self.solve(constraints, checker, context)
         subst = Interface::Substitution.empty
 
+        double_end_constraints = [] #: Array[Symbol]
+        no_constraints = [] #: Array[Symbol]
+
         constraints.dictionary.each_key do |var|
           constraint = constraints.constraint(var)
 
           case constraint
           when Array
-            relation = Relation.new(sub_type: constraint[0], super_type: constraint[1])
-
-            checker.check(relation, self_type: context.self_type, instance_type: context.instance_type, class_type: context.class_type, constraints: Constraints.empty).yield_self do |result|
-              if result.success?
-                upper_bound = constraints.upper_bound(var, skip: true)
-                lower_bound = constraints.lower_bound(var, skip: true)
-
-                type =
-                  case
-                  when context.variance.contravariant?(var)
-                    upper_bound
-                  when context.variance.covariant?(var)
-                    lower_bound
-                  else
-                    if lower_bound.level.join > upper_bound.level.join
-                      upper_bound
-                    else
-                      lower_bound
-                    end
-                  end
-
-                subst.add!(var, type)
-              else
-                return UnsatisfiableConstraint.new(
-                  var: var,
-                  sub_type: result.relation.sub_type,
-                  super_type: result.relation.super_type,
-                  result: result
-                )
-              end
-            end
+            double_end_constraints << var
           when nil
-            subst.add!(var, AST::Types::Any.new())
+            no_constraints << var
           else
-            subst.add!(var, constraint)
+            type = constraint.subst(subst)
+            subst.add!(var, type)
+          end
+        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, Relation[AST::Types::t]]
+        double_end_constraints.each do |var|
+          additional_relations[var] = Relation.new(
+            sub_type: constraints.lower_bound(var).subst(subst),
+            super_type: constraints.upper_bound(var).subst(subst)
+          )
+        end
+
+        fvs = additional_relations.each_with_object(Set.new) do |(var, relation), fvs| #$ Set[Symbol]
+          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
 
-        subst
+        fvs = fvs & no_constraints
+
+        cs = Constraints.new(unknowns: fvs)
+        additional_relations.each do |var, 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
+          end
+        end
+
+        solution = solve(cs, checker, context)
+        if solution.is_a?(Interface::Substitution)
+          subst.merge!(solution)
+
+          additional_relations.each do |var, relation|
+            type =
+              case
+              when context.variance.contravariant?(var)
+                relation.super_type
+              when context.variance.covariant?(var)
+                relation.sub_type
+              else
+                if relation.sub_type.level.join > relation.super_type.level.join
+                  relation.super_type
+                else
+                  relation.sub_type
+                end
+              end
+
+            subst.add!(var, type.subst(solution))
+          end
+
+          subst
+        else
+          solution
+        end
       end
 
       def has_constraint?(var)
@@ -329,16 +360,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/sig/steep/subtyping/constraints.rbs b/sig/steep/subtyping/constraints.rbs
index 8e0fe2153..162660f87 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,10 +64,10 @@ 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]
 
@@ -99,15 +99,14 @@ module Steep
       # Returns the upper bound of the variable
       #
       # If the variable is not constrained, it returns `top` type.
-      # If `skip: true` is given, it ignores the generics upper-bound constraints.
       #
-      def upper_bound: (Symbol var, ?skip: bool) -> AST::Types::t
+      def upper_bound: (Symbol var) -> 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, ?skip: bool) -> AST::Types::t
+      def lower_bound: (Symbol var) -> AST::Types::t
 
       def self.solve: (Constraints constraints, Check, Context) -> (Interface::Substitution | UnsatisfiableConstraint)
 
@@ -126,8 +125,6 @@ module Steep
       # 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.
       #
-      # The `skip` constraints are included in the result.
-      #
       def constraint: (Symbol var_name) -> ([AST::Types::t, AST::Types::t] | AST::Types::t | nil)
 
       private
diff --git a/test/constraints_test.rb b/test/constraints_test.rb
index e42685e2d..171c94652 100644
--- a/test/constraints_test.rb
+++ b/test/constraints_test.rb
@@ -82,14 +82,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]
@@ -104,15 +98,8 @@ def test_subst_with_skip_constraints
       constraints.add(:X, super_type: parse_type("::Array[::Integer]"), skip: false)
 
       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
diff --git a/test/subtyping_test.rb b/test/subtyping_test.rb
index c86f928c7..8f6d515af 100644
--- a/test/subtyping_test.rb
+++ b/test/subtyping_test.rb
@@ -1154,14 +1154,41 @@ def +: (::Integer) -> ::Integer
         )
 
         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
-        )
-        assert_instance_of Interface::Substitution, Constraints.solve(constraints, checker, context)
+        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

From ed9ceff92d07cb36021abb5455d726c22b3e2673 Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Fri, 12 Jul 2024 15:51:16 +0900
Subject: [PATCH 5/7] Gemfile

---
 Gemfile      | 3 ++-
 Gemfile.lock | 9 ++-------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/Gemfile b/Gemfile
index 6013622b1..1dfea64bf 100644
--- a/Gemfile
+++ b/Gemfile
@@ -13,4 +13,5 @@ gem 'minitest-slow_test'
 
 gem "debug", require: false, platform: :mri
 
-gem "rbs", path: "../rbs"
+# gem "rbs", path: File.join(__dir__, "../rbs")
+# gem "rbs", path: "../rbs"
diff --git a/Gemfile.lock b/Gemfile.lock
index fae1b2c4e..5f1f7f0fe 100644
--- a/Gemfile.lock
+++ b/Gemfile.lock
@@ -1,9 +1,3 @@
-PATH
-  remote: ../rbs
-  specs:
-    rbs (3.5.1)
-      logger
-
 PATH
   remote: .
   specs:
@@ -77,6 +71,8 @@ GEM
     rb-fsevent (0.11.2)
     rb-inotify (0.11.1)
       ffi (~> 1.0)
+    rbs (3.5.1)
+      logger
     rdoc (6.7.0)
       psych (>= 4.0.0)
     reline (0.5.9)
@@ -100,7 +96,6 @@ DEPENDENCIES
   minitest-hooks
   minitest-slow_test
   rake
-  rbs!
   stackprof
   steep!
 

From 1cb2896bc70fab63e17a8a78df6fd8131dac4789 Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Fri, 12 Jul 2024 16:22:34 +0900
Subject: [PATCH 6/7] Constraints

---
 lib/steep/subtyping/constraints.rb  | 41 ++++++++++++++++-------------
 sig/steep/subtyping/constraints.rbs | 14 ++++++----
 test/constraints_test.rb            | 20 +++++---------
 3 files changed, 37 insertions(+), 38 deletions(-)

diff --git a/lib/steep/subtyping/constraints.rb b/lib/steep/subtyping/constraints.rb
index 42f8bc374..45324d869 100644
--- a/lib/steep/subtyping/constraints.rb
+++ b/lib/steep/subtyping/constraints.rb
@@ -73,11 +73,11 @@ 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]
@@ -88,20 +88,11 @@ 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)
+      def add(var, sub_type: nil, super_type: nil)
         subs, supers = dictionary[var]
 
         if sub_type.is_a?(AST::Types::Logic::Base)
@@ -162,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(
@@ -320,6 +311,14 @@ def has_constraint?(var)
         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
         if block_given?
           dictionary.each_key do |var|
@@ -332,10 +331,14 @@ 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)
diff --git a/sig/steep/subtyping/constraints.rbs b/sig/steep/subtyping/constraints.rbs
index 162660f87..34f42fdfa 100644
--- a/sig/steep/subtyping/constraints.rbs
+++ b/sig/steep/subtyping/constraints.rbs
@@ -69,20 +69,21 @@ module Steep
 
       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
       #
-      # `skip:` is for generics upper bounds.
       # 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?, ?skip: bool) -> void
+      def add: (Symbol var, ?sub_type: AST::Types::t?, ?super_type: AST::Types::t?) -> 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
 
@@ -112,6 +113,9 @@ module Steep
 
       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
diff --git a/test/constraints_test.rb b/test/constraints_test.rb
index 171c94652..45322c239 100644
--- a/test/constraints_test.rb
+++ b/test/constraints_test.rb
@@ -94,8 +94,8 @@ def test_subst
   def test_subst_with_skip_constraints
     with_checker do |checker|
       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[])
       context = Subtyping::Constraints::Context.new(self_type: nil, instance_type: nil, class_type: nil, variance: variance)
@@ -120,25 +120,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)

From cb9394d84171f5e71c61fac7f1669fa34d0ac1d3 Mon Sep 17 00:00:00 2001
From: Soutaro Matsumoto <matsumoto@soutaro.com>
Date: Fri, 12 Jul 2024 18:07:49 +0900
Subject: [PATCH 7/7] WIP

---
 lib/steep/subtyping/constraints.rb  | 109 ++++++++++++++++++----------
 lib/steep/type_construction.rb      |  30 +++-----
 sig/steep/subtyping/constraints.rbs |   6 +-
 test/constraints_test.rb            | 101 ++++++++++++++++----------
 test/type_check_test.rb             |  45 ++++++++++++
 5 files changed, 194 insertions(+), 97 deletions(-)

diff --git a/lib/steep/subtyping/constraints.rb b/lib/steep/subtyping/constraints.rb
index 45324d869..4f1bb541f 100644
--- a/lib/steep/subtyping/constraints.rb
+++ b/lib/steep/subtyping/constraints.rb
@@ -221,10 +221,20 @@ def lower_bound(var)
 
       Context = _ = Struct.new(:variance, :self_type, :instance_type, :class_type, keyword_init: true)
 
+      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 = [] #: Array[Symbol]
+        double_end_constraints = {} #: Hash[Symbol, Array[Relation[AST::Types::t]]]
         no_constraints = [] #: Array[Symbol]
 
         constraints.dictionary.each_key do |var|
@@ -232,7 +242,7 @@ def self.solve(constraints, checker, context)
 
           case constraint
           when Array
-            double_end_constraints << var
+            double_end_constraints[var] = constraint
           when nil
             no_constraints << var
           else
@@ -246,35 +256,38 @@ def self.solve(constraints, checker, context)
           return subst.merge!(untyped_subst)
         end
 
-        additional_relations = {} #: Hash[Symbol, Relation[AST::Types::t]]
-        double_end_constraints.each do |var|
-          additional_relations[var] = Relation.new(
-            sub_type: constraints.lower_bound(var).subst(subst),
-            super_type: constraints.upper_bound(var).subst(subst)
-          )
+        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, relation), fvs| #$ Set[Symbol]
-          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)
+        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, 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
-              )
+        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
             end
           end
         end
@@ -283,18 +296,21 @@ def self.solve(constraints, checker, context)
         if solution.is_a?(Interface::Substitution)
           subst.merge!(solution)
 
-          additional_relations.each do |var, relation|
+          additional_relations.each do |var, relations|
+            lowest = relations[0].sub_type
+            upest = relations[-1].super_type
+
             type =
               case
               when context.variance.contravariant?(var)
-                relation.super_type
+                upest
               when context.variance.covariant?(var)
-                relation.sub_type
+                lowest
               else
-                if relation.sub_type.level.join > relation.super_type.level.join
-                  relation.super_type
+                if lowest.level.join > upest.level.join
+                  upest
                 else
-                  relation.sub_type
+                  lowest
                 end
               end
 
@@ -344,16 +360,33 @@ def to_s
       def constraint(var_name)
         upper_bound = upper_bound(var_name)
         lower_bound = lower_bound(var_name)
-
-        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
+        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
-          [lower_bound, upper_bound]
+          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
 
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 34f42fdfa..56dd8dab9 100644
--- a/sig/steep/subtyping/constraints.rbs
+++ b/sig/steep/subtyping/constraints.rbs
@@ -95,8 +95,6 @@ module Steep
 
       def empty?: () -> bool
 
-      def sub_constraints: () -> Constraints
-
       # Returns the upper bound of the variable
       #
       # If the variable is not constrained, it returns `top` type.
@@ -111,6 +109,8 @@ module Steep
 
       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
@@ -129,7 +129,7 @@ module Steep
       # 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) -> ([AST::Types::t, AST::Types::t] | AST::Types::t | nil)
+      def constraint: (Symbol var_name) -> (Array[Relation[AST::Types::t]] | AST::Types::t | nil)
 
       private
 
diff --git a/test/constraints_test.rb b/test/constraints_test.rb
index 45322c239..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])
@@ -91,8 +56,12 @@ 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_generics_upper_bound(:X, parse_type("::_Indexable[::Integer]"))
       constraints.add(:X, super_type: parse_type("::Array[::Integer]"))
@@ -154,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/type_check_test.rb b/test/type_check_test.rb
index 655015c9f..76779a61f 100644
--- a/test/type_check_test.rb
+++ b/test/type_check_test.rb
@@ -2659,4 +2659,49 @@ def +: (Integer) -> Complex
       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