Lint: Node pattern match uses subtype instead of type equality.

Author: andorp

grin/src/Grin/Lint.hs

@@ -318,7 +318,7 @@ lint warningKinds mTypeEnv exp@(Program exts _) =
               lhsType         <- normalizeType <$> extract leftExp
               pure $ do -- Lint
                 -- NOTE: This can still give false positive errors, because bottom-up typing can only approximate the result of HPT.
-                when (sameType expectedPatType lhsType == Just False) $ do
+                when (subType expectedPatType lhsType == Just False) $ do
                   warning Semantics $ [beforeMsg $ unwords
                     ["Invalid pattern match for", plainShow lpat ++ "." , "Expected pattern of type:", plainShow expectedPatType ++ ",", "but got:", plainShow lhsType]]
 

grin/src/Grin/TypeEnv.hs

@@ -11,8 +11,8 @@ import Data.Map (Map)
 import Data.Set (Set)
 import Data.Vector (Vector)
 import qualified Data.Map as Map
-import qualified Data.Set as Set (fromList, toList)
-import qualified Data.Vector as Vector (fromList, toList, map)
+import qualified Data.Set as Set
+import qualified Data.Vector as Vector
 import Data.Bifunctor (bimap)
 import Data.Monoid
 import Data.Maybe (fromMaybe)
@@ -181,6 +181,29 @@ sameType (T_SimpleType T_UnspecifiedLocation) _ = Nothing
 sameType _ (T_SimpleType T_UnspecifiedLocation) = Nothing
 sameType t1 t2 = Just $ t1 == t2
 
+subType :: Type -> Type -> Maybe Bool
+subType (T_SimpleType T_Dead) _ = Nothing
+subType _ (T_SimpleType T_Dead) = Nothing
+subType (T_SimpleType T_UnspecifiedLocation) _ = Nothing
+subType _ (T_SimpleType T_UnspecifiedLocation) = Nothing
+subType (T_SimpleType st1) (T_SimpleType st2) = Just $ simpleSubType st1 st2
+subType (T_NodeSet t1) (T_NodeSet t2) = do -- t1 <: t2
+  let ks1     = Map.keysSet t1
+  let ks2     = Map.keysSet t2
+  let subset  = ks1 `Set.isSubsetOf` ks2
+  pure $ subset && and  [ Vector.length v1 == Vector.length v2
+                          && (Vector.all id (Vector.zipWith simpleSubType v1 v2))
+                        | (t,v1)  <- Map.toList t1
+                        , Just v2 <- pure $ Map.lookup t t2
+                        ]
+subType _ _ = Nothing
+
+simpleSubType :: SimpleType -> SimpleType -> Bool
+simpleSubType T_UnspecifiedLocation (T_Location l) = True
+simpleSubType (T_Location ls1) (T_Location ls2) =
+  (Set.fromList ls1) `Set.isSubsetOf` (Set.fromList ls2)
+simpleSubType t1 t2 = t1 == t2
+
 ptrLocations :: TypeEnv -> Name -> [Loc]
 ptrLocations te p = case variableType te p of
   T_SimpleType (T_Location locs) -> locs

grin/test/LintSpec.hs

@@ -224,45 +224,38 @@ spec = do
       let (_, errors) = lint allWarnings (Just typeEnv) program
       lintErrors errors `shouldBe` ["Invalid pattern match for (CInt x). Expected pattern of type: {CInt[T_Dead]}, but got: {CFloat[T_Float]}"]
 
-    it "disregards variable patterns" $ do
+    it "doesn't alert over-approximated binds" $ do
       let program = [prog|
           main =
-            n0 <- pure (CInt 0)
-            n1 <- case n0 of
-              (CInt c0) -> pure n0
-              (CFloat c1) ->
-                a0 <- pure (CFloat 2.0)
-                pure a0
+            i <- pure (CInt 1)
+            f <- pure (CFloat 1.0)
+            l <- store i
+            update l f
+            v <- fetch l
+            (CFloat f2) <- pure v
             pure ()
         |]
       let typeEnv = inferTypeEnv program
       let (_, errors) = lint allWarnings (Just typeEnv) program
       lintErrors errors `shouldBe` []
 
-    -- NOTE: Bottom-up typing can only approximate the result of HPT.
-    it "can give false positive errors" $ do
+    it "disregards variable patterns" $ do
       let program = [prog|
           main =
-            n0 <- case 0 of
-              0 ->
-                n1 <- pure (CInt 0)
-                pure n1
-              1 ->
-                n2 <- pure (CFloat 0.0)
-                pure n2
-            (CInt x) <- case n0 of
+            n0 <- pure (CInt 0)
+            n1 <- case n0 of
               (CInt c0) -> pure n0
               (CFloat c1) ->
-                a0 <- pure (CInt 0)
+                a0 <- pure (CFloat 2.0)
                 pure a0
             pure ()
         |]
       let typeEnv = inferTypeEnv program
       let (_, errors) = lint allWarnings (Just typeEnv) program
-      lintErrors errors `shouldBe` ["Invalid pattern match for (CInt x). Expected pattern of type: {CInt[T_Int64]}, but got: {CFloat[T_Float],CInt[T_Int64]}"]
+      lintErrors errors `shouldBe` []
 
   describe "Producer lint" $ do
-    it "finds nodes in single return statment" $ do
+    it "finds nodes in single return statement" $ do
       let program = [prog|
           grinMain =
             pure (CInt 5)
@@ -271,7 +264,7 @@ spec = do
       let (_, errors) = lint allWarnings (Just typeEnv) program
       lintErrors errors `shouldBe` ["Last return expressions can only return non-node values: pure (CInt 5)"]
 
-    it "finds nodes in last return statment" $ do
+    it "finds nodes in last return statement" $ do
       let program = [prog|
           grinMain =
             n <- pure (CInt 0)
@@ -281,7 +274,7 @@ spec = do
       let (_, errors) = lint allWarnings (Just typeEnv) program
       lintErrors errors `shouldBe` ["Last return expressions can only return non-node values: pure (CInt 5)"]
 
-    it "finds nodes in single return statment in case alternative" $ do
+    it "finds nodes in single return statement in case alternative" $ do
       let program = [prog|
           grinMain =
             case 0 of
@@ -291,7 +284,7 @@ spec = do
       let (_, errors) = lint allWarnings (Just typeEnv) program
       lintErrors errors `shouldBe` ["Last return expressions can only return non-node values: pure (CInt 5)"]
 
-    it "finds nodes in last return statment in case alternative" $ do
+    it "finds nodes in last return statement in case alternative" $ do
       let program = [prog|
           grinMain =
             case 0 of