diff --git a/crates/tinymist-query/src/analysis.rs b/crates/tinymist-query/src/analysis.rs
index c20c17d9..694d0a52 100644
--- a/crates/tinymist-query/src/analysis.rs
+++ b/crates/tinymist-query/src/analysis.rs
@@ -34,7 +34,7 @@ mod type_check_tests {
     use crate::analysis::ty;
     use crate::tests::*;
 
-    use super::{Ty, TypeCheckInfo};
+    use super::{Ty, TypeScheme};
 
     #[test]
     fn test() {
@@ -51,7 +51,7 @@ mod type_check_tests {
         });
     }
 
-    struct TypeCheckSnapshot<'a>(&'a Source, &'a TypeCheckInfo);
+    struct TypeCheckSnapshot<'a>(&'a Source, &'a TypeScheme);
 
     impl fmt::Debug for TypeCheckSnapshot<'_> {
         fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
diff --git a/crates/tinymist-query/src/analysis/global.rs b/crates/tinymist-query/src/analysis/global.rs
index 20107e7a..cc521793 100644
--- a/crates/tinymist-query/src/analysis/global.rs
+++ b/crates/tinymist-query/src/analysis/global.rs
@@ -26,7 +26,7 @@ use typst::{layout::Position, syntax::FileId as TypstFileId};
 
 use super::{
     analyze_bib, post_type_check, BibInfo, DefUseInfo, DefinitionLink, IdentRef, ImportInfo,
-    PathPreference, SigTy, Signature, SignatureTarget, Ty, TypeCheckInfo,
+    PathPreference, SigTy, Signature, SignatureTarget, Ty, TypeScheme,
 };
 use crate::adt::interner::Interned;
 use crate::analysis::analyze_dyn_signature;
@@ -49,7 +49,7 @@ pub struct ModuleAnalysisCache {
     source: OnceCell<FileResult<Source>>,
     import_info: OnceCell<Option<Arc<ImportInfo>>>,
     def_use: OnceCell<Option<Arc<DefUseInfo>>>,
-    type_check: OnceCell<Option<Arc<TypeCheckInfo>>>,
+    type_check: OnceCell<Option<Arc<TypeScheme>>>,
     bibliography: OnceCell<Option<Arc<BibInfo>>>,
 }
 
@@ -93,15 +93,15 @@ impl ModuleAnalysisCache {
     }
 
     /// Try to get the type check information of a file.
