Merge branch 'prototyping-type-normalizaton' into prototyping-function-overload-resolution

Analysis/include/Luau/Clone.h

@@ -18,7 +18,7 @@ struct CloneState
     SeenTypePacks seenTypePacks;
 
     int recursionCount = 0;
-    bool encounteredFreeType = false;
+    bool encounteredFreeType = false; // TODO: Remove with LuauLosslessClone.
 };
 
 TypePackId clone(TypePackId tp, TypeArena& dest, CloneState& cloneState);

Analysis/include/Luau/Frontend.h

@@ -13,6 +13,7 @@
 #include <optional>
 
 LUAU_FASTFLAG(LuauSeparateTypechecks)
+LUAU_FASTFLAG(LuauDirtySourceModule)
 
 namespace Luau
 {
@@ -57,19 +58,27 @@ std::optional<ModuleName> pathExprToModuleName(const ModuleName& currentModuleNa
 
 struct SourceNode
 {
-    bool isDirty(bool forAutocomplete) const
+    bool hasDirtySourceModule() const
+    {
+        LUAU_ASSERT(FFlag::LuauDirtySourceModule);
+
+        return dirtySourceModule;
+    }
+
+    bool hasDirtyModule(bool forAutocomplete) const
     {
         if (FFlag::LuauSeparateTypechecks)
-            return forAutocomplete ? dirtyAutocomplete : dirty;
+            return forAutocomplete ? dirtyModuleForAutocomplete : dirtyModule;
         else
-            return dirty;
+            return dirtyModule;
     }
 
     ModuleName name;
     std::unordered_set<ModuleName> requires;
     std::vector<std::pair<ModuleName, Location>> requireLocations;
-    bool dirty = true;
-    bool dirtyAutocomplete = true;
+    bool dirtySourceModule = true;
+    bool dirtyModule = true;
+    bool dirtyModuleForAutocomplete = true;
     double autocompleteLimitsMult = 1.0;
 };
 
@@ -163,7 +172,7 @@ struct Frontend
     void applyBuiltinDefinitionToEnvironment(const std::string& environmentName, const std::string& definitionName);
 
 private:
-    std::pair<SourceNode*, SourceModule*> getSourceNode(CheckResult& checkResult, const ModuleName& name, bool forAutocomplete);
+    std::pair<SourceNode*, SourceModule*> getSourceNode(CheckResult& checkResult, const ModuleName& name, bool forAutocomplete_DEPRECATED);
     SourceModule parse(const ModuleName& name, std::string_view src, const ParseOptions& parseOptions);
 
     bool parseGraph(std::vector<ModuleName>& buildQueue, CheckResult& checkResult, const ModuleName& root, bool forAutocomplete);

Analysis/include/Luau/TypeVar.h

@@ -373,15 +373,17 @@ struct ClassTypeVar
     std::optional<TypeId> metatable; // metaclass?
     Tags tags;
     std::shared_ptr<ClassUserData> userData;
+    ModuleName definitionModuleName;
 
-    ClassTypeVar(
-        Name name, Props props, std::optional<TypeId> parent, std::optional<TypeId> metatable, Tags tags, std::shared_ptr<ClassUserData> userData)
+    ClassTypeVar(Name name, Props props, std::optional<TypeId> parent, std::optional<TypeId> metatable, Tags tags,
+        std::shared_ptr<ClassUserData> userData, ModuleName definitionModuleName)
         : name(name)
         , props(props)
         , parent(parent)
         , metatable(metatable)
         , tags(tags)
         , userData(userData)
+        , definitionModuleName(definitionModuleName)
     {
     }
 };

Analysis/include/Luau/Unifier.h

@@ -92,7 +92,6 @@ private:
 
     bool canCacheResult(TypeId subTy, TypeId superTy);
     void cacheResult(TypeId subTy, TypeId superTy, size_t prevErrorCount);
-    void cacheResult_DEPRECATED(TypeId subTy, TypeId superTy);
 
 public:
     void tryUnify(TypePackId subTy, TypePackId superTy, bool isFunctionCall = false);

Analysis/include/Luau/VisitTypeVar.h

@@ -52,7 +52,7 @@ inline void unsee(std::unordered_set<void*>& seen, const void* tv)
 
 inline void unsee(DenseHashSet<void*>& seen, const void* tv)
 {
-    // When DenseHashSet is used for 'visitOnce', where don't forget visited elements
+    // When DenseHashSet is used for 'visitTypeVarOnce', where don't forget visited elements
 }
 
 template<typename F, typename Set>

Analysis/src/Autocomplete.cpp

@@ -15,6 +15,7 @@
 
 LUAU_FASTFLAGVARIABLE(LuauIfElseExprFixCompletionIssue, false);
 LUAU_FASTFLAGVARIABLE(LuauAutocompleteSingletonTypes, false);
+LUAU_FASTFLAGVARIABLE(LuauFixAutocompleteClassSecurityLevel, false);
 LUAU_FASTFLAG(LuauSelfCallAutocompleteFix)
 
 static const std::unordered_set<std::string> kStatementStartingKeywords = {
@@ -462,7 +463,8 @@ static void autocompleteProps(const Module& module, TypeArena* typeArena, TypeId
         containingClass = containingClass.value_or(cls);
         fillProps(cls->props);
         if (cls->parent)
-            autocompleteProps(module, typeArena, rootTy, *cls->parent, indexType, nodes, result, seen, cls);
+            autocompleteProps(module, typeArena, rootTy, *cls->parent, indexType, nodes, result, seen,
+                FFlag::LuauFixAutocompleteClassSecurityLevel ? containingClass : cls);
     }
     else if (auto tbl = get<TableTypeVar>(ty))
         fillProps(tbl->props);

Analysis/src/Clone.cpp

@@ -10,6 +10,7 @@ LUAU_FASTFLAG(DebugLuauCopyBeforeNormalizing)
 
 LUAU_FASTINTVARIABLE(LuauTypeCloneRecursionLimit, 300)
 LUAU_FASTFLAG(LuauTypecheckOptPass)
+LUAU_FASTFLAGVARIABLE(LuauLosslessClone, false)
 
 namespace Luau
 {
@@ -87,11 +88,18 @@ struct TypePackCloner
 
     void operator()(const Unifiable::Free& t)
     {
-        cloneState.encounteredFreeType = true;
+        if (FFlag::LuauLosslessClone)
+        {
+            defaultClone(t);
+        }
+        else
+        {
+            cloneState.encounteredFreeType = true;
 
-        TypePackId err = getSingletonTypes().errorRecoveryTypePack(getSingletonTypes().anyTypePack);
-        TypePackId cloned = dest.addTypePack(*err);
-        seenTypePacks[typePackId] = cloned;
+            TypePackId err = getSingletonTypes().errorRecoveryTypePack(getSingletonTypes().anyTypePack);
+            TypePackId cloned = dest.addTypePack(*err);
+            seenTypePacks[typePackId] = cloned;
+        }
     }
 
     void operator()(const Unifiable::Generic& t)
@@ -143,10 +151,18 @@ void TypeCloner::defaultClone(const T& t)
 
 void TypeCloner::operator()(const Unifiable::Free& t)
 {
-    cloneState.encounteredFreeType = true;
-    TypeId err = getSingletonTypes().errorRecoveryType(getSingletonTypes().anyType);
-    TypeId cloned = dest.addType(*err);
-    seenTypes[typeId] = cloned;
+    if (FFlag::LuauLosslessClone)
+    {
+        defaultClone(t);
+    }
+    else
+    {
+        cloneState.encounteredFreeType = true;
+
+        TypeId err = getSingletonTypes().errorRecoveryType(getSingletonTypes().anyType);
+        TypeId cloned = dest.addType(*err);
+        seenTypes[typeId] = cloned;
+    }
 }
 
 void TypeCloner::operator()(const Unifiable::Generic& t)
@@ -174,7 +190,8 @@ void TypeCloner::operator()(const PrimitiveTypeVar& t)
 
 void TypeCloner::operator()(const ConstrainedTypeVar& t)
 {
-    cloneState.encounteredFreeType = true;
+    if (!FFlag::LuauLosslessClone)
+        cloneState.encounteredFreeType = true;
 
     TypeId res = dest.addType(ConstrainedTypeVar{t.level});
     ConstrainedTypeVar* ctv = getMutable<ConstrainedTypeVar>(res);
@@ -252,7 +269,7 @@ void TypeCloner::operator()(const TableTypeVar& t)
     for (TypePackId& arg : ttv->instantiatedTypePackParams)
         arg = clone(arg, dest, cloneState);
 
-    if (ttv->state == TableState::Free)
+    if (!FFlag::LuauLosslessClone && ttv->state == TableState::Free)
     {
         cloneState.encounteredFreeType = true;
 
@@ -276,7 +293,7 @@ void TypeCloner::operator()(const MetatableTypeVar& t)
 
 void TypeCloner::operator()(const ClassTypeVar& t)
 {
-    TypeId result = dest.addType(ClassTypeVar{t.name, {}, std::nullopt, std::nullopt, t.tags, t.userData});
+    TypeId result = dest.addType(ClassTypeVar{t.name, {}, std::nullopt, std::nullopt, t.tags, t.userData, t.definitionModuleName});
     ClassTypeVar* ctv = getMutable<ClassTypeVar>(result);
 
     seenTypes[typeId] = result;
@@ -361,7 +378,10 @@ TypeId clone(TypeId typeId, TypeArena& dest, CloneState& cloneState)
 
         // Persistent types are not being cloned and we get the original type back which might be read-only
         if (!res->persistent)
+        {
             asMutable(res)->documentationSymbol = typeId->documentationSymbol;
+            asMutable(res)->normal = typeId->normal;
+        }
     }
 
     return res;

Analysis/src/Error.cpp

@@ -8,8 +8,6 @@
 
 #include <stdexcept>
 
-LUAU_FASTFLAGVARIABLE(LuauTypeMismatchModuleName, false);
-
 static std::string wrongNumberOfArgsString(size_t expectedCount, size_t actualCount, const char* argPrefix = nullptr, bool isVariadic = false)
 {
     std::string s = "expects ";
@@ -59,27 +57,20 @@ struct ErrorConverter
 
         std::string result;
 
-        if (FFlag::LuauTypeMismatchModuleName)
+        if (givenTypeName == wantedTypeName)
         {
-            if (givenTypeName == wantedTypeName)
+            if (auto givenDefinitionModule = getDefinitionModuleName(tm.givenType))
             {
-                if (auto givenDefinitionModule = getDefinitionModuleName(tm.givenType))
+                if (auto wantedDefinitionModule = getDefinitionModuleName(tm.wantedType))
                 {
-                    if (auto wantedDefinitionModule = getDefinitionModuleName(tm.wantedType))
-                    {
-                        result = "Type '" + givenTypeName + "' from '" + *givenDefinitionModule + "' could not be converted into '" + wantedTypeName +
-                                 "' from '" + *wantedDefinitionModule + "'";
-                    }
+                    result = "Type '" + givenTypeName + "' from '" + *givenDefinitionModule + "' could not be converted into '" + wantedTypeName +
+                             "' from '" + *wantedDefinitionModule + "'";
                 }
             }
+        }
 
-            if (result.empty())
-                result = "Type '" + givenTypeName + "' could not be converted into '" + wantedTypeName + "'";
-        }
-        else
-        {
+        if (result.empty())
             result = "Type '" + givenTypeName + "' could not be converted into '" + wantedTypeName + "'";
-        }
 
         if (tm.error)
         {

Analysis/src/Frontend.cpp

@@ -23,6 +23,7 @@ LUAU_FASTFLAG(LuauInferInNoCheckMode)
 LUAU_FASTFLAGVARIABLE(LuauKnowsTheDataModel3, false)
 LUAU_FASTFLAGVARIABLE(LuauSeparateTypechecks, false)
 LUAU_FASTFLAGVARIABLE(LuauAutocompleteDynamicLimits, false)
+LUAU_FASTFLAGVARIABLE(LuauDirtySourceModule, false)
 LUAU_FASTINTVARIABLE(LuauAutocompleteCheckTimeoutMs, 0)
 
 namespace Luau
@@ -358,7 +359,7 @@ CheckResult Frontend::check(const ModuleName& name, std::optional<FrontendOption
     CheckResult checkResult;
 
     auto it = sourceNodes.find(name);
-    if (it != sourceNodes.end() && !it->second.isDirty(frontendOptions.forAutocomplete))
+    if (it != sourceNodes.end() && !it->second.hasDirtyModule(frontendOptions.forAutocomplete))
     {
         // No recheck required.
         if (FFlag::LuauSeparateTypechecks)
@@ -402,7 +403,7 @@ CheckResult Frontend::check(const ModuleName& name, std::optional<FrontendOption
         LUAU_ASSERT(sourceNodes.count(moduleName));
         SourceNode& sourceNode = sourceNodes[moduleName];
 
-        if (!sourceNode.isDirty(frontendOptions.forAutocomplete))
+        if (!sourceNode.hasDirtyModule(frontendOptions.forAutocomplete))
             continue;
 
         LUAU_ASSERT(sourceModules.count(moduleName));
@@ -478,7 +479,7 @@ CheckResult Frontend::check(const ModuleName& name, std::optional<FrontendOption
             stats.timeCheck += duration;
             stats.filesStrict += 1;
 
-            sourceNode.dirtyAutocomplete = false;
+            sourceNode.dirtyModuleForAutocomplete = false;
             continue;
         }
 
@@ -541,7 +542,7 @@ CheckResult Frontend::check(const ModuleName& name, std::optional<FrontendOption
         checkResult.errors.insert(checkResult.errors.end(), module->errors.begin(), module->errors.end());
 
         moduleResolver.modules[moduleName] = std::move(module);
-        sourceNode.dirty = false;
+        sourceNode.dirtyModule = false;
     }
 
     return checkResult;
@@ -618,7 +619,7 @@ bool Frontend::parseGraph(std::vector<ModuleName>& buildQueue, CheckResult& chec
                     // this relies on the fact that markDirty marks reverse-dependencies dirty as well
                     // thus if a node is not dirty, all its transitive deps aren't dirty, which means that they won't ever need
                     // to be built, *and* can't form a cycle with any nodes we did process.
-                    if (!it->second.isDirty(forAutocomplete))
+                    if (!it->second.hasDirtyModule(forAutocomplete))
                         continue;
 
                     // note: this check is technically redundant *except* that getSourceNode has somewhat broken memoization
@@ -768,7 +769,7 @@ LintResult Frontend::lint(const SourceModule& module, std::optional<Luau::LintOp
 bool Frontend::isDirty(const ModuleName& name, bool forAutocomplete) const
 {
     auto it = sourceNodes.find(name);
-    return it == sourceNodes.end() || it->second.isDirty(forAutocomplete);
+    return it == sourceNodes.end() || it->second.hasDirtyModule(forAutocomplete);
 }
 
 /*
@@ -810,20 +811,31 @@ void Frontend::markDirty(const ModuleName& name, std::vector<ModuleName>* marked
         if (markedDirty)
             markedDirty->push_back(next);
 
-        if (FFlag::LuauSeparateTypechecks)
+        if (FFlag::LuauDirtySourceModule)
         {
-            if (sourceNode.dirty && sourceNode.dirtyAutocomplete)
+            LUAU_ASSERT(FFlag::LuauSeparateTypechecks);
+
+            if (sourceNode.dirtySourceModule && sourceNode.dirtyModule && sourceNode.dirtyModuleForAutocomplete)
                 continue;
 
-            sourceNode.dirty = true;
-            sourceNode.dirtyAutocomplete = true;
+            sourceNode.dirtySourceModule = true;
+            sourceNode.dirtyModule = true;
+            sourceNode.dirtyModuleForAutocomplete = true;
+        }
+        else if (FFlag::LuauSeparateTypechecks)
+        {
+            if (sourceNode.dirtyModule && sourceNode.dirtyModuleForAutocomplete)
+                continue;
+
+            sourceNode.dirtyModule = true;
+            sourceNode.dirtyModuleForAutocomplete = true;
         }
         else
         {
-            if (sourceNode.dirty)
+            if (sourceNode.dirtyModule)
                 continue;
 
-            sourceNode.dirty = true;
+            sourceNode.dirtyModule = true;
         }
 
         if (0 == reverseDeps.count(name))
@@ -851,13 +863,14 @@ const SourceModule* Frontend::getSourceModule(const ModuleName& moduleName) cons
 }
 
 // Read AST into sourceModules if necessary.  Trace require()s.  Report parse errors.
-std::pair<SourceNode*, SourceModule*> Frontend::getSourceNode(CheckResult& checkResult, const ModuleName& name, bool forAutocomplete)
+std::pair<SourceNode*, SourceModule*> Frontend::getSourceNode(CheckResult& checkResult, const ModuleName& name, bool forAutocomplete_DEPRECATED)
 {
     LUAU_TIMETRACE_SCOPE("Frontend::getSourceNode", "Frontend");
     LUAU_TIMETRACE_ARGUMENT("name", name.c_str());
 
     auto it = sourceNodes.find(name);
-    if (it != sourceNodes.end() && !it->second.isDirty(forAutocomplete))
+    if (it != sourceNodes.end() &&
+        (FFlag::LuauDirtySourceModule ? !it->second.hasDirtySourceModule() : !it->second.hasDirtyModule(forAutocomplete_DEPRECATED)))
     {
         auto moduleIt = sourceModules.find(name);
         if (moduleIt != sourceModules.end())
@@ -901,17 +914,20 @@ std::pair<SourceNode*, SourceModule*> Frontend::getSourceNode(CheckResult& check
     sourceNode.requires.clear();
     sourceNode.requireLocations.clear();
 
+    if (FFlag::LuauDirtySourceModule)
+        sourceNode.dirtySourceModule = false;
+
     if (FFlag::LuauSeparateTypechecks)
     {
         if (it == sourceNodes.end())
         {
-            sourceNode.dirty = true;
-            sourceNode.dirtyAutocomplete = true;
+            sourceNode.dirtyModule = true;
+            sourceNode.dirtyModuleForAutocomplete = true;
         }
     }
     else
     {
-        sourceNode.dirty = true;
+        sourceNode.dirtyModule = true;
     }
 
     for (const auto& [moduleName, location] : requireTrace.requires)

Analysis/src/Module.cpp

@@ -14,8 +14,8 @@
 #include <algorithm>
 
 LUAU_FASTFLAGVARIABLE(DebugLuauFreezeArena, false)
-LUAU_FASTFLAGVARIABLE(LuauCloneDeclaredGlobals, false)
 LUAU_FASTFLAG(LuauLowerBoundsCalculation)
+LUAU_FASTFLAG(LuauLosslessClone)
 
 namespace Luau
 {
@@ -182,20 +182,20 @@ bool Module::clonePublicInterface(InternalErrorReporter& ice)
         }
     }
 
-    if (FFlag::LuauCloneDeclaredGlobals)
+    for (auto& [name, ty] : declaredGlobals)
     {
-        for (auto& [name, ty] : declaredGlobals)
-        {
-            ty = clone(ty, interfaceTypes, cloneState);
-            if (FFlag::LuauLowerBoundsCalculation)
-                normalize(ty, interfaceTypes, ice);
-        }
+        ty = clone(ty, interfaceTypes, cloneState);
+        if (FFlag::LuauLowerBoundsCalculation)
+            normalize(ty, interfaceTypes, ice);
     }
 
     freeze(internalTypes);
     freeze(interfaceTypes);
 
-    return cloneState.encounteredFreeType;
+    if (FFlag::LuauLosslessClone)
+        return false; // TODO: make function return void.
+    else
+        return cloneState.encounteredFreeType;
 }
 
 } // namespace Luau

Analysis/src/Normalize.cpp

@@ -5,7 +5,6 @@
 #include <algorithm>
 
 #include "Luau/Clone.h"
-#include "Luau/DenseHash.h"
 #include "Luau/Substitution.h"
 #include "Luau/Unifier.h"
 #include "Luau/VisitTypeVar.h"
@@ -254,7 +253,7 @@ bool isSubtype(TypeId subTy, TypeId superTy, InternalErrorReporter& ice)
 }
 
 template<typename T>
-static bool areNormal_(const T& t, const DenseHashSet<void*>& seen, InternalErrorReporter& ice)
+static bool areNormal_(const T& t, const std::unordered_set<void*>& seen, InternalErrorReporter& ice)
 {
     int count = 0;
     auto isNormal = [&](TypeId ty) {
@@ -262,18 +261,19 @@ static bool areNormal_(const T& t, const DenseHashSet<void*>& seen, InternalErro
         if (count >= FInt::LuauNormalizeIterationLimit)
             ice.ice("Luau::areNormal hit iteration limit");
 
-        return ty->normal || seen.find(asMutable(ty));
+        // The follow is here because a bound type may not be normal, but the bound type is normal.
+        return ty->normal || follow(ty)->normal || seen.find(asMutable(ty)) != seen.end();
     };
 
     return std::all_of(begin(t), end(t), isNormal);
 }
 
-static bool areNormal(const std::vector<TypeId>& types, const DenseHashSet<void*>& seen, InternalErrorReporter& ice)
+static bool areNormal(const std::vector<TypeId>& types, const std::unordered_set<void*>& seen, InternalErrorReporter& ice)
 {
     return areNormal_(types, seen, ice);
 }
 
-static bool areNormal(TypePackId tp, const DenseHashSet<void*>& seen, InternalErrorReporter& ice)
+static bool areNormal(TypePackId tp, const std::unordered_set<void*>& seen, InternalErrorReporter& ice)
 {
     tp = follow(tp);
     if (get<FreeTypePack>(tp))
@@ -288,7 +288,7 @@ static bool areNormal(TypePackId tp, const DenseHashSet<void*>& seen, InternalEr
         return true;
 
     if (auto vtp = get<VariadicTypePack>(*tail))
-        return vtp->ty->normal || seen.find(asMutable(vtp->ty));
+        return vtp->ty->normal || follow(vtp->ty)->normal || seen.find(asMutable(vtp->ty)) != seen.end();
 
     return true;
 }
@@ -335,9 +335,14 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const BoundTypeVar& btv)
+    bool operator()(TypeId ty, const BoundTypeVar& btv, std::unordered_set<void*>& seen)
     {
-        // It should never be the case that this TypeVar is normal, but is bound to a non-normal type.
+        // A type could be considered normal when it is in the stack, but we will eventually find out it is not normal as normalization progresses.
+        // So we need to avoid eagerly saying that this bound type is normal if the thing it is bound to is in the stack.
+        if (seen.find(asMutable(btv.boundTo)) != seen.end())
+            return false;
+
+        // It should never be the case that this TypeVar is normal, but is bound to a non-normal type, except in nontrivial cases.
         LUAU_ASSERT(!ty->normal || ty->normal == btv.boundTo->normal);
 
         asMutable(ty)->normal = btv.boundTo->normal;
@@ -365,7 +370,7 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const ConstrainedTypeVar& ctvRef, DenseHashSet<void*>& seen)
+    bool operator()(TypeId ty, const ConstrainedTypeVar& ctvRef, std::unordered_set<void*>& seen)
     {
         CHECK_ITERATION_LIMIT(false);
 
@@ -391,8 +396,7 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const FunctionTypeVar& ftv) = delete;
-    bool operator()(TypeId ty, const FunctionTypeVar& ftv, DenseHashSet<void*>& seen)
+    bool operator()(TypeId ty, const FunctionTypeVar& ftv, std::unordered_set<void*>& seen)
     {
         CHECK_ITERATION_LIMIT(false);
 
@@ -407,7 +411,7 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const TableTypeVar& ttv, DenseHashSet<void*>& seen)
+    bool operator()(TypeId ty, const TableTypeVar& ttv, std::unordered_set<void*>& seen)
     {
         CHECK_ITERATION_LIMIT(false);
 
@@ -419,7 +423,7 @@ struct Normalize
         auto checkNormal = [&](TypeId t) {
             // if t is on the stack, it is possible that this type is normal.
             // If t is not normal and it is not on the stack, this type is definitely not normal.
-            if (!t->normal && !seen.find(asMutable(t)))
+            if (!t->normal && seen.find(asMutable(t)) == seen.end())
                 normal = false;
         };
 
@@ -449,7 +453,7 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const MetatableTypeVar& mtv, DenseHashSet<void*>& seen)
+    bool operator()(TypeId ty, const MetatableTypeVar& mtv, std::unordered_set<void*>& seen)
     {
         CHECK_ITERATION_LIMIT(false);
 
@@ -477,7 +481,7 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const UnionTypeVar& utvRef, DenseHashSet<void*>& seen)
+    bool operator()(TypeId ty, const UnionTypeVar& utvRef, std::unordered_set<void*>& seen)
     {
         CHECK_ITERATION_LIMIT(false);
 
@@ -507,7 +511,7 @@ struct Normalize
         return false;
     }
 
-    bool operator()(TypeId ty, const IntersectionTypeVar& itvRef, DenseHashSet<void*>& seen)
+    bool operator()(TypeId ty, const IntersectionTypeVar& itvRef, std::unordered_set<void*>& seen)
     {
         CHECK_ITERATION_LIMIT(false);
 
@@ -775,8 +779,8 @@ std::pair<TypeId, bool> normalize(TypeId ty, TypeArena& arena, InternalErrorRepo
         (void)clone(ty, arena, state);
 
     Normalize n{arena, ice, std::move(state.seenTypes), std::move(state.seenTypePacks)};
-    DenseHashSet<void*> seen{nullptr};
-    visitTypeVarOnce(ty, n, seen);
+    std::unordered_set<void*> seen;
+    visitTypeVar(ty, n, seen);
 
     return {ty, !n.limitExceeded};
 }
@@ -800,8 +804,8 @@ std::pair<TypePackId, bool> normalize(TypePackId tp, TypeArena& arena, InternalE
         (void)clone(tp, arena, state);
 
     Normalize n{arena, ice, std::move(state.seenTypes), std::move(state.seenTypePacks)};
-    DenseHashSet<void*> seen{nullptr};
-    visitTypeVarOnce(tp, n, seen);
+    std::unordered_set<void*> seen;
+    visitTypeVar(tp, n, seen);
 
     return {tp, !n.limitExceeded};
 }

Analysis/src/Substitution.cpp

@@ -11,6 +11,7 @@ LUAU_FASTFLAG(LuauLowerBoundsCalculation)
 LUAU_FASTINTVARIABLE(LuauTarjanChildLimit, 1000)
 LUAU_FASTFLAG(LuauTypecheckOptPass)
 LUAU_FASTFLAGVARIABLE(LuauSubstituteFollowNewTypes, false)
+LUAU_FASTFLAGVARIABLE(LuauSubstituteFollowPossibleMutations, false)
 
 namespace Luau
 {
@@ -106,7 +107,7 @@ void Tarjan::visitChildren(TypePackId tp, int index)
 
 std::pair<int, bool> Tarjan::indexify(TypeId ty)
 {
-    if (FFlag::LuauTypecheckOptPass)
+    if (FFlag::LuauTypecheckOptPass && !FFlag::LuauSubstituteFollowPossibleMutations)
         LUAU_ASSERT(ty == log->follow(ty));
     else
         ty = log->follow(ty);
@@ -127,7 +128,7 @@ std::pair<int, bool> Tarjan::indexify(TypeId ty)
 
 std::pair<int, bool> Tarjan::indexify(TypePackId tp)
 {
-    if (FFlag::LuauTypecheckOptPass)
+    if (FFlag::LuauTypecheckOptPass && !FFlag::LuauSubstituteFollowPossibleMutations)
         LUAU_ASSERT(tp == log->follow(tp));
     else
         tp = log->follow(tp);
@@ -148,7 +149,8 @@ std::pair<int, bool> Tarjan::indexify(TypePackId tp)
 
 void Tarjan::visitChild(TypeId ty)
 {
-    ty = log->follow(ty);
+    if (!FFlag::LuauSubstituteFollowPossibleMutations)
+        ty = log->follow(ty);
 
     edgesTy.push_back(ty);
     edgesTp.push_back(nullptr);
@@ -156,7 +158,8 @@ void Tarjan::visitChild(TypeId ty)
 
 void Tarjan::visitChild(TypePackId tp)
 {
-    tp = log->follow(tp);
+    if (!FFlag::LuauSubstituteFollowPossibleMutations)
+        tp = log->follow(tp);
 
     edgesTy.push_back(nullptr);
     edgesTp.push_back(tp);
@@ -471,7 +474,7 @@ TypePackId Substitution::clone(TypePackId tp)
 
 void Substitution::foundDirty(TypeId ty)
 {
-    if (FFlag::LuauTypecheckOptPass)
+    if (FFlag::LuauTypecheckOptPass && !FFlag::LuauSubstituteFollowPossibleMutations)
         LUAU_ASSERT(ty == log->follow(ty));
     else
         ty = log->follow(ty);
@@ -484,7 +487,7 @@ void Substitution::foundDirty(TypeId ty)
 
 void Substitution::foundDirty(TypePackId tp)
 {
-    if (FFlag::LuauTypecheckOptPass)
+    if (FFlag::LuauTypecheckOptPass && !FFlag::LuauSubstituteFollowPossibleMutations)
         LUAU_ASSERT(tp == log->follow(tp));
     else
         tp = log->follow(tp);

Analysis/src/ToDot.cpp

@@ -327,7 +327,7 @@ void StateDot::visitChildren(TypePackId tp, int index)
     }
     else if (const VariadicTypePack* vtp = get<VariadicTypePack>(tp))
     {
-        formatAppend(result, "VariadicTypePack %d", index);
+        formatAppend(result, "VariadicTypePack %s%d", vtp->hidden ? "hidden " : "", index);
         finishNodeLabel(tp);
         finishNode();
 

Analysis/src/Transpiler.cpp

@@ -1025,31 +1025,42 @@ struct Printer
         }
         else if (const auto& a = typeAnnotation.as<AstTypeTable>())
         {
-            CommaSeparatorInserter comma(writer);
+            AstTypeReference* indexType = a->indexer ? a->indexer->indexType->as<AstTypeReference>() : nullptr;
 
-            writer.symbol("{");
-
-            for (std::size_t i = 0; i < a->props.size; ++i)
+            if (a->props.size == 0 && indexType && indexType->name == "number")
             {
-                comma();
-                advance(a->props.data[i].location.begin);
-                writer.identifier(a->props.data[i].name.value);
-                if (a->props.data[i].type)
-                {
-                    writer.symbol(":");
-                    visualizeTypeAnnotation(*a->props.data[i].type);
-                }
-            }
-            if (a->indexer)
-            {
-                comma();
-                writer.symbol("[");
-                visualizeTypeAnnotation(*a->indexer->indexType);
-                writer.symbol("]");
-                writer.symbol(":");
+                writer.symbol("{");
                 visualizeTypeAnnotation(*a->indexer->resultType);
+                writer.symbol("}");
+            }
+            else
+            {
+                CommaSeparatorInserter comma(writer);
+
+                writer.symbol("{");
+
+                for (std::size_t i = 0; i < a->props.size; ++i)
+                {
+                    comma();
+                    advance(a->props.data[i].location.begin);
+                    writer.identifier(a->props.data[i].name.value);
+                    if (a->props.data[i].type)
+                    {
+                        writer.symbol(":");
+                        visualizeTypeAnnotation(*a->props.data[i].type);
+                    }
+                }
+                if (a->indexer)
+                {
+                    comma();
+                    writer.symbol("[");
+                    visualizeTypeAnnotation(*a->indexer->indexType);
+                    writer.symbol("]");
+                    writer.symbol(":");
+                    visualizeTypeAnnotation(*a->indexer->resultType);
+                }
+                writer.symbol("}");
             }
-            writer.symbol("}");
         }
         else if (auto a = typeAnnotation.as<AstTypeTypeof>())
         {

Analysis/src/TypeAttach.cpp

@@ -479,6 +479,20 @@ public:
     {
         return visitLocal(al->local);
     }
+
+    virtual bool visit(AstStatFor* stat) override
+    {
+        visitLocal(stat->var);
+        return true;
+    }
+
+    virtual bool visit(AstStatForIn* stat) override
+    {
+        for (size_t i = 0; i < stat->vars.size; ++i)
+            visitLocal(stat->vars.data[i]);
+        return true;
+    }
+
     virtual bool visit(AstExprFunction* fn) override
     {
         // TODO: add generics if the inferred type of the function is generic CLI-39908

Analysis/src/TypeInfer.cpp

@@ -1,6 +1,7 @@
 // This file is part of the Luau programming language and is licensed under MIT License; see LICENSE.txt for details
 #include "Luau/TypeInfer.h"
 
+#include "Luau/Clone.h"
 #include "Luau/Common.h"
 #include "Luau/ModuleResolver.h"
 #include "Luau/Normalize.h"
@@ -47,7 +48,6 @@ LUAU_FASTFLAGVARIABLE(LuauPropertiesGetExpectedType, false)
 LUAU_FASTFLAGVARIABLE(LuauStatFunctionSimplify4, false)
 LUAU_FASTFLAGVARIABLE(LuauTypecheckOptPass, false)
 LUAU_FASTFLAGVARIABLE(LuauUnsealedTableLiteral, false)
-LUAU_FASTFLAG(LuauTypeMismatchModuleName)
 LUAU_FASTFLAGVARIABLE(LuauTwoPassAliasDefinitionFix, false)
 LUAU_FASTFLAGVARIABLE(LuauAssertStripsFalsyTypes, false)
 LUAU_FASTFLAGVARIABLE(LuauReturnAnyInsteadOfICE, false) // Eventually removed as false.
@@ -61,7 +61,9 @@ LUAU_FASTFLAG(LuauAnyInIsOptionalIsOptional)
 LUAU_FASTFLAGVARIABLE(LuauDecoupleOperatorInferenceFromUnifiedTypeInference, false)
 LUAU_FASTFLAGVARIABLE(LuauArgCountMismatchSaysAtLeastWhenVariadic, false)
 LUAU_FASTFLAGVARIABLE(LuauTableUseCounterInstead, false)
+LUAU_FASTFLAGVARIABLE(LuauReturnTypeInferenceInNonstrict, false)
 LUAU_FASTFLAGVARIABLE(LuauRecursionLimitException, false);
+LUAU_FASTFLAG(LuauLosslessClone)
 
 namespace Luau
 {
@@ -376,7 +378,7 @@ ModulePtr TypeChecker::checkWithoutRecursionCheck(const SourceModule& module, Mo
     prepareErrorsForDisplay(currentModule->errors);
 
     bool encounteredFreeType = currentModule->clonePublicInterface(*iceHandler);
-    if (encounteredFreeType)
+    if (!FFlag::LuauLosslessClone && encounteredFreeType)
     {
         reportError(TypeError{module.root->location,
             GenericError{"Free types leaked into this module's public interface. This is an internal Luau error; please report it."}});
@@ -785,7 +787,7 @@ void TypeChecker::check(const ScopePtr& scope, const AstStatReturn& return_)
 
     TypePackId retPack = checkExprList(scope, return_.location, return_.list, false, {}, expectedTypes).type;
 
-    if (useConstrainedIntersections())
+    if (FFlag::LuauReturnTypeInferenceInNonstrict ? FFlag::LuauLowerBoundsCalculation : useConstrainedIntersections())
     {
         unifyLowerBound(retPack, scope->returnType, return_.location);
         return;
@@ -1241,7 +1243,12 @@ void TypeChecker::check(const ScopePtr& scope, TypeId ty, const ScopePtr& funSco
         // If in nonstrict mode and allowing redefinition of global function, restore the previous definition type
         // in case this function has a differing signature. The signature discrepancy will be caught in checkBlock.
         if (previouslyDefined)
+        {
+            if (FFlag::LuauReturnTypeInferenceInNonstrict && FFlag::LuauLowerBoundsCalculation)
+                quantify(funScope, ty, exprName->location);
+
             globalBindings[name] = oldBinding;
+        }
         else
             globalBindings[name] = {quantify(funScope, ty, exprName->location), exprName->location};
 
@@ -1555,7 +1562,7 @@ void TypeChecker::check(const ScopePtr& scope, const AstStatDeclareClass& declar
 
     Name className(declaredClass.name.value);
 
-    TypeId classTy = addType(ClassTypeVar(className, {}, superTy, std::nullopt, {}, {}));
+    TypeId classTy = addType(ClassTypeVar(className, {}, superTy, std::nullopt, {}, {}, currentModuleName));
     ClassTypeVar* ctv = getMutable<ClassTypeVar>(classTy);
 
     TypeId metaTy = addType(TableTypeVar{TableState::Sealed, scope->level});
@@ -3284,7 +3291,7 @@ std::pair<TypeId, ScopePtr> TypeChecker::checkFunctionSignature(
     TypePackId retPack;
     if (expr.returnAnnotation)
         retPack = resolveTypePack(funScope, *expr.returnAnnotation);
-    else if (isNonstrictMode())
+    else if (FFlag::LuauReturnTypeInferenceInNonstrict ? (!FFlag::LuauLowerBoundsCalculation && isNonstrictMode()) : isNonstrictMode())
         retPack = anyTypePack;
     else if (expectedFunctionType)
     {
@@ -5328,19 +5335,9 @@ TypeId TypeChecker::resolveType(const ScopePtr& scope, const AstType& annotation
         if (const auto& indexer = table->indexer)
             tableIndexer = TableIndexer(resolveType(scope, *indexer->indexType), resolveType(scope, *indexer->resultType));
 
-        if (FFlag::LuauTypeMismatchModuleName)
-        {
-            TableTypeVar ttv{props, tableIndexer, scope->level, TableState::Sealed};
-            ttv.definitionModuleName = currentModuleName;
-            return addType(std::move(ttv));
-        }
-        else
-        {
-            return addType(TableTypeVar{
-                props, tableIndexer, scope->level,
-                TableState::Sealed // FIXME: probably want a way to annotate other kinds of tables maybe
-            });
-        }
+        TableTypeVar ttv{props, tableIndexer, scope->level, TableState::Sealed};
+        ttv.definitionModuleName = currentModuleName;
+        return addType(std::move(ttv));
     }
     else if (const auto& func = annotation.as<AstTypeFunction>())
     {
@@ -5602,9 +5599,7 @@ TypeId TypeChecker::instantiateTypeFun(const ScopePtr& scope, const TypeFun& tf,
     {
         ttv->instantiatedTypeParams = typeParams;
         ttv->instantiatedTypePackParams = typePackParams;
-
-        if (FFlag::LuauTypeMismatchModuleName)
-            ttv->definitionModuleName = currentModuleName;
+        ttv->definitionModuleName = currentModuleName;
     }
 
     return instantiated;

Analysis/src/TypeVar.cpp

@@ -27,6 +27,7 @@ LUAU_FASTFLAG(LuauErrorRecoveryType)
 LUAU_FASTFLAG(LuauSubtypingAddOptPropsToUnsealedTables)
 LUAU_FASTFLAG(LuauDiscriminableUnions2)
 LUAU_FASTFLAGVARIABLE(LuauAnyInIsOptionalIsOptional, false)
+LUAU_FASTFLAGVARIABLE(LuauClassDefinitionModuleInError, false)
 
 namespace Luau
 {
@@ -304,6 +305,11 @@ std::optional<ModuleName> getDefinitionModuleName(TypeId type)
         if (ftv->definition)
             return ftv->definition->definitionModuleName;
     }
+    else if (auto ctv = get<ClassTypeVar>(type); ctv && FFlag::LuauClassDefinitionModuleInError)
+    {
+        if (!ctv->definitionModuleName.empty())
+            return ctv->definitionModuleName;
+    }
 
     return std::nullopt;
 }

Analysis/src/Unifier.cpp

@@ -17,7 +17,6 @@ LUAU_FASTINT(LuauTypeInferTypePackLoopLimit);
 LUAU_FASTINT(LuauTypeInferIterationLimit);
 LUAU_FASTFLAG(LuauAutocompleteDynamicLimits)
 LUAU_FASTINTVARIABLE(LuauTypeInferLowerBoundsIterationLimit, 2000);
-LUAU_FASTFLAGVARIABLE(LuauExtendedIndexerError, false);
 LUAU_FASTFLAGVARIABLE(LuauTableSubtypingVariance2, false);
 LUAU_FASTFLAG(LuauLowerBoundsCalculation);
 LUAU_FASTFLAG(LuauErrorRecoveryType);
@@ -28,7 +27,6 @@ LUAU_FASTFLAGVARIABLE(LuauTxnLogSeesTypePacks2, false)
 LUAU_FASTFLAGVARIABLE(LuauTxnLogCheckForInvalidation, false)
 LUAU_FASTFLAGVARIABLE(LuauTxnLogRefreshFunctionPointers, false)
 LUAU_FASTFLAGVARIABLE(LuauTxnLogDontRetryForIndexers, false)
-LUAU_FASTFLAGVARIABLE(LuauUnifierCacheErrors, false)
 LUAU_FASTFLAG(LuauAnyInIsOptionalIsOptional)
 LUAU_FASTFLAG(LuauTypecheckOptPass)
 
@@ -474,32 +472,21 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
     if (get<ErrorTypeVar>(subTy))
         return tryUnifyWithAny(superTy, subTy);
 
-    bool cacheEnabled;
     auto& cache = sharedState.cachedUnify;
 
     // What if the types are immutable and we proved their relation before
-    if (FFlag::LuauUnifierCacheErrors)
+    bool cacheEnabled = !isFunctionCall && !isIntersection && variance == Invariant;
+
+    if (cacheEnabled)
     {
-        cacheEnabled = !isFunctionCall && !isIntersection && variance == Invariant;
-
-        if (cacheEnabled)
-        {
-            if (cache.contains({subTy, superTy}))
-                return;
-
-            if (auto error = sharedState.cachedUnifyError.find({subTy, superTy}))
-            {
-                reportError(TypeError{location, *error});
-                return;
-            }
-        }
-    }
-    else
-    {
-        cacheEnabled = !isFunctionCall && !isIntersection;
-
-        if (cacheEnabled && cache.contains({superTy, subTy}) && (variance == Covariant || cache.contains({subTy, superTy})))
+        if (cache.contains({subTy, superTy}))
             return;
+
+        if (auto error = sharedState.cachedUnifyError.find({subTy, superTy}))
+        {
+            reportError(TypeError{location, *error});
+            return;
+        }
     }
 
     // If we have seen this pair of types before, we are currently recursing into cyclic types.
@@ -543,12 +530,6 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
     else if (log.getMutable<TableTypeVar>(superTy) && log.getMutable<TableTypeVar>(subTy))
     {
         tryUnifyTables(subTy, superTy, isIntersection);
-
-        if (!FFlag::LuauUnifierCacheErrors)
-        {
-            if (cacheEnabled && errors.empty())
-                cacheResult_DEPRECATED(subTy, superTy);
-        }
     }
 
     // tryUnifyWithMetatable assumes its first argument is a MetatableTypeVar. The check is otherwise symmetrical.
@@ -568,7 +549,7 @@ void Unifier::tryUnify_(TypeId subTy, TypeId superTy, bool isFunctionCall, bool
     else
         reportError(TypeError{location, TypeMismatch{superTy, subTy}});
 
-    if (FFlag::LuauUnifierCacheErrors && cacheEnabled)
+    if (cacheEnabled)
         cacheResult(subTy, superTy, errorCount);
 
     log.popSeen(superTy, subTy);
@@ -705,21 +686,10 @@ void Unifier::tryUnifyTypeWithUnion(TypeId subTy, TypeId superTy, const UnionTyp
         {
             TypeId type = uv->options[i];
 
-            if (FFlag::LuauUnifierCacheErrors)
+            if (cache.contains({subTy, type}))
             {
-                if (cache.contains({subTy, type}))
-                {
-                    startIndex = i;
-                    break;
-                }
-            }
-            else
-            {
-                if (cache.contains({type, subTy}) && (variance == Covariant || cache.contains({subTy, type})))
-                {
-                    startIndex = i;
-                    break;
-                }
+                startIndex = i;
+                break;
             }
         }
     }
@@ -807,21 +777,10 @@ void Unifier::tryUnifyIntersectionWithType(TypeId subTy, const IntersectionTypeV
         {
             TypeId type = uv->parts[i];
 
-            if (FFlag::LuauUnifierCacheErrors)
+            if (cache.contains({type, superTy}))
             {
-                if (cache.contains({type, superTy}))
-                {
-                    startIndex = i;
-                    break;
-                }
-            }
-            else
-            {
-                if (cache.contains({superTy, type}) && (variance == Covariant || cache.contains({type, superTy})))
-                {
-                    startIndex = i;
-                    break;
-                }
+                startIndex = i;
+                break;
             }
         }
     }
@@ -896,19 +855,6 @@ void Unifier::cacheResult(TypeId subTy, TypeId superTy, size_t prevErrorCount)
     }
 }
 
-void Unifier::cacheResult_DEPRECATED(TypeId subTy, TypeId superTy)
-{
-    LUAU_ASSERT(!FFlag::LuauUnifierCacheErrors);
-
-    if (!canCacheResult(subTy, superTy))
-        return;
-
-    sharedState.cachedUnify.insert({superTy, subTy});
-
-    if (variance == Invariant)
-        sharedState.cachedUnify.insert({subTy, superTy});
-}
-
 struct WeirdIter
 {
     TypePackId packId;
@@ -1650,24 +1596,16 @@ void Unifier::tryUnifyTables(TypeId subTy, TypeId superTy, bool isIntersection)
 
         Unifier innerState = makeChildUnifier();
 
-        if (FFlag::LuauExtendedIndexerError)
-        {
-            innerState.tryUnify_(subTable->indexer->indexType, superTable->indexer->indexType);
+        innerState.tryUnify_(subTable->indexer->indexType, superTable->indexer->indexType);
 
-            bool reported = !innerState.errors.empty();
+        bool reported = !innerState.errors.empty();
 
-            checkChildUnifierTypeMismatch(innerState.errors, "[indexer key]", superTy, subTy);
+        checkChildUnifierTypeMismatch(innerState.errors, "[indexer key]", superTy, subTy);
 
-            innerState.tryUnify_(subTable->indexer->indexResultType, superTable->indexer->indexResultType);
+        innerState.tryUnify_(subTable->indexer->indexResultType, superTable->indexer->indexResultType);
 
-            if (!reported)
-                checkChildUnifierTypeMismatch(innerState.errors, "[indexer value]", superTy, subTy);
-        }
-        else
-        {
-            innerState.tryUnifyIndexer(*subTable->indexer, *superTable->indexer);
-            checkChildUnifierTypeMismatch(innerState.errors, superTy, subTy);
-        }
+        if (!reported)
+            checkChildUnifierTypeMismatch(innerState.errors, "[indexer value]", superTy, subTy);
 
         if (innerState.errors.empty())
             log.concat(std::move(innerState.log));
@@ -2225,7 +2163,7 @@ void Unifier::tryUnifyWithClass(TypeId subTy, TypeId superTy, bool reversed)
 
 void Unifier::tryUnifyIndexer(const TableIndexer& subIndexer, const TableIndexer& superIndexer)
 {
-    LUAU_ASSERT(!FFlag::LuauTableSubtypingVariance2 || !FFlag::LuauExtendedIndexerError);
+    LUAU_ASSERT(!FFlag::LuauTableSubtypingVariance2);
 
     tryUnify_(subIndexer.indexType, superIndexer.indexType);
     tryUnify_(subIndexer.indexResultType, superIndexer.indexResultType);

Ast/include/Luau/StringUtils.h

@@ -19,6 +19,7 @@ std::string format(const char* fmt, ...) LUAU_PRINTF_ATTR(1, 2);
 std::string vformat(const char* fmt, va_list args);
 
 void formatAppend(std::string& str, const char* fmt, ...) LUAU_PRINTF_ATTR(2, 3);
+void vformatAppend(std::string& ret, const char* fmt, va_list args);
 
 std::string join(const std::vector<std::string_view>& segments, std::string_view delimiter);
 std::string join(const std::vector<std::string>& segments, std::string_view delimiter);

Ast/src/Parser.cpp

@@ -167,6 +167,7 @@ Parser::Parser(const char* buffer, size_t bufferSize, AstNameTable& names, Alloc
     Function top;
     top.vararg = true;
 
+    functionStack.reserve(8);
     functionStack.push_back(top);
 
     nameSelf = names.addStatic("self");
@@ -186,6 +187,13 @@ Parser::Parser(const char* buffer, size_t bufferSize, AstNameTable& names, Alloc
 
     // all hot comments parsed after the first non-comment lexeme are special in that they don't affect type checking / linting mode
     hotcommentHeader = false;
+
+    // preallocate some buffers that are very likely to grow anyway; this works around std::vector's inefficient growth policy for small arrays
+    localStack.reserve(16);
+    scratchStat.reserve(16);
+    scratchExpr.reserve(16);
+    scratchLocal.reserve(16);
+    scratchBinding.reserve(16);
 }
 
 bool Parser::blockFollow(const Lexeme& l)

Ast/src/StringUtils.cpp

@@ -11,7 +11,7 @@
 namespace Luau
 {
 
-static void vformatAppend(std::string& ret, const char* fmt, va_list args)
+void vformatAppend(std::string& ret, const char* fmt, va_list args)
 {
     va_list argscopy;
     va_copy(argscopy, args);

CLI/Repl.cpp

@@ -579,7 +579,8 @@ static bool compileFile(const char* name, CompileFormat format)
 
         if (format == CompileFormat::Text)
         {
-            bcb.setDumpFlags(Luau::BytecodeBuilder::Dump_Code | Luau::BytecodeBuilder::Dump_Source | Luau::BytecodeBuilder::Dump_Locals);
+            bcb.setDumpFlags(Luau::BytecodeBuilder::Dump_Code | Luau::BytecodeBuilder::Dump_Source | Luau::BytecodeBuilder::Dump_Locals |
+                             Luau::BytecodeBuilder::Dump_Remarks);
             bcb.setDumpSource(*source);
         }
 
@@ -636,13 +637,60 @@ static int assertionHandler(const char* expr, const char* file, int line, const
     return 1;
 }
 
+static void setLuauFlags(bool state)
+{
+    for (Luau::FValue<bool>* flag = Luau::FValue<bool>::list; flag; flag = flag->next)
+    {
+        if (strncmp(flag->name, "Luau", 4) == 0)
+            flag->value = state;
+    }
+}
+
+static void setFlag(std::string_view name, bool state)
+{
+    for (Luau::FValue<bool>* flag = Luau::FValue<bool>::list; flag; flag = flag->next)
+    {
+        if (name == flag->name)
+        {
+            flag->value = state;
+            return;
+        }
+    }
+
+    fprintf(stderr, "Warning: --fflag unrecognized flag '%.*s'.\n\n", int(name.length()), name.data());
+}
+
+static void applyFlagKeyValue(std::string_view element)
+{
+    if (size_t separator = element.find('='); separator != std::string_view::npos)
+    {
+        std::string_view key = element.substr(0, separator);
+        std::string_view value = element.substr(separator + 1);
+
+        if (value == "true")
+            setFlag(key, true);
+        else if (value == "false")
+            setFlag(key, false);
+        else
+            fprintf(stderr, "Warning: --fflag unrecognized value '%.*s' for flag '%.*s'.\n\n", int(value.length()), value.data(), int(key.length()),
+                key.data());
+    }
+    else
+    {
+        if (element == "true")
+            setLuauFlags(true);
+        else if (element == "false")
+            setLuauFlags(false);
+        else
+            setFlag(element, true);
+    }
+}
+
 int replMain(int argc, char** argv)
 {
     Luau::assertHandler() = assertionHandler;
 
-    for (Luau::FValue<bool>* flag = Luau::FValue<bool>::list; flag; flag = flag->next)
-        if (strncmp(flag->name, "Luau", 4) == 0)
-            flag->value = true;
+    setLuauFlags(true);
 
     CliMode mode = CliMode::Unknown;
     CompileFormat compileFormat{};
@@ -727,6 +775,22 @@ int replMain(int argc, char** argv)
             return 1;
 #endif
         }
+        else if (strncmp(argv[i], "--fflags=", 9) == 0)
+        {
+            std::string_view list = argv[i] + 9;
+
+            while (!list.empty())
+            {
+                size_t ending = list.find(",");
+
+                applyFlagKeyValue(list.substr(0, ending));
+
+                if (ending != std::string_view::npos)
+                    list.remove_prefix(ending + 1);
+                else
+                    break;
+            }
+        }
         else if (argv[i][0] == '-')
         {
             fprintf(stderr, "Error: Unrecognized option '%s'.\n\n", argv[i]);

CMakeLists.txt

@@ -73,6 +73,12 @@ else()
     list(APPEND LUAU_OPTIONS -Wall) # All warnings
 endif()
 
+if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+    # Some gcc versions treat var in `if (type var = val)` as unused
+    # Some gcc versions treat variables used in constexpr if blocks as unused
+    list(APPEND LUAU_OPTIONS -Wno-unused)
+endif()
+
 # Enabled in CI; we should be warning free on our main compiler versions but don't guarantee being warning free everywhere
 if(LUAU_WERROR)
     if(MSVC)

Compiler/include/Luau/BytecodeBuilder.h

@@ -3,6 +3,7 @@
 
 #include "Luau/Bytecode.h"
 #include "Luau/DenseHash.h"
+#include "Luau/StringUtils.h"
 
 #include <string>
 
@@ -80,6 +81,8 @@ public:
     void pushDebugUpval(StringRef name);
     uint32_t getDebugPC() const;
 
+    void addDebugRemark(const char* format, ...) LUAU_PRINTF_ATTR(2, 3);
+
     void finalize();
 
     enum DumpFlags
@@ -88,6 +91,7 @@ public:
         Dump_Lines = 1 << 1,
         Dump_Source = 1 << 2,
         Dump_Locals = 1 << 3,
+        Dump_Remarks = 1 << 4,
     };
 
     void setDumpFlags(uint32_t flags)
@@ -228,6 +232,9 @@ private:
 
     DenseHashMap<StringRef, unsigned int, StringRefHash> stringTable;
 
+    DenseHashMap<uint32_t, uint32_t> debugRemarks;
+    std::string debugRemarkBuffer;
+
     BytecodeEncoder* encoder = nullptr;
     std::string bytecode;
 

Compiler/src/BytecodeBuilder.cpp

@@ -181,9 +181,17 @@ BytecodeBuilder::BytecodeBuilder(BytecodeEncoder* encoder)
     : constantMap({Constant::Type_Nil, ~0ull})
     , tableShapeMap(TableShape())
     , stringTable({nullptr, 0})
+    , debugRemarks(~0u)
     , encoder(encoder)
 {
     LUAU_ASSERT(stringTable.find(StringRef{"", 0}) == nullptr);
+
+    // preallocate some buffers that are very likely to grow anyway; this works around std::vector's inefficient growth policy for small arrays
+    insns.reserve(32);
+    lines.reserve(32);
+    constants.reserve(16);
+    protos.reserve(16);
+    functions.reserve(8);
 }
 
 uint32_t BytecodeBuilder::beginFunction(uint8_t numparams, bool isvararg)
@@ -219,8 +227,8 @@ void BytecodeBuilder::endFunction(uint8_t maxstacksize, uint8_t numupvalues)
     validate();
 #endif
 
-    // very approximate: 4 bytes per instruction for code, 1 byte for debug line, and 1-2 bytes for aux data like constants
-    func.data.reserve(insns.size() * 7);
+    // very approximate: 4 bytes per instruction for code, 1 byte for debug line, and 1-2 bytes for aux data like constants plus overhead
+    func.data.reserve(32 + insns.size() * 7);
 
     writeFunction(func.data, currentFunction);
 
@@ -242,6 +250,9 @@ void BytecodeBuilder::endFunction(uint8_t maxstacksize, uint8_t numupvalues)
 
     constantMap.clear();
     tableShapeMap.clear();
+
+    debugRemarks.clear();
+    debugRemarkBuffer.clear();
 }
 
 void BytecodeBuilder::setMainFunction(uint32_t fid)
@@ -505,9 +516,40 @@ uint32_t BytecodeBuilder::getDebugPC() const
     return uint32_t(insns.size());
 }
 
+void BytecodeBuilder::addDebugRemark(const char* format, ...)
+{
+    if ((dumpFlags & Dump_Remarks) == 0)
+        return;
+
+    size_t offset = debugRemarkBuffer.size();
+
+    va_list args;
+    va_start(args, format);
+    vformatAppend(debugRemarkBuffer, format, args);
+    va_end(args);
+
+    // we null-terminate all remarks to avoid storing remark length
+    debugRemarkBuffer += '\0';
+
+    debugRemarks[uint32_t(insns.size())] = uint32_t(offset);
+}
+
 void BytecodeBuilder::finalize()
 {
     LUAU_ASSERT(bytecode.empty());
+
+    // preallocate space for bytecode blob
+    size_t capacity = 16;
+
+    for (auto& p : stringTable)
+        capacity += p.first.length + 2;
+
+    for (const Function& func : functions)
+        capacity += func.data.size();
+
+    bytecode.reserve(capacity);
+
+    // assemble final bytecode blob
     bytecode = char(LBC_VERSION);
 
     writeStringTable(bytecode);
@@ -663,6 +705,8 @@ void BytecodeBuilder::writeFunction(std::string& ss, uint32_t id) const
 
 void BytecodeBuilder::writeLineInfo(std::string& ss) const
 {
+    LUAU_ASSERT(!lines.empty());
+
     // this function encodes lines inside each span as a 8-bit delta to span baseline
     // span is always a power of two; depending on the line info input, it may need to be as low as 1
     int span = 1 << 24;
@@ -693,7 +737,17 @@ void BytecodeBuilder::writeLineInfo(std::string& ss) const
     }
 
     // second pass: compute span base
-    std::vector<int> baseline((lines.size() - 1) / span + 1);
+    int baselineOne = 0;
+    std::vector<int> baselineScratch;
+    int* baseline = &baselineOne;
+    size_t baselineSize = (lines.size() - 1) / span + 1;
+
+    if (baselineSize > 1)
+    {
+        // avoid heap allocation for single-element baseline which is most functions (<256 lines)
+        baselineScratch.resize(baselineSize);
+        baseline = baselineScratch.data();
+    }
 
     for (size_t offset = 0; offset < lines.size(); offset += span)
     {
@@ -725,7 +779,7 @@ void BytecodeBuilder::writeLineInfo(std::string& ss) const
 
     int lastLine = 0;
 
-    for (size_t i = 0; i < baseline.size(); ++i)
+    for (size_t i = 0; i < baselineSize; ++i)
     {
         writeInt(ss, baseline[i] - lastLine);
         lastLine = baseline[i];
@@ -1695,6 +1749,14 @@ std::string BytecodeBuilder::dumpCurrentFunction() const
             continue;
         }
 
+        if (dumpFlags & Dump_Remarks)
+        {
+            const uint32_t* remark = debugRemarks.find(uint32_t(code - insns.data()));
+
+            if (remark)
+                formatAppend(result, "REMARK %s\n", debugRemarkBuffer.c_str() + *remark);
+        }
+
         if (dumpFlags & Dump_Source)
         {
             int line = lines[code - insns.data()];

Compiler/src/Compiler.cpp

@@ -8,12 +8,17 @@
 
 #include "Builtins.h"
 #include "ConstantFolding.h"
+#include "CostModel.h"
 #include "TableShape.h"
 #include "ValueTracking.h"
 
 #include <algorithm>
 #include <bitset>
 #include <math.h>
+#include <limits.h>
+
+LUAU_FASTINTVARIABLE(LuauCompileLoopUnrollThreshold, 25)
+LUAU_FASTINTVARIABLE(LuauCompileLoopUnrollThresholdMaxBoost, 300)
 
 namespace Luau
 {
@@ -77,8 +82,12 @@ struct Compiler
         , globals(AstName())
         , variables(nullptr)
         , constants(nullptr)
+        , locstants(nullptr)
         , tableShapes(nullptr)
     {
+        // preallocate some buffers that are very likely to grow anyway; this works around std::vector's inefficient growth policy for small arrays
+        localStack.reserve(16);
+        upvals.reserve(16);
     }
 
     uint8_t getLocal(AstLocal* local)
@@ -209,7 +218,9 @@ struct Compiler
 
         Function& f = functions[func];
         f.id = fid;
-        f.upvals = std::move(upvals);
+        f.upvals = upvals;
+
+        upvals.clear(); // note: instead of std::move above, we copy & clear to preserve capacity for future pushes
 
         return fid;
     }
@@ -2133,10 +2144,119 @@ struct Compiler
             pushLocal(stat->vars.data[i], uint8_t(vars + i));
     }
 
+    int getConstantShort(AstExpr* expr)
+    {
+        const Constant* c = constants.find(expr);
+
+        if (c && c->type == Constant::Type_Number)
+        {
+            double n = c->valueNumber;
+
+            if (n >= -32767 && n <= 32767 && double(int(n)) == n)
+                return int(n);
+        }
+
+        return INT_MIN;
+    }
+
+    bool canUnrollForBody(AstStatFor* stat)
+    {
+        struct CanUnrollVisitor : AstVisitor
+        {
+            bool result = true;
+
+            bool visit(AstExpr* node) override
+            {
+                // functions may capture loop variable, and our upval handling doesn't handle elided variables (constant)
+                result = result && !node->is<AstExprFunction>();
+                return result;
+            }
+
+            bool visit(AstStat* node) override
+            {
+                // while we can easily unroll nested loops, our cost model doesn't take unrolling into account so this can result in code explosion
+                // we also avoid continue/break since they introduce control flow across iterations
+                result = result && !node->is<AstStatFor>() && !node->is<AstStatContinue>() && !node->is<AstStatBreak>();
+                return result;
+            }
+        };
+
+        CanUnrollVisitor canUnroll;
+        stat->body->visit(&canUnroll);
+
+        return canUnroll.result;
+    }
+
+    bool tryCompileUnrolledFor(AstStatFor* stat, int thresholdBase, int thresholdMaxBoost)
+    {
+        int from = getConstantShort(stat->from);
+        int to = getConstantShort(stat->to);
+        int step = stat->step ? getConstantShort(stat->step) : 1;
+
+        // check that limits are reasonably small and trip count can be computed
+        if (from == INT_MIN || to == INT_MIN || step == INT_MIN || step == 0 || (step < 0 && to > from) || (step > 0 && to < from))
+        {
+            bytecode.addDebugRemark("loop unroll failed: invalid iteration count");
+            return false;
+        }
+
+        if (!canUnrollForBody(stat))
+        {
+            bytecode.addDebugRemark("loop unroll failed: unsupported loop body");
+            return false;
+        }
+
+        int tripCount = (to - from) / step + 1;
+
+        if (tripCount > thresholdBase * thresholdMaxBoost / 100)
+        {
+            bytecode.addDebugRemark("loop unroll failed: too many iterations (%d)", tripCount);
+            return false;
+        }
+
+        AstLocal* var = stat->var;
+        uint64_t costModel = modelCost(stat->body, &var, 1);
+
+        // we use a dynamic cost threshold that's based on the fixed limit boosted by the cost advantage we gain due to unrolling
+        bool varc = true;
+        int unrolledCost = computeCost(costModel, &varc, 1) * tripCount;
+        int baselineCost = (computeCost(costModel, nullptr, 0) + 1) * tripCount;
+        int unrollProfit = (unrolledCost == 0) ? thresholdMaxBoost : std::min(thresholdMaxBoost, 100 * baselineCost / unrolledCost);
+
+        int threshold = thresholdBase * unrollProfit / 100;
+
+        if (unrolledCost > threshold)
+        {
+            bytecode.addDebugRemark(
+                "loop unroll failed: too expensive (iterations %d, cost %d, profit %.2fx)", tripCount, unrolledCost, double(unrollProfit) / 100);
+            return false;
+        }
+
+        bytecode.addDebugRemark("loop unroll succeeded (iterations %d, cost %d, profit %.2fx)", tripCount, unrolledCost, double(unrollProfit) / 100);
+
+        for (int i = from; step > 0 ? i <= to : i >= to; i += step)
+        {
+            // we need to re-fold constants in the loop body with the new value; this reuses computed constant values elsewhere in the tree
+            locstants[var].type = Constant::Type_Number;
+            locstants[var].valueNumber = i;
+
+            foldConstants(constants, variables, locstants, stat);
+
+            compileStat(stat->body);
+        }
+
+        return true;
+    }
+
     void compileStatFor(AstStatFor* stat)
     {
         RegScope rs(this);
 
+        // Optimization: small loops can be unrolled when it is profitable
+        if (options.optimizationLevel >= 2 && isConstant(stat->to) && isConstant(stat->from) && (!stat->step || isConstant(stat->step)))
+            if (tryCompileUnrolledFor(stat, FInt::LuauCompileLoopUnrollThreshold, FInt::LuauCompileLoopUnrollThresholdMaxBoost))
+                return;
+
         size_t oldLocals = localStack.size();
         size_t oldJumps = loopJumps.size();
 
@@ -2826,6 +2946,8 @@ struct Compiler
             : self(self)
             , functions(functions)
         {
+            // preallocate the result; this works around std::vector's inefficient growth policy for small arrays
+            functions.reserve(16);
         }
 
         bool visit(AstExprFunction* node) override
@@ -2979,6 +3101,7 @@ struct Compiler
     DenseHashMap<AstName, Global> globals;
     DenseHashMap<AstLocal*, Variable> variables;
     DenseHashMap<AstExpr*, Constant> constants;
+    DenseHashMap<AstLocal*, Constant> locstants;
     DenseHashMap<AstExprTable*, TableShape> tableShapes;
 
     unsigned int regTop = 0;
@@ -3008,7 +3131,7 @@ void compileOrThrow(BytecodeBuilder& bytecode, AstStatBlock* root, const AstName
     if (options.optimizationLevel >= 1)
     {
         // this pass analyzes constantness of expressions
-        foldConstants(compiler.constants, compiler.variables, root);
+        foldConstants(compiler.constants, compiler.variables, compiler.locstants, root);
 
         // this pass analyzes table assignments to estimate table shapes for initially empty tables
         predictTableShapes(compiler.tableShapes, root);

Compiler/src/ConstantFolding.cpp

@@ -191,13 +191,13 @@ struct ConstantVisitor : AstVisitor
 {
     DenseHashMap<AstExpr*, Constant>& constants;
     DenseHashMap<AstLocal*, Variable>& variables;
+    DenseHashMap<AstLocal*, Constant>& locals;
 
-    DenseHashMap<AstLocal*, Constant> locals;
-
-    ConstantVisitor(DenseHashMap<AstExpr*, Constant>& constants, DenseHashMap<AstLocal*, Variable>& variables)
+    ConstantVisitor(
+        DenseHashMap<AstExpr*, Constant>& constants, DenseHashMap<AstLocal*, Variable>& variables, DenseHashMap<AstLocal*, Constant>& locals)
         : constants(constants)
         , variables(variables)
-        , locals(nullptr)
+        , locals(locals)
     {
     }
 
@@ -385,9 +385,10 @@ struct ConstantVisitor : AstVisitor
     }
 };
 
-void foldConstants(DenseHashMap<AstExpr*, Constant>& constants, DenseHashMap<AstLocal*, Variable>& variables, AstNode* root)
+void foldConstants(DenseHashMap<AstExpr*, Constant>& constants, DenseHashMap<AstLocal*, Variable>& variables,
+    DenseHashMap<AstLocal*, Constant>& locals, AstNode* root)
 {
-    ConstantVisitor visitor{constants, variables};
+    ConstantVisitor visitor{constants, variables, locals};
     root->visit(&visitor);
 }
 

Compiler/src/ConstantFolding.h

@@ -42,7 +42,8 @@ struct Constant
     }
 };
 
-void foldConstants(DenseHashMap<AstExpr*, Constant>& constants, DenseHashMap<AstLocal*, Variable>& variables, AstNode* root);
+void foldConstants(DenseHashMap<AstExpr*, Constant>& constants, DenseHashMap<AstLocal*, Variable>& variables,
+    DenseHashMap<AstLocal*, Constant>& locals, AstNode* root);
 
 } // namespace Compile
 } // namespace Luau

VM/src/lapi.cpp

@@ -14,6 +14,8 @@
 
 #include <string.h>
 
+LUAU_FASTFLAG(LuauGcWorkTrackFix)
+
 const char* lua_ident = "$Lua: Lua 5.1.4 Copyright (C) 1994-2008 Lua.org, PUC-Rio $\n"
                         "$Authors: R. Ierusalimschy, L. H. de Figueiredo & W. Celes $\n"
                         "$URL: www.lua.org $\n";
@@ -1050,6 +1052,7 @@ int lua_gc(lua_State* L, int what, int data)
     {
         size_t prevthreshold = g->GCthreshold;
         size_t amount = (cast_to(size_t, data) << 10);
+        ptrdiff_t oldcredit = g->gcstate == GCSpause ? 0 : g->GCthreshold - g->totalbytes;
 
         // temporarily adjust the threshold so that we can perform GC work
         if (amount <= g->totalbytes)
@@ -1069,9 +1072,9 @@ int lua_gc(lua_State* L, int what, int data)
 
         while (g->GCthreshold <= g->totalbytes)
         {
-            luaC_step(L, false);
+            size_t stepsize = luaC_step(L, false);
 
-            actualwork += g->gcstepsize;
+            actualwork += FFlag::LuauGcWorkTrackFix ? stepsize : g->gcstepsize;
 
             if (g->gcstate == GCSpause)
             {            /* end of cycle? */
@@ -1107,11 +1110,20 @@ int lua_gc(lua_State* L, int what, int data)
         // if cycle hasn't finished, advance threshold forward for the amount of extra work performed
         if (g->gcstate != GCSpause)
         {
-            // if a new cycle was triggered by explicit step, we ignore old threshold as that shows an incorrect 'credit' of GC work
-            if (waspaused)
-                g->GCthreshold = g->totalbytes + actualwork;
+            if (FFlag::LuauGcWorkTrackFix)
+            {
+                // if a new cycle was triggered by explicit step, old 'credit' of GC work is 0
+                ptrdiff_t newthreshold = g->totalbytes + actualwork + oldcredit;
+                g->GCthreshold = newthreshold < 0 ? 0 : newthreshold;
+            }
             else
-                g->GCthreshold = prevthreshold + actualwork;
+            {
+                // if a new cycle was triggered by explicit step, we ignore old threshold as that shows an incorrect 'credit' of GC work
+                if (waspaused)
+                    g->GCthreshold = g->totalbytes + actualwork;
+                else
+                    g->GCthreshold = prevthreshold + actualwork;
+            }
         }
         break;
     }

VM/src/lgc.cpp

@@ -13,9 +13,10 @@
 
 #include <string.h>
 
-#define GC_SWEEPMAX 40
-#define GC_SWEEPCOST 10
-#define GC_SWEEPPAGESTEPCOST 4
+LUAU_FASTFLAGVARIABLE(LuauGcWorkTrackFix, false)
+LUAU_FASTFLAGVARIABLE(LuauGcSweepCostFix, false)
+
+#define GC_SWEEPPAGESTEPCOST (FFlag::LuauGcSweepCostFix ? 16 : 4)
 
 #define GC_INTERRUPT(state) \
     { \
@@ -64,7 +65,7 @@ static void recordGcStateStep(global_State* g, int startgcstate, double seconds,
     case GCSpropagate:
     case GCSpropagateagain:
         g->gcmetrics.currcycle.marktime += seconds;
-        g->gcmetrics.currcycle.markrequests += g->gcstepsize;
+        g->gcmetrics.currcycle.markwork += work;
 
         if (assist)
             g->gcmetrics.currcycle.markassisttime += seconds;
@@ -74,7 +75,7 @@ static void recordGcStateStep(global_State* g, int startgcstate, double seconds,
         break;
     case GCSsweep:
         g->gcmetrics.currcycle.sweeptime += seconds;
-        g->gcmetrics.currcycle.sweeprequests += g->gcstepsize;
+        g->gcmetrics.currcycle.sweepwork += work;
 
         if (assist)
             g->gcmetrics.currcycle.sweepassisttime += seconds;
@@ -87,13 +88,11 @@ static void recordGcStateStep(global_State* g, int startgcstate, double seconds,
     {
         g->gcmetrics.stepassisttimeacc += seconds;
         g->gcmetrics.currcycle.assistwork += work;
-        g->gcmetrics.currcycle.assistrequests += g->gcstepsize;
     }
     else
     {
         g->gcmetrics.stepexplicittimeacc += seconds;
         g->gcmetrics.currcycle.explicitwork += work;
-        g->gcmetrics.currcycle.explicitrequests += g->gcstepsize;
     }
 }
 
@@ -878,11 +877,11 @@ static size_t getheaptrigger(global_State* g, size_t heapgoal)
     return heaptrigger < int64_t(g->totalbytes) ? g->totalbytes : (heaptrigger > int64_t(heapgoal) ? heapgoal : size_t(heaptrigger));
 }
 
-void luaC_step(lua_State* L, bool assist)
+size_t luaC_step(lua_State* L, bool assist)
 {
     global_State* g = L->global;
 
-    int lim = (g->gcstepsize / 100) * g->gcstepmul; /* how much to work */
+    int lim = FFlag::LuauGcWorkTrackFix ? g->gcstepsize * g->gcstepmul / 100 : (g->gcstepsize / 100) * g->gcstepmul; /* how much to work */
     LUAU_ASSERT(g->totalbytes >= g->GCthreshold);
     size_t debt = g->totalbytes - g->GCthreshold;
 
@@ -902,12 +901,13 @@ void luaC_step(lua_State* L, bool assist)
     int lastgcstate = g->gcstate;
 
     size_t work = gcstep(L, lim);
-    (void)work;
 
 #ifdef LUAI_GCMETRICS
     recordGcStateStep(g, lastgcstate, lua_clock() - lasttimestamp, assist, work);
 #endif
 
+    size_t actualstepsize = work * 100 / g->gcstepmul;
+
     // at the end of the last cycle
     if (g->gcstate == GCSpause)
     {
@@ -927,14 +927,16 @@ void luaC_step(lua_State* L, bool assist)
     }
     else
     {
-        g->GCthreshold = g->totalbytes + g->gcstepsize;
+        g->GCthreshold = g->totalbytes + (FFlag::LuauGcWorkTrackFix ? actualstepsize : g->gcstepsize);
 
         // compensate if GC is "behind schedule" (has some debt to pay)
-        if (g->GCthreshold > debt)
+        if (FFlag::LuauGcWorkTrackFix ? g->GCthreshold >= debt : g->GCthreshold > debt)
             g->GCthreshold -= debt;
     }
 
     GC_INTERRUPT(lastgcstate);
+
+    return actualstepsize;
 }
 
 void luaC_fullgc(lua_State* L)

VM/src/lgc.h

@@ -133,7 +133,7 @@
 #define luaC_init(L, o, tt) luaC_initobj(L, cast_to(GCObject*, (o)), tt)
 
 LUAI_FUNC void luaC_freeall(lua_State* L);
-LUAI_FUNC void luaC_step(lua_State* L, bool assist);
+LUAI_FUNC size_t luaC_step(lua_State* L, bool assist);
 LUAI_FUNC void luaC_fullgc(lua_State* L);
 LUAI_FUNC void luaC_initobj(lua_State* L, GCObject* o, uint8_t tt);
 LUAI_FUNC void luaC_initupval(lua_State* L, UpVal* uv);

VM/src/lstate.h

@@ -106,7 +106,7 @@ struct GCCycleMetrics
     double markassisttime = 0.0;
     double markmaxexplicittime = 0.0;
     size_t markexplicitsteps = 0;
-    size_t markrequests = 0;
+    size_t markwork = 0;
 
     double atomicstarttimestamp = 0.0;
     size_t atomicstarttotalsizebytes = 0;
@@ -122,10 +122,7 @@ struct GCCycleMetrics
     double sweepassisttime = 0.0;
     double sweepmaxexplicittime = 0.0;
     size_t sweepexplicitsteps = 0;
-    size_t sweeprequests = 0;
-
-    size_t assistrequests = 0;
-    size_t explicitrequests = 0;
+    size_t sweepwork = 0;
 
     size_t assistwork = 0;
     size_t explicitwork = 0;

bench/bench.py

@@ -814,13 +814,12 @@ def run(args, argsubcb):
 
             analyzeResult('', mainResult, compareResults)
     else:
-        for subdir, dirs, files in os.walk(arguments.folder):
-            for filename in files:
-                filepath = subdir + os.sep + filename
-
-                if filename.endswith(".lua"):
-                    if arguments.run_test == None or re.match(arguments.run_test, filename[:-4]):
-                        runTest(subdir, filename, filepath)
+        all_files = [subdir + os.sep + filename for subdir, dirs, files in os.walk(arguments.folder) for filename in files]
+        for filepath in sorted(all_files):
+            subdir, filename = os.path.split(filepath)
+            if filename.endswith(".lua"):
+                if arguments.run_test == None or re.match(arguments.run_test, filename[:-4]):
+                    runTest(subdir, filename, filepath)
 
     if arguments.sort and len(plotValueLists) > 1:
         rearrange(rearrangeSortKeyForComparison)

fuzz/proto.cpp

@@ -103,7 +103,7 @@ int registerTypes(Luau::TypeChecker& env)
     // Vector3 stub
     TypeId vector3MetaType = arena.addType(TableTypeVar{});
 
-    TypeId vector3InstanceType = arena.addType(ClassTypeVar{"Vector3", {}, nullopt, vector3MetaType, {}, {}});
+    TypeId vector3InstanceType = arena.addType(ClassTypeVar{"Vector3", {}, nullopt, vector3MetaType, {}, {}, "Test"});
     getMutable<ClassTypeVar>(vector3InstanceType)->props = {
         {"X", {env.numberType}},
         {"Y", {env.numberType}},
@@ -117,7 +117,7 @@ int registerTypes(Luau::TypeChecker& env)
     env.globalScope->exportedTypeBindings["Vector3"] = TypeFun{{}, vector3InstanceType};
 
     // Instance stub
-    TypeId instanceType = arena.addType(ClassTypeVar{"Instance", {}, nullopt, nullopt, {}, {}});
+    TypeId instanceType = arena.addType(ClassTypeVar{"Instance", {}, nullopt, nullopt, {}, {}, "Test"});
     getMutable<ClassTypeVar>(instanceType)->props = {
         {"Name", {env.stringType}},
     };
@@ -125,7 +125,7 @@ int registerTypes(Luau::TypeChecker& env)
     env.globalScope->exportedTypeBindings["Instance"] = TypeFun{{}, instanceType};
 
     // Part stub
-    TypeId partType = arena.addType(ClassTypeVar{"Part", {}, instanceType, nullopt, {}, {}});
+    TypeId partType = arena.addType(ClassTypeVar{"Part", {}, instanceType, nullopt, {}, {}, "Test"});
     getMutable<ClassTypeVar>(partType)->props = {
         {"Position", {vector3InstanceType}},
     };
@@ -173,7 +173,7 @@ struct FuzzConfigResolver : Luau::ConfigResolver
 {
     FuzzConfigResolver()
     {
-        defaultConfig.mode = Luau::Mode::Nonstrict; // typecheckTwice option will cover Strict mode
+        defaultConfig.mode = Luau::Mode::Nonstrict;
         defaultConfig.enabledLint.warningMask = ~0ull;
         defaultConfig.parseOptions.captureComments = true;
     }
@@ -275,6 +275,11 @@ DEFINE_PROTO_FUZZER(const luau::ModuleSet& message)
                 // lint (note that we need access to types so we need to do this with typeck in scope)
                 if (kFuzzLinter && result.errors.empty())
                     frontend.lint(name, std::nullopt);
+
+                // Second pass in strict mode (forced by auto-complete)
+                Luau::FrontendOptions opts;
+                opts.forAutocomplete = true;
+                frontend.check(name, opts);
             }
             catch (std::exception&)
             {

prototyping/Luau/FunctionTypes.agda

@@ -0,0 +1,38 @@
+{-# OPTIONS --rewriting #-}
+
+open import FFI.Data.Either using (Either; Left; Right)
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Luau.TypeNormalization using (normalize)
+
+module Luau.FunctionTypes where
+
+-- The domain of a normalized type
+srcⁿ : Type → Type
+srcⁿ (S ⇒ T) = S
+srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
+srcⁿ never = unknown
+srcⁿ T = never
+
+-- To get the domain of a type, we normalize it first We need to do
+-- this, since if we try to use it on non-normalized types, we get
+--
+-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
+-- src(never) = unknown
+--
+-- so src doesn't respect type equivalence.
+src : Type → Type
+src (S ⇒ T) = S
+src T = srcⁿ(normalize T)
+
+-- The codomain of a type
+tgt : Type → Type
+tgt nil = never
+tgt (S ⇒ T) = T
+tgt never = never
+tgt unknown = unknown
+tgt number = never
+tgt boolean = never
+tgt string = never
+tgt (S ∪ T) = (tgt S) ∪ (tgt T)
+tgt (S ∩ T) = (tgt S) ∩ (tgt T)
+

prototyping/Luau/StrictMode.agda

@@ -5,7 +5,8 @@ module Luau.StrictMode where
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_; src; tgt)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_)
 open import Luau.Subtyping using (_≮:_)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)

prototyping/Luau/Subtyping.agda

@@ -26,7 +26,6 @@ data Language where
   function-ok₁ : ∀ {T U t u} → (¬Language T t) → Language (T ⇒ U) (function-ok t u)
   function-ok₂ : ∀ {T U t u} → (Language U u) → Language (T ⇒ U) (function-ok t u)
   function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
-  scalar-function-err : ∀ {S t} → (Scalar S) → Language S (function-err t)
   left : ∀ {T U t} → Language T t → Language (T ∪ U) t
   right : ∀ {T U u} → Language U u → Language (T ∪ U) u
   _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
@@ -37,6 +36,7 @@ data ¬Language where
   scalar-scalar : ∀ {S T} → (s : Scalar S) → (Scalar T) → (S ≢ T) → ¬Language T (scalar s)
   scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
   scalar-function-ok : ∀ {S t u} → (Scalar S) → ¬Language S (function-ok t u)
+  scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
   function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
   function-ok : ∀ {T U t u} → (Language T t) → (¬Language U u) → ¬Language (T ⇒ U) (function-ok t u)
   function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)

prototyping/Luau/Type.agda

@@ -24,6 +24,8 @@ data Scalar : Type → Set where
   string : Scalar string
   nil : Scalar nil
 
+skalar = number ∪ (string ∪ (nil ∪ boolean))
+
 lhs : Type → Type
 lhs (T ⇒ _) = T
 lhs (T ∪ _) = T
@@ -146,28 +148,6 @@ just T ≡ᴹᵀ just U with T ≡ᵀ U
 (just T ≡ᴹᵀ just T) | yes refl = yes refl
 (just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q))
 
-src : Type → Type
-src nil = never
-src number = never
-src boolean = never
-src string = never
-src (S ⇒ T) = S
-src (S ∪ T) = (src S) ∩ (src T)
-src (S ∩ T) = (src S) ∪ (src T)
-src never = unknown
-src unknown = never
-
-tgt : Type → Type
-tgt nil = never
-tgt (S ⇒ T) = T
-tgt never = never
-tgt unknown = unknown
-tgt number = never
-tgt boolean = never
-tgt string = never
-tgt (S ∪ T) = (tgt S) ∪ (tgt T)
-tgt (S ∩ T) = (tgt S) ∩ (tgt T)
-
 optional : Type → Type
 optional nil = nil
 optional (T ∪ nil) = (T ∪ nil)

prototyping/Luau/TypeCheck.agda

@@ -8,14 +8,13 @@ open import FFI.Data.Maybe using (Maybe; just)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
-open import Luau.OverloadedFunctions using (resolve)
+open import Luau.FunctionTypes using (src)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.Subtyping using (_≮:_; _<:_)
-open import Luau.Type using (Type; nil; never; unknown; number; boolean; string; _⇒_; _∪_; _∩_; src; tgt)
+open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
-open import Properties.DecSubtyping using (dec-subtyping)
+open import Properties.DecSubtyping using (dec-subtyping; resolve)
 open import Properties.Product using (_×_; _,_)
 
 orUnknown : Maybe Type → Type

prototyping/Luau/TypeNormalization.agda

@@ -1,6 +1,6 @@
 module Luau.TypeNormalization where
 
-open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
 
 -- The top non-function type
 ¬function : Type
@@ -8,33 +8,24 @@ open import Luau.Type using (Type; nil; number; string; boolean; never; unknown;
 
 -- Unions and intersections of normalized types
 _∪ᶠ_ : Type → Type → Type
-_∩ᶠ_ : Type → Type → Type
 _∪ⁿˢ_ : Type → Type → Type
 _∩ⁿˢ_ : Type → Type → Type
 _∪ⁿ_ : Type → Type → Type
 _∩ⁿ_ : Type → Type → Type
-_⇒ᶠ_ : Type → Type → Type
 
 -- Union of function types
-never ∪ᶠ G = G
-F ∪ᶠ never = F
-(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ᶠ (F₂ ∪ᶠ G)
-F ∪ᶠ (G₁ ∩ G₂) = (F ∪ᶠ G₁) ∩ᶠ (F ∪ᶠ G₂)
-(R ⇒ S) ∪ᶠ (T ⇒ U) = (R ∩ⁿ T) ⇒ᶠ (S ∪ⁿ U)
+(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
+F ∪ᶠ (G₁ ∩ G₂) = (F ∪ᶠ G₁) ∩ (F ∪ᶠ G₂)
+(R ⇒ S) ∪ᶠ (T ⇒ U) = (R ∩ⁿ T) ⇒ (S ∪ⁿ U)
 F ∪ᶠ G = F ∪ G
 
--- Intersection of function types
-F ∩ᶠ never = never
-never ∩ᶠ G = never
-F ∩ᶠ G = F ∩ G
-
 -- Union of normalized types
 S ∪ⁿ (T₁ ∪ T₂) = (S ∪ⁿ T₁) ∪ T₂
 S ∪ⁿ unknown = unknown
 S ∪ⁿ never = S
 unknown ∪ⁿ T = unknown
 never ∪ⁿ T = T
-(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂ 
+(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
 F ∪ⁿ G = F ∪ᶠ G
 
 -- Intersection of normalized types
@@ -44,7 +35,7 @@ S ∩ⁿ never = never
 (S₁ ∪ S₂) ∩ⁿ G = (S₁ ∩ⁿ G)
 unknown ∩ⁿ G = G
 never ∩ⁿ G = never
-F ∩ⁿ G = F ∩ᶠ G
+F ∩ⁿ G = F ∩ G
 
 -- Intersection of normalized types with a scalar
 (S₁ ∪ nil) ∩ⁿˢ nil = nil
@@ -52,6 +43,7 @@ F ∩ⁿ G = F ∩ᶠ G
 (S₁ ∪ number) ∩ⁿˢ number = number
 (S₁ ∪ string) ∩ⁿˢ string = string
 (S₁ ∪ S₂) ∩ⁿˢ T = S₁ ∩ⁿˢ T
+unknown ∩ⁿˢ T = T
 F ∩ⁿˢ T = never
 
 -- Union of normalized types with an optional scalar
@@ -60,18 +52,14 @@ unknown ∪ⁿˢ T = unknown
 (S₁ ∪ nil) ∪ⁿˢ nil = S₁ ∪ nil
 (S₁ ∪ boolean) ∪ⁿˢ boolean = S₁ ∪ boolean
 (S₁ ∪ number) ∪ⁿˢ number = S₁ ∪ number
-(S₁ ∪ string) ∪ⁿˢ string = S₁ ∪ number
-(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₁
+(S₁ ∪ string) ∪ⁿˢ string = S₁ ∪ string
+(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₂
 F ∪ⁿˢ T = F ∪ T
 
--- Functions between normalized types
-(never ⇒ᶠ T) = (never ⇒ unknown)
-(S ⇒ᶠ T) = (S ⇒ T)
-
 -- Normalize!
 normalize : Type → Type
 normalize nil = never ∪ nil
-normalize (S ⇒ T) = (normalize S ⇒ᶠ normalize T)
+normalize (S ⇒ T) = (normalize S ⇒ normalize T)
 normalize never = never
 normalize unknown = unknown
 normalize boolean = never ∪ boolean
@@ -79,4 +67,3 @@ normalize number = never ∪ number
 normalize string = never ∪ string
 normalize (S ∪ T) = normalize S ∪ⁿ normalize T
 normalize (S ∩ T) = normalize S ∩ⁿ normalize T
-

prototyping/Properties.agda

@@ -4,11 +4,13 @@ module Properties where
 
 import Properties.Contradiction
 import Properties.Dec
+import Properties.DecSubtyping
 import Properties.Equality
 import Properties.Functions
-import Properties.OverloadedFunctions
+import Properties.FunctionTypes
 import Properties.Remember
 import Properties.Step
 import Properties.StrictMode
 import Properties.Subtyping
 import Properties.TypeCheck
+import Properties.TypeNormalization

prototyping/Properties/DecSubtyping.agda

@@ -1,117 +1,74 @@
 {-# OPTIONS --rewriting #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 
 module Properties.DecSubtyping where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
-open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
-open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src; tgt)
+open import Luau.FunctionTypes using (src; srcⁿ; tgt)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
 open import Properties.Contradiction using (CONTRADICTION; ¬)
 open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-union)
+open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
+open import Properties.FunctionTypes using (fun-¬scalar; ¬fun-scalar; fun-function; src-unknown-≮:)
+open import Properties.Equality using (_≢_)
 
--- ¬Language T is the complement of Language T
-language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
-language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q
-language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q
-language-comp t (left p) (q₁ , q₂) = language-comp t p q₁
-language-comp t (right p) (q₁ , q₂) = language-comp t p q₂
-language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
-language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
-language-comp (scalar s) never (scalar ())
-language-comp function (scalar-function ()) function
-language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₁ _)
-language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₂ _)
-language-comp (function-ok s t) (function-ok p _) (function-ok₁ q) = language-comp s q p
-language-comp (function-ok s t) (function-ok _ p) (function-ok₂ q) = language-comp t p q
-language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
+-- Honest this terminates, since src and tgt reduce the depth of nested arrows
+{-# TERMINATING #-}
+dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtypingᶠ : ∀ {T U} → FunType T → FunType U → Either (T ≮: U) (T <: U)
+dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
 
--- Properties of src
-function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t)
-function-err-src {T = nil} never = scalar-function-err nil
-function-err-src {T = T₁ ⇒ T₂} p = function-err p
-function-err-src {T = never} (scalar-scalar number () p)
-function-err-src {T = never} (scalar-function-ok ())
-function-err-src {T = unknown} never = unknown
-function-err-src {T = boolean} p = scalar-function-err boolean
-function-err-src {T = number} p = scalar-function-err number
-function-err-src {T = string} p = scalar-function-err string
-function-err-src {T = T₁ ∪ T₂} (left p) = left (function-err-src p)
-function-err-src {T = T₁ ∪ T₂} (right p) = right (function-err-src p)
-function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂
+resolve : Type → Type → Type
+resolve (S ⇒ T) V = T
+resolve T = {!!}
 
-¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
-¬function-err-src {T = nil} (scalar ())
-¬function-err-src {T = T₁ ⇒ T₂} p = function-err p
-¬function-err-src {T = never} unknown = never
-¬function-err-src {T = unknown} (scalar ())
-¬function-err-src {T = boolean} (scalar ())
-¬function-err-src {T = number} (scalar ())
-¬function-err-src {T = string} (scalar ())
-¬function-err-src {T = T₁ ∪ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂)
-¬function-err-src {T = T₁ ∩ T₂} (left p) = left (¬function-err-src p)
-¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p)
+dec-subtypingˢⁿ T U with dec-language _ (scalar T)
+dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p)
+dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)
 
-src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
-src-¬function-err {T = nil} p = never
-src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p
-src-¬function-err {T = never} (scalar-function-err ())
-src-¬function-err {T = unknown} p = never
-src-¬function-err {T = boolean} p = never
-src-¬function-err {T = number} p = never
-src-¬function-err {T = string} p = never
-src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p)
-src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p)
-src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂)
+dec-subtypingᶠ {T = T} _ (U ⇒ V) with dec-subtypingⁿ U (normal (src T)) | dec-subtypingⁿ (normal (tgt T)) V
+dec-subtypingᶠ {T = T} _ (U ⇒ V) | Left p | q = Left (≮:-trans-<: (src-unknown-≮: (≮:-trans-<: p (<:-normalize (src T)))) (<:-function <:-refl <:-unknown))
+dec-subtypingᶠ {T = T} _ (U ⇒ V) | Right p | Left q = {!!} -- Left (≮:-trans-<: (tgt-never-≮: (<:-trans-≮: (normalize-<: (tgt T)) q)) (<:-trans (<:-function <:-never <:-refl) <:-∪-right))
+dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = {!!} -- Right (src-tgtᶠ-<: T (<:-trans p (normalize-<: _)) (<:-trans (<:-normalize _) q))
 
-src-≮: : ∀ {T U} → (src T ≮: src U) → (U ≮: T)
-src-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p)
+dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V
+dec-subtypingᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p)
+dec-subtypingᶠ T (U ∩ V) | Right p | Left q = Left (≮:-∩-right q)
+dec-subtypingᶠ T (U ∩ V) | Right p | Right q = Right (<:-∩-glb p q)
 
--- Language membership is decidable
-dec-language : ∀ T t → Either (¬Language T t) (Language T t)
-dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ()))
-dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
-dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
-dec-language nil (scalar nil) = Right (scalar nil)
-dec-language nil function = Left (scalar-function nil)
-dec-language nil (function-ok s t) = Left (scalar-function-ok nil)
-dec-language nil (function-err t) = Right (scalar-function-err nil)
-dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
-dec-language boolean (scalar boolean) = Right (scalar boolean)
-dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
-dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
-dec-language boolean function = Left (scalar-function boolean)
-dec-language boolean (function-ok s t) = Left (scalar-function-ok boolean)
-dec-language boolean (function-err t) = Right (scalar-function-err boolean)
-dec-language number (scalar number) = Right (scalar number)
-dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
-dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
-dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
-dec-language number function = Left (scalar-function number)
-dec-language number (function-ok s t) = Left (scalar-function-ok number)
-dec-language number (function-err t) = Right (scalar-function-err number)
-dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
-dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
-dec-language string (scalar string) = Right (scalar string)
-dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
-dec-language string function = Left (scalar-function string)
-dec-language string (function-ok s t) = Left (scalar-function-ok string)
-dec-language string (function-err t) = Right (scalar-function-err string)
-dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
-dec-language (T₁ ⇒ T₂) function = Right function
-dec-language (T₁ ⇒ T₂) (function-ok s t) = cond (Right ∘ function-ok₁) (λ p → mapLR (function-ok p) function-ok₂ (dec-language T₂ t)) (dec-language T₁ s)
-dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
-dec-language never t = Left never
-dec-language unknown t = Right unknown
-dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
-dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
+dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
+dec-subtypingᶠⁿ T unknown = Right <:-unknown
+dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
+dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
+dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
+dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , ¬fun-scalar V T p))
+dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)
 
--- if T <: U then ¬Language U ⊆ ¬Language T
-<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t
-<:-impl-⊇ {T} p t ¬Ut with dec-language T t
-<:-impl-⊇ p t ¬Ut | Left ¬Tt = ¬Tt
-<:-impl-⊇ p t ¬Ut | Right Tt = CONTRADICTION (language-comp t ¬Ut (p t Tt))
+dec-subtypingⁿ never U = Right <:-never
+dec-subtypingⁿ unknown unknown = Right <:-refl
+dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
+dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U
+dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ with dec-subtypingˢⁿ string U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ with dec-subtypingˢⁿ nil U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ with dec-subtypingˢⁿ boolean U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Right p₅ = Right (<:-trans <:-everything (<:-∪-lub p₁ (<:-∪-lub p₂ (<:-∪-lub p₃ (<:-∪-lub p₄ p₅)))))
+dec-subtypingⁿ (S ⇒ T) U = dec-subtypingᶠⁿ (S ⇒ T) U
+dec-subtypingⁿ (S ∩ T) U = dec-subtypingᶠⁿ (S ∩ T) U
+dec-subtypingⁿ (S ∪ T) U with dec-subtypingⁿ S U | dec-subtypingˢⁿ T U
+dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
+dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
+dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)
 
