fix: overload subtyping

This commit is contained in:
Shunsuke Shibayama 2023-06-01 19:36:25 +09:00
parent ef3bb68044
commit 1d0657c544
3 changed files with 16 additions and 1 deletions

View file

@ -1255,6 +1255,8 @@ impl Context {
}, },
(_, Not(r)) => self.diff(lhs, r), (_, Not(r)) => self.diff(lhs, r),
(Not(l), _) => self.diff(rhs, l), (Not(l), _) => self.diff(rhs, l),
// overloading
(l, r) if l.is_subr() && r.is_subr() => and(lhs.clone(), rhs.clone()),
_ => self.simple_intersection(lhs, rhs), _ => self.simple_intersection(lhs, rhs),
} }
} }

View file

@ -49,7 +49,18 @@ impl ASTLowerer {
_ => sig.inspect().cloned(), _ => sig.inspect().cloned(),
}; };
let found_body_t = chunk.ref_t(); let found_body_t = chunk.ref_t();
let ast::VarPattern::Ident(ident) = &sig.pat else { unreachable!() }; let ident = match &sig.pat {
ast::VarPattern::Ident(ident) => ident,
ast::VarPattern::Discard(token) => {
return Err(LowerErrors::from(LowerError::declare_error(
self.cfg().input.clone(),
line!() as usize,
token.loc(),
self.module.context.caused_by(),
)));
}
_ => unreachable!(),
};
let id = body.id; let id = body.id;
if let Some(spec_t) = opt_spec_t { if let Some(spec_t) = opt_spec_t {
self.module self.module

View file

@ -1814,6 +1814,7 @@ impl Type {
Self::Subr(_) => true, Self::Subr(_) => true,
Self::Quantified(quant) => quant.is_subr(), Self::Quantified(quant) => quant.is_subr(),
Self::Refinement(refine) => refine.t.is_subr(), Self::Refinement(refine) => refine.t.is_subr(),
Self::And(l, r) => l.is_subr() && r.is_subr(),
_ => false, _ => false,
} }
} }
@ -1823,6 +1824,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_quantified_subr(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_quantified_subr(),
Self::Quantified(_) => true, Self::Quantified(_) => true,
Self::Refinement(refine) => refine.t.is_quantified_subr(), Self::Refinement(refine) => refine.t.is_quantified_subr(),
Self::And(l, r) => l.is_quantified_subr() && r.is_quantified_subr(),
_ => false, _ => false,
} }
} }