feat: implement naive substitution (β-reduction) (#292)

* feat: implement naive substitution (β-reduction)

* fix: order

* dev: harder tests

crates/tinymist-query/src/analysis/signature.rs

@@ -389,7 +389,7 @@ fn analyze_dyn_signature_inner(func: Func) -> Arc<PrimarySignature> {
 
     let sig_ty = SigTy::new(
         pos.iter().map(|e| e.base_type.clone().unwrap_or(Ty::Any)),
-        named_vec.into_iter(),
+        named_vec,
         rest.as_ref()
             .map(|e| e.base_type.clone().unwrap_or(Ty::Any)),
         ret_ty.clone(),

crates/tinymist-query/src/analysis/ty/apply.rs

@@ -37,8 +37,10 @@ impl<'a, 'b, 'w> ApplyChecker for ApplyTypeChecker<'a, 'b, 'w> {
             sig => (sig, false),
         };
 
-        if let Some(ty) = sig.call(args, pol, Some(self.base.ctx)) {
-            self.resultant.push(ty);
+        if !is_partialize {
+            if let Some(ty) = sig.call(args, pol, Some(self.base.ctx)) {
+                self.resultant.push(ty);
+            }
         }
 
         // todo: remove this after we implemented dependent types

crates/tinymist-query/src/analysis/ty/syntax.rs

@@ -353,7 +353,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
             }
         }
 
-        let args = ArgsTy::new(args_res.into_iter(), named.into_iter(), None, None);
+        let args = ArgsTy::new(args_res, named, None, None);
 
         Some(Ty::Args(args.into()))
     }
@@ -408,7 +408,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> {
             self.weaken(rest);
         }
 
-        let sig = SigTy::new(pos.into_iter(), named.into_iter(), rest, Some(body));
+        let sig = SigTy::new(pos, named, rest, Some(body));
         Some(Ty::Func(sig.into()))
     }
 

crates/tinymist-query/src/fixtures/type_check/snaps/test@with.typ.snap

@@ -4,8 +4,9 @@ expression: result
 input_file: crates/tinymist-query/src/fixtures/type_check/with.typ
 ---
 "f" = (Any) => Any
-"g" = (Any | ((Any) => Any).with(..(1) => any))
-"x" = ( ⪰ Any | Type(integer))
+"g" = ((Any) => Any).with(..(1) => any)
+"x" = ( ⪰ Any | Type(integer) | Type(integer))
+"x" = 1
 ---
 5..6 -> @f
 7..8 -> @x
@@ -13,4 +14,7 @@ input_file: crates/tinymist-query/src/fixtures/type_check/with.typ
 20..21 -> @g
 24..25 -> @f
 24..30 -> (@x) => @x
-24..33 -> (@x | ((@x) => @x).with(..(1) => any))
+24..33 -> ((@x) => @x).with(..(1) => any)
+40..41 -> @x
+44..45 -> (@g | Any)
+44..47 -> 1

crates/tinymist-query/src/fixtures/type_check/with.typ

@@ -1,2 +1,3 @@
 #let f(x) = x;
-#let g = f.with(1);
+#let g = f.with(1);
+#let x = g()

crates/tinymist-query/src/ty/builtin.rs

