diff --git a/lib/steep.rb b/lib/steep.rb
index 12eae1ea7..b5c321c8b 100644
--- a/lib/steep.rb
+++ b/lib/steep.rb
@@ -140,7 +140,7 @@ def self.logger
   def self.new_logger(output, prev_level)
     ActiveSupport::TaggedLogging.new(Logger.new(output)).tap do |logger|
       logger.push_tags "Steep #{VERSION}"
-      logger.level = prev_level || Logger::WARN
+      logger.level = prev_level || Logger::ERROR
     end
   end
 
@@ -157,7 +157,7 @@ def self.log_output=(output)
   @logger = nil
   self.log_output = STDERR
 
-  def self.measure(message, level: :info)
+  def self.measure(message, level: :warn)
     start = Time.now
     yield.tap do
       time = Time.now - start
@@ -174,4 +174,63 @@ def self.log_error(exn, message: "Unexpected error: #{exn.inspect}")
       Steep.logger.warn "  #{loc}"
     end
   end
+
+  class Sampler
+    def initialize()
+      @samples = []
+    end
+
+    def sample(message)
+      start = Time.now
+      yield.tap do
+        time = Time.now - start
+        @samples << [message, time]
+      end
+    end
+
+    def count
+      @samples.count
+    end
+
+    def total
+      @samples.sum(&:last)
+    end
+
+    def slowests(num)
+      @samples.sort_by(&:last).reverse.take(num)
+    end
+
+    def average
+      if count > 0
+        total/count
+      else
+        0
+      end
+    end
+
+    def percentile(p)
+      slowests(count - count * p / 100r).last&.last || 0
+    end
+  end
+
+  def self.measure2(message, level: :warn)
+    sampler = Sampler.new
+    result = yield(sampler)
+
+    if level.is_a?(Symbol)
+      level = Logger.const_get(level.to_s.upcase)
+    end
+    logger.log(level) { "#{sampler.total}secs for \"#{message}\"" }
+    logger.log(level) { "  Average: #{sampler.average}secs"}
+    logger.log(level) { "  Median: #{sampler.percentile(50)}secs"}
+    logger.log(level) { "  Samples: #{sampler.count}"}
+    logger.log(level) { "  99 percentile: #{sampler.percentile(99)}secs"}
+    logger.log(level) { "  90 percentile: #{sampler.percentile(90)}secs"}
+    logger.log(level) { "  10 Slowests:"}
+    sampler.slowests(10).each do |message, time|
+      logger.log(level) { "    #{message} (#{time}secs)"}
+    end
+
+    result
+  end
 end
diff --git a/lib/steep/ast/types/class.rb b/lib/steep/ast/types/class.rb
index 7cba9ff1d..6014baf52 100644
--- a/lib/steep/ast/types/class.rb
+++ b/lib/steep/ast/types/class.rb
@@ -8,6 +8,10 @@ def initialize(location: nil)
           @location = location
         end
 
+        def to_s
+          "class"
+        end
+
         def ==(other)
           other.is_a?(Class)
         end
diff --git a/lib/steep/drivers/validate.rb b/lib/steep/drivers/validate.rb
index 2029d63de..a8f052113 100644
--- a/lib/steep/drivers/validate.rb
+++ b/lib/steep/drivers/validate.rb
@@ -23,13 +23,16 @@ def run
           changes = file_loader.load_changes(target.signature_pattern, changes: {})
           controller.update(changes)
 
-          errors = case controller.status
-                   when Services::SignatureService::SyntaxErrorStatus, Services::SignatureService::AncestorErrorStatus
-                     controller.status.diagnostics
-                   when Services::SignatureService::LoadedStatus
-                     check = Subtyping::Check.new(factory: AST::Types::Factory.new(builder: controller.latest_builder))
-                     Signature::Validator.new(checker: check).tap {|v| v.validate() }.each_error.to_a
-                   end
+          errors =
+            Steep.measure "Validation" do
+              case controller.status
+              when Services::SignatureService::SyntaxErrorStatus, Services::SignatureService::AncestorErrorStatus
+                controller.status.diagnostics
+              when Services::SignatureService::LoadedStatus
+                check = Subtyping::Check.new(factory: AST::Types::Factory.new(builder: controller.latest_builder))
+                Signature::Validator.new(checker: check).tap {|v| v.validate() }.each_error.to_a
+              end
+            end
 
           any_error ||= !errors.empty?
 
diff --git a/lib/steep/server/change_buffer.rb b/lib/steep/server/change_buffer.rb
index bbdebbd38..4146b556b 100644
--- a/lib/steep/server/change_buffer.rb
+++ b/lib/steep/server/change_buffer.rb
@@ -24,12 +24,16 @@ def pop_buffer
       end
 
       def load_files(project:, commandline_args:)
-        push_buffer do |changes|
-          loader = Services::FileLoader.new(base_dir: project.base_dir)
+        Steep.logger.tagged "#load_files" do
+          push_buffer do |changes|
+            loader = Services::FileLoader.new(base_dir: project.base_dir)
 
-          project.targets.each do |target|
-            loader.load_changes(target.source_pattern, commandline_args, changes: changes)
-            loader.load_changes(target.signature_pattern, changes: changes)
+            Steep.measure "load changes from disk" do
+              project.targets.each do |target|
+                loader.load_changes(target.source_pattern, commandline_args, changes: changes)
+                loader.load_changes(target.signature_pattern, changes: changes)
+              end
+            end
           end
         end
       end
diff --git a/lib/steep/server/master.rb b/lib/steep/server/master.rb
index 089d5857b..cda064984 100644
--- a/lib/steep/server/master.rb
+++ b/lib/steep/server/master.rb
@@ -305,11 +305,11 @@ def process_message_from_worker(message, worker:)
         case
         when message.key?(:id) && !message.key?(:method)
           # Response from worker
-          Steep.logger.info "Received response #{message[:id]} from worker"
+          Steep.logger.debug { "Received response #{message[:id]} from worker" }
           recon_queue << [message, worker]
         when message.key?(:method) && !message.key?(:id)
           # Notification from worker
-          Steep.logger.info "Received notification #{message[:method]} from worker"
+          Steep.logger.debug { "Received notification #{message[:method]} from worker" }
           write_queue << message
         end
       end
diff --git a/lib/steep/services/signature_service.rb b/lib/steep/services/signature_service.rb
index b371f3ebf..ec1b48ab4 100644
--- a/lib/steep/services/signature_service.rb
+++ b/lib/steep/services/signature_service.rb
@@ -122,114 +122,144 @@ def current_subtyping
       end
 
       def apply_changes(files, changes)
-        changes.each.with_object({}) do |(path, cs), update|
-          old_text = files[path]&.content
-          content = cs.inject(old_text || "") {|text, change| change.apply_to(text) }
-
-          buffer = RBS::Buffer.new(name: path, content: content)
-
-          update[path] = begin
-                           FileStatus.new(path: path, content: content, decls: RBS::Parser.parse_signature(buffer))
-                         rescue RBS::ParsingError => exn
-                           FileStatus.new(path: path, content: content, decls: exn)
-                         end
+        Steep.logger.tagged "#apply_changes" do
+          Steep.measure2 "Applying change" do |sampler|
+            changes.each.with_object({}) do |(path, cs), update|
+              sampler.sample "#{path}" do
+                old_text = files[path]&.content
+                content = cs.inject(old_text || "") {|text, change| change.apply_to(text) }
+
+                buffer = RBS::Buffer.new(name: path, content: content)
+
+                update[path] = begin
+                                 FileStatus.new(path: path, content: content, decls: RBS::Parser.parse_signature(buffer))
+                               rescue RBS::ParsingError => exn
+                                 FileStatus.new(path: path, content: content, decls: exn)
+                               end
+              end
+            end
+          end
         end
       end
 
       def update(changes)
-        updates = apply_changes(files, changes)
-        paths = Set.new(updates.each_key)
-        paths.merge(pending_changed_paths)
-
-        if updates.each_value.any? {|file| file.decls.is_a?(RBS::ParsingError) }
-          diagnostics = []
+        Steep.logger.tagged "#update" do
+          updates = apply_changes(files, changes)
+          paths = Set.new(updates.each_key)
+          paths.merge(pending_changed_paths)
+
+          if updates.each_value.any? {|file| file.decls.is_a?(RBS::ParsingError) }
+            diagnostics = []
+
+            updates.each_value do |file|
+              if file.decls.is_a?(RBS::ParsingError)
+                # factory is not used here because the error is a syntax error.
+                diagnostics << Diagnostic::Signature.from_rbs_error(file.decls, factory: nil)
+              end
+            end
 
-          updates.each do |path, file|
-            if file.decls.is_a?(RBS::ParsingError)
-              # facotry is not used here because the error is a syntax error.
-              diagnostics << Diagnostic::Signature.from_rbs_error(file.decls, factory: nil)
+            @status = SyntaxErrorStatus.new(
+              files: self.files.merge(updates),
+              diagnostics: diagnostics,
+              last_builder: latest_builder,
+              changed_paths: paths
+            )
+          else
+            files = self.files.merge(updates)
+            updated_files = paths.each.with_object({}) do |path, hash|
+              hash[path] = files[path]
             end
-          end
+            result =
+              Steep.measure "#update_env with updated #{paths.size} files" do
+                update_env(updated_files, paths: paths)
+              end
 
-          @status = SyntaxErrorStatus.new(
-            files: self.files.merge(updates),
-            diagnostics: diagnostics,
-            last_builder: latest_builder,
-            changed_paths: paths
-          )
-        else
-          files = self.files.merge(updates)
-          updated_files = paths.each.with_object({}) do |path, hash|
-            hash[path] = files[path]
+            @status = case result
+                      when Array
+                        AncestorErrorStatus.new(
+                          changed_paths: paths,
+                          last_builder: latest_builder,
+                          diagnostics: result,
+                          files: files
+                        )
+                      when RBS::DefinitionBuilder::AncestorBuilder
+                        builder2 = update_builder(ancestor_builder: result, paths: paths)
+                        LoadedStatus.new(builder: builder2, files: files)
+                      end
           end
-          result = update_env(updated_files, paths: paths)
-
-          @status = case result
-                    when Array
-                      AncestorErrorStatus.new(
-                        changed_paths: paths,
-                        last_builder: latest_builder,
-                        diagnostics: result,
-                        files: files
-                      )
-                    when RBS::DefinitionBuilder::AncestorBuilder
-                      LoadedStatus.new(builder: update_builder(ancestor_builder: result, paths: paths), files: files)
-                    end
         end
       end
 
       def update_env(updated_files, paths:)
-        errors = []
+        Steep.logger.tagged "#update_env" do
+          errors = []
+          new_decls = Set[].compare_by_identity
+
+          env =
+            Steep.measure "Deleting out of date decls" do
+              latest_env.reject do |decl|
+                if decl.location
+                  paths.include?(decl.location.buffer.name)
+                end
+              end
+            end
 
-        env = latest_env.reject do |decl|
-          if decl.location
-            paths.include?(decl.location.buffer.name)
+          Steep.measure "Loading new decls" do
+            updated_files.each_value do |content|
+              if content.decls.is_a?(RBS::ErrorBase)
+                errors << content.decls
+              else
+                begin
+                  content.decls.each do |decl|
+                    env << decl
+                    new_decls << decl
+                  end
+                rescue RBS::LoadingError => exn
+                  errors << exn
+                end
+              end
+            end
           end
-        end
 
-        updated_files.each_value do |content|
-          if content.decls.is_a?(RBS::ErrorBase)
-            errors << content.decls
-          else
+          Steep.measure "validate type params" do
             begin
-              content.decls.each do |decl|
-                env << decl
-              end
+              env.validate_type_params
             rescue RBS::LoadingError => exn
               errors << exn
             end
           end
-        end
 
-        begin
-          env.validate_type_params
-        rescue RBS::LoadingError => exn
-          errors << exn
-        end
+          unless errors.empty?
+            return errors.map {|error|
+              # Factory will not be used because of the possible error types.
+              Diagnostic::Signature.from_rbs_error(error, factory: nil)
+            }
+          end
 
-        unless errors.empty?
-          return errors.map {|error|
-            # Factory will not be used because of the possible error types.
-            Diagnostic::Signature.from_rbs_error(error, factory: nil)
-          }
-        end
+          Steep.measure "resolve type names with #{new_decls.size} top-level decls" do
+            env = env.resolve_type_names(only: new_decls)
+          end
 
-        builder = RBS::DefinitionBuilder::AncestorBuilder.new(env: env.resolve_type_names)
-        builder.env.class_decls.each_key do |type_name|
-          rescue_rbs_error(errors) { builder.one_instance_ancestors(type_name) }
-          rescue_rbs_error(errors) { builder.one_singleton_ancestors(type_name) }
-        end
-        builder.env.interface_decls.each_key do |type_name|
-          rescue_rbs_error(errors) { builder.one_interface_ancestors(type_name) }
-        end
+          builder = RBS::DefinitionBuilder::AncestorBuilder.new(env: env)
 
