From 32591847c49160d8c1e0b1e008a8e5f2545b37e5 Mon Sep 17 00:00:00 2001
From: "ajeffrey@roblox.com" <ajeffrey@roblox.com>
Date: Mon, 13 Sep 2021 17:30:45 -0500
Subject: [PATCH] Add first draft of rfcs/recusive-tpe-restriction.md

---
 rfcs/recursive-type-restriction.md | 59 ++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)
 create mode 100644 rfcs/recursive-type-restriction.md

diff --git a/rfcs/recursive-type-restriction.md b/rfcs/recursive-type-restriction.md
new file mode 100644
index 00000000..fb4ae17b
--- /dev/null
+++ b/rfcs/recursive-type-restriction.md
@@ -0,0 +1,59 @@
+# Recursive type restriction
+
+## Motivation
+
+Luau supports reclusive 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.