BUGFIX: Prevent infinite loop in constraint solver.

docs/Todo.org

@@ -6,7 +6,7 @@
 * Unsorted Todo:s
 * Critical Bugs
 ** 0.3
-*** Defining a local variable messes up unqualified lookup of function with the same name, e.g. (let [words (words &s)] ...). Infinite loop now!
+*** Defining a local variable messes up unqualified lookup of function with the same name, e.g. (let [words (words &s)] ...)
 *** References must keep track of their origin and prevent usage of them if the origin has been given away.
     Currently it's possible to set a ref so it points to a value in a more short-lived scope, leads to 'stack-use-after-scope' error in clang-sanitizer.
 *** Can't define '=' in terms of '=' on generic members of type, see Pair.=

examples/bugs.carp

@@ -45,7 +45,9 @@
 ;;       (set! r &xs))
 ;;     (println* r)))
 
-(defn f [] (the t0 123))
+;; Local name in 'let' shadows other symbols
+(defn shadow [] 123)
 
-(defn main []
-  (f))
+(defn f []
+  (let [shadow (shadow)]
+    ()))

src/Constraints.hs

@@ -16,6 +16,10 @@ import Obj
 import Types
 
 data ConstraintOrder = OrdNo
+                     | OrdFunc
+                     | OrdStruct
+                     | OrdPtr
+                     | OrdRef
                      | OrdFuncAppRet
                      | OrdArrHead
                      | OrdArg
@@ -98,7 +102,7 @@ debugSolveOne mappings constraint = let m' = solveOneInternal mappings constrain
 
 solveOneInternal :: TypeMappings -> Constraint -> Either UnificationFailure TypeMappings
 solveOneInternal mappings constraint =
-  case constraint of
+  case constraint of --trace ("SOLVE " ++ show constraint) constraint of
     -- Two type variables
     Constraint aTy@(VarTy aName) bTy@(VarTy bName) _ _ _ ->
       if aTy == bTy
@@ -142,51 +146,55 @@ solveOneInternal mappings constraint =
       then Right mappings
       else Left (UnificationFailure constraint mappings)
 
-mkConstraint :: XObj -> XObj -> Ty -> Ty -> Constraint
-mkConstraint xobj1 xobj2 t1 t2 = Constraint t1 t2 xobj1 xobj2 OrdNo
+mkConstraint :: ConstraintOrder -> XObj -> XObj -> Ty -> Ty -> Constraint
+mkConstraint order xobj1 xobj2 t1 t2 = Constraint t1 t2 xobj1 xobj2 order
 
 checkForConflict :: TypeMappings -> Constraint -> String -> Ty -> Either UnificationFailure TypeMappings
 checkForConflict mappings constraint name otherTy =
   let (Constraint _ _ xobj1 xobj2 _) = constraint
+      found = recursiveLookup mappings name
   in