-        unless errors.empty?
-          # Builder won't be used.
-          factory = AST::Types::Factory.new(builder: nil)
-          return errors.map {|error| Diagnostic::Signature.from_rbs_error(error, factory: factory) }
-        end
+          Steep.measure("Pre-loading one ancestors") do
+            builder.env.class_decls.each_key do |type_name|
+              rescue_rbs_error(errors) { builder.one_instance_ancestors(type_name) }
+              rescue_rbs_error(errors) { builder.one_singleton_ancestors(type_name) }
+            end
+            builder.env.interface_decls.each_key do |type_name|
+              rescue_rbs_error(errors) { builder.one_interface_ancestors(type_name) }
+            end
+          end
 
-        builder
+          unless errors.empty?
+            # Builder won't be used.
+            factory = AST::Types::Factory.new(builder: nil)
+            return errors.map {|error| Diagnostic::Signature.from_rbs_error(error, factory: factory) }
+          end
+
+          builder
+        end
       end
 
       def rescue_rbs_error(errors)
@@ -241,29 +271,30 @@ def rescue_rbs_error(errors)
       end
 
       def update_builder(ancestor_builder:, paths:)
-        changed_names = Set[]
-
-        old_definition_builder = latest_builder
-        old_env = old_definition_builder.env
-        old_names = type_names(paths: paths, env: old_env)
-        old_ancestor_builder = old_definition_builder.ancestor_builder
-        old_method_builder = old_definition_builder.method_builder
-        old_graph = RBS::AncestorGraph.new(env: old_env, ancestor_builder: old_ancestor_builder)
-        add_descendants(graph: old_graph, names: old_names, set: changed_names)
-        add_nested_decls(env: old_env, names: old_names, set: changed_names)
-
-        new_env = ancestor_builder.env
-        new_ancestor_builder = ancestor_builder
-        new_names = type_names(paths: paths, env: new_env)
-        new_graph = RBS::AncestorGraph.new(env: new_env, ancestor_builder: new_ancestor_builder)
-        add_descendants(graph: new_graph, names: new_names, set: changed_names)
-        add_nested_decls(env: new_env, names: new_names, set: changed_names)
-
-        old_definition_builder.update(
-          env: new_env,
-          ancestor_builder: new_ancestor_builder,
-          except: changed_names
-        )
+        Steep.measure "#update_builder with #{paths.size} files" do
+          changed_names = Set[]
+
+          old_definition_builder = latest_builder
+          old_env = old_definition_builder.env
+          old_names = type_names(paths: paths, env: old_env)
+          old_ancestor_builder = old_definition_builder.ancestor_builder
+          old_graph = RBS::AncestorGraph.new(env: old_env, ancestor_builder: old_ancestor_builder)
+          add_descendants(graph: old_graph, names: old_names, set: changed_names)
+          add_nested_decls(env: old_env, names: old_names, set: changed_names)
+
+          new_env = ancestor_builder.env
+          new_ancestor_builder = ancestor_builder
+          new_names = type_names(paths: paths, env: new_env)
+          new_graph = RBS::AncestorGraph.new(env: new_env, ancestor_builder: new_ancestor_builder)
+          add_descendants(graph: new_graph, names: new_names, set: changed_names)
+          add_nested_decls(env: new_env, names: new_names, set: changed_names)
+
+          old_definition_builder.update(
+            env: new_env,
+            ancestor_builder: new_ancestor_builder,
+            except: changed_names
+          )
+        end
       end
 
       def type_names(paths:, env:)
diff --git a/lib/steep/services/type_check_service.rb b/lib/steep/services/type_check_service.rb
index 632aa8809..e74d00168 100644
--- a/lib/steep/services/type_check_service.rb
+++ b/lib/steep/services/type_check_service.rb
@@ -128,138 +128,155 @@ def each_diagnostics(&block)
       end
 
       def update(changes:, &block)
-        updated_targets = Steep.measure "Updating signatures..." do
+        updated_targets = Steep.measure "#update_signature" do
           update_signature(changes: changes, &block)
         end
-        project.targets.each do |target|
-          Steep.measure "Typechecking target `#{target.name}`..." do
-            update_target(target: target, changes: changes, updated: updated_targets.include?(target), &block)
+        Steep.measure2 "Type check target" do |sampler|
+          project.targets.each do |target|
+            sampler.sample target.name.to_s do
+              update_target(target: target, changes: changes, updated: updated_targets.include?(target), &block)
+            end
           end
         end
       end
 
       def update_signature(changes:, &block)
-        updated_targets = []
-
-        project.targets.each do |target|
-          signature_service = signature_services[target.name]
-          signature_changes = changes.filter {|path, _| target.possible_signature_file?(path) }
-
-          unless signature_changes.empty?
-            updated_targets << target
-            signature_service.update(signature_changes)
+        Steep.logger.tagged "#update_signature" do
+          updated_targets = []
+
+          Steep.measure2 "Update signatures" do |sampler|
+            project.targets.each do |target|
+              sampler.sample target.name.to_s do
+                signature_service = signature_services[target.name]
+                signature_changes = changes.filter {|path, _| target.possible_signature_file?(path) }
+
+                unless signature_changes.empty?
+                  updated_targets << target
+                  signature_service.update(signature_changes)
+                end
+              end
+            end
           end
-        end
 
-        accumulated_diagnostics = {}
+          Steep.measure "signature validations" do
+            accumulated_diagnostics = {}
 
-        updated_targets.each do |target|
-          service = signature_services[target.name]
+            updated_targets.each do |target|
+              service = signature_services[target.name]
 
-          next if no_type_checking?
+              next if no_type_checking?
 
-          case service.status
-          when SignatureService::SyntaxErrorStatus, SignatureService::AncestorErrorStatus
-            service.status.diagnostics.group_by {|diag| Pathname(diag.location.buffer.name) }.each do |path, diagnostics|
-              if assignment =~ path
-                array = accumulated_diagnostics[path] ||= []
-                array.push(*diagnostics)
-                yield [path, array]
-              end
-            end
-          when SignatureService::LoadedStatus
-            validator = Signature::Validator.new(checker: service.current_subtyping)
-            paths = service.each_rbs_path.select {|path| assignment =~ path }.to_set
-            type_names = service.type_names(paths: paths, env: service.latest_env)
-
-            validated_names = Set[]
-            type_names.each do |type_name|
-              unless validated_names.include?(type_name)
-                case
-                when type_name.class?
-                  validator.validate_one_class(type_name)
-                when type_name.interface?
-                  validator.validate_one_interface(type_name)
-                when type_name.alias?
-                  validator.validate_one_alias(type_name)
+              case service.status
+              when SignatureService::SyntaxErrorStatus, SignatureService::AncestorErrorStatus
+                service.status.diagnostics.group_by {|diag| Pathname(diag.location.buffer.name) }.each do |path, diagnostics|
+                  if assignment =~ path
+                    array = accumulated_diagnostics[path] ||= []
+                    array.push(*diagnostics)
+                    yield [path, array]
+                  end
+                end
+              when SignatureService::LoadedStatus
+                validator = Signature::Validator.new(checker: service.current_subtyping)
+                paths = service.each_rbs_path.select {|path| assignment =~ path }.to_set
+                type_names = service.type_names(paths: paths, env: service.latest_env).to_set
+
+                Steep.measure2 "Validating #{type_names.size} types from #{paths.size} files" do |sampler|
+                  type_names.each do |type_name|
+                    sampler.sample type_name.to_s do
+                      case
+                      when type_name.class?
+                        validator.validate_one_class(type_name)
+                      when type_name.interface?
+                        validator.validate_one_interface(type_name)
+                      when type_name.alias?
+                        validator.validate_one_alias(type_name)
+                      end
+                    end
+                  end
                 end
 
-                validated_names << type_name
-              end
-            end
-
-            validator.validate_const()
-            validator.validate_global()
+                Steep.measure "Validating const and globals" do
+                  validator.validate_const()
+                  validator.validate_global()
+                end
 
-            target_diagnostics = validator.each_error.group_by {|error| Pathname(error.location.buffer.name) }
-            signature_validation_diagnostics[target.name] = target_diagnostics
+                target_diagnostics = validator.each_error.group_by {|error| Pathname(error.location.buffer.name) }
+                signature_validation_diagnostics[target.name] = target_diagnostics
 
-            paths.each do |path|
-              array = (accumulated_diagnostics[path] ||= [])
-              if ds = target_diagnostics[path]
-                array.push(*ds)
+                paths.each do |path|
+                  array = (accumulated_diagnostics[path] ||= [])
+                  if ds = target_diagnostics[path]
+                    array.push(*ds)
+                  end
+                  yield [path, array]
+                end
               end
-              yield [path, array]
             end
           end
-        end
 
-        updated_targets
+          updated_targets
+        end
       end
 
       def update_target(changes:, target:, updated:, &block)
-        contents = {}
+        Steep.logger.tagged "#update_target" do
+          contents = {}
 
-        if updated
-          source_files.each do |path, file|
-            if target.possible_source_file?(path)
-              contents[path] = file.content
+          if updated
+            source_files.each do |path, file|
+              if target.possible_source_file?(path)
+                contents[path] = file.content
+              end
             end
-          end
 
-          changes.each do |path, changes|
-            if target.possible_source_file?(path)
-              text = contents[path] || ""
-              contents[path] = changes.inject(text) {|text, change| change.apply_to(text) }
+            changes.each do |path, changes|
+              if target.possible_source_file?(path)
+                text = contents[path] || ""
+                contents[path] = changes.inject(text) {|text, change| change.apply_to(text) }
+              end
             end
-          end
-        else
-          changes.each do |path, changes|
-            if target.possible_source_file?(path)
-              text = source_files[path]&.content || ""
-              contents[path] = changes.inject(text) {|text, change| change.apply_to(text) }
+          else
+            changes.each do |path, changes|
+              if target.possible_source_file?(path)
+                text = source_files[path]&.content || ""
+                contents[path] = changes.inject(text) {|text, change| change.apply_to(text) }
+              end
             end
           end
-        end
 
-        signature_service = signature_services[target.name]
-        subtyping = signature_service.current_subtyping
-
-        contents.each do |path, text|
-          if assignment =~ path
-            if subtyping
-              file = type_check_file(target: target, subtyping: subtyping, path: path, text: text)
-              yield [file.path, file.diagnostics]
-            else
-              if source_files.key?(path)
-                file = source_files[path]&.update_content(text)
-              else
-                file = SourceFile.no_data(path: path, content: text)
-                yield [file.path, []]
+          signature_service = signature_services[target.name]
+          subtyping = signature_service.current_subtyping
+
+          Steep.measure2 "Type check sources" do |sampler|
+            contents.each do |path, text|
+              if assignment =~ path
+                if subtyping
+                  file = sampler.sample(path.to_s) do
+                    type_check_file(target: target, subtyping: subtyping, path: path, text: text)
+                  end
+                  yield [file.path, file.diagnostics]
+                else
+                  if source_files.key?(path)
+                    file = source_files[path]&.update_content(text)
+                  else
+                    file = SourceFile.no_data(path: path, content: text)
+                    yield [file.path, []]
+                  end
+                end
+
+                source_files[path] = file
               end
             end
-
-            source_files[path] = file
           end
         end
       end
 
       def type_check_file(target:, subtyping:, path:, text:)
         Steep.logger.tagged "#type_check_file(#{path}@#{target.name})" do
-          source = Source.parse(text, path: path, factory: subtyping.factory)
           if no_type_checking?
             SourceFile.no_data(path: path, content: text)
           else
+            source = Source.parse(text, path: path, factory: subtyping.factory)
             typing = TypeCheckService.type_check(source: source, subtyping: subtyping)
             SourceFile.with_typing(path: path, content: text, node: source.node, typing: typing)
           end
