From cb385a86e461e98c121d292102bd932cf4153aa1 Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Fri, 24 May 2024 19:08:36 +0900 Subject: [PATCH] chore: relax occur check fix #512 --- crates/els/inlay_hint.rs | 6 ++ crates/erg_compiler/context/unify.rs | 68 +++++++++++-------- .../erg_compiler/lib/pystd/os.d/__init__.d.er | 2 +- crates/erg_compiler/ty/constructors.rs | 14 ++++ crates/erg_compiler/ty/mod.rs | 7 +- tests/should_ok/iterator.er | 7 ++ 6 files changed, 73 insertions(+), 31 deletions(-) diff --git a/crates/els/inlay_hint.rs b/crates/els/inlay_hint.rs index f3fed4986..1ff043c35 100644 --- a/crates/els/inlay_hint.rs +++ b/crates/els/inlay_hint.rs @@ -2,6 +2,7 @@ use erg_common::spawn::safe_yield; use erg_compiler::erg_parser::parse::Parsable; +use erg_compiler::hir::GuardClause; use erg_compiler::varinfo::AbsLocation; use lsp_types::InlayHintLabelPart; use serde::Deserialize; @@ -154,6 +155,11 @@ impl<'s, C: BuildRunnable, P: Parsable> InlayHintGenerator<'s, C, P> { let hint = self.type_anot(ln_end, col_end, &d_param.sig.vi.t, false); result.push(hint); } + for guard in params.guards.iter() { + if let GuardClause::Bind(def) = guard { + result.extend(self.get_var_def_hint(def)); + } + } result } diff --git a/crates/erg_compiler/context/unify.rs b/crates/erg_compiler/context/unify.rs index b37828b56..39db7936f 100644 --- a/crates/erg_compiler/context/unify.rs +++ b/crates/erg_compiler/context/unify.rs @@ -66,9 +66,9 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { /// occur(X -> ?T, X -> ?T) ==> OK /// occur(?T, ?T -> X) ==> Error /// occur(?T, Option(?T)) ==> Error - /// occur(?T or ?U, ?T) ==> OK /// occur(?T or Int, Int or ?T) ==> OK /// occur(?T(<: Str) or ?U(<: Int), ?T(<: Str)) ==> Error + /// occur(?T(<: ?U or Y), ?U) ==> OK /// occur(?T, ?T.Output) ==> OK /// ``` fn occur(&self, maybe_sub: &Type, maybe_sup: &Type) -> TyCheckResult<()> { @@ -150,13 +150,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { Ok(()) }*/ (FreeVar(fv), Poly { params, .. }) if fv.is_unbound() => { - for param in params.iter().filter_map(|tp| { - if let TyParam::Type(t) = tp { - Some(t) - } else { - None - } - }) { + for param in params.iter().filter_map(|tp| <&Type>::try_from(tp).ok()) { self.occur_inner(maybe_sub, param)?; } Ok(()) @@ -192,15 +186,17 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { self.ctx.caused_by(), ))) } else { - if let Some((sub_t, sup_t)) = sub.get_subsup() { + if let Some((sub_t, _sup_t)) = sub.get_subsup() { sub.do_avoiding_recursion(|| { - self.occur_inner(&sub_t, maybe_sup)?; - self.occur_inner(&sup_t, maybe_sup) + // occur(?T(<: ?U or Y), ?U) ==> OK + self.occur_inner(&sub_t, maybe_sup) + // self.occur_inner(&sup_t, maybe_sup) })?; } - if let Some((sub_t, sup_t)) = sup.get_subsup() { + if let Some((_sub_t, sup_t)) = sup.get_subsup() { sup.do_avoiding_recursion(|| { - self.occur_inner(maybe_sub, &sub_t)?; + // occur(?U, ?T(:> ?U or Y)) ==> OK + // self.occur_inner(maybe_sub, &sub_t)?; self.occur_inner(maybe_sub, &sup_t) })?; } @@ -259,25 +255,13 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { Ok(()) } (Poly { params, .. }, FreeVar(fv)) if fv.is_unbound() => { - for param in params.iter().filter_map(|tp| { - if let TyParam::Type(t) = tp { - Some(t) - } else { - None - } - }) { + for param in params.iter().filter_map(|tp| <&Type>::try_from(tp).ok()) { self.occur_inner(param, maybe_sup)?; } Ok(()) } (FreeVar(fv), Poly { params, .. }) if fv.is_unbound() => { - for param in params.iter().filter_map(|tp| { - if let TyParam::Type(t) = tp { - Some(t) - } else { - None - } - }) { + for param in params.iter().filter_map(|tp| <&Type>::try_from(tp).ok()) { self.occur_inner(maybe_sub, param)?; } Ok(()) @@ -1957,3 +1941,33 @@ impl Context { unifier.unify(lhs, rhs) } } + +#[cfg(test)] +mod test { + use crate::context::unify::{mono_q, subtypeof, type_q}; + use crate::fn_t; + + use super::Type; + use Type::*; + + #[test] + fn test_occur() { + let ctx = super::Context::default(); + let unifier = super::Unifier::new(&ctx, &(), None, false, None); + + assert!(unifier.occur(&Type, &Type).is_ok()); + let t = type_q("T"); + assert!(unifier.occur(&t, &t).is_ok()); + let or_t = t.clone() | Type; + let or2_t = Type | t.clone(); + assert!(unifier.occur(&Int, &(Int | Str)).is_ok()); + assert!(unifier.occur(&t, &or_t).is_err()); + assert!(unifier.occur(&or_t, &or2_t).is_ok()); + let subr_t = fn_t!(Type => t.clone()); + assert!(unifier.occur(&t, &subr_t).is_err()); + assert!(unifier.occur(&subr_t, &subr_t).is_ok()); + + let u = mono_q("U", subtypeof(t.clone() | Int)); + assert!(unifier.occur(&u, &t).is_ok()); + } +} diff --git a/crates/erg_compiler/lib/pystd/os.d/__init__.d.er b/crates/erg_compiler/lib/pystd/os.d/__init__.d.er index f14e53ac2..b10c258ca 100644 --- a/crates/erg_compiler/lib/pystd/os.d/__init__.d.er +++ b/crates/erg_compiler/lib/pystd/os.d/__init__.d.er @@ -422,6 +422,6 @@ The name of the operating system dependent module imported. The following names topdown := Bool, onerror := Subroutine, followlinks := Bool -) => Iterator [Str, [Str; _], [Str; _]] +) => Iterator((Str, [Str; _], [Str; _]),) .write!: (fd: Nat or FileDescriptor, str: Bytes) => Nat .writev!: (fd: Nat or FileDescriptor, buffers: Ref(ByteArray!)) => Nat diff --git a/crates/erg_compiler/ty/constructors.rs b/crates/erg_compiler/ty/constructors.rs index 37e5350e0..8043d291e 100644 --- a/crates/erg_compiler/ty/constructors.rs +++ b/crates/erg_compiler/ty/constructors.rs @@ -5,6 +5,20 @@ use erg_common::fresh::FRESH_GEN; use crate::ty::*; +#[macro_export] +macro_rules! fn_t { + ($input: expr => $ret: expr) => { + Type::Subr($crate::ty::SubrType::new( + $crate::ty::SubrKind::Func, + vec![$crate::ty::ParamTy::Pos($input)], + None, + vec![], + None, + $ret, + )) + }; +} + #[inline] pub fn pos(ty: Type) -> ParamTy { ParamTy::Pos(ty) diff --git a/crates/erg_compiler/ty/mod.rs b/crates/erg_compiler/ty/mod.rs index 13157892c..2d541c6a9 100644 --- a/crates/erg_compiler/ty/mod.rs +++ b/crates/erg_compiler/ty/mod.rs @@ -3637,10 +3637,11 @@ impl Type { let constraint = Constraint::new_sandwiched(sub.derefine(), sup.derefine()); Self::FreeVar(Free::new_named_unbound(name, level, constraint)) }) - } else { - let t = fv.get_type().unwrap().derefine(); - let constraint = Constraint::new_type_of(t); + } else if let Some(t) = fv.get_type() { + let constraint = Constraint::new_type_of(t.derefine()); Self::FreeVar(Free::new_named_unbound(name, level, constraint)) + } else { + Self::FreeVar(fv.clone()) } } Self::Refinement(refine) => refine.t.as_ref().clone(), diff --git a/tests/should_ok/iterator.er b/tests/should_ok/iterator.er index 97aff01f9..27fa72226 100644 --- a/tests/should_ok/iterator.er +++ b/tests/should_ok/iterator.er @@ -6,3 +6,10 @@ for! filter(x -> x > 1, 0..3), i => assert i > 1 for! map(x -> "\{x}", [1, 2, 3]), s => assert str(s) == s + +for! enumerate([["aaa"], ["aaaa"]]), ((_, a),) => + print! a.filter(s -> "a" in s) + +os = pyimport "os" +for! os.walk!("assets"), ((path, dirs, files),) => + print! files.filter(i -> i != "a").to_list()