Proper type instantiation discipline (#1473)

* Proper type instantiation discipline

This commit is the last missing piece (at least for the time being)
toward a reasonable bidirectional typechecking algorithm that properly
handle higher-rank types.

Instantiation of polymorphic types has been ad-hoc and full of issues.
Simple programs such as:

```nickel
let r : { id : forall a. a -> a } = { id = fun r => r } in
r.id "x"
```

or

```nickel
let eval : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
(eval (fun x => x) 1) : Number
```

wouldn't typecheck. Previously introduced variable levels were required
before we could change that.

This commit is building on the variable level to use a proper
instantiation discipline from the specification of the Nickel type
system located in this repository, and the original inspiration, [A
Quick Look at Impredicativity]() (although type instantiation is
currently predicative, the general structure of the bidirectional
type system is similar). Doing so, we also move code between `check` and
`infer` to better reflect the specification: `infer` is not
wrapper around check + unification anymore, but it actually implements
infer rules (function application, primop application, variable and annotation).

Instantiation is taken care of when switching from infer mode to check
mode within `subsumption` and at function application.

* Add test for unsound generalization

And fix the error expectation for `TypecheckError::VarLevelMismatch`
that still had the old longer name `VariableLevelMismatch`.

* Update core/tests/integration/main.rs

Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>

* Update core/src/typecheck/mod.rs

* Update core/src/typecheck/mod.rs

* Post-rebase fixup + clippy warnings

* Formatting of Nickel test files

---------

Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>

core/src/term/mod.rs

@@ -513,6 +513,7 @@ impl TypeAnnotation {
             .collect::<Result<Vec<_>, _>>()
     }
 
+    /// Set the `field_name` attribute of the labels of the type and contracts annotations.
     pub fn with_field_name(self, field_name: Option<Ident>) -> Self {
         TypeAnnotation {
             typ: self.typ.map(|t| t.with_field_name(field_name)),
@@ -523,6 +524,12 @@ impl TypeAnnotation {
                 .collect(),
         }
     }
+
+    /// Return `true` if this annotation is empty, i.e. hold neither a type annotation nor
+    /// contracts annotations.
+    pub fn is_empty(&self) -> bool {
+        self.typ.is_none() && self.contracts.is_empty()
+    }
 }
 
 impl From<TypeAnnotation> for LetMetadata {

core/tests/integration/main.rs

@@ -163,10 +163,12 @@ enum ErrorExpectation {
     TypecheckExtraDynTail,
     #[serde(rename = "TypecheckError::MissingDynTail")]
     TypecheckMissingDynTail,
+    #[serde(rename = "TypecheckError::ArrowTypeMismatch")]
+    TypecheckArrowTypeMismatch { sub_error: Box<ErrorExpectation> },
     #[serde(rename = "TypecheckError::FlatTypeInTermPosition")]
     TypecheckFlatTypeInTermPosition,
-    #[serde(rename = "TypecheckError::VariableLevelMismatch")]
-    TypecheckVariableLevelMismatch { type_var: String },
+    #[serde(rename = "TypecheckError::VarLevelMismatch")]
+    TypecheckVarLevelMismatch { type_var: String },
     #[serde(rename = "ParseError")]
     AnyParseError,
     #[serde(rename = "ParseError::DuplicateIdentInRecordPattern")]
@@ -287,11 +289,20 @@ impl PartialEq<Error> for ErrorExpectation {
                 _ => false,
             },
             (
-                TypecheckVariableLevelMismatch { type_var: ident },
+                TypecheckVarLevelMismatch { type_var: ident },
                 Error::TypecheckError(TypecheckError::VarLevelMismatch {
                     type_var: constant, ..
                 }),
             ) => ident == constant.label(),
+            // The clone is not ideal, but currently we can't compare `TypecheckError` directly
+            // with an ErrorExpectation. Ideally, we would implement `eq` for all error subtypes,
+            // and have the eq with `Error` just dispatch to those sub-eq functions.
+            (
+                TypecheckArrowTypeMismatch {
+                    sub_error: sub_error1,
+                },
+                Error::TypecheckError(TypecheckError::ArrowTypeMismatch(_, _, _, sub_error2, _)),
+            ) => sub_error1.as_ref() == &Error::TypecheckError((**sub_error2).clone()),
             (_, _) => false,
         }
     }
@@ -352,9 +363,12 @@ impl std::fmt::Display for ErrorExpectation {
             }
             TypecheckExtraDynTail => "TypecheckError::ExtraDynTail".to_owned(),
             TypecheckMissingDynTail => "TypecheckError::MissingDynTail".to_owned(),
+            TypecheckArrowTypeMismatch { sub_error } => {
+                format!("TypecheckError::ArrowTypeMismatch{sub_error})")
+            }
             TypecheckFlatTypeInTermPosition => "TypecheckError::FlatTypeInTermPosition".to_owned(),
-            TypecheckVariableLevelMismatch { type_var: ident } => {
-                format!("TypecheckError::VariableLevelMismatch({ident})")
+            TypecheckVarLevelMismatch { type_var: ident } => {
+                format!("TypecheckError::VarLevelMismatch({ident})")
             }
             SerializeNumberOutOfRange => "ExportError::NumberOutOfRange".to_owned(),
         };

core/tests/integration/typecheck/fail/mismatch_array_typed_entry.ncl

@@ -6,5 +6,5 @@
 #
 # [test.metadata.expectation]
 # expected = 'String'
-# found = 'Dyn'
-[(1 : String), true, "b"] : Array Dyn
+# found = 'Number'
+[(1 : String), true, "b"] : Array Dyn

core/tests/integration/typecheck/fail/unsound_generalization_enum_rows.ncl

@@ -2,16 +2,19 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'tail'
-(fun tag =>
-  let foo = tag
-    |> match { 
+(
+  fun tag =>
+    let foo =
+      tag
+      |> match {
         _ => null,
-    }
-  in
-  let g : forall tail. [| ; tail |] = tag in
-  g
+      }
+    in
+    let g : forall tail. [|; tail |] = tag in
+    g
 ) : _
+

core/tests/integration/typecheck/fail/unsound_generalization_fun.ncl

@@ -2,8 +2,9 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'c'
 (fun x => let y : forall c d. c -> d = fun z => x z in y) : _
+

core/tests/integration/typecheck/fail/unsound_generalization_monomorphic_id.ncl

@@ -0,0 +1,20 @@
+# test.type = 'error'
+# eval = 'typecheck'
+#
+# [test.metadata]
+# error = 'TypecheckError::ArrowTypeMismatch'
+#
+# [test.metadata.expectation.sub_error]
+# error = 'TypecheckError::VarLevelMismatch'
+#
+# [test.metadata.expectation.sub_error.expectation]
+# type_var = 'b'
+(
+  let eval : forall a. (forall b. b -> b) -> a -> a = fun f x => f x
+    in
+  # because g isn't annotated, it doesn't get a polymorphic type, but a
+  # monomorphic _a -> _a
+  let g = fun x => x
+  in eval g
+) : _
+

core/tests/integration/typecheck/fail/unsound_generalization_record_rows.ncl

@@ -2,8 +2,14 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'tail'
-(fun r => let foo = r.foo in let g : forall tail. {foo : _; tail} = r in g.baz) : _
+(
+  fun r =>
+    let foo = r.foo in
+    let g : forall tail. { foo : _; tail } = r in
+    g.baz
+) : _
+

core/tests/integration/typecheck/fail/unsound_generalization_simple.ncl

@@ -2,8 +2,9 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'a'
 (fun x => let y : forall a. a = x in y) : _
+

core/tests/integration/typecheck/pass/forall_inside_row_type.ncl

@@ -0,0 +1,6 @@
+# test.type = 'pass'
+# eval = 'typecheck'
+
+# regression test for https://github.com/tweag/nickel/issues/1027
+let r : { id : forall a. a -> a } = { id = fun r => r } in
+r.id "x"

core/tests/integration/typecheck/pass/higher_rank_coeval.ncl

@@ -0,0 +1,12 @@
+# test.type = 'pass'
+# eval = 'typecheck'
+let co_eval : ((forall a. a -> a) -> Number) -> Number = (
+    (
+      fun eval =>
+        let id : forall b. b -> b = fun y => y
+          in eval id
+    )
+  )
+  in
+(co_eval (fun id => id 3)) : _
+

core/tests/integration/typecheck/pass/higher_rank_eval.ncl

@@ -0,0 +1,6 @@
+# test.type = 'pass'
+# eval = 'typecheck'
+let eval : forall a. (forall b. b -> b) -> a -> a = fun f x => f x
+  in
+(eval (fun x => x)) : _
+