--- Subtyping is decidable
--- TODO: Prove this!
-
-postulate dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
+dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U)
+dec-subtyping T U | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U)))
+dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (normalize-<: U)))

prototyping/Properties/FunctionTypes.agda

@@ -0,0 +1,116 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.FunctionTypes where
+
+open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
+open import Luau.FunctionTypes using (srcⁿ; src; tgt)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
+open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; ≮:-refl; <:-trans-≮:; skalar-scalar; <:-impl-⊇; skalar-function-ok; language-comp)
+open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
+
+-- Properties of src
+function-err-srcⁿ : ∀ {T t} → (FunType T) → (¬Language (srcⁿ T) t) → Language T (function-err t)
+function-err-srcⁿ (S ⇒ T) p = function-err p
+function-err-srcⁿ (S ∩ T) (p₁ , p₂) = (function-err-srcⁿ S p₁ , function-err-srcⁿ T p₂)
+
+¬function-err-srcᶠ : ∀ {T t} → (FunType T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
+¬function-err-srcᶠ (S ⇒ T) p = function-err p
+¬function-err-srcᶠ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
+¬function-err-srcᶠ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)
+
+¬function-err-srcⁿ : ∀ {T t} → (Normal T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
+¬function-err-srcⁿ never p = never
+¬function-err-srcⁿ unknown (scalar ())
+¬function-err-srcⁿ (S ⇒ T) p = function-err p
+¬function-err-srcⁿ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
+¬function-err-srcⁿ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)
+¬function-err-srcⁿ (S ∪ T) (scalar ())
+
+¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
+¬function-err-src {T = S ⇒ T} p = function-err p
+¬function-err-src {T = nil} p = scalar-function-err nil
+¬function-err-src {T = never} p = never
+¬function-err-src {T = unknown} (scalar ())
+¬function-err-src {T = boolean} p = scalar-function-err boolean
+¬function-err-src {T = number} p = scalar-function-err number
+¬function-err-src {T = string} p = scalar-function-err string
+¬function-err-src {T = S ∪ T} p = <:-impl-⊇ (<:-normalize (S ∪ T)) _ (¬function-err-srcⁿ (normal (S ∪ T)) p)
+¬function-err-src {T = S ∩ T} p = <:-impl-⊇ (<:-normalize (S ∩ T)) _ (¬function-err-srcⁿ (normal (S ∩ T)) p)
+
+src-¬function-errᶠ : ∀ {T t} → (FunType T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
+src-¬function-errᶠ (S ⇒ T) (function-err p) = p
+src-¬function-errᶠ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
+
+src-¬function-errⁿ : ∀ {T t} → (Normal T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
+src-¬function-errⁿ unknown p = never
+src-¬function-errⁿ (S ⇒ T) (function-err p) = p
+src-¬function-errⁿ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
+src-¬function-errⁿ (S ∪ T) p = never
+
+src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
+src-¬function-err {T = S ⇒ T} (function-err p) = p
+src-¬function-err {T = unknown} p = never
+src-¬function-err {T = S ∪ T} p = src-¬function-errⁿ (normal (S ∪ T)) (<:-normalize (S ∪ T) _ p)
+src-¬function-err {T = S ∩ T} p = src-¬function-errⁿ (normal (S ∩ T)) (<:-normalize (S ∩ T) _ p)
+
+fun-¬scalar : ∀ {S T} (s : Scalar S) → FunType T → ¬Language T (scalar s)
+fun-¬scalar s (S ⇒ T) = function-scalar s
+fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S)
+
+¬fun-scalar : ∀ {S T t} (s : Scalar S) → FunType T → Language T t → ¬Language S t
+¬fun-scalar s (S ⇒ T) function = scalar-function s
+¬fun-scalar s (S ⇒ T) (function-ok₁ p) = scalar-function-ok s
+¬fun-scalar s (S ⇒ T) (function-ok₂ p) = scalar-function-ok s
+¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s
+¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂
+
+fun-function : ∀ {T} → FunType T → Language T function
+fun-function (S ⇒ T) = function
+fun-function (S ∩ T) = (fun-function S , fun-function T)
+
+srcⁿ-¬scalar : ∀ {S T t} (s : Scalar S) → Normal T → Language T (scalar s) → (¬Language (srcⁿ T) t)
+srcⁿ-¬scalar s never (scalar ())
+srcⁿ-¬scalar s unknown p = never
+srcⁿ-¬scalar s (S ⇒ T) (scalar ())
+srcⁿ-¬scalar s (S ∩ T) (p₁ , p₂) = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s S) p₁)
+srcⁿ-¬scalar s (S ∪ T) p = never
+
+src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
+src-¬scalar {T = nil} s p = never
+src-¬scalar {T = T ⇒ U} s (scalar ())
+src-¬scalar {T = never} s (scalar ())
+src-¬scalar {T = unknown} s p = never
+src-¬scalar {T = boolean} s p = never
+src-¬scalar {T = number} s p = never
+src-¬scalar {T = string} s p = never
+src-¬scalar {T = T ∪ U} s p = srcⁿ-¬scalar s (normal (T ∪ U)) (<:-normalize (T ∪ U) (scalar s) p)
+src-¬scalar {T = T ∩ U} s p = srcⁿ-¬scalar s (normal (T ∩ U)) (<:-normalize (T ∩ U) (scalar s) p)
+
+srcⁿ-unknown-≮: : ∀ {T U} → (Normal U) → (T ≮: srcⁿ U) → (U ≮: (T ⇒ unknown))
+srcⁿ-unknown-≮: never (witness t p q) = CONTRADICTION (language-comp t q unknown)
+srcⁿ-unknown-≮: unknown (witness t p q) = witness (function-err t) unknown (function-err p)
+srcⁿ-unknown-≮: (U ⇒ V) (witness t p q) = witness (function-err t) (function-err q) (function-err p)
+srcⁿ-unknown-≮: (U ∩ V) (witness t p q) = witness (function-err t) (function-err-srcⁿ (U ∩ V) q) (function-err p)
+srcⁿ-unknown-≮: (U ∪ V) (witness t p q) = witness (scalar V) (right (scalar V)) (function-scalar V)
+
+src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
+src-unknown-≮: {U = nil} (witness t p q) = witness (scalar nil) (scalar nil) (function-scalar nil)
+src-unknown-≮: {U = T ⇒ U} (witness t p q) = witness (function-err t) (function-err q) (function-err p)
+src-unknown-≮: {U = never} (witness t p q) = CONTRADICTION (language-comp t q unknown)
+src-unknown-≮: {U = unknown} (witness t p q) = witness (function-err t) unknown (function-err p)
+src-unknown-≮: {U = boolean} (witness t p q) = witness (scalar boolean) (scalar boolean) (function-scalar boolean)
+src-unknown-≮: {U = number} (witness t p q) = witness (scalar number) (scalar number) (function-scalar number)
+src-unknown-≮: {U = string} (witness t p q) = witness (scalar string) (scalar string) (function-scalar string)
+src-unknown-≮: {U = T ∪ U} p = <:-trans-≮: (normalize-<: (T ∪ U)) (srcⁿ-unknown-≮: (normal (T ∪ U)) p)
+src-unknown-≮: {U = T ∩ U} p = <:-trans-≮: (normalize-<: (T ∩ U)) (srcⁿ-unknown-≮: (normal (T ∩ U)) p)
+
+unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
+unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
+unknown-src-≮: r (witness (function-ok s .(scalar s₁)) p (function-ok x (scalar-scalar s₁ () x₂)))
+unknown-src-≮: r (witness (function-ok s .function) p (function-ok x (scalar-function ())))
+unknown-src-≮: r (witness (function-ok s .(function-ok _ _)) p (function-ok x (scalar-function-ok ())))
+unknown-src-≮: r (witness (function-ok s .(function-err _)) p (function-ok x (scalar-function-err ())))
+unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)