@@ -506,3 +506,24 @@ pub static FLOW_RADIUS_DICT: Lazy<Interned<RecordTy>> = Lazy::new(|| {
 // todo: csv.row-type can be an array or a dictionary
 
 // ISO 639
+
+#[cfg(test)]
+mod tests {
+    use reflexo::vector::ir::DefId;
+
+    use super::*;
+
+    // todo: map function
+    // Technical Note for implementing a map function:
+    // `u`, `v` is in level 2
+    // instantiate a `v` as the return type of the map function.
+    #[test]
+    fn test_map() {
+        let u = Ty::Var(TypeVar::new("u".into(), DefId(0)));
+        let v = Ty::Var(TypeVar::new("v".into(), DefId(1)));
+        let mapper_fn = Ty::Func(SigTy::new([u], None, None, Some(v.clone())).into());
+        let map_fn = Ty::Func(SigTy::new([mapper_fn], None, None, Some(v)).into());
+        let _ = map_fn;
+        // println!("{map_fn:?}");
+    }
+}

crates/tinymist-query/src/ty/def.rs

@@ -111,6 +111,23 @@ impl TypeSource {
 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);
@@ -404,6 +421,10 @@ impl TypeInterace for RecordTy {
         &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())
     }
@@ -496,19 +517,20 @@ impl SigTy {
     }
 
     pub(crate) fn new(
-        pos: impl Iterator<Item = Ty>,
-        named: impl Iterator<Item = (Interned<str>, Ty)>,
+        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.chain(types).chain(rest).collect::<Vec<_>>();
+        let types = pos.into_iter().chain(types).chain(rest).collect::<Vec<_>>();
 
         let name_started = (types.len() - name_started) as u32;
 
@@ -541,6 +563,22 @@ impl Default for SigTy {
     }
 }
 
+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)
@@ -575,37 +613,42 @@ impl SigTy {
     pub(crate) fn matches<'a>(
         &'a self,
         args: &'a SigTy,
-        withs: Option<&Vec<Interned<crate::analysis::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().skip(with_len);
+        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(arg_pos.len())
+        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 mut named =
-            self.names
-                .intersect_keys_enumerate(&args.names)
-                .filter_map(move |(i, j)| {
-                    let lhs = self.types.get(i + self.name_started as usize)?;
-                    let rhs = args.types.get(j + args.name_started as usize)?;
-                    Some((lhs, rhs))
-                });
+        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)
     }
@@ -890,45 +933,60 @@ mod tests {
             format!("{res:?}")
         }
 
-        assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1), None), @r###"[("p1", "q1")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1), None), @r###"[("p1", "q1")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, q2), None), @r###"[("p1", "q1"), ("p2", "q2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, q2), None), @r###"[("p1", "q1")]"###);
+        assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1), None), @"[(@p1, @q1)]");
+        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1), None), @"[(@p1, @q1)]");
+        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, q2), None), @"[(@p1, @q1), (@p2, @q2)]");
+        assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, q2), None), @"[(@p1, @q1)]");
 
-        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1), None), @r###"[("p1", "q1")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2), None), @r###"[("p1", "q1"), ("r1", "q2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2, q3), None), @r###"[("p1", "q1"), ("r1", "q2"), ("r1", "q3")]"###);
-        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, q2), None), @r###"[("r1", "q1"), ("r1", "q2")]"###);
+        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1), None), @"[(@p1, @q1)]");
+        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2), None), @"[(@p1, @q1), (@r1, @q2)]");
+        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2, q3), None), @"[(@p1, @q1), (@r1, @q2), (@r1, @q3)]");
+        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, q2), None), @"[(@r1, @q1), (@r1, @q2)]");
 
-        assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1"), ("p2", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, p2, p3), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1"), ("p2", "s2"), ("p3", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(...s2), None), @r###"[("p1", "s2"), ("p2", "s2")]"###);
+        assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, ...s2), None), @"[(@p1, @q1)]");
+        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, ...s2), None), @"[(@p1, @q1), (@p2, @s2)]");
+        assert_snapshot!(matches(literal_sig!(p1, p2, p3), literal_sig!(q1, ...s2), None), @"[(@p1, @q1), (@p2, @s2), (@p3, @s2)]");
+        assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(...s2), None), @"[(@p1, @s2), (@p2, @s2)]");
 
-        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1"), ("r1", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, ...s2), None), @r###"[("r1", "q1"), ("r1", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(...s2), None), @r###"[("p1", "s2"), ("r1", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(...s2), None), @r###"[("r1", "s2")]"###);
+        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, ...s2), None), @"[(@p1, @q1), (@r1, @s2)]");
+        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, ...s2), None), @"[(@r1, @q1), (@r1, @s2)]");
+        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(...s2), None), @"[(@p1, @s2), (@r1, @s2)]");
+        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(...s2), None), @"[(@r1, @s2)]");
 
-        assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(q1, ...s2), None), @r###"[("p0", "q1"), ("p1", "s2"), ("r1", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(...s2), None), @r###"[("p0", "s2"), ("p1", "s2"), ("r1", "s2")]"###);
+        assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(q1, ...s2), None), @"[(@p0, @q1), (@p1, @s2), (@r1, @s2)]");
+        assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(...s2), None), @"[(@p0, @s2), (@p1, @s2), (@r1, @s2)]");
 