-    pub(crate) fn type_check(&self) -> Option<Arc<TypeCheckInfo>> {
+    pub(crate) fn type_check(&self) -> Option<Arc<TypeScheme>> {
         self.type_check.get().cloned().flatten()
     }
 
     /// Compute the type check information of a file.
     pub(crate) fn compute_type_check(
         &self,
-        f: impl FnOnce() -> Option<Arc<TypeCheckInfo>>,
-    ) -> Option<Arc<TypeCheckInfo>> {
+        f: impl FnOnce() -> Option<Arc<TypeScheme>>,
+    ) -> Option<Arc<TypeScheme>> {
         self.type_check.get_or_init(f).clone()
     }
 
@@ -308,7 +308,7 @@ impl<Inputs, Output> ComputingNode<Inputs, Output> {
 #[allow(clippy::type_complexity)]
 pub struct ModuleAnalysisGlobalCache {
     def_use_lexical_hierarchy: ComputingNode<Source, EcoVec<LexicalHierarchy>>,
-    type_check: Arc<ComputingNode<Source, Arc<TypeCheckInfo>>>,
+    type_check: Arc<ComputingNode<Source, Arc<TypeScheme>>>,
     def_use: Arc<ComputingNode<(EcoVec<LexicalHierarchy>, Arc<ImportInfo>), Arc<DefUseInfo>>>,
 
     bibliography: Arc<ComputingNode<EcoVec<(TypstFileId, Bytes)>, Arc<BibInfo>>>,
@@ -670,7 +670,7 @@ impl<'w> AnalysisContext<'w> {
     }
 
     /// Get the type check information of a source file.
-    pub(crate) fn type_check(&mut self, source: Source) -> Option<Arc<TypeCheckInfo>> {
+    pub(crate) fn type_check(&mut self, source: Source) -> Option<Arc<TypeScheme>> {
         let fid = source.id();
 
         if let Some(res) = self.caches.modules.entry(fid).or_default().type_check() {
diff --git a/crates/tinymist-query/src/analysis/ty.rs b/crates/tinymist-query/src/analysis/ty.rs
index 386ed247..67297d23 100644
--- a/crates/tinymist-query/src/analysis/ty.rs
+++ b/crates/tinymist-query/src/analysis/ty.rs
@@ -13,7 +13,7 @@ use typst::{
 };
 
 use crate::analysis::{Ty, *};
-use crate::{analysis::TypeCheckInfo, ty::TypeInterace, AnalysisContext};
+use crate::{analysis::TypeScheme, ty::TypeInterface, AnalysisContext};
 
 use super::{
     resolve_global_value, BuiltinTy, DefUseInfo, FlowVarKind, IdentRef, TypeBounds, TypeVar,
@@ -28,8 +28,8 @@ pub(crate) use apply::*;
 pub(crate) use post_check::*;
 
 /// Type checking at the source unit level.
-pub(crate) fn type_check(ctx: &mut AnalysisContext, source: Source) -> Option<Arc<TypeCheckInfo>> {
-    let mut info = TypeCheckInfo::default();
+pub(crate) fn type_check(ctx: &mut AnalysisContext, source: Source) -> Option<Arc<TypeScheme>> {
+    let mut info = TypeScheme::default();
 
     // Retrieve def-use information for the source.
     let def_use_info = ctx.def_use(source.clone())?;
@@ -64,7 +64,7 @@ struct TypeChecker<'a, 'w> {
     source: Source,
     def_use_info: Arc<DefUseInfo>,
 
-    info: &'a mut TypeCheckInfo,
+    info: &'a mut TypeScheme,
     externals: HashMap<DefId, Option<Ty>>,
     mode: InterpretMode,
 }
@@ -98,7 +98,6 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
                     TypeVar {
                         name: r.name.as_str().into(),
                         def: def_id,
-                        syntax: None,
                     },
                     init_expr,
                 ),
@@ -106,7 +105,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
         }
 
         let var = self.info.vars.get_mut(&def_id).unwrap();
-        TypeCheckInfo::witness_(s, var.as_type(), &mut self.info.mapping);
+        TypeScheme::witness_(s, var.as_type(), &mut self.info.mapping);
         Some(var.as_type())
     }
 
@@ -250,7 +249,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
                 }
             }
             (Ty::Dict(lhs), Ty::Dict(rhs)) => {
-                for (key, lhs, rhs) in lhs.intersect_keys(rhs) {
+                for (key, lhs, rhs) in lhs.common_iface_fields(rhs) {
                     log::debug!("constrain record item {key} {lhs:?} ⪯ {rhs:?}");
                     self.constrain(lhs, rhs);
                     // if !sl.is_detached() {
@@ -280,7 +279,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
             }
             (Ty::Value(lhs), rhs) => {
                 log::debug!("constrain value {lhs:?} ⪯ {rhs:?}");
-                let _ = TypeCheckInfo::witness_at_most;
+                let _ = TypeScheme::witness_at_most;
                 // if !lhs.1.is_detached() {
                 //     self.info.witness_at_most(lhs.1, rhs.clone());
                 // }
@@ -402,7 +401,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
                 self.weaken(&v.lhs);
             }
             Ty::Binary(v) => {
-                let (lhs, rhs) = v.repr();
+                let [lhs, rhs] = v.operands();
                 self.weaken(lhs);
                 self.weaken(rhs);
             }
diff --git a/crates/tinymist-query/src/analysis/ty/apply.rs b/crates/tinymist-query/src/analysis/ty/apply.rs
index 8d076c75..37457351 100644
--- a/crates/tinymist-query/src/analysis/ty/apply.rs
+++ b/crates/tinymist-query/src/analysis/ty/apply.rs
@@ -29,7 +29,7 @@ impl<'a, 'b, 'w> ApplyChecker for ApplyTypeChecker<'a, 'b, 'w> {
             .map(|v| v.bounds.bounds().read().clone())
     }
 
-    fn call(&mut self, sig: Sig, args: &Interned<ArgsTy>, pol: bool) {
+    fn apply(&mut self, sig: Sig, args: &Interned<ArgsTy>, pol: bool) {
         let _ = self.args;
 
         let (sig, is_partialize) = match sig {
diff --git a/crates/tinymist-query/src/analysis/ty/post_check.rs b/crates/tinymist-query/src/analysis/ty/post_check.rs
index a25b3cd5..7203692a 100644
--- a/crates/tinymist-query/src/analysis/ty/post_check.rs
+++ b/crates/tinymist-query/src/analysis/ty/post_check.rs
@@ -15,13 +15,13 @@ use crate::{
     AnalysisContext,
 };
 
-use super::{FieldTy, SigShape, Ty, TypeCheckInfo};
+use super::{FieldTy, SigShape, Ty, TypeScheme};
 
 /// With given type information, check the type of a literal expression again by
 /// touching the possible related nodes.
 pub(crate) fn post_type_check(
     _ctx: &mut AnalysisContext,
-    info: &TypeCheckInfo,
+    info: &TypeScheme,
     node: LinkedNode,
 ) -> Option<Ty> {
     let mut worker = PostTypeCheckWorker {
@@ -108,7 +108,7 @@ fn check_signature<'a>(
 struct PostTypeCheckWorker<'a, 'w> {
     ctx: &'a mut AnalysisContext<'w>,
     checked: HashMap<Span, Option<Ty>>,
-    info: &'a TypeCheckInfo,
+    info: &'a TypeScheme,
 }
 
 impl<'a, 'w> PostTypeCheckWorker<'a, 'w> {
diff --git a/crates/tinymist-query/src/signature_help.rs b/crates/tinymist-query/src/signature_help.rs
index 566823ce..20ebee9c 100644
--- a/crates/tinymist-query/src/signature_help.rs
+++ b/crates/tinymist-query/src/signature_help.rs
@@ -143,7 +143,7 @@ impl SemanticRequest for SignatureHelpRequest {
         label.push(')');
         let ret = type_sig
             .as_ref()
-            .and_then(|sig| sig.ret.as_ref())
+            .and_then(|sig| sig.body.as_ref())
             .or_else(|| sig.primary().ret_ty.as_ref());
         if let Some(ret_ty) = ret {
             label.push_str(" -> ");
diff --git a/crates/tinymist-query/src/ty/apply.rs b/crates/tinymist-query/src/ty/apply.rs
index ec7db1c1..62f8248c 100644
--- a/crates/tinymist-query/src/ty/apply.rs
+++ b/crates/tinymist-query/src/ty/apply.rs
@@ -5,7 +5,7 @@ use crate::{adt::interner::Interned, ty::def::*};
 use super::{Sig, SigChecker, SigSurfaceKind};
 
 pub trait ApplyChecker {
-    fn call(&mut self, sig: Sig, arguments: &Interned<ArgsTy>, pol: bool);
+    fn apply(&mut self, sig: Sig, arguments: &Interned<ArgsTy>, pol: bool);
 
     fn bound_of_var(&mut self, _var: &Interned<TypeVar>, _pol: bool) -> Option<TypeBounds> {
         None
@@ -13,11 +13,12 @@ pub trait ApplyChecker {
 }
 
 impl Ty {
+    /// Call the given type with the given arguments.
     pub fn call(&self, args: &Interned<ArgsTy>, pol: bool, checker: &mut impl ApplyChecker) {
         self.apply(SigSurfaceKind::Call, args, pol, checker)
     }
 
-    #[allow(dead_code)]
+    /// Get the element type of the given type.
     pub fn element_of(&self, pol: bool, checker: &mut impl ApplyChecker) {
         static EMPTY_ARGS: Lazy<Interned<ArgsTy>> = Lazy::new(|| ArgsTy::default().into());
 
@@ -46,18 +47,17 @@ impl<'a, T: ApplyChecker> ApplySigChecker<'a, T> {
 
 impl<'a, T: ApplyChecker> SigChecker for ApplySigChecker<'a, T> {
     fn check(&mut self, cano_sig: Sig, ctx: &mut super::SigCheckContext, pol: bool) -> Option<()> {
-        let args = &ctx.args;
-        let partial_sig = if args.is_empty() {
+        // Bind the arguments to the canonical signature.
+        let partial_sig = if ctx.args.is_empty() {
             cano_sig
         } else {
             Sig::With {
                 sig: &cano_sig,
-                withs: args,
+                withs: &ctx.args,
                 at: &ctx.at,
             }
         };
-
-        self.0.call(partial_sig, self.1, pol);
+        self.0.apply(partial_sig, self.1, pol);
         Some(())
     }
 
diff --git a/crates/tinymist-query/src/ty/bound.rs b/crates/tinymist-query/src/ty/bound.rs
index 2f3a1df0..0ef48ba2 100644
--- a/crates/tinymist-query/src/ty/bound.rs
+++ b/crates/tinymist-query/src/ty/bound.rs
@@ -17,10 +17,12 @@ where
 }
 
 impl Ty {
+    /// Check if the given type has bounds (is combinated).
     pub fn has_bounds(&self) -> bool {
         matches!(self, Ty::Union(_) | Ty::Let(_) | Ty::Var(_))
     }
 
+    /// Profile the bounds of the given type.
     pub fn bounds(&self, pol: bool, checker: &mut impl BoundChecker) {
         let mut worker = BoundCheckContext;
         worker.ty(self, pol, checker);
diff --git a/crates/tinymist-query/src/ty/builtin.rs b/crates/tinymist-query/src/ty/builtin.rs
index cccbb236..0fa5a672 100644
--- a/crates/tinymist-query/src/ty/builtin.rs
+++ b/crates/tinymist-query/src/ty/builtin.rs
@@ -11,7 +11,7 @@ use typst::{
 use crate::{adt::interner::Interned, ty::*};
 
 #[derive(Debug, Clone, Hash, PartialEq, Eq)]
-pub(crate) enum PathPreference {
+pub enum PathPreference {
     None,
     Special,
     Source,
@@ -84,7 +84,7 @@ impl PathPreference {
 }
 
 impl Ty {
-    pub fn from_return_site(f: &Func, c: &'_ CastInfo) -> Option<Self> {
+    pub(crate) fn from_return_site(f: &Func, c: &'_ CastInfo) -> Option<Self> {
         use typst::foundations::func::Repr;
         match f.inner() {
             Repr::Element(e) => return Some(Ty::Builtin(BuiltinTy::Element(*e))),
@@ -95,7 +95,7 @@ impl Ty {
 
         let ty = match c {
             CastInfo::Any => Ty::Any,
-            CastInfo::Value(v, doc) => Ty::Value(InsTy::new_doc(v.clone(), doc)),
+            CastInfo::Value(v, doc) => Ty::Value(InsTy::new_doc(v.clone(), *doc)),
             CastInfo::Type(ty) => Ty::Builtin(BuiltinTy::Type(*ty)),
             CastInfo::Union(e) => {
                 // flat union
@@ -122,7 +122,7 @@ impl Ty {
 
         let ty = match &s {
             CastInfo::Any => Ty::Any,
-            CastInfo::Value(v, doc) => Ty::Value(InsTy::new_doc(v.clone(), doc)),
+            CastInfo::Value(v, doc) => Ty::Value(InsTy::new_doc(v.clone(), *doc)),
             CastInfo::Type(ty) => Ty::Builtin(BuiltinTy::Type(*ty)),
             CastInfo::Union(e) => {
                 // flat union
@@ -159,7 +159,7 @@ impl<'a> Iterator for UnionIter<'a> {
 }
 
 #[derive(Clone, Hash, PartialEq, Eq)]
-pub(crate) enum BuiltinTy {
+pub enum BuiltinTy {
     Clause,
     Undef,
     Content,
diff --git a/crates/tinymist-query/src/ty/def.rs b/crates/tinymist-query/src/ty/def.rs
index 55cd0550..fc2d2f75 100644
--- a/crates/tinymist-query/src/ty/def.rs
+++ b/crates/tinymist-query/src/ty/def.rs
@@ -1,18 +1,21 @@
-#![allow(unused)]
+//! Name Convention:
+//! - `TypeXXX`: abstracted types or clauses
+//! - `XXTy`: concrete types
 
 use core::fmt;
-use ecow::EcoVec;
-use once_cell::sync::OnceCell;
-use parking_lot::{Mutex, RwLock};
-use reflexo::vector::ir::DefId;
 use std::{
     collections::{hash_map::Entry, HashMap, HashSet},
     hash::{Hash, Hasher},
     sync::Arc,
 };
+
+use ecow::EcoVec;
+use once_cell::sync::OnceCell;
+use parking_lot::{Mutex, RwLock};
+use reflexo::vector::ir::DefId;
 use typst::{
     foundations::Value,
-    syntax::{ast, Span, SyntaxNode},
+    syntax::{ast, Span, SyntaxKind, SyntaxNode},
 };
 
 use crate::{
@@ -20,774 +23,61 @@ use crate::{
     analysis::BuiltinTy,
 };
 
-pub type TyRef = Interned<Ty>;
+/// A reference to the interned type
+pub(super) type TyRef = Interned<Ty>;
+/// A reference to the interned string
+pub(super) type StrRef = Interned<str>;
 
-#[derive(Default)]
-pub(crate) struct TypeCheckInfo {
-    pub vars: HashMap<DefId, TypeVarBounds>,
-    pub mapping: HashMap<Span, Vec<Ty>>,
-
-    pub(super) cano_cache: Mutex<TypeCanoStore>,
-}
-
-impl TypeCheckInfo {
-    // todo: distinguish at least, at most
-    pub fn witness_at_least(&mut self, site: Span, ty: Ty) {
-        Self::witness_(site, ty, &mut self.mapping);
-    }
-
-    pub fn witness_at_most(&mut self, site: Span, ty: Ty) {
-        Self::witness_(site, ty, &mut self.mapping);
-    }
-
-    pub(crate) fn witness_(site: Span, ty: Ty, mapping: &mut HashMap<Span, Vec<Ty>>) {
-        if site.is_detached() {
-            return;
-        }
-
-        // todo: intersect/union
-        let site_store = mapping.entry(site);
-        match site_store {
-            Entry::Occupied(e) => {
-                e.into_mut().push(ty);
-            }
-            Entry::Vacant(e) => {
-                e.insert(vec![ty]);
-            }
-        }
-    }
-
-    pub fn type_of_span(&self, site: Span) -> Option<Ty> {
-        self.mapping
-            .get(&site)
-            .cloned()
-            .map(|e| Ty::from_types(e.into_iter()))
-    }
-
-    pub fn type_of_def(&self, def: DefId) -> Option<Ty> {
-        Some(self.simplify(self.vars.get(&def).map(|e| e.as_type())?, false))
-    }
-}
-
-#[derive(Default)]
-pub(super) struct TypeCanoStore {
-    pub cano_cache: HashMap<(Ty, bool), Ty>,
-    pub cano_local_cache: HashMap<(DefId, bool), Ty>,
-    pub negatives: HashSet<DefId>,
-    pub positives: HashSet<DefId>,
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct TypeSource {
-    pub name_node: SyntaxNode,
-    pub name_repr: OnceCell<Interned<str>>,
-    pub span: Span,
-    pub doc: Interned<str>,
-}
-
-impl Hash for TypeSource {
-    fn hash<H: Hasher>(&self, state: &mut H) {
-        self.name_node.hash(state);
-        self.span.hash(state);
-        self.doc.hash(state);
-    }
-}
-
-impl TypeSource {
-    pub fn name(&self) -> Interned<str> {
-        self.name_repr
-            .get_or_init(|| {
-                let name = self.name_node.text();
-                if !name.is_empty() {
-                    return name.into();
-                }
-                let name = self.name_node.clone().into_text();
-                name.into()
-            })
-            .clone()
-    }
-}
-
-pub trait TypeInterace {
-    fn bone(&self) -> &Interned<NameBone>;
-    fn interface(&self) -> impl Iterator<Item = (&Interned<str>, &Ty)>;
-    fn field_by_bone_offset(&self, i: usize) -> Option<&Ty>;
-
-    fn common_iface_fields<'a>(
-        &'a self,
-        rhs: &'a Self,
-    ) -> impl Iterator<Item = (&'a Interned<str>, &'a Ty, &'a Ty)> {
-        let lhs_names = self.bone();
-        let rhs_names = rhs.bone();
-
-        lhs_names
-            .intersect_keys_enumerate(rhs_names)
-            .filter_map(move |(i, j)| {
-                let lhs = self.field_by_bone_offset(i)?;
-                let rhs = rhs.field_by_bone_offset(j)?;
-                Some((&lhs_names.names[i], lhs, rhs))
-            })
-    }
-}
-
-struct RefDebug<'a>(&'a Ty);
-
-impl<'a> fmt::Debug for RefDebug<'a> {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        match self.0 {
-            Ty::Var(v) => write!(f, "@v{:?}", v.name()),
-            _ => write!(f, "{:?}", self.0),
-        }
-    }
-}
-
-#[derive(Debug, Hash, Clone, PartialEq)]
-pub struct InsTy {
-    pub val: Value,
-
-    pub syntax: Option<Interned<TypeSource>>,
-}
-
-// There are some case that val is not Eq, but we make it Eq for simplicity
-impl Eq for InsTy {}
-
-impl InsTy {
-    pub fn new(val: Value) -> Interned<Self> {
-        Self { val, syntax: None }.into()
-    }
-    pub fn new_at(val: Value, s: Span) -> Interned<Self> {
-        Interned::new(Self {
-            val,
-            syntax: Some(Interned::new(TypeSource {
-                name_node: SyntaxNode::default(),
-                name_repr: OnceCell::new(),
-                span: s,
-                doc: "".into(),
-            })),
-        })
-    }
-    pub fn new_doc(val: Value, doc: &str) -> Interned<Self> {
-        Interned::new(Self {
-            val,
-            syntax: Some(Interned::new(TypeSource {
-                name_node: SyntaxNode::default(),
-                name_repr: OnceCell::new(),
-                span: Span::detached(),
-                doc: doc.into(),
-            })),
-        })
-    }
-}
-
-#[derive(Debug, Hash, Clone, PartialEq, Eq)]
-pub struct NameBone {
-    pub names: Vec<Interned<str>>,
-}
-
-impl NameBone {
-    pub fn empty() -> Interned<Self> {
-        Interned::new(Self { names: Vec::new() })
-    }
-}
-
-impl NameBone {
-    fn find(&self, name: &Interned<str>) -> Option<usize> {
-        // binary search
-        self.names.binary_search_by(|probe| probe.cmp(name)).ok()
-    }
-}
-
-impl NameBone {
-    pub(crate) fn intersect_keys_enumerate<'a>(
-        &'a self,
-        rhs: &'a NameBone,
-    ) -> impl Iterator<Item = (usize, usize)> + 'a {
-        let mut lhs_iter = self.names.iter().enumerate();
-        let mut rhs_iter = rhs.names.iter().enumerate();
-
-        let mut lhs = lhs_iter.next();
-        let mut rhs = rhs_iter.next();
-
-        std::iter::from_fn(move || 'key_scanning: loop {
-            if let (Some((i, lhs_key)), Some((j, rhs_key))) = (lhs, rhs) {
-                match lhs_key.cmp(rhs_key) {
-                    std::cmp::Ordering::Less => {
-                        lhs = lhs_iter.next();
-                        continue 'key_scanning;
-                    }
-                    std::cmp::Ordering::Greater => {
-                        rhs = rhs_iter.next();
-                        continue 'key_scanning;
-                    }
-                    std::cmp::Ordering::Equal => {
-                        lhs = lhs_iter.next();
-                        rhs = rhs_iter.next();
-                        return Some((i, j));
-                    }
-                }
-            }
-            return None;
-        })
-    }
-}
-
-#[derive(Debug, Hash, Clone, PartialEq, Eq)]
-pub struct FieldTy {
-    pub name: Interned<str>,
-    pub field: Ty,
-
-    pub syntax: Option<Interned<TypeSource>>,
-}
-impl FieldTy {
-    pub(crate) fn new_untyped(name: Interned<str>) -> Interned<Self> {
-        Interned::new(Self {
-            name,
-            field: Ty::Any,
-            syntax: None,
-        })
-    }
-}
-
-#[derive(Hash, Clone, PartialEq, Eq, Default)]
-pub struct TypeBounds {
-    pub lbs: EcoVec<Ty>,
-    pub ubs: EcoVec<Ty>,
-}
-
-impl fmt::Debug for TypeBounds {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        // write!(f, "{}", self.name)
-        // also where
-        if !self.lbs.is_empty() {
-            write!(f, " ⪰ {:?}", self.lbs[0])?;
-            for lb in &self.lbs[1..] {
-                write!(f, " | {lb:?}")?;
-            }
-        }
-        if !self.ubs.is_empty() {
-            write!(f, " ⪯ {:?}", self.ubs[0])?;
-            for ub in &self.ubs[1..] {
-                write!(f, " & {ub:?}")?;
-            }
-        }
-        Ok(())
-    }
-}
+/// All possible types in tinymist
 #[derive(Hash, Clone, PartialEq, Eq)]
-pub struct TypeVar {
-    pub name: Interned<str>,
-    pub def: DefId,
-
-    pub syntax: Option<Interned<TypeSource>>,
-}
-
-impl Ord for TypeVar {
-    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
-        self.name
-            .cmp(&other.name)
-            .then_with(|| self.def.0.cmp(&other.def.0))
-    }
-}
-
-impl PartialOrd for TypeVar {
-    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        Some(self.cmp(other))
-    }
-}
-
-impl fmt::Debug for TypeVar {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "@{}", self.name)
-    }
-}
-
-#[derive(Clone)]
-pub(crate) enum FlowVarKind {
-    Strong(Arc<RwLock<TypeBounds>>),
-    Weak(Arc<RwLock<TypeBounds>>),
-}
-
-impl FlowVarKind {
-    pub fn bounds(&self) -> &RwLock<TypeBounds> {
-        match self {
-            FlowVarKind::Strong(w) | FlowVarKind::Weak(w) => w,
-        }
-    }
-}
-
-#[derive(Clone)]
-pub struct TypeVarBounds {
-    pub var: Interned<TypeVar>,
-    pub bounds: FlowVarKind,
-}
-
-impl fmt::Debug for TypeVarBounds {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:?}", self.var)
-    }
-}
-
-impl TypeVarBounds {
-    pub fn name(&self) -> Interned<str> {
-        self.var.name.clone()
-    }
-
-    pub fn id(&self) -> DefId {
-        self.var.def
-    }
-
-    pub fn as_type(&self) -> Ty {
-        Ty::Var(self.var.clone())
-    }
-
-    pub(crate) fn new(var: TypeVar, init: TypeBounds) -> Self {
-        Self {
-            var: Interned::new(var),
-            bounds: FlowVarKind::Strong(Arc::new(RwLock::new(init))),
-        }
-    }
-
-    pub(crate) fn weaken(&mut self) {
-        match &self.bounds {
-            FlowVarKind::Strong(w) => {
-                self.bounds = FlowVarKind::Weak(w.clone());
-            }
-            FlowVarKind::Weak(_) => {}
-        }
-    }
-}
-
-impl TypeVar {
-    pub fn new(name: Interned<str>, def: DefId) -> Interned<Self> {
-        Interned::new(Self {
-            name,
-            def,
-            syntax: None,
-        })
-    }
-
-    pub fn name(&self) -> Interned<str> {
-        self.name.clone()
-    }
-
-    pub fn id(&self) -> DefId {
-        self.def
-    }
-}
-
-#[derive(Hash, Clone, PartialEq, Eq)]
-pub struct RecordTy {
-    pub types: Interned<Vec<Ty>>,
-    pub names: Interned<NameBone>,
-    pub syntax: Option<Interned<TypeSource>>,
-}
-
-impl RecordTy {
-    pub(crate) fn shape_fields(mut fields: Vec<(Interned<str>, Ty, Span)>) -> (NameBone, Vec<Ty>) {
-        fields.sort_by(|a, b| a.0.cmp(&b.0));
-        let names = NameBone {
-            names: fields.iter().map(|e| e.0.clone()).collect(),
-        };
-        let types = fields.into_iter().map(|(_, ty, _)| ty).collect::<Vec<_>>();
-
-        (names, types)
-    }
-
-    pub(crate) fn new(fields: Vec<(Interned<str>, Ty, Span)>) -> Interned<Self> {
-        let (names, types) = Self::shape_fields(fields);
-        Interned::new(Self {
-            types: Interned::new(types),
-            names: Interned::new(names),
-            syntax: None,
-        })
-    }
-
-    pub(crate) fn intersect_keys<'a>(
-        &'a self,
-        rhs: &'a RecordTy,
-    ) -> impl Iterator<Item = (&Interned<str>, &Ty, &Ty)> + 'a {
-        self.names
-            .intersect_keys_enumerate(&rhs.names)
-            .filter_map(move |(i, j)| {
-                self.types
-                    .get(i)
-                    .and_then(|lhs| rhs.types.get(j).map(|rhs| (&self.names.names[i], lhs, rhs)))
-            })
-    }
-}
-
-impl TypeInterace for RecordTy {
-    fn bone(&self) -> &Interned<NameBone> {
-        &self.names
-    }
-
-    fn field_by_bone_offset(&self, i: usize) -> Option<&Ty> {
-        self.types.get(i)
-    }
-
-    fn interface(&self) -> impl Iterator<Item = (&Interned<str>, &Ty)> {
-        self.names.names.iter().zip(self.types.iter())
-    }
-}
-
-impl fmt::Debug for RecordTy {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.write_str("{")?;
-        interpersed(
-            f,
-            self.interface().map(|(name, ty)| ParamTy::Named(name, ty)),
-        )?;
-        f.write_str("}")
-    }
-}
-
-enum ParamTy<'a> {
-    Pos(&'a Ty),
-    Named(&'a Interned<str>, &'a Ty),
-    Rest(&'a Ty),
-}
-
-impl fmt::Debug for ParamTy<'_> {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        match self {
-            ParamTy::Pos(ty) => write!(f, "{ty:?}"),
-            ParamTy::Named(name, ty) => write!(f, "{name:?}: {ty:?}"),
-            ParamTy::Rest(ty) => write!(f, "...: {ty:?}[]"),
-        }
-    }
-}
-
-#[derive(Hash, Clone, PartialEq, Eq)]
-pub struct SigTy {
-    pub types: Interned<Vec<Ty>>,
-    pub ret: Option<Ty>,
-    pub names: Interned<NameBone>,
-    pub name_started: u32,
-    pub spread_left: bool,
-    pub spread_right: bool,
-    pub has_free_variables: bool,
-
-    pub syntax: Option<Interned<TypeSource>>,
-}
-
-impl SigTy {
-    /// Array constructor
-    #[comemo::memoize]
-    pub(crate) fn array_cons(elem: Ty, anyify: bool) -> Interned<SigTy> {
-        let ret = if anyify {
-            Ty::Any
-        } else {
-            Ty::Array(Interned::new(elem.clone()))
-        };
-        Interned::new(Self {
-            types: Interned::new(vec![elem]),
-            ret: Some(ret),
-            names: NameBone::empty(),
-            name_started: 0,
-            spread_left: false,
-            spread_right: true,
-            has_free_variables: false,
-            syntax: None,
-        })
-    }
-
-    pub(crate) fn inputs(&self) -> impl Iterator<Item = &Ty> {
-        self.types.iter()
-    }
-
-    /// Dictionary constructor
-    #[comemo::memoize]
-    pub(crate) fn dict_cons(named: &Interned<RecordTy>, anyify: bool) -> Interned<SigTy> {
-        let ret = if anyify {
-            Ty::Any
-        } else {
-            Ty::Dict(named.clone())
-        };
-
-        Interned::new(Self {
-            types: named.types.clone(),
-            ret: Some(ret),
-            names: named.names.clone(),
-            name_started: 0,
-            spread_left: false,
-            spread_right: false,
-            has_free_variables: false,
-            syntax: None,
-        })
-    }
-
-    pub(crate) fn new(
-        pos: impl IntoIterator<Item = Ty>,
-        named: impl IntoIterator<Item = (Interned<str>, Ty)>,
-        rest: Option<Ty>,
-        ret_ty: Option<Ty>,
-    ) -> Self {
-        let named = named
-            .into_iter()
-            .map(|(name, ty)| (name, ty, Span::detached()))
-            .collect::<Vec<_>>();
-        let (names, types) = RecordTy::shape_fields(named);
-        let spread_right = rest.is_some();
-
-        let name_started = if spread_right { 1 } else { 0 } + types.len();
-        let types = pos.into_iter().chain(types).chain(rest).collect::<Vec<_>>();
-
-        let name_started = (types.len() - name_started) as u32;
-
-        Self {
-            types: Interned::new(types),
-            ret: ret_ty,
-            names: Interned::new(names),
-            name_started,
-            spread_left: false,
-            spread_right,
-            // todo: substitute with actual value
-            has_free_variables: false,
-            syntax: None,
-        }
-    }
-}
-
-impl Default for SigTy {
-    fn default() -> Self {
-        Self {
-            types: Interned::new(Vec::new()),
-            ret: None,
-            names: NameBone::empty(),
-            name_started: 0,
-            spread_left: false,
-            spread_right: false,
-            has_free_variables: false,
-            syntax: None,
-        }
-    }
-}
-
-impl TypeInterace for SigTy {
-    fn bone(&self) -> &Interned<NameBone> {
-        &self.names
-    }
-
-    fn interface(&self) -> impl Iterator<Item = (&Interned<str>, &Ty)> {
-        let names = self.names.names.iter();
-        let types = self.types.iter().skip(self.name_started as usize);
-        names.zip(types)
-    }
-
-    fn field_by_bone_offset(&self, i: usize) -> Option<&Ty> {
-        self.types.get(i + self.name_started as usize)
-    }
-}
-
-impl SigTy {
-    pub fn positional_params(&self) -> impl ExactSizeIterator<Item = &Ty> {
-        self.types.iter().take(self.name_started as usize)
-    }
-
-    pub fn named_params(&self) -> impl ExactSizeIterator<Item = (&Interned<str>, &Ty)> {
-        let named_names = self.names.names.iter();
-        let named_types = self.types.iter().skip(self.name_started as usize);
-
-        named_names.zip(named_types)
-    }
-
-    pub fn rest_param(&self) -> Option<&Ty> {
-        if self.spread_right {
-            self.types.last()
-        } else {
-            None
-        }
-    }
-
-    pub fn pos(&self, idx: usize) -> Option<&Ty> {
-        (idx < self.name_started as usize)
-            .then_some(())
-            .and_then(|_| self.types.get(idx))
-    }
-
-    pub fn named(&self, name: &Interned<str>) -> Option<&Ty> {
-        let idx = self.names.find(name)?;
-        self.types.get(idx + self.name_started as usize)
-    }
-
-    pub(crate) fn matches<'a>(
-        &'a self,
-        args: &'a SigTy,
-        withs: Option<&'a Vec<Interned<crate::analysis::SigTy>>>,
-    ) -> impl Iterator<Item = (&'a Ty, &'a Ty)> + 'a {
-        let with_len = withs
-            .map(|w| w.iter().map(|w| w.positional_params().len()).sum::<usize>())
-            .unwrap_or(0);
-
-        let sig_pos = self.positional_params();
-        let arg_pos = args.positional_params();
-
-        let sig_rest = self.rest_param();
-        let arg_rest = args.rest_param();
-
-        let max_len = sig_pos.len().max(with_len + arg_pos.len())
-            + if sig_rest.is_some() && arg_rest.is_some() {
-                1
-            } else {
-                0
-            };
-
-        let arg_pos = withs
-            .into_iter()
-            .flat_map(|w| w.iter().rev().map(|w| w.positional_params()))
-            .flatten()
-            .chain(arg_pos);
-
-        let sig_stream = sig_pos.chain(sig_rest.into_iter().cycle()).take(max_len);
-        let arg_stream = arg_pos.chain(arg_rest.into_iter().cycle()).take(max_len);
-
-        let mut pos = sig_stream.zip(arg_stream);
-        let common_ifaces = withs
-            .map(|e| e.iter().rev())
-            .into_iter()
-            .flatten()
-            .flat_map(|w| self.common_iface_fields(w))
-            .chain(self.common_iface_fields(args));
-        let mut named = common_ifaces.map(|(n, l, r)| (l, r));
-
-        pos.chain(named)
-    }
-}
-
-impl fmt::Debug for SigTy {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.write_str("(")?;
-        let pos = self.positional_params().map(ParamTy::Pos);
-        let named = self
-            .named_params()
-            .map(|(name, ty)| ParamTy::Named(name, ty));
-        let rest = self.rest_param().map(ParamTy::Rest);
-        interpersed(f, pos.chain(named).chain(rest))?;
-        f.write_str(") => ")?;
-        if let Some(ret) = &self.ret {
-            ret.fmt(f)?;
-        } else {
-            f.write_str("any")?;
-        }
-        Ok(())
-    }
-}
-
-pub type ArgsTy = SigTy;
-
-#[derive(Hash, Clone, PartialEq, Eq)]
-pub struct SigWithTy {
-    pub sig: TyRef,
-    pub with: Interned<ArgsTy>,
-}
-
-impl SigWithTy {
-    pub fn new(sig: TyRef, with: Interned<ArgsTy>) -> Interned<Self> {
-        Interned::new(Self { sig, with })
-    }
-}
-
-impl fmt::Debug for SigWithTy {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:?}.with({:?})", self.sig, self.with)
-    }
-}
-
-#[derive(Hash, Clone, PartialEq, Eq)]
-pub struct SelectTy {
-    pub ty: Interned<Ty>,
-    pub select: Interned<str>,
-}
-
-impl SelectTy {
-    pub fn new(ty: Interned<Ty>, select: Interned<str>) -> Interned<Self> {
-        Interned::new(Self { ty, select })
-    }
-}
-
-impl fmt::Debug for SelectTy {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{:?}.{}", RefDebug(&self.ty), self.select)
-    }
-}
-
-#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
-pub(crate) enum UnaryOp {
-    Pos,
-    Neg,
-    Not,
-    Context,
-    NotElementOf,
-    ElementOf,
-    TypeOf,
-}
-
-#[derive(Debug, Hash, Clone, PartialEq, Eq)]
-pub struct TypeUnary {
-    pub lhs: Interned<Ty>,
-    pub op: UnaryOp,
-}
-
-impl TypeUnary {
-    pub fn new(op: UnaryOp, lhs: Interned<Ty>) -> Interned<Self> {
-        Interned::new(Self { lhs, op })
-    }
-}
-
-#[derive(Debug, Hash, Clone, PartialEq, Eq)]
-pub struct TypeBinary {
-    pub operands: (Interned<Ty>, Interned<Ty>),
-    pub op: ast::BinOp,
-}
-
-impl TypeBinary {
-    pub fn new(op: ast::BinOp, lhs: Interned<Ty>, rhs: Interned<Ty>) -> Interned<Self> {
-        Interned::new(Self {
-            operands: (lhs, rhs),
-            op,
-        })
-    }
-
-    pub fn repr(&self) -> (&Interned<Ty>, &Interned<Ty>) {
-        (&self.operands.0, &self.operands.1)
-    }
-}
-
-#[derive(Debug, Hash, Clone, PartialEq, Eq)]
-pub(crate) struct IfTy {
-    pub cond: Interned<Ty>,
-    pub then: Interned<Ty>,
-    pub else_: Interned<Ty>,
-}
-
-impl IfTy {
-    pub fn new(cond: Interned<Ty>, then: Interned<Ty>, else_: Interned<Ty>) -> Interned<Self> {
-        Interned::new(Self { cond, then, else_ })
-    }
-}
-
-#[derive(Hash, Clone, PartialEq, Eq)]
-pub(crate) enum Ty {
+pub enum Ty {
+    // Simple Types
+    /// A top type, whose negation is bottom type.
+    /// `t := top, t^- := bottom`
     Any,
+    /// A boolean type, can be `false`, `true`, or both (boolean type).
+    /// `t := false | true`
     Boolean(Option<bool>),
+    /// All possible types in typst.
     Builtin(BuiltinTy),
+    /// A possible typst instance of some type.
     Value(Interned<InsTy>),
+    /// A field type
     Field(Interned<FieldTy>),
 
-    Var(Interned<TypeVar>),
+    // Combination Types
+    /// A union type, whose negation is intersection type.
+    /// `t := t1 | t2 | ... | tn, t^- := t1 & t2 & ... & tn`
     Union(Interned<Vec<Ty>>),
+    /// A frozen type variable
+    /// `t :> t1 | t2 | ... | tn <: f1 & f2 & ... & fn`
     Let(Interned<TypeBounds>),
+    /// An opening type variable owing bounds
+    Var(Interned<TypeVar>),
 
-    Func(Interned<SigTy>),
-    With(Interned<SigWithTy>),
-    Args(Interned<ArgsTy>),
+    // Composite Types
+    /// A typst dictionary type
     Dict(Interned<RecordTy>),
-    Array(Interned<Ty>),
-    // Note: may contains spread types
+    /// An array type
+    Array(TyRef),
+    /// A tuple type
+    /// Note: may contains spread types
     Tuple(Interned<Vec<Ty>>),
+    /// A function type
+    Func(Interned<SigTy>),
+    /// An argument type
+    Args(Interned<ArgsTy>),
+
+    // Type operations
+    /// A partially applied function type
+    With(Interned<SigWithTy>),
+    /// Select a field from a type
     Select(Interned<SelectTy>),
+    /// A unary operation
     Unary(Interned<TypeUnary>),
+    /// A binary operation
     Binary(Interned<TypeBinary>),
+    /// A conditional type
     If(Interned<IfTy>),
 }
 
@@ -838,11 +128,13 @@ impl fmt::Debug for Ty {
 }
 
 impl Ty {
-    pub(crate) fn is_dict(&self) -> bool {
+    /// Whether the type is a dictionary type
+    pub fn is_dict(&self) -> bool {
         matches!(self, Ty::Dict(..))
     }
 
-    pub(crate) fn from_types(e: impl ExactSizeIterator<Item = Ty>) -> Self {
+    /// Create a union type from an iterator of types
+    pub fn from_types(e: impl ExactSizeIterator<Item = Ty>) -> Self {
         if e.len() == 0 {
             Ty::Any
         } else if e.len() == 1 {
@@ -853,15 +145,851 @@ impl Ty {
         }
     }
 
-    pub(crate) fn iter_union(e: impl IntoIterator<Item = Ty>) -> Self {
+    /// Create a union type from an iterator of types
+    pub fn iter_union(e: impl IntoIterator<Item = Ty>) -> Self {
         Ty::Union(Interned::new(e.into_iter().collect()))
     }
 
+    /// Create an undefined type (which will emit an error)
+    /// A that type is annotated if the syntax structure causes an type error
     pub const fn undef() -> Self {
         Ty::Builtin(BuiltinTy::Undef)
     }
 }
 
+/// A function parameter type
+pub enum TypeSigParam<'a> {
+    /// A positional parameter
+    Pos(&'a Ty),
+    /// A named parameter
+    Named(&'a StrRef, &'a Ty),
+    /// A rest parameter (spread right)
+    Rest(&'a Ty),
+}
+
+impl fmt::Debug for TypeSigParam<'_> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            TypeSigParam::Pos(ty) => write!(f, "{ty:?}"),
+            TypeSigParam::Named(name, ty) => write!(f, "{name:?}: {ty:?}"),
+            TypeSigParam::Rest(ty) => write!(f, "...: {ty:?}[]"),
+        }
+    }
+}
+
+/// The syntax source (definition) of a type node
+/// todo: whether we should store them in the type node
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct TypeSource {
+    /// A name node with span
+    pub name_node: SyntaxNode,
+    /// A lazy evaluated name
+    pub name_repr: OnceCell<StrRef>,
+    /// Attached documentation
+    pub doc: StrRef,
+}
+
+impl Hash for TypeSource {
+    fn hash<H: Hasher>(&self, state: &mut H) {
+        self.name_node.hash(state);
+        self.doc.hash(state);
+    }
+}
+
+impl TypeSource {
+    /// Get name of the type node
+    pub fn name(&self) -> StrRef {
+        self.name_repr
+            .get_or_init(|| {
+                let name = self.name_node.text();
+                if !name.is_empty() {
+                    return name.into();
+                }
+                let name = self.name_node.clone().into_text();
+                name.into()
+            })
+            .clone()
+    }
+}
+
+/// An ordered list of names
+#[derive(Debug, Hash, Clone, PartialEq, Eq)]
+pub struct NameBone {
+    /// The names in the bone
+    pub names: Box<[StrRef]>,
+}
+
+impl NameBone {
+    /// Create an empty bone
+    pub fn empty() -> Interned<Self> {
+        Interned::new(Self {
+            names: Box::new([]),
+        })
+    }
+}
+
+impl NameBone {
+    /// Find the index of the name in the bone
+    pub fn find(&self, name: &StrRef) -> Option<usize> {
+        self.names.binary_search_by(|probe| probe.cmp(name)).ok()
+    }
+}
+
+impl NameBone {
+    /// Intersect the names of two bones
+    pub fn intersect_enumerate<'a>(
+        &'a self,
+        rhs: &'a NameBone,
+    ) -> impl Iterator<Item = (usize, usize)> + 'a {
+        let mut lhs_iter = self.names.iter().enumerate();
+        let mut rhs_iter = rhs.names.iter().enumerate();
+
+        let mut lhs = lhs_iter.next();
+        let mut rhs = rhs_iter.next();
+
+        std::iter::from_fn(move || 'name_scanning: loop {
+            if let (Some((i, lhs_key)), Some((j, rhs_key))) = (lhs, rhs) {
+                match lhs_key.cmp(rhs_key) {
+                    std::cmp::Ordering::Less => {
+                        lhs = lhs_iter.next();
+                        continue 'name_scanning;
+                    }
+                    std::cmp::Ordering::Greater => {
+                        rhs = rhs_iter.next();
+                        continue 'name_scanning;
+                    }
+                    std::cmp::Ordering::Equal => {
+                        lhs = lhs_iter.next();
+                        rhs = rhs_iter.next();
+                        return Some((i, j));
+                    }
+                }
+            }
+            return None;
+        })
+    }
+}
+
+/// A frozen type variable (bounds of some type in program)
+/// `t :> t1 | ... | tn <: f1 & ... & fn`
+/// `  lbs------------- ubs-------------`
+#[derive(Hash, Clone, PartialEq, Eq, Default)]
+pub struct TypeBounds {
+    /// The lower bounds
+    pub lbs: EcoVec<Ty>,
+    /// The upper bounds
+    pub ubs: EcoVec<Ty>,
+}
+
+impl fmt::Debug for TypeBounds {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        // write!(f, "{}", self.name)
+        // also where
+        if !self.lbs.is_empty() {
+            write!(f, " ⪰ {:?}", self.lbs[0])?;
+            for lb in &self.lbs[1..] {
+                write!(f, " | {lb:?}")?;
+            }
+        }
+        if !self.ubs.is_empty() {
+            write!(f, " ⪯ {:?}", self.ubs[0])?;
+            for ub in &self.ubs[1..] {
+                write!(f, " & {ub:?}")?;
+            }
+        }
+        Ok(())
+    }
+}
+
+/// A common type kinds for those types that has fields (Abstracted record
+/// type).
+pub trait TypeInterface {
+    /// Get the bone of a record.
+    /// See [`NameBone`] for more details.
+    fn bone(&self) -> &Interned<NameBone>;
+    /// Iterate over the fields of a record.
+    fn interface(&self) -> impl Iterator<Item = (&StrRef, &Ty)>;
+    /// Get the field by bone offset.
+    fn field_by_bone_offset(&self, i: usize) -> Option<&Ty>;
+}
+
+/// Extension common methods for [`TypeInterface`].
+pub trait TypeInterfaceExt: TypeInterface {
+    /// Convenience method to get the common fields of two records.
+    fn common_iface_fields<'a>(
+        &'a self,
+        rhs: &'a Self,
+    ) -> impl Iterator<Item = (&'a StrRef, &'a Ty, &'a Ty)> {
+        let lhs_names = self.bone();
+        let rhs_names = rhs.bone();
+
+        lhs_names
+            .intersect_enumerate(rhs_names)
+            .filter_map(move |(i, j)| {
+                let lhs = self.field_by_bone_offset(i)?;
+                let rhs = rhs.field_by_bone_offset(j)?;
+                Some((&lhs_names.names[i], lhs, rhs))
+            })
+    }
+}
+
+impl<T: TypeInterface> TypeInterfaceExt for T {}
+
+/// An instance of a typst type
+#[derive(Debug, Hash, Clone, PartialEq)]
+pub struct InsTy {
+    /// The value of the instance
+    pub val: Value,
+    /// The syntax source of the instance
+    pub syntax: Option<Interned<TypeSource>>,
+}
+
+/// There are some case that val is not Eq, but we make it Eq for simplicity
+/// For example, a float instance which is NaN.
+impl Eq for InsTy {}
+
+impl InsTy {
+    /// Create a instance
+    pub fn new(val: Value) -> Interned<Self> {
+        Self { val, syntax: None }.into()
+    }
+
+    /// Create a instance with a sapn
+    pub fn new_at(val: Value, s: Span) -> Interned<Self> {
+        let mut l = SyntaxNode::leaf(SyntaxKind::Ident, "");
+        l.synthesize(s);
+        Interned::new(Self {
+            val,
+            syntax: Some(Interned::new(TypeSource {
+                name_node: l,
+                name_repr: OnceCell::new(),
+                doc: "".into(),
+            })),
+        })
+    }
+    /// Create a instance with a documentation string
+    pub fn new_doc(val: Value, doc: impl Into<StrRef>) -> Interned<Self> {
+        Interned::new(Self {
+            val,
+            syntax: Some(Interned::new(TypeSource {
+                name_node: SyntaxNode::default(),
+                name_repr: OnceCell::new(),
+                doc: doc.into(),
+            })),
+        })
+    }
+}
+
+/// A field type
+#[derive(Debug, Hash, Clone, PartialEq, Eq)]
+pub struct FieldTy {
+    /// The name of the field
+    pub name: StrRef,
+    /// The type of the field
+    pub field: Ty,
+}
+
+impl FieldTy {
+    /// Create an untyped field type
+    pub fn new_untyped(name: StrRef) -> Interned<Self> {
+        Interned::new(Self {
+            name,
+            field: Ty::Any,
+        })
+    }
+}
+
+/// A type variable
+#[derive(Hash, Clone, PartialEq, Eq)]
+pub struct TypeVar {
+    /// The name of the type variable
+    pub name: StrRef,
+    /// The definition id of the type variable
+    pub def: DefId,
+}
+
+impl Ord for TypeVar {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.name
+            .cmp(&other.name)
+            .then_with(|| self.def.0.cmp(&other.def.0))
+    }
+}
+
+impl PartialOrd for TypeVar {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+impl fmt::Debug for TypeVar {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "@{}", self.name)
+    }
+}
+
+impl TypeVar {
+    /// Create a type variable
+    pub fn new(name: StrRef, def: DefId) -> Interned<Self> {
+        Interned::new(Self { name, def })
+    }
+
+    /// Get the name of the type variable
+    pub fn name(&self) -> StrRef {
+        self.name.clone()
+    }
+
+    /// Get the definition id of the type variable
+    pub fn id(&self) -> DefId {
+        self.def
+    }
+}
+
+/// A record type
+#[derive(Hash, Clone, PartialEq, Eq)]
+pub struct RecordTy {
+    /// The names of the fields
+    pub names: Interned<NameBone>,
+    /// The types of the fields
+    pub types: Interned<Vec<Ty>>,
+}
+
+impl RecordTy {
+    /// Shape the fields of a record
+    pub fn shape_fields(mut fields: Vec<(StrRef, Ty, Span)>) -> (NameBone, Vec<Ty>) {
+        fields.sort_by(|a, b| a.0.cmp(&b.0));
+        let names = NameBone {
+            names: fields.iter().map(|e| e.0.clone()).collect(),
+        };
+        let types = fields.into_iter().map(|(_, ty, _)| ty).collect::<Vec<_>>();
+
+        (names, types)
+    }
+
+    /// Create a record type
+    pub fn new(fields: Vec<(StrRef, Ty, Span)>) -> Interned<Self> {
+        let (names, types) = Self::shape_fields(fields);
+        Interned::new(Self {
+            types: Interned::new(types),
+            names: Interned::new(names),
+        })
+    }
+}
+
+impl TypeInterface for RecordTy {
+    fn bone(&self) -> &Interned<NameBone> {
+        &self.names
+    }
+
+    fn field_by_bone_offset(&self, i: usize) -> Option<&Ty> {
+        self.types.get(i)
+    }
+
+    fn interface(&self) -> impl Iterator<Item = (&StrRef, &Ty)> {
+        self.names.names.iter().zip(self.types.iter())
+    }
+}
+
+impl fmt::Debug for RecordTy {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str("{")?;
+        interpersed(
+            f,
+            self.interface()
+                .map(|(name, ty)| TypeSigParam::Named(name, ty)),
+        )?;
+        f.write_str("}")
+    }
+}
+
+/// A typst function type
+#[derive(Hash, Clone, PartialEq, Eq)]
+pub struct SigTy {
+    /// The input types of the function
+    pub inputs: Interned<Vec<Ty>>,
+    /// The return (body) type of the function
+    pub body: Option<Ty>,
+    /// The name bone of the named parameters
+    pub names: Interned<NameBone>,
+    /// The index of the first named parameter
+    pub name_started: u32,
+    /// Whether the function has a spread left parameter
+    pub spread_left: bool,
+    /// Whether the function has a spread right parameter
+    pub spread_right: bool,
+}
+
+impl SigTy {
+    /// Array constructor
+    #[comemo::memoize]
+    pub fn array_cons(elem: Ty, anyify: bool) -> Interned<SigTy> {
+        let ret = if anyify {
+            Ty::Any
+        } else {
+            Ty::Array(Interned::new(elem.clone()))
+        };
+        Interned::new(Self {
+            inputs: Interned::new(vec![elem]),
+            body: Some(ret),
+            names: NameBone::empty(),
+            name_started: 0,
+            spread_left: false,
+            spread_right: true,
+        })
+    }
+
+    /// Dictionary constructor
+    #[comemo::memoize]
+    pub fn dict_cons(named: &Interned<RecordTy>, anyify: bool) -> Interned<SigTy> {
+        let ret = if anyify {
+            Ty::Any
+        } else {
+            Ty::Dict(named.clone())
+        };
+
+        Interned::new(Self {
+            inputs: named.types.clone(),
+            body: Some(ret),
+            names: named.names.clone(),
+            name_started: 0,
+            spread_left: false,
+            spread_right: false,
+        })
+    }
+
+    /// Create a function type
+    pub fn new(
+        pos: impl IntoIterator<Item = Ty>,
+        named: impl IntoIterator<Item = (StrRef, Ty)>,
+        rest: Option<Ty>,
+        ret_ty: Option<Ty>,
+    ) -> Self {
+        let named = named
+            .into_iter()
+            .map(|(name, ty)| (name, ty, Span::detached()))
+            .collect::<Vec<_>>();
+        let (names, types) = RecordTy::shape_fields(named);
+        let spread_right = rest.is_some();
+
+        let name_started = if spread_right { 1 } else { 0 } + types.len();
+        let types = pos.into_iter().chain(types).chain(rest).collect::<Vec<_>>();
+
+        let name_started = (types.len() - name_started) as u32;
+
+        Self {
+            inputs: Interned::new(types),
+            body: ret_ty,
+            names: Interned::new(names),
+            name_started,
+            spread_left: false,
+            spread_right,
+        }
+    }
+}
+
+impl Default for SigTy {
+    fn default() -> Self {
+        Self {
+            inputs: Interned::new(Vec::new()),
+            body: None,
+            names: NameBone::empty(),
+            name_started: 0,
+            spread_left: false,
+            spread_right: false,
+        }
+    }
+}
+
+impl TypeInterface for SigTy {
+    fn bone(&self) -> &Interned<NameBone> {
+        &self.names
+    }
+
+    fn interface(&self) -> impl Iterator<Item = (&StrRef, &Ty)> {
+        let names = self.names.names.iter();
+        let types = self.inputs.iter().skip(self.name_started as usize);
+        names.zip(types)
+    }
+
+    fn field_by_bone_offset(&self, i: usize) -> Option<&Ty> {
+        self.inputs.get(i + self.name_started as usize)
+    }
+}
+
+impl SigTy {
+    /// Get the input types of the function
+    pub fn inputs(&self) -> impl Iterator<Item = &Ty> {
+        self.inputs.iter()
+    }
+
+    /// Get the positional parameters of the function
+    pub fn positional_params(&self) -> impl ExactSizeIterator<Item = &Ty> {
+        self.inputs.iter().take(self.name_started as usize)
+    }
+
+    /// Get the parameter at the given index
+    pub fn pos(&self, idx: usize) -> Option<&Ty> {
+        (idx < self.name_started as usize)
+            .then_some(())
+            .and_then(|_| self.inputs.get(idx))
+    }
+
+    /// Get the named parameters of the function
+    pub fn named_params(&self) -> impl ExactSizeIterator<Item = (&StrRef, &Ty)> {
+        let named_names = self.names.names.iter();
+        let named_types = self.inputs.iter().skip(self.name_started as usize);
+
+        named_names.zip(named_types)
+    }
+
+    /// Get the named parameter by given name
+    pub fn named(&self, name: &StrRef) -> Option<&Ty> {
+        let idx = self.names.find(name)?;
+        self.inputs.get(idx + self.name_started as usize)
+    }
+
+    /// Get the rest parameter of the function
+    pub fn rest_param(&self) -> Option<&Ty> {
+        if self.spread_right {
+            self.inputs.last()
+        } else {
+            None
+        }
+    }
+
+    /// Match the function type with the given arguments
+    pub fn matches<'a>(
+        &'a self,
+        args: &'a SigTy,
+        withs: Option<&'a Vec<Interned<crate::analysis::SigTy>>>,
+    ) -> impl Iterator<Item = (&'a Ty, &'a Ty)> + 'a {
+        let with_len = withs
+            .map(|w| w.iter().map(|w| w.positional_params().len()).sum::<usize>())
+            .unwrap_or(0);
+
+        let sig_pos = self.positional_params();
+        let arg_pos = args.positional_params();
+
+        let sig_rest = self.rest_param();
+        let arg_rest = args.rest_param();
+
+        let max_len = sig_pos.len().max(with_len + arg_pos.len())
+            + if sig_rest.is_some() && arg_rest.is_some() {
+                1
+            } else {
+                0
+            };
+
+        let arg_pos = withs
+            .into_iter()
+            .flat_map(|w| w.iter().rev().map(|w| w.positional_params()))
+            .flatten()
+            .chain(arg_pos);
+
+        let sig_stream = sig_pos.chain(sig_rest.into_iter().cycle()).take(max_len);
+        let arg_stream = arg_pos.chain(arg_rest.into_iter().cycle()).take(max_len);
+
+        let pos = sig_stream.zip(arg_stream);
+        let common_ifaces = withs
+            .map(|e| e.iter().rev())
+            .into_iter()
+            .flatten()
+            .flat_map(|w| self.common_iface_fields(w))
+            .chain(self.common_iface_fields(args));
+        let named = common_ifaces.map(|(_, l, r)| (l, r));
+
+        pos.chain(named)
+    }
+}
+
+impl fmt::Debug for SigTy {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.write_str("(")?;
+        let pos = self.positional_params().map(TypeSigParam::Pos);
+        let named = self
+            .named_params()
+            .map(|(name, ty)| TypeSigParam::Named(name, ty));
+        let rest = self.rest_param().map(TypeSigParam::Rest);
+        interpersed(f, pos.chain(named).chain(rest))?;
+        f.write_str(") => ")?;
+        if let Some(ret) = &self.body {
+            ret.fmt(f)?;
+        } else {
+            f.write_str("any")?;
+        }
+        Ok(())
+    }
+}
+
+/// A function argument type
+pub type ArgsTy = SigTy;
+
+/// A type with partially applied arguments
+#[derive(Hash, Clone, PartialEq, Eq)]
+pub struct SigWithTy {
+    /// The signature of the function
+    pub sig: TyRef,
+    /// The arguments applied to the function
+    pub with: Interned<ArgsTy>,
+}
+
+impl SigWithTy {
+    /// Create a type with applied arguments
+    pub fn new(sig: TyRef, with: Interned<ArgsTy>) -> Interned<Self> {
+        Interned::new(Self { sig, with })
+    }
+}
+
+impl fmt::Debug for SigWithTy {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{:?}.with({:?})", self.sig, self.with)
+    }
+}
+
+/// A field selection type
+#[derive(Hash, Clone, PartialEq, Eq)]
+pub struct SelectTy {
+    /// The type to select from
+    pub ty: TyRef,
+    /// The field to select
+    pub select: StrRef,
+}
+
+impl SelectTy {
+    /// Create a field selection type
+    pub fn new(ty: TyRef, select: StrRef) -> Interned<Self> {
+        Interned::new(Self { ty, select })
+    }
+}
+
+impl fmt::Debug for SelectTy {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{:?}.{}", RefDebug(&self.ty), self.select)
+    }
+}
+
+/// The kind of unary operation
+#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
+pub enum UnaryOp {
+    /// The (arithmetic) positive operation
+    /// `+t`
+    Pos,
+    /// The (arithmetic) negate operation
+    /// `-t`
+    Neg,
+    /// The (logical) not operation
+    /// `not t`
+    Not,
+    /// The typst context operation
+    /// `context t`
+    Context,
+    /// The not element of operation
+    /// `not in t`
+    NotElementOf,
+    /// The element of operation
+    /// `in t`
+    ElementOf,
+    /// The type of operation
+    /// `type(t)`
+    TypeOf,
+}
+
+/// A unary operation type
+#[derive(Debug, Hash, Clone, PartialEq, Eq)]
+pub struct TypeUnary {
+    /// The operand of the unary operation
+    pub lhs: TyRef,
+    /// The kind of the unary operation
+    pub op: UnaryOp,
+}
+
+impl TypeUnary {
+    /// Create a unary operation type
+    pub fn new(op: UnaryOp, lhs: TyRef) -> Interned<Self> {
+        Interned::new(Self { lhs, op })
+    }
+
+    /// Get the operands of the unary operation
+    pub fn operands(&self) -> [&TyRef; 1] {
+        [&self.lhs]
+    }
+}
+
+/// The kind of binary operation
+pub type BinaryOp = ast::BinOp;
+
+/// A binary operation type
+#[derive(Debug, Hash, Clone, PartialEq, Eq)]
+pub struct TypeBinary {
+    /// The operands of the binary operation
+    pub operands: (TyRef, TyRef),
+    /// The kind of the binary operation
+    pub op: BinaryOp,
+}
+
+impl TypeBinary {
+    /// Create a binary operation type
+    pub fn new(op: BinaryOp, lhs: TyRef, rhs: TyRef) -> Interned<Self> {
+        Interned::new(Self {
+            operands: (lhs, rhs),
+            op,
+        })
+    }
+
+    /// Get the operands of the binary operation
+    pub fn operands(&self) -> [&TyRef; 2] {
+        [&self.operands.0, &self.operands.1]
+    }
+}
+
+/// A conditional type
+/// `if t1 then t2 else t3`
+#[derive(Debug, Hash, Clone, PartialEq, Eq)]
+pub struct IfTy {
+    /// The condition
+    pub cond: TyRef,
+    /// The type when the condition is true
+    pub then: TyRef,
+    /// The type when the condition is false
+    pub else_: TyRef,
+}
+
+impl IfTy {
+    /// Create a conditional type
+    pub fn new(cond: TyRef, then: TyRef, else_: TyRef) -> Interned<Self> {
+        Interned::new(Self { cond, then, else_ })
+    }
+}
+
+/// A type scheme on a group of syntax structures (typing)
+#[derive(Default)]
+pub struct TypeScheme {
+    /// The typing on definitions
+    pub vars: HashMap<DefId, TypeVarBounds>,
+    /// The typing on syntax structures
+    pub mapping: HashMap<Span, Vec<Ty>>,
+
+    pub(super) cano_cache: Mutex<TypeCanoStore>,
+}
+
+impl TypeScheme {
+    /// Get the type of a definition
+    pub fn type_of_def(&self, def: DefId) -> Option<Ty> {
+        Some(self.simplify(self.vars.get(&def).map(|e| e.as_type())?, false))
+    }
+    /// Get the type of a syntax structure
+    pub fn type_of_span(&self, site: Span) -> Option<Ty> {
+        self.mapping
+            .get(&site)
+            .cloned()
+            .map(|e| Ty::from_types(e.into_iter()))
+    }
+
+    // todo: distinguish at least, at most
+    /// Witness a lower-bound type on a syntax structure
+    pub fn witness_at_least(&mut self, site: Span, ty: Ty) {
+        Self::witness_(site, ty, &mut self.mapping);
+    }
+    /// Witness a upper-bound type on a syntax structure
+    pub fn witness_at_most(&mut self, site: Span, ty: Ty) {
+        Self::witness_(site, ty, &mut self.mapping);
+    }
+
+    /// Witness a type
+    pub fn witness_(site: Span, ty: Ty, mapping: &mut HashMap<Span, Vec<Ty>>) {
+        if site.is_detached() {
+            return;
+        }
+
+        // todo: intersect/union
+        let site_store = mapping.entry(site);
+        match site_store {
+            Entry::Occupied(e) => {
+                e.into_mut().push(ty);
+            }
+            Entry::Vacant(e) => {
+                e.insert(vec![ty]);
+            }
+        }
+    }
+}
+
+/// A type variable bounds
+#[derive(Clone)]
+pub struct TypeVarBounds {
+    /// The type variable representation
+    pub var: Interned<TypeVar>,
+    /// The bounds of the type variable
+    pub bounds: FlowVarKind,
+}
+
+impl fmt::Debug for TypeVarBounds {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{:?}", self.var)
+    }
+}
+
+impl TypeVarBounds {
+    /// Create a type variable bounds
+    pub fn new(var: TypeVar, init: TypeBounds) -> Self {
+        Self {
+            var: Interned::new(var),
+            bounds: FlowVarKind::Strong(Arc::new(RwLock::new(init))),
+        }
+    }
+
+    /// Get the name of the type variable
+    pub fn name(&self) -> StrRef {
+        self.var.name.clone()
+    }
+    /// Get the definition id of the type variable
+    pub fn id(&self) -> DefId {
+        self.var.def
+    }
+
+    /// Get self as a type
+    pub fn as_type(&self) -> Ty {
+        Ty::Var(self.var.clone())
+    }
+
+    /// Slightly close the type variable
+    pub fn weaken(&mut self) {
+        match &self.bounds {
+            FlowVarKind::Strong(w) => {
+                self.bounds = FlowVarKind::Weak(w.clone());
+            }
+            FlowVarKind::Weak(_) => {}
+        }
+    }
+}
+
+/// A type variable bounds
+#[derive(Clone)]
+pub enum FlowVarKind {
+    /// A type variable that receives both types and values (type instnaces)
+    Strong(Arc<RwLock<TypeBounds>>),
+    /// A type variable that receives only types
+    /// The received values will be lifted to types
+    Weak(Arc<RwLock<TypeBounds>>),
+}
+
+impl FlowVarKind {
+    /// Get the bounds of the type variable
+    pub fn bounds(&self) -> &RwLock<TypeBounds> {
+        match self {
+            FlowVarKind::Strong(w) | FlowVarKind::Weak(w) => w,
+        }
+    }
+}
+
+#[derive(Default)]
+pub(super) struct TypeCanoStore {
+    pub cano_cache: HashMap<(Ty, bool), Ty>,
+    pub cano_local_cache: HashMap<(DefId, bool), Ty>,
+    pub negatives: HashSet<DefId>,
+    pub positives: HashSet<DefId>,
+}
+
 impl_internable!(Ty,);
 impl_internable!(InsTy,);
 impl_internable!(FieldTy,);
@@ -879,6 +1007,17 @@ impl_internable!(TypeBounds,);
 impl_internable!(NameBone,);
 impl_internable!((Ty, Ty),);
 
+struct RefDebug<'a>(&'a Ty);
+
+impl<'a> fmt::Debug for RefDebug<'a> {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self.0 {
+            Ty::Var(v) => write!(f, "@v{:?}", v.name()),
+            _ => write!(f, "{:?}", self.0),
+        }
+    }
+}
+
 fn interpersed<T: fmt::Debug>(
     f: &mut fmt::Formatter<'_>,
     iter: impl Iterator<Item = T>,
diff --git a/crates/tinymist-query/src/ty/describe.rs b/crates/tinymist-query/src/ty/describe.rs
index b4bf81a3..c20aa7b1 100644
--- a/crates/tinymist-query/src/ty/describe.rs
+++ b/crates/tinymist-query/src/ty/describe.rs
@@ -5,7 +5,8 @@ use typst::foundations::Repr;
 
 use crate::{adt::interner::Interned, analysis::*, ty::def::*};
 
-impl TypeCheckInfo {
+impl TypeScheme {
+    /// Describe the given type with the given type scheme.
     pub fn describe(&self, ty: &Ty) -> Option<String> {
         let mut worker = TypeDescriber::default();
         worker.describe_root(ty)
@@ -13,6 +14,7 @@ impl TypeCheckInfo {
 }
 
 impl Ty {
+    /// Describe the given type.
     pub fn describe(&self) -> Option<String> {
         let mut worker = TypeDescriber::default();
         worker.describe_root(self)
@@ -80,7 +82,7 @@ impl TypeDescriber {
             }
             res.push_str(") => ");
             res.push_str(
-                f.ret
+                f.body
                     .as_ref()
                     .and_then(|ret| self.describe_root(ret))
                     .as_deref()
diff --git a/crates/tinymist-query/src/ty/mod.rs b/crates/tinymist-query/src/ty/mod.rs
index 4193ff45..3da0cf57 100644
--- a/crates/tinymist-query/src/ty/mod.rs
+++ b/crates/tinymist-query/src/ty/mod.rs
@@ -13,7 +13,7 @@ mod subst;
 pub(crate) use apply::*;
 pub(crate) use bound::*;
 pub(crate) use builtin::*;
-pub(crate) use def::*;
+pub use def::*;
 pub(crate) use mutate::*;
 pub(crate) use sig::*;
 
diff --git a/crates/tinymist-query/src/ty/mutate.rs b/crates/tinymist-query/src/ty/mutate.rs
index 255a9cae..9a6a09bd 100644
--- a/crates/tinymist-query/src/ty/mutate.rs
+++ b/crates/tinymist-query/src/ty/mutate.rs
@@ -32,17 +32,21 @@ pub trait MutateDriver {
     }
 
     fn mutate_func(&mut self, ty: &Interned<SigTy>, pol: bool) -> Option<SigTy> {
-        let types = self.mutate_vec(&ty.types, pol);
-        let ret = self.mutate_option(ty.ret.as_ref(), pol);
+        let types = self.mutate_vec(&ty.inputs, pol);
+        let ret = self.mutate_option(ty.body.as_ref(), pol);
 
         if types.is_none() && ret.is_none() {
             return None;
         }
 
         let sig = ty.as_ref().clone();
-        let types = types.unwrap_or_else(|| ty.types.clone());
-        let ret = ret.unwrap_or_else(|| ty.ret.clone());
-        Some(SigTy { types, ret, ..sig })
+        let types = types.unwrap_or_else(|| ty.inputs.clone());
+        let ret = ret.unwrap_or_else(|| ty.body.clone());
+        Some(SigTy {
+            inputs: types,
+            body: ret,
+            ..sig
+        })
     }
 
     fn mutate_record(&mut self, ty: &Interned<RecordTy>, pol: bool) -> Option<RecordTy> {
@@ -127,6 +131,7 @@ where
 }
 
 impl Ty {
+    /// Mutate the given type.
     pub fn mutate(&self, pol: bool, checker: &mut impl MutateDriver) -> Option<Ty> {
         let mut worker = Mutator;
         worker.ty(self, pol, checker)
diff --git a/crates/tinymist-query/src/ty/sig.rs b/crates/tinymist-query/src/ty/sig.rs
index 195b2405..b1b9a4bf 100644
--- a/crates/tinymist-query/src/ty/sig.rs
+++ b/crates/tinymist-query/src/ty/sig.rs
@@ -90,6 +90,7 @@ where
 }
 
 impl Ty {
+    /// Iterate over the signatures of the given type.
     pub fn sig_surface(&self, pol: bool, sig_kind: SigSurfaceKind, checker: &mut impl SigChecker) {
         let context = SigCheckContext {
             sig_kind,
@@ -104,6 +105,7 @@ impl Ty {
         worker.ty(self, pol);
     }
 
+    /// Get the signature representation of the given type.
     pub fn sig_repr(&self, pol: bool) -> Option<Interned<SigTy>> {
         // todo: union sig
         // let mut pos = vec![];
@@ -248,7 +250,7 @@ impl BoundChecker for SigCheckDriver<'_> {
     }
 }
 
-struct MethodDriver<'a, 'b>(&'a mut SigCheckDriver<'b>, &'a Interned<str>);
+struct MethodDriver<'a, 'b>(&'a mut SigCheckDriver<'b>, &'a StrRef);
 
 impl<'a, 'b> MethodDriver<'a, 'b> {
     fn is_binder(&self) -> bool {
diff --git a/crates/tinymist-query/src/ty/simplify.rs b/crates/tinymist-query/src/ty/simplify.rs
index 0e2dd0ef..41a8251e 100644
--- a/crates/tinymist-query/src/ty/simplify.rs
+++ b/crates/tinymist-query/src/ty/simplify.rs
@@ -17,7 +17,8 @@ struct CompactTy {
     is_final: bool,
 }
 
-impl TypeCheckInfo {
+impl TypeScheme {
+    /// Simplify (Canonicalize) the given type with the given type scheme.
     pub fn simplify(&self, ty: Ty, principal: bool) -> Ty {
         let mut c = self.cano_cache.lock();
         let c = &mut *c;
@@ -94,7 +95,7 @@ impl<'a, 'b> TypeSimplifier<'a, 'b> {
                 for p in f.inputs() {
                     self.analyze(p, !pol);
                 }
-                if let Some(ret) = &f.ret {
+                if let Some(ret) = &f.body {
                     self.analyze(ret, pol);
                 }
             }
@@ -124,7 +125,7 @@ impl<'a, 'b> TypeSimplifier<'a, 'b> {
             }
             Ty::Unary(u) => self.analyze(&u.lhs, pol),
             Ty::Binary(b) => {
-                let (lhs, rhs) = b.repr();
+                let [lhs, rhs] = b.operands();
                 self.analyze(lhs, pol);
                 self.analyze(rhs, pol);
             }
@@ -203,7 +204,7 @@ impl<'a, 'b> TypeSimplifier<'a, 'b> {
             Ty::Args(args) => Ty::Args(self.transform_sig(args, !pol)),
             Ty::Unary(u) => Ty::Unary(TypeUnary::new(u.op, self.transform(&u.lhs, pol).into())),
             Ty::Binary(b) => {
-                let (lhs, rhs) = b.repr();
+                let [lhs, rhs] = b.operands();
                 let lhs = self.transform(lhs, pol);
                 let rhs = self.transform(rhs, pol);
 
@@ -272,9 +273,9 @@ impl<'a, 'b> TypeSimplifier<'a, 'b> {
 
     fn transform_sig(&mut self, sig: &SigTy, pol: bool) -> Interned<SigTy> {
         let mut sig = sig.clone();
-        sig.types = self.transform_seq(&sig.types, !pol);
-        if let Some(ret) = &sig.ret {
-            sig.ret = Some(self.transform(ret, pol));
+        sig.inputs = self.transform_seq(&sig.inputs, !pol);
+        if let Some(ret) = &sig.body {
+            sig.body = Some(self.transform(ret, pol));
         }
 
         // todo: we can reduce one clone by early compare on sig.types
diff --git a/crates/tinymist-query/src/ty/subst.rs b/crates/tinymist-query/src/ty/subst.rs
index 0190bb7d..1d24b3ac 100644
--- a/crates/tinymist-query/src/ty/subst.rs
+++ b/crates/tinymist-query/src/ty/subst.rs
@@ -42,7 +42,7 @@ impl<'a> Sig<'a> {
             }
         }
 
-        Some((arguments, sig.ret.clone()))
+        Some((arguments, sig.body.clone()))
     }
 }
 
@@ -96,7 +96,7 @@ mod tests {
     struct CallCollector(Vec<Ty>);
 
     impl ApplyChecker for CallCollector {
-        fn call(
+        fn apply(
             &mut self,
             sig: super::Sig,
             arguments: &crate::adt::interner::Interned<super::ArgsTy>,
diff --git a/docs/overview.typ b/docs/overview.typ
index 9921a4a9..92321d54 100644
--- a/docs/overview.typ
+++ b/docs/overview.typ
@@ -23,7 +23,7 @@
   it.lines.at(0).body.children.slice(0, -2).join()
 }
 
-This document gives an overview of tinymist service, which provides a single integrated language service for Typst. This document doesn't dive in details but doesn't avoid showing code if necessary.
+This document gives an overview of tinymist service, which provides a single integrated language service for Typst. This document doesn't dive in details unless necessary.
 
 == Principles
 
@@ -61,13 +61,13 @@ Four principles are followed:
 
   A _Hover_ request is taken as example of that events.
 
-  A global unique `LspActor` takes the event and mutates a global server state. If the event requires some additional code analysis, it is converted into an analysis request, #link("https://github.com/search?q=repo%3AMyriad-Dreamin/tinymist%20CompilerQueryRequest&type=code")[```rs struct CompilerQueryRequest```], and pushed to the actors owning compiler resources. Otherwise, `LspActor` responds to the event according to its state. Obviously, the _Hover_ on code request requires code analysis.
+  A global unique `LspActor` takes the event and _mutates_ a global server state by the event. If the event requires some additional code analysis, it is converted into an analysis request, #link("https://github.com/search?q=repo%3AMyriad-Dreamin/tinymist%20CompilerQueryRequest&type=code")[```rs struct CompilerQueryRequest```], and pushed to the actors owning compiler resources. Otherwise, `LspActor` responds to the event directly. Obviously, the _Hover_ on code request requires code analysis.
 
-  The `CompileServerActor`s are created for each workspace and main entries (files/documents) in workspaces. When a compiler query is coming, a subset of that actors will take it and give project-specific responses, combining into a final concluded LSP response. Some analysis requests even require rendering features, and those requests will be pushed to the actors owning rendering resources. If you enable the periscope feature, a `Hover` on content request requires rendering on documents.
+  The `CompileServerActor`s are created for workspaces and main entries (files/documents) in workspaces. When a compiler query is coming, a subset of that actors will take it and give project-specific responses, combining into a final concluded LSP response. Some analysis requests even require rendering features, and those requests will be pushed to the actors owning rendering resources. If you enable the periscope feature, a `Hover` on content request requires rendering on documents.
 
-  The `RenderActor`s don't do compilations, but own project-specific rendering cache. They are designed for rendering docuemnt in _low latency_. This is the last sink of `Hover` requests. A `RenderActor` will receive an additional compiled `Document` object, and render the compiled frames in needed. After finishing rendering, a response attached with the rendered picture is sent to the LSP response channel intermediately.
+  The `RenderActor`s don't do compilations, but own project-specific rendering cache. They are designed for rendering documents in _low latency_. This is the last sink of `Hover` requests. A `RenderActor` will receive an additional compiled `Document` object, and render the compiled frames in needed. After finishing rendering, a response attached with the rendered picture is sent to the LSP response channel intermediately.
 
-/ Multi-level Analysis: The most critical features are lsp functions, built on the #link("https://github.com/Myriad-Dreamin/tinymist/tree/main/crates/tinymist-query")[tinymist-query] crate. To achieve low latency, functions are classified into different levels of analysis.
+/ Multi-level Analysis: The most critical features are lsp functions, built on the #link("https://github.com/Myriad-Dreamin/tinymist/tree/main/crates/tinymist-query")[tinymist-query] crate. To achieve higher concurrency, functions are classified into different levels of analysis.
   // + `query_token_cache` – `TokenRequest` – locks and accesses token cache.
   + `query_source` – `SyntaxRequest` – locks and accesses a single source unit.
   + `query_world` – `SemanticRequest` – locks and accesses multiple source units.