Repository: tweag/nickel
Pull request #540 (2022-01-04 15:19:31)

Get apparent type from imported term instead of defaulting to Dyn
Simple fix for issue #430 
Has the inconvenient of passing the ImportResolver to the `apparent_type` function.
Using `Option<_>` to allow one to simply ignore the apparent typing of the imported terms (notably useful for the `infer_type` function which doesn't have access to any ImportResolver).

Would it be needed to add a regression test for this particular issue ?

litchipi: The new regression test works as intended and doesn't pollute much the existing one, however I still don't really find it elegant but I'm not really confortable with the Nickel langage yet.
Is there a way to use `deepseq` to force the typechecking and use it elegantly with the existing term ?
Or should I let it ugly and functionnal ?
yannham: You can put the test in `typechecking.ncl`, which is specifically for typechecking. It doesn't evaluate anything (because lists are lazy in Nickel, and this test file is just one big list), so it just typechecks.

You don't need to change the `typed-import.ncl`. You can leave it as it was, with the type annotation: in both case it has the same apparent type (`Num`), and the apparent type of the import itself doesn't even matter. What matters is that if you put this import in a variable without annotation, this variable is assigned the same type `Num`, while it was assigned `Dyn` before. So, to sum up:

1. Leave `typed-import.ncl` alone
2. Inside `tests/pass/typechecking.ncl`, add a new element at the end of the list (with the comment about it being a regression test): `let x = import "typed-import.ncl" in x : Num,`
litchipi: Fair enough, didn't see how to add a typechecking-only test into the suite, I'll know later.
Added the test as you intended, should be okay now
yannham: @litchipi there's a conflict now and the code hasn't been formatted properly.

Patch:
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_<S, E>(
                 .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_<S, E>(
                     });
                 }
             }
-            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_<S, E>(
             // 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_<S, E>(
                 .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_<S, E>(
 ///       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<ApparentType> 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(),
     }
 }
 


Test patch:
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},