Repository: tweag/nickel
Pull request #684 (2022-04-24 00:09:37)

flake.lock: Update
Automated changes by the [update-flake-lock](https://github.com/DeterminateSystems/update-flake-lock) GitHub Action.

```
Flake lock file updates:

• Updated input 'nixpkgs':
    'github:NixOS/nixpkgs/75ad56bdc927f3a9f9e05e3c3614c4c1fcd99fcb' (2022-04-16)
  → 'github:NixOS/nixpkgs/bc41b01dd7a9fdffd32d9b03806798797532a5fe' (2022-04-23)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/d154de7dae2da8b52084ddbfe95ce6e5b0ba0a37' (2022-04-16)
  → 'github:oxalica/rust-overlay/d10f36b093459eb71ddcfedbab538c1ae3dfebb2' (2022-04-23)
```

### Running GitHub Actions on this PR

GitHub Actions will not run workflows on pull requests which are opened by a GitHub Action.

To run GitHub Actions workflows on this PR, run:

```sh
git branch -D update_flake_lock_action
git fetch origin
git checkout update_flake_lock_action
git commit --amend --no-edit
git push origin update_flake_lock_action --force
```


Patch:
diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml
index 7cb60c92..01cacdd4 100644
--- a/.github/workflows/update-flake-lock.yml
+++ b/.github/workflows/update-flake-lock.yml
@@ -16,4 +16,4 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - name: Update flake.lock
-        uses: DeterminateSystems/update-flake-lock@v9
+        uses: DeterminateSystems/update-flake-lock@v8
diff --git a/RATIONALE.md b/RATIONALE.md
index f563f28d..d9c324f0 100644
--- a/RATIONALE.md
+++ b/RATIONALE.md
@@ -1,4 +1,5 @@
-# Why Nickel ?
+Why Nickel ?
+============
 
 There already exist quite a few languages with a similar purpose to Nickel:
 [CUE](https://cuelang.org/), [Dhall](https://dhall-lang.org/),
@@ -32,7 +33,6 @@ alternatives.
 ## Design rationale
 
 ### Functions
-
 The main contribution of a configuration language over a static configuration is
 *abstraction*: make the same code reusable in different contexts by just varying
 some inputs, instead of pasting variations of the same chunks all over the
@@ -48,7 +48,6 @@ first-class: they can be created everywhere, passed around as any other value,
 and called at will.
 
 ### Typing
-
 One recurring difference between Nickel and other configuration languages is
 that Nickel has a static type system. The trade-offs of static typing for
 configurations are different than in the case of a general purpose programming
@@ -57,7 +56,6 @@ language.
 #### Reusable versus specific code
 
 We can divide code in two categories:
-
 1. Configuration-specific code: local code that will only be used for the
    generation of said configuration.
 2. Reusable code: code that is used in several configurations and will be
@@ -71,11 +69,9 @@ require annotations and forbids correct but non typable code, while not really
 adding value.
 
 On the other hand, reusable code may be called on infinitely many different inputs:
-
-```nickel
+```
 let f x = fun x => if x < 1000 then x + 1 else x ++ 2
 ```
-
 In this contrived but illustrative example, `f` can work fine on a thousand
 inputs, but fails on the next one. Functions in general can never be tested
 exhaustively.  Meanwhile, static typing would catch the typo `x ++ 2` even
@@ -84,7 +80,6 @@ before the first usage.
 To this problem, Nickel offers the solution of a gradual type system which
 supports a mix of both typed and non typed parts, with the following
 perks:
-
 - You get to chose when to use static typing or not.
 - You can write code without any type annotation even when calling to statically
   typed code.
@@ -112,15 +107,13 @@ specification dictated by this tool, which is a priori alien to the generating
 program.
 
 In the following example,
-
-```json
+```
 {
   ...
-  "id": "www.github.com/nickel/back",
-  "baseURL": 2
+  id: "www.github.com/nickel/back",
+  baseURL: 2,
 }
 ```
-
 the configuration language has no reason to suspect that `id` and `baseURL`
 contents have been mistakingly swapped. It would need to be aware of the fact
 that `id` should be an integer and `baseURL` a string. Surely, an error will
@@ -140,7 +133,6 @@ can for example ensure that `baseURL` is not only a string but a valid URL, and
 document that it should be the Github homepage of a project.
 
 ### Turing completeness
-
 All listed languages but Jsonnet forbid general recursion, and are hence non
 Turing-complete. The idea is that generating configuration should always
 terminate, and combinators on collections (e.g. `map` or `fold`) - or equivalent
@@ -156,7 +148,6 @@ functionalities \[2\].
 \[2\]: [Turing incomplete languages](http://www.haskellforall.com/2020/01/why-dhall-advertises-absence-of-turing.html)
 
 ### Side-Effects
-
 As for Turing-completeness, most of these languages also forbid side-effects.
 Side-effects suffer from general drawbacks: they make code harder to reason
 about, to compose, to refactor and to parallelize. In general-purpose
@@ -182,12 +173,9 @@ externally the associated effect handlers in order to customize Nickel for
 specific use-cases.
 
 ## Comparison with alternatives
-
-Let's compare Nickel with the languages cited at the beginning: Starlark, Dhall,
-CUE and Jsonnet.
+Let's compare Nickel with the languages cited at the beginning: Starlark, Dhall, CUE and Jsonnet.
 
 ### Starlark: the standard package
-
 Starlark is a language originally designed for the [Bazel](https://bazel.build/)
 build system, but it can also be used independently as a configuration language.
 It is a dialect of Python and includes the following classical features:
@@ -197,7 +185,6 @@ It is a dialect of Python and includes the following classical features:
 - Dynamic typing: no type annotations
 
 With the following restrictions:
-
 - No recursion: the language is not Turing-complete
 - No side-effects: execution cannot access the file system, network or system clock.
 
@@ -205,20 +192,18 @@ In summary, Starlark comes with a sensible basic set of capabilities which is
 good enough to enable the writing of parametrizable and reusable configurations.
 
 ### Starlark vs Nickel
-
 Starlark forbids recursion and side-effects which are allowed in Nickel. It
 lacks a static type system, which hampers the ability to write robust library
 code and prevents the expression of data schemas inside the language.
 
 ### Dhall: powerful type system
-
 Dhall is heavily inspired by Nix, to which it adds a [powerful type
 system](https://github.com/dhall-lang/dhall-lang/blob/master/standard/README.md#summary).
 Because of its complexity, the type system only supports a limited type
 inference.  This can lead to code that is sometimes heavy on type annotations,
 as in the following example:
 
-```dhall
+```
 let filterOptional
     : ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b
     =   λ(a : Type)
@@ -254,23 +239,19 @@ JSON](#typing-json). Typically, Dhall lists must be homogeneous: all elements
 must have the same type. In particular, you can't represent directly the
 following list of objects with different structure, which is valid JSON `[{a:
 1}, {b: 2}]`. One has to write:
-
-```dhall
+```
 let Union = < Left : {a : Natural} | Right : {b : Natural} >
 in [Union.Left {a = 1}, Union.Right {b = 2}]
 ```
-
 and write boilerplate code accordingly when manipulating this list.
 
 ### Dhall vs Nickel
-
 Dhall is entirely statically typed, with an expressive but complex type system.
 It requires type annotations, and may add boilerplate for code that is hard to
 type, while Nickel prefers the mixed approach of gradual typing. As Starlark,
 and as opposed to Nickel, Dhall forbids recursion and side-effects.
 
 ### CUE: opinionated data validation
-
 CUE is quite a different beast. It focuses on data validation rather than
 boilerplate removal. To do so, it sacrifices flexibility by not supporting not
 only general recursion, but even general functions, in exchange of a
@@ -280,7 +261,6 @@ inhabitant. These types form a lattice, which means they come with a union and
 an intersection operation.
 
 This provides:
-
 - Merging: combine mixed schemas and values together in a well behaved way
   (merge is commutative, everywhere defined and idempotent)
 - Querying: synthesize values inhabiting a type
@@ -291,27 +271,23 @@ although the flexibility of Nickel necessarily makes the two system behave
 differently.
 
 ### CUE vs Nickel
-
 CUE is an outsider. While it produces elegant code, is backed by a solid theory
 and is excellent at data validation, it seems less adapted to generating
 configuration in general. It is also heavily constrained, which might be
 limiting for specific use-cases.
 
 ### Jsonnet: JSON, functions and inheritance
-
 In this list, Jsonnet is arguably the closest language to Nickel. As Nickel, it
 is a JSON with higher-order functions, recursion and lazy evaluation. It
 features a simplified object system with inheritance, which achieves similar
 functionalities to Nickel's merge system.
 
 ### Jsonnet vs Nickel
-
 The main difference between Jsonnet and Nickel are types. Jsonnet does not
 feature static types, contracts or enriched values, and thus can't type library
 code and has no principled approach to data validation.
 
 ### Summary
-
 | Language | Typing                        | Recursion | Evaluation | Side-effects                                      |
 |----------|-------------------------------|-----------|------------|---------------------------------------------------|
 | Nickel   | Gradual (dynamic + static)    | Yes       | Lazy       | Yes (constrained)                                 |
@@ -321,7 +297,6 @@ code and has no principled approach to data validation.
 | Jsonnet  | Dynamic                       | Yes       | Lazy       | No                                                |
 
 ## Conclusion
-
 We outlined our motivations for creating Nickel, our main design choices and why
 we made them. To give an idea of the position of Nickel in the ecosystem, we
 compared it to a handful of related languages.  They are all very well designed
diff --git a/benches/numeric/fibonacci.ncl b/benches/numeric/fibonacci.ncl
index 1971b4bd..1cc55f6f 100644
--- a/benches/numeric/fibonacci.ncl
+++ b/benches/numeric/fibonacci.ncl
@@ -1,9 +1,9 @@
 {
-  run =
-    let rec f = fun n =>
-      if n == 0 || n == 1 then
-        1
-      else
-        f (n - 1) + f (n - 2)
-    in f
+  run = {
+      f = fun n =>
+        if n == 0 || n == 1 then
+          1
+        else
+          f (n - 1) + f (n - 2)
+    }.f
 }
diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md
index 96a3b749..8e747f1c 100644
--- a/doc/manual/syntax.md
+++ b/doc/manual/syntax.md
@@ -328,8 +328,7 @@ Examples:
 ```
 
 ### Let-In
-Let-in allows the binding of an expression. It is used as `let <rec?> <ident> = <expr> in <expr>`.
-The `rec` keyword in Let-in constructs allows the let binding to become recursive, enabling the use of the `<ident>` within the first `<expr>`.
+Let-in allows the binding of an expression. It is used as `let <ident> = <expr> in <expr>`.
 
 Examples:
 ```
@@ -341,15 +340,6 @@ true
 
 > let a = 1 in let b = 2 in a + b
 3
-
-> let rec f = fun n => if n == 0 then n else n + f (n - 1) in f 10
-55
-
-> let rec fib = fun n => if n <= 2 then 1 else fib (n - 1) + fib (n - 2) in fib 9
-34
-
-> let rec repeat = fun n x => if n <= 0 then [] else repeat (n - 1) x @ [x] in repeat 3 "foo"
-["foo", "foo", "foo"]
 ```
 
 ## Functions
diff --git a/examples/fibonacci/README.md b/examples/fibonacci/README.md
index 13d63a17..b63e6e05 100644
--- a/examples/fibonacci/README.md
+++ b/examples/fibonacci/README.md
@@ -3,6 +3,9 @@
 This is a basic example of a recursive function: fibonnacci. This is the naive,
 exponential version of fibonacci: don't call it on a big value!
 
+Currently, only record bindings are recursive. To use a recursive function, one
+has to use a record.
+
 ## Run
 
 ```
diff --git a/examples/fibonacci/fibonacci.ncl b/examples/fibonacci/fibonacci.ncl
index 6cfc9c64..8c6644e2 100644
--- a/examples/fibonacci/fibonacci.ncl
+++ b/examples/fibonacci/fibonacci.ncl
@@ -1,11 +1,15 @@
+# Currently, only record bindings are recursive. To use a recursive function,
+# one has to use a record.
+
 # This is the naive, exponential version of fibonacci: don't call it on a big
 # value!
-let rec fibonacci = fun n =>
+let fibonacci = {
+ f = fun n =>
   if n == 0 then
     0
   else if n == 1 then
     1
   else
-    fibonacci (n - 1) + fibonacci (n - 2)
-in
+    f (n - 1) + f (n - 2)
+}.f in
 fibonacci 10
diff --git a/flake.lock b/flake.lock
index b420bda5..1a4f8f34 100644
--- a/flake.lock
+++ b/flake.lock
@@ -32,11 +32,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1650076401,
-        "narHash": "sha256-QGxadqKWICchuuLIF2QwmHPVaUk+qO33ml5p1wW4IyA=",
+        "lastModified": 1650701402,
+        "narHash": "sha256-XKfstdtqDg+O+gNBx1yGVKWIhLgfEDg/e2lvJSsp9vU=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "75ad56bdc927f3a9f9e05e3c3614c4c1fcd99fcb",
+        "rev": "bc41b01dd7a9fdffd32d9b03806798797532a5fe",
         "type": "github"
       },
       "original": {
@@ -87,11 +87,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1650076354,
-        "narHash": "sha256-HgHeh+VOuvSBSM7kAORcy4aMJ4LuOiWBegOGSIzi7nI=",
+        "lastModified": 1650681299,
+        "narHash": "sha256-JNvHHeeXDl3UnjWolMSbH2sWvhAYPfAutL815kZ6vFs=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "d154de7dae2da8b52084ddbfe95ce6e5b0ba0a37",
+        "rev": "d10f36b093459eb71ddcfedbab538c1ae3dfebb2",
         "type": "github"
       },
       "original": {
diff --git a/lsp/nls/src/linearization/mod.rs b/lsp/nls/src/linearization/mod.rs
index 3d73ce83..8a59c57c 100644
--- a/lsp/nls/src/linearization/mod.rs
+++ b/lsp/nls/src/linearization/mod.rs
@@ -161,11 +161,11 @@ impl Linearizer for AnalysisHost {
             Term::LetPattern(ident, destruct, ..) | Term::FunPattern(ident, destruct, _) => {
                 if let Some(ident) = ident {
                     let value_ptr = match term {
-                        Term::LetPattern(..) => {
+                        Term::LetPattern(_, _, _, _) => {
                             self.let_binding = Some(id);
                             ValueState::Unknown
                         }
-                        Term::FunPattern(..) => {
+                        Term::FunPattern(_, _, _) => {
                             // stub object
                             lin.push(LinearizationItem {
                                 id: id_gen.get_and_advance(),
@@ -218,13 +218,13 @@ impl Linearizer for AnalysisHost {
                     });
                 }
             }
-            Term::Let(ident, ..) | Term::Fun(ident, ..) => {
+            Term::Let(ident, _, _, _) | Term::Fun(ident, _) => {
                 let value_ptr = match term {
-                    Term::Let(..) => {
+                    Term::Let(_, _, _, _) => {
                         self.let_binding = Some(id);
                         ValueState::Unknown
                     }
-                    Term::Fun(..) => {
+                    Term::Fun(_, _) => {
                         // stub object
                         lin.push(LinearizationItem {
                             id: id_gen.get_and_advance(),
diff --git a/src/error.rs b/src/error.rs
index 642ec386..4d2265ee 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -306,9 +306,6 @@ pub enum ParseError {
         RawSpan, /* tail position */
         RawSpan, /* whole record position */
     ),
-    /// A recursive let pattern was encountered. They are not currently supported because we
-    /// decided it was too involved to implement them.
-    RecursiveLetPattern(RawSpan),
 }
 
 /// An error occurring during the resolution of an import.
@@ -465,9 +462,6 @@ impl ParseError {
                 InternalParseError::InvalidUniRecord(illegal_pos, tail_pos, pos) => {
                     ParseError::InvalidUniRecord(illegal_pos, tail_pos, pos)
                 }
-                InternalParseError::RecursiveLetPattern(pos) => {
-                    ParseError::RecursiveLetPattern(pos)
-                }
             },
         }
     }
@@ -1226,15 +1220,6 @@ impl ToDiagnostic<FileId> for ParseError {
                     String::from("Using a polymorphic tail in a record `{ ..; a}` requires the rest of the record to be only composed of type annotations, of the form `<field>: <type>`."),
                     String::from("Value assignements, such as `<field> = <expr>`, metadata, etc. are forbidden."),
                 ]),
-            ParseError::RecursiveLetPattern(span) => Diagnostic::error()
-                .with_message(format!("recursive destructuring is not supported"))
-                .with_labels(vec![
-                    primary(span),
-                ])
-                .with_notes(vec![
-                    String::from("A destructuring let-binding can't be recursive. Try removing the `rec` from `let rec`."),
-                    String::from("Note: you can reference other fields of a record recursively from within a field, so you might not need the recursive let."),
-                ]),
         };
 
         vec![diagnostic]
diff --git a/src/eval/mod.rs b/src/eval/mod.rs
index 3d0a9d6f..1a392861 100644
--- a/src/eval/mod.rs
+++ b/src/eval/mod.rs
@@ -95,8 +95,8 @@ use crate::{
     identifier::Ident,
     match_sharedterm, mk_app,
     term::{
-        make as mk_term, BinaryOp, BindingType, LetAttrs, MetaValue, RichTerm, SharedTerm,
-        StrChunk, Term, UnaryOp,
+        make as mk_term, BinaryOp, BindingType, MetaValue, RichTerm, SharedTerm, StrChunk, Term,
+        UnaryOp,
     },
 };
 
@@ -225,7 +225,7 @@ where
     use crate::transform::fresh_var;
 
     let var = fresh_var();
-    // Desugar to let x = term in %deep_seq% x x
+    // Desugar to let x = term in deepSeq x x
     let wrapper = mk_term::let_in(
         var.clone(),
         t0,
@@ -357,25 +357,19 @@ where
                     env,
                 }
             }
-            Term::Let(x, s, t, LetAttrs { binding_type, rec }) => {
+            Term::Let(x, s, t, btype) => {
                 let closure = Closure {
                     body: s.clone(),
                     env: env.clone(),
                 };
 
-                let mut thunk = match binding_type {
+                let thunk = match btype {
                     BindingType::Normal => Thunk::new(closure, IdentKind::Let),
                     BindingType::Revertible(deps) => {
                         Thunk::new_rev(closure, IdentKind::Let, deps.clone())
                     }
                 };
 
-                // Patch the environment with the (x <- closure) binding
-                if *rec {
-                    let thunk_ = thunk.clone();
-                    thunk.borrow_mut().env.insert(x.clone(), thunk_);
-                }
-
                 env.insert(x.clone(), thunk);
                 Closure {
                     body: t.clone(),
@@ -698,11 +692,11 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
             | v @ Term::Enum(_)
             | v @ Term::Import(_)
             | v @ Term::ResolvedImport(_) => RichTerm::new(v, pos),
-            Term::Let(id, t1, t2, attrs) => {
+            Term::Let(id, t1, t2, btype) => {
                 let t1 = subst_(t1, global_env, env, Cow::Borrowed(bound.as_ref()));
                 let t2 = subst_(t2, global_env, env, bound);
 
-                RichTerm::new(Term::Let(id, t1, t2, attrs), pos)
+                RichTerm::new(Term::Let(id, t1, t2, btype), pos)
             }
             p @ Term::LetPattern(..) => panic!("Pattern {:?} has not been transformed before evaluation", p),
             p @ Term::FunPattern(..) => panic!("Pattern {:?} has not been transformed before evaluation", p),
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 1ffefed3..8730a2df 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -166,9 +166,9 @@ UniTerm: UniTerm = {
     InfixExpr,
     AnnotatedInfixExpr,
     AsUniTerm<Forall>,
-    "let" <l: @L> <recursive:"rec"?> <r: @R> <pat:Pattern> <meta: Annot<FixedType>?>
+    "let" <pat:Pattern> <meta: Annot<FixedType>?>
         "=" <t1: Term>
-        "in" <t2: Term> =>? {
+        "in" <t2: Term> => {
         let t1 = if let Some(mut meta) = meta {
             let pos = t1.pos;
             meta.value = Some(t1);
@@ -178,7 +178,7 @@ UniTerm: UniTerm = {
             t1
         };
 
-        Ok(UniTerm::from(mk_let(recursive.is_some(), pat.0, pat.1, t1, t2, mk_span(src_id, l, r))?))
+        UniTerm::from(mk_term::let_pat(pat.0, pat.1, t1, t2))
     },
     <l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
         let pos = mk_pos(src_id, l, r);
@@ -781,7 +781,6 @@ extern {
         "forall" => Token::Normal(NormalToken::Forall),
         "in" => Token::Normal(NormalToken::In),
         "let" => Token::Normal(NormalToken::Let),
-	"rec" => Token::Normal(NormalToken::Rec),
         "switch" => Token::Normal(NormalToken::Switch),
 
         "null" => Token::Normal(NormalToken::Null),
diff --git a/src/parser/error.rs b/src/parser/error.rs
index ab79be26..a7cd46f4 100644
--- a/src/parser/error.rs
+++ b/src/parser/error.rs
@@ -33,7 +33,4 @@ pub enum ParseError {
         RawSpan, /* tail position */
         RawSpan, /* whole record position */
     ),
-    /// A recursive let pattern was encountered. They are not currently supported because we
-    /// decided it was too involved to implement them.
-    RecursiveLetPattern(RawSpan),
 }
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 54a9ef2d..704d6f29 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -68,8 +68,6 @@ pub enum NormalToken<'input> {
     In,
     #[token("let")]
     Let,
-    #[token("rec")]
-    Rec,
     #[token("switch")]
     Switch,
 
diff --git a/src/parser/utils.rs b/src/parser/utils.rs
index 3f172bd3..21d09f57 100644
--- a/src/parser/utils.rs
+++ b/src/parser/utils.rs
@@ -7,10 +7,7 @@ use std::rc::Rc;
 
 use codespan::FileId;
 
-use super::error::ParseError;
-
 use crate::{
-    destruct::Destruct,
     identifier::Ident,
     label::Label,
     mk_app, mk_fun,
@@ -317,41 +314,6 @@ pub fn mk_label(types: Types, src_id: FileId, l: usize, r: usize) -> Label {
     }
 }
 
-/// Generate a `Let` or a `LetPattern` (depending on `pat` being empty or not) from a the parsing
-/// of a let definition. This function fails if the definition has both a non-empty pattern and
-/// is recursive (`pat != Destruct::Empty && rec`), because recursive let-patterns are currently
-/// not supported.
-pub fn mk_let(
-    rec: bool,
-    id: Option<Ident>,
-    pat: Destruct,
-    t1: RichTerm,
-    t2: RichTerm,
-    span: RawSpan,
-) -> Result<RichTerm, ParseError> {
-    let result = match pat.into() {
-        d @ (Destruct::Record { .. } | Destruct::Array { .. }) => {
-            if rec {
-                return Err(ParseError::RecursiveLetPattern(span));
-            }
-            mk_term::let_pat(id, d, t1, t2)
-        }
-        Destruct::Empty => {
-            if let Some(id) = id {
-                if rec {
-                    mk_term::let_rec_in(id, t1, t2)
-                } else {
-                    mk_term::let_in(id, t1, t2)
-                }
-            } else {
-                panic!("unexpected let-binding without pattern or identifier")
-            }
-        }
-    };
-
-    Ok(result)
-}
-
 /// Determine the minimal level of indentation of a multi-line string.
 ///
 /// The result is determined by computing the minimum indentation level among all lines, where the
diff --git a/src/term.rs b/src/term.rs
index e3ff97f7..f683bd1d 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -69,7 +69,7 @@ pub enum Term {
 
     /// A let binding.
     #[serde(skip)]
-    Let(Ident, RichTerm, RichTerm, LetAttrs),
+    Let(Ident, RichTerm, RichTerm, BindingType),
     /// A destructuring let-binding.
     #[serde(skip)]
     LetPattern(Option<Ident>, Destruct, RichTerm, RichTerm),
@@ -185,15 +185,6 @@ pub struct RecordAttrs {
     pub open: bool,
 }
 
-/// The attributes of a let binding.
-#[derive(Debug, Default, Eq, PartialEq, Clone)]
-pub struct LetAttrs {
-    /// The type of a let binding. See the documentation of [`BindingType`].
-    pub binding_type: BindingType,
-    /// A recursive let binding adds its binding to the environment of the expression.
-    pub rec: bool,
-}
-
 impl RecordAttrs {
     pub fn merge(attrs1: RecordAttrs, attrs2: RecordAttrs) -> RecordAttrs {
         RecordAttrs {
@@ -1011,11 +1002,11 @@ impl RichTerm {
                     pos,
                 )
             },
-            Term::Let(id, t1, t2, attrs) => {
+            Term::Let(id, t1, t2, btype) => {
                 let t1 = t1.traverse(f, state, order)?;
                 let t2 = t2.traverse(f, state, order)?;
                 RichTerm::new(
-                    Term::Let(id, t1, t2, attrs),
+                    Term::Let(id, t1, t2, btype),
                     pos,
                 )
             },
@@ -1355,35 +1346,13 @@ pub mod make {
         Term::Var(v.into()).into()
     }
 
-    fn let_in_<I, T1, T2>(rec: bool, id: I, t1: T1, t2: T2) -> RichTerm
-    where
-        T1: Into<RichTerm>,
-        T2: Into<RichTerm>,
-        I: Into<Ident>,
-    {
-        let attrs = LetAttrs {
-            binding_type: BindingType::Normal,
-            rec,
-        };
-        Term::Let(id.into(), t1.into(), t2.into(), attrs).into()
-    }
-
     pub fn let_in<I, T1, T2>(id: I, t1: T1, t2: T2) -> RichTerm
     where
         T1: Into<RichTerm>,
         T2: Into<RichTerm>,
         I: Into<Ident>,
     {
-        let_in_(false, id, t1, t2)
-    }
-
-    pub fn let_rec_in<I, T1, T2>(id: I, t1: T1, t2: T2) -> RichTerm
-    where
-        T1: Into<RichTerm>,
-        T2: Into<RichTerm>,
-        I: Into<Ident>,
-    {
-        let_in_(true, id, t1, t2)
+        Term::Let(id.into(), t1.into(), t2.into(), BindingType::Normal).into()
     }
 
     pub fn let_pat<I, D, T1, T2>(id: Option<I>, pat: D, t1: T1, t2: T2) -> RichTerm
@@ -1393,7 +1362,18 @@ pub mod make {
         D: Into<Destruct>,
         I: Into<Ident>,
     {
-        Term::LetPattern(id.map(|i| i.into()), pat.into(), t1.into(), t2.into()).into()
+        match pat.into() {
+            d @ (Destruct::Record { .. } | Destruct::Array { .. }) => {
+                Term::LetPattern(id.map(|i| i.into()), d, t1.into(), t2.into()).into()
+            }
+            Destruct::Empty => {
+                if let Some(id) = id {
+                    let_in(id, t1, t2)
+                } else {
+                    Term::Null.into()
+                }
+            }
+        }
     }
 
     #[cfg(test)]
diff --git a/src/transform/desugar_destructuring.rs b/src/transform/desugar_destructuring.rs
index 4b767f4e..fef3b6bf 100644
--- a/src/transform/desugar_destructuring.rs
+++ b/src/transform/desugar_destructuring.rs
@@ -34,7 +34,9 @@ use crate::destruct::{Destruct, Match};
 use crate::identifier::Ident;
 use crate::match_sharedterm;
 use crate::term::make::{op1, op2};
-use crate::term::{BinaryOp::DynRemove, MetaValue, RichTerm, Term, UnaryOp::StaticAccess};
+use crate::term::{
+    BinaryOp::DynRemove, BindingType, MetaValue, RichTerm, Term, UnaryOp::StaticAccess,
+};
 
 /// Entry point of the patterns desugaring.
 /// It desugar a `RichTerm` if possible (the term is a let pattern or a function with patterns in
@@ -115,7 +117,7 @@ pub fn desugar(rt: RichTerm) -> RichTerm {
                         x.clone(),
                         t_,
                         destruct_term(x.clone(), &pat, bind_open_field(x, &pat, body)),
-                        Default::default(),
+                        BindingType::Normal,
                     ),
                     pos,
                 )
@@ -159,7 +161,7 @@ fn bind_open_field(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
             }
         }),
         body,
-        Default::default(),
+        BindingType::Normal,
     )
     .into()
 }
@@ -175,7 +177,7 @@ fn destruct_term(x: Ident, pat: &Destruct, body: RichTerm) -> RichTerm {
                     id.clone(),
                     op1(StaticAccess(id.clone()), Term::Var(x.clone())),
                     t,
-                    Default::default(),
+                    BindingType::Normal,
                 ),
                 pos,
             ),
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index 22248f3c..afc5972d 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -53,15 +53,10 @@ fn collect_free_vars(rt: &mut RichTerm, free_vars: &mut HashSet<Ident>) {
 
             free_vars.extend(fresh);
         }
-        Term::Let(id, t1, t2, attrs) => {
+        Term::Let(id, t1, t2, _) => {
             let mut fresh = HashSet::new();
 
-            if attrs.rec {
-                collect_free_vars(t1, &mut fresh);
-            } else {
-                collect_free_vars(t1, free_vars);
-            }
-
+            collect_free_vars(t1, free_vars);
             collect_free_vars(t2, &mut fresh);
             fresh.remove(id);
 
diff --git a/src/transform/share_normal_form.rs b/src/transform/share_normal_form.rs
index dbb3d710..c1876872 100644
--- a/src/transform/share_normal_form.rs
+++ b/src/transform/share_normal_form.rs
@@ -32,7 +32,7 @@ use crate::{
     identifier::Ident,
     match_sharedterm,
     position::TermPos,
-    term::{BindingType, LetAttrs, RichTerm, Term},
+    term::{BindingType, RichTerm, Term},
 };
 
 use std::{collections::HashSet, rc::Rc};
@@ -165,11 +165,7 @@ pub fn transform_one(rt: RichTerm) -> RichTerm {
                     meta.value
                         .replace(RichTerm::new(Term::Var(fresh_var.clone()), t.pos));
                     let inner = RichTerm::new(Term::MetaValue(meta), pos);
-                    let attrs = LetAttrs {
-                        binding_type: BindingType::Normal,
-                        rec : false,
-                    };
-                    RichTerm::new(Term::Let(fresh_var, t, inner, attrs), pos)
+                    RichTerm::new(Term::Let(fresh_var, t, inner, BindingType::Normal), pos)
             }
         } else rt
     }
@@ -207,19 +203,6 @@ fn with_bindings(
 ) -> RichTerm {
     bindings.into_iter().fold(
         RichTerm::new(body, pos.into_inherited()),
-        |acc, (id, t, binding_type)| {
-            RichTerm::new(
-                Term::Let(
-                    id,
-                    t,
-                    acc,
-                    LetAttrs {
-                        binding_type,
-                        rec: false,
-                    },
-                ),
-                pos,
-            )
-        },
+        |acc, (id, t, btype)| RichTerm::new(Term::Let(id, t, acc, btype), pos),
     )
 }
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index cf260635..5ad80466 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -391,12 +391,8 @@ fn type_check_<L: Linearizer>(
             unify(state, strict, ty, mk_typewrapper::dynamic())
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
-        Term::Let(x, re, rt, attrs) => {
+        Term::Let(x, re, rt, _) => {
             let ty_let = binding_type(re.as_ref(), &envs, state.table, strict, state.resolver);
-            if attrs.rec {
-                envs.insert(x.clone(), ty_let.clone());
-            }
-
             linearizer.retype_ident(lin, x, ty_let.clone());
             type_check_(
                 state,
@@ -408,9 +404,8 @@ fn type_check_<L: Linearizer>(
                 ty_let.clone(),
             )?;
 
-            if !attrs.rec {
-                envs.insert(x.clone(), ty_let);
-            }
+            // TODO move this up once lets are rec
+            envs.insert(x.clone(), ty_let);
             type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
         Term::LetPattern(x, pat, re, rt) => {


Test patch:
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 39d97a5f..a435eb19 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -127,7 +127,7 @@ fn records_contracts_poly() {
                 (forall b. {a: Num, b: Num ; b} -> { a: Num ; b})
                 -> {a: Num ; a}
                 -> { ; a}
-            = fun f r => %record_remove% \"b\" (%record_remove% \"a\" (f r)) in
+            = fun f rec => %record_remove% \"b\" (%record_remove% \"a\" (f rec)) in
         f (fun x => x) {a = 1, b = true, c = 3}"
     );
 }
diff --git a/tests/free_vars.rs b/tests/free_vars.rs
index 30662520..a8d61069 100644
--- a/tests/free_vars.rs
+++ b/tests/free_vars.rs
@@ -163,19 +163,3 @@ fn nested_records() {
         HashMap::from([("a", vec!["c"]), ("b", vec!["a", "c"]), ("c", vec!["b"]),])
     ));
 }
-
-#[test]
-fn recursive_let() {
-    assert!(check_stat_vars(
-        "{
-          a = let rec b = b + a + h in b,
-          b = let rec a = a + b in f (a + 1) z,
-          c = let rec foo = b in let rec bar = c in if a.r then [b] else {foo = c}
-        }",
-        HashMap::from([
-            ("a", vec!["a"]),
-            ("b", vec!["b"]),
-            ("c", vec!["a", "b", "c"])
-        ])
-    ));
-}
diff --git a/tests/pass.rs b/tests/pass.rs
index 91b51ec9..a2b15a97 100644
--- a/tests/pass.rs
+++ b/tests/pass.rs
@@ -117,8 +117,3 @@ fn importing() {
 fn overriding() {
     check_file("overriding.ncl");
 }
-
-#[test]
-fn recursive_let() {
-    check_file("recursive_let.ncl");
-}
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 2cbab5c7..a4599653 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -81,7 +81,7 @@ let Assert = fun l x => x || %blame% l in
     (remove (extend {}) == {} | Assert) &&
     (extend (remove {foo = 2}) == {foo =1} | Assert) &&
     (let f | forall a b. {f: a -> a, arg: a ; b} -> a =
-        fun r => r.f (r.arg) in
+        fun rec => rec.f (rec.arg) in
       f { f = fun x => x ++ " suffix", arg = "foo" }
       == "foo suffix"
       | Assert)
diff --git a/tests/pass/recursive_let.ncl b/tests/pass/recursive_let.ncl
deleted file mode 100644
index 1cb46f4e..00000000
--- a/tests/pass/recursive_let.ncl
+++ /dev/null
@@ -1,7 +0,0 @@
-let Assert = fun l x => x || %blame% l in
-
-[
-  let rec f = fun n => if n == 0 then n else f (n - 1) in f 10 == 0,
-  let rec fib = fun n => if n == 0 || n == 1 then 1 else fib (n - 1) + fib (n - 2) in fib 5 == 8,
-]
-|> array.foldl (fun x y => (x | Assert) && y) true
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 9ffe18a8..12b8aa0d 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -74,15 +74,6 @@ let typecheck = [
     fun x => switch {`blo => `bla, `ble => `bli, _ => `bla} x in
     f `bli,
 
-  # recursive let bindings
-  let rec f : forall a. a -> Num -> a = fun x n =>
-    if n == 0 then x else if f "0" n == "1" then f x (n - 1) else f x (f 1 n) in
-    (f "0" 2 : Str),
-  let rec f : Num -> Num = fun x => if x == 0 then x else f (x - 1) in
-    (f 10 : Num),
-  let rec repeat : forall a. Num -> a -> Array a = fun n x =>
-    if n <= 0 then [] else repeat (n - 1) x @ [x] in (repeat 3 "foo" : Array Str),
-
   # static records
   ({bla = 1} : {bla : Num}),
   ({blo = true, bla = 1} : {bla : Num, blo : Bool}),
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 08c62f34..165e633f 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -230,10 +230,3 @@ fn piecewise_signature() {
         Err(TypecheckError::TypeMismatch(..))
     );
 }
-#[test]
-fn recursive_let() {
-    assert_matches!(
-        type_check_expr("let rec f : Num -> Num = fun x => f \"hoi\" in null"),
-        Err(TypecheckError::TypeMismatch(..))
-    );
-}