module TypeProf::Core
  $box_counts = Hash.new(0)
  class Box
    def initialize(node)
      @node = node
      @changes = ChangeSet.new(node, self)
      @destroyed = false
      $box_counts[Box] += 1
      $box_counts[self.class] += 1
    end

    attr_reader :changes

    attr_reader :node, :destroyed

    def destroy(genv)
      $box_counts[self.class] -= 1
      $box_counts[Box] -= 1
      @destroyed = true
      destroy_symbol_proc_call_boxes(genv)
      @changes.reinstall(genv) # rollback all changes
    end

    def reuse(new_node)
      @node = new_node
      @changes.reuse(new_node)
    end

    def on_type_added(genv, src_tyvar, added_types)
      genv.add_run(self)
    end

    def on_type_removed(genv, src_tyvar, removed_types)
      genv.add_run(self)
    end

    def run(genv)
      return if @destroyed
      run0(genv, @changes)
      @changes.reinstall(genv)
    end

    def run0(genv, changes)
      raise NotImplementedError
    end

    def add_symbol_proc_call_box(_changes, genv, sym, caller_positionals, caller_keywords = nil)
      return if caller_positionals.empty?

      recv = caller_positionals.first
      positionals = caller_positionals[1..]
      @symbol_proc_call_boxes ||= {}
      @symbol_proc_call_boxes[[recv, sym, *positionals, caller_keywords]] ||= begin
        a_args = ActualArguments.new(positionals, ::Array.new(positionals.size, false), caller_keywords, nil)
        MethodCallBox.new(@node, genv, recv, sym, a_args, false)
      end
    end

    def destroy_symbol_proc_call_boxes(genv)
      return unless @symbol_proc_call_boxes
      @symbol_proc_call_boxes.each_value { |box| box.destroy(genv) }
      @symbol_proc_call_boxes = nil
    end

    def to_s
      "#{ self.class.to_s.split("::").last }#{ @id ||= $new_id += 1 }"
    end

    alias inspect to_s
  end

  class ConstReadBox < Box
    def initialize(node, genv, const_read)
      super(node)
      @const_read = const_read
      const_read.followers << self
      @ret = Vertex.new(node)
      genv.add_run(self)
    end

    attr_reader :node, :const_read, :ret

    def run0(genv, changes)
      cdef = @const_read.cdef
      if cdef
        changes.add_depended_value_entity(cdef)
        changes.add_edge(genv, cdef.vtx, @ret)
      end
    end
  end

  class TypeReadBox < Box
    def initialize(node, genv, rbs_type)
      super(node)
      @rbs_type = rbs_type
      @ret = Vertex.new(node)
      genv.add_run(self)
    end

    attr_reader :node, :rbs_type, :ret

    def run0(genv, changes)
      # Create substitution map for type parameters if we're in a SigInstanceVariableNode within a generic class
      subst = {}
      if @node.is_a?(AST::SigInstanceVariableNode) && @node.cpath
        mod = genv.resolve_cpath(@node.cpath)
        if mod.type_params && !mod.type_params.empty?
          # Create a substitution map where each type parameter maps to a type variable vertex
          subst = mod.type_params.to_h do |param, _default_ty|
            type_var_vtx = Vertex.new(@node)
            [param, type_var_vtx]
          end
        end
      end

      vtx = @rbs_type.covariant_vertex(genv, changes, subst)
      changes.add_edge(genv, vtx, @ret)
    end
  end

  class OverloadSet
    include Enumerable

    def initialize(method_types)
      @method_types = method_types
    end

    def each(&blk) = @method_types.each(&blk)
    def map(&blk)  = @method_types.map(&blk)
    def first      = @method_types.first
    def size       = @method_types.size
    def to_a       = @method_types

    # lazy cache: combination(2) for all-pair comparison
    def overloads_differ_in_args?
      return @overloads_differ_in_args if defined?(@overloads_differ_in_args)
      @overloads_differ_in_args = !@method_types.combination(2).all? { |a, b|
        positionals_match?(a, b) && keywords_match?(a, b)
      }
    end

    def overloads_differ_at_top_level?
      return @overloads_differ_at_top_level if defined?(@overloads_differ_at_top_level)
      @overloads_differ_at_top_level = !@method_types.combination(2).all? { |a, b|
        positionals_match_shallow?(a, b) && keywords_match_shallow?(a, b)
      }
    end

    # lazy cache: overloads split into fixed-arity ones and rest-positional ones
    def partition_by_rest_positionals
      @partition_by_rest_positionals ||=
        @method_types.partition {|method_type| !method_type.rest_positionals }
    end

    private

    # Check if two method types have structurally identical positional
    # parameter types (req, opt, rest).
    def positionals_match?(mt1, mt2)
      return false unless mt1.req_positionals.size == mt2.req_positionals.size
      return false unless mt1.opt_positionals.size == mt2.opt_positionals.size
      return false unless mt1.rest_positionals.nil? == mt2.rest_positionals.nil?
      mt1.req_positionals.zip(mt2.req_positionals).all? {|a, b| sig_types_match?(a, b) } &&
        mt1.opt_positionals.zip(mt2.opt_positionals).all? {|a, b| sig_types_match?(a, b) } &&
        (mt1.rest_positionals.nil? || sig_types_match?(mt1.rest_positionals, mt2.rest_positionals))
    end

    # Check if two method types have identical positional parameter
    # types at the top level (ignoring type parameter contents).
    def positionals_match_shallow?(mt1, mt2)
      return false unless mt1.req_positionals.size == mt2.req_positionals.size
      return false unless mt1.opt_positionals.size == mt2.opt_positionals.size
      return false unless mt1.rest_positionals.nil? == mt2.rest_positionals.nil?
      mt1.req_positionals.zip(mt2.req_positionals).all? {|a, b| sig_types_match_shallow?(a, b) } &&
        mt1.opt_positionals.zip(mt2.opt_positionals).all? {|a, b| sig_types_match_shallow?(a, b) } &&
        (mt1.rest_positionals.nil? || sig_types_match_shallow?(mt1.rest_positionals, mt2.rest_positionals))
    end

    # Check if two method types have structurally identical keyword
    # parameter types (req, opt, rest).
    def keywords_match?(mt1, mt2)
      return false unless mt1.req_keyword_keys == mt2.req_keyword_keys
      return false unless mt1.opt_keyword_keys == mt2.opt_keyword_keys
      return false unless mt1.rest_keywords.nil? == mt2.rest_keywords.nil?
      mt1.req_keyword_values.zip(mt2.req_keyword_values).all? {|a, b| sig_types_match?(a, b) } &&
        mt1.opt_keyword_values.zip(mt2.opt_keyword_values).all? {|a, b| sig_types_match?(a, b) } &&
        (mt1.rest_keywords.nil? || sig_types_match?(mt1.rest_keywords, mt2.rest_keywords))
    end

    # Shallow version: compare keyword keys and structure, but use
    # shallow type comparison for values.
    def keywords_match_shallow?(mt1, mt2)
      return false unless mt1.req_keyword_keys == mt2.req_keyword_keys
      return false unless mt1.opt_keyword_keys == mt2.opt_keyword_keys
      return false unless mt1.rest_keywords.nil? == mt2.rest_keywords.nil?
      mt1.req_keyword_values.zip(mt2.req_keyword_values).all? {|a, b| sig_types_match_shallow?(a, b) } &&
        mt1.opt_keyword_values.zip(mt2.opt_keyword_values).all? {|a, b| sig_types_match_shallow?(a, b) } &&
        (mt1.rest_keywords.nil? || sig_types_match_shallow?(mt1.rest_keywords, mt2.rest_keywords))
    end

    # Structural equality check for two SigTyNode objects.
    def sig_types_match?(a, b)
      return false unless a.class == b.class
      case a
      when AST::SigTyInstanceNode, AST::SigTyInterfaceNode
        a.cpath == b.cpath &&
          a.args.size == b.args.size &&
          a.args.zip(b.args).all? {|x, y| sig_types_match?(x, y) }
      when AST::SigTySingletonNode
        a.cpath == b.cpath
      when AST::SigTyTupleNode, AST::SigTyUnionNode, AST::SigTyIntersectionNode
        a.types.size == b.types.size &&
          a.types.zip(b.types).all? {|x, y| sig_types_match?(x, y) }
      when AST::SigTyRecordNode
        a.fields.size == b.fields.size &&
          a.fields.all? {|k, v| b.fields[k] && sig_types_match?(v, b.fields[k]) }
      when AST::SigTyOptionalNode, AST::SigTyProcNode
        sig_types_match?(a.type, b.type)
      when AST::SigTyVarNode
        a.var == b.var
      when AST::SigTyLiteralNode
        a.lit == b.lit
      when AST::SigTyAliasNode
        a.cpath == b.cpath && a.name == b.name &&
          a.args.size == b.args.size &&
          a.args.zip(b.args).all? {|x, y| sig_types_match?(x, y) }
      else
        true # Leaf types (bool, nil, self, void, untyped, etc.)
      end
    end

    # Shallow structural equality: compare only the top-level type
    # identity without recursing into type parameters.
    def sig_types_match_shallow?(a, b)
      return false unless a.class == b.class
      case a
      when AST::SigTyInstanceNode, AST::SigTyInterfaceNode
        a.cpath == b.cpath
      when AST::SigTySingletonNode
        a.cpath == b.cpath
      when AST::SigTyTupleNode
        a.types.size == b.types.size
      when AST::SigTyUnionNode, AST::SigTyIntersectionNode
        a.types.size == b.types.size &&
          a.types.zip(b.types).all? {|x, y| sig_types_match_shallow?(x, y) }
      when AST::SigTyRecordNode
        a.fields.keys.sort == b.fields.keys.sort
      when AST::SigTyOptionalNode, AST::SigTyProcNode
        true
      when AST::SigTyVarNode
        a.var == b.var
      when AST::SigTyLiteralNode
        a.lit == b.lit
      when AST::SigTyAliasNode
        a.cpath == b.cpath && a.name == b.name
      else
        true
      end
    end
  end

  class MethodDeclBox < Box
    def initialize(node, genv, cpath, singleton, mid, method_types, overloading)
      super(node)
      @cpath = cpath
      @singleton = singleton
      @mid = mid
      @method_types = method_types
      @overloading = overloading
      @ret = Source.new

      me = genv.resolve_method(@cpath, @singleton, @mid)
      me.add_decl(self)
      me.add_run_all_method_call_boxes(genv)
      me.add_run_all_mdefs(genv)
    end

    attr_accessor :node

    attr_reader :cpath, :singleton, :mid, :method_types, :overloading, :ret

    def destroy(genv)
      me = genv.resolve_method(@cpath, @singleton, @mid)
      me.remove_decl(self)
      me.add_run_all_method_call_boxes(genv)
      destroy_symbol_proc_call_boxes(genv)
    end

    def match_arguments?(genv, changes, param_map, a_args, method_type)
      # TODO: handle a tuple as a splat argument?
      if a_args.splat_flags.any?
        return false unless method_type.rest_positionals
        method_type.req_positionals.size.times do |i|
          return false if a_args.splat_flags[i]
        end
        method_type.post_positionals.size.times do |i|
          return false if a_args.splat_flags[-i - 1]
        end
      else
        actual = a_args.positionals.size
        required_formal = method_type.req_positionals.size + method_type.post_positionals.size
        if actual < required_formal
          # too few actual arguments
          return false
        end
        if !method_type.rest_positionals && actual > required_formal + method_type.opt_positionals.size
          # too many actual arguments
          return false
        end
      end

      method_type.req_positionals.each_with_index do |ty, i|
        return false unless ty.typecheck(genv, changes, a_args.positionals[i], param_map)
      end
      method_type.post_positionals.each_with_index do |ty, i|
        i -= method_type.post_positionals.size
        return false unless ty.typecheck(genv, changes, a_args.positionals[i], param_map)
      end

      start_rest = method_type.req_positionals.size
      end_rest = a_args.positionals.size - method_type.post_positionals.size

      i = 0
      while i < method_type.opt_positionals.size && start_rest < end_rest
        break if a_args.splat_flags[start_rest]
        return false unless method_type.opt_positionals[i].typecheck(genv, changes, a_args.positionals[start_rest], param_map)
        i += 1
        start_rest += 1
      end

      if start_rest < end_rest
        vtxs = a_args.get_rest_args(genv, changes, start_rest, end_rest)
        while i < method_type.opt_positionals.size
          ty = method_type.opt_positionals[i]
          return false if vtxs.any? {|vtx| !ty.typecheck(genv, changes, vtx, param_map) }
          i += 1
        end
        if method_type.rest_positionals
          return false if vtxs.any? {|vtx| !method_type.rest_positionals.typecheck(genv, changes, vtx, param_map) }
        end
      end

      # Check keyword arguments by inspecting the keywords vertex types
      # directly. We avoid get_keyword_arg here because it creates a fresh
      # Vertex each call, which would destabilize the change-set edges and
      # cause oscillation when match_arguments? runs on every box re-eval.
      if a_args.keywords
        method_type.req_keyword_keys.zip(method_type.req_keyword_values) do |key, ty|
          return false unless keyword_arg_typecheck?(genv, changes, a_args.keywords, key, ty, param_map)
        end
        method_type.opt_keyword_keys.zip(method_type.opt_keyword_values) do |key, ty|
          return false unless keyword_arg_typecheck?(genv, changes, a_args.keywords, key, ty, param_map)
        end
        if method_type.rest_keywords
          return false unless rest_keyword_args_typecheck?(genv, changes, a_args.keywords, method_type, param_map)
        end
      end

      return true
    end

    def resolve_overload(changes, genv, method_type, node, param_map, a_args, ret, force)
      param_map0 = param_map.dup
      if method_type.type_params
        method_type.type_params.zip(yield(method_type)) do |(var, _default_ty), vtx|
          param_map0[var] = vtx # TODO: default_ty?
        end
      end

      unless match_arguments?(genv, changes, param_map0, a_args, method_type)
        if force
          meth = node.mid_code_range ? :mid_code_range : :code_range
          changes.add_diagnostic(meth, "wrong type of arguments") # XXX: more friendly and fine-grained error message
        end
        return false
      end

      rbs_blk = method_type.block
      if method_type.block_required && !a_args.block
        if force
          meth = node.mid_code_range ? :mid_code_range : :code_range
          changes.add_diagnostic(meth, "block is expected") # XXX: more friendly error message
        end
        return false
      end
      if !rbs_blk && a_args.block
        if force
          meth = node.mid_code_range ? :mid_code_range : :code_range
          changes.add_diagnostic(meth, "block is not expected") # XXX: more friendly error message
        end
        return false
      end

      if rbs_blk && a_args.block
        # rbs_blk_func.optional_keywords, ...
        blk_a_args = rbs_blk.req_positionals.map do |blk_a_arg|
          blk_a_arg.covariant_vertex(genv, changes, param_map0)
        end
        a_args.block.each_type do |ty|
          case ty
          when Type::Proc
            ty.block.accept_args(genv, changes, blk_a_args)

            if ty.block.is_a?(Block)
              ty.block.next_boxes.each do |next_box|
                unless rbs_blk.return_type.typecheck(genv, changes, next_box.a_ret, param_map0)
                  next_box.wrong_return_type(rbs_blk.return_type.show, changes)
                end
              end
            end
          when Type::Symbol
            resolve_symbol_proc(changes, genv, ty.sym, blk_a_args, rbs_blk, param_map0)
          end
        end
      end

      force = true
      return true

    ensure
      if force
        ret_vtx = method_type.return_type.covariant_vertex(genv, changes, param_map0)
        changes.add_edge(genv, ret_vtx, ret)
      end
    end

    def resolve_symbol_proc(changes, genv, sym, blk_a_args, rbs_blk, param_map)
      box = add_symbol_proc_call_box(changes, genv, sym, blk_a_args)
      return unless box

      rbs_blk.return_type.typecheck(genv, changes, box.ret, param_map)
    end

    def resolve_overloads(changes, genv, node, param_map, a_args, ret, &blk)
      if @method_types.size == 1
        method_type = @method_types.first
        resolve_overload(changes, genv, method_type, node, param_map, a_args, ret, true, &blk)
        return
      end

      # If any positional argument has no type information, we cannot
      # determine which overload to select. Return silently (untyped)
      # rather than attempting to match. This prevents oscillation in
      # cyclic cases and avoids false "failed to resolve overloads"
      # diagnostics for untyped arguments.
      #
      # We check at two levels:
      # 1. Top-level empty vertices are always uninformative.
      # 2. Empty type parameter vertices (e.g., Array[T] where T is
      #    empty) are only uninformative when overloads differ solely
      #    in their type parameters (e.g., Array[Integer] vs
      #    Array[String]). When overloads differ at the top level
      #    (e.g., Integer vs Float), the type parameter contents are
      #    irrelevant for overload selection and should not trigger
      #    bail-out.
      has_uninformative_args = if @method_types.overloads_differ_in_args?
        # Check whether overloads also differ at the top level (e.g.,
        # Integer vs Float) or only in their type parameters (e.g.,
        # Array[Integer] vs Array[String]).
        if @method_types.overloads_differ_at_top_level?
          # Overloads are distinguished by top-level types.
          # Only top-level empty vertices matter; empty type parameters
          # are irrelevant for overload selection.
          # However, splatted arguments have their elements extracted
          # during matching, so also check splat element vertices.
          a_args.positionals.any? {|vtx| vtx.types.empty? } ||
            splat_elements_uninformative?(genv, a_args) ||
            (a_args.keywords && a_args.keywords.types.empty?)
        else
          # Overloads differ only in type parameters (e.g.,
          # Array[Integer] vs Array[String]). Empty type parameter
          # vertices can cause oscillation, so check recursively.
          a_args.positionals.any? {|vtx| vertex_uninformative?(genv, vtx) } ||
            (a_args.keywords && vertex_uninformative?(genv, a_args.keywords))
        end
      else
        a_args.positionals.any? {|vtx| vtx.types.empty? } ||
          (a_args.keywords && a_args.keywords.types.empty?)
      end
      if has_uninformative_args
        a_args.positionals.each do |vtx|
          changes.add_edge(genv, vtx, changes.target)
        end
        # Note: keywords already have a permanent edge to the box
        # (established in MethodCallBox#initialize), so no extra edge needed.
        return
      end

      # A splatted call can match only a rest-positional overload; otherwise prefer
      # the fixed-arity ones, as a rest-positional one is usually a catch-all
      overload_groups =
        a_args.splat_flags.any? ? [@method_types] : @method_types.partition_by_rest_positionals

      match_any_overload = false
      overload_groups.each do |method_types|
        method_types.each do |method_type|
          if resolve_overload(changes, genv, method_type, node, param_map, a_args, ret, false, &blk)
            match_any_overload = true
          end
        end
        break if match_any_overload
      end
      unless match_any_overload
        meth = node.mid_code_range ? :mid_code_range : :code_range
        changes.add_diagnostic(meth, "failed to resolve overloads")
      end
    end

    # Check if any splatted argument has an Array element vertex
    # that is empty. Splat expansion extracts elements during
    # overload matching, so empty element types can cause oscillation
    # even when the top-level Array type is present.
    def splat_elements_uninformative?(genv, a_args)
      a_args.positionals.each_with_index do |vtx, i|
        next unless a_args.splat_flags[i]
        vtx.each_type do |ty|
          base = ty.base_type(genv)
          if base.is_a?(Type::Instance) && base.mod == genv.mod_ary && base.args[0]
            return true if base.args[0].types.empty?
          end
        end
      end
      false
    end

    def vertex_uninformative?(genv, vtx, depth = 0)
      return true if vtx.types.empty?
      return false if depth > 3
      vtx.each_type do |ty|
        base = ty.base_type(genv)
        next unless base.is_a?(Type::Instance) && !base.args.empty?
        base.args.each do |arg_vtx|
          return true if arg_vtx && vertex_uninformative?(genv, arg_vtx, depth + 1)
        end
      end
      false
    end

    # Typecheck a single keyword argument value against the expected type
    # by directly inspecting the pre-existing value vertices in the
    # keywords vertex's types (Record, Hash, Instance).
    def keyword_arg_typecheck?(genv, changes, keywords_vtx, key, expected_ty, param_map)
      keywords_vtx.each_type do |kw_ty|
        val_vtx = case kw_ty
        when Type::Hash then kw_ty.get_value(key)
        when Type::Record then kw_ty.get_value(key)
        when Type::Instance then kw_ty.mod == genv.mod_hash ? kw_ty.args[1] : nil
        else nil
        end
        return false if val_vtx && !expected_ty.typecheck(genv, changes, val_vtx, param_map)
      end
      true
    end

    # Typecheck rest keyword argument values (those not consumed by named
    # keywords) against the method type's rest_keywords type.
    def rest_keyword_args_typecheck?(genv, changes, keywords_vtx, method_type, param_map)
      named_keys = method_type.req_keyword_keys + method_type.opt_keyword_keys
      rest_ty = method_type.rest_keywords
      keywords_vtx.each_type do |kw_ty|
        case kw_ty
        when Type::Record
          kw_ty.fields.each do |key, val_vtx|
            next if named_keys.include?(key)
            return false unless rest_ty.typecheck(genv, changes, val_vtx, param_map)
          end
        when Type::Hash
          val_vtx = kw_ty.base_type(genv).args[1]
          return false if val_vtx && !rest_ty.typecheck(genv, changes, val_vtx, param_map)
        when Type::Instance
          if kw_ty.mod == genv.mod_hash && kw_ty.args[1]
            return false unless rest_ty.typecheck(genv, changes, kw_ty.args[1], param_map)
          end
        end
      end
      true
    end

    def show
      @method_types.map do |method_type|
        args = []
        method_type.req_positionals.each do |arg|
          args << arg.show
        end
        method_type.opt_positionals.each do |arg|
          args << "?#{arg.show}"
        end
        if method_type.rest_positionals
          args << "*#{method_type.rest_positionals.show}"
        end
        method_type.post_positionals.each do |arg|
          args << arg.show
        end

        method_type.req_keyword_keys.zip(method_type.req_keyword_values) do |key, arg|
          args << "#{ key }: #{arg.show}"
        end
        method_type.opt_keyword_keys.zip(method_type.opt_keyword_values) do |key, arg|
          args << "?#{ key }: #{arg.show}"
        end
        if method_type.rest_keywords
          args << "**#{method_type.rest_keywords.show}"
        end

        s = args.empty? ? "-> " : "(#{ args.join(", ") }) -> "
        s += method_type.return_type.show
      end.join(" | ")
    end
  end

  class EscapeBox < Box
    def initialize(node, genv, a_ret)
      super(node)
      @a_ret = a_ret.new_vertex(genv, node)
    end

    attr_reader :a_ret

    def ret = @a_ret

    def run0(genv, changes)
      return
    end

    def wrong_return_type(f_ret_show, changes)
      actual_ty = @a_ret.show
      msg = "expected: #{ f_ret_show }; actual: #{ actual_ty }"
      case @node
      when AST::ReturnNode
        changes.add_diagnostic(:code_range, msg, @node)
      when AST::DefNode
        changes.add_diagnostic(:last_stmt_code_range, msg, @node)
      when AST::NextNode
        changes.add_diagnostic(:code_range, msg, @node)
      when AST::CallNode
        changes.add_diagnostic(:block_last_stmt_code_range, msg, @node)
      when AST::AttrReaderMetaNode, AST::AttrAccessorMetaNode
        changes.add_diagnostic(:code_range, msg, @node)
      else
        pp @node.class
      end
    end
  end

  class SplatBox < Box
    def initialize(node, genv, ary, idx, orig = nil)
      super(node)
      @ary = ary
      @idx = idx
      @orig = orig
      @ary.add_edge(genv, self)
      @orig.add_edge(genv, self) if @orig
      @ret = Vertex.new(node)
    end

    attr_reader :ary, :idx, :ret

    def run0(genv, changes)
      @ary.each_type do |ty|
        case ty
        when Type::Instance
          if ty.mod == genv.mod_ary
            changes.add_edge(genv, ty.args[0], @ret)
          else
            "???"
          end
        when Type::Array
          if @idx && @idx < ty.elems.size
            changes.add_edge(genv, ty.elems[@idx], @ret)
          else
            changes.add_edge(genv, ty.get_elem(genv, @idx), @ret)
          end
        else
          "???"
        end
      end
      # For types where to_a is not defined, [*x] wraps x as [x]
      if @orig && @ary.types.empty?
        @orig.each_type do |ty|
          changes.add_edge(genv, Source.new(ty), @ret)
        end
      end
    end
  end

  class HashSplatBox < Box
    def initialize(node, genv, hsh, unified_key, unified_val)
      super(node)
      @hsh = hsh
      @unified_key = unified_key
      @unified_val = unified_val
      @hsh.add_edge(genv, self)
    end

    def ret = @hsh # dummy

    attr_reader :hsh, :unified_key, :unified_val

    def run0(genv, changes)
      @hsh.each_type do |ty|
        ty = ty.base_type(genv)
        if ty.mod == genv.mod_hash
          changes.add_edge(genv, ty.args[0].new_vertex(genv, :__hash_splat), @unified_key)
          changes.add_edge(genv, ty.args[1].new_vertex(genv, :__hash_splat), @unified_val)
        else
          "???"
        end
      end
    end
  end

  class MethodDefBox < Box
    def initialize(node, genv, cpath, singleton, mid, f_args, ret_boxes)
      super(node)
      @cpath = cpath
      @singleton = singleton
      @mid = mid
      raise unless f_args
      @f_args = f_args
      raise unless f_args.is_a?(FormalArguments)

      @record_block = RecordBlock.new(@node)
      if @f_args.block
        record_blk_ty = Source.new(Type::Proc.new(genv, @record_block))
        record_blk_ty.add_edge(genv, @f_args.block)
      end

      @ret_boxes = ret_boxes
      @ret = Vertex.new(node)
      ret_boxes.each do |box|
        @changes.add_edge(genv, box.ret, @ret)
      end
      me = genv.resolve_method(@cpath, @singleton, @mid)
      me.add_def(self)
      me.add_run_all_method_call_boxes(genv) if me.decls.empty?
      genv.add_run(self)
    end

    attr_accessor :node

    attr_reader :cpath, :singleton, :mid, :f_args, :ret, :record_block

    def destroy(genv)
      me = genv.resolve_method(@cpath, @singleton, @mid)
      me.remove_def(self)
      me.add_run_all_method_call_boxes(genv) if me.decls.empty?
      genv.add_run(self)
      super(genv)
    end

    def run0(genv, changes)
      me = genv.resolve_method(@cpath, @singleton, @mid)
      return if me.decls.empty?

      # TODO: support "| ..."
      decl = me.decls.to_a.first
      # TODO: support overload?
      method_type = decl.method_types.first
      _block = method_type.block

      mod = genv.resolve_cpath(@cpath)
      if @singleton
        ty = Type::Singleton.new(genv, mod)
        param_map0 = Type.default_param_map(genv, ty)
      else
        type_params = mod.type_params.map {|(_name, _default_ty)| Source.new() } # TODO: better support
        ty = Type::Instance.new(genv, mod, type_params)
        param_map0 = Type.default_param_map(genv, ty)
        if ty.is_a?(Type::Instance)
          ty.mod.type_params.zip(ty.args) do |(name, _default_ty), arg|
            param_map0[name] = arg
          end
        end
      end
      method_type.type_params.each do |name, _default_ty|
        param_map0[name] = Source.new()
      end

      positional_args = []
      splat_flags = []

      method_type.req_positionals.each do |a_arg|
        positional_args << a_arg.contravariant_vertex(genv, changes, param_map0)
        splat_flags << false
      end
      method_type.opt_positionals.each do |a_arg|
        positional_args << a_arg.contravariant_vertex(genv, changes, param_map0)
        splat_flags << false
      end
      if method_type.rest_positionals
        elems = method_type.rest_positionals.contravariant_vertex(genv, changes, param_map0)
        positional_args << Source.new(genv.gen_ary_type(elems))
        splat_flags << true
      end
      method_type.post_positionals.each do |a_arg|
        positional_args << a_arg.contravariant_vertex(genv, changes, param_map0)
        splat_flags << false
      end

      a_args = ActualArguments.new(positional_args, splat_flags, nil, nil) # TODO: keywords and block
      if pass_arguments(changes, genv, a_args)
        # TODO: block
        f_ret = method_type.return_type.contravariant_vertex(genv, changes, param_map0)
        changes.add_edge(genv, f_ret, @ret)
        @ret_boxes.each do |ret_box|
          unless method_type.return_type.typecheck(genv, changes, ret_box.a_ret, param_map0)
            ret_box.wrong_return_type(method_type.return_type.show, changes)
          end
        end
      end
    end

    def pass_arguments(changes, genv, a_args)
      if a_args.splat_flags.any?
        # there is at least one splat actual argument

        lower = @f_args.req_positionals.size + @f_args.post_positionals.size
        upper = @f_args.rest_positionals ? nil : lower + @f_args.opt_positionals.size
        if upper && upper < a_args.positionals.size
          meth = changes.node.mid_code_range ? :mid_code_range : :code_range
          err = "#{ a_args.positionals.size } for #{ lower }#{ upper ? lower < upper ? "...#{ upper }" : "" : "+" }"
          changes.add_diagnostic(meth, "wrong number of arguments (#{ err })")
          return false
        end

        start_rest = [a_args.splat_flags.index(true), @f_args.req_positionals.size + @f_args.opt_positionals.size].min
        end_rest = [a_args.splat_flags.rindex(true) + 1, a_args.positionals.size - @f_args.post_positionals.size].max
        rest_vtxs = a_args.get_rest_args(genv, changes, start_rest, end_rest)

        @f_args.req_positionals.each_with_index do |f_vtx, i|
          if i < start_rest
            changes.add_edge(genv, a_args.positionals[i], f_vtx)
          else
            rest_vtxs.each do |vtx|
              changes.add_edge(genv, vtx, f_vtx)
            end
          end
        end
        @f_args.opt_positionals.each_with_index do |f_vtx, i|
          i += @f_args.req_positionals.size
          if i < start_rest
            changes.add_edge(genv, a_args.positionals[i], f_vtx)
          else
            rest_vtxs.each do |vtx|
              changes.add_edge(genv, vtx, f_vtx)
            end
          end
        end
        @f_args.post_positionals.each_with_index do |f_vtx, i|
          i += a_args.positionals.size - @f_args.post_positionals.size
          if end_rest <= i
            changes.add_edge(genv, a_args.positionals[i], f_vtx)
          else
            rest_vtxs.each do |vtx|
              changes.add_edge(genv, vtx, f_vtx)
            end
          end
        end

        if @f_args.rest_positionals
          rest_vtxs.each do |vtx|
            @f_args.rest_positionals.each_type do |ty|
              if ty.is_a?(Type::Instance) && ty.mod == genv.mod_ary && ty.args[0]
                changes.add_edge(genv, vtx, ty.args[0])
              end
            end
          end
        end
      else
        # there is no splat actual argument

        lower = @f_args.req_positionals.size + @f_args.post_positionals.size
        upper = @f_args.rest_positionals ? nil : lower + @f_args.opt_positionals.size
        if a_args.positionals.size < lower || (upper && upper < a_args.positionals.size)
          meth = changes.node.mid_code_range ? :mid_code_range : :code_range
          err = "#{ a_args.positionals.size } for #{ lower }#{ upper ? lower < upper ? "...#{ upper }" : "" : "+" }"
          changes.add_diagnostic(meth, "wrong number of arguments (#{ err })")
          return false
        end

        @f_args.req_positionals.each_with_index do |f_vtx, i|
          changes.add_edge(genv, a_args.positionals[i], f_vtx)
        end
        @f_args.post_positionals.each_with_index do |f_vtx, i|
          i -= @f_args.post_positionals.size
          changes.add_edge(genv, a_args.positionals[i], f_vtx)
        end
        start_rest = @f_args.req_positionals.size
        end_rest = a_args.positionals.size - @f_args.post_positionals.size
        i = 0
        while i < @f_args.opt_positionals.size && start_rest < end_rest
          f_arg = @f_args.opt_positionals[i]
          changes.add_edge(genv, a_args.positionals[start_rest], f_arg)
          i += 1
          start_rest += 1
        end

        if start_rest < end_rest
          if @f_args.rest_positionals
            (start_rest..end_rest-1).each do |i|
              @f_args.rest_positionals.each_type do |ty|
                if ty.is_a?(Type::Instance) && ty.mod == genv.mod_ary && ty.args[0]
                  changes.add_edge(genv, a_args.positionals[i], ty.args[0])
                end
              end
            end
          end
        end
      end

      if a_args.keywords
        # TODO: support diagnostics
        @node.req_keywords.zip(@f_args.req_keywords) do |name, f_vtx|
          changes.add_edge(genv, a_args.get_keyword_arg(genv, changes, name), f_vtx)
        end

        @node.opt_keywords.zip(@f_args.opt_keywords).each do |name, f_vtx|
          changes.add_edge(genv, a_args.get_keyword_arg(genv, changes, name), f_vtx)
        end

        if @node.rest_keywords
          named_keys = @node.req_keywords + @node.opt_keywords
          a_args.keywords.each_type do |kw_ty|
            case kw_ty
            when Type::Record
              rest_fields = kw_ty.fields.reject {|key, _| named_keys.include?(key) }
              base = kw_ty.base_type(genv)
              rest_record = Type::Record.new(genv, rest_fields, base)
              changes.add_edge(genv, Source.new(rest_record), @f_args.rest_keywords)
            when Type::Hash, Type::Instance
              changes.add_edge(genv, Source.new(kw_ty), @f_args.rest_keywords)
            end
          end
        end
      end

      return true
    end

    def normalize_keyword_hash_argument_for_def(a_args)
      return a_args unless a_args.keywords
      return a_args if @node.no_keywords
      return a_args if @node.rest_keywords
      return a_args unless @node.req_keywords.empty? && @node.opt_keywords.empty?

      a_args.with_keywords_as_last_positional_hash
    end

    def call(changes, genv, a_args, ret)
      a_args = normalize_keyword_hash_argument_for_def(a_args)
      if pass_arguments(changes, genv, a_args)
        if @node.is_a?(AST::DefNode)
          @node.body.lenv.forward_args&.accept_actual_arguments(genv, changes, a_args)
        end
        changes.add_edge(genv, a_args.block, @f_args.block) if @f_args.block && a_args.block

        changes.add_edge(genv, @ret, ret)
      end
    end

    def show(output_parameter_names)
      block_show = []
      if @record_block.used
        blk_f_args = @record_block.f_args.map {|arg| arg.show }.join(", ")
        blk_ret = @record_block.ret.show
        block_show << "{ (#{ blk_f_args }) -> #{ blk_ret } }"
      end
      args = []
      @f_args.req_positionals.each do |f_vtx|
        args << Type.strip_parens(f_vtx.show)
      end
      @f_args.opt_positionals.each do |f_vtx|
        args << ("?" + Type.strip_parens(f_vtx.show))
      end
      if @f_args.rest_positionals
        args << ("*" + Type.strip_array(Type.strip_parens(@f_args.rest_positionals.show)))
      end
      @f_args.post_positionals.each do |var|
        args << Type.strip_parens(var.show)
      end
      if @node.respond_to?(:req_keywords) &&
         @node.req_keywords.size == @f_args.req_keywords.size &&
         @node.opt_keywords.size == @f_args.opt_keywords.size
        @node.req_keywords.zip(@f_args.req_keywords) do |name, f_vtx|
          args << "#{ name }: #{Type.strip_parens(f_vtx.show)}"
        end
        @node.opt_keywords.zip(@f_args.opt_keywords) do |name, f_vtx|
          args << "?#{ name }: #{Type.strip_parens(f_vtx.show)}"
        end
      end
      if @f_args.rest_keywords
        args << "**#{ Type.extract_hash_value_type(Type.strip_parens(@f_args.rest_keywords.show)) }"
      end

      if output_parameter_names && @node.is_a?(AST::DefNode)
        names = []
        names.concat(@node.req_positionals)
        names.concat(@node.opt_positionals)
        names << @node.rest_positionals if @node.rest_positionals
        names.concat(@node.post_positionals)
        names.concat(@node.req_keywords)
        names.concat(@node.opt_keywords)
        names << @node.rest_keywords if @node.rest_keywords
        args = args.zip(names).map do |arg, name|
          name ? "#{ arg } #{ name }" : arg
        end
      end

      args = args.join(", ")
      s = args.empty? ? [] : ["(#{ args })"]
      s << "#{ block_show.sort.join(" | ") }" unless block_show.empty?
      s << "-> #{ @mid == :initialize ? "void" : @ret.show }"
      s.join(" ")
    end
  end

  class MethodAliasBox < Box
    def initialize(node, genv, cpath, singleton, new_mid, old_mid)
      super(node)
      @cpath = cpath
      @singleton = singleton
      @new_mid = new_mid
      @old_mid = old_mid
      @ret = Source.new(genv.nil_type)

      me = genv.resolve_method(@cpath, @singleton, @new_mid)
      me.add_alias(self, @old_mid)
      me.add_run_all_method_call_boxes(genv) if me.decls.empty?
      genv.add_run(self)
    end

    attr_accessor :node

    attr_reader :cpath, :singleton, :new_mid, :old_mid, :ret

    def destroy(genv)
      me = genv.resolve_method(@cpath, @singleton, @new_mid)
      me.remove_alias(self)
      me.add_run_all_method_call_boxes(genv) if me.decls.empty?
      genv.add_run(self)
      super(genv)
    end

    def run0(genv, changes)
      # TODO: what to do?
    end
  end

  class MethodCallBox < Box
    def initialize(node, genv, recv, mid, a_args, subclasses, suppress_errors: false)
      raise mid.to_s unless mid
      super(node)
      @recv = recv.new_vertex(genv, node)
      @recv.add_edge(genv, self)
      @mid = mid
      @a_args = a_args.new_vertexes(genv, node)
      @a_args.keywords.add_edge(genv, self) if @a_args.keywords
      @a_args.block.add_edge(genv, self) if @a_args.block
      @ret = Vertex.new(node)
      @subclasses = subclasses
      @suppress_errors = suppress_errors
      @generics = {}
    end

    attr_reader :recv, :mid, :ret

    def run0(genv, changes)
      edges = Set.empty
      called_mdefs = Set.empty
      error_count = 0
      resolve(genv, changes) do |me, ty, mid, orig_ty|
        if @node.is_a?(AST::YieldNode) && mid == :call && orig_ty.is_a?(Type::Symbol)
          box = add_symbol_proc_call_box(changes, genv, orig_ty.sym, @a_args.positionals, @a_args.keywords)
          changes.add_edge(genv, box.ret, @ret) if box
        elsif !me
          unless @suppress_errors
            if error_count < 3
              meth = @node.mid_code_range ? :mid_code_range : :code_range
              changes.add_diagnostic(meth, "undefined method: #{ orig_ty.show }##{ mid }")
            end
          end
          error_count += 1
        elsif me.builtin && me.builtin[changes, @node, orig_ty, @a_args, @ret]
          # do nothing
        elsif !me.decls.empty?
          # TODO: support "| ..."
          me.decls.each do |mdecl|
            # TODO: union type is ok?
            # TODO: add_depended_method_entity for types used to resolve overloads
            ty_env = Type.default_param_map(genv, orig_ty)
            if ty.is_a?(Type::Instance)
              ty.mod.type_params.zip(ty.args) do |(param, default_ty), arg|
                ty_env[param] = arg || (default_ty ? default_ty.covariant_vertex(genv, changes, ty_env) : Source.new)
              end
            end
            mdecl.resolve_overloads(changes, genv, @node, ty_env, @a_args, @ret) do |method_type|
              @generics[method_type] ||= method_type.type_params.map { Vertex.new(@node) }
            end
          end
        elsif !me.defs.empty?
          me.defs.each do |mdef|
            next if called_mdefs.include?(mdef)
            called_mdefs << mdef
            mdef.call(changes, genv, @a_args, @ret)
          end
        else
          pp me
          raise
        end
      end
      if @subclasses
        resolve_subclasses(genv, changes) do |recv_ty, me|
          if !me.defs.empty?
            me.defs.each do |mdef|
              next if called_mdefs.include?(mdef)
              called_mdefs << mdef
              mdef.call(changes, genv, @a_args, @ret)
            end
          end
        end
      end
      edges.each do |src, dst|
        changes.add_edge(genv, src, dst)
      end
      if error_count > 3 && !@suppress_errors
        meth = @node.mid_code_range ? :mid_code_range : :code_range
        changes.add_diagnostic(meth, "... and other #{ error_count - 3 } errors")
      end
    end

    def resolve(genv, changes, &blk)
      @recv.each_type do |orig_ty|
        next if orig_ty == genv.bot_type
        if @mid == :"*super"
          mid = @node.lenv.cref.mid
          skip = true
        else
          mid = @mid
          skip = false
        end

        ty = orig_ty.base_type(genv)

        base_ty_env = Type.default_param_map(genv, ty)

        alias_limit = 0
        while ty
          unless skip
            # First check prepended modules
            if !ty.is_a?(Type::Singleton)
              if resolve_prepended_modules(genv, changes, base_ty_env, ty, mid) do |me, ty, mid|
                  yield me, ty, mid, orig_ty
                end
                break
              end
            end

            # Then check the class/module itself
            me = ty.mod.get_method(ty.is_a?(Type::Singleton), mid)
            changes.add_depended_method_entity(me) if changes
            if !me.aliases.empty?
              mid = me.aliases.values.first
              alias_limit += 1
              redo if alias_limit < 5
            end
            if me.exist?
              yield me, ty, mid, orig_ty
              break
            end
          end

          skip = false

          if ty.is_a?(Type::Singleton)
            # TODO: extended modules
          else
            # Finally check included modules
            break if resolve_included_modules(genv, changes, base_ty_env, ty, mid) do |me, ty, mid|
              yield me, ty, mid, orig_ty
            end
          end

          ty = genv.get_superclass_type(ty, changes, base_ty_env)
        end

        yield nil, nil, mid, orig_ty unless ty
      end
    end

    def resolve_prepended_modules(genv, changes, base_ty_env, ty, mid, &blk)
      found = false

      alias_limit = 0
      # Process prepended modules in reverse order (last prepended = first in ancestor chain)
      ty.mod.prepended_modules.reverse_each do |prep_decl, prep_mod|
        if prep_decl.is_a?(AST::SigPrependNode) && prep_mod.type_params
          prep_ty = genv.get_instance_type(prep_mod, prep_decl.args, changes, base_ty_env, ty)
        else
          type_params = prep_mod.type_params.map { Source.new() } # TODO: better support
          prep_ty = Type::Instance.new(genv, prep_mod, type_params)
        end

        me = prep_ty.mod.get_method(false, mid)
        changes.add_depended_method_entity(me) if changes
        if !me.aliases.empty?
          mid = me.aliases.values.first
          alias_limit += 1
          redo if alias_limit < 5
        end
        if me.exist?
          found = true
          yield me, prep_ty, mid
        else
          found = resolve_prepended_modules(genv, changes, base_ty_env, prep_ty, mid, &blk)
        end
        break if found
      end

      found
    end

    def resolve_included_modules(genv, changes, base_ty_env, ty, mid, &blk)
      found = false

      alias_limit = 0
      ty.mod.self_types.each do |(mdecl, idx), self_ty_mod|
        raise unless mdecl.is_a?(AST::SigModuleNode)
        if self_ty_mod.type_params
          self_ty = genv.get_instance_type(self_ty_mod, mdecl.self_type_args[idx], changes, base_ty_env, ty)
        else
          self_ty = Type::Instance.new(genv, self_ty_mod, [])
        end

        me = self_ty.mod.get_method(false, mid)
        changes.add_depended_method_entity(me) if changes
        if !me.aliases.empty?
          mid = me.aliases.values.first
          alias_limit += 1
          redo if alias_limit < 5
        end
        if me.exist?
          found = true
          yield me, self_ty, mid
        else
          found ||= resolve_included_modules(genv, changes, base_ty_env, self_ty, mid, &blk)
        end
      end

      alias_limit = 0
      ty.mod.included_modules.each do |inc_decl, inc_mod|
        if inc_decl.is_a?(AST::SigIncludeNode) && inc_mod.type_params
          inc_ty = genv.get_instance_type(inc_mod, inc_decl.args, changes, base_ty_env, ty)
        else
          type_params = inc_mod.type_params.map { Source.new() } # TODO: better support
          inc_ty = Type::Instance.new(genv, inc_mod, type_params)
        end

        me = inc_ty.mod.get_method(false, mid)
        changes.add_depended_method_entity(me) if changes
        if !me.aliases.empty?
          mid = me.aliases.values.first
          alias_limit += 1
          redo if alias_limit < 5
        end
        if me.exist?
          found = true
          yield me, inc_ty, mid
        else
          found ||= resolve_included_modules(genv, changes, base_ty_env, inc_ty, mid, &blk)
        end
      end
      found
    end

    def resolve_subclasses(genv, changes)
      # TODO: This does not follow new subclasses
      @recv.each_type do |ty|
        next if ty == genv.bot_type
        base_ty = ty.base_type(genv)
        singleton = base_ty.is_a?(Type::Singleton)
        mod = base_ty.mod
        mod.each_descendant do |desc_mod|
          next if mod == desc_mod
          me = desc_mod.get_method(singleton, @mid)
          changes.add_depended_method_entity(me)
          if me && me.exist?
            yield ty, me
          end
        end
      end
    end
  end

  class GVarReadBox < Box
    def initialize(node, genv, name)
      super(node)
      @vtx = genv.resolve_gvar(name).vtx
      @ret = Vertex.new(node)
      genv.add_run(self)
    end

    attr_reader :node, :const_read, :ret

    def run0(genv, changes)
      changes.add_edge(genv, @vtx, @ret)
    end
  end

  class IVarReadBox < Box
    def initialize(node, genv, cpath, singleton, name)
      super(node)
      @cpath = cpath
      @singleton = singleton
      @name = name
      genv.resolve_cpath(cpath).ivar_reads << self
      @proxy = Vertex.new(node)
      @ret = Vertex.new(node)
      genv.add_run(self)
    end

    attr_reader :node, :const_read, :ret

    def destroy(genv)
      genv.resolve_cpath(@cpath).ivar_reads.delete(self)
      super(genv)
    end

    def run0(genv, changes)
      mod = genv.resolve_cpath(@cpath)
      singleton = @singleton
      cur_ive = mod.get_ivar(singleton, @name)
      target_vtx = nil
      target_decls = nil
      genv.each_direct_superclass(mod, singleton) do |mod, singleton|
        ive = mod.get_ivar(singleton, @name)
        # Subscribe to every visited ive so that, if one later acquires an
        # RBS declaration, this box is re-run and switches to the declared
        # type instead of the inferred one.
        changes.add_depended_value_entity(ive)
        if ive.exist?
          target_vtx = ive.vtx
          target_decls = ive.decls unless ive.decls.empty?
          break if target_decls
        end
      end

      if target_decls
        # When declarations exist, return declared types instead of assigned types
        target_decls.each do |decl|
          subst = {}
          if decl.cpath
            decl_mod = genv.resolve_cpath(decl.cpath)
            if decl_mod.type_params && !decl_mod.type_params.empty?
              subst = decl_mod.type_params.to_h do |param, _default_ty|
                [param, Vertex.new(@node)]
              end
            end
          end
          vtx = decl.type.covariant_vertex(genv, changes, subst)
          changes.add_edge(genv, vtx, @ret)
        end
      elsif target_vtx
        edges = []
        if target_vtx != cur_ive.vtx
          edges << [cur_ive.vtx, @proxy] << [@proxy, target_vtx]
        end
        edges << [target_vtx, @ret]
        edges.each do |src, dst|
          changes.add_edge(genv, src, dst)
        end
      end
    end
  end

  class CVarReadBox < Box
    def initialize(node, genv, cpath, name)
      super(node)
      @cpath = cpath
      @name = name
      genv.resolve_cpath(cpath).cvar_reads << self
      @proxy = Vertex.new(node)
      @ret = Vertex.new(node)
      genv.add_run(self)
    end

    attr_reader :node, :const_read, :ret

    def destroy(genv)
      genv.resolve_cpath(@cpath).cvar_reads.delete(self)
      super(genv)
    end

    def run0(genv, changes)
      mod = genv.resolve_cpath(@cpath)
      cur_cve = mod.get_cvar(@name)
      target_vtx = nil
      genv.each_direct_superclass(mod, nil) do |mod, _|
        cve = mod.get_cvar(@name)
        if cve.exist?
          target_vtx = cve.vtx
        end
      end

      edges = []
      if target_vtx
        if target_vtx != cur_cve.vtx
          edges << [cur_cve.vtx, @proxy] << [@proxy, target_vtx]
        end
        edges << [target_vtx, @ret]
      end

      edges.each do |src, dst|
        changes.add_edge(genv, src, dst)
      end
    end
  end

  class MAsgnBox < Box
    def initialize(node, genv, value, lefts, rest_elem, rights)
      super(node)
      @value = value
      @lefts = lefts
      @rest_elem = rest_elem
      @rights = rights
      @value.add_edge(genv, self)
    end

    attr_reader :node, :value, :lefts, :rest_elem, :rights

    def destroy(genv)
      @value.remove_edge(genv, self) # TODO: Is this really needed?
      super(genv)
    end

    def ret = @rhs

    def run0(genv, changes)
      @value.each_type do |ty|
        # TODO: call to_ary?
        case ty
        when Type::Array
          ty.splat_assign(genv, @lefts, @rest_elem, @rights).each do |src, dst|
            changes.add_edge(genv, src, dst)
          end
        when Type::Instance
          if ty.mod == genv.mod_ary && (elem_vtx = ty.args[0])
            @lefts.each {|lhs| changes.add_edge(genv, elem_vtx, lhs) }
            changes.add_edge(genv, elem_vtx, @rest_elem) if @rest_elem
            @rights&.each {|rhs| changes.add_edge(genv, elem_vtx, rhs) }
          else
            lhs = @lefts[0] || (@rights && @rights[0]) || @rest_elem
            changes.add_edge(genv, Source.new(ty), lhs) if lhs
          end
        else
          lhs = @lefts[0] || (@rights && @rights[0]) || @rest_elem
          changes.add_edge(genv, Source.new(ty), lhs) if lhs
        end
      end
    end
  end

  class InstanceTypeBox < Box
    def initialize(node, genv, singleton_ty_vtx)
      super(node)
      @singleton_ty_vtx = singleton_ty_vtx
      @ret = Vertex.new(node)
      genv.add_run(self)
    end

    attr_reader :ret

    def run0(genv, changes)
      instance_tys = []
      @singleton_ty_vtx.each_type do |ty|
        instance_tys << ty.get_instance_type(genv) if ty.is_a?(Type::Singleton)
      end
      source_vtx = Source.new(*instance_tys)
      changes.add_edge(genv, source_vtx, @ret)
    end
  end
end
