Repository: tweag/nickel (rust)

Issue:
Implement a proper bidirectional algorithm
**Is your feature request related to a problem? Please describe.**
The current implementation of the typechecker is more or less based on a bidirectional typechecking algorithm, but mixes both inference, checking and a third nickel-specific mode, the non-strict mode (where we just walk the AST looking for the next statically typed block to handle). The information flow is not always clear, the algorithm is hard to extend, and some edge cases are not handled well (higher rank types checking and polymorphic type instantiation, mainly). A proper bidirectional algorithm would make it easier to add subtyping as well, with the relation induced by `T <: Dyn`, for example. The walking phase is also wasteful: we continue to generate unification variable, but just don't actually unify them. 

**Describe the solution you'd like**
Have a formal bidirectional formulation of the type system on paper. Implement it and break the `type_check_` function into three mutually recursive functions (or, constraints generating function later, if this is too stack-hungry), `walk`, `infer` and `check`, with clear roles and information flow.

**Additional context**
Such an enterprise was already tried in #392, but it hit some non-trivial issues with polymorphic instantiation and order of arguments (dubbed the "tabby-first problem" in section 5.1 of [Krishnaswami and Dunfield](https://arxiv.org/abs/1908.05839)). A first step could be to forget about `Dyn`-induced subtying for now, and adapt [Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism](https://arxiv.org/abs/1306.6032), which doesn't have this issue.


Pull request:
Fix instantiation of polymorphic functions accessed from a record
Fix the last avatar of #375. Currently the polymorphic functions from the stdlib can't be used in typed code, because they are not instantiated correctly:

```
nickel>(lists.map (fun x => x + 1) [1,2,3]) : List Num
error: Type mismatch
...
```

The general issue is not stdlib-specific, but has to do with a polymorphic function accessed from a record being the head of an application. If we use a variable as a gateway, then it works again:

```
nickel>(let m = lists.map in m (fun x => x + 1) [1,2,3]) : List Num
[2,3,4]
```

This PR fixes the issue by always instantiating the type resulting from the application of a unary operator (which record access is), and by re-ordering the information flow to check the final result type only after we've instantiated potential heading foralls.

To be honest, this is quite ad-hoc (it arbitrarily only covers the case of unary operators): the proper fix is to close #584, but in the meantime, those few lines of diff allow us to use the functions from the stdlib in typed code and relegate the issue to edge cases that, I hope, are much rarer.

