From 655400b9236b3606bc0879e7257c814d68ae0b6b Mon Sep 17 00:00:00 2001
From: Kevin Barabash <kevinb7@gmail.com>
Date: Sun, 11 Aug 2024 16:24:48 -0400
Subject: [PATCH] Add test case to check that intersection with exact types is
 'never' (#336)

---
 src/Escalier.TypeChecker.Tests/Exact.fs | 27 ++++++++++++++++++++++++-
 src/Escalier.TypeChecker/Infer.fs       | 13 ++++++------
 src/Escalier.TypeChecker/Unify.fs       |  6 ++++++
 3 files changed, 39 insertions(+), 7 deletions(-)

diff --git a/src/Escalier.TypeChecker.Tests/Exact.fs b/src/Escalier.TypeChecker.Tests/Exact.fs
index 4ceb424..7eb8e1e 100644
--- a/src/Escalier.TypeChecker.Tests/Exact.fs
+++ b/src/Escalier.TypeChecker.Tests/Exact.fs
@@ -187,7 +187,7 @@ let InexactMappedTypesPreserveExactness () =
 
   Assert.False(Result.isError res)
 
-
+[<Fact>]
 let ExactMappedTypesPreserveExactness () =
   let res =
     result {
@@ -225,3 +225,28 @@ let ExactMappedTypesPreserveExactness () =
     }
 
   Assert.False(Result.isError res)
+
+[<Fact>]
+let IntersectionOfExactTypesIsNever () =
+  let res =
+    result {
+      let src =
+        """
+        type Foo = {foo: string};
+        type Bar = {bar: number, ...};
+        
+        type FooAndBar = Foo & Bar;
+        """
+
+      let! ctx, env = inferModule src
+
+      Assert.Empty(ctx.Report.Diagnostics)
+
+      let! t =
+        expandScheme ctx env None (env.FindScheme "FooAndBar") Map.empty None
+        |> Result.mapError CompileError.TypeError
+
+      Assert.Equal(t.ToString(), "never")
+    }
+
+  Assert.False(Result.isError res)
diff --git a/src/Escalier.TypeChecker/Infer.fs b/src/Escalier.TypeChecker/Infer.fs
index 106ee14..c08aeec 100644
--- a/src/Escalier.TypeChecker/Infer.fs
+++ b/src/Escalier.TypeChecker/Infer.fs
@@ -2242,10 +2242,6 @@ module rec Infer =
     result {
       let mutable patternTypes = []
 
-      // TODO: do two passes
-      // 1. unify all of the patterns with `exprType`
-      // 2. infer the types of all of the bodies
-
       // Infer all pattern types
       let! assumps =
         List.traverseResultM
@@ -2259,8 +2255,13 @@ module rec Infer =
 
       let mutable newExprTypes: list<Type> = []
 
-      // TODO: check mutability when unifying by computing invariant paths
-      // using checkMutability
+      // TODO(#335): Check mutability when unifying by computing invariant paths
+      // using checkMutability.
+
+      // TODO(#332): Prevent pattern matching of unions of untagged inexact object
+      // types. Untagged inexact object types can have extra properties that we
+      // can't account for that could result in a different pattern being matched
+      // than the intended one.
 
       // NOTE: the direction of assignability for patternType and exprType is
       // reversed.  This is because the type of the expression being assigned is
diff --git a/src/Escalier.TypeChecker/Unify.fs b/src/Escalier.TypeChecker/Unify.fs
index 719e6fa..e57b0e0 100644
--- a/src/Escalier.TypeChecker/Unify.fs
+++ b/src/Escalier.TypeChecker/Unify.fs
@@ -1591,6 +1591,12 @@ module rec Unify =
               { Kind = TypeKind.Intersection types
                 Provenance = None }
           else if hasExactObjects then
+            // The intersection of exact types is never unless the types are
+            // exactly the same.  Checking if two object types are exactly the
+            // same is expensive so we just return `never` for now.  Spread
+            // types should be used instead of intersection types when working
+            // with object types since it actually corresponds to a real value-
+            // level operation.
             return
               { Kind = TypeKind.Keyword Keyword.Never
                 Provenance = None }