-        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q0, q1, ...s2), None), @r###"[("p1", "q0"), ("r1", "q1"), ("r1", "s2")]"###);
-        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q0, q1, ...s2), None), @r###"[("r1", "q0"), ("r1", "q1"), ("r1", "s2")]"###);
+        assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q0, q1, ...s2), None), @"[(@p1, @q0), (@r1, @q1), (@r1, @s2)]");
+        assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q0, q1, ...s2), None), @"[(@r1, @q0), (@r1, @q1), (@r1, @s2)]");
 
-        assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2), None), @r###"[("p1", "q1"), ("w1", "w2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2), None), @r###"[("p1", "q1"), ("w1", "w2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2, ...s2), None), @r###"[("p1", "q1"), ("w1", "w2")]"###);
-        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2, ...s2), None), @r###"[("p1", "q1"), ("r1", "s2"), ("w1", "w2")]"###);
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2), None), @"[(@p1, @q1), (@w1, @w2)]");
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2), None), @"[(@p1, @q1), (@w1, @w2)]");
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2, ...s2), None), @"[(@p1, @q1), (@w1, @w2)]");
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2, ...s2), None), @"[(@p1, @q1), (@r1, @s2), (@w1, @w2)]");
 
         assert_snapshot!(matches(literal_sig!(), literal_sig!(!u1: w2), None), @"[]");
         assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(), None), @"[]");
-        assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(!u1: w2), None), @r###"[("w1", "w2")]"###);
+        assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(!u1: w2), None), @"[(@w1, @w2)]");
         assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(!u2: w2), None), @"[]");
         assert_snapshot!(matches(literal_sig!(!u2: w1), literal_sig!(!u1: w2), None), @"[]");
-        assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u1: w2, !u2: w4), None), @r###"[("w1", "w2"), ("w3", "w4")]"###);
-        assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u2: w2, !u1: w4), None), @r###"[("w1", "w4"), ("w3", "w2")]"###);
-        assert_snapshot!(matches(literal_sig!(!u2: w1), literal_sig!(!u1: w2, !u2: w4), None), @r###"[("w1", "w4")]"###);
-        assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w2), literal_sig!(!u2: w4), None), @r###"[("w2", "w4")]"###);
+        assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u1: w2, !u2: w4), None), @"[(@w1, @w2), (@w3, @w4)]");
+        assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u2: w2, !u1: w4), None), @"[(@w1, @w4), (@w3, @w2)]");
+        assert_snapshot!(matches(literal_sig!(!u2: w1), literal_sig!(!u1: w2, !u2: w4), None), @"[(@w1, @w4)]");
+        assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w2), literal_sig!(!u2: w4), None), @"[(@w2, @w4)]");
+
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, !u2: w2), literal_sig!(q1), Some(vec![
+            literal_sig!(!u2: w6),
+        ])), @"[(@p1, @q1), (@w2, @w6)]");
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, !u2: w2), literal_sig!(q1 !u2: w4), Some(vec![
+            literal_sig!(!u2: w5),
+        ])), @"[(@p1, @q1), (@w2, @w5), (@w2, @w4)]");
+        assert_snapshot!(matches(literal_sig!(p1 !u1: w1, !u2: w2), literal_sig!(q1 ), Some(vec![
+            literal_sig!(!u2: w7),
+            literal_sig!(!u2: w8),
+        ])), @"[(@p1, @q1), (@w2, @w8), (@w2, @w7)]");
+        assert_snapshot!(matches(literal_sig!(p1, p2, p3), literal_sig!(q1), Some(vec![
+            literal_sig!(q2),
+            literal_sig!(q3),
+        ])), @"[(@p1, @q3), (@p2, @q2), (@p3, @q1)]");
     }
 }

crates/tinymist-query/src/ty/mod.rs

@@ -5,6 +5,7 @@ mod bound;
 mod builtin;
 mod def;
 mod describe;
+mod mutate;
 mod sig;
 mod simplify;
 mod subst;
@@ -13,16 +14,18 @@ pub(crate) use apply::*;
 pub(crate) use bound::*;
 pub(crate) use builtin::*;
 pub(crate) use def::*;
