From 53f62db4c299914d2dab4f3e614beb412dc53c1e Mon Sep 17 00:00:00 2001
From: jsonch <jsonch@seas.upenn.edu>
Date: Tue, 27 Aug 2024 11:59:48 -0400
Subject: [PATCH] properly fixed longstanding bug in typer related to records
 and list expressions that contained projections and get operations.

---
 src/lib/frontend/typing/Typer.ml      | 23 +++++++++++++----------
 src/lib/frontend/typing/TyperUnify.ml | 10 ++++++++++
 2 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/src/lib/frontend/typing/Typer.ml b/src/lib/frontend/typing/Typer.ml
index 5506b9d5..85402d03 100644
--- a/src/lib/frontend/typing/Typer.ml
+++ b/src/lib/frontend/typing/Typer.ml
@@ -254,18 +254,21 @@ let rec infer_exp (env : env) (e : exp) : env * exp =
             e'.espan
             "Cannot dynamically create tuples containing global types"
         else (
-          (* WARNING: This is a hack that needs to be fixed if users can write tuples. 
-              If we have a tuple that contains a get operation to another tuple, 
-              the effect of the get op will be a projection to the element 
-              of the inner tuple. In the current representation I don't think there's a 
-              way to unify something like "the effect of the 5th element of the outer tuple is 
-              equal to the 2nd element of some other tuple". And expressions like this can 
-              be generated by the compiler -- e.g., when recordElimination turns records 
-              into tuples. *)
-          let expected = match (e'.e) with 
+          (* This commented out code was a workaround to get unification to work 
+             for tuple expressions that contained elements from other tuples. 
+             The problem was that: tup foo = (bar.1, bar.2)  failed to unify, 
+             because it tried to unify the effect of foo.0 with bar.1, and there 
+             so it ended up trying to unify FSucc(FProj()) with FProj()
+            The solution was to add a case in TyperUnify.try_unify_effect: 
+                | FProj(FVar(tqv)), eff | eff, FProj(FVar(tqv)) -> ...
+            This solves the problem because in such a case, one of the sides 
+            is going to be a variable. And it is safe because projecting 
+            does not have an effect itself. *)
+          (* let expected = match (e'.e) with 
             | EOp(TGet(_, idx), _) -> wrap_effect tuple_eff [None, 0; None, idx]
             | _ -> wrap_effect tuple_eff [None, 0; None, i] 
-          in
+          in *)
+          let expected = wrap_effect tuple_eff [None, 0; None, i] in
           let derived = (Option.get e'.ety).teffect in           
           unify_effect e.espan expected derived
         )
diff --git a/src/lib/frontend/typing/TyperUnify.ml b/src/lib/frontend/typing/TyperUnify.ml
index 2abbda53..f9b8baee 100644
--- a/src/lib/frontend/typing/TyperUnify.ml
+++ b/src/lib/frontend/typing/TyperUnify.ml
@@ -210,6 +210,16 @@ let rec try_unify_effect span eff1 eff2 =
         eff
     | FZero, FZero -> ()
     | FSucc eff1, FSucc eff2 | FProj eff1, FProj eff2 -> try_unify eff1 eff2
+    (* unwrap a projection of a variable, because projection itself does not change effect *)
+    (* note: this has to come after the base FProj case. *)
+    | FProj(FVar(tqv)), eff | eff, FProj(FVar(tqv)) -> 
+      try_unify_tqvar
+        (occurs_effect span)
+        try_unify
+        FTQVar.phys_equiv_tqvar
+        tqv
+        eff
+
     | FIndex (id1, eff1), FIndex (id2, eff2) ->
       if not (Id.equal id1 id2) then raise CannotUnify else try_unify eff1 eff2
     | (FZero | FSucc _ | FProj _ | FIndex _), _ -> raise CannotUnify)