prototyping/Properties/StrictMode.agda

@@ -11,20 +11,22 @@ open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warning
 open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
 open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language)
 open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
-open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; src; tgt; _≡ᵀ_; _≡ᴹᵀ_)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; _≡ᵀ_; _≡ᴹᵀ_)
 open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp)
 open import Luau.Var using (_≡ⱽ_)
 open import Luau.Addr using (_≡ᴬ_)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
 open import Luau.VarCtxt using (VarCtxt; ∅)
-open import Luau.OverloadedFunctions using (resolve)
 open import Properties.Remember using (remember; _,_)
 open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
 open import Properties.Dec using (Dec; yes; no)
 open import Properties.Contradiction using (CONTRADICTION; ¬)
 open import Properties.Functions using (_∘_)
-open import Properties.DecSubtyping using (dec-subtyping)
-open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
+open import Properties.DecSubtyping using (dec-subtyping; resolve)
+open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
+open import Properties.FunctionTypes using (src-unknown-≮:; unknown-src-≮:)
+open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
 open import Properties.TypeCheck using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ)
 open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)

prototyping/Properties/Subtyping.agda

@@ -6,13 +6,66 @@ open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; left; right; _,_)
-open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src; tgt)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
 open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
-open import Properties.DecSubtyping using (language-comp; dec-language; function-err-src; ¬function-err-src; src-¬function-err; <:-impl-⊇)
 open import Properties.Equality using (_≢_)
 open import Properties.Functions using (_∘_)
 open import Properties.Product using (_×_; _,_)
 
