Don’t recurse forever when inferring roles of recursive types

kl0tl · kl0tl · commit d60a158fb14d · 2020-05-01T19:37:00.000+02:00
diff --git a/src/Language/PureScript/TypeChecker/Roles.hs b/src/Language/PureScript/TypeChecker/Roles.hs
@@ -11,8 +11,10 @@ module Language.PureScript.TypeChecker.Roles
 import Prelude.Compat
 
 import Data.Coerce (coerce)
+import Data.Foldable (fold)
 import qualified Data.Map as M
 import Data.Maybe (fromMaybe)
+import Data.Monoid (Endo(..))
 import qualified Data.Set as S
 import Data.Text (Text)
 
@@ -27,7 +29,7 @@ import Language.PureScript.Types
 -- ascribed to any given variable, as defined by the @Role@ type's @Ord@
 -- instance. That is, a variable that has been marked as @Nominal@ can not
 -- later be marked @Representational@, and so on.
-newtype RoleMap = RoleMap { getRoleMap :: M.Map Text Role }
+newtype RoleMap = RoleMap (M.Map Text Role)
 
 instance Semigroup RoleMap where
   (<>) =
@@ -37,46 +39,65 @@ instance Monoid RoleMap where
   mempty =
     RoleMap M.empty
 
+type RoleEnv = M.Map (Qualified (ProperName 'TypeName)) [Role]
+
 -- |
 -- Given an environment and the qualified name of a type constructor in that
 -- environment, returns a list of roles, in the order they are defined in the
 -- type definition.
 inferRoles :: Environment -> Qualified (ProperName 'TypeName) -> [Role]
-inferRoles env tyName
-  | Just roles <- M.lookup tyName (roleDeclarations env) =
-      roles
-  | Just (_, DataType tvs ctors) <- envMeta =
+inferRoles env tyName =
+  fold . M.lookup tyName $ updateRoleEnv env tyName (roleDeclarations env)
+
+updateRoleEnv :: Environment -> Qualified (ProperName 'TypeName) -> RoleEnv -> RoleEnv
+updateRoleEnv env tyName initialRoleEnv =
+  case M.lookup tyName (types env) of
+    Nothing ->
+      initialRoleEnv
+    Just ty ->
+      case updateRoleEnvOnce tyName ty initialRoleEnv of
+        (updatedRoleEnv, dependencies)
+          | null dependencies ->
+              updatedRoleEnv
+          | otherwise ->
+              let initialRoleEnv' = foldMap (Endo . updateRoleEnv env) dependencies
+                          `appEndo` updatedRoleEnv
+              in updateRoleEnv env tyName $ initialRoleEnv'
+
+updateRoleEnvOnce :: Qualified (ProperName 'TypeName) -> (SourceType, TypeKind) -> RoleEnv -> (RoleEnv, S.Set (Qualified (ProperName 'TypeName)))
+updateRoleEnvOnce tyName ty roleEnv
+  | (_, DataType tvs ctors) <- ty =
       -- A plain data type. For each constructor the type has, walk its list of
       -- field types and accumulate a list of (formal parameter name, role)
       -- pairs. Then, walk the list of defined parameters, ensuring both that
       -- every parameter appears (with a default role of phantom) and that they
       -- appear in the right order.
-      let ctorRoles = getRoleMap $ foldMap (foldMap (walk mempty) . snd) ctors
-      in  map (\(tv, _) -> fromMaybe Phantom (M.lookup tv ctorRoles)) tvs
-  | Just (k, ExternData) <- envMeta =
+      let (RoleMap ctorsRoles, dependencies) = foldMap (foldMap (walk mempty roleEnv) . snd) ctors
+          roles = map (\(tv, _) -> fromMaybe Phantom (M.lookup tv ctorsRoles)) tvs
+      in (updateRoles tyName roles roleEnv, dependencies)
+  | (k, ExternData) <- ty
+  , Nothing <- M.lookup tyName roleEnv =
       -- A foreign data type. Since the type will have no defined constructors
       -- nor associated data types, infer the set of type parameters from its
       -- kind and assume in the absence of role signatures that all such
       -- parameters are nominal.
-      rolesFromForeignTypeKind k
+      (updateRoles tyName (rolesFromForeignTypeKind k) roleEnv, mempty)
   | otherwise =
-      []
+      (roleEnv, mempty)
   where
-    envTypes = types env
-    envMeta = M.lookup tyName envTypes
     -- This function is named walk to match the specification given in the "Role
     -- inference" section of the paper "Safe Zero-cost Coercions for Haskell".
-    walk :: S.Set Text -> SourceType -> RoleMap
-    walk btvs (TypeVar _ v)
+    walk :: S.Set Text -> RoleEnv -> SourceType -> (RoleMap, S.Set (Qualified (ProperName 'TypeName)))
+    walk btvs _ (TypeVar _ v)
       -- A type variable standing alone (e.g. @a@ in @data D a b = D a@) is
       -- representational, _unless_ it has been bound by a quantifier, in which
       -- case it is not actually a parameter to the type (e.g. @z@ in
       -- @data T z = T (forall z. z -> z)@).
       | S.member v btvs =
           mempty
       | otherwise =
-          RoleMap $ M.singleton v Representational
-    walk btvs (ForAll _ tv _ t _) =
+          (RoleMap $ M.singleton v Representational, mempty)
+    walk btvs roleEnv' (ForAll _ tv _ t _) =
       -- We can walk under universal quantifiers as long as we make note of the
       -- variables that they bind. For instance, given a definition
       -- @data T z = T (forall z. z -> z)@, we will make note that @z@ is bound
@@ -85,15 +106,15 @@ inferRoles env tyName
       -- @data D a = D (forall r. r -> a)@, we'll mark @r@ as bound so that it
       -- doesn't appear as a spurious parameter to @D@ when we complete
       -- inference.
-      walk (S.insert tv btvs) t
-    walk btvs (RCons _ _ thead ttail) =
+      walk (S.insert tv btvs) roleEnv' t
+    walk btvs roleEnv' (RCons _ _ thead ttail) =
       -- For row types, we just walk along them and collect the results.
-      walk btvs thead <> walk btvs ttail
-    walk btvs (KindedType _ t _k) =
+      walk btvs roleEnv' thead <> walk btvs roleEnv' ttail
+    walk btvs roleEnv' (KindedType _ t _k) =
       -- For kind-annotated types, discard the annotation and recurse on the
       -- type beneath.
-      walk btvs t
-    walk btvs t
+      walk btvs roleEnv' t
+    walk btvs roleEnv' t
       | (t1, _, t2s) <- unapplyTypes t
       , not $ null t2s =
           case t1 of
@@ -109,31 +130,37 @@ inferRoles env tyName
             -- * If the role is phantom, terminate, since the argument's use of
             --   our parameters is unimportant.
             TypeConstructor _ t1Name ->
-              let t1Roles = inferRoles env t1Name
+              let roles = M.lookup t1Name roleEnv'
+                  inferred = fromMaybe (repeat Phantom) roles
+                  dependencies = maybe (S.singleton t1Name) mempty roles
                   k role ti = case role of
                     Nominal ->
-                      freeNominals ti
+                      (freeNominals ti, mempty)
                     Representational ->
                       go ti
                     Phantom ->
                       mempty
-              in  mconcat (zipWith k t1Roles t2s)
+              in mappend dependencies <$> mconcat (zipWith k inferred t2s)
             -- If the type is an application of any other type-level term, walk
             -- that term to collect its roles and mark all free variables in
             -- its argument as nominal.
             _ ->
-              go t1 <> foldMap freeNominals t2s
+              go t1 <> (foldMap freeNominals t2s, mempty)
       | otherwise =
           mempty
       where
-        go = walk btvs
+        go = walk btvs roleEnv'
         -- Given a type, computes the list of free variables in that type
         -- (taking into account those bound in @walk@) and returns a @RoleMap@
         -- ascribing a nominal role to each of those variables.
         freeNominals x =
           let ftvs = filter (flip S.notMember btvs) (freeTypeVariables x)
           in  RoleMap (M.fromList $ map (, Nominal) ftvs)
 
+updateRoles :: Qualified (ProperName 'TypeName) -> [Role] -> RoleEnv -> RoleEnv
+updateRoles = M.insertWith $ \roles' roles ->
+  uncurry min <$> zip roles' roles
+
 -- |
 -- Given the kind of a foreign type, generate a list @Nominal@ roles which, in
 -- the absence of a role signature, provides the safest default for a type whose
diff --git a/tests/purs/passing/Coercible.purs b/tests/purs/passing/Coercible.purs
@@ -163,4 +163,22 @@ type ContextualKeywords =
   , role :: String
   )
 
+data Recursive a
+  = RecursiveBaseCase
+  | Recursive a (Recursive a)
+
+recursiveTerminates :: ∀ a. Recursive a
+recursiveTerminates = coerce (RecursiveBaseCase :: Recursive (NTLib a))
+
+data MutuallyRecursive1 a
+  = MutuallyRecursiveBaseCase1
+  | MutuallyRecursive1 a (MutuallyRecursive2 a)
+
+data MutuallyRecursive2 a
+  = MutuallyRecursiveBaseCase2
+  | MutuallyRecursive2 a (MutuallyRecursive1 a)
+
+mutuallyRecursiveTerminates :: ∀ a. MutuallyRecursive1 a
+mutuallyRecursiveTerminates = coerce (MutuallyRecursiveBaseCase1 :: MutuallyRecursive1 (NTLib a))
+
 main = log (coerce (NTString1 "Done") :: String)