Patch:
diff --git a/examples/lists/lists.ncl b/examples/lists/lists.ncl
index be4a275e..d3f52473 100644
--- a/examples/lists/lists.ncl
+++ b/examples/lists/lists.ncl
@@ -1,19 +1,12 @@
 // Example list functions. This code is illustrative: prefer using the list
 // stdlib functions `lists.map` and `lists.fold` instead.
 let my_list_lib = {
-  // We have to wrap `head` and `tail` with the right annotations if we want our
-  // map and fold to be statically typed. This is due to a current issue with
-  // the how the stdlib is typed, see
-  // https://github.com/tweag/nickel/issues/226. It won't be needed eventually.
-  head | forall a. List a -> a = fun l => %head% l,
-  tail | forall a. List a -> List a = fun l => %tail% l,
-
   map : forall a b. (a -> b) -> List a -> List b = fun f list =>
     if list == [] then
       []
     else
-      let head = head list in
-      let tail = tail list in
+      let head = lists.head list in
+      let tail = lists.tail list in
       [f head] @ map f tail,
 
   fold : forall a b. (a -> b -> b) -> List a -> b -> b =
@@ -21,7 +14,9 @@ let my_list_lib = {
         if list == [] then
           first
         else
-          f (head list) (fold f (tail list) first),
+          let head = lists.head list in
+          let tail = lists.tail list in
+          f head (fold f tail first),
 } in
 // Compute `7!`
 let l = my_list_lib.map (fun x => x+1) [1, 2, 3, 4, 5, 6] in
diff --git a/lsp/nls/src/linearization/completed.rs b/lsp/nls/src/linearization/completed.rs
index 057b85df..4894d809 100644
--- a/lsp/nls/src/linearization/completed.rs
+++ b/lsp/nls/src/linearization/completed.rs
@@ -111,7 +111,7 @@ impl Completed {
             TermKind::Usage(UsageState::Resolved(usage)) => {
                 usage.and_then(|u| self.get_item(u)).unwrap_or(item)
             }
-            TermKind::Declaration(_, _) => self.get_item(item.id).unwrap_or(item),
+            TermKind::Declaration(_, _) => self.get_item(item.id + 1).unwrap_or(item),
             _ => item,
         };
 
diff --git a/lsp/nls/src/linearization/mod.rs b/lsp/nls/src/linearization/mod.rs
index 29f6d383..1ec0f0a2 100644
--- a/lsp/nls/src/linearization/mod.rs
+++ b/lsp/nls/src/linearization/mod.rs
@@ -139,40 +139,8 @@ impl Linearizer for AnalysisHost {
 
         let id = id_gen.get();
         match term {
-            Term::FunPattern(ident, destruct, _) => {
-                if let Some(ident) = ident {
-                    self.env.insert(ident.to_owned(), id);
-                    lin.push(LinearizationItem {
-                        id: id_gen.get_and_advance(),
-                        ty,
-                        pos: ident.pos.unwrap(),
-                        scope: self.scope.clone(),
-                        kind: TermKind::Declaration(ident.to_owned(), Vec::new()),
-                        meta: self.meta.take(),
-                    });
-                }
-                for matched in destruct.to_owned().inner() {
-                    let (ident, term) = matched.as_meta_field();
-                    self.env.insert(ident.to_owned(), id_gen.get());
-                    lin.push(LinearizationItem {
-                        id: id_gen.get_and_advance(),
-                        // TODO: get type from pattern
-                        ty: TypeWrapper::Concrete(AbsType::Dyn()),
-                        pos: ident.pos.unwrap(),
-                        scope: self.scope.clone(),
-                        kind: TermKind::Declaration(ident.to_owned(), Vec::new()),
-                        meta: match &*term.term {
-                            Term::MetaValue(meta) => Some(MetaValue {
-                                value: None,
-                                ..meta.clone()
-                            }),
-                            _ => None,
-                        },
-                    });
-                }
-            }
             Term::Let(ident, _, _, _) | Term::Fun(ident, _) => {
-                self.env.insert(ident.to_owned(), id);
+                self.env.insert(ident.to_owned(), lin.linearization.len());
                 lin.push(LinearizationItem {
                     id,
                     ty,
diff --git a/scripts/channel_beta.toml b/scripts/channel_beta.toml
index f80029dd..29b5bb72 100644
--- a/scripts/channel_beta.toml
+++ b/scripts/channel_beta.toml
@@ -1,3 +1,3 @@
 channel="beta"
-date="2022-01-20"
-sha256="sha256-knwb680axCRe2NFA/VbRhKD0XGCbWxY+YqF+s3miCCE="
+date="2022-01-14"
+sha256="sha256-Qsf9R7GoiSyfgMWS7PfYASHL/B/VmAC5gd6uB5k0dGQ="
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index a782905e..c4d3cb3b 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -593,8 +593,6 @@ fn type_check_<L: Linearizer>(
         Term::Op1(op, t) => {
             let (ty_arg, ty_res) = get_uop_type(state, op)?;
 
-            unify(state, strict, ty, ty_res)
-                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
             type_check_(
                 state,
                 envs.clone(),
@@ -603,7 +601,11 @@ fn type_check_<L: Linearizer>(
                 strict,
                 t,
                 ty_arg,
-            )
+            )?;
+
+            let instantiated = instantiate_foralls(state, ty_res, ForallInst::Ptr);
+            unify(state, strict, ty, instantiated)
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Op2(op, t1, t2) => {
             let (ty_arg1, ty_arg2, ty_res) = get_bop_type(state, op)?;


Test patch:
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 04582eee..85a47dd0 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -4,7 +4,7 @@ let typecheck = [
   false : Bool,
   0 : Num,
   45 : Num,
-  fun x => x : forall a. a -> a,
+  (fun x => x) : forall a. a -> a,
   let x = 3 in (x : Num),
   4 + false,
   (true | Num) : Num,
@@ -82,7 +82,7 @@ let typecheck = [
   let r : {bla : Bool, blo : Num} = {blo = 1, bla = true} in
     ((if r.bla then r.blo else 2) : Num),
 
-  let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
+  let f : forall a r. {bla : Bool, blo : a, ble : a | r} -> a =
       fun r => if r.bla then r.blo else r.ble in
     (if (f {bla = true, blo = false, ble = true, blip = 1, }) then
       (f {bla = true, blo = 1, ble = 2, blip = `blip, })
@@ -181,8 +181,8 @@ let typecheck = [
   (strings.length "Ok" == 2) : Bool,
   // partial application
   (strings.split ".") : Str -> List Str,
-  // TODO: fix issue with `forall`
-  // (lists.length [] == 0) : Bool,
+  (lists.length [] == 0) : Bool,
+  (lists.map (fun x => x ++ "1") ["a", "b", "c"]) : List Str,
 ] in
 
 true