From 887d1c70038257876280d1053b5eec74f201bf82 Mon Sep 17 00:00:00 2001
From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com>
Date: Mon, 27 Sep 2021 12:49:03 -0500
Subject: [PATCH] RFC: Recursive type restriction (#68)

Co-authored-by: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com>
Co-authored-by: vegorov-rbx <75688451+vegorov-rbx@users.noreply.github.com>
---
 docs/recursive-type-restriction.md | 59 ++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)
 create mode 100644 docs/recursive-type-restriction.md

diff --git a/docs/recursive-type-restriction.md b/docs/recursive-type-restriction.md
new file mode 100644
index 0000000..eb9b212
--- /dev/null
+++ b/docs/recursive-type-restriction.md
@@ -0,0 +1,59 @@
+# Recursive type restriction
+
+## Motivation
+
+Luau supports recursive type aliases, but with an important restriction:
+users can declare functions of recursive types, such as:
+```lua
+  type Tree<a> = { data: a, children: {Tree<a>} }
+```
+but *not* recursive type functions, such as:
+```lua
+  type Weird<a> = { data: a, children: Weird<{a}> }
+```
+If types such as `Weird` were allowed, they would have infinite unfoldings for example:
+```lua
+  Weird<number> = { data: number, children: Weird<{number}> }`
+  Weird<{number}> = { data: {number}, children: Weird<{{number}}> }
+  Weird<{{number}}> = { data: {{number}}, children: Weird<{{{number}}}> }
+  ...
+```
+
+Currently Luau has this restriction, but does not enforce it, and instead
+produces unexpected types, which can result in free types leaking into
+the module exports.
+
+## Design
+
+To enforce the restriction that recursive types aliases produce functions of
+recursive types, we require that in any recursive type alias defining `T<gs>`,
+in any recursive use of `T<Us>`, we have that `gs` and `Us` are equal.
+
+This allows types such as:
+```lua
+  type Tree<a> = { data: a, children: {Tree<a>} }
+```
+but *not*:
+```lua
+  type Weird<a> = { data: a, children: Weird<{a}> }
+```
+since in the recursive use `a` is not equal to `{a}`.
+
+This restriction applies to mutually recursive types too.
+
+## Drawbacks
+
+This restriction bans some type declarations which do not produce infinite unfoldings,
+such as:
+```lua
+  type WeirdButFinite<a> = { data: a, children: WeirdButFinite<number> }
+```
+This restriction is stricter than TypeScript, which allows programs such as:
+```typescript
+interface Foo<a> { x: Foo<a[]>[]; y: a; }
+let x: Foo<number> = { x: [], y: 37 }
+```
+
+## Alternatives
+
+We could adopt a solution more like TypeScript's, which is to lazily rather than eagerly instantiate types.