-  case recursiveLookup mappings name of
-    Just (VarTy _) -> ok
-    Just (StructTy structName structTyVars) ->
-      case otherTy of
-        StructTy otherStructName otherTyVars | structName == otherStructName ->
-                                               foldM solveOneInternal mappings (zipWith (mkConstraint xobj1 xobj2) structTyVars otherTyVars)
-        VarTy _ -> Right mappings
-        _ -> Left (UnificationFailure constraint mappings)
-    Just (FuncTy argTys retTy) ->
-      case otherTy of
-        FuncTy otherArgTys otherRetTy -> do m <- foldM solveOneInternal mappings (zipWith (mkConstraint xobj1 xobj2) argTys otherArgTys)
-                                            solveOneInternal m (mkConstraint xobj1 xobj2 retTy otherRetTy)
-        VarTy _ -> Right mappings
-        _ -> Left (UnificationFailure constraint mappings)
-    Just (PointerTy innerTy) ->
-      case otherTy of
-        PointerTy otherInnerTy -> solveOneInternal mappings (mkConstraint xobj1 xobj2 innerTy otherInnerTy)
-        VarTy _ -> Right mappings
-        _ -> Left (UnificationFailure constraint mappings)
-    Just (RefTy innerTy) ->
-      case otherTy of
-        RefTy otherInnerTy -> solveOneInternal mappings (mkConstraint xobj1 xobj2 innerTy otherInnerTy)
-        VarTy _ -> Right mappings
-        _ -> Left (UnificationFailure constraint mappings)
-    Just foundNonVar -> case otherTy of
-                          (VarTy v) -> case recursiveLookup mappings v of
-                                         Just (VarTy _) -> Right mappings
-                                         Just otherNonVar -> if foundNonVar == otherNonVar
-                                                             then Right mappings
-                                                             else Left (UnificationFailure constraint mappings)
-                                         Nothing -> Right mappings
-                          _ -> if otherTy == foundNonVar
-                               then ok
-                               else Left (UnificationFailure constraint mappings)
-    -- Not found, no risk for conflict:
-    Nothing -> ok
-  where
-    ok = Right (Map.insert name otherTy mappings)
+    if doesTypeContainTyVarWithName name otherTy
+    then Left (UnificationFailure constraint mappings)
+    else
+      case found of --trace ("CHECK CONFLICT " ++ show constraint ++ " with name " ++ name ++ ", otherTy: " ++ show otherTy ++ ", found: " ++ show found) found of
+        Just (VarTy _) -> ok
+        Just (StructTy structName structTyVars) ->
+          case otherTy of
+            StructTy otherStructName otherTyVars | structName == otherStructName ->
+                                                   foldM solveOneInternal mappings (zipWith (mkConstraint OrdStruct xobj1 xobj2) structTyVars otherTyVars)
+            VarTy _ -> Right mappings
+            _ -> Left (UnificationFailure constraint mappings)
+        Just (FuncTy argTys retTy) ->
+          case otherTy of
+            FuncTy otherArgTys otherRetTy -> do m <- foldM solveOneInternal mappings (zipWith (mkConstraint OrdFunc xobj1 xobj2) argTys otherArgTys)
+                                                solveOneInternal m (mkConstraint OrdFunc xobj1 xobj2 retTy otherRetTy)
+            VarTy _ -> Right mappings
+            _ -> Left (UnificationFailure constraint mappings)
+        Just (PointerTy innerTy) ->
+          case otherTy of
+            PointerTy otherInnerTy -> solveOneInternal mappings (mkConstraint OrdPtr xobj1 xobj2 innerTy otherInnerTy)
+            VarTy _ -> Right mappings
+            _ -> Left (UnificationFailure constraint mappings)
+        Just (RefTy innerTy) ->
+          case otherTy of
+            RefTy otherInnerTy -> solveOneInternal mappings (mkConstraint OrdRef xobj1 xobj2 innerTy otherInnerTy)
+            VarTy _ -> Right mappings
+            _ -> Left (UnificationFailure constraint mappings)
+        Just foundNonVar -> case otherTy of
+                              (VarTy v) -> case recursiveLookup mappings v of
+                                             Just (VarTy _) -> Right mappings
+                                             Just otherNonVar -> if foundNonVar == otherNonVar
+                                                                 then Right mappings
+                                                                 else Left (UnificationFailure constraint mappings)
+                                             Nothing -> Right mappings
+                              _ -> if otherTy == foundNonVar
+                                   then ok
+                                   else Left (UnificationFailure constraint mappings)
+        -- Not found, no risk for conflict:
+        Nothing -> ok
+      where
+        ok = Right (Map.insert name otherTy mappings)
 
 debugResolveFully :: TypeMappings -> String -> Either UnificationFailure TypeMappings
 debugResolveFully mappings var = trace ("Mappings: " ++ show mappings ++ ", will resolve " ++ show var) (resolveFully mappings var)

src/Types.hs

@@ -13,6 +13,7 @@ module Types ( TypeMappings
              , typesCopyFunctionType
              , isFullyGenericType
              , consPath
+             , doesTypeContainTyVarWithName
              ) where
 
 import qualified Data.Map as Map
@@ -111,6 +112,14 @@ isTypeGeneric (PointerTy p) = isTypeGeneric p
 isTypeGeneric (RefTy r) = isTypeGeneric r
 isTypeGeneric _ = False
 
+doesTypeContainTyVarWithName :: String -> Ty -> Bool
+doesTypeContainTyVarWithName name (VarTy n) = name == n
+doesTypeContainTyVarWithName name (FuncTy argTys retTy) = any (doesTypeContainTyVarWithName name) argTys || (doesTypeContainTyVarWithName name) retTy
+doesTypeContainTyVarWithName name (StructTy _ tyArgs) = any (doesTypeContainTyVarWithName name) tyArgs
+doesTypeContainTyVarWithName name (PointerTy p) = doesTypeContainTyVarWithName name p
+doesTypeContainTyVarWithName name (RefTy r) = doesTypeContainTyVarWithName name r
+doesTypeContainTyVarWithName _ _ = False
+
 -- | Map type variable names to actual types, eg. t0 => Int, t1 => Float
 type TypeMappings = Map.Map String Ty