+-- Language membership is decidable
+dec-language : ∀ T t → Either (¬Language T t) (Language T t)
+dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ()))
+dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
+dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
+dec-language nil (scalar nil) = Right (scalar nil)
+dec-language nil function = Left (scalar-function nil)
+dec-language nil (function-ok s t) = Left (scalar-function-ok nil)
+dec-language nil (function-err t) = Left (scalar-function-err nil)
+dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
+dec-language boolean (scalar boolean) = Right (scalar boolean)
+dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
+dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
+dec-language boolean function = Left (scalar-function boolean)
+dec-language boolean (function-ok s t) = Left (scalar-function-ok boolean)
+dec-language boolean (function-err t) = Left (scalar-function-err boolean)
+dec-language number (scalar number) = Right (scalar number)
+dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
+dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
+dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
+dec-language number function = Left (scalar-function number)
+dec-language number (function-ok s t) = Left (scalar-function-ok number)
+dec-language number (function-err t) = Left (scalar-function-err number)
+dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
+dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
+dec-language string (scalar string) = Right (scalar string)
+dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
+dec-language string function = Left (scalar-function string)
+dec-language string (function-ok s t) = Left (scalar-function-ok string)
+dec-language string (function-err t) = Left (scalar-function-err string)
+dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
+dec-language (T₁ ⇒ T₂) function = Right function
+dec-language (T₁ ⇒ T₂) (function-ok s t) = cond (Right ∘ function-ok₁) (λ p → mapLR (function-ok p) function-ok₂ (dec-language T₂ t)) (dec-language T₁ s)
+dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
+dec-language never t = Left never
+dec-language unknown t = Right unknown
+dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
+dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
+
+-- ¬Language T is the complement of Language T
+language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
+language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q
+language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q
+language-comp t (left p) (q₁ , q₂) = language-comp t p q₁
+language-comp t (right p) (q₁ , q₂) = language-comp t p q₂
+language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
+language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
+language-comp (scalar s) never (scalar ())
+language-comp function (scalar-function ()) function
+language-comp (function-ok s t) (scalar-function-ok ()) (function-ok₁ p)
+language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₁ q) = language-comp s q p₁
+language-comp (function-ok s t) (function-ok p₁ p₂) (function-ok₂ q) = language-comp t p₂ q
+language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
+
 -- ≮: is the complement of <:
 ¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
 ¬≮:-impl-<: {T} {U} p t q with dec-language U t
@@ -22,6 +75,11 @@ open import Properties.Product using (_×_; _,_)
 <:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U)
 <:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)
 
+<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t
+<:-impl-⊇ {T} p t q with dec-language T t
+<:-impl-⊇ {_} p t q | Left r = r
+<:-impl-⊇ {_} p t q | Right r = CONTRADICTION (language-comp t q (p t r))
+
 -- reflexivity
 ≮:-refl : ∀ {T} → ¬(T ≮: T)
 ≮:-refl (witness t p q) = language-comp t q p
@@ -45,6 +103,9 @@ open import Properties.Product using (_×_; _,_)
 <:-trans-≮: : ∀ {S T U} → (S <: T) → (S ≮: U) → (T ≮: U)
 <:-trans-≮: p (witness t q r) = witness t (p t q) r
 
+≮:-trans-<: : ∀ {S T U} → (S ≮: U) → (T <: U) → (S ≮: T)
+≮:-trans-<: (witness t p q) r = witness t p (<:-impl-⊇ r t q)
+
 -- Properties of union
 
 <:-union : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∪ S) <: (T ∪ U))
@@ -61,6 +122,20 @@ open import Properties.Product using (_×_; _,_)
 <:-∪-lub p q t (left r) = p t r
 <:-∪-lub p q t (right r) = q t r
 
+<:-∪-symm : ∀ {T U} → (T ∪ U) <: (U ∪ T)
+<:-∪-symm t (left p) = right p
+<:-∪-symm t (right p) = left p
+
+<:-∪-assocl : ∀ {S T U} → (S ∪ (T ∪ U)) <: ((S ∪ T) ∪ U)
+<:-∪-assocl t (left p) = left (left p)
+<:-∪-assocl t (right (left p)) = left (right p)
+<:-∪-assocl t (right (right p)) = right p
+
+<:-∪-assocr : ∀ {S T U} → ((S ∪ T) ∪ U) <: (S ∪ (T ∪ U))
+<:-∪-assocr t (left (left p)) = left p
+<:-∪-assocr t (left (right p)) = right (left p)
+<:-∪-assocr t (right p) = right (right p)
+
 ≮:-∪-left : ∀ {S T U} → (S ≮: U) → ((S ∪ T) ≮: U)
 ≮:-∪-left (witness t p q) = witness t (left p) q
 
@@ -81,6 +156,9 @@ open import Properties.Product using (_×_; _,_)
 <:-∩-glb : ∀ {S T U} → (S <: T) → (S <: U) → (S <: (T ∩ U))
 <:-∩-glb p q t r = (p t r , q t r)
 
+<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
+<:-∩-symm t (p₁ , p₂) = (p₂ , p₁)
+
 ≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
 ≮:-∩-left (witness t p q) = witness t p (left q)
 
@@ -88,22 +166,39 @@ open import Properties.Product using (_×_; _,_)
 ≮:-∩-right (witness t p q) = witness t p (right q)
 
 -- Distribution properties
-<:-∩-dist-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U))
-<:-∩-dist-∪ t (p₁ , left p₂) = left (p₁ , p₂)
-<:-∩-dist-∪ t (p₁ , right p₂) = right (p₁ , p₂)
+<:-∩-distl-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U))
+<:-∩-distl-∪ t (p₁ , left p₂) = left (p₁ , p₂)
+<:-∩-distl-∪ t (p₁ , right p₂) = right (p₁ , p₂)
 
