Fix sub_unify with class&trait

This commit is contained in:
Shunsuke Shibayama 2022-10-12 18:32:24 +09:00
parent 57da071ba8
commit 08e501f103
9 changed files with 60 additions and 39 deletions

View file

@ -20,7 +20,7 @@ use Type::*;
use crate::context::cache::{SubtypePair, GLOBAL_TYPE_CACHE};
use crate::context::eval::SubstContext;
use crate::context::instantiate::TyVarContext;
use crate::context::instantiate::TyVarInstContext;
use crate::context::{Context, TraitInstance, Variance};
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@ -619,8 +619,8 @@ impl Context {
}
(Quantified(l), Quantified(r)) => {
// REVIEW: maybe this should be `unreachable`
let l_tv_ctx = TyVarContext::new(self.level, l.bounds.clone(), self);
let r_tv_ctx = TyVarContext::new(self.level, r.bounds.clone(), self);
let l_tv_ctx = TyVarInstContext::new(self.level, l.bounds.clone(), self);
let r_tv_ctx = TyVarInstContext::new(self.level, r.bounds.clone(), self);
let l_callable = self
.instantiate_t(
l.unbound_callable.as_ref().clone(),
@ -639,7 +639,7 @@ impl Context {
}
(Quantified(q), r) => {
// REVIEW: maybe this should be `unreachable`
let tmp_tv_ctx = TyVarContext::new(self.level, q.bounds.clone(), self);
let tmp_tv_ctx = TyVarInstContext::new(self.level, q.bounds.clone(), self);
let q_callable = self
.instantiate_t(
q.unbound_callable.as_ref().clone(),

View file

@ -24,7 +24,7 @@ use crate::ty::typaram::{OpKind, TyParam};
use crate::ty::value::ValueObj;
use crate::ty::{ConstSubr, HasType, Predicate, SubrKind, TyBound, Type, UserConstSubr, ValueArgs};
use crate::context::instantiate::TyVarContext;
use crate::context::instantiate::TyVarInstContext;
use crate::context::{ClassDefType, Context, ContextKind, RegistrationMode};
use crate::error::{EvalError, EvalErrors, EvalResult, SingleEvalResult, TyCheckResult};
@ -172,7 +172,7 @@ impl<'c> SubstContext<'c> {
}
pub fn substitute(&self, quant_t: Type) -> TyCheckResult<Type> {
let tv_ctx = TyVarContext::new(self.ctx.level, self.bounds.clone(), self.ctx);
let tv_ctx = TyVarInstContext::new(self.ctx.level, self.bounds.clone(), self.ctx);
let inst = self.ctx.instantiate_t(quant_t, &tv_ctx, self.loc)?;
for param in inst.typarams() {
self.substitute_tp(&param)?;
@ -425,7 +425,7 @@ impl Context {
Signature::Subr(subr) => {
let bounds =
self.instantiate_ty_bounds(&subr.bounds, RegistrationMode::Normal)?;
Some(TyVarContext::new(self.level, bounds, self))
Some(TyVarInstContext::new(self.level, bounds, self))
}
Signature::Var(_) => None,
};
@ -507,7 +507,7 @@ impl Context {
/// FIXME: grow
fn eval_const_lambda(&self, lambda: &Lambda) -> EvalResult<ValueObj> {
let bounds = self.instantiate_ty_bounds(&lambda.sig.bounds, RegistrationMode::Normal)?;
let tv_ctx = TyVarContext::new(self.level, bounds, self);
let tv_ctx = TyVarInstContext::new(self.level, bounds, self);
let mut non_default_params = Vec::with_capacity(lambda.sig.params.non_defaults.len());
for sig in lambda.sig.params.non_defaults.iter() {
let pt =

View file

@ -1397,6 +1397,11 @@ impl Context {
Some(vec![ctx].into_iter().chain(sups))
}
pub(crate) fn _get_super_traits(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
self.get_nominal_type_ctx(typ)
.map(|ctx| ctx.super_traits.clone().into_iter())
}
/// if `typ` is a refinement type, include the base type (refine.t)
pub(crate) fn get_super_classes(&self, typ: &Type) -> Option<impl Iterator<Item = Type>> {
self.get_nominal_type_ctx(typ).map(|ctx| {

View file

@ -33,23 +33,23 @@ use RegistrationMode::*;
/// Context for instantiating a quantified type
/// 量化型をインスタンス化するための文脈
#[derive(Debug, Clone)]
pub struct TyVarContext {
pub struct TyVarInstContext {
level: usize,
pub(crate) tyvar_instances: Dict<Str, Type>,
pub(crate) typaram_instances: Dict<Str, TyParam>,
}
impl fmt::Display for TyVarContext {
impl fmt::Display for TyVarInstContext {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(
f,
"TyVarContext {{ tyvar_instances: {}, typaram_instances: {} }}",
"TyVarInstContext {{ tyvar_instances: {}, typaram_instances: {} }}",
self.tyvar_instances, self.typaram_instances,
)
}
}
impl TyVarContext {
impl TyVarInstContext {
pub fn new(level: usize, bounds: Set<TyBound>, ctx: &Context) -> Self {
let mut self_ = Self {
level,
@ -509,7 +509,7 @@ impl Context {
.ok()
.map(|t| enum_unwrap!(t, Type::Subr));
let bounds = self.instantiate_ty_bounds(&sig.bounds, PreRegister)?;
let tv_ctx = TyVarContext::new(self.level, bounds, self);
let tv_ctx = TyVarInstContext::new(self.level, bounds, self);
let mut non_defaults = vec![];
for (n, p) in sig.params.non_defaults.iter().enumerate() {
let opt_decl_t = opt_decl_sig_t
@ -558,7 +558,7 @@ impl Context {
&self,
sig: &ParamSignature,
opt_decl_t: Option<&ParamTy>,
tmp_tv_ctx: Option<&TyVarContext>,
tmp_tv_ctx: Option<&TyVarInstContext>,
mode: RegistrationMode,
) -> TyCheckResult<Type> {
let spec_t = if let Some(spec_with_op) = &sig.t_spec {
@ -595,7 +595,7 @@ impl Context {
&self,
sig: &ParamSignature,
opt_decl_t: Option<&ParamTy>,
tmp_tv_ctx: Option<&TyVarContext>,
tmp_tv_ctx: Option<&TyVarInstContext>,
mode: RegistrationMode,
) -> TyCheckResult<ParamTy> {
let t = self.instantiate_param_sig_t(sig, opt_decl_t, tmp_tv_ctx, mode)?;
@ -618,7 +618,7 @@ impl Context {
&self,
predecl: &PreDeclTypeSpec,
opt_decl_t: Option<&ParamTy>,
tmp_tv_ctx: Option<&TyVarContext>,
tmp_tv_ctx: Option<&TyVarInstContext>,
) -> TyCheckResult<Type> {
match predecl {
ast::PreDeclTypeSpec::Simple(simple) => {
@ -632,7 +632,7 @@ impl Context {
&self,
simple: &SimpleTypeSpec,
opt_decl_t: Option<&ParamTy>,
tmp_tv_ctx: Option<&TyVarContext>,
tmp_tv_ctx: Option<&TyVarInstContext>,
) -> TyCheckResult<Type> {
match &simple.name.inspect()[..] {
"_" | "Obj" => Ok(Type::Obj),
@ -740,7 +740,7 @@ impl Context {
&self,
p: &ParamTySpec,
opt_decl_t: Option<&ParamTy>,
tmp_tv_ctx: Option<&TyVarContext>,
tmp_tv_ctx: Option<&TyVarInstContext>,
mode: RegistrationMode,
) -> TyCheckResult<ParamTy> {
let t = self.instantiate_typespec(&p.ty, opt_decl_t, tmp_tv_ctx, mode)?;
@ -754,7 +754,7 @@ impl Context {
&self,
spec: &TypeSpec,
opt_decl_t: Option<&ParamTy>,
tmp_tv_ctx: Option<&TyVarContext>,
tmp_tv_ctx: Option<&TyVarInstContext>,
mode: RegistrationMode,
) -> TyCheckResult<Type> {
match spec {
@ -897,7 +897,7 @@ impl Context {
fn instantiate_tp(
&self,
quantified: TyParam,
tmp_tv_ctx: &TyVarContext,
tmp_tv_ctx: &TyVarInstContext,
loc: Location,
) -> TyCheckResult<TyParam> {
match quantified {
@ -950,7 +950,7 @@ impl Context {
// K('U) -> K(?U)
else {
let ctx = self.get_nominal_type_ctx(&t).unwrap();
let tv_ctx = TyVarContext::new(self.level, ctx.bounds(), self);
let tv_ctx = TyVarInstContext::new(self.level, ctx.bounds(), self);
let t = self.instantiate_t(*t, &tv_ctx, loc)?;
Ok(TyParam::t(t))
}
@ -970,7 +970,7 @@ impl Context {
pub(crate) fn instantiate_t(
&self,
unbound: Type,
tmp_tv_ctx: &TyVarContext,
tmp_tv_ctx: &TyVarInstContext,
loc: Location,
) -> TyCheckResult<Type> {
match unbound {
@ -1121,7 +1121,7 @@ impl Context {
pub(crate) fn instantiate(&self, quantified: Type, callee: &hir::Expr) -> TyCheckResult<Type> {
match quantified {
Quantified(quant) => {
let tmp_tv_ctx = TyVarContext::new(self.level, quant.bounds, self);
let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self);
let t = self.instantiate_t(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?;
match &t {
Type::Subr(subr) => {
@ -1141,7 +1141,7 @@ impl Context {
// HACK: {op: |T|(T -> T) | op == F} => ?T -> ?T
Refinement(refine) if refine.t.is_quantified() => {
let quant = enum_unwrap!(*refine.t, Type::Quantified);
let tmp_tv_ctx = TyVarContext::new(self.level, quant.bounds, self);
let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self);
let t = self.instantiate_t(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?;
match &t {
Type::Subr(subr) => {

View file

@ -39,7 +39,7 @@ use ast::{DefId, VarName};
use erg_parser::ast;
use erg_parser::token::Token;
use crate::context::instantiate::{ConstTemplate, TyVarContext};
use crate::context::instantiate::{ConstTemplate, TyVarInstContext};
use crate::error::{SingleTyCheckResult, TyCheckError, TyCheckErrors, TyCheckResult};
use crate::mod_cache::SharedModuleCache;
use crate::varinfo::{Mutability, ParamIdx, VarInfo, VarKind};
@ -380,7 +380,7 @@ pub struct Context {
pub(crate) patches: Dict<VarName, Context>,
pub(crate) mod_cache: Option<SharedModuleCache>,
pub(crate) py_mod_cache: Option<SharedModuleCache>,
pub(crate) tv_ctx: Option<TyVarContext>,
pub(crate) tv_ctx: Option<TyVarInstContext>,
pub(crate) level: usize,
}
@ -840,7 +840,7 @@ impl Context {
name: &str,
kind: ContextKind,
vis: Visibility,
tv_ctx: Option<TyVarContext>,
tv_ctx: Option<TyVarInstContext>,
) -> TyCheckResult<()> {
let name = if vis.is_public() {
format!("{parent}.{name}", parent = self.name)

View file

@ -34,7 +34,7 @@ use Mutability::*;
use RegistrationMode::*;
use Visibility::*;
use super::instantiate::TyVarContext;
use super::instantiate::TyVarInstContext;
use super::OperationKind;
impl Context {
@ -517,7 +517,7 @@ impl Context {
ast::Signature::Subr(sig) => {
if sig.is_const() {
let bounds = self.instantiate_ty_bounds(&sig.bounds, PreRegister)?;
let tv_ctx = TyVarContext::new(self.level, bounds, self);
let tv_ctx = TyVarInstContext::new(self.level, bounds, self);
let vis = def.sig.vis();
self.grow(__name__, ContextKind::Proc, vis, Some(tv_ctx))?;
let (obj, const_t) = match self.eval_const_block(&def.body.block) {

View file

@ -9,7 +9,7 @@ use crate::ty::typaram::TyParam;
use crate::ty::{Predicate, TyBound, Type};
use Type::*;
use crate::context::instantiate::TyVarContext;
use crate::context::instantiate::TyVarInstContext;
use crate::context::Context;
impl Context {
@ -54,7 +54,7 @@ impl Context {
let unbound_t = func1(t.clone(), t);
let quantified = quant(unbound_t.clone(), bounds.clone());
println!("quantified : {quantified}");
let tv_ctx = TyVarContext::new(self.level + 1, bounds, self);
let tv_ctx = TyVarInstContext::new(self.level + 1, bounds, self);
println!("tv_ctx: {tv_ctx}");
let inst = self
.instantiate_t(unbound_t, &tv_ctx, Location::Unknown)

View file

@ -15,8 +15,7 @@ use crate::ty::value::ValueObj;
use crate::ty::{HasType, Predicate, TyBound, Type};
use crate::context::eval::SubstContext;
use crate::context::{Context, TyVarContext, Variance};
// use crate::context::instantiate::TyVarContext;
use crate::context::{Context, TyVarInstContext, Variance};
use crate::error::{SingleTyCheckResult, TyCheckError, TyCheckErrors, TyCheckResult};
use crate::hir;
@ -81,7 +80,7 @@ impl Context {
// NOTE: `?T(<: TraitX) -> Int` should be `TraitX -> Int`
// However, the current Erg cannot handle existential types, so it quantifies anyway
/*if !maybe_unbound_t.return_t().unwrap().has_qvar() {
let mut tv_ctx = TyVarContext::new(self.level, bounds.clone(), self);
let mut tv_ctx = TyVarInstContext::new(self.level, bounds.clone(), self);
let inst = Self::instantiate_t(
maybe_unbound_t,
&mut tv_ctx,
@ -532,7 +531,7 @@ impl Context {
for inst in self.get_trait_impls(trait_).into_iter() {
let sub_type = if inst.sub_type.has_qvar() {
let sub_ctx = self.get_nominal_type_ctx(&inst.sub_type).unwrap();
let tv_ctx = TyVarContext::new(self.level, sub_ctx.bounds(), self);
let tv_ctx = TyVarInstContext::new(self.level, sub_ctx.bounds(), self);
self.instantiate_t(inst.sub_type, &tv_ctx, Location::Unknown)
.unwrap()
} else {
@ -540,7 +539,7 @@ impl Context {
};
let sup_trait = if inst.sup_trait.has_qvar() {
let sup_ctx = self.get_nominal_type_ctx(&inst.sup_trait).unwrap();
let tv_ctx = TyVarContext::new(self.level, sup_ctx.bounds(), self);
let tv_ctx = TyVarInstContext::new(self.level, sup_ctx.bounds(), self);
self.instantiate_t(inst.sup_trait, &tv_ctx, Location::Unknown)
.unwrap()
} else {
@ -1470,7 +1469,24 @@ impl Context {
params: rps,
},
) => {
// e.g. Set(?T) <: Eq(Set(?T))
if ln != rn {
if let Some(sub_ctx) = self.get_nominal_type_ctx(maybe_sub) {
let subst_ctx = SubstContext::new(maybe_sub, self, loc);
for sup_trait in sub_ctx.super_traits.iter() {
let sup_trait = if sup_trait.has_qvar() {
subst_ctx.substitute(sup_trait.clone())?
} else {
sup_trait.clone()
};
if self.supertype_of(maybe_sup, &sup_trait) {
for (l_maybe_sub, r_maybe_sup) in sup_trait.typarams().iter().zip(rps.iter()) {
self.sub_unify_tp(l_maybe_sub, r_maybe_sup, None, loc, false)?;
}
return Ok(());
}
}
}
return Err(TyCheckErrors::from(TyCheckError::unification_error(
self.cfg.input.clone(),
line!() as usize,

View file

@ -26,7 +26,7 @@ use crate::ty::typaram::TyParam;
use crate::ty::value::{GenTypeObj, TypeKind, TypeObj, ValueObj};
use crate::ty::{HasType, ParamTy, Type};
use crate::context::instantiate::TyVarContext;
use crate::context::instantiate::TyVarInstContext;
use crate::context::{
ClassDefType, Context, ContextKind, OperationKind, RegistrationMode, TraitInstance,
};
@ -785,7 +785,7 @@ impl ASTLowerer {
let bounds = self
.ctx
.instantiate_ty_bounds(&lambda.sig.bounds, RegistrationMode::Normal)?;
let tv_ctx = TyVarContext::new(self.ctx.level, bounds, &self.ctx);
let tv_ctx = TyVarInstContext::new(self.ctx.level, bounds, &self.ctx);
self.ctx.grow(&name, kind, Private, Some(tv_ctx))?;
if let Err(errs) = self.ctx.assign_params(&lambda.sig.params, None) {
self.errs.extend(errs.into_iter());
@ -869,7 +869,7 @@ impl ASTLowerer {
let bounds = self
.ctx
.instantiate_ty_bounds(&sig.bounds, RegistrationMode::Normal)?;
let tv_ctx = TyVarContext::new(self.ctx.level, bounds, &self.ctx);
let tv_ctx = TyVarInstContext::new(self.ctx.level, bounds, &self.ctx);
self.ctx.grow(&name, kind, vis, Some(tv_ctx))?;
self.lower_subr_def(sig, def.body)
}