Fix type inference

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"

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)

lib/steep/subtyping/constraints.rb

@@ -73,36 +73,27 @@ 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
 
       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