-∩-dist-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U))
-∩-dist-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂)
-∩-dist-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂)
+∩-distl-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U))
+∩-distl-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂)
+∩-distl-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂)
 
-<:-∪-dist-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U))
-<:-∪-dist-∩ t (left p) = (left p , left p)
-<:-∪-dist-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂)
+<:-∩-distr-∪ : ∀ {S T U} → ((S ∪ T) ∩ U) <:  ((S ∩ U) ∪ (T ∩ U))
+<:-∩-distr-∪ t (left p₁ , p₂) = left (p₁ , p₂)
+<:-∩-distr-∪ t (right p₁ , p₂) = right (p₁ , p₂)
 
-∪-dist-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U))
-∪-dist-∩-<: t (left p₁ , p₂) = left p₁
-∪-dist-∩-<: t (right p₁ , left p₂) = left p₂
-∪-dist-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂)
+∩-distr-∪-<: : ∀ {S T U} → ((S ∩ U) ∪ (T ∩ U)) <: ((S ∪ T) ∩ U)
+∩-distr-∪-<: t (left (p₁ , p₂)) = (left p₁ , p₂)
+∩-distr-∪-<: t (right (p₁ , p₂)) = (right p₁ , p₂)
+
+<:-∪-distl-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U))
+<:-∪-distl-∩ t (left p) = (left p , left p)
+<:-∪-distl-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂)
+
+∪-distl-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U))
+∪-distl-∩-<: t (left p₁ , p₂) = left p₁
+∪-distl-∩-<: t (right p₁ , left p₂) = left p₂
+∪-distl-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂)
+
+<:-∪-distr-∩ : ∀ {S T U} → ((S ∩ T) ∪ U) <: ((S ∪ U) ∩ (T ∪ U))
+<:-∪-distr-∩ t (left (p₁ , p₂)) = left p₁ , left p₂
+<:-∪-distr-∩ t (right p) = (right p , right p)
+
+∪-distr-∩-<: : ∀ {S T U} → ((S ∪ U) ∩ (T ∪ U)) <: ((S ∩ T) ∪ U)
+∪-distr-∩-<: t (left p₁ , left p₂) = left (p₁ , p₂)
+∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
+∪-distr-∩-<: t (right p₁ , p₂) = right p₁
 
 -- Properties of functions
 <:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U)
@@ -116,7 +211,7 @@ open import Properties.Product using (_×_; _,_)
 <:-function-∩-∪ function (function , function) = function
 <:-function-∩-∪ (function-ok s t) (function-ok₁ p₁ , function-ok₁ p₂) = function-ok₁ (p₁ , p₂)
 <:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂)
-<:-function-∩-∪ (function-ok _ _) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁)
+<:-function-∩-∪ (function-ok s t) (function-ok₂ p₁ , p₂) = function-ok₂ (left p₁)
 <:-function-∩-∪ (function-err _) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
 
 <:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
@@ -126,17 +221,48 @@ open import Properties.Product using (_×_; _,_)
 <:-function-∩ (function-ok s t) (function-ok₂ p₁ , function-ok₂ p₂) = function-ok₂ (p₁ , p₂)
 <:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂
 
+<:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U))
+<:-function-∪ function (left function) = function
+<:-function-∪ (function-ok s t) (left (function-ok₁ p)) = function-ok₁ (left p)
+<:-function-∪ (function-ok s t) (left (function-ok₂ p)) = function-ok₂ (left p)
+<:-function-∪ (function-err s) (left (function-err p)) = function-err (left p)
+<:-function-∪ (scalar s) (left (scalar ()))
+<:-function-∪ function (right function) = function
+<:-function-∪ (function-ok s t) (right (function-ok₁ p)) = function-ok₁ (right p)
+<:-function-∪ (function-ok s t) (right (function-ok₂ p)) = function-ok₂ (right p)
+<:-function-∪ (function-err s) (right (function-err x)) = function-err (right x)
+<:-function-∪ (scalar s) (right (scalar ()))
+
 <:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U))
 <:-function-∪-∩ function function = left function
 <:-function-∪-∩ (function-ok s t) (function-ok₁ (left p)) = left (function-ok₁ p)
-<:-function-∪-∩ (function-ok s t) (function-ok₁ (right p)) = right (function-ok₁ p)
 <:-function-∪-∩ (function-ok s t) (function-ok₂ (left p)) = left (function-ok₂ p)
+<:-function-∪-∩ (function-ok s t) (function-ok₁ (right p)) = right (function-ok₁ p)
 <:-function-∪-∩ (function-ok s t) (function-ok₂ (right p)) = right (function-ok₂ p)
 <:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p)
 <:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)
 
+≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U)
+≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p)
+
+≮:-function-right : ∀ {R S T U} → (R ≮: never) → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
+≮:-function-right (witness s r _) (witness t p q) = witness (function-ok s t) (function-ok₂ p) (function-ok r q)
+
 -- Properties of scalars
-skalar = number ∪ (string ∪ (nil ∪ boolean))
+skalar-function-ok : ∀ {s t} → (¬Language skalar (function-ok s t))
+skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))
+
+scalar-<: : ∀ {S T} → (s : Scalar S) → Language T (scalar s) → (S <: T)
+scalar-<: number p (scalar number) (scalar number) = p
+scalar-<: boolean p (scalar boolean) (scalar boolean) = p
+scalar-<: string p (scalar string) (scalar string) = p
+scalar-<: nil p (scalar nil) (scalar nil) = p
+
+scalar-∩-function-<:-never : ∀ {S T U} → (Scalar S) → ((T ⇒ U) ∩ S) <: never
+scalar-∩-function-<:-never number .(scalar number) (() , scalar number)
+scalar-∩-function-<:-never boolean .(scalar boolean) (() , scalar boolean)
+scalar-∩-function-<:-never string .(scalar string) (() , scalar string)
+scalar-∩-function-<:-never nil .(scalar nil) (() , scalar nil)
 
 function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
 function-≮:-scalar s = witness function function (scalar-function s)
@@ -145,7 +271,7 @@ scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T))
 scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s)
 
 unknown-≮:-scalar : ∀ {U} → (Scalar U) → (unknown ≮: U)
-unknown-≮:-scalar s = witness (function) unknown (scalar-function s)
+unknown-≮:-scalar s = witness function unknown (scalar-function s)
 
 scalar-≮:-never : ∀ {U} → (Scalar U) → (U ≮: never)
 scalar-≮:-never s = witness (scalar s) (scalar s) never
@@ -153,8 +279,8 @@ scalar-≮:-never s = witness (scalar s) (scalar s) never
 scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U)
 scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)
 
-skalar-function-ok : ∀ {s t} → (¬Language skalar (function-ok s t))
-skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))
+scalar-≢-∩-<:-never : ∀ {T U V} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ∩ U) <: V
+scalar-≢-∩-<:-never s t p u (scalar s₁ , scalar s₂) = CONTRADICTION (p refl)
 
 skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
 skalar-scalar number = left (scalar number)
@@ -162,25 +288,6 @@ skalar-scalar boolean = right (right (right (scalar boolean)))
 skalar-scalar string = right (left (scalar string))
 skalar-scalar nil = right (right (left (scalar nil)))
 
-src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
-src-¬scalar number (scalar number) = never
-src-¬scalar boolean (scalar boolean) = never
-src-¬scalar string (scalar string) = never
-src-¬scalar nil (scalar nil) = never
-src-¬scalar s (left p) = left (src-¬scalar s p)
-src-¬scalar s (right p) = right (src-¬scalar s p)
-src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂)
-src-¬scalar s unknown = never
-
-src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
-src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p)
-
-unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
-unknown-src-≮: (witness t p _) (witness (scalar s) q (function-scalar s)) = witness t p (src-¬scalar s q)
-unknown-src-≮: (witness _ _ _) (witness function _ (scalar-function ()))
-unknown-src-≮: (witness _ _ _) (witness (function-ok _ t) _ (function-ok _ r)) = CONTRADICTION (language-comp t r unknown)
-unknown-src-≮: (witness _ _ _) (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
-
 -- Properties of unknown and never
 unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U)
 unknown-≮: (witness t p q) = witness t unknown q
@@ -196,7 +303,6 @@ function-≮:-never = witness function function never
 
 <:-never : ∀ {T} → (never <: T)
 <:-never t (scalar ())
-<:-never t (scalar-function-err ())
 
 ≮:-never-left : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: T) → (S ∩ U) ≮: never
 ≮:-never-left p (witness t q₁ q₂) with p t q₁
@@ -256,7 +362,7 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T
 
   ¬T₁u : ¬(Language T₁ u)
   ¬T₁u T₁u with p (function-ok t u) (function-ok₂ T₁u)
-  ¬T₁u T₁u | function-ok₁ ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
+  ¬T₁u T₁u | function-ok₁ ¬S₂t = language-comp t ¬S₂t S₂t
   ¬T₁u T₁u | function-ok₂ T₂u = ¬T₂u T₂u
 
 set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _) = q (t , nothing) Qt- (S₁t , λ ()) where

prototyping/Properties/TypeCheck.agda

@@ -8,15 +8,16 @@ open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import FFI.Data.Either using (Either)
 open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp)
 open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
-open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_; src; tgt)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_)
 open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
 open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import Luau.Addr using (Addr)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.OverloadedFunctions using (resolve)
 open import Properties.Contradiction using (CONTRADICTION)
 open import Properties.Dec using (yes; no)
+open import Properties.DecSubtyping using (resolve)
 open import Properties.Equality using (_≢_; sym; trans; cong)
 open import Properties.Product using (_×_; _,_)
 open import Properties.Remember using (Remember; remember; _,_)

prototyping/Properties/TypeNormalization.agda

@@ -2,10 +2,11 @@
 
 module Properties.TypeNormalization where
 
-open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
-open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∩ᶠ_; _∪ˢ_; _∩ˢ_; _⇒ᶠ_; normalize)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Luau.Subtyping using (scalar-function-err)
+open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
 open import Luau.Subtyping using (_<:_)
-open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; ∪-dist-∩-<:; <:-function; <:-function-∪-∩; <:-everything)
+open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect;  ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never)
 
 -- Notmal forms for types
 data FunType : Type → Set
@@ -15,7 +16,7 @@ data FunType where
   _⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T)
   _∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G)
 
-data Normal where 
+data Normal where
   never : Normal never
   unknown : Normal unknown
   _⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T)
@@ -28,18 +29,18 @@ data OptScalar : Type → Set where
   boolean : OptScalar boolean
   string : OptScalar string
   nil : OptScalar nil
-  
+
 -- Normalization produces normal types
 normal : ∀ T → Normal (normalize T)
 normalᶠ : ∀ {F} → FunType F → Normal F
 normal-∪ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∪ⁿ T)
 normal-∩ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∩ⁿ T)
+normal-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → Normal (S ∪ⁿˢ T)
+normal-∩ⁿˢ : ∀ {S T} → Normal S → Scalar T → OptScalar (S ∩ⁿˢ T)
 normal-∪ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∪ᶠ G)
-normal-∩ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ᶠ G)
-normal-⇒ᶠ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ᶠ T)
 
 normal nil = never ∪ nil
-normal (S ⇒ T) = normalᶠ (normal-⇒ᶠ (normal S) (normal T))
+normal (S ⇒ T) = normalᶠ ((normal S) ⇒ (normal T))
 normal never = never
 normal unknown = unknown
 normal boolean = never ∪ boolean
@@ -59,185 +60,317 @@ normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂
 normal-∪ⁿ unknown (T ⇒ U) = unknown
 normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown
 normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U))
-normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂)) 
+normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂))
 normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U))
 normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂))
 normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂
 normal-∪ⁿ (S₁ ∪ S₂) (G₁ ∩ G₂) = normal-∪ⁿ S₁ (G₁ ∩ G₂) ∪ S₂
 
--- normal-∪ⁿ never never = never
--- normal-∪ⁿ never unknown = unknown
--- normal-∪ⁿ never (scalar number) = scalar number
--- normal-∪ⁿ never (scalar boolean) = scalar boolean
--- normal-∪ⁿ never (scalar string) = scalar string
--- normal-∪ⁿ never (scalar nil) = scalar nil
--- normal-∪ⁿ never (T ⇒ U) = T ⇒ U
--- normal-∪ⁿ never (T ∩ U) = T ∩ U
--- normal-∪ⁿ never (T ∪ U) = T ∪ U
--- normal-∪ⁿ unknown never = unknown
--- normal-∪ⁿ unknown unknown = unknown
--- normal-∪ⁿ unknown (scalar number) = unknown
--- normal-∪ⁿ unknown (scalar boolean) = unknown
--- normal-∪ⁿ unknown (scalar string) = unknown
--- normal-∪ⁿ unknown (scalar nil) = unknown
--- normal-∪ⁿ unknown (T ⇒ U) = unknown
--- normal-∪ⁿ unknown (T ∩ U) = unknown
--- normal-∪ⁿ unknown (T ∪ U) = unknown
--- normal-∪ⁿ (scalar number) never = scalar number
--- normal-∪ⁿ (scalar number) unknown = unknown
--- normal-∪ⁿ (scalar number) (scalar number) = scalar number ∪ scalar number
--- normal-∪ⁿ (scalar number) (scalar boolean) = scalar number ∪ scalar boolean
--- normal-∪ⁿ (scalar number) (scalar string) = scalar number ∪ scalar string
--- normal-∪ⁿ (scalar number) (scalar nil) = scalar number ∪ scalar nil
--- normal-∪ⁿ (scalar number) (T ⇒ U) = {!!}
--- normal-∪ⁿ (scalar number) (T ∩ U) = {!!}
--- normal-∪ⁿ (scalar number) (T ∪ U) = {!!}
--- normal-∪ⁿ (scalar boolean) T = {!!}
--- normal-∪ⁿ (scalar string) T = {!!}
--- normal-∪ⁿ (scalar nil) T = {!!}
--- normal-∪ⁿ (S ⇒ S₁) T = {!!}
--- normal-∪ⁿ (x ∩ x₁) T = {!!}
--- normal-∪ⁿ (S ∪ x) T = {!!}
--- -- normal-∪ⁿ never (¬fun (S₁ ∪ S₂)) = ¬fun (S₁ ∪ S₂)
--- -- normal-∪ⁿ never (fun (S ⇒ T)) = fun (S ⇒ T)
--- -- normal-∪ⁿ never (fun (F₁ ∩ F₂)) = fun (F₁ ∩ F₂)
--- -- normal-∪ⁿ never (fun function) = fun function
--- -- normal-∪ⁿ never (both F S) = both F S
--- -- normal-∪ⁿ never unknown = unknown
--- -- normal-∪ⁿ (¬fun (scalar s)) never = ¬fun (scalar s)
--- -- normal-∪ⁿ (¬fun (scalar s)) (¬fun (scalar t)) = {!!}
--- -- normal-∪ⁿ (¬fun (scalar s)) (¬fun (T ∪ U)) = {!!}
--- -- normal-∪ⁿ (¬fun (scalar s)) (fun G) = {!!}
--- -- normal-∪ⁿ (¬fun (scalar s)) (both G T) = {!!}
--- -- normal-∪ⁿ (¬fun (scalar s)) unknown = {!!}
--- -- normal-∪ⁿ (¬fun (S ∪ S₁)) T = {!!}
--- -- normal-∪ⁿ (fun F) T = {!!}
--- -- normal-∪ⁿ (both F S) T = {!!}
--- -- normal-∪ⁿ unknown T = {!!}
--- -- normal-∪ⁿ never T = {!!}
+normal-∩ⁿ S never = never
+normal-∩ⁿ S unknown = S
+normal-∩ⁿ S (T ∪ U) = normal-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U )
+normal-∩ⁿ never (T ⇒ U) = never
+normal-∩ⁿ unknown (T ⇒ U) = T ⇒ U
+normal-∩ⁿ (R ⇒ S) (T ⇒ U) = (R ⇒ S) ∩ (T ⇒ U)
+normal-∩ⁿ (R ∩ S) (T ⇒ U) = (R ∩ S) ∩ (T ⇒ U)
+normal-∩ⁿ (R ∪ S) (T ⇒ U) = normal-∩ⁿ R (T ⇒ U)
+normal-∩ⁿ never (T ∩ U) = never
+normal-∩ⁿ unknown (T ∩ U) = T ∩ U
+normal-∩ⁿ (R ⇒ S) (T ∩ U) = (R ⇒ S) ∩ (T ∩ U)
+normal-∩ⁿ (R ∩ S) (T ∩ U) = (R ∩ S) ∩ (T ∩ U)
+normal-∩ⁿ (R ∪ S) (T ∩ U) = normal-∩ⁿ R (T ∩ U)
 
--- normal-∩ⁿ S T = {!!}
+normal-∪ⁿˢ S never = S
+normal-∪ⁿˢ never number = never ∪ number
+normal-∪ⁿˢ unknown number = unknown
+normal-∪ⁿˢ (R ⇒ S) number = (R ⇒ S) ∪ number
+normal-∪ⁿˢ (R ∩ S) number = (R ∩ S) ∪ number
+normal-∪ⁿˢ (R ∪ number) number = R ∪ number
+normal-∪ⁿˢ (R ∪ boolean) number = normal-∪ⁿˢ R number ∪ boolean
+normal-∪ⁿˢ (R ∪ string) number = normal-∪ⁿˢ R number ∪ string
+normal-∪ⁿˢ (R ∪ nil) number = normal-∪ⁿˢ R number ∪ nil
+normal-∪ⁿˢ never boolean = never ∪ boolean
+normal-∪ⁿˢ unknown boolean = unknown
+normal-∪ⁿˢ (R ⇒ S) boolean = (R ⇒ S) ∪ boolean
+normal-∪ⁿˢ (R ∩ S) boolean = (R ∩ S) ∪ boolean
+normal-∪ⁿˢ (R ∪ number) boolean = normal-∪ⁿˢ R boolean ∪ number
+normal-∪ⁿˢ (R ∪ boolean) boolean = R ∪ boolean
+normal-∪ⁿˢ (R ∪ string) boolean = normal-∪ⁿˢ R boolean ∪ string
+normal-∪ⁿˢ (R ∪ nil) boolean = normal-∪ⁿˢ R boolean ∪ nil
+normal-∪ⁿˢ never string = never ∪ string
+normal-∪ⁿˢ unknown string = unknown
+normal-∪ⁿˢ (R ⇒ S) string = (R ⇒ S) ∪ string
+normal-∪ⁿˢ (R ∩ S) string = (R ∩ S) ∪ string
+normal-∪ⁿˢ (R ∪ number) string = normal-∪ⁿˢ R string ∪ number
+normal-∪ⁿˢ (R ∪ boolean) string = normal-∪ⁿˢ R string ∪ boolean
+normal-∪ⁿˢ (R ∪ string) string = R ∪ string
+normal-∪ⁿˢ (R ∪ nil) string = normal-∪ⁿˢ R string ∪ nil
+normal-∪ⁿˢ never nil = never ∪ nil
+normal-∪ⁿˢ unknown nil = unknown
+normal-∪ⁿˢ (R ⇒ S) nil = (R ⇒ S) ∪ nil
+normal-∪ⁿˢ (R ∩ S) nil = (R ∩ S) ∪ nil
+normal-∪ⁿˢ (R ∪ number) nil = normal-∪ⁿˢ R nil ∪ number
+normal-∪ⁿˢ (R ∪ boolean) nil = normal-∪ⁿˢ R nil ∪ boolean
+normal-∪ⁿˢ (R ∪ string) nil = normal-∪ⁿˢ R nil ∪ string
+normal-∪ⁿˢ (R ∪ nil) nil = R ∪ nil
 
--- -- normal-∪ⁿ S never = S
--- -- normal-∪ⁿ (F ∪ S) unknown = unknown
--- -- normal-∪ⁿ never unknown = unknown
--- -- normal-∪ⁿ unknown unknown = unknown
--- -- normal-∪ⁿ never (G ∪ T) = G ∪ T
--- -- normal-∪ⁿ unknown (G ∪ T) = unknown
--- -- normal-∪ⁿ (F ∪ S) (G ∪ T) = (normal-∪ᶠ F G) ∪ (normal-∪ˢ S T)
+normal-∩ⁿˢ never number = never
+normal-∩ⁿˢ never boolean = never
+normal-∩ⁿˢ never string = never
+normal-∩ⁿˢ never nil = never
+normal-∩ⁿˢ unknown number = number
+normal-∩ⁿˢ unknown boolean = boolean
+normal-∩ⁿˢ unknown string = string
+normal-∩ⁿˢ unknown nil = nil
+normal-∩ⁿˢ (R ⇒ S) number = never
+normal-∩ⁿˢ (R ⇒ S) boolean = never
+normal-∩ⁿˢ (R ⇒ S) string = never
+normal-∩ⁿˢ (R ⇒ S) nil = never
+normal-∩ⁿˢ (R ∩ S) number = never
+normal-∩ⁿˢ (R ∩ S) boolean = never
+normal-∩ⁿˢ (R ∩ S) string = never
+normal-∩ⁿˢ (R ∩ S) nil = never
+normal-∩ⁿˢ (R ∪ number) number = number
+normal-∩ⁿˢ (R ∪ boolean) number = normal-∩ⁿˢ R number
+normal-∩ⁿˢ (R ∪ string) number = normal-∩ⁿˢ R number
+normal-∩ⁿˢ (R ∪ nil) number = normal-∩ⁿˢ R number
+normal-∩ⁿˢ (R ∪ number) boolean = normal-∩ⁿˢ R boolean
+normal-∩ⁿˢ (R ∪ boolean) boolean = boolean
+normal-∩ⁿˢ (R ∪ string) boolean = normal-∩ⁿˢ R boolean
+normal-∩ⁿˢ (R ∪ nil) boolean = normal-∩ⁿˢ R boolean
+normal-∩ⁿˢ (R ∪ number) string = normal-∩ⁿˢ R string
+normal-∩ⁿˢ (R ∪ boolean) string = normal-∩ⁿˢ R string
+normal-∩ⁿˢ (R ∪ string) string = string
+normal-∩ⁿˢ (R ∪ nil) string = normal-∩ⁿˢ R string
+normal-∩ⁿˢ (R ∪ number) nil = normal-∩ⁿˢ R nil
+normal-∩ⁿˢ (R ∪ boolean) nil = normal-∩ⁿˢ R nil
+normal-∩ⁿˢ (R ∪ string) nil = normal-∩ⁿˢ R nil
+normal-∩ⁿˢ (R ∪ nil) nil = nil
 
--- -- normal-∩ⁿ S never = never
--- -- normal-∩ⁿ (F ∪ S) unknown = F ∪ S
--- -- normal-∩ⁿ never unknown = never
--- -- normal-∩ⁿ unknown unknown = unknown
--- -- normal-∩ⁿ never (G ∪ T) = never
--- -- normal-∩ⁿ unknown (G ∪ T) = G ∪ T
--- -- normal-∩ⁿ (F ∪ S) (G ∪ T) = (normal-∩ᶠ F G) ∪ (normal-∩ˢ S T)
+normal-∪ᶠ (R ⇒ S) (T ⇒ U) = (normal-∩ⁿ R T) ⇒ (normal-∪ⁿ S U)
+normal-∪ᶠ (R ⇒ S) (G ∩ H) = normal-∪ᶠ (R ⇒ S) G ∩ normal-∪ᶠ (R ⇒ S) H
+normal-∪ᶠ (E ∩ F) G = normal-∪ᶠ E G ∩ normal-∪ᶠ F G
 
--- normal-∪ᶠ (R ⇒ S) (T ⇒ U) = normal-⇒ᶠ (normal-∩ⁿ R T) (normal-∪ⁿ S U)
--- normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂) = normal-∩ᶠ (normal-∪ᶠ (R ⇒ S) G₁) (normal-∪ᶠ (R ⇒ S) G₂)
--- normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U) = normal-∩ᶠ (normal-∪ᶠ F₁ (T ⇒ U)) (normal-∪ᶠ F₂ (T ⇒ U))
--- normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂) = normal-∩ᶠ (normal-∪ᶠ F₁ (G₁ ∩ G₂)) (normal-∪ᶠ F₂ (G₁ ∩ G₂))
+scalar-∩-fun-<:-never : ∀ {F S} → FunType F → Scalar S → (F ∩ S) <: never
+scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S
+scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S)
 
--- normal-∩ᶠ (F₁ ∩ F₂) (T ⇒ U) = (F₁ ∩ F₂) ∩ (T ⇒ U)
--- normal-∩ᶠ (F₁ ∩ F₂) (G ∩ G₁) = (F₁ ∩ F₂) ∩ (G ∩ G₁)
--- normal-∩ᶠ (R ⇒ S) (G₁ ∩ G₂) = (R ⇒ S) ∩ (G₁ ∩ G₂)
--- normal-∩ᶠ (R ⇒ S) (T ⇒ U) = (R ⇒ S) ∩ (T ⇒ U)
+flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T)
+flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl)
 
--- normal-∪ˢ F G = {!!}
+∩-<:-∩ⁿ :  ∀ {S T} → Normal S → Normal T → (S ∩ T) <: (S ∩ⁿ T)
+∩ⁿ-<:-∩ :  ∀ {S T} → Normal S → Normal T → (S ∩ⁿ T) <: (S ∩ T)
+∩-<:-∩ⁿˢ :  ∀ {S T} → Normal S → Scalar T → (S ∩ T) <: (S ∩ⁿˢ T)
+∩ⁿˢ-<:-∩ :  ∀ {S T} → Normal S → Scalar T → (S ∩ⁿˢ T) <: (S ∩ T)
+∪ᶠ-<:-∪ : ∀ {F G} → FunType F → FunType G → (F ∪ᶠ G) <: (F ∪ G)
+∪ⁿ-<:-∪ : ∀ {S T} → Normal S → Normal T → (S ∪ⁿ T) <: (S ∪ T)
+∪-<:-∪ⁿ : ∀ {S T} → Normal S → Normal T → (S ∪ T) <: (S ∪ⁿ T)
+∪ⁿˢ-<:-∪ : ∀ {S T} → Normal S → OptScalar T → (S ∪ⁿˢ T) <: (S ∪ T)
+∪-<:-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → (S ∪ T) <: (S ∪ⁿˢ T)
 
--- normal-∩ˢ F G = {!!}
+∩-<:-∩ⁿ S never = <:-∩-right
+∩-<:-∩ⁿ S unknown = <:-∩-left
+∩-<:-∩ⁿ S (T ∪ U) = <:-trans <:-∩-distl-∪ (<:-trans (<:-union (∩-<:-∩ⁿ S T) (∩-<:-∩ⁿˢ S U)) (∪-<:-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) )
+∩-<:-∩ⁿ never (T ⇒ U) = <:-∩-left
+∩-<:-∩ⁿ unknown (T ⇒ U) = <:-∩-right
+∩-<:-∩ⁿ (R ⇒ S) (T ⇒ U) = <:-refl
+∩-<:-∩ⁿ (R ∩ S) (T ⇒ U) = <:-refl
+∩-<:-∩ⁿ (R ∪ S) (T ⇒ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ⇒ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ⇒ U) S))) (<:-∪-lub <:-refl <:-never))
+∩-<:-∩ⁿ never (T ∩ U) = <:-∩-left
+∩-<:-∩ⁿ unknown (T ∩ U) = <:-∩-right
+∩-<:-∩ⁿ (R ⇒ S) (T ∩ U) = <:-refl
+∩-<:-∩ⁿ (R ∩ S) (T ∩ U) = <:-refl
+∩-<:-∩ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ∩ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ∩ U) S))) (<:-∪-lub <:-refl <:-never))
 
