Update random.d.er

compiler/erg_compiler/context/instantiate.rs

@@ -947,8 +947,13 @@ impl Context {
                         )?),
                         _ => unreachable!(),
                     };
-                let tv = named_free_var(lhs.inspect().clone(), self.level, constr);
+                if constr.get_sub_sup().is_none() {
-                tv_cache.push_or_init_tyvar(lhs.inspect(), &tv);
+                    let tp = TyParam::named_free_var(lhs.inspect().clone(), self.level, constr);
+                    tv_cache.push_or_init_typaram(lhs.inspect(), &tp);
+                } else {
+                    let tv = named_free_var(lhs.inspect().clone(), self.level, constr);
+                    tv_cache.push_or_init_tyvar(lhs.inspect(), &tv);
+                }
                 Ok(())
             }
             TypeBoundSpec::WithDefault { .. } => type_feature_error!(

compiler/erg_compiler/context/tyvar.rs

@@ -248,6 +248,21 @@ impl Context {
                 let rhs = self.generalize_tp(rhs, variance);
                 Predicate::ne(lhs, rhs)
             }
+            Predicate::And(lhs, rhs) => {
+                let lhs = self.generalize_pred(*lhs, variance);
+                let rhs = self.generalize_pred(*rhs, variance);
+                Predicate::and(lhs, rhs)
+            }
+            Predicate::Or(lhs, rhs) => {
+                let lhs = self.generalize_pred(*lhs, variance);
+                let rhs = self.generalize_pred(*rhs, variance);
+                Predicate::or(lhs, rhs)
+            }
+            Predicate::Not(lhs, rhs) => {
+                let lhs = self.generalize_pred(*lhs, variance);
+                let rhs = self.generalize_pred(*rhs, variance);
+                Predicate::not(lhs, rhs)
+            }
             other => todo!("{other}"),
         }
     }

compiler/erg_compiler/lib/pystd/random.d.er

@@ -1,3 +1,14 @@
 .seed!: (a := Num, version := Int) => NoneType
+.randbytes!: (n: Nat) => Bytes
+.randrange!: (start: Int, stop := Int, step := Int) => Int
 .randint!: (a: Int, b: Int) => Int
+.getrandbits!: (k: Nat) => Nat
 .choice!: |T: Type, S <: Seq(T)|(seq: S) => T
+# TODO: dependent length array type
+.choices!: |T: Type, S <: Seq(T)|(population: S, weights := [Nat; _] or NoneType, k := Nat) => [T; _]
+# TODO: Seq!
+.shuffle!: |T: Type, S <: Seq(T)|(seq: S) => NoneType
+.sample!: |T: Type, S <: Seq(T)|(population: S, k := Nat) => [T; _]
+.random!: () => 0.0..1.0 # TODO: <1.0
+.dep_uniform! = 'uniform': |A: Int, B: Int|(a: {A}, b: {B}) => A..B
+.uniform!: (a: Int, b: Int) => Int

compiler/erg_compiler/ty/mod.rs

@@ -339,7 +339,9 @@ impl HasLevel for Predicate {
             | Self::GreaterEqual { rhs, .. }
             | Self::LessEqual { rhs, .. }
             | Self::NotEqual { rhs, .. } => rhs.level(),
-            Self::And(_lhs, _rhs) | Self::Or(_lhs, _rhs) | Self::Not(_lhs, _rhs) => todo!(),
+            Self::And(lhs, rhs) | Self::Or(lhs, rhs) | Self::Not(lhs, rhs) => {
+                lhs.level().zip(rhs.level()).map(|(a, b)| a.min(b))
+            }
         }
     }
 
@@ -825,7 +827,11 @@ impl LimitedDisplay for RefinementType {
                 let (_, rhs) = enum_unwrap!(pred, Predicate::Equal { lhs, rhs });
                 write!(f, "{}, ", rhs)?;
             }
-            write!(f, "}}")
+            write!(f, "}}")?;
+            if cfg!(feature = "debug") {
+                write!(f, "(<: {})", self.t)?;
+            }
+            Ok(())
         } else {
             write!(f, "{{{}: ", self.var)?;
             self.t.limited_fmt(f, limit - 1)?;