Repository: tweag/nickel
Pull request #395 (2021-09-13 15:47:27)

[Fix]Unsound typechecking of imports
Following #393, imports are now correctly type-checked individually. However, #393 unveiled a bug: one can use imports in a typed block with any type, and it typechecks, such as in:

```
// file import.ncl
1 + 1 : Num

// file main.ncl
let x : Str = import "import.ncl" in ... // Passes!
```

This PR fixes the issue by adding a missing call to `unify` when typechecking an import in a statically typed block, fixes an existing test, and adds a regression test. In the process, we got rid of the `to_typewrapper` function, to have it rather as a trait impl `From<Types> for TypeWrapper`.

We use the apparent type of the import for the unification constraint. That is, typechecking the usage of an import in a statically typed block is equivalent to typechecking the usage of a variable coming from code external to the block:

```
// previous example now equivalent to (with respect to typechecking):
let __import = 1 + 1 : Num in
let x : Str = __import in ... // Fail
```

Concretely, an import must either be annotated at the top-level, or be a trivial expression whose apparent type can be inferred, to be assigned something else than the `Dyn` type.


Patch:
diff --git a/src/typecheck.rs b/src/typecheck.rs
index 71061430..2e9d9202 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -354,6 +354,15 @@ impl<'a> Envs<'a> {
         }
     }
 
+    /// Similar to [`from_global`](./struct.Envs.html#method.from_global), but
+    /// use another `Envs` to provide the global environment.
+    pub fn from_envs(envs: &'a Envs) -> Self {
+        Envs {
+            global: envs.global,
+            local: Environment::new(),
+        }
+    }
+
     /// Populate a new global typing environment from a global term environment.
     pub fn mk_global(eval_env: &eval::Environment) -> Environment {
         eval_env
@@ -361,7 +370,7 @@ impl<'a> Envs<'a> {
             .map(|(id, thunk)| {
                 (
                     id.clone(),
-                    to_typewrapper(apparent_type(thunk.borrow().body.as_ref(), None).into()),
+                    apparent_type(thunk.borrow().body.as_ref(), None).into(),
                 )
             })
             .collect()
@@ -393,7 +402,7 @@ impl<'a> Envs<'a> {
     pub fn env_add(env: &mut Environment, id: Ident, rt: &RichTerm) {
         env.insert(
             id,
-            to_typewrapper(apparent_type(rt.as_ref(), Some(&Envs::from_global(env))).into()),
+            apparent_type(rt.as_ref(), Some(&Envs::from_global(env))).into(),
         );
     }
 
@@ -687,7 +696,7 @@ fn type_check_(
             value: Some(t),
             ..
         }) => {
-            let tyw2 = to_typewrapper(ty2.clone());
+            let tyw2 = TypeWrapper::from(ty2.clone());
 
             let instantiated = instantiate_foralls(state, tyw2.clone(), ForallInst::Constant);
 
@@ -704,7 +713,7 @@ fn type_check_(
             let ctr = contracts.get(0).unwrap();
             let Contract { types: ty2, .. } = ctr;
 
-            unify(state, strict, ty, to_typewrapper(ty2.clone()))
+            unify(state, strict, ty, ty2.clone().into())
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
 
             // if there's an inner value, we have to recursively typecheck it, but in non strict
@@ -732,12 +741,16 @@ fn type_check_(
         },
         Term::Import(_) => unify(state, strict, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
+        // We typecheck the import in a fresh typing environment, and then use its apparent type
+        // for checking. 
         Term::ResolvedImport(file_id) => {
             let t = state
                 .resolver
                 .get(*file_id)
                 .expect("Internal error: resolved import not found ({:?}) during typechecking.");
-            type_check_in_env(&t, envs.global, state.resolver).map(|_ty| ())
+            let _ = type_check_in_env(&t, envs.global, state.resolver)?;
+            let ty_import : TypeWrapper = apparent_type(t.as_ref(), Some(&Envs::from_envs(&envs))).into();
+            unify(state, strict, ty, ty_import).map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
     }
 }
@@ -796,7 +809,7 @@ impl From<ApparentType> for TypeWrapper {
         match at {
             ApparentType::Annotated(ty)
             | ApparentType::Inferred(ty)
-            | ApparentType::Approximated(ty) => to_typewrapper(ty),
+            | ApparentType::Approximated(ty) => ty.into(),
             ApparentType::FromEnv(tyw) => tyw,
         }
     }
@@ -927,6 +940,12 @@ impl From<AbsType<Box<TypeWrapper>>> for TypeWrapper {
     }
 }
 
+impl From<Types> for TypeWrapper {
+    fn from(ty: Types) -> Self {
+        TypeWrapper::Concrete(ty.0.map(|ty_| Box::new(TypeWrapper::from(*ty_))))
+    }
+}
+
 #[macro_use]
 /// Helpers for building `TypeWrapper`s.
 pub mod mk_typewrapper {
@@ -1307,15 +1326,6 @@ pub fn unify_rows(
     }
 }
 
-/// Convert a vanilla Nickel type to a type wrapper.
-fn to_typewrapper(t: Types) -> TypeWrapper {
-    let Types(t2) = t;
-
-    let t3 = t2.map(|x| Box::new(to_typewrapper(*x)));
-
-    TypeWrapper::Concrete(t3)
-}
-
 /// Extract the concrete type corresponding to a type wrapper. Free unification variables as well
 /// as type constants are replaced with the type `Dyn`.
 fn to_type(table: &UnifTable, ty: TypeWrapper) -> Types {


Test patch:
diff --git a/tests/pass/typed-import.ncl b/tests/pass/typed-import.ncl
index 8d2f0971..a4368194 100644
--- a/tests/pass/typed-import.ncl
+++ b/tests/pass/typed-import.ncl
@@ -1,1 +1,1 @@
-1 + 1
+1 + 1 : Num
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 99d94d8f..af78813e 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -158,9 +158,13 @@ fn imports() {
     resolver.add_source(String::from("good"), String::from("1 + 1 : Num"));
     resolver.add_source(String::from("bad"), String::from("false : Num"));
     resolver.add_source(
-        String::from("proxy"),
+        String::from("proxy-bad"),
         String::from("let x = import \"bad\" in x"),
     );
+    resolver.add_source(
+        String::from("proxy-wrong-type"),
+        String::from("let x : Str = import \"good\" in x"),
+    );
 
     fn mk_import<R>(import: &str, resolver: &mut R) -> Result<RichTerm, ImportError>
     where
@@ -172,18 +176,23 @@ fn imports() {
         )
     }
 
-    type_check_in_env(
-        &mk_import("good", &mut resolver).unwrap(),
-        &Environment::new(),
-        &mut resolver,
-    )
-    .unwrap();
-    type_check_in_env(
-        &mk_import("proxy", &mut resolver).unwrap(),
-        &Environment::new(),
-        &mut resolver,
-    )
-    .unwrap_err();
+    assert_matches!(
+        type_check_in_env(
+            &mk_import("proxy-wrong-type", &mut resolver).unwrap(),
+            &Environment::new(),
+            &mut resolver,
+        ),
+        Err(TypecheckError::TypeMismatch(..))
+    );
+
+    assert_matches!(
+        type_check_in_env(
+            &mk_import("proxy-bad", &mut resolver).unwrap(),
+            &Environment::new(),
+            &mut resolver,
+        ),
+        Err(TypecheckError::TypeMismatch(..))
+    );
 }
 
 #[test]