Repository: tweag/nickel (rust)

Issue:
Standard library functions can't be used in typed code
This problem has been described in more general terms in #226, but #226 is rather an open-ended reflection than a focused issue. This issue is dedicated to the specific problem of using stdlib functions within typed code.

**Describe the bug**
The stdlib modules hide the types of stdlib functions, making them unusable within typed code.

**To Reproduce**

```
nickel> (lists.length [] == 0) : Bool
error: Incompatible types
  ┌─ repl-input-1:1:2
  │
1 │ (lists.length [] == 0) : Bool
  │  ^^^^^ this expression
  │
  = The type of the expression was expected to be `{length: _a -> _b | _c}`
  = The type of the expression was inferred to be `Dyn`
  = These types are not compatible
```

**Expected behavior**
The type of stdlib functions is taken into account:

```
nickel> (lists.length [] == 0) : Bool
true
```

Pull request description:
Fix/stdlib typechecking
fix typing with stdlib.
specific type environment construction for the stdlib. the records are typed on top level traversing recursively the records to infer type of fields. From each typed fields, construct a type record to type the top level record.
close #375 

Patch:
diff --git a/lsp/nls/src/cache.rs b/lsp/nls/src/cache.rs
index d1ba016d..1643c30c 100644
--- a/lsp/nls/src/cache.rs
+++ b/lsp/nls/src/cache.rs
@@ -4,7 +4,6 @@ use codespan::FileId;
 use nickel::{
     cache::{Cache, CacheError, CacheOp, CachedTerm, EntryState},
     error::TypecheckError,
-    eval,
     typecheck::{self, linearization::Completed},
 };
 