--- normal-⇒ᶠ S T = {!!}
+∩ⁿ-<:-∩ S never = <:-never
+∩ⁿ-<:-∩ S unknown = <:-∩-glb <:-refl <:-unknown
+∩ⁿ-<:-∩ S (T ∪ U) = <:-trans (∪ⁿˢ-<:-∪ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) (<:-trans (<:-union (∩ⁿ-<:-∩ S T) (∩ⁿˢ-<:-∩ S U)) ∩-distl-∪-<:)
+∩ⁿ-<:-∩ never (T ⇒ U) = <:-never
+∩ⁿ-<:-∩ unknown (T ⇒ U) = <:-∩-glb <:-unknown <:-refl
+∩ⁿ-<:-∩ (R ⇒ S) (T ⇒ U) = <:-refl
+∩ⁿ-<:-∩ (R ∩ S) (T ⇒ U) = <:-refl
+∩ⁿ-<:-∩ (R ∪ S) (T ⇒ U) = <:-trans (∩ⁿ-<:-∩ R (T ⇒ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
+∩ⁿ-<:-∩ never (T ∩ U) = <:-never
+∩ⁿ-<:-∩ unknown (T ∩ U) = <:-∩-glb <:-unknown <:-refl
+∩ⁿ-<:-∩ (R ⇒ S) (T ∩ U) = <:-refl
+∩ⁿ-<:-∩ (R ∩ S) (T ∩ U) = <:-refl
+∩ⁿ-<:-∩ (R ∪ S) (T ∩ U) = <:-trans (∩ⁿ-<:-∩ R (T ∩ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
 
--- record _<:forget_ {P : Type → Set} (S : Type) (T : ∃ P) : Set where
---   constructor ⟨_⟩
---   field sub : (S <: forget T)
--- open _<:forget_ public
+∩-<:-∩ⁿˢ never number = <:-∩-left
+∩-<:-∩ⁿˢ never boolean = <:-∩-left
+∩-<:-∩ⁿˢ never string = <:-∩-left
+∩-<:-∩ⁿˢ never nil = <:-∩-left
+∩-<:-∩ⁿˢ unknown T = <:-∩-right
+∩-<:-∩ⁿˢ (R ⇒ S) T = scalar-∩-fun-<:-never (R ⇒ S) T
+∩-<:-∩ⁿˢ (F ∩ G) T = scalar-∩-fun-<:-never (F ∩ G) T
+∩-<:-∩ⁿˢ (R ∪ number) number = <:-∩-right
+∩-<:-∩ⁿˢ (R ∪ boolean) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never boolean number (λ ())))
+∩-<:-∩ⁿˢ (R ∪ string) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never string number (λ ())))
+∩-<:-∩ⁿˢ (R ∪ nil) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never nil number (λ ())))
+∩-<:-∩ⁿˢ (R ∪ number) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never number boolean (λ ())))
+∩-<:-∩ⁿˢ (R ∪ boolean) boolean = <:-∩-right
+∩-<:-∩ⁿˢ (R ∪ string) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never string boolean (λ ())))
+∩-<:-∩ⁿˢ (R ∪ nil) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never nil boolean (λ ())))
+∩-<:-∩ⁿˢ (R ∪ number) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never number string (λ ())))
+∩-<:-∩ⁿˢ (R ∪ boolean) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never boolean string (λ ())))
+∩-<:-∩ⁿˢ (R ∪ string) string = <:-∩-right
+∩-<:-∩ⁿˢ (R ∪ nil) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never nil string (λ ())))
+∩-<:-∩ⁿˢ (R ∪ number) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never number nil (λ ())))
+∩-<:-∩ⁿˢ (R ∪ boolean) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never boolean nil (λ ())))
+∩-<:-∩ⁿˢ (R ∪ string) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never string nil (λ ())))
+∩-<:-∩ⁿˢ (R ∪ nil) nil = <:-∩-right
 
--- record _:>forget_ {P : Type → Set} (S : Type) (T : ∃ P) : Set where
---   constructor ⟨_⟩
---   field sup : (forget T <: S)
--- open _:>forget_ public
+∩ⁿˢ-<:-∩ never T = <:-never
+∩ⁿˢ-<:-∩ unknown T = <:-∩-glb <:-unknown <:-refl
+∩ⁿˢ-<:-∩ (R ⇒ S) T = <:-never
+∩ⁿˢ-<:-∩ (F ∩ G) T = <:-never
+∩ⁿˢ-<:-∩ (R ∪ number) number = <:-∩-glb <:-∪-right <:-refl
+∩ⁿˢ-<:-∩ (R ∪ boolean) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ string) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ nil) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ number) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ boolean) boolean = <:-∩-glb <:-∪-right <:-refl
+∩ⁿˢ-<:-∩ (R ∪ string) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ nil) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ number) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ boolean) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ string) string = <:-∩-glb <:-∪-right <:-refl
+∩ⁿˢ-<:-∩ (R ∪ nil) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ number) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ boolean) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ string) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ nil) nil = <:-∩-glb <:-∪-right <:-refl
 
--- forget-∩ⁿ-<: : ∀ {S T} → (forget S ∩ forget T) <:forget (S ∩ⁿ T)
--- forget-∩ⁿ-<: = {!!}
+∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) = <:-trans (<:-function (∩-<:-∩ⁿ R T) (∪ⁿ-<:-∪ S U)) <:-function-∪-∩
+∪ᶠ-<:-∪ (R ⇒ S) (G ∩ H) = <:-trans (<:-intersect (∪ᶠ-<:-∪ (R ⇒ S) G) (∪ᶠ-<:-∪ (R ⇒ S) H)) ∪-distl-∩-<:
+∪ᶠ-<:-∪ (E ∩ F) G = <:-trans (<:-intersect (∪ᶠ-<:-∪ E G) (∪ᶠ-<:-∪ F G)) ∪-distr-∩-<:
 
--- <:-forget-∪ⁿ : ∀ {S T} → (forget S ∪ forget T) :>forget (S ∪ⁿ T) 
--- <:-forget-∪ⁿ = {!!}
+∪-<:-∪ᶠ : ∀ {F G} → FunType F → FunType G → (F ∪ G) <: (F ∪ᶠ G)
+∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ R T) (∪-<:-∪ⁿ S U))
+∪-<:-∪ᶠ (R ⇒ S) (G ∩ H) = <:-trans <:-∪-distl-∩ (<:-intersect (∪-<:-∪ᶠ (R ⇒ S) G) (∪-<:-∪ᶠ (R ⇒ S) H))
+∪-<:-∪ᶠ (E ∩ F) G = <:-trans <:-∪-distr-∩ (<:-intersect (∪-<:-∪ᶠ E G) (∪-<:-∪ᶠ F G))
 
--- <:-forget-⇒ⁿ : ∀ {S T} →  (forget S ⇒ forget T) :>forget (S ⇒ⁿ T)
--- <:-forget-⇒ⁿ = {!!}
+∪ⁿˢ-<:-∪ S never = <:-∪-left
+∪ⁿˢ-<:-∪ never number = <:-refl
+∪ⁿˢ-<:-∪ never boolean = <:-refl
+∪ⁿˢ-<:-∪ never string = <:-refl
+∪ⁿˢ-<:-∪ never nil = <:-refl
+∪ⁿˢ-<:-∪ unknown number = <:-∪-left
+∪ⁿˢ-<:-∪ unknown boolean = <:-∪-left
+∪ⁿˢ-<:-∪ unknown string = <:-∪-left
+∪ⁿˢ-<:-∪ unknown nil = <:-∪-left
+∪ⁿˢ-<:-∪ (R ⇒ S) number = <:-refl
+∪ⁿˢ-<:-∪ (R ⇒ S) boolean = <:-refl
+∪ⁿˢ-<:-∪ (R ⇒ S) string = <:-refl
+∪ⁿˢ-<:-∪ (R ⇒ S) nil = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) number = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) boolean = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) string = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) nil = <:-refl
+∪ⁿˢ-<:-∪ (R ∪ number) number = <:-union <:-∪-left <:-refl
+∪ⁿˢ-<:-∪ (R ∪ boolean) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ string) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ nil) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ number) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ boolean) boolean = <:-union <:-∪-left <:-refl
+∪ⁿˢ-<:-∪ (R ∪ string) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ nil) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ number) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ boolean) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ string) string = <:-union <:-∪-left <:-refl
+∪ⁿˢ-<:-∪ (R ∪ nil) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ number) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ boolean) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ string) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ nil) nil = <:-union <:-∪-left <:-refl
 
--- <:-forget-∩ᶠ : ∀ {F G} → (forget F ∩ forget G) :>forget (F ∩ᶠ G)
--- <:-forget-∩ᶠ = {!!}
+∪-<:-∪ⁿˢ T never = <:-∪-lub <:-refl <:-never
+∪-<:-∪ⁿˢ never number = <:-refl
+∪-<:-∪ⁿˢ never boolean = <:-refl
+∪-<:-∪ⁿˢ never string = <:-refl
+∪-<:-∪ⁿˢ never nil = <:-refl
+∪-<:-∪ⁿˢ unknown number = <:-unknown
+∪-<:-∪ⁿˢ unknown boolean = <:-unknown
+∪-<:-∪ⁿˢ unknown string = <:-unknown
+∪-<:-∪ⁿˢ unknown nil = <:-unknown
+∪-<:-∪ⁿˢ (R ⇒ S) number = <:-refl
+∪-<:-∪ⁿˢ (R ⇒ S) boolean = <:-refl
+∪-<:-∪ⁿˢ (R ⇒ S) string = <:-refl
+∪-<:-∪ⁿˢ (R ⇒ S) nil = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) number = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) boolean = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) string = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) nil = <:-refl
+∪-<:-∪ⁿˢ (R ∪ number) number = <:-∪-lub <:-refl <:-∪-right
+∪-<:-∪ⁿˢ (R ∪ boolean) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ string) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ nil) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ number) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ boolean) boolean = <:-∪-lub <:-refl <:-∪-right
+∪-<:-∪ⁿˢ (R ∪ string) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ nil) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ number) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ boolean) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ string) string = <:-∪-lub <:-refl <:-∪-right
+∪-<:-∪ⁿˢ (R ∪ nil) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ number) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ boolean) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ string) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ nil) nil = <:-∪-lub <:-refl <:-∪-right
 
--- <:-forget-∪ᶠ : ∀ {F G} → (forget F ∪ forget G) :>forget (F ∪ᶠ G) 
--- <:-forget-∪ᶠ {⟨ R ⇒ S ⟩} {⟨ T ⇒ U ⟩} = ⟨ <:-trans (sup <:-forget-⇒ⁿ) {!!} ⟩ -- <:-trans (<:-forget-⇒ⁿ {⟨ R ⟩ ∩ⁿ ⟨ T ⟩} {⟨ S ⟩ ∪ⁿ ⟨ U ⟩}) (<:-trans (<:-function (forget-∩ⁿ-<: { ⟨ R ⟩ }) (<:-forget-∪ⁿ {⟨ S ⟩})) <:-function-∪-∩)
--- <:-forget-∪ᶠ {⟨ R ⇒ S ⟩} {⟨ G₁ ∩ G₂ ⟩} = {!!} -- <:-trans (<:-trans (<:-forget-∩ᶠ {⟨ R ⇒ S ⟩ ∪ᶠ ⟨ G₁ ⟩}) {!!}) ∪-dist-∩-<:
--- <:-forget-∪ᶠ {⟨ R ⇒ S ⟩} {⟨ never ⟩} = {!!}
--- <:-forget-∪ᶠ {⟨ R ⇒ S ⟩} {⟨ function ⟩} = {!!}
--- <:-forget-∪ᶠ {⟨ F₁ ∩ F₂ ⟩} {⟨ G ⟩} = {!!}
--- <:-forget-∪ᶠ {⟨ never ⟩} {⟨ G ⟩} = ⟨ <:-∪-right ⟩
--- <:-forget-∪ᶠ {⟨ function ⟩} {⟨ G ⟩} = {!!}
+∪ⁿ-<:-∪ S never = <:-∪-left
+∪ⁿ-<:-∪ S unknown = <:-∪-right
+∪ⁿ-<:-∪ never (T ⇒ U) = <:-∪-right
+∪ⁿ-<:-∪ unknown (T ⇒ U) = <:-∪-left
+∪ⁿ-<:-∪ (R ⇒ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U)
+∪ⁿ-<:-∪ (R ∩ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ⇒ U)
+∪ⁿ-<:-∪ (R ∪ S) (T ⇒ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ⇒ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
+∪ⁿ-<:-∪ never (T ∩ U) = <:-∪-right
+∪ⁿ-<:-∪ unknown (T ∩ U) = <:-∪-left
+∪ⁿ-<:-∪ (R ⇒ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ∩ U)
+∪ⁿ-<:-∪ (R ∩ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ∩ U)
+∪ⁿ-<:-∪ (R ∪ S) (T ∩ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ∩ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
+∪ⁿ-<:-∪ S (T ∪ U) = <:-∪-lub (<:-trans (∪ⁿ-<:-∪ S T) (<:-union <:-refl <:-∪-left)) (<:-trans <:-∪-right <:-∪-right)
 
--- forget-∪ᶠ-<: : ∀ {F G} → (forget F ∪ forget G) <: forget (F ∪ᶠ G)
--- forget-∪ᶠ-<: = {!!}
+∪-<:-∪ⁿ S never = <:-∪-lub <:-refl <:-never
+∪-<:-∪ⁿ S unknown = <:-unknown
+∪-<:-∪ⁿ never (T ⇒ U) = <:-∪-lub <:-never <:-refl
+∪-<:-∪ⁿ unknown (T ⇒ U) = <:-unknown
+∪-<:-∪ⁿ (R ⇒ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U)
+∪-<:-∪ⁿ (R ∩ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ∩ S) (T ⇒ U)
+∪-<:-∪ⁿ (R ∪ S) (T ⇒ U) =  <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ⇒ U)) <:-refl)))
+∪-<:-∪ⁿ never (T ∩ U) = <:-∪-lub <:-never <:-refl
+∪-<:-∪ⁿ unknown (T ∩ U) = <:-unknown
+∪-<:-∪ⁿ (R ⇒ S) (T ∩ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ∩ U)
+∪-<:-∪ⁿ (R ∩ S) (T ∩ U) = ∪-<:-∪ᶠ (R ∩ S) (T ∩ U)
+∪-<:-∪ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ∩ U)) <:-refl)))
+∪-<:-∪ⁿ never (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ never T) <:-refl)
+∪-<:-∪ⁿ unknown (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ unknown T) <:-refl)
+∪-<:-∪ⁿ (R ⇒ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ⇒ S) T) <:-refl)
+∪-<:-∪ⁿ (R ∩ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∩ S) T) <:-refl)
+∪-<:-∪ⁿ (R ∪ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∪ S) T) <:-refl)
 
--- <:-∪ᶠ-left : ∀ {F G} → forget F <: forget (F ∪ᶠ G)
--- <:-∪ᶠ-left {F} = <:-trans (<:-∪-left {forget F}) (forget-∪ᶠ-<: {F})
+normalize-<: : ∀ T → normalize T <: T
+<:-normalize : ∀ T → T <: normalize T
 
--- -- <:-∪ᶠ-left {⟨ R ⇒ S ⟩} {⟨ T ⇒ U ⟩} = {!<:-∪-lub!}
--- -- <:-∪ᶠ-left {⟨ R ⇒ S ⟩} {⟨ G₁ ∩ G₂ ⟩} = {!<:-∩-glb!}
--- -- <:-∪ᶠ-left {⟨ R ⇒ S ⟩} {⟨ never ⟩} = <:-refl
--- -- <:-∪ᶠ-left {⟨ R ⇒ S ⟩} {⟨ function ⟩} = <:-function <:-never <:-unknown
--- -- <:-∪ᶠ-left {⟨ F₁ ∩ F₂ ⟩} {⟨ T ⇒ U ⟩} = {!!}
--- -- <:-∪ᶠ-left {⟨ F₁ ∩ F₂ ⟩} {⟨ G ∩ G₁ ⟩} = {!!}
--- -- <:-∪ᶠ-left {⟨ F₁ ∩ F₂ ⟩} {⟨ never ⟩} = <:-refl
--- -- <:-∪ᶠ-left {⟨ F₁ ∩ F₂ ⟩} {⟨ function ⟩} = {!<:-function <:-never <:-unknown!}
--- -- <:-∪ᶠ-left {⟨ never ⟩} {⟨ G ⟩} = <:-never
--- -- <:-∪ᶠ-left {⟨ function ⟩} {⟨ T ⇒ U ⟩} = <:-refl
--- -- <:-∪ᶠ-left {⟨ function ⟩} {⟨ G₁ ∩ G₂ ⟩} = <:-refl
--- -- <:-∪ᶠ-left {⟨ function ⟩} {⟨ never ⟩} = <:-refl
--- -- <:-∪ᶠ-left {⟨ function ⟩} {⟨ function ⟩} = <:-refl
+<:-normalize nil = <:-∪-right
+<:-normalize (S ⇒ T) = <:-function (normalize-<: S) (<:-normalize T)
+<:-normalize never = <:-refl
+<:-normalize unknown = <:-refl
+<:-normalize boolean = <:-∪-right
+<:-normalize number = <:-∪-right
+<:-normalize string = <:-∪-right
+<:-normalize (S ∪ T) = <:-trans (<:-union (<:-normalize S) (<:-normalize T)) (∪-<:-∪ⁿ (normal S) (normal T))
+<:-normalize (S ∩ T) = <:-trans (<:-intersect (<:-normalize S) (<:-normalize T)) (∩-<:-∩ⁿ (normal S) (normal T))
 
--- <:-∪ⁿ-left : ∀ {S T} → forget S <: forget (S ∪ⁿ T)
--- <:-∪ⁿ-left {⟨ F ∪ S ⟩} {⟨ G ∪ T ⟩} = <:-∪-lub {!!} {!!}
+normalize-<: nil = <:-∪-lub <:-never <:-refl
+normalize-<: (S ⇒ T) = <:-function (<:-normalize S) (normalize-<: T)
+normalize-<: never = <:-refl
+normalize-<: unknown = <:-refl
+normalize-<: boolean = <:-∪-lub <:-never <:-refl
+normalize-<: number = <:-∪-lub <:-never <:-refl
+normalize-<: string = <:-∪-lub <:-never <:-refl
+normalize-<: (S ∪ T) = <:-trans (∪ⁿ-<:-∪ (normal S) (normal T)) (<:-union (normalize-<: S) (normalize-<: T))
+normalize-<: (S ∩ T) = <:-trans (∩ⁿ-<:-∩ (normal S) (normal T)) (<:-intersect (normalize-<: S) (normalize-<: T))
 
--- <:-∪ⁿ-right : ∀ {S T} → forget T <: forget (S ∪ⁿ T)
--- <:-∪ⁿ-right = {!!}
 
--- <:-∪ⁿ-lub : ∀ {S T U} → forget S <: U → forget T <: U → forget (S ∪ⁿ T) <: U
--- <:-∪ⁿ-lub = {!!}
-
--- <:-∩ⁿ-left : ∀ {S T} → forget (S ∩ⁿ T) <: forget S
--- <:-∩ⁿ-left = {!!}
-
--- <:-∩ⁿ-right : ∀ {S T} → forget (S ∩ⁿ T) <: forget T
--- <:-∩ⁿ-right = {!!}
-
--- <:-∩ⁿ-glb : ∀ {S T U} → S <: forget T → S <: forget U → S <: forget (T ∩ⁿ U)
--- <:-∩ⁿ-glb = {!!}
-
--- normalize-<: : ∀ T → forget (normalize T) <: T
--- <:-normalize : ∀ T → T <: forget (normalize T)
-
--- <:-normalize nil = <:-∪-right
--- <:-normalize (S ⇒ T) = <:-trans (<:-function (normalize-<: S) (<:-normalize T)) <:-∪-left
--- <:-normalize never = <:-never
--- <:-normalize unknown = <:-everything
--- <:-normalize boolean = <:-∪-right
--- <:-normalize number = <:-∪-right
--- <:-normalize string = <:-∪-right
--- <:-normalize (S ∪ T) = <:-∪-lub (<:-trans (<:-normalize S) (<:-∪ⁿ-left {normalize S})) (<:-trans (<:-normalize T) (<:-∪ⁿ-right {normalize S}))
--- <:-normalize (S ∩ T) = <:-∩ⁿ-glb {S ∩ T} {normalize S} (<:-trans <:-∩-left (<:-normalize S)) (<:-trans <:-∩-right (<:-normalize T))
-
--- normalize-<: nil = <:-∪-lub <:-never <:-refl
--- normalize-<: (S ⇒ T) = <:-∪-lub (<:-function (<:-normalize S) (normalize-<: T)) <:-never
--- normalize-<: never = <:-∪-lub <:-never <:-refl
--- normalize-<: unknown = <:-unknown
--- normalize-<: boolean = <:-∪-lub <:-never <:-refl
--- normalize-<: number = <:-∪-lub <:-never <:-refl
--- normalize-<: string = <:-∪-lub <:-never <:-refl
--- normalize-<: (S ∪ T) = <:-∪ⁿ-lub {normalize S} (<:-trans (normalize-<: S) <:-∪-left) (<:-trans (normalize-<: T) <:-∪-right)
--- normalize-<: (S ∩ T) = <:-∩-glb (<:-trans (<:-∩ⁿ-left {normalize S}) (normalize-<: S)) (<:-trans (<:-∩ⁿ-right {normalize S}) (normalize-<: T))

tests/Autocomplete.test.cpp

@@ -3034,4 +3034,40 @@ string:@1
     CHECK(ac.entryMap["sub"].wrongIndexType == true);
 }
 
+TEST_CASE_FIXTURE(ACFixture, "source_module_preservation_and_invalidation")
+{
+    check(R"(
+local a = { x = 2, y = 4 }
+a.@1
+    )");
+
+    frontend.clear();
+
+    auto ac = autocomplete('1');
+
+    CHECK(ac.entryMap.count("x"));
+    CHECK(ac.entryMap.count("y"));
+
+    frontend.check("MainModule", {});
+
+    ac = autocomplete('1');
+
+    CHECK(ac.entryMap.count("x"));
+    CHECK(ac.entryMap.count("y"));
+
+    frontend.markDirty("MainModule", nullptr);
+
+    ac = autocomplete('1');
+
+    CHECK(ac.entryMap.count("x"));
+    CHECK(ac.entryMap.count("y"));
+
+    frontend.check("MainModule", {});
+
+    ac = autocomplete('1');
+
+    CHECK(ac.entryMap.count("x"));
+    CHECK(ac.entryMap.count("y"));
+}
+
 TEST_SUITE_END();

tests/Compiler.test.cpp

@@ -17,11 +17,13 @@ std::string rep(const std::string& s, size_t n);
 
 using namespace Luau;
 
-static std::string compileFunction(const char* source, uint32_t id)
+static std::string compileFunction(const char* source, uint32_t id, int optimizationLevel = 1)
 {
     Luau::BytecodeBuilder bcb;
     bcb.setDumpFlags(Luau::BytecodeBuilder::Dump_Code);
-    Luau::compileOrThrow(bcb, source);
+    Luau::CompileOptions options;
+    options.optimizationLevel = optimizationLevel;
+    Luau::compileOrThrow(bcb, source, options);
 
     return bcb.dumpFunction(id);
 }
@@ -2689,6 +2691,27 @@ local 8: reg 3, start pc 34 line 21, end pc 34 line 21
 )");
 }
 
+TEST_CASE("DebugRemarks")
+{
+    Luau::BytecodeBuilder bcb;
+    bcb.setDumpFlags(Luau::BytecodeBuilder::Dump_Code | Luau::BytecodeBuilder::Dump_Remarks);
+
+    uint32_t fid = bcb.beginFunction(0);
+
+    bcb.addDebugRemark("test remark #%d", 42);
+    bcb.emitABC(LOP_RETURN, 0, 1, 0);
+
+    bcb.endFunction(0, 0);
+
+    bcb.setMainFunction(fid);
+    bcb.finalize();
+
+    CHECK_EQ("\n" + bcb.dumpFunction(0), R"(
+REMARK test remark #42
+RETURN R0 0
+)");
+}
+
 TEST_CASE("AssignmentConflict")
 {
     // assignments are left to right
@@ -4076,4 +4099,336 @@ RETURN R1 6
 )");
 }
 
