From 308649472d5a77a103791cc65131720e7c88138e Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Tue, 10 Mar 2026 17:58:24 -0300
Subject: [PATCH 1/8] Adding a check to avoid recursive type definitions

* This PR adds a check which do not allow the declaration of recursive
types (direct or indirect).
* Add new tests and changes some tests to failing due to the use of
recursive types.
---
 .../Frontend/TypeInference/TcContract.hs      | 51 +++++++++++++++++++
 test/Cases.hs                                 | 20 ++++----
 .../examples/cases/recursive-type-direct.solc |  9 ++++
 .../examples/cases/recursive-type-mutual.solc | 10 ++++
 4 files changed, 81 insertions(+), 9 deletions(-)
 create mode 100644 test/examples/cases/recursive-type-direct.solc
 create mode 100644 test/examples/cases/recursive-type-mutual.solc

diff --git a/src/Solcore/Frontend/TypeInference/TcContract.hs b/src/Solcore/Frontend/TypeInference/TcContract.hs
index ab6ecf69e..6bd79de80 100644
--- a/src/Solcore/Frontend/TypeInference/TcContract.hs
+++ b/src/Solcore/Frontend/TypeInference/TcContract.hs
@@ -1,5 +1,8 @@
 module Solcore.Frontend.TypeInference.TcContract where
 
+import Algebra.Graph.AdjacencyMap
+import Algebra.Graph.AdjacencyMap.Algorithm
+import Algebra.Graph.NonEmpty.AdjacencyMap qualified as NAG
 import Control.Monad
 import Control.Monad.Except
 import Control.Monad.State
@@ -8,6 +11,8 @@ import Data.List
 import Data.List.NonEmpty qualified as N
 import Data.Map qualified as Map
 import Data.Maybe
+import Data.Set (Set)
+import Data.Set qualified as Set
 import Solcore.Frontend.Pretty.ShortName
 import Solcore.Frontend.Pretty.SolcorePretty
 import Solcore.Frontend.Syntax
@@ -41,6 +46,7 @@ tcCompUnit (CompUnit imps cs) =
   do
     setupPragmas ps
     checkSynonymCycles syns
+    checkRecursiveTypes dts
     mapM_ checkTopDecl cls
     mapM_ checkTopDecl nonClassDecls
     typedDecls <- mapM tcTopDecl' cs
@@ -53,6 +59,7 @@ tcCompUnit (CompUnit imps cs) =
     isClass (TClassDef _) = True
     isClass _ = False
     syns = [s | TSym s <- cs]
+    dts = allDataTys cs
     tcTopDecl' d = timeItNamed (shortName d) $ do
       clearSubst
       tcTopDecl d
@@ -101,6 +108,50 @@ recursiveSynonymError cyclePath =
         "  " ++ intercalate " -> " (map pretty cyclePath)
       ]
 
+-- check for recursive data types
+
+allDataTys :: [TopDecl Name] -> [DataTy]
+allDataTys = concatMap collect
+  where
+    collect (TDataDef d) = [d]
+    collect (TContr (Contract _ _ cds)) = [d | CDataDecl d <- cds]
+    collect _ = []
+
+buildTypeDepsGraph :: Set Name -> [DataTy] -> AdjacencyMap Name
+buildTypeDepsGraph userTypes dts =
+  overlay isolated edged
+  where
+    isolated = vertices (Set.toList userTypes)
+    edged = stars [(dataName dt, deps dt) | dt <- dts]
+    deps (DataTy _ _ ctors) =
+      nub
+        . filter (`Set.member` userTypes)
+        . concatMap (\(Constr _ tys) -> concatMap tyNames tys)
+        $ ctors
+
+checkRecursiveTypes :: [DataTy] -> TcM ()
+checkRecursiveTypes dts =
+  case cyclicSccs of
+    [] -> pure ()
+    (c : _) -> recursiveTypeError (NAG.vertexList1 c)
+  where
+    userTypes = Set.fromList (map dataName dts)
+    graph = buildTypeDepsGraph userTypes dts
+    cyclicSccs = filter (isCyclic graph) (vertexList (scc graph))
+    isCyclic origGraph sccComp =
+      case N.toList (NAG.vertexList1 sccComp) of
+        [v] -> hasEdge v v origGraph -- singleton SCC: cyclic only if self-loop
+        _ -> True -- 2+ vertices: always a mutual cycle
+
+recursiveTypeError :: N.NonEmpty Name -> TcM a
+recursiveTypeError cycleVerts =
+  throwError $
+    unlines
+      [ "Recursive data type detected:",
+        "  " ++ intercalate ", " (map pretty (N.toList cycleVerts)),
+        "  (Data types must be non-recursive)"
+      ]
+
 -- setting up pragmas for type checking
 
 setupPragmas :: [Pragma] -> TcM ()