@@ -15,7 +14,7 @@ pub trait CacheExt {
     fn typecheck_with_analysis(
         &mut self,
         file_id: FileId,
-        global_env: &eval::Environment,
+        global_env: &typecheck::Environment,
         lin_cache: &mut HashMap<FileId, Completed>,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>>;
 }
@@ -35,7 +34,7 @@ impl CacheExt for Cache {
     fn typecheck_with_analysis<'a>(
         &mut self,
         file_id: FileId,
-        global_env: &eval::Environment,
+        global_env: &typecheck::Environment,
         lin_cache: &mut HashMap<FileId, Completed>,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         if !self.terms_mut().contains_key(&file_id) {
diff --git a/lsp/nls/src/server.rs b/lsp/nls/src/server.rs
index c305455b..a4680ad0 100644
--- a/lsp/nls/src/server.rs
+++ b/lsp/nls/src/server.rs
@@ -16,8 +16,8 @@ use lsp_types::{
     TextDocumentSyncOptions, WorkDoneProgressOptions,
 };
 
-use nickel::typecheck::linearization::Completed;
-use nickel::{cache::Cache, environment::Environment, eval::Thunk, identifier::Ident};
+use nickel::cache::Cache;
+use nickel::typecheck::{linearization::Completed, Environment};
 
 use crate::{
     requests::{completion, goto, hover, symbols},
@@ -28,7 +28,7 @@ pub struct Server {
     pub connection: Connection,
     pub cache: Cache,
     pub lin_cache: HashMap<FileId, Completed>,
-    pub global_env: Environment<Ident, Thunk>,
+    pub global_env: Environment,
 }
 
 impl Server {
@@ -59,9 +59,9 @@ impl Server {
 
     pub fn new(connection: Connection) -> Server {
         let mut cache = Cache::new();
-        cache.prepare_stdlib().unwrap();
+        cache.load_stdlib().unwrap();
+        let global_env = cache.mk_types_env().unwrap();
         let lin_cache = HashMap::new();
-        let global_env = cache.mk_global_env().unwrap();
         Server {
             connection,
             cache,
diff --git a/src/cache.rs b/src/cache.rs
index 81ceb679..e50e2dc2 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -5,6 +5,7 @@ use crate::parser::lexer::Lexer;
 use crate::position::TermPos;
 use crate::stdlib as nickel_stdlib;
 use crate::term::{RichTerm, Term};
+use crate::typecheck;
 use crate::typecheck::{linearization::StubHost, type_check};
 use crate::{eval, parser, transformations};
 use codespan::{FileId, Files};
@@ -68,6 +69,26 @@ pub struct Cache {
     stdlib_ids: Option<Vec<FileId>>,
 }
 
+/// wrapping eval environment with typing environment
+#[derive(Debug, Clone)]
+pub struct GlobalEnv {
+    /// The eval environment.
+    pub eval_env: eval::Environment,
+    /// The typing environment, counterpart of the eval environment for typechecking. Entries are
+    /// [`TypeWrapper`](../typecheck/enum.TypeWrapper.html) for the ease of interacting with the
+    /// typechecker, but there are not any unification variable in it.
+    pub type_env: typecheck::Environment,
+}
+
+impl GlobalEnv {
+    pub fn new() -> Self {
+        GlobalEnv {
+            eval_env: eval::Environment::new(),
+            type_env: typecheck::Environment::new(),
+        }
+    }
+}
+
 #[derive(Debug, Clone, PartialEq)]
 pub struct CachedTerm {
     pub term: RichTerm,
@@ -385,7 +406,7 @@ impl Cache {
     pub fn typecheck(
         &mut self,
         file_id: FileId,
-        global_env: &eval::Environment,
+        global_env: &typecheck::Environment,
     ) -> Result<CacheOp<()>, CacheError<TypecheckError>> {
         match self.terms.get(&file_id) {
             Some(CachedTerm { state, .. }) if *state >= EntryState::Typechecked => {
@@ -577,7 +598,7 @@ impl Cache {
     pub fn prepare(
         &mut self,
         file_id: FileId,
-        global_env: &eval::Environment,
+        global_env: &typecheck::Environment,
     ) -> Result<CacheOp<()>, Error> {
         let mut result = CacheOp::Cached(());
 
@@ -622,7 +643,7 @@ impl Cache {
     pub fn prepare_nocache(
         &mut self,
         file_id: FileId,
-        global_env: &eval::Environment,
+        global_env: &typecheck::Environment,
     ) -> Result<(RichTerm, Vec<FileId>), Error> {
         let (term, errs) = self.parse_nocache(file_id)?;
         if errs.no_errors() {
@@ -754,7 +775,7 @@ impl Cache {
         if let Some(ids) = self.stdlib_ids.as_ref().cloned() {
             ids.iter()
                 .try_fold(CacheOp::Cached(()), |cache_op, file_id| {
-                    let global_env = self.mk_global_env().map_err(|err| match err {
+                    let global_env = self.mk_types_env().map_err(|err| match err {
                         CacheError::NotParsed => CacheError::NotParsed,
                         CacheError::Error(_) => unreachable!(),
                     })?;
@@ -770,8 +791,13 @@ impl Cache {
 
     /// Load, parse, and apply program transformations to the standard library. Do not typecheck
     /// for performance reason: this is done in the test suite.
-    pub fn prepare_stdlib(&mut self) -> Result<(), Error> {
+    /// Return a global environment containing both eval and type environment. If you need only the
+    /// type environment, use `load_stdlib()` then `mk_global_type` to avoid
+    /// transformations and evaluation preparation.
+    pub fn prepare_stdlib(&mut self) -> Result<GlobalEnv, Error> {
         self.load_stdlib()?;
+        let type_env = self.mk_types_env().unwrap();
+
         self.stdlib_ids
             .as_ref()
             .cloned()
@@ -782,18 +808,37 @@ impl Cache {
                 cache_err
                     .unwrap_error("cache::prepare_stdlib(): expected standard library to be parsed")
             })?;
-        Ok(())
+        let eval_env = self.mk_eval_env().unwrap();
+        Ok(GlobalEnv { eval_env, type_env })
     }
 
-    /// Generate a global environment from the list of `file_ids` corresponding to the standard
+    /// Generate a global typing environment from the list of `file_ids` corresponding to the standard
     /// library parts.
-    pub fn mk_global_env(&self) -> Result<eval::Environment, CacheError<Void>> {
-        if let Some(ids) = self.stdlib_ids.as_ref().cloned() {
-            let mut env = eval::Environment::new();
+    pub fn mk_types_env(&self) -> Result<typecheck::Environment, CacheError<Void>> {
+        let stdlib_terms_vec =
+            self.stdlib_ids
+                .as_ref()
+                .map_or(Err(CacheError::NotParsed), |ids| {
+                    Ok(ids
+                        .iter()
+                        .map(|file_id| {
+                            self.get_owned(*file_id).expect(
+                            "cache::mk_global_env(): can't build environment, stdlib not parsed",
+                        )
+                        })
+                        .collect())
+                })?;
+        Ok(typecheck::Envs::mk_global(stdlib_terms_vec).unwrap())
+    }
 
+    /// Generate a global evaluation environment from the list of `file_ids` corresponding to the standard
+    /// library parts.
+    pub fn mk_eval_env(&self) -> Result<eval::Environment, CacheError<Void>> {
+        if let Some(ids) = self.stdlib_ids.as_ref().cloned() {
+            let mut eval_env = eval::Environment::new();
             ids.iter().for_each(|file_id| {
                 let result = eval::env_add_term(
-                    &mut env,
+                    &mut eval_env,
                     self.get_owned(*file_id).expect(
                         "cache::mk_global_env(): can't build environment, stdlib not parsed",
                     ),
@@ -806,8 +851,7 @@ impl Cache {
                      )
                 }
             });
-
-            Ok(env)
+            Ok(eval_env)
         } else {
             Err(CacheError::NotParsed)
         }
diff --git a/src/program.rs b/src/program.rs
index e94e92eb..072b64f9 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -72,13 +72,9 @@ impl Program {
     /// Retrieve the parsed term and typecheck it, and generate a fresh global environment. Return
     /// both.
     fn prepare_eval(&mut self) -> Result<(RichTerm, eval::Environment), Error> {
-        self.cache.prepare_stdlib()?;
-        let global_env = self
-            .cache
-            .mk_global_env()
-            .expect("program::prepare_eval(): expected event to be ready");
-        self.cache.prepare(self.main_id, &global_env)?;
-        Ok((self.cache.get(self.main_id).unwrap(), global_env))
+        let GlobalEnv { eval_env, type_env } = self.cache.prepare_stdlib()?;
+        self.cache.prepare(self.main_id, &type_env)?;
+        Ok((self.cache.get(self.main_id).unwrap(), eval_env))
     }
 
     /// Parse if necessary, typecheck and then evaluate the program.
@@ -95,11 +91,7 @@ impl Program {
 
     /// Wrapper for [`query`](./fn.query.html).
     pub fn query(&mut self, path: Option<String>) -> Result<Term, Error> {
-        self.cache.prepare_stdlib()?;
-        let global_env = self
-            .cache
-            .mk_global_env()
-            .expect("program::prepare_eval(): expected event to be ready");
+        let global_env = self.cache.prepare_stdlib()?;
         query(&mut self.cache, self.main_id, &global_env, path)
     }
 
@@ -107,7 +99,7 @@ impl Program {
     pub fn typecheck(&mut self) -> Result<(), Error> {
         self.cache.parse(self.main_id)?;
         self.cache.load_stdlib()?;
-        let global_env = self.cache.mk_global_env().expect("program::typecheck(): stdlib has been loaded but was not found in cache on mk_global_env()");
+        let global_env = self.cache.mk_types_env().expect("program::typecheck(): stdlib has been loaded but was not found in cache on mk_types_env()");
         self.cache
             .resolve_imports(self.main_id)
             .map_err(|cache_err| {
@@ -148,10 +140,10 @@ impl Program {
 pub fn query(
     cache: &mut Cache,
     file_id: FileId,
-    global_env: &eval::Environment,
+    global_env: &GlobalEnv,
     path: Option<String>,
 ) -> Result<Term, Error> {
-    cache.prepare(file_id, global_env)?;
+    cache.prepare(file_id, &global_env.type_env)?;
 
     let t = if let Some(p) = path {
         // Parsing `y.path`. We `seq` it to force the evaluation of the underlying value,
@@ -175,7 +167,7 @@ pub fn query(
         cache.get_owned(file_id).unwrap()
     };
 
-    Ok(eval::eval_meta(t, global_env, cache)?)
+    Ok(eval::eval_meta(t, &global_env.eval_env, cache)?)
 }
 
 /// Pretty-print an error.
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index ff085b1c..bc3870bd 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -6,7 +6,7 @@
 //! Dually, the frontend is the user-facing part, which may be a CLI, a web application, a
 //! jupyter-kernel (which is not exactly user-facing, but still manages input/output and
 //! formatting), etc.
-use crate::cache::Cache;
+use crate::cache::{Cache, GlobalEnv};
 use crate::error::{Error, EvalError, IOError, ParseError, ParseErrors, REPLError};
 use crate::identifier::Ident;
 use crate::parser::{grammar, lexer, ExtendedTerm};
@@ -70,16 +70,12 @@ pub struct REPLImpl {
     cache: Cache,
     /// The parser, supporting toplevel let declaration.
     parser: grammar::ExtendedTermParser,
-    /// The eval environment. Contain the global environment with the stdlib, plus toplevel
+    /// The global environment. Contain the global environment with the stdlib, plus toplevel
     /// declarations and loadings made inside the REPL.
-    eval_env: eval::Environment,
-    /// The initial eval environment, without the toplevel declarations made inside the REPL. Used
+    env: GlobalEnv,
+    /// The initial type environment, without the toplevel declarations made inside the REPL. Used
     /// to typecheck imports in a fresh environment.
-    init_eval_env: eval::Environment,
-    /// The typing environment, counterpart of the eval environment for typechecking. Entries are
-    /// [`TypeWrapper`](../typecheck/enum.TypeWrapper.html) for the ease of interacting with the
-    /// typechecker, but there are not any unification variable in it.
-    type_env: typecheck::Environment,
+    init_type_env: typecheck::Environment,
 }
 
 impl REPLImpl {
@@ -88,20 +84,16 @@ impl REPLImpl {
         REPLImpl {
             cache: Cache::new(),
             parser: grammar::ExtendedTermParser::new(),
-            eval_env: eval::Environment::new(),
-            init_eval_env: eval::Environment::new(),
-            type_env: typecheck::Environment::new(),
+            env: GlobalEnv::new(),
+            init_type_env: typecheck::Environment::new(),
         }
     }
 
     /// Load and process the stdlib, and use it to populate the eval environment as well as the
     /// typing environment.
     pub fn load_stdlib(&mut self) -> Result<(), Error> {
-        self.cache.prepare_stdlib()?;
-
-        self.eval_env = self.cache.mk_global_env().unwrap();
-        self.init_eval_env = self.eval_env.clone();
-        self.type_env = typecheck::Envs::mk_global(&self.eval_env);
+        self.env = self.cache.prepare_stdlib()?;
+        self.init_type_env = self.env.type_env.clone();
         Ok(())
     }
 
@@ -134,10 +126,10 @@ impl REPLImpl {
                     self.cache.resolve_imports(*id).unwrap();
                 }
 
-                typecheck::type_check_in_env(&t, &self.type_env, &self.cache)?;
+                typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?;
                 for id in &pending {
                     self.cache
-                        .typecheck(*id, &self.init_eval_env)
+                        .typecheck(*id, &self.init_type_env)
                         .map_err(|cache_err| {
                             cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
                         })?;
@@ -150,7 +142,7 @@ impl REPLImpl {
                         .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
                 }
 
-                Ok(eval_function(t, &self.eval_env, &mut self.cache)?.into())
+                Ok(eval_function(t, &self.env.eval_env, &mut self.cache)?.into())
             }
             ExtendedTerm::ToplevelLet(id, t) => {
                 let (t, pending) = transformations::resolve_imports(t, &mut self.cache)?;
@@ -158,11 +150,11 @@ impl REPLImpl {
                     self.cache.resolve_imports(*id).unwrap();
                 }
 
-                typecheck::type_check_in_env(&t, &self.type_env, &self.cache)?;
-                typecheck::Envs::env_add(&mut self.type_env, id.clone(), &t);
+                typecheck::type_check_in_env(&t, &self.env.type_env, &self.cache)?;
+                typecheck::Envs::env_add(&mut self.env.type_env, id.clone(), &t);
                 for id in &pending {
                     self.cache
-                        .typecheck(*id, &self.init_eval_env)
+                        .typecheck(*id, &self.init_type_env)
                         .map_err(|cache_err| {
                             cache_err.unwrap_error("repl::eval_(): expected imports to be parsed")
                         })?;
@@ -175,8 +167,8 @@ impl REPLImpl {
                         .unwrap_or_else(|_| panic!("repl::eval_(): expected imports to be parsed"));
                 }
 
-                let local_env = self.eval_env.clone();
-                eval::env_add(&mut self.eval_env, id.clone(), t, local_env);
+                let local_env = self.env.eval_env.clone();
+                eval::env_add(&mut self.env.eval_env, id.clone(), t, local_env);
                 Ok(EvalResult::Bound(id))
             }
         }
@@ -219,8 +211,8 @@ impl REPL for REPLImpl {
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
-        typecheck::Envs::env_add_term(&mut self.type_env, &term).unwrap();
-        eval::env_add_term(&mut self.eval_env, term.clone()).unwrap();
+        typecheck::Envs::env_add_term(&mut self.env.type_env, &term).unwrap();
+        eval::env_add_term(&mut self.env.eval_env, term.clone()).unwrap();
 
         Ok(term)
     }
@@ -233,11 +225,11 @@ impl REPL for REPLImpl {
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
-        typecheck::type_check_in_env(&term, &self.type_env, &self.cache)?;
+        typecheck::type_check_in_env(&term, &self.env.type_env, &self.cache)?;
 
         Ok(typecheck::apparent_type(
             term.as_ref(),
-            Some(&typecheck::Envs::from_global(&self.type_env)),
+            Some(&typecheck::Envs::from_global(&self.env.type_env)),
         )
         .into())
     }
@@ -246,7 +238,7 @@ impl REPL for REPLImpl {
         use crate::program;
 
         let file_id = self.cache.add_tmp("<repl-query>", String::from(exp));
-        program::query(&mut self.cache, file_id, &self.eval_env, None)
+        program::query(&mut self.cache, file_id, &self.env, None)
     }
 
     fn cache_mut(&mut self) -> &mut Cache {
diff --git a/src/term.rs b/src/term.rs
index c69fadbb..cf7508c0 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -146,6 +146,12 @@ pub enum Term {
     ParseError,
 }
 
+impl From<MetaValue> for Term {
+    fn from(m: MetaValue) -> Self {
+        Term::MetaValue(m)
+    }
+}
+
 #[derive(Debug, Eq, PartialEq, Copy, Clone)]
 pub struct RecordAttrs {
     pub open: bool,
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 1a49fa69..61d000e5 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -43,7 +43,6 @@
 use crate::cache::ImportResolver;
 use crate::environment::Environment as GenericEnvironment;
 use crate::error::TypecheckError;
-use crate::eval;
 use crate::identifier::Ident;
 use crate::label::ty_path;
 use crate::position::TermPos;
@@ -353,6 +352,11 @@ pub struct Envs<'a> {
     local: Environment,
 }
 
+#[derive(Clone, Debug)]
+pub enum EnvBuildError {
+    NotARecord(RichTerm),
+}
+
 impl<'a> Envs<'a> {
     /// Create an `Envs` value with an empty local environment from a global environment.
     pub fn from_global(global: &'a Environment) -> Self {
@@ -371,23 +375,29 @@ impl<'a> Envs<'a> {
         }
     }
 
-    /// Populate a new global typing environment from a global term environment.
-    pub fn mk_global(eval_env: &eval::Environment) -> Environment {
-        eval_env
+    /// Populate a new global typing environment from a `Vec` of parsed files.
+    pub fn mk_global(envs: Vec<RichTerm>) -> Result<Environment, EnvBuildError> {
+        Ok(envs
             .iter()
-            .map(|(id, thunk)| {
-                (
-                    id.clone(),
-                    apparent_type(thunk.borrow().body.as_ref(), None).into(),
-                )
+            .map(|rt| {
+                if let Term::RecRecord(rec, ..) = rt.as_ref() {
+                    Ok(rec
+                        .iter()
+                        .map(|(id, rt)| (id.clone(), infer_type(rt.as_ref()))))
+                } else {
+                    Err(EnvBuildError::NotARecord(rt.clone()))
+                }
             })
-            .collect()
+            .collect::<Result<Vec<_>, EnvBuildError>>()?
+            .into_iter()
+            .flatten()
+            .collect())
     }
 
     /// 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<(), eval::EnvBuildError> {
+    pub fn env_add_term(env: &mut Environment, rt: &RichTerm) -> Result<(), EnvBuildError> {
         let RichTerm { term, pos } = rt;
 
         match term.as_ref() {
@@ -400,10 +410,7 @@ impl<'a> Envs<'a> {
 
                 Ok(())
             }
-            t => Err(eval::EnvBuildError::NotARecord(RichTerm::new(
-                t.clone(),
-                *pos,
-            ))),
+            t => Err(EnvBuildError::NotARecord(RichTerm::new(t.clone(), *pos))),
         }
     }
 
@@ -452,7 +459,7 @@ pub struct State<'a> {
 /// file. It however still needs the resolver to get the apparent type of imports.
 pub fn type_check<L>(
     t: &RichTerm,
-    global_eval_env: &eval::Environment,
+    global_env: &Environment,
     resolver: &impl ImportResolver,
     mut linearizer: impl Linearizer<L, (UnifTable, HashMap<usize, Ident>)>,
 ) -> Result<(Types, Completed), TypecheckError>
@@ -461,7 +468,6 @@ where
 {
     let (mut table, mut names) = (UnifTable::new(), HashMap::new());
     let mut building = Linearization::building();
-    let global = Envs::mk_global(global_eval_env);
     let ty = TypeWrapper::Ptr(new_var(&mut table));
 
     {
@@ -474,7 +480,7 @@ where
 
         type_check_(
             &mut state,
-            Envs::from_global(&global),
+            Envs::from_global(&global_env),
             &mut building,
             linearizer.scope(linearization::ScopeId::Right),
             false,
@@ -1023,6 +1029,30 @@ pub fn apparent_type(t: &Term, envs: Option<&Envs>) -> ApparentType {
     }
 }
 
+/// Infer type of a more complex structure.
+/// For now, it's implemented only to infer the type of a non annotated record by gathering the apparent type of the fields.
+/// It's used essentially to type the stdlib.
+pub fn infer_type(t: &Term) -> TypeWrapper {
+    match t {
+        Term::Record(rec, ..) | Term::RecRecord(rec, ..) => AbsType::StaticRecord(Box::new(
+            TypeWrapper::Concrete(rec.iter().fold(AbsType::RowEmpty(), |r, (id, rt)| {
+                AbsType::RowExtend(
+                    id.clone(),
+                    Some(Box::new(infer_type(rt.term.as_ref()))),
+                    Box::new(r.into()),
+                )
+            })),
+        ))
+        .into(),
+        Term::MetaValue(MetaValue {
+            value: Some(rt),
+            types: None,
+            ..
+        }) => infer_type(rt.as_ref()),
+        t => apparent_type(t, None).into(),
+    }
+}
+
 /// The types on which the unification algorithm operates, which may be either a concrete type, a
 /// type constant or a unification variable.
 #[derive(Clone, PartialEq, Debug)]


Test patch:
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 38885827..f6e7d46a 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -170,6 +170,15 @@ let typecheck = [
 
   // recursive_records_quoted
   {"foo" = 1} : {foo : Num},
+
+  // stdlib typechecking:
+  strings.length : Str -> Num,
+  (strings.length "Ok") : Num,
+  (strings.length "Ok" == 2) : Bool,
+  // partial application
+  (strings.split ".") : Str -> List Str,
+  // TODO: fix issue with `forall`
+  // (lists.length [] == 0) : Bool,
 ] in
 
 true