fix: refinement type bug

crates/erg_compiler/context/eval.rs

@@ -1687,8 +1687,8 @@ impl Context {
         lhs: TyParam,
         rhs: TyParam,
     ) -> EvalResult<TyParam> {
-        let lhs = self.eval_tp(lhs).map_err(|(_, es)| es)?;
-        let rhs = self.eval_tp(rhs).map_err(|(_, es)| es)?;
+        // let lhs = self.eval_tp(lhs).map_err(|(_, es)| es)?;
+        // let rhs = self.eval_tp(rhs).map_err(|(_, es)| es)?;
         match (lhs, rhs) {
             (TyParam::Value(lhs), TyParam::Value(rhs)) => {
                 self.eval_bin(op, lhs, rhs).map(TyParam::value)
@@ -1807,7 +1807,7 @@ impl Context {
 
     /// val: may be unevaluated
     pub(crate) fn eval_unary_tp(&self, op: OpKind, val: TyParam) -> EvalResult<TyParam> {
-        let val = self.eval_tp(val).map_err(|(_, es)| es)?;
+        // let val = self.eval_tp(val).map_err(|(_, es)| es)?;
         match val {
             TyParam::Value(c) => self.eval_unary_val(op, c).map(TyParam::Value),
             TyParam::FreeVar(fv) if fv.is_linked() => {
@@ -1824,9 +1824,9 @@ impl Context {
 
     /// args: may be unevaluated
     pub(crate) fn eval_app(&self, name: Str, args: Vec<TyParam>) -> Failable<TyParam> {
-        let args = self
-            .eval_type_args(args)
-            .map_err(|(args, es)| (TyParam::app(name.clone(), args), es))?;
+        /*let args = self
+        .eval_type_args(args)
+        .map_err(|(args, es)| (TyParam::app(name.clone(), args), es))?;*/
         if let Ok(value_args) = args
             .iter()
             .map(|tp| self.convert_tp_into_value(tp.clone()))

tests/should_ok/dependent_refinement.er

@@ -0,0 +1,13 @@
+ndarray = pyimport "ndarray"
+
+a as ndarray.NDArray(Int, [2, 3]) = todo()
+
+check|T, Shape: {A: [Nat; _] | all(map((X -> X > 1), A))}|(
+    _: ndarray.NDArray(T, Shape)
+) = None
+check a
+
+check2|T, Shape: [Nat; _]|(
+    _: {_: ndarray.NDArray(T, Shape) | all(map((X -> X > 1), Shape))}
+) = None
+check2 a

tests/should_ok/ndarray.d.er

@@ -0,0 +1,3 @@
+.NDArray: (T: Type, Shape: [Nat; _]) -> ClassType
+.NDArray(T, _) <: Output T
+.NDArray(_, _) <: Num

tests/test.rs

@@ -126,6 +126,11 @@ fn exec_dependent() -> Result<(), ()> {
     expect_success("tests/should_ok/dependent.er", 0)
 }
 
+#[test]
+fn exec_dependent_refinement() -> Result<(), ()> {
+    expect_compile_success("tests/should_ok/dependent_refinement.er", 0)
+}
+
 #[test]
 fn exec_dict() -> Result<(), ()> {
     expect_success("examples/dict.er", 0)