@@ -281,7 +298,9 @@ def self.type_check(source:, subtyping:)
                                                 signatures: subtyping.factory.env)
         lvar_env = TypeInference::LocalVariableTypeEnv.empty(
           subtyping: subtyping,
-          self_type: AST::Builtin::Object.instance_type
+          self_type: AST::Builtin::Object.instance_type,
+          instance_type: AST::Builtin::Object.instance_type,
+          class_type: AST::Builtin::Object.module_type
         ).annotate(annotations)
 
         context = TypeInference::Context.new(
diff --git a/lib/steep/signature/validator.rb b/lib/steep/signature/validator.rb
index 477640c8d..ea116f327 100644
--- a/lib/steep/signature/validator.rb
+++ b/lib/steep/signature/validator.rb
@@ -121,8 +121,20 @@ def validate_one_class(name)
                   parent_type = checker.factory.type(parent.type)
 
                   relation = Subtyping::Relation.new(sub_type: var_type, super_type: parent_type)
-                  result1 = checker.check(relation, self_type: nil, constraints: Subtyping::Constraints.empty)
-                  result2 = checker.check(relation.flip, self_type: nil, constraints: Subtyping::Constraints.empty)
+                  result1 = checker.check(
+                    relation,
+                    self_type: AST::Types::Self.new,
+                    instance_type: AST::Types::Instance.new,
+                    class_type: AST::Types::Class.new,
+                    constraints: Subtyping::Constraints.empty
+                  )
+                  result2 = checker.check(
+                    relation.flip,
+                    self_type: AST::Types::Self.new,
+                    instance_type: AST::Types::Instance.new,
+                    class_type: AST::Types::Class.new,
+                    constraints: Subtyping::Constraints.empty
+                  )
 
                   unless result1.success? and result2.success?
                     @errors << Diagnostic::Signature::InstanceVariableTypeError.new(
@@ -137,7 +149,13 @@ def validate_one_class(name)
 
               ancestors = builder.ancestor_builder.one_instance_ancestors(name)
               mixin_constraints(definition, ancestors.included_modules, immediate_self_types: ancestors.self_types).each do |relation, ancestor|
-                checker.check(relation, self_type: nil, constraints: Subtyping::Constraints.empty).else do
+                checker.check(
+                  relation,
+                  self_type: AST::Types::Self.new,
+                  instance_type: AST::Types::Instance.new,
+                  class_type: AST::Types::Class.new,
+                  constraints: Subtyping::Constraints.empty
+                ).else do
                   @errors << Diagnostic::Signature::ModuleSelfTypeError.new(
                     name: name,
                     location: ancestor.source&.location || raise,
@@ -159,8 +177,20 @@ def validate_one_class(name)
                   parent_type = checker.factory.type(parent.type)
 
                   relation = Subtyping::Relation.new(sub_type: var_type, super_type: parent_type)
-                  result1 = checker.check(relation, self_type: nil, constraints: Subtyping::Constraints.empty)
-                  result2 = checker.check(relation.flip, self_type: nil, constraints: Subtyping::Constraints.empty)
+                  result1 = checker.check(
+                    relation,
+                    self_type: AST::Types::Self.new,
+                    instance_type: AST::Types::Instance.new,
+                    class_type: AST::Types::Class.new,
+                    constraints: Subtyping::Constraints.empty
+                  )
+                  result2 = checker.check(
+                    relation.flip,
+                    self_type: AST::Types::Self.new,
+                    instance_type: AST::Types::Instance.new,
+                    class_type: AST::Types::Class.new,
+                    constraints: Subtyping::Constraints.empty
+                  )
 
                   unless result1.success? and result2.success?
                     @errors << Diagnostic::Signature::InstanceVariableTypeError.new(
@@ -175,7 +205,13 @@ def validate_one_class(name)
 
               ancestors = builder.ancestor_builder.one_singleton_ancestors(name)
               mixin_constraints(definition, ancestors.extended_modules, immediate_self_types: ancestors.self_types).each do |relation, ancestor|
-                checker.check(relation, self_type: nil, constraints: Subtyping::Constraints.empty).else do
+                checker.check(
+                  relation,
+                  self_type: AST::Types::Self.new,
+                  instance_type: AST::Types::Instance.new,
+                  class_type: AST::Types::Class.new,
+                  constraints: Subtyping::Constraints.empty
+                ).else do
                   @errors << Diagnostic::Signature::ModuleSelfTypeError.new(
                     name: name,
                     location: ancestor.source&.location || raise,
diff --git a/lib/steep/subtyping/check.rb b/lib/steep/subtyping/check.rb
index a21b5c016..54174db7d 100644
--- a/lib/steep/subtyping/check.rb
+++ b/lib/steep/subtyping/check.rb
@@ -98,10 +98,10 @@ def singleton_super_types(type_name)
         end
       end
 
-      def check(relation, constraints:, self_type:, assumption: Set.new, trace: Trace.new)
+      def check(relation, constraints:, self_type:, instance_type:, class_type:, assumption: Set.new, trace: Trace.new)
         Steep.logger.tagged "#{relation.sub_type} <: #{relation.super_type}" do
           prefix = trace.size
-          cached = cache[[relation, self_type]]
+          cached = cache[[relation, self_type, instance_type, class_type]]
           if cached && constraints.empty?
             if cached.success?
               cached
@@ -113,7 +113,15 @@ def check(relation, constraints:, self_type:, assumption: Set.new, trace: Trace.
               success(constraints: constraints)
             else
               assumption = assumption + Set[relation]
-              check0(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints).tap do |result|
+              check0(
+                relation,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                assumption: assumption,
+                trace: trace,
+                constraints: constraints
+              ).tap do |result|
                 result = result.else do |failure|
                   failure.drop(prefix)
                 end
@@ -160,7 +168,7 @@ def false_type?(type)
         end
       end
 
-      def check0(relation, self_type:, assumption:, trace:, constraints:)
+      def check0(relation, self_type:, class_type:, instance_type:, assumption:, trace:, constraints:)
         # puts relation
         trace.type(relation.sub_type, relation.super_type) do
           case
@@ -186,6 +194,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             check(
               Relation.new(sub_type: relation.sub_type, super_type: AST::Types::Union.build(types: [AST::Builtin.true_type, AST::Builtin.false_type])),
               self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
               assumption: assumption,
               trace: trace,
               constraints: constraints
@@ -196,6 +206,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
               Relation.new(sub_type: AST::Types::Union.build(types: [AST::Builtin.true_type, AST::Builtin.false_type]),
                            super_type: relation.super_type),
               self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
               assumption: assumption,
               trace: trace,
               constraints: constraints
@@ -205,15 +217,77 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             check(
               Relation.new(sub_type: self_type, super_type: relation.super_type),
               self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
               assumption: assumption,
               trace: trace,
               constraints: constraints
             )
 
+          when relation.sub_type.is_a?(AST::Types::Instance) && !instance_type.is_a?(AST::Types::Instance)
+            check(
+              Relation.new(sub_type: instance_type, super_type: relation.super_type),
+              self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
+              assumption: assumption,
+              trace: trace,
+              constraints: constraints
+            )
+
+          when relation.super_type.is_a?(AST::Types::Instance) && !instance_type.is_a?(AST::Types::Instance)
+            rel = Relation.new(sub_type: relation.sub_type, super_type: instance_type)
+
+            success_all?([rel, rel.flip]) do |r|
+              check(
+                r,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                assumption: assumption,
+                trace: trace,
+                constraints: constraints
+              )
+            end.then do |result|
+              Steep.logger.error { "`T <: instance` doesn't hold generally, but testing it with `#{relation} && #{relation.flip}` for compatibility"}
+              result
+            end
+
+          when relation.sub_type.is_a?(AST::Types::Class) && !instance_type.is_a?(AST::Types::Class)
+            check(
+              Relation.new(sub_type: class_type, super_type: relation.super_type),
+              self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
+              assumption: assumption,
+              trace: trace,
+              constraints: constraints
+            )
+
+          when relation.super_type.is_a?(AST::Types::Class) && !instance_type.is_a?(AST::Types::Class)
+            rel = Relation.new(sub_type: relation.sub_type, super_type: class_type)
+
+            success_all?([rel, rel.flip]) do |r|
+              check(
+                r,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                assumption: assumption,
+                trace: trace,
+                constraints: constraints
+              )
+            end.then do |result|
+              Steep.logger.error { "`T <: class` doesn't hold generally, but testing with `#{relation} && |- #{relation.flip}` for compatibility"}
+              result
+            end
+
           when alias?(relation.sub_type)
             check(
               Relation.new(sub_type: expand_alias(relation.sub_type), super_type: relation.super_type),
               self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
               assumption: assumption,
               trace: trace,
               constraints: constraints
@@ -223,6 +297,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             check(
               Relation.new(super_type: expand_alias(relation.super_type), sub_type: relation.sub_type),
               self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
               assumption: assumption,
               trace: trace,
               constraints: constraints
@@ -239,10 +315,12 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
           when relation.sub_type.is_a?(AST::Types::Union)
             results = relation.sub_type.types.map do |sub_type|
               check(Relation.new(sub_type: sub_type, super_type: relation.super_type),
-                     self_type: self_type,
-                     assumption: assumption,
-                     trace: trace,
-                     constraints: constraints)
+                    self_type: self_type,
+                    instance_type: instance_type,
+                    class_type: class_type,
+                    assumption: assumption,
+                    trace: trace,
+                    constraints: constraints)
             end
 
             if results.all?(&:success?)
@@ -254,10 +332,12 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
           when relation.super_type.is_a?(AST::Types::Union)
             results = relation.super_type.types.map do |super_type|
               check(Relation.new(sub_type: relation.sub_type, super_type: super_type),
-                     self_type: self_type,
-                     assumption: assumption,
-                     trace: trace,
-                     constraints: constraints)
+                    self_type: self_type,
+                    instance_type: instance_type,
+                    class_type: class_type,
+                    assumption: assumption,
+                    trace: trace,
+                    constraints: constraints)
             end
 
             results.find(&:success?) || results.first
@@ -265,10 +345,12 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
           when relation.sub_type.is_a?(AST::Types::Intersection)
             results = relation.sub_type.types.map do |sub_type|
               check(Relation.new(sub_type: sub_type, super_type: relation.super_type),
-                     self_type: self_type,
-                     assumption: assumption,
-                     trace: trace,
-                     constraints: constraints)
+                    self_type: self_type,
+                    instance_type: instance_type,
+                    class_type: class_type,
+                    assumption: assumption,
+                    trace: trace,
+                    constraints: constraints)
             end
 
             results.find(&:success?) || results.first
@@ -276,10 +358,12 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
           when relation.super_type.is_a?(AST::Types::Intersection)
             results = relation.super_type.types.map do |super_type|
               check(Relation.new(sub_type: relation.sub_type, super_type: super_type),
-                     self_type: self_type,
-                     assumption: assumption,
-                     trace: trace,
-                     constraints: constraints)
+                    self_type: self_type,
+                    instance_type: instance_type,
+                    class_type: class_type,
+                    assumption: assumption,
+                    trace: trace,
+                    constraints: constraints)
             end
 
             if results.all?(&:success?)
@@ -299,6 +383,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             check_interface(sub_interface,
                             super_interface,
                             self_type: self_type,
+                            instance_type: instance_type,
+                            class_type: class_type,
                             assumption: assumption,
                             trace: trace,
                             constraints: constraints)
@@ -306,7 +392,15 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
           when relation.sub_type.is_a?(AST::Types::Name::Base) && relation.super_type.is_a?(AST::Types::Name::Base)
             if relation.sub_type.name == relation.super_type.name && relation.sub_type.class == relation.super_type.class
               if arg_type?(relation.sub_type) && arg_type?(relation.super_type)
-                check_type_arg(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+                check_type_arg(
+                  relation,
+                  self_type: self_type,
+                  instance_type: instance_type,
+                  class_type: class_type,
+                  assumption: assumption,
+                  trace: trace,
+                  constraints: constraints
+                )
               else
                 success(constraints: constraints)
               end
@@ -324,6 +418,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
                 success_any?(possible_sub_types) do |sub_type|
                   check(Relation.new(sub_type: sub_type, super_type: relation.super_type),
                         self_type: self_type,
+                        instance_type: instance_type,
+                        class_type: class_type,
                         assumption: assumption,
                         trace: trace,
                         constraints: constraints)
@@ -339,12 +435,20 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             sub_type = relation.sub_type
             super_type = relation.super_type
 
-            check_method_params(name, sub_type.type.params, super_type.type.params, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints).then do
+            check_method_params(name, sub_type.type.params, super_type.type.params, self_type: self_type, instance_type: instance_type, class_type: class_type, assumption: assumption, trace: trace, constraints: constraints).then do
               check_block_given(name, sub_type.block, super_type.block, trace: trace, constraints: constraints).then do
-                check_block_params(name, sub_type.block, super_type.block, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints).then do
-                  check_block_return(sub_type.block, super_type.block, self_type: self_type, assumption: assumption, trace: trace, constraints:constraints).then do
+                check_block_params(name, sub_type.block, super_type.block, self_type: self_type, instance_type: instance_type, class_type: class_type, assumption: assumption, trace: trace, constraints: constraints).then do
+                  check_block_return(sub_type.block, super_type.block, self_type: self_type, instance_type: instance_type, class_type: class_type, assumption: assumption, trace: trace, constraints:constraints).then do
                     relation = Relation.new(super_type: super_type.type.return_type, sub_type: sub_type.type.return_type)
-                    check(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+                    check(
+                      relation,
+                      self_type: self_type,
+                      instance_type: instance_type,
+                      class_type: class_type,
+                      assumption: assumption,
+                      trace: trace,
+                      constraints: constraints
+                    )
                   end
                 end
               end
@@ -355,7 +459,15 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
               pairs = relation.sub_type.types.take(relation.super_type.types.size).zip(relation.super_type.types)
               results = pairs.map do |t1, t2|
                 relation = Relation.new(sub_type: t1, super_type: t2)
-                check(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+                check(
+                  relation,
+                  self_type: self_type,
+                  instance_type: instance_type,
+                  class_type: class_type,
+                  assumption: assumption,
+                  trace: trace,
+                  constraints: constraints
+                )
               end
 
               if results.all?(&:success?)
@@ -376,6 +488,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
 
             check(Relation.new(sub_type: tuple_element_type, super_type: relation.super_type.args[0]),
                   self_type: self_type,
+                  instance_type: instance_type,
+                  class_type: class_type,
                   assumption: assumption,
                   trace: trace,
                   constraints: constraints)
@@ -389,7 +503,15 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
               )
             }
             results = relations.map do |relation|
-              check(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+              check(
+                relation,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                assumption: assumption,
+                trace: trace,
+                constraints: constraints
+              )
             end
 
             if results.all?(&:success?)
@@ -405,6 +527,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             check_interface(record_interface,
                             type_interface,
                             self_type: self_type,
+                            instance_type: instance_type,
+                            class_type: class_type,
                             assumption: assumption,
                             trace: trace,
                             constraints: constraints)
@@ -430,6 +554,8 @@ def check0(relation, self_type:, assumption:, trace:, constraints:)
             check(
               Relation.new(sub_type: relation.sub_type.back_type, super_type: relation.super_type),
               self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
               assumption: assumption,
               trace: trace,
               constraints: constraints
@@ -466,7 +592,7 @@ def arg_type?(type)
         end
       end
 
-      def check_type_arg(relation, self_type:, assumption:, trace:, constraints:)
+      def check_type_arg(relation, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         sub_args = relation.sub_type.args
         sup_args = relation.super_type.args
 
@@ -476,13 +602,37 @@ def check_type_arg(relation, self_type:, assumption:, trace:, constraints:)
         success_all?(sub_args.zip(sup_args, sup_params.each)) do |sub_arg, sup_arg, sup_param|
           case sup_param.variance
           when :covariant
-            check(Relation.new(sub_type: sub_arg, super_type: sup_arg), self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+            check(
+              Relation.new(sub_type: sub_arg, super_type: sup_arg),
+              self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
+              assumption: assumption,
+              trace: trace,
+              constraints: constraints
+            )
           when :contravariant
-            check(Relation.new(sub_type: sup_arg, super_type: sub_arg), self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+            check(
+              Relation.new(sub_type: sup_arg, super_type: sub_arg),
+              self_type: self_type,
+              instance_type: instance_type,
+              class_type: class_type,
+              assumption: assumption,
+              trace: trace,
+              constraints: constraints
+            )
           when :invariant
             rel = Relation.new(sub_type: sub_arg, super_type: sup_arg)
             success_all?([rel, rel.flip]) do |r|
-              check(r, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+              check(
+                r,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                assumption: assumption,
+                trace: trace,
+                constraints: constraints
+              )
             end
           end
         end
@@ -548,7 +698,7 @@ def same_type?(relation, assumption:)
         relation.sub_type == relation.super_type
       end
 
-      def check_interface(sub_interface, super_interface, self_type:, assumption:, trace:, constraints:)
+      def check_interface(sub_interface, super_interface, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         trace.interface sub_interface, super_interface do
           method_triples = []
 
@@ -568,6 +718,8 @@ def check_interface(sub_interface, super_interface, self_type:, assumption:, tra
                                   sub_method,
                                   sup_method,
                                   self_type: self_type,
+                                  instance_type: instance_type,
+                                  class_type: class_type,
                                   assumption: assumption,
                                   trace: trace,
                                   constraints: constraints)
@@ -578,7 +730,7 @@ def check_interface(sub_interface, super_interface, self_type:, assumption:, tra
         end
       end
 
-      def check_method(name, sub_method, super_method, self_type:, assumption:, trace:, constraints:)
+      def check_method(name, sub_method, super_method, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         trace.method name, sub_method, super_method do
           super_method.method_types.map do |super_type|
             sub_method.method_types.map do |sub_type|
@@ -586,6 +738,8 @@ def check_method(name, sub_method, super_method, self_type:, assumption:, trace:
                                         sub_type,
                                         super_type,
                                         self_type: self_type,
+                                        instance_type: instance_type,
+                                        class_type: class_type,
                                         assumption: assumption,
                                         trace: trace,
                                         constraints: constraints
@@ -602,7 +756,7 @@ def check_method(name, sub_method, super_method, self_type:, assumption:, trace:
         end
       end
 
-      def check_generic_method_type(name, sub_type, super_type, self_type:, assumption:, trace:, constraints:)
+      def check_generic_method_type(name, sub_type, super_type, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         trace.method_type name, sub_type, super_type do
           case
           when sub_type.type_params.empty? && super_type.type_params.empty?
@@ -610,6 +764,8 @@ def check_generic_method_type(name, sub_type, super_type, self_type:, assumption
                               sub_type,
                               super_type,
                               self_type: self_type,
+                              instance_type: instance_type,
+                              class_type: class_type,
                               assumption: assumption,
                               trace: trace,
                               constraints: constraints
@@ -648,6 +804,8 @@ def check_generic_method_type(name, sub_type, super_type, self_type:, assumption
                                     sub_type.subst(subst),
                                     super_type,
                                     self_type: self_type,
+                                    instance_type: instance_type,
+                                    class_type: class_type,
                                     assumption: assumption,
                                     trace: trace,
                                     constraints: constraints)
@@ -672,6 +830,8 @@ def check_generic_method_type(name, sub_type, super_type, self_type:, assumption
                                              sub_type,
                                              super_type,
                                              self_type: self_type,
+                                             instance_type: instance_type,
+                                             class_type: class_type,
                                              assumption: assumption,
                                              trace: trace,
                                              constraints: constraints)
@@ -703,6 +863,8 @@ def check_generic_method_type(name, sub_type, super_type, self_type:, assumption
                                 sub_type_,
                                 super_type_,
                                 self_type: self_type,
+                                instance_type: instance_type,
+                                class_type: class_type,
                                 assumption: assumption,
                                 trace: trace,
                                 constraints: constraints)
@@ -716,15 +878,23 @@ def check_generic_method_type(name, sub_type, super_type, self_type:, assumption
         end
       end
 
-      def check_method_type(name, sub_type, super_type, self_type:, assumption:, trace:, constraints:)
+      def check_method_type(name, sub_type, super_type, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         Steep.logger.tagged("#{name}: #{sub_type} <: #{super_type}") do
-          check_method_params(name, sub_type.type.params, super_type.type.params, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints).then do
+          check_method_params(name, sub_type.type.params, super_type.type.params, self_type: self_type, instance_type: instance_type, class_type: class_type, assumption: assumption, trace: trace, constraints: constraints).then do
             check_block_given(name, sub_type.block, super_type.block, trace: trace, constraints: constraints).then do
-              check_block_params(name, sub_type.block, super_type.block, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints).then do
-                check_block_return(sub_type.block, super_type.block, self_type: self_type, assumption: assumption, trace: trace, constraints:constraints).then do
+              check_block_params(name, sub_type.block, super_type.block, self_type: self_type, instance_type: instance_type, class_type: class_type, assumption: assumption, trace: trace, constraints: constraints).then do
+                check_block_return(sub_type.block, super_type.block, self_type: self_type, instance_type: instance_type, class_type: class_type, assumption: assumption, trace: trace, constraints:constraints).then do
                   relation = Relation.new(super_type: super_type.type.return_type,
                                           sub_type: sub_type.type.return_type)
-                  check(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+                  check(
+                    relation,
+                    self_type: self_type,
+                    instance_type: instance_type,
+                    class_type: class_type,
+                    assumption: assumption,
+                    trace: trace,
+                    constraints: constraints
+                  )
                 end
               end
             end
@@ -748,14 +918,20 @@ def check_block_given(name, sub_block, super_block, trace:, constraints:)
         end
       end
 
-      def check_method_params(name, sub_params, super_params, self_type:, assumption:, trace:, constraints:)
+      def check_method_params(name, sub_params, super_params, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         match_params(name, sub_params, super_params, trace: trace).yield_self do |pairs|
           case pairs
           when Array
             pairs.each do |(sub_type, super_type)|
               relation = Relation.new(super_type: sub_type, sub_type: super_type)
 
-              result = check(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+              result = check(relation,
+                             self_type: self_type,
+                             instance_type: instance_type,
+                             class_type: class_type,
+                             assumption: assumption,
+                             trace: trace,
+                             constraints: constraints)
               return result if result.failure?
             end
 
@@ -884,12 +1060,14 @@ def match_params(name, sub_params, super_params, trace:)
         pairs
       end
 
-      def check_block_params(name, sub_block, super_block, self_type:, assumption:, trace:, constraints:)
+      def check_block_params(name, sub_block, super_block, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         if sub_block && super_block
           check_method_params(name,
                               super_block.type.params,
                               sub_block.type.params,
                               self_type: self_type,
+                              instance_type: instance_type,
+                              class_type: class_type,
                               assumption: assumption,
                               trace: trace,
                               constraints: constraints)
@@ -898,11 +1076,19 @@ def check_block_params(name, sub_block, super_block, self_type:, assumption:, tr
         end
       end
 
-      def check_block_return(sub_block, super_block, self_type:, assumption:, trace:, constraints:)
+      def check_block_return(sub_block, super_block, self_type:, instance_type:, class_type:, assumption:, trace:, constraints:)
         if sub_block && super_block
           relation = Relation.new(sub_type: super_block.type.return_type,
                                       super_type: sub_block.type.return_type)
-          check(relation, self_type: self_type, assumption: assumption, trace: trace, constraints: constraints)
+          check(
+            relation,
+            self_type: self_type,
+            instance_type: instance_type,
+            class_type: class_type,
+            assumption: assumption,
+            trace: trace,
+            constraints: constraints
+          )
         else
           success(constraints: constraints)
         end
diff --git a/lib/steep/subtyping/constraints.rb b/lib/steep/subtyping/constraints.rb
index e85e0e4fe..9f4cfe768 100644
--- a/lib/steep/subtyping/constraints.rb
+++ b/lib/steep/subtyping/constraints.rb
@@ -207,7 +207,7 @@ def lower_bound(var)
         end
       end
 
-      def solution(checker, variance:, variables:, self_type:)
+      def solution(checker, variance:, variables:, self_type:, instance_type:, class_type:)
         vars = []
         types = []
 
@@ -218,7 +218,7 @@ def solution(checker, variance:, variables:, self_type:)
               lower_bound = lower_bound(var)
               relation = Relation.new(sub_type: lower_bound, super_type: upper_bound)
 
-              checker.check(relation, self_type: self_type, constraints: self.class.empty).yield_self do |result|
+              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
 
diff --git a/lib/steep/type_construction.rb b/lib/steep/type_construction.rb
index db9ebc412..8def73dc1 100644
--- a/lib/steep/type_construction.rb
+++ b/lib/steep/type_construction.rb
@@ -115,8 +115,15 @@ def update_lvar_env
     end
 
     def check_relation(sub_type:, super_type:, constraints: Subtyping::Constraints.empty)
-      Steep.logger.debug { "check_relation: self:#{self_type} |- #{sub_type} <: #{super_type}" }
-      checker.check(Subtyping::Relation.new(sub_type: sub_type, super_type: super_type), self_type: self_type, constraints: constraints)
+      Steep.logger.debug { "check_relation: self:#{self_type}, instance:#{module_context.instance_type}, class:#{module_context.module_type} |- #{sub_type} <: #{super_type}" }
+      relation = Subtyping::Relation.new(sub_type: sub_type, super_type: super_type)
+      checker.check(
+        relation,
+        self_type: self_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type,
+        constraints: constraints
+      )
     end
 
     def for_new_method(method_name, node, args:, self_type:, definition:)
@@ -200,12 +207,16 @@ def for_new_method(method_name, node, args:, self_type:, definition:)
       type_env = type_env.with_annotations(
         ivar_types: annots.ivar_types,
         const_types: annots.const_types,
-        self_type: annots.self_type || self_type
+        self_type: annots.self_type || self_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
       )
 
       lvar_env = TypeInference::LocalVariableTypeEnv.empty(
         subtyping: checker,
-        self_type: annots.self_type || self_type
+        self_type: annots.self_type || self_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
       )
 
       if var_types
@@ -359,7 +370,9 @@ def for_module(node)
 
       lvar_env = TypeInference::LocalVariableTypeEnv.empty(
         subtyping: checker,
-        self_type: module_context_.module_type
+        self_type: module_context_.module_type,
+        instance_type: module_context_.instance_type,
+        class_type: module_context_.module_type
       ).annotate(annots)
 
       self.class.new(
@@ -437,7 +450,9 @@ def for_class(node)
 
       lvar_env = TypeInference::LocalVariableTypeEnv.empty(
         subtyping: checker,
-        self_type: module_context.module_type
+        self_type: module_context.module_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
       ).annotate(annots)
 
       class_body_context = TypeInference::Context.new(
@@ -523,7 +538,9 @@ def for_sclass(node, type)
 
       lvar_env = TypeInference::LocalVariableTypeEnv.empty(
         subtyping: checker,
-        self_type: module_context.module_type
+        self_type: module_context.module_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
       ).annotate(annots)
 
       body_context = TypeInference::Context.new(
@@ -604,14 +621,20 @@ def for_branch(node, truthy_vars: Set.new, type_case_override: nil, break_contex
       type_env = context.type_env
 
       if type_case_override
-        type_env = type_env.with_annotations(self_type: self_type)
+        type_env = type_env.with_annotations(
+          self_type: self_type,
+          instance_type: module_context.instance_type,
+          class_type: module_context.module_type
+        )
       end
 
       type_env = type_env.with_annotations(
         ivar_types: annots.ivar_types,
         const_types: annots.const_types,
         gvar_types: {},
-        self_type: self_type
+        self_type: self_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
       ) do |var, relation, result|
         typing.add_error(
           Diagnostic::Ruby::IncompatibleAnnotation.new(
@@ -1450,7 +1473,13 @@ def synthesize(node, hint: nil, condition: false)
 
               const_type = type_env.get(const: const_name) {}
               value_type, constr = constr.synthesize(node.children.last, hint: const_type)
-              type = type_env.assign(const: const_name, type: value_type, self_type: self_type) do |error|
+              type = type_env.assign(
+                const: const_name,
+                type: value_type,
+                self_type: self_type,
+                instance_type: module_context.instance_type,
+                class_type: module_context.module_type
+              ) do |error|
                 case error
                 when Subtyping::Result::Failure
                   const_type = type_env.get(const: const_name)
@@ -1942,7 +1971,7 @@ def synthesize(node, hint: nil, condition: false)
                        when AST::Types::Any
                          AST::Types::Any.new
                        else
-                         each = checker.factory.interface(collection_type, private: true).methods[:each]
+                         each = calculate_interface(collection_type, private: true).methods[:each]
                          method_type = (each&.method_types || []).find {|type| type.block && type.block.type.params.first_param }
                          method_type&.yield_self do |method_type|
                            method_type.block.type.params.first_param&.type
@@ -2148,7 +2177,7 @@ def synthesize(node, hint: nil, condition: false)
                 when AST::Types::Any
                   type = AST::Types::Any.new
                 else
-                  interface = checker.factory.interface(param_type, private: true)
+                  interface = calculate_interface(param_type, private: true)
                   method = interface.methods[value.children[0]]
                   if method
                     return_types = method.method_types.select {|method_type|
@@ -2267,6 +2296,7 @@ def synthesize(node, hint: nil, condition: false)
           end
         end
       rescue StandardError => exn
+        Steep.log_error exn
         typing.add_error(Diagnostic::Ruby::UnexpectedError.new(node: node, error: exn))
         type_any_rec(node)
       end
@@ -2286,7 +2316,13 @@ def check(node, type, constraints: Subtyping::Constraints.empty)
 
     def type_ivasgn(name, rhs, node)
       rhs_type = synthesize(rhs, hint: type_env.get(ivar: name) { fallback_to_any(node) }).type
-      ivar_type = type_env.assign(ivar: name, type: rhs_type, self_type: self_type) do |error|
+      ivar_type = type_env.assign(
+        ivar: name,
+        type: rhs_type,
+        self_type: self_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
+      ) do |error|
         case error
         when Subtyping::Result::Failure
           type = type_env.get(ivar: name)
@@ -2335,7 +2371,13 @@ def lvasgn(node, type)
     def ivasgn(node, type)
       ivar = node.children[0]
 
-      type_env.assign(ivar: ivar, type: type, self_type: self_type) do |error|
+      type_env.assign(
+        ivar: ivar,
+        type: type,
+        self_type: self_type,
+        instance_type: module_context.instance_type,
+        class_type: module_context.module_type
+      ) do |error|
         case error
         when Subtyping::Result::Failure
           var_type = type_env.get(ivar: ivar)
@@ -2722,9 +2764,9 @@ def type_send(node, send_node:, block_params:, block_body:, unwrap: false)
                            )
                          )
                        else
-                         interface = checker.factory.interface(expanded_self,
-                                                               private: !receiver,
-                                                               self_type: AST::Types::Self.new)
+                         interface = calculate_interface(expanded_self,
+                                                         private: !receiver,
+                                                         self_type: AST::Types::Self.new)
 
                          constr.type_send_interface(node,
                                                     interface: interface,
@@ -2736,9 +2778,7 @@ def type_send(node, send_node:, block_params:, block_body:, unwrap: false)
                                                     block_body: block_body)
                        end
                      else
-                       interface = checker.factory.interface(receiver_type,
-                                                             private: !receiver,
-                                                             self_type: receiver_type)
+                       interface = calculate_interface(receiver_type, private: !receiver, self_type: receiver_type)
 
                        constr.type_send_interface(node,
                                                   interface: interface,
@@ -2753,6 +2793,19 @@ def type_send(node, send_node:, block_params:, block_body:, unwrap: false)
       Pair.new(type: type, constr: constr)
     end
 
+    def calculate_interface(type, private:, self_type: type)
+      case type
+      when AST::Types::Self
+        type = self_type
+      when AST::Types::Instance
+        type = module_context.instance_type
+      when AST::Types::Class
+        type = module_context.module_type
+      end
+
+      checker.factory.interface(type, private: private, self_type: self_type)
+    end
+
     def expand_self(type)
       if type.is_a?(AST::Types::Self) && self_type
         self_type
@@ -3043,6 +3096,8 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, args:, arg
               s = constraints.solution(
                 checker,
                 self_type: self_type,
+                instance_type: module_context.instance_type,
+                class_type: module_context.module_type,
                 variance: variance,
                 variables: method_type.type.params.free_variables + method_type.block.type.params.free_variables
               )
@@ -3064,7 +3119,14 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, args:, arg
 
               case result
               when Subtyping::Result::Success
-                s = constraints.solution(checker, self_type: self_type, variance: variance, variables: fresh_vars)
+                s = constraints.solution(
+                  checker,
+                  self_type: self_type,
+                  instance_type: module_context.instance_type,
+                  class_type: module_context.module_type,
+                  variance: variance,
+                  variables: fresh_vars
+                )
                 method_type = method_type.subst(s)
 
                 return_type = method_type.type.return_type
@@ -3109,7 +3171,14 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, args:, arg
               message: "Unsupported block params pattern, probably masgn?"
             )
 
-            s = constraints.solution(checker, variance: variance, variables: fresh_vars, self_type: self_type)
+            s = constraints.solution(
+              checker,
+              variance: variance,
+              variables: fresh_vars,
+              self_type: self_type,
+              instance_type: module_context.instance_type,
+              class_type: module_context.module_type
+            )
             method_type = method_type.subst(s)
           end
         else
@@ -3130,11 +3199,25 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, args:, arg
           # Method call without block is allowed
           unless args.block_pass_arg
             # OK, without block
-            s = constraints.solution(checker, variance: variance, variables: fresh_vars, self_type: self_type)
+            s = constraints.solution(
+              checker,
+              variance: variance,
+              variables: fresh_vars,
+              self_type: self_type,
+              instance_type: module_context.instance_type,
+              class_type: module_context.module_type
+            )
             method_type = method_type.subst(s)
           else
             # &block arg is given
-            s = constraints.solution(checker, variance: variance, variables: fresh_vars, self_type: self_type)
+            s = constraints.solution(
+              checker,
+              variance: variance,
+              variables: fresh_vars,
+              self_type: self_type,
+              instance_type: module_context.instance_type,
+              class_type: module_context.module_type
+            )
             method_type = method_type.subst(s)
 
             errors << Diagnostic::Ruby::UnexpectedBlockGiven.new(
@@ -3150,11 +3233,27 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, args:, arg
               method_type: method_type
             )
 
-            s = constraints.solution(checker, variance: variance, variables: fresh_vars, self_type: self_type)
+            s = constraints.solution(
+              checker,
+              variance: variance,
+              variables: fresh_vars,
+              self_type: self_type,
+              instance_type: module_context.instance_type,
+              class_type: module_context.module_type
+            )
             method_type = method_type.subst(s)
           else
             begin
-              method_type = method_type.subst(constraints.solution(checker, self_type: self_type, variance: variance, variables: occurence.params))
+              method_type = method_type.subst(
+                constraints.solution(
+                  checker,
+                  self_type: self_type,
+                  instance_type: module_context.instance_type,
+                  class_type: module_context.module_type,
+                  variance: variance,
+                  variables: occurence.params
+                )
+              )
               hint_type = if topdown_hint
                             AST::Types::Proc.new(type: method_type.block.type, block: nil)
                           end
@@ -3178,7 +3277,16 @@ def try_method_type(node, receiver_type:, method_name:, method_type:, args:, arg
                 )
               end
 
-              method_type = method_type.subst(constraints.solution(checker, self_type: self_type, variance: variance, variables: method_type.free_variables))
+              method_type = method_type.subst(
+                constraints.solution(
+                  checker,
+                  self_type: self_type,
+                  instance_type: module_context.instance_type,
+                  class_type: module_context.module_type,
+                  variance: variance,
+                  variables: method_type.free_variables
+                )
+              )
             end
           end
         end
diff --git a/lib/steep/type_inference/local_variable_type_env.rb b/lib/steep/type_inference/local_variable_type_env.rb
index 7f452c883..a9314cd7a 100644
--- a/lib/steep/type_inference/local_variable_type_env.rb
+++ b/lib/steep/type_inference/local_variable_type_env.rb
@@ -1,9 +1,6 @@
 module Steep
   module TypeInference
     class LocalVariableTypeEnv
-      attr_reader :subtyping
-      attr_reader :self_type
-
       class Entry
         attr_reader :type
         attr_reader :annotations
@@ -39,31 +36,46 @@ def optional
         end
       end
 
+      attr_reader :subtyping
+      attr_reader :self_type
+      attr_reader :instance_type
+      attr_reader :class_type
       attr_reader :declared_types
       attr_reader :assigned_types
 
-      def self.empty(subtyping:, self_type:)
-        new(subtyping: subtyping, declared_types: {}, assigned_types: {}, self_type: self_type)
+      def self.empty(subtyping:, self_type:, instance_type:, class_type:)
+        new(
+          subtyping: subtyping,
+          declared_types: {},
+          assigned_types: {},
+          self_type: self_type,
+          instance_type: instance_type,
+          class_type: class_type
+        )
       end
 
-      def initialize(subtyping:, declared_types:, assigned_types:, self_type:)
+      def initialize(subtyping:, declared_types:, assigned_types:, self_type:, instance_type:, class_type:)
         @subtyping = subtyping
         @self_type = self_type
 
         @declared_types = declared_types
         @assigned_types = assigned_types
+        @class_type = class_type
+        @instance_type = instance_type
 
         unless (intersection = Set.new(declared_types.keys) & Set.new(assigned_types.keys)).empty?
           raise "Declared types and assigned types should be disjoint: #{intersection}"
         end
       end
 
-      def update(declared_types: self.declared_types, assigned_types: self.assigned_types, self_type: self.self_type)
+      def update(declared_types: self.declared_types, assigned_types: self.assigned_types, self_type: self.self_type, instance_type: self.instance_type, class_type: self.class_type)
         self.class.new(
           subtyping: subtyping,
           declared_types: declared_types,
           assigned_types: assigned_types,
-          self_type: self_type
+          self_type: self_type,
+          instance_type: instance_type,
+          class_type: class_type
         )
       end
 
@@ -73,7 +85,7 @@ def assign!(var, node:, type:)
         if declared_type
           relation = Subtyping::Relation.new(sub_type: type, super_type: declared_type)
           constraints = Subtyping::Constraints.new(unknowns: Set.new)
-          subtyping.check(relation, constraints: constraints, self_type: self_type).else do |result|
+          subtyping.check(relation, constraints: constraints, self_type: self_type, instance_type: instance_type, class_type: class_type).else do |result|
             yield declared_type, type, result
           end
         end
@@ -89,7 +101,7 @@ def assign(var, node:, type:)
         if declared_type
           relation = Subtyping::Relation.new(sub_type: type, super_type: declared_type)
           constraints = Subtyping::Constraints.new(unknowns: Set.new)
-          subtyping.check(relation, constraints: constraints, self_type: self_type).else do |result|
+          subtyping.check(relation, constraints: constraints, self_type: self_type, instance_type: instance_type, class_type: class_type).else do |result|
             yield declared_type, type, result
           end
 
@@ -113,7 +125,7 @@ def annotate(collection)
           if outer_type
             relation = Subtyping::Relation.new(sub_type: inner_type, super_type: outer_type)
             constraints = Subtyping::Constraints.new(unknowns: Set.new)
-            subtyping.check(relation, constraints: constraints, self_type: self_type).else do |result|
+            subtyping.check(relation, constraints: constraints, self_type: self_type, instance_type: instance_type, class_type: class_type).else do |result|
               if block_given?
                 yield var, outer_type, inner_type, result
               end
@@ -194,7 +206,9 @@ def join(*envs)
               subtyping: subtyping,
               self_type: self_type,
               declared_types: declared_types,
-              assigned_types: assigned_types
+              assigned_types: assigned_types,
+              instance_type: instance_type,
+              class_type: class_type
             )
           end
 
diff --git a/lib/steep/type_inference/logic_type_interpreter.rb b/lib/steep/type_inference/logic_type_interpreter.rb
index 28afe1f94..748dfdb86 100644
--- a/lib/steep/type_inference/logic_type_interpreter.rb
+++ b/lib/steep/type_inference/logic_type_interpreter.rb
@@ -283,7 +283,7 @@ def type_case_select0(type, klass)
 
         else
           relation = Subtyping::Relation.new(sub_type: type, super_type: instance_type)
-          if subtyping.check(relation, constraints: Subtyping::Constraints.empty, self_type: AST::Types::Self.new).success?
+          if subtyping.check(relation, constraints: Subtyping::Constraints.empty, self_type: AST::Types::Self.new, instance_type: AST::Types::Instance.new, class_type: AST::Types::Class.new).success?
             [
               [type],
               []
diff --git a/lib/steep/type_inference/type_env.rb b/lib/steep/type_inference/type_env.rb
index abaa9cd95..bf3fed4bf 100644
--- a/lib/steep/type_inference/type_env.rb
+++ b/lib/steep/type_inference/type_env.rb
@@ -38,19 +38,23 @@ def self.build(annotations:, signatures:, subtyping:, const_env:)
         end
       end
 
-      def with_annotations(ivar_types: {}, const_types: {}, gvar_types: {}, self_type:, &block)
+      def with_annotations(ivar_types: {}, const_types: {}, gvar_types: {}, self_type:, instance_type:, class_type:, &block)
         dup.tap do |env|
-          merge!(original_env: env.ivar_types, override_env: ivar_types, self_type: self_type, &block)
-          merge!(original_env: env.gvar_types, override_env: gvar_types, self_type: self_type, &block)
+          merge!(original_env: env.ivar_types, override_env: ivar_types, self_type: self_type, instance_type: instance_type, class_type: class_type, &block)
+          merge!(original_env: env.gvar_types, override_env: gvar_types, self_type: self_type, instance_type: instance_type, class_type: class_type, &block)
 
           const_types.each do |name, annotated_type|
             original_type = self.const_types[name] || const_env.lookup(name)
             if original_type
-              assert_annotation name,
-                                original_type: original_type,
-                                annotated_type: annotated_type,
-                                self_type: self_type,
-                                &block
+              assert_annotation(
+                name,
+                original_type: original_type,
+                annotated_type: annotated_type,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                &block
+              )
             end
             env.const_types[name] = annotated_type
           end
@@ -101,13 +105,20 @@ def set(const: nil, gvar: nil, ivar: nil, type:)
       # @type method assign: (const: TypeName, type: AST::Type) { (Subtyping::Result::Failure | nil) -> void } -> AST::Type
       #                    | (gvar: Symbol, type: AST::Type) { (Subtyping::Result::Failure | nil) -> void } -> AST::Type
       #                    | (ivar: Symbol, type: AST::Type) { (Subtyping::Result::Failure | nil) -> void } -> AST::Type
-      def assign(const: nil, gvar: nil, ivar: nil, type:, self_type:, &block)
+      def assign(const: nil, gvar: nil, ivar: nil, type:, self_type:, instance_type:, class_type:, &block)
         case
         when const
           yield_self do
             const_type = const_types[const] || const_env.lookup(const)
             if const_type
-              assert_assign(var_type: const_type, lhs_type: type, self_type: self_type, &block)
+              assert_assign(
+                var_type: const_type,
+                lhs_type: type,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                &block
+              )
             else
               yield nil
               AST::Types::Any.new
@@ -116,7 +127,14 @@ def assign(const: nil, gvar: nil, ivar: nil, type:, self_type:, &block)
         else
           lookup_dictionary(ivar: ivar, gvar: gvar) do |var_name, dictionary|
             if dictionary.key?(var_name)
-              assert_assign(var_type: dictionary[var_name], lhs_type: type, self_type: self_type, &block)
+              assert_assign(
+                var_type: dictionary[var_name],
+                lhs_type: type,
+                self_type: self_type,
+                instance_type: instance_type,
+                class_type: class_type,
+                &block
+              )
             else
               yield nil
               AST::Types::Any.new
@@ -134,7 +152,7 @@ def lookup_dictionary(ivar:, gvar:)
         end
       end
 
-      def assert_assign(var_type:, lhs_type:, self_type:)
+      def assert_assign(var_type:, lhs_type:, self_type:, instance_type:, class_type:)
         return var_type if var_type == lhs_type
 
         var_type = subtyping.expand_alias(var_type)
@@ -143,20 +161,28 @@ def assert_assign(var_type:, lhs_type:, self_type:)
         relation = Subtyping::Relation.new(sub_type: lhs_type, super_type: var_type)
         constraints = Subtyping::Constraints.new(unknowns: Set.new)
 
-        subtyping.check(relation, self_type: self_type, constraints: constraints).else do |result|
+        subtyping.check(relation, self_type: self_type, constraints: constraints, instance_type: instance_type, class_type: class_type).else do |result|
           yield result
         end
 
         var_type
       end
 
-      def merge!(original_env:, override_env:, self_type:, &block)
+      def merge!(original_env:, override_env:, self_type:, instance_type:, class_type:, &block)
         original_env.merge!(override_env) do |name, original_type, override_type|
-          assert_annotation name, annotated_type: override_type, original_type: original_type, self_type: self_type, &block
+          assert_annotation(
+            name,
+            annotated_type: override_type,
+            original_type: original_type,
+            self_type: self_type,
+            instance_type: instance_type,
+            class_type: class_type,
+            &block
+          )
         end
       end
 
-      def assert_annotation(name, annotated_type:, original_type:, self_type:)
+      def assert_annotation(name, annotated_type:, original_type:, self_type:, instance_type:, class_type:)
         return annotated_type if annotated_type == original_type
 
         annotated_type = subtyping.expand_alias(annotated_type)
@@ -165,7 +191,7 @@ def assert_annotation(name, annotated_type:, original_type:, self_type:)
         relation = Subtyping::Relation.new(sub_type: annotated_type, super_type: original_type)
         constraints = Subtyping::Constraints.new(unknowns: Set.new)
 
-        subtyping.check(relation, constraints: constraints, self_type: self_type).else do |result|
+        subtyping.check(relation, constraints: constraints, self_type: self_type, instance_type: instance_type, class_type: class_type).else do |result|
           yield name, relation, result
         end
 
diff --git a/test/constraints_test.rb b/test/constraints_test.rb
index 06d357809..a6f7657e1 100644
--- a/test/constraints_test.rb
+++ b/test/constraints_test.rb
@@ -78,7 +78,14 @@ def test_subst
         contravariants: Set.new([:b, :c])
       )
 
-      subst = constraints.solution(checker, self_type: AST::Types::Self.new, variance: variance, variables: Set.new([:a, :b, :c]))
+      subst = constraints.solution(
+        checker,
+        self_type: AST::Types::Self.new,
+        instance_type: AST::Types::Instance.new,
+        class_type: AST::Types::Class.new,
+        variance: variance,
+        variables: Set.new([:a, :b, :c])
+      )
 
       assert_equal string, subst[:a]
       assert_equal integer, subst[:b]
@@ -102,7 +109,14 @@ def test_subst2
         contravariants: Set.new([:b, :c])
       )
 
-      subst = constraints.solution(checker, self_type: AST::Types::Self.new, variance: variance, variables: Set.new([:a, :b]))
+      subst = constraints.solution(
+        checker,
+        self_type: AST::Types::Self.new,
+        instance_type: AST::Types::Instance.new,
+        class_type: AST::Types::Class.new,
+        variance: variance,
+        variables: Set.new([:a, :b])
+      )
 
       assert_equal string, subst[:a]
       assert_equal integer, subst[:b]
diff --git a/test/local_variable_type_env_test.rb b/test/local_variable_type_env_test.rb
index f4e23d993..7970e2c54 100644
--- a/test/local_variable_type_env_test.rb
+++ b/test/local_variable_type_env_test.rb
@@ -18,7 +18,9 @@ def test_assign_no_decl
         subtyping: checker,
         declared_types: {},
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -44,7 +46,9 @@ def test_assign_with_decl_no_error
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::Integer | ::String")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -67,7 +71,9 @@ def test_assign_with_decl_type_error
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::Integer | ::String")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -94,7 +100,9 @@ def test_annotate
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::Integer | ::String")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -123,7 +131,9 @@ def test_annotate_with_error
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::Integer | ::String")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -155,7 +165,9 @@ def test_annotate_block
         subtyping: checker,
         declared_types: {},
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -189,7 +201,9 @@ def test_for_loop_no_decl
         subtyping: checker,
         declared_types: {},
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -221,7 +235,9 @@ def test_for_loop_with_decl
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::String | ::Integer")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -250,7 +266,9 @@ def test_for_loop_assign_and_decl_error
         subtyping: checker,
         declared_types: {},
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -285,7 +303,9 @@ def test_for_loop_assign_and_decl_error2
         subtyping: checker,
         declared_types: {},
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       source = parse_ruby(<<EOF)
@@ -343,7 +363,9 @@ def test_join_assignment
         subtyping: checker,
         declared_types: {},
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       env2 = LocalVariableTypeEnv.new(
@@ -351,7 +373,9 @@ def test_join_assignment
         declared_types: {},
         assigned_types: { x: Entry.new(type: parse_type("::String")),
                           y: Entry.new(type: parse_type("::Symbol")) },
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       env3 = LocalVariableTypeEnv.new(
@@ -359,7 +383,9 @@ def test_join_assignment
         declared_types: {},
         assigned_types: { x: Entry.new(type: parse_type("::Integer")),
                           z: Entry.new(type: parse_type("::Array[::Integer]")) },
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       join = env1.join(env2, env3)
@@ -391,7 +417,9 @@ def test_join_with_decl
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::String | ::Integer | ::Symbol")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       env2 = LocalVariableTypeEnv.new(
@@ -399,14 +427,18 @@ def test_join_with_decl
         declared_types: { x: Entry.new(type: parse_type("::String")),
                           y: Entry.new(type: parse_type("::String")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       env3 = LocalVariableTypeEnv.new(
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::Integer")) },
         assigned_types: {},
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       join = env1.join(env2, env3)
@@ -430,14 +462,18 @@ def test_join_loop_assignment
         subtyping: checker,
         declared_types: {},
         assigned_types: { x: Entry.new(type: parse_type("::String")) },
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       env2 = LocalVariableTypeEnv.new(
         subtyping: checker,
         declared_types: { x: Entry.new(type: parse_type("::String")) },
         assigned_types: { y: Entry.new(type: parse_type("::Integer")) },
-        self_type: parse_type("::Object")
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
       )
 
       join = env1.join(env1, env2)
diff --git a/test/logic_test.rb b/test/logic_test.rb
index b94a183ed..98f64f7a4 100644
--- a/test/logic_test.rb
+++ b/test/logic_test.rb
@@ -143,7 +143,12 @@ def test_environments
     with_checker do |checker|
       logic = Logic.new(subtyping: checker)
 
-      env = LocalVariableTypeEnv.empty(subtyping: checker, self_type: parse_type("::Object"))
+      env = LocalVariableTypeEnv.empty(
+        subtyping: checker,
+        self_type: parse_type("::Object"),
+        instance_type: parse_type("::Object"),
+        class_type: parse_type("singleton(::Object)")
+      )
         .assign(:x, type: parse_type("::Integer?"), node: nil)
 
       truthy, falsey = logic.environments(truthy_vars: Set[:x], falsey_vars: Set[:x], lvar_env: env)
diff --git a/test/rbs_index_test.rb b/test/rbs_index_test.rb
index a34ba2355..16c1a15c7 100644
--- a/test/rbs_index_test.rb
+++ b/test/rbs_index_test.rb
@@ -6,22 +6,6 @@ class RBSIndexTest < Minitest::Test
 
   RBSIndex = Steep::Index::RBSIndex
 
-  def test_class_decl
-    with_factory({ "a.rbs" => <<-RBS }) do |factory|
-class HelloWorld
-end
-    RBS
-      env = factory.definition_builder.env
-
-      index = RBSIndex.new()
-      builder = RBSIndex::Builder.new(index: index)
-
-      builder.env(env)
-
-      assert_equal 1, index.each_declaration(type_name: TypeName("::HelloWorld")).count
-    end
-  end
-
   def test_class_decl
     with_factory({ "a.rbs" => <<-RBS }) do |factory|
 module HelloWorld
diff --git a/test/subtyping_test.rb b/test/subtyping_test.rb
index f34bf9fc4..6efea482b 100644
--- a/test/subtyping_test.rb
+++ b/test/subtyping_test.rb
@@ -84,6 +84,18 @@ def parse_relation(sub_type, super_type, checker:)
     )
   end
 
+  def self_type
+    AST::Types::Self.new()
+  end
+
+  def instance_type
+    AST::Types::Instance.new
+  end
+
+  def class_type
+    AST::Types::Class.new()
+  end
+
   def with_checker(*files, nostdlib: false, &block)
     paths = {}
 
@@ -118,6 +130,8 @@ def test_reflexive
       result = checker.check(
         Relation.new(sub_type: type, super_type: type),
         self_type: parse_type("self", checker: checker),
+        instance_type: instance_type,
+        class_type: class_type,
         constraints: Constraints.empty
       )
 
@@ -136,8 +150,8 @@ def foo: -> untyped
 end
     EOS
 
-      assert_success_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_success_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "::_A", "::_B"
+      assert_success_check checker, "::_B", "::_A"
     end
   end
 
@@ -152,8 +166,8 @@ def bar: -> untyped
   def foo: -> untyped
 end
     EOS
-      assert_success_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_fail_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_success_check checker, "::_A", "::_B"
+      assert_fail_check checker, "::_B", "::_A" do |result|
         assert_instance_of Failure::MethodMissingError, result.error
         assert_equal :bar, result.error.name
       end
@@ -171,7 +185,7 @@ def foo: -> String
 end
     EOS
 
-      assert_fail_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_A", "::_B" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
     end
@@ -188,8 +202,8 @@ def foo: (?Integer, ?foo: Symbol) -> untyped
 end
     EOS
 
-      assert_success_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_fail_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_success_check checker, "::_B", "::_A"
+      assert_fail_check checker, "::_A", "::_B" do |result|
         assert_instance_of Failure::ParameterMismatchError, result.error
         assert_equal :foo, result.error.name
       end
@@ -206,12 +220,12 @@ def foo: [A] () -> A
   def foo: () -> Integer
 end
     EOS
-      assert_fail_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_B", "::_A" do |result|
         assert_instance_of Failure::PolyMethodSubtyping, result.error
         assert_equal :foo, result.error.name
       end
 
-      assert_success_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "::_A", "::_B"
     end
   end
 
@@ -226,12 +240,12 @@ def foo: (String) -> Integer
 end
     EOS
 
-      assert_fail_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_A", "::_B" do |result|
         assert_instance_of Failure::PolyMethodSubtyping, result.error
         assert_equal :foo, result.error.name
       end
 
-      assert_fail_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_B", "::_A" do |result|
         assert_instance_of Failure::PolyMethodSubtyping, result.error
         assert_equal :foo, result.error.name
       end
@@ -248,11 +262,11 @@ def foo: [X] (X) -> Object
   def foo: (String) -> Integer
 end
     EOS
-      assert_fail_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_B", "::_A" do |result|
         assert_instance_of Failure::PolyMethodSubtyping, result.error
       end
 
-      assert_fail_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_A", "::_B" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
     end
@@ -298,8 +312,8 @@ def foo: [A, B] (A) -> B
   def foo: [X, Y] (X) -> Y
 end
     EOS
-      assert_success_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_success_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "::_A", "::_B"
+      assert_success_check checker, "::_B", "::_A"
     end
   end
 
@@ -315,9 +329,9 @@ def foo: (String) -> String
 end
     EOS
 
-      assert_success_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "::_A", "::_B"
 
-      assert_fail_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_B", "::_A" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
     end
@@ -334,9 +348,9 @@ def foo: () { () -> String } -> Object
 end
     EOS
 
-      assert_success_result checker.check(parse_relation("::_A", "::_B", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "::_A", "::_B"
 
-      assert_fail_result checker.check(parse_relation("::_B", "::_A", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::_B", "::_A" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
     end
@@ -344,13 +358,13 @@ def foo: () { () -> String } -> Object
 
   def test_literal
     with_checker do |checker|
-      assert_success_result checker.check(parse_relation("123", "::Integer", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "123", "::Integer"
 
-      assert_fail_result checker.check(parse_relation("::Integer", "123", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "::Integer", "123" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
 
-      assert_fail_result checker.check(parse_relation(":foo", "::Integer", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, ":foo", "::Integer" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
     end
@@ -358,36 +372,39 @@ def test_literal
 
   def test_literal_bidirectional
     with_checker do |checker|
-      assert_success_result checker.check(parse_relation("true", "::TrueClass", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_success_result checker.check(parse_relation("::TrueClass", "true", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "true", "::TrueClass"
+      assert_success_check checker, "::TrueClass", "true"
 
-      assert_success_result checker.check(parse_relation("false", "::FalseClass", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_success_result checker.check(parse_relation("::FalseClass", "false", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "false", "::FalseClass"
+      assert_success_check checker, "::FalseClass", "false"
     end
   end
 
   def test_nil_type
     with_checker do |checker|
-      assert_success_result checker.check(parse_relation("nil", "::NilClass", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-      assert_success_result checker.check(parse_relation("::NilClass", "nil", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "nil", "::NilClass"
+      assert_success_check checker, "::NilClass", "nil"
     end
   end
 
   def test_void
     with_checker do |checker|
-      assert_success_result checker.check(parse_relation("void", "void", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
-
-      assert_success_result checker.check(parse_relation("::Integer", "void", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+      assert_success_check checker, "void", "void"
+      assert_success_check checker, "::Integer", "void"
 
-      assert_fail_result checker.check(parse_relation("void", "::String", checker: checker), self_type: parse_type("self", checker: checker), constraints: Constraints.empty) do |result|
+      assert_fail_check checker, "void", "::String" do |result|
         assert_instance_of Failure::UnknownPairError, result.error
       end
     end
   end
 
-  def assert_success_check(checker, sub_type, super_type, self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+  def assert_success_check(checker, sub_type, super_type, self_type: parse_type("self", checker: checker), instance_type: parse_type("instance", checker: checker), class_type: parse_type("class", checker: checker), constraints: Constraints.empty)
+    self_type = parse_type(self_type, checker: checker) if self_type.is_a?(String)
+    instance_type = parse_type(instance_type, checker: checker) if instance_type.is_a?(String)
+    class_type = parse_type(class_type, checker: checker) if class_type.is_a?(String)
+
     relation = parse_relation(sub_type, super_type, checker: checker)
-    result = checker.check(relation, self_type: self_type, constraints: constraints)
+    result = checker.check(relation, self_type: self_type, instance_type: instance_type, class_type: class_type, constraints: constraints)
 
     assert result.instance_of?(Subtyping::Result::Success), message {
       str = ""
@@ -401,9 +418,19 @@ def assert_success_check(checker, sub_type, super_type, self_type: parse_type("s
     yield result if block_given?
   end
 
-  def assert_fail_check(checker, sub_type, super_type, self_type: parse_type("self", checker: checker), constraints: Constraints.empty)
+  def assert_fail_check(checker, sub_type, super_type, self_type: nil, instance_type: nil, class_type: nil, constraints: Constraints.empty)
+    self_type = parse_type(self_type, checker: checker) if self_type.is_a?(String)
+    instance_type = parse_type(instance_type, checker: checker) if instance_type.is_a?(String)
+    class_type = parse_type(class_type, checker: checker) if class_type.is_a?(String)
+
     relation = parse_relation(sub_type, super_type, checker: checker)
-    result = checker.check(relation, self_type: self_type, constraints: constraints)
+    result = checker.check(
+      relation,
+      self_type: self_type,
+      instance_type: instance_type,
+      class_type: class_type,
+      constraints: constraints
+    )
 
     assert result.instance_of?(Subtyping::Result::Failure), message {
       str = ""
@@ -473,6 +500,8 @@ def test_caching
           super_type: AST::Types::Var.new(name: :foo)
         ),
         self_type: parse_type("self", checker: checker),
+        instance_type: nil,
+        class_type: nil,
         constraints: Subtyping::Constraints.empty
       )
 
@@ -484,6 +513,8 @@ def test_caching
       checker.check(
         parse_relation("::Integer", "::Object", checker: checker),
         self_type: parse_type("self", checker: checker),
+        instance_type: nil,
+        class_type: nil,
         constraints: Subtyping::Constraints.empty
       )
 
@@ -577,7 +608,14 @@ def set: (String) -> self
         assert_equal "::String", result.constraints.lower_bound(:T).to_s
 
         variance = Subtyping::VariableVariance.new(covariants: Set[:T], contravariants: Set[:T])
-        s = result.constraints.solution(checker, variance: variance, variables: Set[:T], self_type: parse_type("self", checker: checker))
+        s = result.constraints.solution(
+          checker,
+          variance: variance,
+          variables: Set[:T],
+          self_type: parse_type("self", checker: checker),
+          instance_type: parse_type("instance", checker: checker),
+          class_type: parse_type("class", checker: checker)
+        )
         assert_equal "::String", s[:T].to_s
       end
     end
@@ -832,4 +870,39 @@ def test_proc_type
       assert_fail_check checker, "^() { () -> ::String } -> void", "^() { () -> ::Object } -> void"
     end
   end
+
+  def test_self_type
+    with_checker do |checker|
+      assert_success_check checker, "self", "::Integer", self_type: "::Integer"
+      assert_success_check checker, "self", "::Object", self_type: "::Integer"
+      assert_fail_check checker, "self", "::String", self_type: "::Integer"
+
+      assert_fail_check checker, "::Integer", "self", self_type: "::Integer"
+      assert_fail_check checker, "::String", "self", self_type: "::Integer"
+      assert_fail_check checker, "::Object", "self", self_type: "::Integer"
+    end
+  end
+
+  def test_instance_type
+    with_checker do |checker|
+      assert_success_check checker, "instance", "::Integer", instance_type: "::Integer"
+      assert_success_check checker, "instance", "::Object", instance_type: "::Integer"
+      assert_fail_check checker, "instance", "::String", instance_type: "::Integer"
+
+      assert_success_check checker, "::Integer", "instance", instance_type: "::Integer"
+      assert_fail_check checker, "::String", "instance", instance_type: "::Integer"
+      assert_fail_check checker, "::Object", "instance", instance_type: "::Integer"
+    end
+  end
+
+  def test_class_type
+    with_checker do |checker|
+      assert_success_check checker, "class", "singleton(::Integer)", class_type: "singleton(::Integer)"
+      assert_success_check checker, "class", "singleton(::Object)", class_type: "singleton(::Integer)"
+      assert_fail_check checker, "class", "singleton(::String)", class_type: "singleton(::Integer)"
+
+      assert_success_check checker, "singleton(::Integer)", "class", class_type: "singleton(::Integer)"
+      assert_fail_check checker, "singleton(::Object)", "class", class_type: "singleton(::Integer)"
+    end
+  end
 end
diff --git a/test/test_helper.rb b/test/test_helper.rb
index 81f88fe22..9728e2901 100644
--- a/test/test_helper.rb
+++ b/test/test_helper.rb
@@ -493,7 +493,9 @@ def with_standard_construction(checker, source)
                              signatures: checker.factory.env)
     lvar_env = LocalVariableTypeEnv.empty(
       subtyping: checker,
-      self_type: self_type
+      self_type: self_type,
+      instance_type: AST::Builtin::Object.instance_type,
+      class_type: AST::Builtin::Object.module_type,
     ).annotate(annotations)
 
     context = Context.new(
diff --git a/test/type_construction_test.rb b/test/type_construction_test.rb
index 4e4ef115f..28ced9b03 100644
--- a/test/type_construction_test.rb
+++ b/test/type_construction_test.rb
@@ -1037,7 +1037,9 @@ class Names
                                signatures: checker.factory.env)
       lvar_env = LocalVariableTypeEnv.empty(
         subtyping: checker,
-        self_type: parse_type("singleton(::Steep::Names::Module)")
+        self_type: parse_type("singleton(::Steep::Names::Module)"),
+        instance_type: parse_type("::Steep"),
+        class_type: parse_type("singleton(::Steep)")
       ).annotate(annotations)
 
       module_context = Context::ModuleContext.new(
@@ -1135,8 +1137,10 @@ class Steep end
                                signatures: checker.factory.env)
       lvar_env = LocalVariableTypeEnv.empty(
         subtyping: checker,
-        self_type: parse_type("singleton(::Steep)")
-      )
+        self_type: parse_type("singleton(::Steep)"),
+        instance_type: parse_type("::Steep"),
+        class_type: parse_type("singleton(::Steep)")
+        )
 
       module_context = Context::ModuleContext.new(
         instance_type: parse_type("::Steep"),
@@ -2506,6 +2510,161 @@ def foo
     end
   end
 
+  def test_instance_type_defn
+    with_checker <<-EOF do |checker|
+class Hoge
+  def foo: (instance) -> void
+  def bar: () -> instance
+end
+    EOF
+
+      source = parse_ruby(<<-'EOF')
+class Hoge
+  def foo(hoge)
+    hoge.bar()
+
+    # @type var x: Hoge
+    x = hoge
+  end
+
+  def bar
+    Hoge.new()
+  end
+end
+      EOF
+
+      with_standard_construction(checker, source) do |construction, typing|
+        construction.synthesize(source.node)
+
+        assert_no_error typing
+      end
+    end
+  end
+
+  def test_instance_type_send
+    with_checker <<-EOF do |checker|
+class Hoge
+  def foo: (instance) -> void
+  def bar: () -> instance
+end
+    EOF
+
+      source = parse_ruby(<<-'EOF')
+Hoge.new.foo(Hoge.new)
+Hoge.new.bar().bar()
+      EOF
+
+      with_standard_construction(checker, source) do |construction, typing|
+        construction.synthesize(source.node)
+
+        assert_no_error typing
+      end
+    end
+  end
+
+  def test_instance_type_poly
+    with_checker <<-EOF do |checker|
+class Hoge
+  def foo: (instance) -> void
+end
+
+class Huga < Hoge
+end
+    EOF
+
+      source = parse_ruby(<<-'EOF')
+Hoge.new.foo(Huga.new)
+Huga.new.foo(Hoge.new)
+      EOF
+
+      with_standard_construction(checker, source) do |construction, typing|
+        construction.synthesize(source.node)
+
+        assert_typing_error(typing, size: 1) do |errors|
+          assert_any!(errors) do |error|
+            assert_instance_of Diagnostic::Ruby::ArgumentTypeMismatch, error
+          end
+        end
+      end
+    end
+  end
+
+  def test_class_type_defn
+    with_checker <<-EOF do |checker|
+class Hoge
+  def foo: (class) -> void
+  def bar: () -> class
+end
+    EOF
+
+      source = parse_ruby(<<-'EOF')
+class Hoge
+  def foo(hoge)
+    hoge.new
+  end
+
+  def bar
+    Hoge
+  end
+end
+      EOF
+
+      with_standard_construction(checker, source) do |construction, typing|
+        construction.synthesize(source.node)
+
+        assert_no_error typing
+      end
+    end
+  end
+
+  def test_class_type_send
+    with_checker <<-EOF do |checker|
+class Hoge
+  def foo: (class) -> void
+  def bar: () -> class
+end
+    EOF
+
+      source = parse_ruby(<<-'EOF')
+Hoge.new.foo(Hoge)
+Hoge.new.bar().new
+      EOF
+
+      with_standard_construction(checker, source) do |construction, typing|
+        construction.synthesize(source.node)
+
+        assert_no_error typing
+      end
+    end
+  end
+
+  def test_class_type_poly
+    with_checker <<-EOF do |checker|
+class Hoge
+  def foo: (class) -> void
+end
+
+class Huga < Hoge
+end
+    EOF
+
+      source = parse_ruby(<<-'EOF')
+Hoge.new.foo(Huga)
+Huga.new.foo(Hoge)
+      EOF
+
+      with_standard_construction(checker, source) do |construction, typing|
+        construction.synthesize(source.node)
+
+        assert_typing_error(typing, size: 1) do |errors|
+          assert_any!(errors) do |error|
+            assert_instance_of Diagnostic::Ruby::ArgumentTypeMismatch, error
+          end
+        end
+      end
+    end
+  end
+
   def test_void
     with_checker <<-EOF do |checker|
 class Hoge
diff --git a/test/type_env_test.rb b/test/type_env_test.rb
index 22ded3f7d..8ab5fc5b5 100644
--- a/test/type_env_test.rb
+++ b/test/type_env_test.rb
@@ -17,9 +17,13 @@ def test_ivar_without_annotation
 
       # If no annotation is given to ivar, assign yields the block with nil and returns `any`
       yield_self do
-        ivar_type = type_env.assign(ivar: :"@x",
-                                    type: AST::Types::Name.new_instance(name: "::String"),
-                                    self_type: parse_type("self")) { |error| assert_nil error }
+        ivar_type = type_env.assign(
+          ivar: :"@x",
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) { |error| assert_nil error }
         assert_instance_of AST::Types::Any, ivar_type
       end
 
@@ -46,9 +50,13 @@ def test_ivar_with_annotation
 
       # If annotation is given and assigned type is compatible with that, assign returns annotated type, no yield
       yield_self do
-        ivar_type = type_env.assign(ivar: :"@x",
-                                    type: AST::Types::Name.new_instance(name: "::Integer"),
-                                    self_type: parse_type("self")) do |_|
+        ivar_type = type_env.assign(
+          ivar: :"@x",
+          type: AST::Types::Name.new_instance(name: "::Integer"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_|
           raise
         end
         assert_equal AST::Types::Name.new_instance(name: "::Numeric"), ivar_type
@@ -56,9 +64,13 @@ def test_ivar_with_annotation
 
       # If annotation is given and assigned type is incompatible with that, assign returns annotated type and yield an failure result
       yield_self do
-        ivar_type = type_env.assign(ivar: :"@x",
-                                    type: AST::Types::Name.new_instance(name: "::String"),
-                                    self_type: parse_type("self")) do |error|
+        ivar_type = type_env.assign(
+          ivar: :"@x",
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |error|
           assert_instance_of Subtyping::Result::Failure, error
         end
         assert_equal AST::Types::Name.new_instance(name: "::Numeric"), ivar_type
@@ -73,9 +85,13 @@ def test_gvar_without_annotation
 
       # If no annotation is given to ivar, assign yields the block with nil and returns `any`
       yield_self do
-        type = type_env.assign(gvar: :"$x",
-                               type: AST::Types::Name.new_instance(name: "::String"),
-                               self_type: parse_type("self")) { |error| assert_nil error }
+        type = type_env.assign(
+          gvar: :"$x",
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) { |error| assert_nil error }
         assert_instance_of AST::Types::Any, type
       end
 
@@ -102,9 +118,13 @@ def test_gvar_with_annotation
 
       # If annotation is given and assigned type is compatible with that, assign returns annotated type, no yield
       yield_self do
-        type = type_env.assign(gvar: :"$x",
-                               type: AST::Types::Name.new_instance(name: "::Integer"),
-                               self_type: parse_type("self")) do |_|
+        type = type_env.assign(
+          gvar: :"$x",
+          type: AST::Types::Name.new_instance(name: "::Integer"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_|
           raise
         end
         assert_equal AST::Types::Name.new_instance(name: "::Numeric"), type
@@ -112,9 +132,13 @@ def test_gvar_with_annotation
 
       # If annotation is given and assigned type is incompatible with that, assign returns annotated type and yield an failure result
       yield_self do
-        type = type_env.assign(gvar: :"$x",
-                               type: AST::Types::Name.new_instance(name: "::String"),
-                               self_type: parse_type("self")) do |error|
+        type = type_env.assign(
+          gvar: :"$x",
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |error|
           assert_instance_of Subtyping::Result::Failure, error
         end
         assert_equal AST::Types::Name.new_instance(name: "::Numeric"), type
@@ -135,18 +159,26 @@ def test_const_without_annotation
       end
 
       yield_self do
-        type = type_env.assign(const: TypeName("Regexp"),
-                               type: AST::Types::Name.new_instance(name: "::String"),
-                               self_type: parse_type("self")) do |error|
+        type = type_env.assign(
+          const: TypeName("Regexp"),
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |error|
           assert_instance_of Subtyping::Result::Failure, error
         end
         assert_equal AST::Types::Name.new_singleton(name: "::Regexp"), type
       end
 
       yield_self do
-        type = type_env.assign(const: TypeName("Regexp"),
-                               type: AST::Types::Any.new,
-                               self_type: parse_type("self")) do |_|
+        type = type_env.assign(
+          const: TypeName("Regexp"),
+          type: AST::Types::Any.new,
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_|
           raise
         end
         assert_equal AST::Types::Name.new_singleton(name: "::Regexp"), type
@@ -161,9 +193,13 @@ def test_const_without_annotation
       end
 
       yield_self do
-        type = type_env.assign(const: TypeName("HOGE"),
-                               type: AST::Types::Name.new_instance(name: "::String"),
-                               self_type: parse_type("self")) do |error|
+        type = type_env.assign(
+          const: TypeName("HOGE"),
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |error|
           assert_nil error
         end
         assert_instance_of AST::Types::Any, type
@@ -184,18 +220,26 @@ def test_const_with_annotation
       end
 
       yield_self do
-        type = type_env.assign(const: TypeName("Regexp"),
-                               type: AST::Types::Name.new_instance(name: "::Integer"),
-                               self_type: parse_type("self")) do |error|
+        type = type_env.assign(
+          const: TypeName("Regexp"),
+          type: AST::Types::Name.new_instance(name: "::Integer"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |error|
           assert_instance_of Subtyping::Result::Failure, error
         end
         assert_equal AST::Types::Name.new_instance(name: "::String"), type
       end
 
       yield_self do
-        type = type_env.assign(const: TypeName("Regexp"),
-                               type: AST::Types::Name.new_instance(name: "::String"),
-                               self_type: parse_type("self")) do |_|
+        type = type_env.assign(
+          const: TypeName("Regexp"),
+          type: AST::Types::Name.new_instance(name: "::String"),
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_|
           raise
         end
         assert_equal AST::Types::Name.new_instance(name: "::String"), type
@@ -216,11 +260,14 @@ def test_with_annotation_ivar
       original_env.set(ivar: :"@x", type: union_type)
 
       yield_self do
-        type_env = original_env.with_annotations(ivar_types:
-                                                   {
-                                                     "@x": AST::Types::Name.new_instance(name: "::String")
-                                                   },
-                                                 self_type: parse_type("self")) do |_, _, _|
+        type_env = original_env.with_annotations(
+          ivar_types: {
+            "@x": AST::Types::Name.new_instance(name: "::String")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_, _, _|
           raise
         end
 
@@ -228,11 +275,14 @@ def test_with_annotation_ivar
       end
 
       yield_self do
-        type_env = original_env.with_annotations(ivar_types:
-                                                   {
-                                                     "@x": AST::Types::Name.new_instance(name: "::Regexp")
-                                                   },
-                                                 self_type: parse_type("self")) do |name, relation, error|
+        type_env = original_env.with_annotations(
+          ivar_types: {
+            "@x": AST::Types::Name.new_instance(name: "::Regexp")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |name, relation, error|
           assert_equal name, :"@x"
           assert_instance_of Subtyping::Result::Failure, error
         end
@@ -241,11 +291,14 @@ def test_with_annotation_ivar
       end
 
       yield_self do
-        type_env = original_env.with_annotations(ivar_types:
-                                                   {
-                                                     "@y": AST::Types::Name.new_instance(name: "::String")
-                                                   },
-                                                 self_type: parse_type("self")) do |_, _, _|
+        type_env = original_env.with_annotations(
+          ivar_types: {
+            "@y": AST::Types::Name.new_instance(name: "::String")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_, _, _|
           raise
         end
 
@@ -267,11 +320,14 @@ def test_with_annotation_gvar
       original_env.set(gvar: :"$x", type: union_type)
 
       yield_self do
-        type_env = original_env.with_annotations(gvar_types:
-                                                   {
-                                                     "$x": AST::Types::Name.new_instance(name: "::String")
-                                                   },
-                                                 self_type: parse_type("self")) do |_, _|
+        type_env = original_env.with_annotations(
+          gvar_types: {
+            "$x": AST::Types::Name.new_instance(name: "::String")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_, _|
           raise
         end
 
@@ -279,11 +335,14 @@ def test_with_annotation_gvar
       end
 
       yield_self do
-        type_env = original_env.with_annotations(gvar_types:
-                                                   {
-                                                     "$x": AST::Types::Name.new_instance(name: "::Regexp")
-                                                   },
-                                                 self_type: parse_type("self")) do |name, relation, error|
+        type_env = original_env.with_annotations(
+          gvar_types: {
+            "$x": AST::Types::Name.new_instance(name: "::Regexp")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |name, relation, error|
           assert_equal name, :"$x"
           assert_instance_of Subtyping::Result::Failure, error
         end
@@ -292,11 +351,14 @@ def test_with_annotation_gvar
       end
 
       yield_self do
-        type_env = original_env.with_annotations(gvar_types:
-                                                   {
-                                                     "$y": AST::Types::Name.new_instance(name: "::String")
-                                                   },
-                                                 self_type: parse_type("self")) do |_, _|
+        type_env = original_env.with_annotations(
+          gvar_types: {
+            "$y": AST::Types::Name.new_instance(name: "::String")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_, _|
           raise
         end
 
@@ -318,11 +380,14 @@ def test_with_annotation_const
       original_env.set(const: TypeName("FOO"), type: union_type)
 
       yield_self do
-        type_env = original_env.with_annotations(const_types:
-                                                   {
-                                                     TypeName("FOO") => AST::Types::Name.new_instance(name: "::String")
-                                                   },
-                                                 self_type: parse_type("self")) do |_, _|
+        type_env = original_env.with_annotations(
+          const_types: {
+            TypeName("FOO") => AST::Types::Name.new_instance(name: "::String")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_, _|
           raise
         end
 
@@ -331,11 +396,14 @@ def test_with_annotation_const
       end
 
       yield_self do
-        type_env = original_env.with_annotations(const_types:
-                                                   {
-                                                     TypeName("FOO") => AST::Types::Name.new_instance(name: "::Regexp")
-                                                   },
-                                                 self_type: parse_type("self")) do |name, relation, error|
+        type_env = original_env.with_annotations(
+          const_types: {
+            TypeName("FOO") => AST::Types::Name.new_instance(name: "::Regexp")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |name, relation, error|
           assert_equal name, TypeName("FOO")
           assert_instance_of Subtyping::Result::Failure, error
         end
@@ -345,11 +413,14 @@ def test_with_annotation_const
       end
 
       yield_self do
-        type_env = original_env.with_annotations(const_types:
-                                                   {
-                                                     TypeName("String") => AST::Types::Name.new_instance(name: "::Regexp")
-                                                   },
-                                                 self_type: parse_type("self")) do |name, relation, error|
+        type_env = original_env.with_annotations(
+          const_types: {
+            TypeName("String") => AST::Types::Name.new_instance(name: "::Regexp")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |name, relation, error|
           assert_equal name, TypeName("String")
           assert_instance_of Subtyping::Result::Failure, error
         end
@@ -359,11 +430,14 @@ def test_with_annotation_const
       end
 
       yield_self do
-        type_env = original_env.with_annotations(const_types:
-                                                   {
-                                                     TypeName("BAR") => AST::Types::Name.new_instance(name: "::String")
-                                                   },
-                                                 self_type: parse_type("self")) do |_, _, _|
+        type_env = original_env.with_annotations(
+          const_types: {
+            TypeName("BAR") => AST::Types::Name.new_instance(name: "::String")
+          },
+          self_type: parse_type("self"),
+          instance_type: parse_type("instance"),
+          class_type: parse_type("class")
+        ) do |_, _, _|
           raise
         end