feat: add Dimension and unit module

crates/erg_compiler/codegen.rs

@@ -2716,7 +2716,7 @@ impl PyCodeGenerator {
                 Expr::Accessor(Accessor::Ident(ident)) if ident.vis().is_private() => {
                     self.emit_call_local(ident, call.args)
                 }
-                other if other.ref_t().is_poly_type_meta() => {
+                other if other.ref_t().is_poly_meta_type() => {
                     self.emit_expr(other);
                     self.emit_index_args(call.args);
                 }
@@ -2754,7 +2754,7 @@ impl PyCodeGenerator {
                 self.emit_load_name_instr(Identifier::private("#sum"));
                 self.emit_args_311(args, Name);
             }
-            other if local.ref_t().is_poly_type_meta() && other != "classof" => {
+            other if local.ref_t().is_poly_meta_type() && other != "classof" => {
                 if self.py_version.minor <= Some(9) {
                     self.load_fake_generic();
                     self.emit_load_name_instr(Identifier::private("#FakeGenericAlias"));
@@ -2798,7 +2798,7 @@ impl PyCodeGenerator {
         if let Some(func_name) = debind(&method_name) {
             return self.emit_call_fake_method(obj, func_name, method_name, args);
         }
-        let is_type = method_name.ref_t().is_poly_type_meta();
+        let is_type = method_name.ref_t().is_poly_meta_type();
         let kind = if self.py_version.minor >= Some(11) || method_name.vi.t.is_method() {
             BoundAttr
         } else {

crates/erg_compiler/context/compare.rs

@@ -1154,12 +1154,15 @@ impl Context {
                         Type::Obj
                     }
                 };
+                /*
                 if variance == Variance::Contravariant {
                     self.subtype_of(&fv_t, &sub_t)
                 } else {
                     // REVIEW: covariant, invariant
                     self.supertype_of(&fv_t, &sub_t)
                 }
+                */
+                self.subtype_of(&sub_t, &fv_t) || self.supertype_of(&sub_t, &fv_t)
             }
             (_, TyParam::FreeVar(fv)) if fv.is_unbound() => {
                 let Some(fv_t) = fv.get_type() else {
@@ -1172,14 +1175,18 @@ impl Context {
                         Type::Obj
                     }
                 };
+                /*
                 if variance == Variance::Contravariant {
                     self.subtype_of(&sup_t, &fv_t)
                 } else {
                     // REVIEW: covariant, invariant
                     self.supertype_of(&sup_t, &fv_t)
                 }
+                */
+                self.subtype_of(&sup_t, &fv_t) || self.supertype_of(&sup_t, &fv_t)
             }
             (TyParam::Value(sup), _) => {
+                // Value([Value(1)]) => TyParam([Value(1)])
                 if let Ok(sup) = Self::convert_value_into_tp(sup.clone()) {
                     self.supertype_of_tp(&sup, sub_p, variance)
                 } else {
@@ -1408,6 +1415,7 @@ impl Context {
     /// union(?T(<: Str), ?U(<: Int)) == ?T or ?U
     /// union(List(Int, 2), List(Str, 2)) == List(Int or Str, 2)
     /// union(List(Int, 2), List(Str, 3)) == List(Int, 2) or List(Int, 3)
+    /// union(List(Int, 2), List(Int, ?N)) == List(Int, ?N)
     /// union({ .a = Int }, { .a = Str }) == { .a = Int or Str }
     /// union({ .a = Int }, { .a = Int; .b = Int }) == { .a = Int } or { .a = Int; .b = Int } # not to lost `b` information
     /// union((A and B) or C) == (A or C) and (B or C)

crates/erg_compiler/context/initialize/classes.rs

@@ -4055,6 +4055,161 @@ impl Context {
             Immutable,
             Visibility::BUILTIN_PRIVATE,
         );
+        // TODO: non-builtin
+        /* Dimension */
+        let Ty = type_q("Ty");
+        let M = mono_q_tp("M", instanceof(Int));
+        let L = mono_q_tp("L", instanceof(Int));
+        let Time = mono_q_tp("T", instanceof(Int));
+        let I = mono_q_tp("I", instanceof(Int));
+        let Temp = mono_q_tp("Θ", instanceof(Int));
+        let N = mono_q_tp("N", instanceof(Int));
+        let J = mono_q_tp("J", instanceof(Int));
+        let M2 = mono_q_tp("M2", instanceof(Int));
+        let L2 = mono_q_tp("L2", instanceof(Int));
+        let Time2 = mono_q_tp("T2", instanceof(Int));
+        let I2 = mono_q_tp("I2", instanceof(Int));
+        let Temp2 = mono_q_tp("Θ2", instanceof(Int));
+        let N2 = mono_q_tp("N2", instanceof(Int));
+        let J2 = mono_q_tp("J2", instanceof(Int));
+        let dimension_t = poly(
+            DIMENSION,
+            vec![
+                ty_tp(Ty.clone()),
+                M.clone(),
+                L.clone(),
+                Time.clone(),
+                I.clone(),
+                Temp.clone(),
+                N.clone(),
+                J.clone(),
+            ],
+        );
+        let dimension2_t = poly(
+            DIMENSION,
+            vec![
+                ty_tp(Ty.clone()),
+                M2.clone(),
+                L2.clone(),
+                Time2.clone(),
+                I2.clone(),
+                Temp2.clone(),
+                N2.clone(),
+                J2.clone(),
+            ],
+        );
+        let params = vec![
+            PS::t_nd("Ty"),
+            PS::named_nd("M", Int),
+            PS::named_nd("L", Int),
+            PS::named_nd("T", Int),
+            PS::named_nd("I", Int),
+            PS::named_nd("Θ", Int),
+            PS::named_nd("N", Int),
+            PS::named_nd("J", Int),
+        ];
+        let mut dimension = Self::builtin_poly_class(DIMENSION, params, 10);
+        dimension
+            .register_trait(self, poly(OUTPUT, vec![ty_tp(Ty.clone())]))
+            .unwrap();
+        let value_t = fn0_met(dimension_t.clone(), Ty.clone()).quantify();
+        dimension.register_builtin_erg_impl(
+            FUNC_VALUE,
+            value_t,
+            Immutable,
+            Visibility::BUILTIN_PUBLIC,
+        );
+        let mut dimension_add =
+            Self::builtin_methods(Some(poly(ADD, vec![ty_tp(dimension_t.clone())])), 2);
+        let t = fn1_met(
+            dimension_t.clone(),
+            dimension_t.clone(),
+            dimension_t.clone(),
+        )
+        .quantify();
+        dimension_add.register_builtin_erg_impl(OP_ADD, t, Immutable, Visibility::BUILTIN_PUBLIC);
+        let out_t = dimension_t.clone();
+        dimension_add.register_builtin_const(
+            OUTPUT,
+            Visibility::BUILTIN_PUBLIC,
+            None,
+            ValueObj::builtin_class(out_t.clone()),
+        );
+        dimension.register_trait_methods(dimension_t.clone(), dimension_add);
+        let mut dimension_sub =
+            Self::builtin_methods(Some(poly(SUB, vec![ty_tp(dimension_t.clone())])), 2);
+        let t = fn1_met(
+            dimension_t.clone(),
+            dimension_t.clone(),
+            dimension_t.clone(),
+        )
+        .quantify();
+        dimension_sub.register_builtin_erg_impl(OP_SUB, t, Immutable, Visibility::BUILTIN_PUBLIC);
+        dimension_sub.register_builtin_const(
+            OUTPUT,
+            Visibility::BUILTIN_PUBLIC,
+            None,
+            ValueObj::builtin_class(out_t),
+        );
+        dimension.register_trait_methods(dimension_t.clone(), dimension_sub);
+        let mut dimension_mul =
+            Self::builtin_methods(Some(poly(MUL, vec![ty_tp(dimension2_t.clone())])), 2);
+        let dimension_added_t = poly(
+            DIMENSION,
+            vec![
+                ty_tp(Ty.clone()),
+                M.clone() + M2.clone(),
+                L.clone() + L2.clone(),
+                Time.clone() + Time2.clone(),
+                I.clone() + I2.clone(),
+                Temp.clone() + Temp2.clone(),
+                N.clone() + N2.clone(),
+                J.clone() + J2.clone(),
+            ],
+        );
+        let t = fn1_met(
+            dimension_t.clone(),
+            dimension2_t.clone(),
+            dimension_added_t.clone(),
+        )
+        .quantify();
+        dimension_mul.register_builtin_erg_impl(OP_MUL, t, Immutable, Visibility::BUILTIN_PUBLIC);
+        dimension_mul.register_builtin_const(
+            OUTPUT,
+            Visibility::BUILTIN_PUBLIC,
+            None,
+            ValueObj::builtin_class(dimension_added_t),
+        );
+        dimension.register_trait_methods(dimension_t.clone(), dimension_mul);
+        let mut dimension_div =
+            Self::builtin_methods(Some(poly(DIV, vec![ty_tp(dimension2_t.clone())])), 2);
+        let dimension_subtracted_t = poly(
+            DIMENSION,
+            vec![
+                ty_tp(Ty.clone()),
+                M.clone() - M2.clone(),
+                L.clone() - L2.clone(),
+                Time.clone() - Time2.clone(),
+                I.clone() - I2.clone(),
+                Temp.clone() - Temp2.clone(),
+                N.clone() - N2.clone(),
+                J.clone() - J2.clone(),
+            ],
+        );
+        let t = fn1_met(
+            dimension_t.clone(),
+            dimension2_t.clone(),
+            dimension_subtracted_t.clone(),
+        )
+        .quantify();
+        dimension_div.register_builtin_erg_impl(OP_DIV, t, Immutable, Visibility::BUILTIN_PUBLIC);
+        dimension_div.register_builtin_const(
+            OUTPUT,
+            Visibility::BUILTIN_PUBLIC,
+            None,
+            ValueObj::builtin_class(dimension_subtracted_t),
+        );
+        dimension.register_trait_methods(dimension_t.clone(), dimension_div);
         let mut base_exception = Self::builtin_mono_class(BASE_EXCEPTION, 2);
         base_exception.register_superclass(Obj, &obj);
         base_exception.register_builtin_erg_impl(
@@ -4472,6 +4627,7 @@ impl Context {
             Const,
             Some(GENERATOR),
         );
+        self.register_builtin_type(dimension_t, dimension, vis.clone(), Const, Some(DIMENSION));
         self.register_builtin_type(
             mono(BASE_EXCEPTION),
             base_exception,

crates/erg_compiler/context/initialize/mod.rs

@@ -403,6 +403,8 @@ const FUNC_TO_LIST: &str = "to_list";
 const FILE: &str = "File";
 const CALLABLE: &str = "Callable";
 const GENERATOR: &str = "Generator";
+const DIMENSION: &str = "Dimension";
+const FUNC_VALUE: &str = "value";
 const BASE_EXCEPTION: &str = "BaseException";
 const ATTR_ARGS: &str = "args";
 const FUNC_WITH_TRACEBACK: &str = "with_traceback";

crates/erg_compiler/context/inquire.rs

@@ -2689,6 +2689,7 @@ impl Context {
             fmt_slice(pos_args),
             fmt_slice(kw_args)
         );
+        debug_assert!(instance.has_no_qvar(), "{instance} has qvar");
         let instance = match self
             .substitute_call(
                 obj,
@@ -2717,6 +2718,7 @@ impl Context {
             "{instance} is quantified subr"
         );
         log!(info "Substituted:\ninstance: {instance}");
+        debug_assert!(instance.has_no_qvar(), "{instance} has qvar");
         let res = self
             .eval_t_params(instance, self.level, obj)
             .map_err(|(t, errs)| {

crates/erg_compiler/context/unify.rs

@@ -12,6 +12,7 @@ use erg_common::Str;
 use erg_common::{fmt_vec, fn_name, log};
 
 use crate::context::eval::Substituter;
+use crate::context::instantiate::TyVarCache;
 use crate::ty::constructors::*;
 use crate::ty::free::{Constraint, FreeKind, HasLevel, GENERIC_LEVEL};
 use crate::ty::typaram::{OpKind, TyParam};
@@ -1377,6 +1378,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
                 // * sub_unify({0},   ?T(:> {1},   <: Nat)): (?T(:> {0, 1}, <: Nat))
                 // * sub_unify(Bool,  ?T(<: Bool or Y)): (?T == Bool)
                 // * sub_unify(Float, ?T(<: Structural{ .imag = ?U })) ==> ?U == Float
+                // * sub_unify(K(Int, 1), ?T(:> K(?A, ?N))) ==> ?A(:> Int), ?N == 1
                 if let Type::Refinement(refine) = maybe_sub {
                     if refine.t.addr_eq(maybe_sup) {
                         return Ok(());
@@ -1386,7 +1388,18 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
                     if sup.is_structural() || !sup.is_recursive() {
                         self.sub_unify(maybe_sub, &sup)?;
                     }
-                    let new_sub = self.ctx.union(maybe_sub, &sub);
+                    let mut new_sub = self.ctx.union(maybe_sub, &sub);
+                    if maybe_sub.qual_name() == sub.qual_name() && new_sub.has_unbound_var() {
+                        let list = UndoableLinkedList::new();
+                        if self
+                            .ctx
+                            .undoable_sub_unify(maybe_sub, &sub, &(), &list, None)
+                            .is_ok()
+                        {
+                            drop(list);
+                            self.sub_unify(maybe_sub, &sub)?;
+                        }
+                    }
                     // Expanding to an Or-type is prohibited by default
                     // This increases the quality of error reporting
                     // (Try commenting out this part and run tests/should_err/subtyping.er to see the error report changes on lines 29-30)
@@ -1397,6 +1410,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
                         let unified = self.unify(&l, &r);
                         if let Some(unified) = unified {
                             log!("unify({l}, {r}) == {unified}");
+                            new_sub = unified;
                         } else {
                             let maybe_sub = self.ctx.readable_type(maybe_sub.clone());
                             let new_sub = self.ctx.readable_type(new_sub);
@@ -1987,6 +2001,8 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
     /// unify(Eq, Int) == None
     /// unify(Int or Str, Int) == Some(Int or Str)
     /// unify(Int or Str, NoneType) == None
+    /// unify(K(1), K(2)) == None
+    /// unify(Int, ?U(<: Int) and ?T(<: Int)) == Some(?U and ?T)
     /// ```
     fn unify(&self, lhs: &Type, rhs: &Type) -> Option<Type> {
         match (lhs, rhs) {
@@ -2006,6 +2022,19 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
                     return None;
                 }
             }
+            (And(tys), other) | (other, And(tys)) => {
+                let mut unified = Obj;
+                for ty in tys {
+                    if let Some(t) = self.unify(ty, other) {
+                        unified = self.ctx.intersection(&unified, &t);
+                    }
+                }
+                if unified != Obj && unified != Never {
+                    return Some(unified);
+                } else {
+                    return None;
+                }
+            }
             (FreeVar(fv), _) if fv.is_linked() => return self.unify(&fv.crack(), rhs),
             (_, FreeVar(fv)) if fv.is_linked() => return self.unify(lhs, &fv.crack()),
             // TODO: unify(?T, ?U) ?
@@ -2035,6 +2064,20 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
                 if r_sup == Obj || self.ctx.is_trait(&r_sup) {
                     continue;
                 }
+                let Ok(l_substituter) = Substituter::substitute_typarams(self.ctx, &l_sup, lhs)
+                else {
+                    continue;
+                };
+                let mut tv_cache = TyVarCache::new(self.ctx.level, self.ctx);
+                let l_sup = self.ctx.detach(l_sup.clone(), &mut tv_cache);
+                drop(l_substituter);
+                let Ok(r_substituter) = Substituter::substitute_typarams(self.ctx, &r_sup, rhs)
+                else {
+                    continue;
+                };
+                let mut tv_cache = TyVarCache::new(self.ctx.level, self.ctx);
+                let r_sup = self.ctx.detach(r_sup.clone(), &mut tv_cache);
+                drop(r_substituter);
                 if let Some(t) = self.ctx.max(&l_sup, &r_sup).either() {
                     return Some(t.clone());
                 }

crates/erg_compiler/lib/core/_erg_std_prelude.py

@@ -24,3 +24,37 @@
 
 class Never:
     pass
+
+from typing import Generic, TypeVar
+
+Ty = TypeVar('Ty')
+M = TypeVar('M', bound=int)
+L = TypeVar("L", bound=int)
+T = TypeVar("T", bound=int)
+I = TypeVar("I", bound=int)
+Θ = TypeVar("Θ", bound=int)
+N = TypeVar("N", bound=int)
+J = TypeVar("J", bound=int)
+class Dimension(float, Generic[Ty, M, L, T, I, Θ, N, J]):
+    def value(self) -> float:
+        return float(self)
+    def __str__(self):
+        return f"Dimension({float(self)})"
+    def __add__(self, other):
+        return Dimension(float(self) + other)
+    def __sub__(self, other):
+        return Dimension(float(self) - other)
+    def __mul__(self, other):
+        return Dimension(float(self) * other)
+    def __rmul__(self, other):
+        return Dimension(other * float(self))
+    def __truediv__(self, other):
+        return Dimension(float(self) / other)
+    def __floordiv__(self, other):
+        return Dimension(float(self) // other)
+    def __rtruediv__(self, other):
+        return Dimension(other / float(self))
+    def __rfloordiv__(self, other):
+        return Dimension(other // float(self))
+    def type_check(self, t: type) -> bool:
+        return t.__name__ == "Dimension"