From 0a94d6fae742101bc78748b613d8981ad25dcdf3 Mon Sep 17 00:00:00 2001 From: Litchi Pi Date: Tue, 4 Jan 2022 16:16:14 +0100 Subject: [PATCH] Get apparent type from imported term instead of defaulting to Dyn Signed-off-by: Litchi Pi --- src/repl/mod.rs | 5 +-- src/typecheck/mod.rs | 63 ++++++++++++++++++++++++++++--------- tests/pass/typechecking.ncl | 4 +++ 3 files changed, 56 insertions(+), 16 deletions(-) diff --git a/src/repl/mod.rs b/src/repl/mod.rs index 8dd12eca..596de211 100644 --- a/src/repl/mod.rs +++ b/src/repl/mod.rs @@ -151,7 +151,7 @@ impl ReplImpl { } typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?; - typecheck::Envs::env_add(&mut self.env.type_env, id.clone(), &t); + typecheck::Envs::env_add(&mut self.env.type_env, id.clone(), &t, &self.cache); for id in &pending { self.cache .typecheck(*id, &self.init_type_env) @@ -211,7 +211,7 @@ impl Repl for ReplImpl { for id in &pending { self.cache.resolve_imports(*id).unwrap(); } - typecheck::Envs::env_add_term(&mut self.env.type_env, &term).unwrap(); + typecheck::Envs::env_add_term(&mut self.env.type_env, &term, &self.cache).unwrap(); eval::env_add_term(&mut self.env.eval_env, term.clone()).unwrap(); Ok(term) @@ -230,6 +230,7 @@ impl Repl for ReplImpl { Ok(typecheck::apparent_type( term.as_ref(), Some(&typecheck::Envs::from_global(&self.env.type_env)), + Some(&self.cache), ) .into()) } diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs index 421fe6b9..db89a000 100644 --- a/src/typecheck/mod.rs +++ b/src/typecheck/mod.rs @@ -397,14 +397,19 @@ impl<'a> Envs<'a> { /// Add the bindings of a record to a typing environment. Ignore fields whose name are defined /// through interpolation. //TODO: support the case of a record with a type annotation. - pub fn env_add_term(env: &mut Environment, rt: &RichTerm) -> Result<(), EnvBuildError> { + pub fn env_add_term( + env: &mut Environment, + rt: &RichTerm, + resolver: &dyn ImportResolver, + ) -> Result<(), EnvBuildError> { let RichTerm { term, pos } = rt; match term.as_ref() { Term::Record(bindings, _) | Term::RecRecord(bindings, ..) => { for (id, t) in bindings { let tyw: TypeWrapper = - apparent_type(t.as_ref(), Some(&Envs::from_global(env))).into(); + apparent_type(t.as_ref(), Some(&Envs::from_global(env)), Some(resolver)) + .into(); env.insert(id.clone(), tyw); } @@ -415,10 +420,10 @@ impl<'a> Envs<'a> { } /// Bind one term in a typing environment. - pub fn env_add(env: &mut Environment, id: Ident, rt: &RichTerm) { + pub fn env_add(env: &mut Environment, id: Ident, rt: &RichTerm, resolver: &dyn ImportResolver) { env.insert( id, - apparent_type(rt.as_ref(), Some(&Envs::from_global(env))).into(), + apparent_type(rt.as_ref(), Some(&Envs::from_global(env)), Some(resolver)).into(), ); } @@ -629,7 +634,7 @@ fn type_check_( .map_err(|err| err.into_typecheck_err(state, rt.pos)) } Term::Let(x, re, rt, _) => { - let ty_let = binding_type(re.as_ref(), &envs, state.table, strict); + let ty_let = binding_type(re.as_ref(), &envs, state.table, strict, state.resolver); linearizer.retype_ident(lin, x, ty_let.clone()); type_check_( state, @@ -667,7 +672,7 @@ fn type_check_( }); } } - let ty_let = binding_type(re.as_ref(), &envs, state.table, strict); + let ty_let = binding_type(re.as_ref(), &envs, state.table, strict, state.resolver); type_check_( state, envs.clone(), @@ -789,7 +794,7 @@ fn type_check_( // Fields defined by interpolation are ignored. if let Term::RecRecord(..) = t.as_ref() { for (id, rt) in stat_map { - let tyw = binding_type(rt.as_ref(), &envs, state.table, strict); + let tyw = binding_type(rt.as_ref(), &envs, state.table, strict, state.resolver); envs.insert(id.clone(), tyw.clone()); linearizer.retype_ident(lin, id, tyw); } @@ -963,8 +968,12 @@ fn type_check_( .resolver .get(*file_id) .expect("Internal error: resolved import not found during typechecking."); - let ty_import: TypeWrapper = - apparent_type(t.as_ref(), Some(&Envs::from_envs(&envs))).into(); + let ty_import: TypeWrapper = apparent_type( + t.as_ref(), + Some(&Envs::from_envs(&envs)), + Some(state.resolver), + ) + .into(); unify(state, strict, ty, ty_import).map_err(|err| err.into_typecheck_err(state, rt.pos)) } } @@ -979,8 +988,16 @@ fn type_check_( /// return `Dyn`. /// * in strict mode, we will typecheck `bound_exp`: return a new unification variable to be /// associated to `bound_exp`. -fn binding_type(t: &Term, envs: &Envs, table: &mut UnifTable, strict: bool) -> TypeWrapper { - let ty_apt = apparent_type(t, Some(envs)); +/// As this function is always called in a context where an `ImportResolver` is present, expect +/// it passed in arguments. +fn binding_type( + t: &Term, + envs: &Envs, + table: &mut UnifTable, + strict: bool, + resolver: &dyn ImportResolver, +) -> TypeWrapper { + let ty_apt = apparent_type(t, Some(envs), Some(resolver)); match ty_apt { ApparentType::Approximated(_) if strict => TypeWrapper::Ptr(new_var(table)), @@ -1042,9 +1059,15 @@ impl From for TypeWrapper { /// - if `bound_exp` is a constant (string, number, boolean or symbol) which type can be deduced /// directly without unfolding the expression further, return the corresponding exact type. /// - if `bound_exp` is a list, return `List Dyn`. +/// - if `bound_exp` is a resolved import, return the apparent type of the imported term. Returns +/// `Dyn` if the resolver is not passed as a parameter to the function. /// - Otherwise, return an approximation of the type (currently `Dyn`, but could be more precise in /// the future, such as `Dyn -> Dyn` for functions, `{ | Dyn}` for records, and so on). -pub fn apparent_type(t: &Term, envs: Option<&Envs>) -> ApparentType { +pub fn apparent_type( + t: &Term, + envs: Option<&Envs>, + resolver: Option<&dyn ImportResolver>, +) -> ApparentType { match t { Term::MetaValue(MetaValue { types: Some(Contract { types: ty, .. }), @@ -1054,7 +1077,9 @@ pub fn apparent_type(t: &Term, envs: Option<&Envs>) -> ApparentType { Term::MetaValue(MetaValue { contracts, .. }) if !contracts.is_empty() => { ApparentType::Annotated(contracts.get(0).unwrap().types.clone()) } - Term::MetaValue(MetaValue { value: Some(v), .. }) => apparent_type(v.as_ref(), envs), + Term::MetaValue(MetaValue { value: Some(v), .. }) => { + apparent_type(v.as_ref(), envs, resolver) + } Term::Num(_) => ApparentType::Inferred(Types(AbsType::Num())), Term::Bool(_) => ApparentType::Inferred(Types(AbsType::Bool())), Term::Sym(_) => ApparentType::Inferred(Types(AbsType::Sym())), @@ -1066,6 +1091,16 @@ pub fn apparent_type(t: &Term, envs: Option<&Envs>) -> ApparentType { .and_then(|envs| envs.get(id)) .map(ApparentType::FromEnv) .unwrap_or(ApparentType::Approximated(Types(AbsType::Dyn()))), + Term::ResolvedImport(f) => { + if let Some(r) = resolver { + let t = r + .get(*f) + .expect("Internal error: resolved import not found during typechecking."); + apparent_type(&t.term, envs, Some(r)) + } else { + ApparentType::Approximated(Types(AbsType::Dyn())) + } + } _ => ApparentType::Approximated(Types(AbsType::Dyn())), } } @@ -1090,7 +1125,7 @@ pub fn infer_type(t: &Term) -> TypeWrapper { types: None, .. }) => infer_type(rt.as_ref()), - t => apparent_type(t, None).into(), + t => apparent_type(t, None, None).into(), } } diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl index d0a10342..a9400346 100644 --- a/tests/pass/typechecking.ncl +++ b/tests/pass/typechecking.ncl @@ -168,6 +168,10 @@ let typecheck = [ // Typed import import "typed-import.ncl" : Num, + // Regression test for #430 (https://github.com/tweag/nickel/issues/430) + let x = import "typed-import.ncl" + in x : Num, + // recursive_records_quoted {"foo" = 1} : {foo : Num},