+pub(crate) use mutate::*;
 pub(crate) use sig::*;
 
 #[cfg(test)]
 mod tests {
     use super::*;
     use crate::adt::interner::Interned;
-    use typst::foundations::Value;
+    use fxhash::hash64;
+    use reflexo::vector::ir::DefId;
 
-    pub fn str_ins(s: &str) -> Ty {
-        Ty::Value(InsTy::new(Value::Str(s.into())))
+    pub fn var_ins(s: &str) -> Ty {
+        Ty::Var(TypeVar::new(s.into(), DefId(hash64(s))))
     }
 
     pub fn str_sig(
@@ -31,10 +34,10 @@ mod tests {
         rest: Option<&str>,
         ret: Option<&str>,
     ) -> Interned<SigTy> {
-        let pos = pos.iter().map(|s| str_ins(s));
-        let named = named.iter().map(|(n, t)| ((*n).into(), str_ins(t)));
-        let rest = rest.map(str_ins);
-        let ret = ret.map(str_ins);
+        let pos = pos.iter().map(|s| var_ins(s));
+        let named = named.iter().map(|(n, t)| ((*n).into(), var_ins(t)));
+        let rest = rest.map(var_ins);
+        let ret = ret.map(var_ins);
         SigTy::new(pos, named, rest, ret).into()
     }
 
@@ -55,4 +58,5 @@ mod tests {
     }
 
     pub(crate) use literal_sig;
+    pub(crate) use literal_sig as literal_args;
 }

crates/tinymist-query/src/ty/mutate.rs

@@ -0,0 +1,207 @@
+use crate::{adt::interner::Interned, ty::def::*};
+
+pub trait MutateDriver {
+    fn mutate(&mut self, ty: &Ty, pol: bool) -> Option<Ty>;
+
+    fn mutate_vec(&mut self, ty: &[Ty], pol: bool) -> Option<Interned<Vec<Ty>>> {
+        let mut mutated = false;
+
+        let mut types = Vec::with_capacity(ty.len());
+        for ty in ty.iter() {
+            match self.mutate(ty, pol) {
+                Some(ty) => {
+                    types.push(ty);
+                    mutated = true;
+                }
+                None => types.push(ty.clone()),
+            }
+        }
+
+        if mutated {
+            Some(types.into())
+        } else {
+            None
+        }
+    }
+
+    fn mutate_option(&mut self, ty: Option<&Ty>, pol: bool) -> Option<Option<Ty>> {
+        match ty {
+            Some(ty) => self.mutate(ty, pol).map(Some),
+            None => None,
+        }
+    }
+
+    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);
+
+        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 })
+    }
+
+    fn mutate_record(&mut self, ty: &Interned<RecordTy>, pol: bool) -> Option<RecordTy> {
+        let types = self.mutate_vec(&ty.types, pol)?;
+
+        let rec = ty.as_ref().clone();
+        Some(RecordTy { types, ..rec })
+    }
+
+    fn mutate_with_sig(&mut self, ty: &Interned<SigWithTy>, pol: bool) -> Option<SigWithTy> {
+        let sig = self.mutate(ty.sig.as_ref(), pol);
+        let with = self.mutate_func(&ty.with, pol);
+
+        if sig.is_none() && with.is_none() {
+            return None;
+        }
+
+        let sig = sig.map(Interned::new).unwrap_or_else(|| ty.sig.clone());
+        let with = with.map(Interned::new).unwrap_or_else(|| ty.with.clone());
+
+        Some(SigWithTy { sig, with })
+    }
+
+    fn mutate_unary(&mut self, ty: &Interned<TypeUnary>, pol: bool) -> Option<TypeUnary> {
+        let lhs = self.mutate(ty.lhs.as_ref(), pol)?.into();
+
+        Some(TypeUnary { lhs, op: ty.op })
+    }
+
+    fn mutate_binary(&mut self, ty: &Interned<TypeBinary>, pol: bool) -> Option<TypeBinary> {
+        let (lhs, rhs) = &ty.operands;
+
+        let x = self.mutate(lhs, pol);
+        let y = self.mutate(rhs, pol);
+
+        if x.is_none() && y.is_none() {
+            return None;
+        }
+
+        let lhs = x.map(Interned::new).unwrap_or_else(|| lhs.clone());
+        let rhs = y.map(Interned::new).unwrap_or_else(|| rhs.clone());
+
+        Some(TypeBinary {
+            operands: (lhs, rhs),
+            op: ty.op,
+        })
+    }
+
+    fn mutate_if(&mut self, ty: &Interned<IfTy>, pol: bool) -> Option<IfTy> {
+        let cond = self.mutate(ty.cond.as_ref(), pol);
+        let then = self.mutate(ty.then.as_ref(), pol);
+        let else_ = self.mutate(ty.else_.as_ref(), pol);
+
+        if cond.is_none() && then.is_none() && else_.is_none() {
+            return None;
+        }
+
+        let cond = cond.map(Interned::new).unwrap_or_else(|| ty.cond.clone());
+        let then = then.map(Interned::new).unwrap_or_else(|| ty.then.clone());
+        let else_ = else_.map(Interned::new).unwrap_or_else(|| ty.else_.clone());
+
+        Some(IfTy { cond, then, else_ })
+    }
+
+    fn mutate_select(&mut self, ty: &Interned<SelectTy>, pol: bool) -> Option<SelectTy> {
+        let target = self.mutate(ty.ty.as_ref(), pol)?.into();
+
+        Some(SelectTy {
+            ty: target,
+            select: ty.select.clone(),
+        })
+    }
+}
+
+impl<T> MutateDriver for T
+where
+    T: FnMut(&Ty, bool) -> Option<Ty>,
+{
+    fn mutate(&mut self, ty: &Ty, pol: bool) -> Option<Ty> {
+        self(ty, pol)
+    }
+}
+
+impl Ty {
+    pub fn mutate(&self, pol: bool, checker: &mut impl MutateDriver) -> Option<Ty> {
+        let mut worker = Mutator;
+        worker.ty(self, pol, checker)
+    }
+}
+
+struct Mutator;
+
+impl Mutator {
+    fn ty(&mut self, ty: &Ty, pol: bool, mutator: &mut impl MutateDriver) -> Option<Ty> {
+        match ty {
+            Ty::Func(f) => {
+                let f = mutator.mutate_func(f, pol)?;
+                Some(Ty::Func(f.into()))
+            }
+            Ty::Dict(r) => {
+                let r = mutator.mutate_record(r, pol)?;
+                Some(Ty::Dict(r.into()))
+            }
+            Ty::Tuple(e) => {
+                let e = mutator.mutate_vec(e, pol)?;
+                Some(Ty::Tuple(e))
+            }
+            Ty::Array(e) => {
+                let ty = mutator.mutate(e, pol)?;
+                Some(Ty::Array(ty.into()))
+            }
+            Ty::With(w) => {
+                let w = mutator.mutate_with_sig(w, pol)?;
+                Some(Ty::With(w.into()))
+            }
+            Ty::Args(args) => {
+                let args = mutator.mutate_func(args, pol)?;
+                Some(Ty::Args(args.into()))
+            }
+            Ty::Unary(u) => {
+                let u = mutator.mutate_unary(u, pol)?;
+                Some(Ty::Unary(u.into()))
+            }
+            Ty::Binary(b) => {
+                let b = mutator.mutate_binary(b, pol)?;
+                Some(Ty::Binary(b.into()))
+            }
+            Ty::If(i) => {
+                let i = mutator.mutate_if(i, pol)?;
+                Some(Ty::If(i.into()))
+            }
+            Ty::Union(v) => {
+                let v = mutator.mutate_vec(v, pol)?;
+                Some(Ty::Union(v))
+            }
+            Ty::Field(f) => {
+                let field = f.field.mutate(pol, mutator)?;
+                let mut f = f.as_ref().clone();
+                f.field = field;
+                Some(Ty::Field(f.into()))
+            }
+            Ty::Select(s) => {
+                let s = mutator.mutate_select(s, pol)?;
+                Some(Ty::Select(s.into()))
+            }
+            Ty::Var(..)
+            | Ty::Let(..)
+            | Ty::Value(..)
+            | Ty::Clause
+            | Ty::Undef
+            | Ty::Content
+            | Ty::Any
+            | Ty::None
+            | Ty::Infer
+            | Ty::FlowNone
+            | Ty::Space
+            | Ty::Auto
+            | Ty::Boolean(..)
+            | Ty::Builtin(..) => mutator.mutate(ty, pol),
+        }
+    }
+}

