Doc work for hir-analysis::ty module

Author: Y-Nak

crates/hir-analysis/src/lib.rs

@@ -32,11 +32,11 @@ pub struct Jar(
     ty::def_analysis::analyze_trait,
     ty::def_analysis::analyze_impl_trait,
     /// Trait system.
-    ty::trait_::TraitDef,
-    ty::trait_::TraitInstId,
-    ty::trait_::Implementor,
-    ty::trait_::ingot_trait_env,
-    ty::trait_::trait_implementors,
+    ty::trait_def::TraitDef,
+    ty::trait_def::TraitInstId,
+    ty::trait_def::Implementor,
+    ty::trait_def::ingot_trait_env,
+    ty::trait_def::trait_implementors,
     ty::constraint::collect_super_traits,
     ty::constraint::collect_trait_constraints,
     ty::constraint::collect_adt_constraints,
@@ -48,7 +48,7 @@ pub struct Jar(
     ty::constraint::PredicateId,
     ty::constraint::PredicateListId,
     ty::constraint_solver::is_goal_satisfiable,
-    ty::constraint_solver::check_ty_sat,
+    ty::constraint_solver::check_ty_app_sat,
     ty::constraint_solver::check_trait_inst_sat,
     /// Diagnostic accumulators.
     ty::diagnostics::AdtDefDiagAccumulator,

crates/hir-analysis/src/ty/constraint.rs

@@ -1,3 +1,6 @@
+//! This module contains the implementation of the constraint collection
+//! algorithms.
+
 use std::collections::BTreeSet;
 
 use hir::hir_def::{scope_graph::ScopeId, GenericParam, GenericParamOwner, IngotId, TypeBound};
@@ -11,12 +14,24 @@ use crate::{
 
 use super::{
     constraint_solver::{is_goal_satisfiable, GoalSatisfiability},
-    trait_::{Implementor, TraitDef, TraitInstId},
+    trait_def::{Implementor, TraitDef, TraitInstId},
     trait_lower::lower_trait_ref,
     ty_def::{AdtDef, Subst, TyConcrete, TyData, TyId},
     ty_lower::{collect_generic_params, lower_hir_ty, GenericParamOwnerId},
 };
 
+/// Returns a constraints list which is derived from the given type.
+/// # Returns
+///
+/// ##  The first `AssumptionListId`
+/// This is a list of assumptions that should be merged to the context where the
+/// constraints are solved.
+/// This new assumptions are obtained when the given type is a partial applied
+/// type, i.e., the assumptions describes the free type variables.
+///
+/// ## The second `ConstraintListId`
+/// This is a list of constraints that should be solved to ensure the type is
+/// valid.
 #[salsa::tracked]
 pub(crate) fn ty_constraints(
     db: &dyn HirAnalysisDb,
@@ -102,6 +117,7 @@ pub(crate) fn trait_inst_constraints(
     )
 }
 
+/// Collect super traits of the given trait.
 #[salsa::tracked(return_ref, recovery_fn = recover_collect_super_traits)]
 pub(crate) fn collect_super_traits(
     db: &dyn HirAnalysisDb,
@@ -141,6 +157,9 @@ pub(crate) fn super_trait_insts(
         .collect()
 }
 
+/// Collect trait constraints that are specified by the given trait definition.
+/// This constraints describes 1. the constraints about self type(i.e.,
+/// implementor type), and 2. the generic parameter constraints.
 #[salsa::tracked]
 pub(crate) fn collect_trait_constraints(
     db: &dyn HirAnalysisDb,
@@ -152,6 +171,7 @@ pub(crate) fn collect_trait_constraints(
     collector.collect()
 }
 
+/// Collect constraints that are specified by the given ADT definition.
 #[salsa::tracked]
 pub(crate) fn collect_adt_constraints(db: &dyn HirAnalysisDb, adt: AdtDef) -> ConstraintListId {
     let Some(owner) = adt.as_generic_param_owner(db) else {
@@ -162,6 +182,8 @@ pub(crate) fn collect_adt_constraints(db: &dyn HirAnalysisDb, adt: AdtDef) -> Co
     collector.collect()
 }
 
+/// Collect constraints that are specified by the given implementor(i.e., impl
+/// trait).
 #[salsa::tracked]
 pub(crate) fn collect_implementor_constraints(
     db: &dyn HirAnalysisDb,
@@ -173,7 +195,7 @@ pub(crate) fn collect_implementor_constraints(
     collector.collect()
 }
 
-/// Returns a list of assumptions obtained by the given assumptions by looking
+/// Returns a list of assumptions derived from the given assumptions by looking
 /// up super traits.
 #[salsa::tracked(return_ref)]
 pub(crate) fn compute_super_assumptions(
@@ -195,20 +217,23 @@ pub(crate) fn compute_super_assumptions(
     AssumptionListId::new(db, super_assumptions, ingot)
 }
 
+/// Describes a predicate indicating `ty` implements `trait_`.
 #[salsa::interned]
 pub struct PredicateId {
     pub(super) ty: TyId,
     pub(super) trait_inst: TraitInstId,
 }
 
 impl PredicateId {
+    /// Applies the given substitution to the predicate.
     pub fn apply_subst<S: Subst>(self, db: &dyn HirAnalysisDb, subst: &mut S) -> Self {
         let ty = self.ty(db).apply_subst(db, subst);
         let trait_ = self.trait_inst(db).apply_subst(db, subst);
         Self::new(db, ty, trait_)
     }
 }
 
+/// The list of predicates.
 #[salsa::interned]
 pub(crate) struct PredicateListId {
     #[return_ref]

crates/hir-analysis/src/ty/constraint_solver.rs

@@ -1,16 +1,26 @@
+//! This module implements a constraint(trait bound) satisfiability solver.
+//! The algorithm is based on the paper [Typing Haskell in Haskell](https://web.cecs.pdx.edu/~mpj/thih/),
+//! but the algorithm here is slightly extended to support multi parametrized
+//! traits.
+
 use crate::{ty::constraint::ty_constraints, HirAnalysisDb};
 
 use super::{
     constraint::{compute_super_assumptions, AssumptionListId, PredicateId, PredicateListId},
-    trait_::{TraitEnv, TraitInstId},
+    trait_def::{TraitEnv, TraitInstId},
     ty_def::{Subst, TyId},
     unify::UnificationTable,
 };
 
 type Goal = PredicateId;
 
+/// Checks if the arguments of the given type applications satisfies the
+/// constraints under the given assumptions.
+///
+/// # Panics
+/// This function panics if the given type contains free inference keys.
 #[salsa::tracked]
-pub(crate) fn check_ty_sat(
+pub(crate) fn check_ty_app_sat(
     db: &dyn HirAnalysisDb,
     ty: TyId,
     assumptions: AssumptionListId,
@@ -20,7 +30,7 @@ pub(crate) fn check_ty_sat(
     let (_, args) = ty.decompose_ty_app(db);
 
     for arg in args {
-        match check_ty_sat(db, arg, assumptions) {
+        match check_ty_app_sat(db, arg, assumptions) {
             GoalSatisfiability::Satisfied => {}
             err => return err,
         }
@@ -39,6 +49,8 @@ pub(crate) fn check_ty_sat(
     GoalSatisfiability::Satisfied
 }
 
+/// Checks if the given argument of the given trait instantiation satisfies the
+/// constraints under the given assumptions.
 #[salsa::tracked]
 pub(crate) fn check_trait_inst_sat(
     db: &dyn HirAnalysisDb,
@@ -97,7 +109,7 @@ struct ConstraintSolver<'db> {
 
 impl<'db> ConstraintSolver<'db> {
     fn new(db: &'db dyn HirAnalysisDb, goal: Goal, assumptions: AssumptionListId) -> Self {
-        let ingot = goal.trait_inst(db).ingot(db);
+        let ingot = assumptions.ingot(db);
         let env = TraitEnv::new(db, ingot);
 
         Self {
@@ -108,6 +120,8 @@ impl<'db> ConstraintSolver<'db> {
         }
     }
 
+    /// The main entry point of the constraint solver, whici performs actual
+    /// solving.
     fn solve(self) -> GoalSatisfiability {
         let goal_ty = self.goal.ty(self.db);
         let goal_trait = self.goal.trait_inst(self.db);
@@ -141,7 +155,7 @@ impl<'db> ConstraintSolver<'db> {
                 if table.unify(gen_impl.ty(self.db), goal_ty)
                     && table.unify(gen_impl.trait_(self.db), goal_trait)
                 {
-                    let mut subst = ChainedSubst::chain(&mut gen_param_map, &mut table);
+                    let mut subst = SubstComposition::compose(&mut gen_param_map, &mut table);
                     let constraints = impl_.constraints(self.db);
                     Some(constraints.apply_subst(self.db, &mut subst))
                 } else {
@@ -152,6 +166,7 @@ impl<'db> ConstraintSolver<'db> {
             return GoalSatisfiability::NotSatisfied(self.goal);
         };
 
+        // Checks if the all subgoals are satisfied.
         for &sub_goal in sub_goals.predicates(self.db) {
             match is_goal_satisfiable(self.db, sub_goal, self.assumptions) {
                 GoalSatisfiability::Satisfied => {}
@@ -175,18 +190,20 @@ impl PredicateListId {
     }
 }
 
-struct ChainedSubst<'a, 'b, S1, S2> {
+/// A substitution that composes multiple substitutions.
+struct SubstComposition<'a, 'b, S1, S2> {
     first: &'a mut S1,
     second: &'b mut S2,
 }
 
-impl<'a, 'b, S1, S2> ChainedSubst<'a, 'b, S1, S2> {
-    fn chain(first: &'a mut S1, second: &'b mut S2) -> Self {
+impl<'a, 'b, S1, S2> SubstComposition<'a, 'b, S1, S2> {
+    /// Creates a new `SubstComposition` from two substitutions.
+    fn compose(first: &'a mut S1, second: &'b mut S2) -> Self {
         Self { first, second }
     }
 }
 
-impl<'a, 'b, S1, S2> Subst for ChainedSubst<'a, 'b, S1, S2>
+impl<'a, 'b, S1, S2> Subst for SubstComposition<'a, 'b, S1, S2>
 where
     S1: Subst,
     S2: Subst,

crates/hir-analysis/src/ty/def_analysis.rs

@@ -1,3 +1,7 @@
+//! This module contains analysis for the definition of the type/trait.
+//! This module is the only module in `ty` module which is allowed to emit
+//! diagnostics.
+
 use hir::{
     hir_def::{
         scope_graph::ScopeId, FieldDef, ImplTrait, Trait, TraitRefId, TypeAlias, TypeId as HirTyId,
@@ -25,13 +29,23 @@ use super::{
     constraint::{collect_super_traits, AssumptionListId, SuperTraitCycle},
     constraint_solver::{is_goal_satisfiable, GoalSatisfiability},
     diagnostics::{TraitConstraintDiag, TraitLowerDiag, TyDiagCollection, TyLowerDiag},
-    trait_::{ingot_trait_env, Implementor, TraitDef},
+    trait_def::{ingot_trait_env, Implementor, TraitDef},
     trait_lower::{lower_trait, lower_trait_ref, TraitRefLowerError},
     ty_def::{AdtDef, AdtRefId, TyId},
     ty_lower::{lower_adt, lower_hir_ty, lower_kind},
     visitor::{walk_ty, TyVisitor},
 };
 
+/// This function implements analysis for the ADT definition.
+/// The analysis includes the following:
+/// - Check if the types in the ADT is well-formed.
+/// - Check if the trait instantiation appears in the ADT is well-formed.
+/// - Check if the field types are fully applied(i.e., these types should have
+///   `*` kind).
+/// - Check if the types in the ADT satisfies the constraints which is required
+///   in type application.
+/// - Check if the trait instantiations in the ADT satisfies the constraints.
+/// - Check if the recursive types has indirect type wrapper like pointer.
 #[salsa::tracked]
 pub fn analyze_adt(db: &dyn HirAnalysisDb, adt_ref: AdtRefId) {
     let analyzer = DefAnalyzer::for_adt(db, adt_ref);
@@ -46,6 +60,13 @@ pub fn analyze_adt(db: &dyn HirAnalysisDb, adt_ref: AdtRefId) {
     }
 }
 
+/// This function implements analysis for the trait definition.
+/// The analysis includes the following:
+/// - Check if the types appear in the trait is well-formed.
+/// - Check if the trait instantiation appears in the trait is well-formed.
+/// - Check if the types in the trait satisfy the constraints which is required
+///   in type application.
+/// - Check if the trait instantiations in the trait satisfies the constraints.
 #[salsa::tracked]
 pub fn analyze_trait(db: &dyn HirAnalysisDb, trait_: Trait) {
     let analyzer = DefAnalyzer::for_trait(db, trait_);
@@ -56,6 +77,17 @@ pub fn analyze_trait(db: &dyn HirAnalysisDb, trait_: Trait) {
     }
 }
 
+/// This function implements analysis for the trait implementation definition.
+/// The analysis include the following:
+/// - Check if the types appear in the trait impl is well-formed.
+/// - Check if the trait instantiation appears in the trait impl is well-formed.
+/// - Check if the types in the trait impl satisfy the constraints which is
+///   required in type application.
+/// - Check if the trait instantiations in the trait impl satisfies the
+///   constraints.
+/// - Check if the conflict doesn't occur.
+/// - Check if the trait or type is included in the ingot which contains the
+///   impl trait.
 #[salsa::tracked]
 pub fn analyze_impl_trait(db: &dyn HirAnalysisDb, impl_trait: ImplTrait) {
     let implementor = match analyze_trait_impl_specific_error(db, impl_trait) {
@@ -76,6 +108,15 @@ pub fn analyze_impl_trait(db: &dyn HirAnalysisDb, impl_trait: ImplTrait) {
     }
 }
 
+/// This function implements analysis for the type alias definition.
+/// The analysis includes the following:
+/// - Check if the type alias is not recursive.
+/// - Check if the type in the type alias is well-formed.
+///
+/// NOTE: This function doesn't check the satisfiability of the type since our
+/// type system treats the alias as kind of macro, meaning type alias doesn't
+/// included in the type system. Satisfiability is checked where the type alias
+/// is used.
 #[salsa::tracked]
 pub fn analyze_type_alias(db: &dyn HirAnalysisDb, alias: TypeAlias) {
     let Some(hir_ty) = alias.ty(db.as_hir_db()).to_opt() else {
@@ -360,6 +401,10 @@ impl<'db> Visitor for DefAnalyzer<'db> {
         self.current_ty = Some((self.def.trait_self_param(self.db), name_span));
         walk_super_trait_list(self, ctxt, super_traits);
     }
+
+    fn visit_func(&mut self, _ctxt: &mut VisitorCtxt<'_, LazyFuncSpan>, _func: hir::hir_def::Func) {
+        // TODO:
+    }
 }
 
 #[salsa::tracked(recovery_fn = check_recursive_adt_impl)]
@@ -502,7 +547,7 @@ impl DefKind {
     }
 }
 
-/// This function analyzes
+/// This function analyzes the trait impl specific error.
 /// 1. If the trait ref is well-formed except for the satisfiability.
 /// 2. If implementor type is well-formed except for the satisfiability.
 /// 3. If the ingot contains impl trait is the same as the ingot which contains

crates/hir-analysis/src/ty/mod.rs

@@ -13,7 +13,7 @@ use self::{
 pub mod constraint_solver;
 pub mod def_analysis;
 pub mod diagnostics;
-pub mod trait_;
+pub mod trait_def;
 pub mod trait_lower;
 pub mod ty_def;
 pub mod ty_lower;
@@ -23,6 +23,7 @@ pub(crate) mod constraint;
 
 mod unify;
 
+/// An analysis pass for type definitions.
 pub struct TypeDefAnalysisPass<'db> {
     db: &'db dyn HirAnalysisDb,
 }
@@ -64,6 +65,7 @@ impl<'db> ModuleAnalysisPass for TypeDefAnalysisPass<'db> {
     }
 }
 
+/// An analysis pass for trait definitions.
 pub struct TraitAnalysisPass<'db> {
     db: &'db dyn HirAnalysisDb,
 }
@@ -89,6 +91,7 @@ impl<'db> ModuleAnalysisPass for TraitAnalysisPass<'db> {
     }
 }
 
+/// An analysis pass for `ImplTrait'.
 pub struct ImplTraitAnalysisPass<'db> {
     db: &'db dyn HirAnalysisDb,
 }
@@ -115,6 +118,7 @@ impl<'db> ModuleAnalysisPass for ImplTraitAnalysisPass<'db> {
     }
 }
 
+/// An analysis pass for type aliases.
 pub struct TypeAliasAnalysisPass<'db> {
     db: &'db dyn HirAnalysisDb,
 }