Adding a check to avoid recursive type definitions

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,76 @@ 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 _ = []
+
+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 (nonPhantomTyNames phantomMap) 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 ()

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,
@@ -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,
@@ -204,8 +205,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 +217,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 +251,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,

test/examples/cases/rec-memory.solc

@@ -0,0 +1,3 @@
+data memory(a) = memory(word);
+
+data List(a) = Nil | Cons(a, memory(List(a)));

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
+  }
+}

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
+  }
+}