crates/tinymist-query/src/ty/subst.rs

@@ -15,8 +15,11 @@ impl<'a> Sig<'a> {
             return body;
         }
 
+        let body = body?;
+
+        // Substitute the bound variables in the body or just body
         let mut checker = SubstituteChecker { bound_variables };
-        checker.ty(&body?, pol)
+        Some(checker.ty(&body, pol).unwrap_or(body))
     }
 
     pub fn check_bind(
@@ -26,11 +29,13 @@ impl<'a> Sig<'a> {
     ) -> Option<(HashMap<DefId, Ty>, Option<Ty>)> {
         let SigShape { sig, withs } = self.shape(ctx)?;
 
-        let has_free_vars = sig.has_free_variables;
+        // todo: check if the signature has free variables
+        // let has_free_vars = sig.has_free_variables;
+        let has_free_vars = true;
 
         let mut arguments = HashMap::new();
-        for (arg_recv, arg_ins) in sig.matches(args, withs) {
-            if has_free_vars {
+        if has_free_vars {
+            for (arg_recv, arg_ins) in sig.matches(args, withs) {
                 if let Ty::Var(arg_recv) = arg_recv {
                     arguments.insert(arg_recv.def, arg_ins.clone());
                 }
@@ -41,15 +46,100 @@ impl<'a> Sig<'a> {
     }
 }
 
-// todo
 struct SubstituteChecker {
     bound_variables: HashMap<DefId, Ty>,
 }
+
 impl SubstituteChecker {
     fn ty(&mut self, body: &Ty, pol: bool) -> Option<Ty> {
-        let _ = self.bound_variables;
-        let _ = pol;
-
-        Some(body.clone())
+        body.mutate(pol, self)
+    }
+}
+
+impl MutateDriver for SubstituteChecker {
+    fn mutate(&mut self, ty: &Ty, pol: bool) -> Option<Ty> {
+        // todo: extrude the type into a polarized type
+        let _ = pol;
+
+        Some(match ty {
+            // todo: substitute the bound in the type
+            Ty::Let(..) => return None,
+            Ty::Var(v) => {
+                if let Some(ty) = self.bound_variables.get(&v.def) {
+                    ty.clone()
+                } else {
+                    return None;
+                }
+            }
+            Ty::Value(..)
+            | Ty::Clause
+            | Ty::Undef
+            | Ty::Content
+            | Ty::Any
+            | Ty::None
+            | Ty::Infer
+            | Ty::FlowNone
+            | Ty::Space
+            | Ty::Auto
+            | Ty::Boolean(..)
+            | Ty::Builtin(..) => return None,
+            _ => return None,
+        })
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use insta::{assert_debug_snapshot, assert_snapshot};
+
+    use crate::ty::tests::*;
+
+    use super::{ApplyChecker, Ty};
+    #[test]
+    fn test_ty() {
+        use super::*;
+        let ty = Ty::Clause;
+        let ty_ref = TyRef::new(ty.clone());
+        assert_debug_snapshot!(ty_ref, @"Clause");
+    }
+
+    #[derive(Default)]
+    struct CallCollector(Vec<Ty>);
+
+    impl ApplyChecker for CallCollector {
+        fn call(
+            &mut self,
+            sig: super::Sig,
+            arguments: &crate::adt::interner::Interned<super::ArgsTy>,
+            pol: bool,
+        ) {
+            let ty = sig.call(arguments, pol, None);
+            if let Some(ty) = ty {
+                self.0.push(ty);
+            }
+        }
+    }
+
+    #[test]
+    fn test_sig_call() {
+        use super::*;
+
+        fn call(sig: Interned<SigTy>, args: Interned<SigTy>) -> String {
+            let sig_ty = Ty::Func(sig);
+            let mut collector = CallCollector::default();
+            sig_ty.call(&args, false, &mut collector);
+
+            collector.0.iter().fold(String::new(), |mut acc, ty| {
+                if !acc.is_empty() {
+                    acc.push_str(", ");
+                }
+
+                acc.push_str(&format!("{ty:?}"));
+                acc
+            })
+        }
+
+        assert_snapshot!(call(literal_sig!(p1 -> p1), literal_args!(q1)), @"@q1");
+        assert_snapshot!(call(literal_sig!(!u1: w1 -> w1), literal_args!(!u1: w2)), @"@w2");
     }
 }