+TEST_CASE("LoopUnrollBasic")
+{
+    // forward loops
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=1,2 do
+    t[i] = i
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 2
+LOADN R1 1
+SETTABLEN R1 R0 1
+LOADN R1 2
+SETTABLEN R1 R0 2
+RETURN R0 1
+)");
+
+    // backward loops
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=2,1,-1 do
+    t[i] = i
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 0
+LOADN R1 2
+SETTABLEN R1 R0 2
+LOADN R1 1
+SETTABLEN R1 R0 1
+RETURN R0 1
+)");
+
+    // loops with step that doesn't divide to-from
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=1,4,2 do
+    t[i] = i
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 0
+LOADN R1 1
+SETTABLEN R1 R0 1
+LOADN R1 3
+SETTABLEN R1 R0 3
+RETURN R0 1
+)");
+}
+
+TEST_CASE("LoopUnrollUnsupported")
+{
+    // can't unroll loops with non-constant bounds
+    CHECK_EQ("\n" + compileFunction(R"(
+for i=x,y,z do
+end
+)",
+                        0, 2),
+        R"(
+GETIMPORT R2 1
+GETIMPORT R0 3
+GETIMPORT R1 5
+FORNPREP R0 +1
+FORNLOOP R0 -1
+RETURN R0 0
+)");
+
+    // can't unroll loops with bounds where we can't compute trip count
+    CHECK_EQ("\n" + compileFunction(R"(
+for i=2,1 do
+end
+)",
+                        0, 2),
+        R"(
+LOADN R2 2
+LOADN R0 1
+LOADN R1 1
+FORNPREP R0 +1
+FORNLOOP R0 -1
+RETURN R0 0
+)");
+
+    // can't unroll loops with bounds that might be imprecise (non-integer)
+    CHECK_EQ("\n" + compileFunction(R"(
+for i=1,2,0.1 do
+end
+)",
+                        0, 2),
+        R"(
+LOADN R2 1
+LOADN R0 2
+LOADK R1 K0
+FORNPREP R0 +1
+FORNLOOP R0 -1
+RETURN R0 0
+)");
+
+    // can't unroll loops if the bounds are too large, as it might overflow trip count math
+    CHECK_EQ("\n" + compileFunction(R"(
+for i=4294967295,4294967296 do
+end
+)",
+                        0, 2),
+        R"(
+LOADK R2 K0
+LOADK R0 K1
+LOADN R1 1
+FORNPREP R0 +1
+FORNLOOP R0 -1
+RETURN R0 0
+)");
+
+    // can't unroll loops if the body has loop control flow or nested loops
+    CHECK_EQ("\n" + compileFunction(R"(
+for i=1,1 do
+    for j=1,1 do
+        if i == 1 then
+            continue
+        else
+            break
+        end
+    end
+end
+)",
+                        0, 2),
+        R"(
+LOADN R2 1
+LOADN R0 1
+LOADN R1 1
+FORNPREP R0 +11
+LOADN R5 1
+LOADN R3 1
+LOADN R4 1
+FORNPREP R3 +6
+JUMPIFNOTEQK R2 K0 +5
+JUMP +2
+JUMP +1
+JUMP +1
+FORNLOOP R3 -6
+FORNLOOP R0 -11
+RETURN R0 0
+)");
+
+    // can't unroll loops if the body has functions that refer to loop variables
+    CHECK_EQ("\n" + compileFunction(R"(
+for i=1,1 do
+    local x = function() return i end
+end
+)",
+                        1, 2),
+        R"(
+LOADN R2 1
+LOADN R0 1
+LOADN R1 1
+FORNPREP R0 +3
+NEWCLOSURE R3 P0
+CAPTURE VAL R2
+FORNLOOP R0 -3
+RETURN R0 0
+)");
+}
+
+TEST_CASE("LoopUnrollCost")
+{
+    ScopedFastInt sfis[] = {
+        {"LuauCompileLoopUnrollThreshold", 25},
+        {"LuauCompileLoopUnrollThresholdMaxBoost", 300},
+    };
+
+    // loops with short body
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=1,10 do
+    t[i] = i
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 10
+LOADN R1 1
+SETTABLEN R1 R0 1
+LOADN R1 2
+SETTABLEN R1 R0 2
+LOADN R1 3
+SETTABLEN R1 R0 3
+LOADN R1 4
+SETTABLEN R1 R0 4
+LOADN R1 5
+SETTABLEN R1 R0 5
+LOADN R1 6
+SETTABLEN R1 R0 6
+LOADN R1 7
+SETTABLEN R1 R0 7
+LOADN R1 8
+SETTABLEN R1 R0 8
+LOADN R1 9
+SETTABLEN R1 R0 9
+LOADN R1 10
+SETTABLEN R1 R0 10
+RETURN R0 1
+)");
+
+    // loops with body that's too long
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=1,100 do
+    t[i] = i
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 0
+LOADN R3 1
+LOADN R1 100
+LOADN R2 1
+FORNPREP R1 +2
+SETTABLE R3 R0 R3
+FORNLOOP R1 -2
+RETURN R0 1
+)");
+
+    // loops with body that's long but has a high boost factor due to constant folding
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=1,30 do
+    t[i] = i * i * i
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 0
+LOADN R1 1
+SETTABLEN R1 R0 1
+LOADN R1 8
+SETTABLEN R1 R0 2
+LOADN R1 27
+SETTABLEN R1 R0 3
+LOADN R1 64
+SETTABLEN R1 R0 4
+LOADN R1 125
+SETTABLEN R1 R0 5
+LOADN R1 216
+SETTABLEN R1 R0 6
+LOADN R1 343
+SETTABLEN R1 R0 7
+LOADN R1 512
+SETTABLEN R1 R0 8
+LOADN R1 729
+SETTABLEN R1 R0 9
+LOADN R1 1000
+SETTABLEN R1 R0 10
+LOADN R1 1331
+SETTABLEN R1 R0 11
+LOADN R1 1728
+SETTABLEN R1 R0 12
+LOADN R1 2197
+SETTABLEN R1 R0 13
+LOADN R1 2744
+SETTABLEN R1 R0 14
+LOADN R1 3375
+SETTABLEN R1 R0 15
+LOADN R1 4096
+SETTABLEN R1 R0 16
+LOADN R1 4913
+SETTABLEN R1 R0 17
+LOADN R1 5832
+SETTABLEN R1 R0 18
+LOADN R1 6859
+SETTABLEN R1 R0 19
+LOADN R1 8000
+SETTABLEN R1 R0 20
+LOADN R1 9261
+SETTABLEN R1 R0 21
+LOADN R1 10648
+SETTABLEN R1 R0 22
+LOADN R1 12167
+SETTABLEN R1 R0 23
+LOADN R1 13824
+SETTABLEN R1 R0 24
+LOADN R1 15625
+SETTABLEN R1 R0 25
+LOADN R1 17576
+SETTABLEN R1 R0 26
+LOADN R1 19683
+SETTABLEN R1 R0 27
+LOADN R1 21952
+SETTABLEN R1 R0 28
+LOADN R1 24389
+SETTABLEN R1 R0 29
+LOADN R1 27000
+SETTABLEN R1 R0 30
+RETURN R0 1
+)");
+
+    // loops with body that's long and doesn't have a high boost factor
+    CHECK_EQ("\n" + compileFunction(R"(
+local t = {}
+for i=1,10 do
+    t[i] = math.abs(math.sin(i))
+end
+return t
+)",
+                        0, 2),
+        R"(
+NEWTABLE R0 0 10
+LOADN R3 1
+LOADN R1 10
+LOADN R2 1
+FORNPREP R1 +11
+FASTCALL1 24 R3 +3
+MOVE R6 R3
+GETIMPORT R5 2
+CALL R5 1 -1
+FASTCALL 2 +2
+GETIMPORT R4 4
+CALL R4 -1 1
+SETTABLE R4 R0 R3
+FORNLOOP R1 -11
+RETURN R0 1
+)");
+}
+
 TEST_SUITE_END();

tests/CostModel.test.cpp

@@ -98,4 +98,129 @@ end
     CHECK_EQ(2, Luau::Compile::computeCost(model, args2, 1));
 }
 
+TEST_CASE("ImportCall")
+{
+    uint64_t model = modelFunction(R"(
+function test(a)
+    return Instance.new(a)
+end
+)");
+
+    const bool args1[] = {false};
+    const bool args2[] = {true};
+
+    CHECK_EQ(6, Luau::Compile::computeCost(model, args1, 1));
+    CHECK_EQ(6, Luau::Compile::computeCost(model, args2, 1));
+}
+
+TEST_CASE("FastCall")
+{
+    uint64_t model = modelFunction(R"(
+function test(a)
+    return math.abs(a + 1)
+end
+)");
+
+    const bool args1[] = {false};
+    const bool args2[] = {true};
+
+    // note: we currently don't treat fast calls differently from cost model perspective
+    CHECK_EQ(6, Luau::Compile::computeCost(model, args1, 1));
+    CHECK_EQ(5, Luau::Compile::computeCost(model, args2, 1));
+}
+
+TEST_CASE("ControlFlow")
+{
+    uint64_t model = modelFunction(R"(
+function test(a)
+    while a < 0 do
+        a += 1
+    end
+    for i=1,2 do
+        a += 1
+    end
+    for i in pairs({}) do
+        a += 1
+        if a % 2 == 0 then continue end
+    end
+    repeat
+        a += 1
+        if a % 2 == 0 then break end
+    until a > 10
+    return a
+end
+)");
+
+    const bool args1[] = {false};
+    const bool args2[] = {true};
+
+    CHECK_EQ(38, Luau::Compile::computeCost(model, args1, 1));
+    CHECK_EQ(37, Luau::Compile::computeCost(model, args2, 1));
+}
+
+TEST_CASE("Conditional")
+{
+    uint64_t model = modelFunction(R"(
+function test(a)
+    return if a < 0 then -a else a
+end
+)");
+
+    const bool args1[] = {false};
+    const bool args2[] = {true};
+
+    CHECK_EQ(4, Luau::Compile::computeCost(model, args1, 1));
+    CHECK_EQ(2, Luau::Compile::computeCost(model, args2, 1));
+}
+
+TEST_CASE("VarArgs")
+{
+    uint64_t model = modelFunction(R"(
+function test(...)
+    return select('#', ...) :: number
+end
+)");
+
+    CHECK_EQ(8, Luau::Compile::computeCost(model, nullptr, 0));
+}
+
+TEST_CASE("TablesFunctions")
+{
+    uint64_t model = modelFunction(R"(
+function test()
+    return { 42, op = function() end }
+end
+)");
+
+    CHECK_EQ(22, Luau::Compile::computeCost(model, nullptr, 0));
+}
+
+TEST_CASE("CostOverflow")
+{
+    uint64_t model = modelFunction(R"(
+function test()
+    return {{{{{{{{{{{{{{{}}}}}}}}}}}}}}}
+end
+)");
+
+    CHECK_EQ(127, Luau::Compile::computeCost(model, nullptr, 0));
+}
+
+TEST_CASE("TableAssign")
+{
+    uint64_t model = modelFunction(R"(
+function test(a)
+    for i=1,#a do
+        a[i] = i
+    end
+end
+)");
+
+    const bool args1[] = {false};
+    const bool args2[] = {true};
+
+    CHECK_EQ(4, Luau::Compile::computeCost(model, args1, 1));
+    CHECK_EQ(3, Luau::Compile::computeCost(model, args2, 1));
+}
+
 TEST_SUITE_END();

tests/JsonEncoder.test.cpp

@@ -9,6 +9,46 @@
 
 using namespace Luau;
 
+struct JsonEncoderFixture
+{
+    Allocator allocator;
+    AstNameTable names{allocator};
+
+    ParseResult parse(std::string_view src)
+    {
+        ParseOptions opts;
+        opts.allowDeclarationSyntax = true;
+        return Parser::parse(src.data(), src.size(), names, allocator, opts);
+    }
+
+    AstStatBlock* expectParse(std::string_view src)
+    {
+        ParseResult res = parse(src);
+        REQUIRE(res.errors.size() == 0);
+        return res.root;
+    }
+
+    AstStat* expectParseStatement(std::string_view src)
+    {
+        AstStatBlock* root = expectParse(src);
+        REQUIRE(1 == root->body.size);
+        return root->body.data[0];
+    }
+
+    AstExpr* expectParseExpr(std::string_view src)
+    {
+        std::string s = "a = ";
+        s.append(src);
+        AstStatBlock* root = expectParse(s);
+
+        AstStatAssign* statAssign = root->body.data[0]->as<AstStatAssign>();
+        REQUIRE(statAssign != nullptr);
+        REQUIRE(statAssign->values.size == 1);
+
+        return statAssign->values.data[0];
+    }
+};
+
 TEST_SUITE_BEGIN("JsonEncoderTests");
 
 TEST_CASE("encode_constants")
@@ -51,7 +91,7 @@ TEST_CASE("encode_AstStatBlock")
         toJson(&block));
 }
 
-TEST_CASE("encode_tables")
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_tables")
 {
     std::string src = R"(
         local x: {
@@ -61,16 +101,294 @@ TEST_CASE("encode_tables")
         }
     )";
 
-    Allocator allocator;
-    AstNameTable names(allocator);
-    ParseResult parseResult = Parser::parse(src.c_str(), src.length(), names, allocator);
-
-    REQUIRE(parseResult.errors.size() == 0);
-    std::string json = toJson(parseResult.root);
+    AstStatBlock* root = expectParse(src);
+    std::string json = toJson(root);
 
     CHECK(
         json ==
         R"({"type":"AstStatBlock","location":"0,0 - 6,4","body":[{"type":"AstStatLocal","location":"1,8 - 5,9","vars":[{"type":{"type":"AstTypeTable","location":"1,17 - 3,9","props":[{"name":"foo","location":"2,12 - 2,15","type":{"type":"AstTypeReference","location":"2,17 - 2,23","name":"number","parameters":[]}}],"indexer":false},"name":"x","location":"1,14 - 1,15"}],"values":[{"type":"AstExprTable","location":"3,12 - 5,9","items":[{"kind":"record","key":{"type":"AstExprConstantString","location":"4,12 - 4,15","value":"foo"},"value":{"type":"AstExprConstantNumber","location":"4,18 - 4,21","value":123}}]}]}]})");
 }
 
+TEST_CASE("encode_AstExprGroup")
+{
+    AstExprConstantNumber number{Location{}, 5.0};
+    AstExprGroup group{Location{}, &number};
+
+    std::string json = toJson(&group);
+
+    const std::string expected = R"({"type":"AstExprGroup","location":"0,0 - 0,0","expr":{"type":"AstExprConstantNumber","location":"0,0 - 0,0","value":5}})";
+
+    CHECK(json == expected);
+}
+
+TEST_CASE("encode_AstExprGlobal")
+{
+    AstExprGlobal global{Location{}, AstName{"print"}};
+
+    std::string json = toJson(&global);
+    std::string expected = R"({"type":"AstExprGlobal","location":"0,0 - 0,0","global":"print"})";
+
+    CHECK(json == expected);
+}
+
+TEST_CASE("encode_AstExprLocal")
+{
+    AstLocal local{AstName{"foo"}, Location{}, nullptr, 0, 0, nullptr};
+    AstExprLocal exprLocal{Location{}, &local, false};
+
+    CHECK(toJson(&exprLocal) ==  R"({"type":"AstExprLocal","location":"0,0 - 0,0","local":{"type":null,"name":"foo","location":"0,0 - 0,0"}})");
+}
+
+TEST_CASE("encode_AstExprVarargs")
+{
+    AstExprVarargs varargs{Location{}};
+
+    CHECK(toJson(&varargs) == R"({"type":"AstExprVarargs","location":"0,0 - 0,0"})");
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprCall")
+{
+    AstExpr* expr = expectParseExpr("foo(1, 2, 3)");
+    std::string_view expected = R"({"type":"AstExprCall","location":"0,4 - 0,16","func":{"type":"AstExprGlobal","location":"0,4 - 0,7","global":"foo"},"args":[{"type":"AstExprConstantNumber","location":"0,8 - 0,9","value":1},{"type":"AstExprConstantNumber","location":"0,11 - 0,12","value":2},{"type":"AstExprConstantNumber","location":"0,14 - 0,15","value":3}],"self":false,"argLocation":"0,8 - 0,16"})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprIndexName")
+{
+    AstExpr* expr = expectParseExpr("foo.bar");
+
+    std::string_view expected = R"({"type":"AstExprIndexName","location":"0,4 - 0,11","expr":{"type":"AstExprGlobal","location":"0,4 - 0,7","global":"foo"},"index":"bar","indexLocation":"0,8 - 0,11","op":"."})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprIndexExpr")
+{
+    AstExpr* expr = expectParseExpr("foo['bar']");
+
+    std::string_view expected = R"({"type":"AstExprIndexExpr","location":"0,4 - 0,14","expr":{"type":"AstExprGlobal","location":"0,4 - 0,7","global":"foo"},"index":{"type":"AstExprConstantString","location":"0,8 - 0,13","value":"bar"}})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprFunction")
+{
+    AstExpr* expr = expectParseExpr("function (a) return a end");
+
+    std::string_view expected = R"({"type":"AstExprFunction","location":"0,4 - 0,29","generics":[],"genericPacks":[],"args":[{"type":null,"name":"a","location":"0,14 - 0,15"}],"vararg":false,"varargLocation":"0,0 - 0,0","body":{"type":"AstStatBlock","location":"0,16 - 0,26","body":[{"type":"AstStatReturn","location":"0,17 - 0,25","list":[{"type":"AstExprLocal","location":"0,24 - 0,25","local":{"type":null,"name":"a","location":"0,14 - 0,15"}}]}]},"functionDepth":1,"debugname":"","hasEnd":true})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprTable")
+{
+    AstExpr* expr = expectParseExpr("{true, key=true, [key2]=true}");
+
+    std::string_view expected = R"({"type":"AstExprTable","location":"0,4 - 0,33","items":[{"kind":"item","value":{"type":"AstExprConstantBool","location":"0,5 - 0,9","value":true}},{"kind":"record","key":{"type":"AstExprConstantString","location":"0,11 - 0,14","value":"key"},"value":{"type":"AstExprConstantBool","location":"0,15 - 0,19","value":true}},{"kind":"general","key":{"type":"AstExprGlobal","location":"0,22 - 0,26","global":"key2"},"value":{"type":"AstExprConstantBool","location":"0,28 - 0,32","value":true}}]})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprUnary")
+{
+    AstExpr* expr = expectParseExpr("-b");
+
+    std::string_view expected = R"({"type":"AstExprUnary","location":"0,4 - 0,6","op":"minus","expr":{"type":"AstExprGlobal","location":"0,5 - 0,6","global":"b"}})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprBinary")
+{
+    AstExpr* expr = expectParseExpr("b + c");
+
+    std::string_view expected = R"({"type":"AstExprBinary","location":"0,4 - 0,9","op":"Add","left":{"type":"AstExprGlobal","location":"0,4 - 0,5","global":"b"},"right":{"type":"AstExprGlobal","location":"0,8 - 0,9","global":"c"}})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprTypeAssertion")
+{
+    AstExpr* expr = expectParseExpr("b :: any");
+
+    std::string_view expected = R"({"type":"AstExprTypeAssertion","location":"0,4 - 0,12","expr":{"type":"AstExprGlobal","location":"0,4 - 0,5","global":"b"},"annotation":{"type":"AstTypeReference","location":"0,9 - 0,12","name":"any","parameters":[]}})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstExprError")
+{
+    std::string_view src = "a = ";
+    ParseResult parseResult = Parser::parse(src.data(), src.size(), names, allocator);
+
+    REQUIRE(1 == parseResult.root->body.size);
+
+    AstStatAssign* statAssign = parseResult.root->body.data[0]->as<AstStatAssign>();
+    REQUIRE(statAssign != nullptr);
+    REQUIRE(1 == statAssign->values.size);
+
+    AstExpr* expr = statAssign->values.data[0];
+
+    std::string_view expected = R"({"type":"AstExprError","location":"0,4 - 0,4","expressions":[],"messageIndex":0})";
+
+    CHECK(toJson(expr) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatIf")
+{
+    AstStat* statement = expectParseStatement("if true then else end");
+
+    std::string_view expected = R"({"type":"AstStatIf","location":"0,0 - 0,21","condition":{"type":"AstExprConstantBool","location":"0,3 - 0,7","value":true},"thenbody":{"type":"AstStatBlock","location":"0,12 - 0,13","body":[]},"elsebody":{"type":"AstStatBlock","location":"0,17 - 0,18","body":[]},"hasThen":true,"hasEnd":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatWhile")
+{
+    AstStat* statement = expectParseStatement("while true do end");
+
+    std::string_view expected = R"({"type":"AtStatWhile","location":"0,0 - 0,17","condition":{"type":"AstExprConstantBool","location":"0,6 - 0,10","value":true},"body":{"type":"AstStatBlock","location":"0,13 - 0,14","body":[]},"hasDo":true,"hasEnd":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatRepeat")
+{
+    AstStat* statement = expectParseStatement("repeat until true");
+
+    std::string_view expected = R"({"type":"AstStatRepeat","location":"0,0 - 0,17","condition":{"type":"AstExprConstantBool","location":"0,13 - 0,17","value":true},"body":{"type":"AstStatBlock","location":"0,6 - 0,7","body":[]},"hasUntil":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatBreak")
+{
+    AstStat* statement = expectParseStatement("while true do break end");
+
+    std::string_view expected = R"({"type":"AtStatWhile","location":"0,0 - 0,23","condition":{"type":"AstExprConstantBool","location":"0,6 - 0,10","value":true},"body":{"type":"AstStatBlock","location":"0,13 - 0,20","body":[{"type":"AstStatBreak","location":"0,14 - 0,19"}]},"hasDo":true,"hasEnd":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatContinue")
+{
+    AstStat* statement = expectParseStatement("while true do continue end");
+
+    std::string_view expected = R"({"type":"AtStatWhile","location":"0,0 - 0,26","condition":{"type":"AstExprConstantBool","location":"0,6 - 0,10","value":true},"body":{"type":"AstStatBlock","location":"0,13 - 0,23","body":[{"type":"AstStatContinue","location":"0,14 - 0,22"}]},"hasDo":true,"hasEnd":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatFor")
+{
+    AstStat* statement = expectParseStatement("for a=0,1 do end");
+
+    std::string_view expected = R"({"type":"AstStatFor","location":"0,0 - 0,16","var":{"type":null,"name":"a","location":"0,4 - 0,5"},"from":{"type":"AstExprConstantNumber","location":"0,6 - 0,7","value":0},"to":{"type":"AstExprConstantNumber","location":"0,8 - 0,9","value":1},"body":{"type":"AstStatBlock","location":"0,12 - 0,13","body":[]},"hasDo":true,"hasEnd":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatForIn")
+{
+    AstStat* statement = expectParseStatement("for a in b do end");
+
+    std::string_view expected = R"({"type":"AstStatForIn","location":"0,0 - 0,17","vars":[{"type":null,"name":"a","location":"0,4 - 0,5"}],"values":[{"type":"AstExprGlobal","location":"0,9 - 0,10","global":"b"}],"body":{"type":"AstStatBlock","location":"0,13 - 0,14","body":[]},"hasIn":true,"hasDo":true,"hasEnd":true})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatCompoundAssign")
+{
+    AstStat* statement = expectParseStatement("a += b");
+
+    std::string_view expected = R"({"type":"AstStatCompoundAssign","location":"0,0 - 0,6","op":"Add","var":{"type":"AstExprGlobal","location":"0,0 - 0,1","global":"a"},"value":{"type":"AstExprGlobal","location":"0,5 - 0,6","global":"b"}})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatLocalFunction")
+{
+    AstStat* statement = expectParseStatement("local function a(b) return end");
+
+    std::string_view expected = R"({"type":"AstStatLocalFunction","location":"0,0 - 0,30","name":{"type":null,"name":"a","location":"0,15 - 0,16"},"func":{"type":"AstExprFunction","location":"0,0 - 0,30","generics":[],"genericPacks":[],"args":[{"type":null,"name":"b","location":"0,17 - 0,18"}],"vararg":false,"varargLocation":"0,0 - 0,0","body":{"type":"AstStatBlock","location":"0,19 - 0,27","body":[{"type":"AstStatReturn","location":"0,20 - 0,26","list":[]}]},"functionDepth":1,"debugname":"a","hasEnd":true}})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatTypeAlias")
+{
+    AstStat* statement = expectParseStatement("type A = B");
+
+    std::string_view expected = R"({"type":"AstStatTypeAlias","location":"0,0 - 0,10","name":"A","generics":[],"genericPacks":[],"type":{"type":"AstTypeReference","location":"0,9 - 0,10","name":"B","parameters":[]},"exported":false})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatDeclareFunction")
+{
+    AstStat* statement = expectParseStatement("declare function foo(x: number): string");
+
+    std::string_view expected = R"({"type":"AstStatDeclareFunction","location":"0,0 - 0,39","name":"foo","params":{"types":[{"type":"AstTypeReference","location":"0,24 - 0,30","name":"number","parameters":[]}]},"retTypes":{"types":[{"type":"AstTypeReference","location":"0,33 - 0,39","name":"string","parameters":[]}]},"generics":[],"genericPacks":[]})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstStatDeclareClass")
+{
+    AstStatBlock* root = expectParse(R"(
+        declare class Foo
+            prop: number
+            function method(self, foo: number): string
+        end
+
+        declare class Bar extends Foo
+            prop2: string
+        end
+    )");
+
+    REQUIRE(2 == root->body.size);
+
+    std::string_view expected1 = R"({"type":"AstStatDeclareClass","location":"1,22 - 4,11","name":"Foo","props":[{"name":"prop","type":{"type":"AstTypeReference","location":"2,18 - 2,24","name":"number","parameters":[]}},{"name":"method","type":{"type":"AstTypeFunction","location":"3,21 - 4,11","generics":[],"genericPacks":[],"argTypes":{"types":[{"type":"AstTypeReference","location":"3,39 - 3,45","name":"number","parameters":[]}]},"returnTypes":{"types":[{"type":"AstTypeReference","location":"3,48 - 3,54","name":"string","parameters":[]}]}}}]})";
+    CHECK(toJson(root->body.data[0]) == expected1);
+
+    std::string_view expected2 = R"({"type":"AstStatDeclareClass","location":"6,22 - 8,11","name":"Bar","superName":"Foo","props":[{"name":"prop2","type":{"type":"AstTypeReference","location":"7,19 - 7,25","name":"string","parameters":[]}}]})";
+    CHECK(toJson(root->body.data[1]) == expected2);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_annotation")
+{
+    AstStat* statement = expectParseStatement("type T = ((number) -> (string | nil)) & ((string) -> ())");
+
+    std::string_view expected = R"({"type":"AstStatTypeAlias","location":"0,0 - 0,55","name":"T","generics":[],"genericPacks":[],"type":{"type":"AstTypeIntersection","location":"0,9 - 0,55","types":[{"type":"AstTypeFunction","location":"0,10 - 0,35","generics":[],"genericPacks":[],"argTypes":{"types":[{"type":"AstTypeReference","location":"0,11 - 0,17","name":"number","parameters":[]}]},"returnTypes":{"types":[{"type":"AstTypeUnion","location":"0,23 - 0,35","types":[{"type":"AstTypeReference","location":"0,23 - 0,29","name":"string","parameters":[]},{"type":"AstTypeReference","location":"0,32 - 0,35","name":"nil","parameters":[]}]}]}},{"type":"AstTypeFunction","location":"0,41 - 0,55","generics":[],"genericPacks":[],"argTypes":{"types":[{"type":"AstTypeReference","location":"0,42 - 0,48","name":"string","parameters":[]}]},"returnTypes":{"types":[]}}]},"exported":false})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstTypeError")
+{
+    ParseResult parseResult = parse("type T = ");
+    REQUIRE(1 == parseResult.root->body.size);
+
+    AstStat* statement = parseResult.root->body.data[0];
+
+    std::string_view expected = R"({"type":"AstStatTypeAlias","location":"0,0 - 0,9","name":"T","generics":[],"genericPacks":[],"type":{"type":"AstTypeError","location":"0,8 - 0,9","types":[],"messageIndex":0},"exported":false})";
+
+    CHECK(toJson(statement) == expected);
+}
+
+TEST_CASE_FIXTURE(JsonEncoderFixture, "encode_AstTypePackExplicit")
+{
+    AstStatBlock* root = expectParse(R"(
+        type A<T...> = () -> T...
+        local a: A<(number, string)>
+    )");
+
+    CHECK(2 == root->body.size);
+
+    std::string_view expected = R"({"type":"AstStatLocal","location":"2,8 - 2,36","vars":[{"type":{"type":"AstTypeReference","location":"2,17 - 2,36","name":"A","parameters":[{"type":"AstTypePackExplicit","location":"2,19 - 2,20","typeList":{"types":[{"type":"AstTypeReference","location":"2,20 - 2,26","name":"number","parameters":[]},{"type":"AstTypeReference","location":"2,28 - 2,34","name":"string","parameters":[]}]}}]},"name":"a","location":"2,14 - 2,15"}],"values":[]})";
+
+    CHECK(toJson(root->body.data[1]) == expected);
+}
+
 TEST_SUITE_END();

tests/Linter.test.cpp

@@ -1436,7 +1436,7 @@ TEST_CASE_FIXTURE(Fixture, "LintHygieneUAF")
 TEST_CASE_FIXTURE(Fixture, "DeprecatedApi")
 {
     unfreeze(typeChecker.globalTypes);
-    TypeId instanceType = typeChecker.globalTypes.addType(ClassTypeVar{"Instance", {}, std::nullopt, std::nullopt, {}, {}});
+    TypeId instanceType = typeChecker.globalTypes.addType(ClassTypeVar{"Instance", {}, std::nullopt, std::nullopt, {}, {}, "Test"});
     persist(instanceType);
     typeChecker.globalScope->exportedTypeBindings["Instance"] = TypeFun{{}, instanceType};
 

tests/Module.test.cpp

@@ -173,13 +173,13 @@ TEST_CASE_FIXTURE(Fixture, "clone_class")
         {
             {"__add", {typeChecker.anyType}},
         },
-        std::nullopt, std::nullopt, {}, {}}};
+        std::nullopt, std::nullopt, {}, {}, "Test"}};
     TypeVar exampleClass{ClassTypeVar{"ExampleClass",
         {
             {"PropOne", {typeChecker.numberType}},
             {"PropTwo", {typeChecker.stringType}},
         },
-        std::nullopt, &exampleMetaClass, {}, {}}};
+        std::nullopt, &exampleMetaClass, {}, {}, "Test"}};
 
     TypeArena dest;
     CloneState cloneState;
@@ -196,9 +196,12 @@ TEST_CASE_FIXTURE(Fixture, "clone_class")
     CHECK_EQ("ExampleClassMeta", metatable->name);
 }
 
-TEST_CASE_FIXTURE(Fixture, "clone_sanitize_free_types")
+TEST_CASE_FIXTURE(Fixture, "clone_free_types")
 {
-    ScopedFastFlag sff{"LuauErrorRecoveryType", true};
+    ScopedFastFlag sff[]{
+        {"LuauErrorRecoveryType", true},
+        {"LuauLosslessClone", true},
+    };
 
     TypeVar freeTy(FreeTypeVar{TypeLevel{}});
     TypePackVar freeTp(FreeTypePack{TypeLevel{}});
@@ -207,17 +210,17 @@ TEST_CASE_FIXTURE(Fixture, "clone_sanitize_free_types")
     CloneState cloneState;
 
     TypeId clonedTy = clone(&freeTy, dest, cloneState);
-    CHECK_EQ("any", toString(clonedTy));
-    CHECK(cloneState.encounteredFreeType);
+    CHECK(get<FreeTypeVar>(clonedTy));
 
     cloneState = {};
     TypePackId clonedTp = clone(&freeTp, dest, cloneState);
-    CHECK_EQ("...any", toString(clonedTp));
-    CHECK(cloneState.encounteredFreeType);
+    CHECK(get<FreeTypePack>(clonedTp));
 }
 