diff --git a/test/Cases.hs b/test/Cases.hs
index 9a5d1981c..045e7e7dd 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -102,7 +102,7 @@ pragmas =
   testGroup
     "Files for pragmas cases"
     [ runTestExpectingFailure "bound.solc" pragmaFolder,
-      runTestForFile "coverage.solc" pragmaFolder,
+      runTestExpectingFailure "coverage.solc" pragmaFolder,
       runTestForFile "patterson.solc" pragmaFolder
     ]
   where
@@ -112,7 +112,7 @@ cases :: TestTree
 cases =
   testGroup
     "Files for folder cases"
-    [ runTestForFile "Ackermann.solc" caseFolder,
+    [ runTestExpectingFailure "Ackermann.solc" caseFolder,
       runTestForFile "Add1.solc" caseFolder,
       runTestExpectingFailure "add-moritz.solc" caseFolder,
       runTestForFile "another-subst.solc" caseFolder,
@@ -152,12 +152,12 @@ cases =
       runTestExpectingFailure "duplicated-type-name.solc" caseFolder,
       runTestForFile "DuplicateFun.solc" caseFolder,
       runTestExpectingFailure "DupFun.solc" caseFolder,
-      runTestForFile "EitherModule.solc" caseFolder,
+      runTestExpectingFailure "EitherModule.solc" caseFolder,
       runTestForFile "empty-asm.solc" caseFolder,
       runTestExpectingFailure "Enum.solc" caseFolder,
       runTestExpectingFailure "Eq.solc" caseFolder,
       runTestForFile "EqQual.solc" caseFolder,
-      runTestForFile "EvenOdd.solc" caseFolder,
+      runTestExpectingFailure "EvenOdd.solc" caseFolder,
       runTestExpectingFailure "Filter.solc" caseFolder,
       runTestForFile "foo-class.solc" caseFolder,
       runTestForFile "Foo.solc" caseFolder,
@@ -177,8 +177,8 @@ cases =
       runTestExpectingFailure "joinErr.solc" caseFolder,
       runTestExpectingFailure "KindTest.solc" caseFolder,
       runTestExpectingFailure "listeq.solc" caseFolder,
-      runTestForFile "ListModule.solc" caseFolder,
-      runTestForFile "listid.solc" caseFolder,
+      runTestExpectingFailure "ListModule.solc" caseFolder,
+      runTestExpectingFailure "listid.solc" caseFolder,
       runTestForFile "Logic.solc" caseFolder,
       runTestExpectingFailure "mainproxy.solc" caseFolder,
       runTestForFile "MatchCall.solc" caseFolder,
@@ -204,8 +204,8 @@ cases =
       runTestExpectingFailure "PairMatch2.solc" caseFolder,
       -- failing due to missing assign constraint
       runTestExpectingFailure "patterson-bug.solc" caseFolder,
-      runTestForFile "Peano.solc" caseFolder,
-      runTestForFile "PeanoMatch.solc" caseFolder,
+      runTestExpectingFailure "Peano.solc" caseFolder,
+      runTestExpectingFailure "PeanoMatch.solc" caseFolder,
       runTestForFile "polymatch-error.solc" caseFolder,
       runTestExpectingFailure "pragma_merge_fail_coverage.solc" caseFolder,
       runTestExpectingFailure "pragma_merge_fail_patterson.solc" caseFolder,
@@ -216,6 +216,8 @@ cases =
       runTestForFile "proxy.solc" caseFolder,
       runTestExpectingFailure "proxy1.solc" caseFolder,
       runTestForFile "rec.solc" caseFolder,
+      runTestExpectingFailure "recursive-type-direct.solc" caseFolder,
+      runTestExpectingFailure "recursive-type-mutual.solc" caseFolder,
       runTestExpectingFailure "Ref.solc" caseFolder,
       runTestForFile "RefDeref.solc" caseFolder,
       runTestExpectingFailure "reference.solc" caseFolder,
@@ -248,7 +250,7 @@ cases =
       runTestExpectingFailure "subject-index.solc" caseFolder,
       runTestExpectingFailure "subject-reduction.solc" caseFolder,
       runTestExpectingFailure "subsumption-test.solc" caseFolder,
-      runTestForFile "super-class.solc" caseFolder,
+      runTestExpectingFailure "super-class.solc" caseFolder,
       runTestForFile "super-class-num.solc" caseFolder,
       runTestForFile "tiamat.solc" caseFolder,
       runTestForFile "tuple-trick.solc" caseFolder,
diff --git a/test/examples/cases/recursive-type-direct.solc b/test/examples/cases/recursive-type-direct.solc
new file mode 100644
index 000000000..ff180526c
--- /dev/null
+++ b/test/examples/cases/recursive-type-direct.solc
@@ -0,0 +1,9 @@
+-- Direct recursion: Nat refers to itself in the Succ constructor.
+-- Expected: type checker rejects with "Recursive data type detected".
+data Nat = Zero | Succ(Nat);
+
+contract RecursiveTypeDirect {
+  function main() -> Nat {
+    Zero
+  }
+}
diff --git a/test/examples/cases/recursive-type-mutual.solc b/test/examples/cases/recursive-type-mutual.solc
new file mode 100644
index 000000000..8b4452438
--- /dev/null
+++ b/test/examples/cases/recursive-type-mutual.solc
@@ -0,0 +1,10 @@
+-- Mutual recursion: Even refers to Odd and Odd refers to Even.
+-- Expected: type checker rejects with "Recursive data type detected".
+data Even = Zero | SuccE(Odd);
+data Odd  = SuccO(Even);
+
+contract RecursiveTypeMutual {
+  function main() -> Even {
+    Zero
+  }
+}

From 2a7a4dca13ed0e9b8f407933ab5fa6e30daf57b9 Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Wed, 11 Mar 2026 17:21:10 -0300
Subject: [PATCH 2/8] Fixing by allowing recursion through phantom type
 arguments.

* New test added.
---
 .../Frontend/TypeInference/TcContract.hs      | 28 ++++++++++++++++++-
 test/Cases.hs                                 |  1 +
 test/examples/cases/rec-memory.solc           |  3 ++
 3 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 test/examples/cases/rec-memory.solc

diff --git a/src/Solcore/Frontend/TypeInference/TcContract.hs b/src/Solcore/Frontend/TypeInference/TcContract.hs
index 6bd79de80..7a9aa29bd 100644
--- a/src/Solcore/Frontend/TypeInference/TcContract.hs
+++ b/src/Solcore/Frontend/TypeInference/TcContract.hs
@@ -117,16 +117,42 @@ allDataTys = concatMap collect
     collect (TContr (Contract _ _ cds)) = [d | CDataDecl d <- cds]
     collect _ = []
 
+tyVarNames :: Ty -> [Name]
+tyVarNames (TyVar tv) = [tyvarName tv]
+tyVarNames (TyCon _ ts) = concatMap tyVarNames ts
+tyVarNames _ = []
+
+buildPhantomMap :: [DataTy] -> Map.Map Name (Set Int)
+buildPhantomMap = Map.fromList . map phantomEntry
+  where
+    phantomEntry (DataTy n params ctors) =
+      let allFieldTys = concatMap constrTy ctors
+          usedVarNames = concatMap tyVarNames allFieldTys
+          isPhantomParam p = tyvarName p `notElem` usedVarNames
+          phantomIdxs = Set.fromList [i | (i, p) <- zip [0 ..] params, isPhantomParam p]
+       in (n, phantomIdxs)
+
+nonPhantomTyNames :: Map.Map Name (Set Int) -> Ty -> [Name]
+nonPhantomTyNames phantomMap (TyCon n args) =
+  n : concatMap processArg (zip [0 ..] args)
+  where
+    phantomIdxs = Map.findWithDefault Set.empty n phantomMap
+    processArg (i, arg)
+      | Set.member i phantomIdxs = []
+      | otherwise = nonPhantomTyNames phantomMap arg
+nonPhantomTyNames _ _ = []
+
 buildTypeDepsGraph :: Set Name -> [DataTy] -> AdjacencyMap Name
 buildTypeDepsGraph userTypes dts =
   overlay isolated edged
   where
+    phantomMap = buildPhantomMap dts
     isolated = vertices (Set.toList userTypes)
     edged = stars [(dataName dt, deps dt) | dt <- dts]
     deps (DataTy _ _ ctors) =
       nub
         . filter (`Set.member` userTypes)
-        . concatMap (\(Constr _ tys) -> concatMap tyNames tys)
+        . concatMap (\(Constr _ tys) -> concatMap (nonPhantomTyNames phantomMap) tys)
         $ ctors
 
 checkRecursiveTypes :: [DataTy] -> TcM ()
diff --git a/test/Cases.hs b/test/Cases.hs
index 045e7e7dd..ab80af49b 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -190,6 +190,7 @@ cases =
       runTestForFile "modifier.solc" caseFolder,
       runTestForFile "morefun.solc" caseFolder,
       runTestForFile "Mutuals.solc" caseFolder,
+      runTestForFile "rec-memory.solc" caseFolder,
       runTestExpectingFailure "nano-desugared.solc" caseFolder,
       runTestForFile "NegPair.solc" caseFolder,
       runTestForFile "nid.solc" caseFolder,
diff --git a/test/examples/cases/rec-memory.solc b/test/examples/cases/rec-memory.solc
new file mode 100644
index 000000000..f3807c4f6
--- /dev/null
+++ b/test/examples/cases/rec-memory.solc
@@ -0,0 +1,3 @@
+data memory(a) = memory(word);
+
+data List(a) = Nil | Cons(a, memory(List(a)));

From d5ef74182c38962ebc7f4ab192ca8db78e68170d Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Thu, 12 Mar 2026 13:16:23 -0300
Subject: [PATCH 3/8] Fixing test cases.

---
 test/Cases.hs                         |  6 +++---
 test/examples/cases/Ackermann.solc    |  4 +++-
 test/examples/cases/EitherModule.solc | 22 ++++++++++++++++++----
 test/examples/pragmas/coverage.solc   |  4 +++-
 4 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/test/Cases.hs b/test/Cases.hs
index ab80af49b..45d9c0676 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -102,7 +102,7 @@ pragmas =
   testGroup
     "Files for pragmas cases"
     [ runTestExpectingFailure "bound.solc" pragmaFolder,
-      runTestExpectingFailure "coverage.solc" pragmaFolder,
+      runTestForFile "coverage.solc" pragmaFolder,
       runTestForFile "patterson.solc" pragmaFolder
     ]
   where
@@ -112,7 +112,7 @@ cases :: TestTree
 cases =
   testGroup
     "Files for folder cases"
-    [ runTestExpectingFailure "Ackermann.solc" caseFolder,
+    [ runTestForFile "Ackermann.solc" caseFolder,
       runTestForFile "Add1.solc" caseFolder,
       runTestExpectingFailure "add-moritz.solc" caseFolder,
       runTestForFile "another-subst.solc" caseFolder,
@@ -152,7 +152,7 @@ cases =
       runTestExpectingFailure "duplicated-type-name.solc" caseFolder,
       runTestForFile "DuplicateFun.solc" caseFolder,
       runTestExpectingFailure "DupFun.solc" caseFolder,
-      runTestExpectingFailure "EitherModule.solc" caseFolder,
+      runTestForFile "EitherModule.solc" caseFolder,
       runTestForFile "empty-asm.solc" caseFolder,
       runTestExpectingFailure "Enum.solc" caseFolder,
       runTestExpectingFailure "Eq.solc" caseFolder,
diff --git a/test/examples/cases/Ackermann.solc b/test/examples/cases/Ackermann.solc
index 5c413dc50..5d1946e03 100644
--- a/test/examples/cases/Ackermann.solc
+++ b/test/examples/cases/Ackermann.solc
@@ -1,4 +1,6 @@
-data Nat = Zero | Succ(Nat) ;
+data memory(a) = memory(word);
+
+data Nat = Zero | Succ(memory(Nat)) ;
 
 function foo (x, y) {
   match y, x {
diff --git a/test/examples/cases/EitherModule.solc b/test/examples/cases/EitherModule.solc
index 2b0845d83..720f5e776 100644
--- a/test/examples/cases/EitherModule.solc
+++ b/test/examples/cases/EitherModule.solc
@@ -1,16 +1,30 @@
 contract EitherModule {
+  data memory(a) = memory(word);
   data Either(a,b) = Left(a) | Right(b);
-  data List(a) = Nil | Cons(a,List(a));
+  data List(a) = Nil | Cons(a, memory(List(a)));
 
-  function lefts(xs) {
+  forall a b . function lefts(xs : List (Either(a,b))) -> List(a) {
     match xs {
     | Nil => return Nil ;
     | Cons(y,ys) =>
       match y {
-      | Left(z) => return Cons(z,lefts(ys)) ;
-      | Right(z) => return lefts(ys) ;
+      | Left(z) => return Cons(z,storeList(lefts(loadList(ys)))) ;
+      | Right(z) => return lefts(loadList(ys)) ;
       }
     }
   }
 
+  forall a . function loadList(xs : memory(List(a))) -> List(a) {
+    match xs {
+    | memory(_) => return Nil ;
+    }
+  }
+
+  forall a . function storeList (xs : List(a)) -> memory(List(a)) {
+    return memory(0);
+  }
+
+  function main () -> word {
+    return 42;
+  }
 }
diff --git a/test/examples/pragmas/coverage.solc b/test/examples/pragmas/coverage.solc
index c412dc914..62f2ba545 100644
--- a/test/examples/pragmas/coverage.solc
+++ b/test/examples/pragmas/coverage.solc
@@ -1,6 +1,8 @@
 pragma no-coverage-condition ;
 
-data List(a) = Nil | Cons(a,List(a));
+data memory(a) = memory(word);
+
+data List(a) = Nil | Cons(a,memory(List(a)));
 data Bool = True | False ;
 
 forall a b c . class a : C(b,c) {}

From 646f451a33ee693e17a7000b7009dd0dd365e3ae Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Mon, 16 Mar 2026 14:27:09 -0300
Subject: [PATCH 4/8] Fixes on recursive check on types

* Adding an example suggested by Y-Nak.
---
 .../Frontend/TypeInference/TcContract.hs      | 33 ++++++++++++++++---
 test/Cases.hs                                 |  3 +-
 test/examples/cases/box.solc                  |  3 ++
 3 files changed, 34 insertions(+), 5 deletions(-)
 create mode 100644 test/examples/cases/box.solc

diff --git a/src/Solcore/Frontend/TypeInference/TcContract.hs b/src/Solcore/Frontend/TypeInference/TcContract.hs
index 7a9aa29bd..1d91489be 100644
--- a/src/Solcore/Frontend/TypeInference/TcContract.hs
+++ b/src/Solcore/Frontend/TypeInference/TcContract.hs
@@ -122,13 +122,38 @@ tyVarNames (TyVar tv) = [tyvarName tv]
 tyVarNames (TyCon _ ts) = concatMap tyVarNames ts
 tyVarNames _ = []
 
+-- Collect type variable names that appear in non-phantom argument positions.
+-- Phantom positions (indices in the map for the head type constructor) are skipped.
+nonPhantomVarNames :: Map.Map Name (Set Int) -> Ty -> [Name]
+nonPhantomVarNames m (TyCon n args) =
+  let phantomIdxs = Map.findWithDefault Set.empty n m
+   in concatMap
+        (\(i, arg) ->
+          if Set.member i phantomIdxs then [] else nonPhantomVarNames m arg)
+        (zip [0 ..] args)
+nonPhantomVarNames _ (TyVar v) = [tyvarName v]
+nonPhantomVarNames _ _ = []
+
+-- Build the phantom-parameter map using fixpoint iteration so that
+-- transitively-phantom positions are discovered.  A parameter at index i of
+-- type T is phantom when it never appears in a non-phantom position across all
+-- constructor field types (using the current map to decide what counts as
+-- non-phantom).  Starting from the empty map and iterating monotonically to a
+-- fixpoint ensures that every position that can be proved phantom eventually is.
 buildPhantomMap :: [DataTy] -> Map.Map Name (Set Int)
-buildPhantomMap = Map.fromList . map phantomEntry
+buildPhantomMap dts = fixpoint initial
   where
-    phantomEntry (DataTy n params ctors) =
+    initial = Map.fromList [(dataName dt, Set.empty) | dt <- dts]
+
+    fixpoint m =
+      let m' = Map.fromList (map (refineEntry m) dts)
+       in if m == m' then m else fixpoint m'
+
+    refineEntry m (DataTy n params ctors) =
       let allFieldTys = concatMap constrTy ctors
-          usedVarNames = concatMap tyVarNames allFieldTys
-          isPhantomParam p = tyvarName p `notElem` usedVarNames
+          isPhantomParam p =
+            let pName = tyvarName p
+             in all (\ty -> pName `notElem` nonPhantomVarNames m ty) allFieldTys
           phantomIdxs = Set.fromList [i | (i, p) <- zip [0 ..] params, isPhantomParam p]
        in (n, phantomIdxs)
 
diff --git a/test/Cases.hs b/test/Cases.hs
index 45d9c0676..1401fd554 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -291,7 +291,8 @@ cases =
       runTestForFile "field-name-error.solc" caseFolder,
       runTestExpectingFailure "field-access.solc" caseFolder,
       runTestForFile "mod-example.solc" caseFolder,
-      runTestForFile "proxy-desugar.solc" caseFolder
+      runTestForFile "proxy-desugar.solc" caseFolder,
+      runTestForFile "box.solc" caseFolder
     ]
   where
     caseFolder = "./test/examples/cases"
diff --git a/test/examples/cases/box.solc b/test/examples/cases/box.solc
new file mode 100644
index 000000000..060928a85
--- /dev/null
+++ b/test/examples/cases/box.solc
@@ -0,0 +1,3 @@
+data memory(a) = memory(word);
+data Box(a) = Box(memory(a));
+data Rec = Rec(Box(Rec));

From 9854d924041890cd64bda1bd3525077d13a27c35 Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Mon, 16 Mar 2026 14:37:56 -0300
Subject: [PATCH 5/8] Ormulu format.

---
 src/Solcore/Frontend/TypeInference/TcContract.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Solcore/Frontend/TypeInference/TcContract.hs b/src/Solcore/Frontend/TypeInference/TcContract.hs
index 1d91489be..26ff3d890 100644
--- a/src/Solcore/Frontend/TypeInference/TcContract.hs
+++ b/src/Solcore/Frontend/TypeInference/TcContract.hs
@@ -128,8 +128,9 @@ nonPhantomVarNames :: Map.Map Name (Set Int) -> Ty -> [Name]
 nonPhantomVarNames m (TyCon n args) =
   let phantomIdxs = Map.findWithDefault Set.empty n m
    in concatMap
-        (\(i, arg) ->
-          if Set.member i phantomIdxs then [] else nonPhantomVarNames m arg)
+        ( \(i, arg) ->
+            if Set.member i phantomIdxs then [] else nonPhantomVarNames m arg
+        )
         (zip [0 ..] args)
 nonPhantomVarNames _ (TyVar v) = [tyvarName v]
 nonPhantomVarNames _ _ = []

From 9c2b92043dec504c18dd20123f0f65ff83a7f02c Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Sun, 19 Apr 2026 18:41:48 -0300
Subject: [PATCH 6/8] Fixes suggested by YNak

---
 src/Solcore/Frontend/TypeInference/TcContract.hs |  8 +++++---
 src/Solcore/Frontend/TypeInference/TcMonad.hs    | 12 ++++++++++++
 test/Cases.hs                                    |  4 +++-
 test/examples/cases/constructors-contract.solc   |  9 +++++++++
 test/examples/cases/synonym-example.solc         |  3 +++
 5 files changed, 32 insertions(+), 4 deletions(-)
 create mode 100644 test/examples/cases/constructors-contract.solc
 create mode 100644 test/examples/cases/synonym-example.solc

diff --git a/src/Solcore/Frontend/TypeInference/TcContract.hs b/src/Solcore/Frontend/TypeInference/TcContract.hs
index a275a9d3a..6b1431ad0 100644
--- a/src/Solcore/Frontend/TypeInference/TcContract.hs
+++ b/src/Solcore/Frontend/TypeInference/TcContract.hs
@@ -96,9 +96,10 @@ tcTopDeclChecks topDeclChecks =
   do
     setupPragmas ps
     checkSynonymCycles syns
-    checkRecursiveTypes dts
     let st = buildSynTable syns
     csExpanded <- everywhereM (mkM (expandTyM st)) cs
+    checkRecursiveTypes (topLevelDts csExpanded)
+    mapM_ checkRecursiveTypes (perContractDts csExpanded)
     mapM_ checkTopDecl (filter isClass csExpanded)
     mapM_ checkTopDecl (filter (not . isClass) csExpanded)
     trustImportedDecls csExpanded
@@ -111,7 +112,6 @@ tcTopDeclChecks topDeclChecks =
     isClass (TClassDef _) = True
     isClass _ = False
     syns = [s | TSym s <- cs]
-    dts = allDataTys cs
     trustImportedDecls expandedDecls =
       mapM_
         (withPartialDataTypesDisabled . trustImportedTopDecl)
@@ -126,6 +126,8 @@ tcTopDeclChecks topDeclChecks =
         TrustTopDeclBody ->
           withPartialDataTypesDisabled $
             pure Nothing
+    topLevelDts cs' = [d | TDataDef d <- cs']
+    perContractDts cs' = [[d | CDataDecl d <- cds] | TContr (Contract _ _ cds) <- cs']
     tcTopDecl' d = timeItNamed (shortName d) $ do
       clearSubst
       tcTopDecl d
@@ -367,7 +369,7 @@ checkTopDecl _ = pure ()
 
 tcContract :: Contract Name -> TcM (Contract Id, [(Name, Scheme)])
 tcContract c@(Contract n vs cdecls) =
-  withLocalEnv $ withContractName n $ do
+  withLocalContractEnv $ withContractName n $ do
     ctx' <- gets ctx
     initializeEnv c
     decls' <- mapM tcDecl' cdecls
diff --git a/src/Solcore/Frontend/TypeInference/TcMonad.hs b/src/Solcore/Frontend/TypeInference/TcMonad.hs
index e44176cbe..33006a3bf 100644
--- a/src/Solcore/Frontend/TypeInference/TcMonad.hs
+++ b/src/Solcore/Frontend/TypeInference/TcMonad.hs
@@ -417,6 +417,18 @@ withLocalEnv ta =
     putEnv savedCtx
     pure a
 
+-- Like withLocalEnv but also restores the typeTable, for contract scopes
+-- where data type names must not leak between sibling contracts.
+withLocalContractEnv :: TcM a -> TcM a
+withLocalContractEnv ta =
+  do
+    savedCtx   <- gets ctx
+    savedTypes <- gets typeTable
+    a <- ta
+    putEnv savedCtx
+    modify (\env -> env {typeTable = savedTypes})
+    pure a
+
 envList :: TcM [(Name, Scheme)]
 envList = gets (Map.toList . ctx)
 
diff --git a/test/Cases.hs b/test/Cases.hs
index 35824b0f0..1569f25f7 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -243,6 +243,7 @@ cases =
       runTestForFile "const.solc" caseFolder,
       runTestExpectingFailure "const-array.solc" caseFolder,
       runTestForFile "constructor-weak-args.solc" caseFolder,
+      runTestForFile "constructors-contract.solc" caseFolder,
       runTestExpectingFailure "complexproxy.solc" caseFolder,
       runTestForFile "cyclical-defs.solc" caseFolder,
       runTestForFile "cyclical-defs-inferred.solc" caseFolder,
@@ -454,7 +455,8 @@ cases =
       runTestForFile "ltimp.solc" caseFolder,
       runTestExpectingFailure "class-return-type-miss.solc" caseFolder,
       runTestExpectingFailure "catenable-err.solc" caseFolder,
-      runTestForFile "pars.solc" caseFolder
+      runTestForFile "pars.solc" caseFolder,
+      runTestExpectingFailure "synonym-example.solc" caseFolder
     ]
   where
     caseFolder = "./test/examples/cases"
diff --git a/test/examples/cases/constructors-contract.solc b/test/examples/cases/constructors-contract.solc
new file mode 100644
index 000000000..6ea5bd923
--- /dev/null
+++ b/test/examples/cases/constructors-contract.solc
@@ -0,0 +1,9 @@
+contract A {
+  data T = MkT(U);
+  data U = MkU(word);
+}
+
+contract B {
+  data T = MkT2(word);
+  data U = MkU2(T);
+}
diff --git a/test/examples/cases/synonym-example.solc b/test/examples/cases/synonym-example.solc
new file mode 100644
index 000000000..bae9ff259
--- /dev/null
+++ b/test/examples/cases/synonym-example.solc
@@ -0,0 +1,3 @@
+
+type Ref = T;
+data T = Mk(Ref);

From 6e1959d7b45b15ef338975a0da897c99ce96c276 Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Sun, 19 Apr 2026 18:51:19 -0300
Subject: [PATCH 7/8] Ormolu formatting.

---
 src/Solcore/Frontend/TypeInference/TcMonad.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Solcore/Frontend/TypeInference/TcMonad.hs b/src/Solcore/Frontend/TypeInference/TcMonad.hs
index 33006a3bf..0b7bdee83 100644
--- a/src/Solcore/Frontend/TypeInference/TcMonad.hs
+++ b/src/Solcore/Frontend/TypeInference/TcMonad.hs
@@ -422,7 +422,7 @@ withLocalEnv ta =
 withLocalContractEnv :: TcM a -> TcM a
 withLocalContractEnv ta =
   do
-    savedCtx   <- gets ctx
+    savedCtx <- gets ctx
     savedTypes <- gets typeTable
     a <- ta
     putEnv savedCtx

From 186e3e14d432f6f49e150b1285b69a25c32a3c5e Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Wed, 3 Jun 2026 07:27:02 -0300
Subject: [PATCH 8/8] Fixing test cases

---
 test/Cases.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Cases.hs b/test/Cases.hs
index 1569f25f7..58a46359b 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -264,7 +264,7 @@ cases =
       runTestExpectingFailure "duplicated-type-name.solc" caseFolder,
       runTestForFile "DuplicateFun.solc" caseFolder,
       runTestExpectingFailure "DupFun.solc" caseFolder,
-      runTestForFile "EitherModule.solc" caseFolder,
+      runTestExpectingFailure "EitherModule.solc" caseFolder,
       runTestForFile "empty-asm.solc" caseFolder,
       runTestExpectingFailure "Enum.solc" caseFolder,
       runTestExpectingFailure "Eq.solc" caseFolder,