module TypeProf::Core
  class AST
    def self.typecheck_for_module(genv, changes, f_mod, f_args, a_vtx, subst)
      changes.add_edge(genv, a_vtx, changes.target)
      found_any = false
      a_vtx.each_type do |ty|
        next if ty.is_a?(Type::Bot)
        found_any = true
        ty = ty.base_type(genv)
        while ty
          if ty.mod == f_mod && ty.is_a?(Type::Instance)
            args_all_match = true
            f_args.zip(ty.args) do |f_arg_node, a_arg_ty|
              unless f_arg_node.typecheck(genv, changes, a_arg_ty, subst)
                args_all_match = false
                break
              end
            end
            return true if args_all_match
          end
          changes.add_depended_superclass(ty.mod)

          if f_mod.module?
            return true if typecheck_for_prepended_modules(genv, changes, ty, f_mod, f_args, subst)
            return true if typecheck_for_included_modules(genv, changes, ty, f_mod, f_args, subst)
          end

          ty = genv.get_superclass_type(ty, changes, {})
        end
      end
      return !found_any
    end

    def self.typecheck_for_prepended_modules(genv, changes, a_ty, f_mod, f_args, subst)
      a_ty.mod.prepended_modules.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, {}, a_ty)
        else
          type_params = prep_mod.type_params.map {|(_name, _default_ty)| Source.new() } # TODO: better support
          prep_ty = Type::Instance.new(genv, prep_mod, type_params)
        end
        if prep_ty.mod == f_mod
          args_all_match = true
          f_args.zip(prep_ty.args) do |f_arg_node, a_arg_ty|
            unless f_arg_node.typecheck(genv, changes, a_arg_ty, subst)
              args_all_match = false
              break
            end
          end
          return true if args_all_match
        end
        changes.add_depended_superclass(prep_ty.mod)

        return true if typecheck_for_prepended_modules(genv, changes, prep_ty, f_mod, f_args, subst)
      end
      return false
    end

    def self.typecheck_for_included_modules(genv, changes, a_ty, f_mod, f_args, subst)
      a_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, {}, a_ty)
        else
          type_params = inc_mod.type_params.map {|(_name, _default_ty)| Source.new() } # TODO: better support
          inc_ty = Type::Instance.new(genv, inc_mod, type_params)
        end
        if inc_ty.mod == f_mod
          args_all_match = true
          f_args.zip(inc_ty.args) do |f_arg_node, a_arg_vtx|
            unless f_arg_node.typecheck(genv, changes, a_arg_vtx, subst)
              args_all_match = false
              break
            end
          end
          return true if args_all_match
        end
        changes.add_depended_superclass(inc_ty.mod)

        return true if typecheck_for_included_modules(genv, changes, inc_ty, f_mod, f_args, subst)
      end
      return false
    end

    class SigFuncType < Node
      def initialize(raw_decl, raw_type_params, raw_block, lenv)
        super(raw_decl, lenv)
        if raw_block
          @block_required = raw_block.required
          @block = AST.create_rbs_func_type(raw_block, nil, nil, lenv)
        else
          @block_required = false
          @block = nil
        end

        # TODO?: param.variance, param.unchecked, param.upper_bound
        @type_params = raw_type_params ? raw_type_params.map {|param| param.name } : nil

        if raw_decl.type.is_a?(RBS::Types::Function)
          @req_positionals = raw_decl.type.required_positionals.map do |ty|
            raise "unsupported argument type: #{ ty.class }" if !ty.is_a?(RBS::Types::Function::Param)
            AST.create_rbs_type(ty.type, lenv)
          end
          @post_positionals = raw_decl.type.trailing_positionals.map do |ty|
            raise "unsupported argument type: #{ ty.class }" if !ty.is_a?(RBS::Types::Function::Param)
            AST.create_rbs_type(ty.type, lenv)
          end
          @opt_positionals = raw_decl.type.optional_positionals.map do |ty|
            raise "unsupported argument type: #{ ty.class }" if !ty.is_a?(RBS::Types::Function::Param)
            AST.create_rbs_type(ty.type, lenv)
          end
          param = raw_decl.type.rest_positionals
          @rest_positionals = param ? AST.create_rbs_type(param.type, lenv) : nil

          @req_keyword_keys = []
          @req_keyword_values = []
          raw_decl.type.required_keywords.each do |key, ty|
            raise "unsupported argument type: #{ ty.class }" if !ty.is_a?(RBS::Types::Function::Param)
            @req_keyword_keys << key
            @req_keyword_values << AST.create_rbs_type(ty.type, lenv)
          end
          @opt_keyword_keys = []
          @opt_keyword_values = []
          raw_decl.type.optional_keywords.each do |key, ty|
            raise "unsupported argument type: #{ ty.class }" if !ty.is_a?(RBS::Types::Function::Param)
            @opt_keyword_keys << key
            @opt_keyword_values << AST.create_rbs_type(ty.type, lenv)
          end
          param = raw_decl.type.rest_keywords
          @rest_keywords = param ? AST.create_rbs_type(param.type, lenv) : nil
        else
          # RBS::Types::UntypedFunction
          @req_positionals = []
          @post_positionals = []
          @opt_positionals = []
          @rest_positionals = SigTyBaseAnyNode.new(raw_decl, lenv)
          @req_keyword_keys = []
          @req_keyword_values = []
          @opt_keyword_keys = []
          @opt_keyword_values = []
          @rest_keywords = nil
        end

        @return_type = AST.create_rbs_type(raw_decl.type.return_type, lenv)
      end

      attr_reader :type_params, :block, :block_required
      attr_reader :req_positionals
      attr_reader :post_positionals
      attr_reader :opt_positionals
      attr_reader :rest_positionals
      attr_reader :req_keyword_keys
      attr_reader :req_keyword_values
      attr_reader :opt_keyword_keys
      attr_reader :opt_keyword_values
      attr_reader :rest_keywords
      attr_reader :return_type

      def subnodes = {
        block:,
        req_positionals:,
        post_positionals:,
        opt_positionals:,
        rest_positionals:,
        req_keyword_values:,
        opt_keyword_values:,
        rest_keywords:,
        return_type:,
      }
      def attrs = {
        type_params:,
        req_keyword_keys:,
        opt_keyword_keys:,
        block_required:,
      }
    end

    class SigTyNode < Node
      def covariant_vertex(genv, changes, subst)
        vtx = changes.new_covariant_vertex(genv, self)
        covariant_vertex0(genv, changes, vtx, subst)
        vtx
      end

      def contravariant_vertex(genv, changes, subst)
        vtx = changes.new_contravariant_vertex(genv, self)
        contravariant_vertex0(genv, changes, vtx, subst)
        vtx
      end
    end

    class SigTyBaseBoolNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.true_type, genv.false_type), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.true_type, genv.false_type), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_edge(genv, vtx, changes.target)
        vtx.each_type do |ty|
          next if ty.is_a?(Type::Bot)
          return false unless ty == genv.true_type || ty == genv.false_type
        end
        true
      end

      def show
        "bool"
      end
    end

    class SigTyBaseNilNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.nil_type), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.nil_type), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_edge(genv, vtx, changes.target)
        vtx.each_type do |ty|
          next if ty.is_a?(Type::Bot)
          return false unless ty == genv.nil_type
        end
        true
      end

      def show
        "nil"
      end
    end

    class SigTyBaseSelfNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, subst[:"*self"], vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, subst[:"*self"], vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        true # TODO: check self type
      end

      def show
        "self"
      end
    end

    class SigTyBaseVoidNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.obj_type), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.obj_type), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        true
      end

      def show
        "void"
      end
    end

    class SigTyBaseAnyNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        #Source.new(genv.obj_type).add_edge(genv, vtx) # TODO
      end

      def typecheck(genv, changes, vtx, subst)
        true
      end

      def show
        "untyped"
      end
    end

    class SigTyBaseTopNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        # TODO
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        # TODO
      end

      def typecheck(genv, changes, vtx, subst)
        true
      end

      def show
        "top"
      end
    end

    class SigTyBaseBottomNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.bot_type), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.bot_type), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_edge(genv, vtx, changes.target)
        vtx.types.empty?
      end

      def show
        "bot"
      end
    end

    class SigTyBaseInstanceNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, subst[:"*instance"], vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, subst[:"*instance"], vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        true # TODO: implement
      end

      def show
        "instance"
      end
    end

    class SigTyBaseClassNode < SigTyNode
      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, subst[:"*class"], vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, subst[:"*class"], vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        true # TODO: implement
      end

      def show
        "class"
      end
    end

    class SigTyAliasNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        name = raw_decl.name
        @cpath = name.namespace.path
        @toplevel = name.namespace.absolute?
        @name = name.name
        @args = raw_decl.args.map {|arg| AST.create_rbs_type(arg, lenv) }
      end

      attr_reader :cpath, :toplevel, :name, :args
      def subnodes = { args: }
      def attrs = { cpath:, toplevel:, name: }

      def define0(genv)
        @args.each {|arg| arg.define(genv) }

        static_reads = []
        if @cpath.empty?
          static_reads << BaseTypeAliasRead.new(genv, @name, @toplevel ? CRef::Toplevel : @lenv.cref, false)
        else
          static_reads << BaseConstRead.new(genv, @cpath.first, @toplevel ? CRef::Toplevel : @lenv.cref, false)
          @cpath[1..].each do |cname|
            static_reads << ScopedConstRead.new(cname, static_reads.last, false)
          end
          static_reads << ScopedTypeAliasRead.new(@name, static_reads.last, false)
        end
        static_reads
      end

      def undefine0(genv)
        @static_ret.each do |static_read|
          static_read.destroy(genv)
        end
        @args.each {|arg| arg.undefine(genv) }
      end

      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        tae = @static_ret.last.type_alias_entity
        if tae && tae.exist?
          # Check for recursive expansion
          expansion_key = [@cpath, @name]
          subst[:__expansion_stack__] ||= []

          if subst[:__expansion_stack__].include?(expansion_key)
            # Recursive expansion detected: this type alias references itself
            # Stop expansion here to prevent SystemStackError. The type system
            # will handle the incomplete expansion gracefully, typically by
            # treating unresolved recursive references as 'untyped', which
            # maintains type safety while allowing the program to continue.
            return
          end

          # need to check tae decls are all consistent?
          decl = tae.decls.each {|decl| break decl }
          subst0 = subst.dup
          subst0[:__expansion_stack__] = subst[:__expansion_stack__].dup + [expansion_key]

          # raise if decl.params.size != @args.size # ?
          decl.params.zip(@args) do |param, arg|
            subst0[param] = arg.covariant_vertex(genv, changes, subst0) # passing subst0 is ok?
          end
          tae.type.covariant_vertex0(genv, changes, vtx, subst0)
        end
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        tae = @static_ret.last.type_alias_entity
        if tae && tae.exist?
          # Check for recursive expansion
          expansion_key = [@cpath, @name]
          subst[:__expansion_stack__] ||= []

          if subst[:__expansion_stack__].include?(expansion_key)
            # Recursive expansion detected: this type alias references itself
            # Stop expansion here to prevent SystemStackError. The type system
            # will handle the incomplete expansion gracefully, typically by
            # treating unresolved recursive references as 'untyped', which
            # maintains type safety while allowing the program to continue.
            return
          end

          # need to check tae decls are all consistent?
          decl = tae.decls.each {|decl| break decl }
          subst0 = subst.dup
          subst0[:__expansion_stack__] = subst[:__expansion_stack__].dup + [expansion_key]

          # raise if decl.params.size != @args.size # ?
          decl.params.zip(@args) do |param, arg|
            subst0[param] = arg.contravariant_vertex(genv, changes, subst0)
          end
          tae.type.contravariant_vertex0(genv, changes, vtx, subst0)
        end
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        tae = @static_ret.last.type_alias_entity
        if tae && tae.exist?
          # TODO: check for recursive expansion
          decl = tae.decls.each {|decl| break decl }
          subst0 = subst.dup
          decl.params.zip(@args) do |param, arg|
            if arg.is_a?(SigTyVarNode) && subst[arg.var]
              # Share the vertex so that the types inferred in the alias body flow
              # back into the variable, which makes `U` of `(array[U])` inferrable
              subst0[param] = subst[arg.var]
            else
              subst0[param] = arg.covariant_vertex(genv, changes, subst0)
            end
          end
          tae.type.typecheck(genv, changes, vtx, subst0)
        end
      end

      def show
        "(...alias...)"
      end
    end

    class SigTyUnionNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @types = (raw_decl.types || []).map {|type| AST.create_rbs_type(type, lenv) }
      end

      attr_reader :types

      def subnodes = { types: }

      def covariant_vertex0(genv, changes, vtx, subst)
        @types.each do |type|
          type.covariant_vertex0(genv, changes, vtx, subst)
        end
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        @types.each do |type|
          type.contravariant_vertex0(genv, changes, vtx, subst)
        end
      end

      def typecheck(genv, changes, vtx, subst)
        @types.each do |type|
          return true if type.typecheck(genv, changes, vtx, subst)
        end
        false
      end

      def show
        @types.map {|ty| ty.show }.join(" | ")
      end
    end

    class SigTyIntersectionNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @types = (raw_decl.types || []).map {|type| AST.create_rbs_type(type, lenv) }
      end

      attr_reader :types

      def subnodes = { types: }

      def covariant_vertex0(genv, changes, vtx, subst)
        @types.each do |type|
          type.covariant_vertex0(genv, changes, vtx, subst)
        end
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        @types.each do |type|
          type.contravariant_vertex0(genv, changes, vtx, subst)
        end
      end

      def typecheck(genv, changes, vtx, subst)
        @types.each do |type|
          return false unless type.typecheck(genv, changes, vtx, subst)
        end
        true
      end

      def show
        @types.map {|ty| ty.show }.join(" & ")
      end
    end

    class SigTySingletonNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        name = raw_decl.name
        @cpath = name.namespace.path + [name.name]
        @toplevel = name.namespace.absolute?
        # RBS::Types::ClassSingleton#args was added in RBS 4.0
        @args = raw_decl.respond_to?(:args) ? raw_decl.args.map {|arg| AST.create_rbs_type(arg, lenv) } : []
      end

      attr_reader :cpath, :toplevel
      def attrs = { cpath:, toplevel: }

      def define0(genv)
        const_reads = []
        const_read = BaseConstRead.new(genv, @cpath.first, @toplevel ? CRef::Toplevel : @lenv.cref, false)
        const_reads << const_read
        unless @cpath.empty?
          @cpath[1..].each do |cname|
            const_read = ScopedConstRead.new(cname, const_read, false)
            const_reads << const_read
          end
        end
        const_reads
      end

      def undefine0(genv)
        @static_ret.each do |const_read|
          const_read.destroy(genv)
        end
      end

      def covariant_vertex0(genv, changes, vtx, subst)
        # TODO: type.args
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        mod = genv.resolve_cpath(cpath)
        changes.add_edge(genv, Source.new(Type::Singleton.new(genv, mod)), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        # TODO: type.args
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        mod = genv.resolve_cpath(cpath)
        changes.add_edge(genv, Source.new(Type::Singleton.new(genv, mod)), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        f_mod = genv.resolve_cpath(cpath)
        changes.add_edge(genv, vtx, changes.target)
        found_any = false
        vtx.each_type do |ty|
          next if ty.is_a?(Type::Bot)
          found_any = true
          case ty
          when Type::Singleton
            if f_mod.module?
              # TODO: implement
            else
              a_mod = ty.mod
              while a_mod
                return true if a_mod == f_mod
                changes.add_depended_superclass(a_mod)
                a_mod = a_mod.superclass
              end
            end
          end
        end
        !found_any
      end

      def show
        s = "::#{ @cpath.join("::") }"
        if !@args.empty?
          s << "[...]"
        end
        "singleton(#{ s })"
      end
    end

    class SigTyInstanceNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        name = raw_decl.name
        @cpath = name.namespace.path + [name.name]
        @toplevel = name.namespace.absolute? # "::Foo" or "Foo"
        @args = raw_decl.args.map {|arg| AST.create_rbs_type(arg, lenv) }
      end

      attr_reader :cpath, :toplevel, :args
      def subnodes = { args: }
      def attrs = { cpath:, toplevel: }

      def define0(genv)
        @args.each {|arg| arg.define(genv) }
        const_reads = []
        const_read = BaseConstRead.new(genv, @cpath.first, @toplevel ? CRef::Toplevel : @lenv.cref, false)
        const_reads << const_read
        unless @cpath.empty?
          @cpath[1..].each do |cname|
            const_read = ScopedConstRead.new(cname, const_read, false)
            const_reads << const_read
          end
        end
        const_reads
      end

      def undefine0(genv)
        @static_ret.each do |const_read|
          const_read.destroy(genv)
        end
        @args.each {|arg| arg.undefine(genv) }
      end

      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        mod = genv.resolve_cpath(cpath)
        args = @args.map {|arg| arg.covariant_vertex(genv, changes, subst) }
        changes.add_edge(genv, Source.new(Type::Instance.new(genv, mod, args)), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        mod = genv.resolve_cpath(cpath)
        # TODO: report error for wrong type arguments
        # TODO: support default type args
        args = mod.type_params.zip(@args).map do |_, arg|
          arg ? arg.contravariant_vertex(genv, changes, subst) : Source.new
        end
        changes.add_edge(genv, Source.new(Type::Instance.new(genv, mod, args)), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        f_mod = genv.resolve_cpath(cpath)
        AST.typecheck_for_module(genv, changes, f_mod, @args, vtx, subst)
      end

      def show
        cpath = @static_ret.last.cpath
        if cpath
          s = "#{ cpath.join("::") }"
          if !@args.empty?
            s << "[...]"
          end
          s
        else
          "(unknown instance)"
        end
      end
    end

    class SigTyTupleNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @types = raw_decl.types.map {|type| AST.create_rbs_type(type, lenv) }
      end

      attr_reader :types
      def subnodes = { types: }

      def covariant_vertex0(genv, changes, vtx, subst)
        unified_elem = changes.new_covariant_vertex(genv, [self, :Elem]) # TODO
        elems = @types.map do |type|
          nvtx = type.covariant_vertex(genv, changes, subst)
          changes.add_edge(genv, nvtx, unified_elem)
          nvtx
        end
        changes.add_edge(genv, Source.new(Type::Array.new(genv, elems, genv.gen_ary_type(unified_elem))), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        unified_elem = changes.new_contravariant_vertex(genv, [self, :Elem]) # TODO
        elems = @types.map do |type|
          nvtx = type.contravariant_vertex(genv, changes, subst)
          changes.add_edge(genv, nvtx, unified_elem)
          nvtx
        end
        changes.add_edge(genv, Source.new(Type::Array.new(genv, elems, genv.gen_ary_type(unified_elem))), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_edge(genv, vtx, changes.target)
        found_any = false
        vtx.each_type do |ty|
          next if ty.is_a?(Type::Bot)
          found_any = true
          case ty
          when Type::Array
            next if ty.elems.size != @types.size
            @types.zip(ty.elems) do |f_ty, a_ty|
              return false unless f_ty.typecheck(genv, changes, a_ty, subst)
            end
            return true
          when Type::Instance
            @types.each do |f_ty|
              return false unless f_ty.typecheck(genv, changes, vtx, subst)
            end
            return true
          end
        end
        !found_any
      end

      def show
        "[#{ @types.map {|ty| ty.show }.join(", ") }]"
      end
    end

    class SigTyRecordNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @keys = raw_decl.fields.keys
        @vals = raw_decl.fields.values.map { |val| AST.create_rbs_type(val, lenv) }
      end

      attr_reader :keys, :vals
      def subnodes = { vals: }
      def attrs = { keys: }

      def covariant_vertex0(genv, changes, vtx, subst)
        field_vertices = {}
        @keys.zip(@vals) do |key, val_node|
          field_vertices[key] = val_node.covariant_vertex(genv, changes, subst)
        end

        # Create base Hash type for Record
        key_vtx = Source.new(genv.symbol_type)
        # Create union of all field values for the Hash value type
        val_vtx = changes.new_covariant_vertex(genv, [self, :union])
        field_vertices.each_value do |field_vtx|
          changes.add_edge(genv, field_vtx, val_vtx)
        end
        base_hash_type = genv.gen_hash_type(key_vtx, val_vtx)

        changes.add_edge(genv, Source.new(Type::Record.new(genv, field_vertices, base_hash_type)), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        field_vertices = {}
        @keys.zip(@vals) do |key, val_node|
          field_vertices[key] = val_node.contravariant_vertex(genv, changes, subst)
        end

        # Create base Hash type for Record
        key_vtx = Source.new(genv.symbol_type)
        # Create union of all field values for the Hash value type
        val_vtx = changes.new_contravariant_vertex(genv, [self, :union])
        field_vertices.each_value do |field_vtx|
          changes.add_edge(genv, field_vtx, val_vtx)
        end
        base_hash_type = genv.gen_hash_type(key_vtx, val_vtx)

        changes.add_edge(genv, Source.new(Type::Record.new(genv, field_vertices, base_hash_type)), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_edge(genv, vtx, changes.target)
        found_any = false
        vtx.each_type do |ty|
          next if ty.is_a?(Type::Bot)
          found_any = true
          case ty
          when Type::Hash
            @keys.zip(@vals) do |key, val_node|
              val_vtx = ty.get_value(key)
              return false unless val_node.typecheck(genv, changes, val_vtx, subst)
            end
            return true
          end
        end
        !found_any
      end

      def show
        field_strs = @keys.zip(@vals).map do |key, val_node|
          "#{ key }: #{ val_node.show }"
        end
        "{ #{ field_strs.join(", ") } }"
      end
    end

    class SigTyVarNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @var = raw_decl.name
      end

      attr_reader :var

      def attrs = { var: }

      def covariant_vertex0(genv, changes, vtx, subst)
        raise "unknown type variable: #{ @var }" unless subst[@var]
        changes.add_edge(genv, subst[@var], vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        raise "unknown type variable: #{ @var }" unless subst[@var]
        changes.add_edge(genv, Source.new(Type::Var.new(genv, @var, subst[@var])), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_edge(genv, vtx.new_vertex(genv, self), subst[@var]) unless vtx == subst[@var]
        true
      end

      def show
        "#{ @var }"
      end
    end

    class SigTyOptionalNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @type = AST.create_rbs_type(raw_decl.type, lenv)
      end

      attr_reader :type
      def subnodes = { type: }

      def covariant_vertex0(genv, changes, vtx, subst)
        @type.covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.nil_type), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        @type.contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(genv.nil_type), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        # For optional type T?, check if all non-nil types match T.
        # nil is always acceptable.
        changes.add_edge(genv, vtx, changes.target)
        has_non_nil = false
        vtx.each_type do |ty|
          next if ty.is_a?(Type::Bot)
          next if ty == genv.nil_type
          has_non_nil = true
        end
        return true unless has_non_nil
        @type.typecheck(genv, changes, vtx, subst)
      end

      def show
        s = @type.show
        if @type.is_a?(SigTyIntersectionNode) || @type.is_a?(SigTyUnionNode)
          s = "(#{ s })"
        end
        s + "?"
      end
    end

    class SigTyLiteralNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        @lit = raw_decl.literal
      end

      attr_reader :lit
      def attrs = { lit: }

      def get_type(genv)
        case @lit
        when ::Symbol
          Type::Symbol.new(genv, @lit)
        when ::Integer then genv.int_type
        when ::String then genv.str_type
        when ::TrueClass then genv.true_type
        when ::FalseClass then genv.false_type
        else
          raise "unknown RBS literal: #{ @lit.inspect }"
        end
      end

      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(get_type(genv)), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_edge(genv, Source.new(get_type(genv)), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        if @lit.is_a?(::Symbol)
          changes.add_edge(genv, vtx, changes.target)
          found_any = false
          vtx.each_type do |ty|
            next if ty.is_a?(Type::Bot)
            found_any = true
            case ty
            when Type::Symbol
              return true if ty.sym == @lit
            end
          end
          return !found_any
        end
        f_mod = get_type(genv).mod
        AST.typecheck_for_module(genv, changes, f_mod, [], vtx, subst)
      end

      def show
        @lit.inspect
      end
    end

    class SigTyProcNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        # raw_decl.type is an RBS::Types::Function, we need to wrap it in a MethodType
        if raw_decl.type
          method_type = RBS::MethodType.new(
            type: raw_decl.type,
            type_params: [],
            block: raw_decl.block,
            location: raw_decl.location
          )
          @type = AST.create_rbs_func_type(method_type, nil, raw_decl.block, lenv)
        else
          @type = nil
        end
      end

      attr_reader :type
      def subnodes = { type: }

      def covariant_vertex0(genv, changes, vtx, subst)
        # For now, just return the base Proc type without the function signature details
        # TODO: Create a proper Type::Proc with the function signature
        changes.add_edge(genv, Source.new(genv.proc_type), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        # For now, just return the base Proc type without the function signature details
        # TODO: Create a proper Type::Proc with the function signature
        changes.add_edge(genv, Source.new(genv.proc_type), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        # TODO: proper check
        AST.typecheck_for_module(genv, changes, genv.proc_type.mod, [], vtx, subst)
      end

      def show
        "^(...)"
      end
    end

    class SigTyInterfaceNode < SigTyNode
      def initialize(raw_decl, lenv)
        super(raw_decl, lenv)
        name = raw_decl.name
        @cpath = name.namespace.path + [name.name]

        @toplevel = name.namespace.absolute? # "::Foo" or "Foo"
        @args = raw_decl.args.map {|arg| AST.create_rbs_type(arg, lenv) }
      end

      attr_reader :cpath, :toplevel, :args
      def subnodes = { args: }
      def attrs = { cpath:, toplevel: }

      def define0(genv)
        @args.each {|arg| arg.define(genv) }
        const_reads = []
        const_read = BaseConstRead.new(genv, @cpath.first, @toplevel ? CRef::Toplevel : @lenv.cref, false)
        const_reads << const_read
        unless @cpath.empty?
          @cpath[1..].each do |cname|
            const_read = ScopedConstRead.new(cname, const_read, false)
            const_reads << const_read
          end
        end
        const_reads
      end

      def undefine0(genv)
        @static_ret.each do |const_read|
          const_read.destroy(genv)
        end
        @args.each {|arg| arg.undefine(genv) }
      end

      def covariant_vertex0(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        mod = genv.resolve_cpath(cpath)
        args = @args.map {|arg| arg.covariant_vertex(genv, changes, subst) }
        changes.add_edge(genv, Source.new(Type::Instance.new(genv, mod, args)), vtx)
      end

      def contravariant_vertex0(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        mod = genv.resolve_cpath(cpath)
        args = @args.map {|arg| arg.contravariant_vertex(genv, changes, subst) }
        changes.add_edge(genv, Source.new(Type::Instance.new(genv, mod, args)), vtx)
      end

      def typecheck(genv, changes, vtx, subst)
        changes.add_depended_static_read(@static_ret.last)
        cpath = @static_ret.last.cpath
        return unless cpath
        f_mod = genv.resolve_cpath(cpath)
        # self/f_mod: formal, vtx: actual
        AST.typecheck_for_module(genv, changes, f_mod, @args, vtx, subst)
      end

      def show
        s = "::#{ @cpath.join("::") }"
        if !@args.empty?
          s << "[...]"
        end
        s
      end
    end
  end
end