-TEST_CASE_FIXTURE(Fixture, "clone_seal_free_tables")
+TEST_CASE_FIXTURE(Fixture, "clone_free_tables")
 {
+    ScopedFastFlag sff{"LuauLosslessClone", true};
+
     TypeVar tableTy{TableTypeVar{}};
     TableTypeVar* ttv = getMutable<TableTypeVar>(&tableTy);
     ttv->state = TableState::Free;
@@ -227,8 +230,7 @@ TEST_CASE_FIXTURE(Fixture, "clone_seal_free_tables")
 
     TypeId cloned = clone(&tableTy, dest, cloneState);
     const TableTypeVar* clonedTtv = get<TableTypeVar>(cloned);
-    CHECK_EQ(clonedTtv->state, TableState::Sealed);
-    CHECK(cloneState.encounteredFreeType);
+    CHECK_EQ(clonedTtv->state, TableState::Free);
 }
 
 TEST_CASE_FIXTURE(Fixture, "clone_constrained_intersection")

tests/NonstrictMode.test.cpp

@@ -13,6 +13,29 @@ using namespace Luau;
 
 TEST_SUITE_BEGIN("NonstrictModeTests");
 
+TEST_CASE_FIXTURE(Fixture, "function_returns_number_or_string")
+{
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true}
+    };
+
+    CheckResult result = check(R"(
+        --!nonstrict
+        local function f()
+            if math.random() > 0.5 then
+                return 5
+            else
+                return "hi"
+            end
+        end
+    )");
+
+    LUAU_REQUIRE_NO_ERRORS(result);
+
+    CHECK("() -> number | string" == toString(requireType("f")));
+}
+
 TEST_CASE_FIXTURE(Fixture, "infer_nullary_function")
 {
     CheckResult result = check(R"(
@@ -35,8 +58,13 @@ TEST_CASE_FIXTURE(Fixture, "infer_nullary_function")
     REQUIRE_EQ(0, rets.size());
 }
 
-TEST_CASE_FIXTURE(Fixture, "infer_the_maximum_number_of_values_the_function_could_return")
+TEST_CASE_FIXTURE(Fixture, "first_return_type_dictates_number_of_return_types")
 {
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+    };
+
     CheckResult result = check(R"(
         --!nonstrict
         function getMinCardCountForWidth(width)
@@ -51,22 +79,18 @@ TEST_CASE_FIXTURE(Fixture, "infer_the_maximum_number_of_values_the_function_coul
     TypeId t = requireType("getMinCardCountForWidth");
     REQUIRE(t);
 
-    REQUIRE_EQ("(any) -> (...any)", toString(t));
+    REQUIRE_EQ("(any) -> number", toString(t));
 }
 
-#if 0
-// Maybe we want this?
 TEST_CASE_FIXTURE(Fixture, "return_annotation_is_still_checked")
 {
     CheckResult result = check(R"(
+        --!nonstrict
         function foo(x): number return 'hello' end
     )");
 
     LUAU_REQUIRE_ERROR_COUNT(1, result);
-
-    REQUIRE_NE(*typeChecker.anyType, *requireType("foo"));
 }
-#endif
 
 TEST_CASE_FIXTURE(Fixture, "function_parameters_are_any")
 {
@@ -256,6 +280,12 @@ TEST_CASE_FIXTURE(Fixture, "delay_function_does_not_require_its_argument_to_retu
 
 TEST_CASE_FIXTURE(Fixture, "inconsistent_module_return_types_are_ok")
 {
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+        {"LuauSealExports", true},
+    };
+
     CheckResult result = check(R"(
         --!nonstrict
 
@@ -272,7 +302,7 @@ TEST_CASE_FIXTURE(Fixture, "inconsistent_module_return_types_are_ok")
 
     LUAU_REQUIRE_NO_ERRORS(result);
 
-    REQUIRE_EQ("any", toString(getMainModule()->getModuleScope()->returnType));
+    REQUIRE_EQ("((any) -> string) | {| foo: any |}", toString(getMainModule()->getModuleScope()->returnType));
 }
 
 TEST_CASE_FIXTURE(Fixture, "returning_insufficient_return_values")

tests/Normalize.test.cpp

@@ -21,7 +21,7 @@ void createSomeClasses(TypeChecker& typeChecker)
 
     unfreeze(arena);
 
-    TypeId parentType = arena.addType(ClassTypeVar{"Parent", {}, std::nullopt, std::nullopt, {}, nullptr});
+    TypeId parentType = arena.addType(ClassTypeVar{"Parent", {}, std::nullopt, std::nullopt, {}, nullptr, "Test"});
 
     ClassTypeVar* parentClass = getMutable<ClassTypeVar>(parentType);
     parentClass->props["method"] = {makeFunction(arena, parentType, {}, {})};
@@ -31,7 +31,7 @@ void createSomeClasses(TypeChecker& typeChecker)
     addGlobalBinding(typeChecker, "Parent", {parentType});
     typeChecker.globalScope->exportedTypeBindings["Parent"] = TypeFun{{}, parentType};
 
-    TypeId childType = arena.addType(ClassTypeVar{"Child", {}, parentType, std::nullopt, {}, nullptr});
+    TypeId childType = arena.addType(ClassTypeVar{"Child", {}, parentType, std::nullopt, {}, nullptr, "Test"});
 
     ClassTypeVar* childClass = getMutable<ClassTypeVar>(childType);
     childClass->props["virtual_method"] = {makeFunction(arena, childType, {}, {})};
@@ -39,7 +39,7 @@ void createSomeClasses(TypeChecker& typeChecker)
     addGlobalBinding(typeChecker, "Child", {childType});
     typeChecker.globalScope->exportedTypeBindings["Child"] = TypeFun{{}, childType};
 
-    TypeId unrelatedType = arena.addType(ClassTypeVar{"Unrelated", {}, std::nullopt, std::nullopt, {}, nullptr});
+    TypeId unrelatedType = arena.addType(ClassTypeVar{"Unrelated", {}, std::nullopt, std::nullopt, {}, nullptr, "Test"});
 
     addGlobalBinding(typeChecker, "Unrelated", {unrelatedType});
     typeChecker.globalScope->exportedTypeBindings["Unrelated"] = TypeFun{{}, unrelatedType};
@@ -400,7 +400,6 @@ TEST_CASE_FIXTURE(NormalizeFixture, "table_with_table_prop")
     CHECK_EQ("{| x: {| y: number & string |} |}", toString(requireType("a")));
 }
 
-#if 0
 TEST_CASE_FIXTURE(NormalizeFixture, "tables")
 {
     check(R"(
@@ -428,6 +427,7 @@ TEST_CASE_FIXTURE(NormalizeFixture, "tables")
     CHECK(!isSubtype(b, d));
 }
 
+#if 0
 TEST_CASE_FIXTURE(NormalizeFixture, "table_indexers_are_invariant")
 {
     check(R"(
@@ -619,6 +619,7 @@ TEST_CASE_FIXTURE(Fixture, "normalize_module_return_type")
 {
     ScopedFastFlag sff[] = {
         {"LuauLowerBoundsCalculation", true},
+        {"LuauReturnTypeInferenceInNonstrict", true},
     };
 
     check(R"(
@@ -639,7 +640,7 @@ TEST_CASE_FIXTURE(Fixture, "normalize_module_return_type")
         end
     )");
 
-    CHECK_EQ("(any, any) -> (...any)", toString(getMainModule()->getModuleScope()->returnType));
+    CHECK_EQ("(any, any) -> (any, any) -> any", toString(getMainModule()->getModuleScope()->returnType));
 }
 
 TEST_CASE_FIXTURE(Fixture, "return_type_is_not_a_constrained_intersection")
@@ -950,6 +951,27 @@ TEST_CASE_FIXTURE(Fixture, "nested_table_normalization_with_non_table__no_ice")
     LUAU_REQUIRE_NO_ERRORS(result);
 }
 
+TEST_CASE_FIXTURE(Fixture, "visiting_a_type_twice_is_not_considered_normal")
+{
+    ScopedFastFlag sff{"LuauLowerBoundsCalculation", true};
+
+    CheckResult result = check(R"(
+        --!strict
+        function f(a, b)
+            local function g()
+                if math.random() > 0.5 then
+                    return a()
+                else
+                    return b
+                end
+            end
+        end
+    )");
+
+    LUAU_REQUIRE_NO_ERRORS(result);
+    CHECK_EQ("<a>(() -> a, a) -> ()", toString(requireType("f")));
+}
+
 TEST_CASE_FIXTURE(Fixture, "fuzz_failure_instersection_combine_must_follow")
 {
     ScopedFastFlag flags[] = {
@@ -964,4 +986,16 @@ TEST_CASE_FIXTURE(Fixture, "fuzz_failure_instersection_combine_must_follow")
     LUAU_REQUIRE_NO_ERRORS(result);
 }
 
+TEST_CASE_FIXTURE(Fixture, "fuzz_failure_bound_type_is_normal_but_not_its_bounded_to")
+{
+    ScopedFastFlag sff{"LuauLowerBoundsCalculation", true};
+
+    CheckResult result = check(R"(
+        type t252 = ((t0<t252...>)|(any))|(any)
+        type t0 = t252<t0<any,t24...>,t24...>
+    )");
+
+    LUAU_REQUIRE_ERRORS(result);
+}
+
 TEST_SUITE_END();

tests/ToDot.test.cpp

@@ -21,13 +21,13 @@ struct ToDotClassFixture : Fixture
 
         TypeId baseClassMetaType = arena.addType(TableTypeVar{});
 
-        TypeId baseClassInstanceType = arena.addType(ClassTypeVar{"BaseClass", {}, std::nullopt, baseClassMetaType, {}, {}});
+        TypeId baseClassInstanceType = arena.addType(ClassTypeVar{"BaseClass", {}, std::nullopt, baseClassMetaType, {}, {}, "Test"});
         getMutable<ClassTypeVar>(baseClassInstanceType)->props = {
             {"BaseField", {typeChecker.numberType}},
         };
         typeChecker.globalScope->exportedTypeBindings["BaseClass"] = TypeFun{{}, baseClassInstanceType};
 
-        TypeId childClassInstanceType = arena.addType(ClassTypeVar{"ChildClass", {}, baseClassInstanceType, std::nullopt, {}, {}});
+        TypeId childClassInstanceType = arena.addType(ClassTypeVar{"ChildClass", {}, baseClassInstanceType, std::nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(childClassInstanceType)->props = {
             {"ChildField", {typeChecker.stringType}},
         };

tests/Transpiler.test.cpp

@@ -661,4 +661,21 @@ type t4 = false
     CHECK_EQ(code, transpile(code, {}, true).code);
 }
 
+TEST_CASE_FIXTURE(Fixture, "transpile_array_types")
+{
+    std::string code = R"(
+type t1 = {number}
+type t2 = {[string]: number}
+    )";
+
+    CHECK_EQ(code, transpile(code, {}, true).code);
+}
+
+TEST_CASE_FIXTURE(Fixture, "transpile_for_in_multiple_types")
+{
+    std::string code = "for k:string,v:boolean in next,{}do end";
+
+    CHECK_EQ(code, transpile(code, {}, true).code);
+}
+
 TEST_SUITE_END();

tests/TypeInfer.classes.test.cpp

@@ -19,13 +19,13 @@ struct ClassFixture : Fixture
 
         unfreeze(arena);
 
-        TypeId baseClassInstanceType = arena.addType(ClassTypeVar{"BaseClass", {}, nullopt, nullopt, {}, {}});
+        TypeId baseClassInstanceType = arena.addType(ClassTypeVar{"BaseClass", {}, nullopt, nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(baseClassInstanceType)->props = {
             {"BaseMethod", {makeFunction(arena, baseClassInstanceType, {numberType}, {})}},
             {"BaseField", {numberType}},
         };
 
-        TypeId baseClassType = arena.addType(ClassTypeVar{"BaseClass", {}, nullopt, nullopt, {}, {}});
+        TypeId baseClassType = arena.addType(ClassTypeVar{"BaseClass", {}, nullopt, nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(baseClassType)->props = {
             {"StaticMethod", {makeFunction(arena, nullopt, {}, {numberType})}},
             {"Clone", {makeFunction(arena, nullopt, {baseClassInstanceType}, {baseClassInstanceType})}},
@@ -34,39 +34,39 @@ struct ClassFixture : Fixture
         typeChecker.globalScope->exportedTypeBindings["BaseClass"] = TypeFun{{}, baseClassInstanceType};
         addGlobalBinding(typeChecker, "BaseClass", baseClassType, "@test");
 
-        TypeId childClassInstanceType = arena.addType(ClassTypeVar{"ChildClass", {}, baseClassInstanceType, nullopt, {}, {}});
+        TypeId childClassInstanceType = arena.addType(ClassTypeVar{"ChildClass", {}, baseClassInstanceType, nullopt, {}, {}, "Test"});
 
         getMutable<ClassTypeVar>(childClassInstanceType)->props = {
             {"Method", {makeFunction(arena, childClassInstanceType, {}, {typeChecker.stringType})}},
         };
 
-        TypeId childClassType = arena.addType(ClassTypeVar{"ChildClass", {}, baseClassType, nullopt, {}, {}});
+        TypeId childClassType = arena.addType(ClassTypeVar{"ChildClass", {}, baseClassType, nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(childClassType)->props = {
             {"New", {makeFunction(arena, nullopt, {}, {childClassInstanceType})}},
         };
         typeChecker.globalScope->exportedTypeBindings["ChildClass"] = TypeFun{{}, childClassInstanceType};
         addGlobalBinding(typeChecker, "ChildClass", childClassType, "@test");
 
-        TypeId grandChildInstanceType = arena.addType(ClassTypeVar{"GrandChild", {}, childClassInstanceType, nullopt, {}, {}});
+        TypeId grandChildInstanceType = arena.addType(ClassTypeVar{"GrandChild", {}, childClassInstanceType, nullopt, {}, {}, "Test"});
 
         getMutable<ClassTypeVar>(grandChildInstanceType)->props = {
             {"Method", {makeFunction(arena, grandChildInstanceType, {}, {typeChecker.stringType})}},
         };
 
-        TypeId grandChildType = arena.addType(ClassTypeVar{"GrandChild", {}, baseClassType, nullopt, {}, {}});
+        TypeId grandChildType = arena.addType(ClassTypeVar{"GrandChild", {}, baseClassType, nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(grandChildType)->props = {
             {"New", {makeFunction(arena, nullopt, {}, {grandChildInstanceType})}},
         };
         typeChecker.globalScope->exportedTypeBindings["GrandChild"] = TypeFun{{}, grandChildInstanceType};
         addGlobalBinding(typeChecker, "GrandChild", childClassType, "@test");
 
-        TypeId anotherChildInstanceType = arena.addType(ClassTypeVar{"AnotherChild", {}, baseClassInstanceType, nullopt, {}, {}});
+        TypeId anotherChildInstanceType = arena.addType(ClassTypeVar{"AnotherChild", {}, baseClassInstanceType, nullopt, {}, {}, "Test"});
 
         getMutable<ClassTypeVar>(anotherChildInstanceType)->props = {
             {"Method", {makeFunction(arena, anotherChildInstanceType, {}, {typeChecker.stringType})}},
         };
 
-        TypeId anotherChildType = arena.addType(ClassTypeVar{"AnotherChild", {}, baseClassType, nullopt, {}, {}});
+        TypeId anotherChildType = arena.addType(ClassTypeVar{"AnotherChild", {}, baseClassType, nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(anotherChildType)->props = {
             {"New", {makeFunction(arena, nullopt, {}, {anotherChildInstanceType})}},
         };
@@ -75,13 +75,13 @@ struct ClassFixture : Fixture
 
         TypeId vector2MetaType = arena.addType(TableTypeVar{});
 
-        TypeId vector2InstanceType = arena.addType(ClassTypeVar{"Vector2", {}, nullopt, vector2MetaType, {}, {}});
+        TypeId vector2InstanceType = arena.addType(ClassTypeVar{"Vector2", {}, nullopt, vector2MetaType, {}, {}, "Test"});
         getMutable<ClassTypeVar>(vector2InstanceType)->props = {
             {"X", {numberType}},
             {"Y", {numberType}},
         };
 
-        TypeId vector2Type = arena.addType(ClassTypeVar{"Vector2", {}, nullopt, nullopt, {}, {}});
+        TypeId vector2Type = arena.addType(ClassTypeVar{"Vector2", {}, nullopt, nullopt, {}, {}, "Test"});
         getMutable<ClassTypeVar>(vector2Type)->props = {
             {"New", {makeFunction(arena, nullopt, {numberType, numberType}, {vector2InstanceType})}},
         };
@@ -468,4 +468,18 @@ caused by:
         toString(result.errors[0]));
 }
 
+TEST_CASE_FIXTURE(ClassFixture, "class_type_mismatch_with_name_conflict")
+{
+    ScopedFastFlag luauClassDefinitionModuleInError{"LuauClassDefinitionModuleInError", true};
+
+    CheckResult result = check(R"(
+local i = ChildClass.New()
+type ChildClass = { x: number }
+local a: ChildClass = i
+    )");
+
+    LUAU_REQUIRE_ERROR_COUNT(1, result);
+    CHECK_EQ("Type 'ChildClass' from 'Test' could not be converted into 'ChildClass' from 'MainModule'", toString(result.errors[0]));
+}
+
 TEST_SUITE_END();

tests/TypeInfer.definitions.test.cpp

@@ -295,8 +295,6 @@ TEST_CASE_FIXTURE(Fixture, "documentation_symbols_dont_attach_to_persistent_type
 
 TEST_CASE_FIXTURE(Fixture, "single_class_type_identity_in_global_types")
 {
-    ScopedFastFlag luauCloneDeclaredGlobals{"LuauCloneDeclaredGlobals", true};
-
     loadDefinition(R"(
 declare class Cls
 end

tests/TypeInfer.functions.test.cpp

@@ -656,6 +656,11 @@ TEST_CASE_FIXTURE(Fixture, "toposort_doesnt_break_mutual_recursion")
 
 TEST_CASE_FIXTURE(Fixture, "check_function_before_lambda_that_uses_it")
 {
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+    };
+
     CheckResult result = check(R"(
         --!nonstrict
 
@@ -664,7 +669,7 @@ TEST_CASE_FIXTURE(Fixture, "check_function_before_lambda_that_uses_it")
         end
 
         return function()
-            return f():andThen()
+            return f()
         end
     )");
 
@@ -791,14 +796,18 @@ TEST_CASE_FIXTURE(Fixture, "calling_function_with_incorrect_argument_type_yields
 
 TEST_CASE_FIXTURE(Fixture, "calling_function_with_anytypepack_doesnt_leak_free_types")
 {
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+    };
+
     CheckResult result = check(R"(
         --!nonstrict
 
-        function Test(a)
+        function Test(a): ...any
             return 1, ""
         end
 
-
         local tab = {}
         table.insert(tab, Test(1));
     )");
@@ -1616,4 +1625,19 @@ TEST_CASE_FIXTURE(Fixture, "occurs_check_failure_in_function_return_type")
     CHECK(nullptr != get<OccursCheckFailed>(result.errors[0]));
 }
 
+TEST_CASE_FIXTURE(Fixture, "weird_fail_to_unify_type_pack")
+{
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+    };
+
+    CheckResult result = check(R"(
+        local function f() return end
+        local g = function() return f() end
+    )");
+
+    LUAU_REQUIRE_NO_ERRORS(result);
+}
+
 TEST_SUITE_END();

tests/TypeInfer.modules.test.cpp

@@ -307,8 +307,6 @@ type Rename = typeof(x.x)
 
 TEST_CASE_FIXTURE(Fixture, "module_type_conflict")
 {
-    ScopedFastFlag luauTypeMismatchModuleName{"LuauTypeMismatchModuleName", true};
-
     fileResolver.source["game/A"] = R"(
 export type T = { x: number }
 return {}
@@ -343,8 +341,6 @@ caused by:
 
 TEST_CASE_FIXTURE(Fixture, "module_type_conflict_instantiated")
 {
-    ScopedFastFlag luauTypeMismatchModuleName{"LuauTypeMismatchModuleName", true};
-
     fileResolver.source["game/A"] = R"(
 export type Wrap<T> = { x: T }
 return {}

tests/TypeInfer.provisional.test.cpp

@@ -584,20 +584,6 @@ TEST_CASE_FIXTURE(Fixture, "specialization_binds_with_prototypes_too_early")
     LUAU_REQUIRE_ERRORS(result); // Should not have any errors.
 }
 
-TEST_CASE_FIXTURE(Fixture, "weird_fail_to_unify_type_pack")
-{
-    ScopedFastFlag sff[] = {
-        {"LuauLowerBoundsCalculation", false},
-    };
-
-    CheckResult result = check(R"(
-        local function f() return end
-        local g = function() return f() end
-    )");
-
-    LUAU_REQUIRE_ERRORS(result); // Should not have any errors.
-}
-
 TEST_CASE_FIXTURE(Fixture, "weird_fail_to_unify_variadic_pack")
 {
     ScopedFastFlag sff[] = {

tests/TypeInfer.refinements.test.cpp

@@ -44,7 +44,7 @@ struct RefinementClassFixture : Fixture
         TypeArena& arena = typeChecker.globalTypes;
 
         unfreeze(arena);
-        TypeId vec3 = arena.addType(ClassTypeVar{"Vector3", {}, std::nullopt, std::nullopt, {}, nullptr});
+        TypeId vec3 = arena.addType(ClassTypeVar{"Vector3", {}, std::nullopt, std::nullopt, {}, nullptr, "Test"});
         getMutable<ClassTypeVar>(vec3)->props = {
             {"X", Property{typeChecker.numberType}},
             {"Y", Property{typeChecker.numberType}},
@@ -52,7 +52,7 @@ struct RefinementClassFixture : Fixture
         };
         normalize(vec3, arena, *typeChecker.iceHandler);
 
-        TypeId inst = arena.addType(ClassTypeVar{"Instance", {}, std::nullopt, std::nullopt, {}, nullptr});
+        TypeId inst = arena.addType(ClassTypeVar{"Instance", {}, std::nullopt, std::nullopt, {}, nullptr, "Test"});
 
         TypePackId isAParams = arena.addTypePack({inst, typeChecker.stringType});
         TypePackId isARets = arena.addTypePack({typeChecker.booleanType});
@@ -66,9 +66,9 @@ struct RefinementClassFixture : Fixture
         };
         normalize(inst, arena, *typeChecker.iceHandler);
 
-        TypeId folder = typeChecker.globalTypes.addType(ClassTypeVar{"Folder", {}, inst, std::nullopt, {}, nullptr});
+        TypeId folder = typeChecker.globalTypes.addType(ClassTypeVar{"Folder", {}, inst, std::nullopt, {}, nullptr, "Test"});
         normalize(folder, arena, *typeChecker.iceHandler);
-        TypeId part = typeChecker.globalTypes.addType(ClassTypeVar{"Part", {}, inst, std::nullopt, {}, nullptr});
+        TypeId part = typeChecker.globalTypes.addType(ClassTypeVar{"Part", {}, inst, std::nullopt, {}, nullptr, "Test"});
         getMutable<ClassTypeVar>(part)->props = {
             {"Position", Property{vec3}},
         };

tests/TypeInfer.tables.test.cpp

@@ -2086,7 +2086,6 @@ caused by:
 TEST_CASE_FIXTURE(Fixture, "error_detailed_indexer_key")
 {
     ScopedFastFlag luauTableSubtypingVariance2{"LuauTableSubtypingVariance2", true}; // Only for new path
-    ScopedFastFlag luauExtendedIndexerError{"LuauExtendedIndexerError", true};
 
     CheckResult result = check(R"(
         type A = { [number]: string }
@@ -2105,7 +2104,6 @@ caused by:
 TEST_CASE_FIXTURE(Fixture, "error_detailed_indexer_value")
 {
     ScopedFastFlag luauTableSubtypingVariance2{"LuauTableSubtypingVariance2", true}; // Only for new path
-    ScopedFastFlag luauExtendedIndexerError{"LuauExtendedIndexerError", true};
 
     CheckResult result = check(R"(
         type A = { [number]: number }

tests/TypeInfer.test.cpp

@@ -86,16 +86,21 @@ TEST_CASE_FIXTURE(Fixture, "infer_locals_via_assignment_from_its_call_site")
 
 TEST_CASE_FIXTURE(Fixture, "infer_in_nocheck_mode")
 {
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+    };
+
     CheckResult result = check(R"(
         --!nocheck
         function f(x)
-            return x
+            return 5
         end
          -- we get type information even if there's type errors
         f(1, 2)
     )");
 
-    CHECK_EQ("(any) -> (...any)", toString(requireType("f")));
+    CHECK_EQ("(any) -> number", toString(requireType("f")));
 
     LUAU_REQUIRE_NO_ERRORS(result);
 }
@@ -363,6 +368,11 @@ TEST_CASE_FIXTURE(Fixture, "globals")
 
 TEST_CASE_FIXTURE(Fixture, "globals2")
 {
+    ScopedFastFlag sff[]{
+        {"LuauReturnTypeInferenceInNonstrict", true},
+        {"LuauLowerBoundsCalculation", true},
+    };
+
     CheckResult result = check(R"(
         --!nonstrict
         foo = function() return 1 end
@@ -373,9 +383,9 @@ TEST_CASE_FIXTURE(Fixture, "globals2")
 
     TypeMismatch* tm = get<TypeMismatch>(result.errors[0]);
     REQUIRE(tm);
-    CHECK_EQ("() -> (...any)", toString(tm->wantedType));
+    CHECK_EQ("() -> number", toString(tm->wantedType));
     CHECK_EQ("string", toString(tm->givenType));
-    CHECK_EQ("() -> (...any)", toString(requireType("foo")));
+    CHECK_EQ("() -> number", toString(requireType("foo")));
 }
 
 TEST_CASE_FIXTURE(Fixture, "globals_are_banned_in_strict_mode")

tests/TypeVar.test.cpp

@@ -275,7 +275,7 @@ TEST_CASE("tagging_tables")
 
 TEST_CASE("tagging_classes")
 {
-    TypeVar base{ClassTypeVar{"Base", {}, std::nullopt, std::nullopt, {}, nullptr}};
+    TypeVar base{ClassTypeVar{"Base", {}, std::nullopt, std::nullopt, {}, nullptr, "Test"}};
     CHECK(!Luau::hasTag(&base, "foo"));
     Luau::attachTag(&base, "foo");
     CHECK(Luau::hasTag(&base, "foo"));
@@ -283,8 +283,8 @@ TEST_CASE("tagging_classes")
 
 TEST_CASE("tagging_subclasses")
 {
-    TypeVar base{ClassTypeVar{"Base", {}, std::nullopt, std::nullopt, {}, nullptr}};
-    TypeVar derived{ClassTypeVar{"Derived", {}, &base, std::nullopt, {}, nullptr}};
+    TypeVar base{ClassTypeVar{"Base", {}, std::nullopt, std::nullopt, {}, nullptr, "Test"}};
+    TypeVar derived{ClassTypeVar{"Derived", {}, &base, std::nullopt, {}, nullptr, "Test"}};
 
     CHECK(!Luau::hasTag(&base, "foo"));
     CHECK(!Luau::hasTag(&derived, "foo"));