Strict typechecking mode (#2077)

* Add interpreter config and strict typecheck mode

* Add tests

* Make it typechecker-only, and run it twice

* Add a test for imports

* Test the cli also

* Fix benches, add a comment

* Remove unused config module

cli/src/doctest.rs

@@ -18,6 +18,7 @@ use nickel_lang_core::{
         TypeAnnotation,
     },
     typ::{Type, TypeF},
+    typecheck::TypecheckMode,
 };
 use once_cell::sync::Lazy;
 use regex::Regex;
@@ -282,7 +283,7 @@ impl TestCommand {
         program: &mut Program<CacheImpl>,
     ) -> Result<(RichTerm, TestRegistry), CoreError> {
         let mut registry = TestRegistry::default();
-        program.typecheck()?;
+        program.typecheck(TypecheckMode::Walk)?;
         program
             .custom_transform(|cache, rt| doctest_transform(cache, &mut registry, rt))
             .map_err(|e| e.unwrap_error("transforming doctest"))?;

cli/src/typecheck.rs

@@ -1,3 +1,5 @@
+use nickel_lang_core::typecheck::TypecheckMode;
+
 use crate::{
     cli::GlobalOptions,
     customize::NoCustomizeMode,
@@ -9,11 +11,32 @@ use crate::{
 pub struct TypecheckCommand {
     #[command(flatten)]
     inputs: InputOptions<NoCustomizeMode>,
+
+    /// Start the type-checker in strict mode, so that the entire input is treated as a typed block.
+    #[arg(long, global = true)]
+    pub strict_typechecking: bool,
 }
 
 impl TypecheckCommand {
     pub fn run(self, global: GlobalOptions) -> CliResult<()> {
+        if self.strict_typechecking {
+            // In strict mode we run *both* forms of typechecking, because in
+            // fact neither one is more strict than the other. For example,
+            // given the input
+            //
+            // let x = (1 + 1) in (x + 1 : Number)
+            //
+            // typechecking in "enforce" mode will succeed because it will infer
+            // `x: Number`, while typechecking in walk mode will fail because it
+            // will treat `x` as `Dyn` and then try to typecheck `x + 1`.
+            let mut program = self.inputs.prepare(&global)?;
+            program
+                .typecheck(TypecheckMode::Enforce)
+                .report_with_program(program)?;
+        }
         let mut program = self.inputs.prepare(&global)?;
-        program.typecheck().report_with_program(program)
+        program
+            .typecheck(TypecheckMode::Walk)
+            .report_with_program(program)
     }
 }

cli/tests/snapshot/inputs/errors/typecheck_strict_mode.ncl

@@ -0,0 +1,3 @@
+# capture = 'stderr'
+# command = ['typecheck', '--strict-typechecking']
+1 + "foo"

cli/tests/snapshot/inputs/errors/typedcheck_strict_mode_is_strict.ncl

@@ -0,0 +1,3 @@
+# capture = 'stderr'
+# command = ['typecheck', '--strict-typechecking']
+let x = (1 + 1) in (x + 1 : Number)

cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typecheck_strict_mode.ncl.snap

@@ -0,0 +1,13 @@
+---
+source: cli/tests/snapshot/main.rs
+expression: err
+---
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/typecheck_strict_mode.ncl:3:5
+  │
+3 │ 1 + "foo"
+  │     ^^^^^ this expression
+  │
+  = Expected an expression of type `Number`
+  = Found an expression of type `String`
+  = These types are not compatible

cli/tests/snapshot/snapshots/snapshot__typecheck_stderr_typedcheck_strict_mode_is_strict.ncl.snap

@@ -0,0 +1,13 @@
+---
+source: cli/tests/snapshot/main.rs
+expression: err
+---
+error: incompatible types
+  ┌─ [INPUTS_PATH]/errors/typedcheck_strict_mode_is_strict.ncl:3:21
+  │
+3 │ let x = (1 + 1) in (x + 1 : Number)
+  │                     ^ this expression
+  │
+  = Expected an expression of type `Number`
+  = Found an expression of type `Dyn`
+  = These types are not compatible

core/src/cache.rs

@@ -14,7 +14,7 @@ use crate::term::record::{Field, RecordData};
 use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
 use crate::typ::UnboundTypeVariableError;
-use crate::typecheck::{self, type_check, Wildcards};
+use crate::typecheck::{self, type_check, TypecheckMode, Wildcards};
 use crate::{eval, parser, transform};
 
 use codespan::{FileId, Files};
@@ -638,20 +638,21 @@ impl Cache {
         &mut self,
         file_id: FileId,
         initial_ctxt: &typecheck::Context,
+        initial_mode: TypecheckMode,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         match self.terms.get(&file_id) {
             Some(TermEntry { state, .. }) if *state >= EntryState::Typechecked => {
                 Ok(CacheOp::Cached(()))
             }
             Some(TermEntry { term, state, .. }) if *state >= EntryState::Parsed => {
                 if *state < EntryState::Typechecking {
-                    let wildcards = type_check(term, initial_ctxt.clone(), self)?;
+                    let wildcards = type_check(term, initial_ctxt.clone(), self, initial_mode)?;
                     self.update_state(file_id, EntryState::Typechecking);
                     self.wildcards.insert(file_id, wildcards);
 
                     if let Some(imports) = self.imports.get(&file_id).cloned() {
                         for f in imports.into_iter() {
-                            self.typecheck(f, initial_ctxt)?;
+                            self.typecheck(f, initial_ctxt, initial_mode)?;
                         }
                     }
 
@@ -1005,10 +1006,13 @@ impl Cache {
             result = CacheOp::Done(());
         }
 
-        let typecheck_res = self.typecheck(file_id, initial_ctxt).map_err(|cache_err| {
-            cache_err
-                .unwrap_error("cache::prepare(): expected source to be parsed before typechecking")
-        })?;
+        let typecheck_res = self
+            .typecheck(file_id, initial_ctxt, TypecheckMode::Walk)
+            .map_err(|cache_err| {
+                cache_err.unwrap_error(
+                    "cache::prepare(): expected source to be parsed before typechecking",
+                )
+            })?;
         if typecheck_res == CacheOp::Done(()) {
             result = CacheOp::Done(());
         };
@@ -1052,7 +1056,7 @@ impl Cache {
             resolved_ids: pending,
         } = import_resolution::strict::resolve_imports(term, self)?;
 
-        let wildcards = type_check(&term, initial_ctxt.clone(), self)?;
+        let wildcards = type_check(&term, initial_ctxt.clone(), self, TypecheckMode::Walk)?;
         let term = transform::transform(term, Some(&wildcards))
             .map_err(|err| Error::ParseErrors(err.into()))?;
         Ok((term, pending))
@@ -1291,7 +1295,7 @@ impl Cache {
         if let Some(ids) = self.stdlib_ids.as_ref().cloned() {
             ids.iter()
                 .try_fold(CacheOp::Cached(()), |cache_op, (_, file_id)| {
-                    match self.typecheck(*file_id, initial_ctxt)? {
+                    match self.typecheck(*file_id, initial_ctxt, TypecheckMode::Walk)? {
                         done @ CacheOp::Done(()) => Ok(done),
                         _ => Ok(cache_op),
                     }

core/src/program.rs

@@ -36,6 +36,7 @@ use crate::{
         record::Field,
         BinaryOp, MergePriority, RichTerm, Term,
     },
+    typecheck::TypecheckMode,
 };
 
 use clap::ColorChoice;
@@ -531,7 +532,7 @@ impl<EC: EvalCache> Program<EC> {
     }
 
     /// Load, parse, and typecheck the program and the standard library, if not already done.
-    pub fn typecheck(&mut self) -> Result<(), Error> {
+    pub fn typecheck(&mut self, initial_mode: TypecheckMode) -> Result<(), Error> {
         self.vm
             .import_resolver_mut()
             .parse(self.main_id, InputFormat::Nickel)?;
@@ -548,7 +549,7 @@ impl<EC: EvalCache> Program<EC> {
             })?;
         self.vm
             .import_resolver_mut()
-            .typecheck(self.main_id, &initial_env)
+            .typecheck(self.main_id, &initial_env, initial_mode)
             .map_err(|cache_err| {
                 cache_err.unwrap_error("program::typecheck(): expected source to be parsed")
             })?;
@@ -1186,7 +1187,7 @@ mod tests {
                     TermPos::None,
                 ))
             })?;
-        p.typecheck()
+        p.typecheck(TypecheckMode::Walk)
     }
 
     #[test]

core/src/repl/mod.rs

@@ -20,6 +20,7 @@ use crate::term::TraverseOrder;
 use crate::term::{record::Field, RichTerm, Term, Traverse};
 use crate::transform::import_resolution;
 use crate::typ::Type;
+use crate::typecheck::TypecheckMode;
 use crate::{eval, transform, typecheck};
 use codespan::FileId;
 use simple_counter::*;
@@ -129,8 +130,12 @@ impl<EC: EvalCache> ReplImpl<EC> {
                 })?;
         }
 
-        let wildcards =
-            typecheck::type_check(&t, self.env.type_ctxt.clone(), self.vm.import_resolver())?;
+        let wildcards = typecheck::type_check(
+            &t,
+            self.env.type_ctxt.clone(),
+            self.vm.import_resolver(),
+            TypecheckMode::Walk,
+        )?;
 
         if let Some(id) = id {
             typecheck::env_add(
@@ -150,7 +155,7 @@ impl<EC: EvalCache> ReplImpl<EC> {
         for id in &pending {
             self.vm
                 .import_resolver_mut()
-                .typecheck(*id, &self.initial_type_ctxt)
+                .typecheck(*id, &self.initial_type_ctxt, TypecheckMode::Walk)
                 .map_err(|cache_err| {
                     cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
                 })?;
@@ -293,8 +298,12 @@ impl<EC: EvalCache> Repl for ReplImpl<EC> {
             self.vm.import_resolver_mut().resolve_imports(*id).unwrap();
         }
 
-        let wildcards =
-            typecheck::type_check(&term, self.env.type_ctxt.clone(), self.vm.import_resolver())?;
+        let wildcards = typecheck::type_check(
+            &term,
+            self.env.type_ctxt.clone(),
+            self.vm.import_resolver(),
+            TypecheckMode::Walk,
+        )?;
         // Substitute the wildcard types for their inferred types We need to `traverse` the term, in
         // case the type depends on inner terms that also contain wildcards
         let term = term

core/src/typecheck/mod.rs

@@ -17,9 +17,10 @@
 //!   typecheck. Walk mode also stores the annotations of bound identifiers in the environment. This
 //!   is implemented by the `walk` function.
 //!
-//! The algorithm starts in walk mode. A typed block (an expression annotated with a type) switches
-//! to enforce mode, and is switched back to walk mode when entering an expression annotated with a
-//! contract. Type and contract annotations thus serve as a switch for the typechecking mode.
+//! The algorithm usually starts in walk mode, although this can be configured. A typed block
+//! (an expression annotated with a type) switches to enforce mode, and is switched back to walk
+//! mode when entering an expression annotated with a contract. Type and contract annotations thus
+//! serve as a switch for the typechecking mode.
 //!
 //! Note that the static typing part (enforce mode) is based on the bidirectional typing framework,
 //! which defines two different modes. Thus, the enforce mode is itself divided again into
@@ -95,6 +96,15 @@ use self::subtyping::SubsumedBy;
 /// The max depth parameter used to limit the work performed when inferring the type of the stdlib.
 const INFER_RECORD_MAX_DEPTH: u8 = 4;
 
+/// The typechecker has two modes, one for statically typed code and one for dynamically type code.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum TypecheckMode {
+    /// In `Walk` mode, the typechecker traverses the AST looking for typed blocks.
+    Walk,
+    /// In `Enforce` mode, the typechecker checks types.
+    Enforce,
+}
+
 /// The typing environment.
 pub type Environment = GenericEnvironment<Ident, UnifType>;
 
@@ -1382,8 +1392,10 @@ pub fn type_check(
     t: &RichTerm,
     initial_ctxt: Context,
     resolver: &impl ImportResolver,
+    initial_mode: TypecheckMode,
 ) -> Result<Wildcards, TypecheckError> {
-    type_check_with_visitor(t, initial_ctxt, resolver, &mut ()).map(|tables| tables.wildcards)
+    type_check_with_visitor(t, initial_ctxt, resolver, &mut (), initial_mode)
+        .map(|tables| tables.wildcards)
 }
 
 /// Typecheck a term while providing the type information to a visitor.
@@ -1392,6 +1404,7 @@ pub fn type_check_with_visitor<V>(
     initial_ctxt: Context,
     resolver: &impl ImportResolver,
     visitor: &mut V,
+    initial_mode: TypecheckMode,
 ) -> Result<TypeTables, TypecheckError>
 where
     V: TypecheckVisitor,
@@ -1408,7 +1421,12 @@ where
             wildcard_vars: &mut wildcard_vars,
         };
 
-        walk(&mut state, initial_ctxt, visitor, t)?;
+        if initial_mode == TypecheckMode::Enforce {
+            let uty = state.table.fresh_type_uvar(initial_ctxt.var_level);
+            check(&mut state, initial_ctxt, visitor, t, uty)?;
+        } else {
+            walk(&mut state, initial_ctxt, visitor, t)?;
+        }
     }
 
     let result = wildcard_vars_to_type(wildcard_vars.clone(), &table);
@@ -1475,7 +1493,7 @@ fn walk<V: TypecheckVisitor>(
             walk(state, ctxt, visitor, t)
         }
         Term::FunPattern(pat, t) => {
-            let PatternTypeData { bindings: pat_bindings, ..} = pat.pattern_types(state, &ctxt, pattern::TypecheckMode::Walk)?;
+            let PatternTypeData { bindings: pat_bindings, ..} = pat.pattern_types(state, &ctxt, TypecheckMode::Walk)?;
             ctxt.type_env.extend(pat_bindings.into_iter().map(|(id, typ)| (id.ident(), typ)));
 
             walk(state, ctxt, visitor, t)
@@ -1552,7 +1570,7 @@ fn walk<V: TypecheckVisitor>(
                 //
                 // The use of start_ctxt here looks like it might be wrong for let rec, but in fact
                 // it's unused in TypecheckMode::Walk anyway.
-                let PatternTypeData {bindings: pat_bindings, ..} = pat.data.pattern_types(state, &start_ctxt, pattern::TypecheckMode::Walk)?;
+                let PatternTypeData {bindings: pat_bindings, ..} = pat.data.pattern_types(state, &start_ctxt, TypecheckMode::Walk)?;
 
                 for (id, typ) in pat_bindings {
                     visitor.visit_ident(&id, typ.clone());
@@ -1574,7 +1592,7 @@ fn walk<V: TypecheckVisitor>(
         Term::Match(data) => {
             data.branches.iter().try_for_each(|MatchBranch { pattern, guard, body }| {
                 let mut local_ctxt = ctxt.clone();
-                let PatternTypeData { bindings: pat_bindings, .. } = pattern.data.pattern_types(state, &ctxt, pattern::TypecheckMode::Walk)?;
+                let PatternTypeData { bindings: pat_bindings, .. } = pattern.data.pattern_types(state, &ctxt, TypecheckMode::Walk)?;
 
                 if let Some(alias) = &pattern.alias {
                     visitor.visit_ident(alias, mk_uniftype::dynamic());
@@ -1916,9 +1934,9 @@ fn check<V: TypecheckVisitor>(
         }
         Term::FunPattern(pat, t) => {
             // See [^separate-alias-treatment].
-            let pat_types =
-                pat.data
-                    .pattern_types(state, &ctxt, pattern::TypecheckMode::Enforce)?;
+            let pat_types = pat
+                .data
+                .pattern_types(state, &ctxt, TypecheckMode::Enforce)?;
             // In the destructuring case, there's no alternative pattern, and we must thus
             // immediately close all the row types.
             pattern::close_all_enums(pat_types.enum_open_tails, state);
@@ -2036,8 +2054,7 @@ fn check<V: TypecheckVisitor>(
             let start_ctxt = ctxt.clone();
             for (pat, re) in bindings {
                 // See [^separate-alias-treatment].
-                let pat_types =
-                    pat.pattern_types(state, &start_ctxt, pattern::TypecheckMode::Enforce)?;
+                let pat_types = pat.pattern_types(state, &start_ctxt, TypecheckMode::Enforce)?;
 
                 // In the destructuring case, there's no alternative pattern, and we must thus
                 // immediatly close all the row types.
@@ -2109,11 +2126,9 @@ fn check<V: TypecheckVisitor>(
                 .map(|branch| -> Result<_, TypecheckError> {
                     Ok((
                         branch,
-                        branch.pattern.pattern_types(
-                            state,
-                            &ctxt,
-                            pattern::TypecheckMode::Enforce,
-                        )?,
+                        branch
+                            .pattern
+                            .pattern_types(state, &ctxt, TypecheckMode::Enforce)?,
                     ))
                 })
                 .collect::<Result<Vec<(&MatchBranch, PatternTypeData<_>)>, _>>()?;

core/src/typecheck/pattern.rs

@@ -8,12 +8,6 @@ use crate::{
 
 use super::*;
 
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub(super) enum TypecheckMode {
-    Walk,
-    Enforce,
-}
-
 /// A list of pattern variables and their associated type.
 pub type TypeBindings = Vec<(LocIdent, UnifType)>;
 

core/tests/integration/inputs/lib/import_typecheck_strict.ncl

@@ -0,0 +1,4 @@
+# test.type = 'skip'
+
+# This is an auxiliary file used by typechecking tests
+1 + "foo"

core/tests/integration/inputs/typecheck/shallow_type_inference_strict_mode.ncl

@@ -0,0 +1,3 @@
+# test.type = 'pass'
+# eval = 'typecheck_strict'
+let x = (1 + 1) in (x + 1 : Number)