purescript · hdgarrood · Jul 11, 2020 · May 16, 2020 · Jul 11, 2020 · hdgarrood
diff --git a/src/Language/PureScript/TypeChecker.hs b/src/Language/PureScript/TypeChecker.hs
@@ -277,7 +277,8 @@ typeCheckAll moduleName _ = traverse go
       checkDuplicateTypeArguments $ map fst args
       (dataCtors, ctorKind) <- kindOfData moduleName (sa, name, args, dctors)
       let args' = args `withKinds` ctorKind
-      roles <- checkRoles moduleName name args' dctors
+      env <- getEnv
+      roles <- checkRoles env moduleName name args' dctors
       let args'' = args' `withRoles` roles
       addDataType moduleName dtype name args'' dataCtors ctorKind
     return $ DataDeclaration sa dtype name args dctors
@@ -289,18 +290,22 @@ typeCheckAll moduleName _ = traverse go
         bindingGroupNames = ordNub ((syns^..traverse._2) ++ (dataDecls^..traverse._2._2) ++ (fmap coerceProperName (clss^..traverse._2._2)))
         sss = fmap declSourceSpan tys
     warnAndRethrow (addHint (ErrorInDataBindingGroup bindingGroupNames) . addHint (PositionedError sss)) $ do
+      env <- getEnv
       (syn_ks, data_ks, cls_ks) <- kindsOfAll moduleName syns (fmap snd dataDecls) (fmap snd clss)
-      for_ (zip dataDecls data_ks) $ \((dtype, (_, name, args, dctors)), (dataCtors, ctorKind)) -> do
-        when (dtype == Newtype) $ checkNewtype name dctors
-        checkDuplicateTypeArguments $ map fst args
-        let args' = args `withKinds` ctorKind `withRoles` repeat Phantom
-        addDataType moduleName dtype name args' dataCtors ctorKind
+      let dataDeclsWithKinds = zipWith (\(dtype, (_, name, args, _)) (dataCtors, ctorKind) -> (dtype, name, args `withKinds` ctorKind, dataCtors, ctorKind)) dataDecls data_ks
+          checkRoles' = checkDataBindingGroupRoles env moduleName $
+            map (\(_, name, args, dataCtors, _) -> (name, args, map fst dataCtors)) dataDeclsWithKinds
+      for_ dataDeclsWithKinds $ \(dtype, name, args', dataCtors, ctorKind) -> do
+        when (dtype == Newtype) $ checkNewtype name (map fst dataCtors)
+        checkDuplicateTypeArguments $ map fst args'
+        roles <- checkRoles' name args'
+        let args'' = args' `withRoles` roles
+        addDataType moduleName dtype name args'' dataCtors ctorKind
       for_ (zip syns syn_ks) $ \((_, name, args, _), (elabTy, kind)) -> do
         checkDuplicateTypeArguments $ map fst args
         let args' = args `withKinds` kind
         addTypeSynonym moduleName name args' elabTy kind
       for_ (zip clss cls_ks) $ \((deps, (sa, pn, _, _, _)), (args', implies', tys', kind)) -> do
-        env <- getEnv
         let qualifiedClassName = Qualified (Just moduleName) pn
         guardWith (errorMessage (DuplicateTypeClass pn (fst sa))) $
           not (M.member qualifiedClassName (typeClasses env))

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -424,7 +424,7 @@ entails SolverOptions{..} constraint context hints =
             -- constructor's arguments and generate wanted constraints
             -- appropriately (e.g. here @a@ is representational and @b@ is
             -- phantom, yielding @Coercible a a'@).
-            let tyRoles = lookupEnvRoles env aTyName
+            let tyRoles = lookupRoles env aTyName
                 k role ax bx = case role of
                   Nominal
                     -- If we had first-class equality constraints, we'd just

diff --git a/src/Language/PureScript/TypeChecker/Roles.hs b/src/Language/PureScript/TypeChecker/Roles.hs
@@ -5,27 +5,27 @@
 -- Role inference
 --
 module Language.PureScript.TypeChecker.Roles
-  ( lookupEnvRoles
+  ( lookupRoles
   , checkRoles
+  , checkDataBindingGroupRoles
   ) where
 
 import Prelude.Compat
 
-import Control.Monad
 import Control.Monad.Error.Class (MonadError(..))
-import Control.Monad.State.Class (MonadState(..))
+import Control.Monad.State (MonadState(..), runState, state)
 import Data.Coerce (coerce)
 import qualified Data.Map as M
 import Data.Maybe (fromMaybe)
 import qualified Data.Set as S
+import Data.Semigroup (Any(..))
 import Data.Text (Text)
 
 import Language.PureScript.Environment
 import Language.PureScript.Errors
 import Language.PureScript.Names
 import Language.PureScript.Roles
 import Language.PureScript.Types
-import Language.PureScript.TypeChecker.Monad
 
 -- |
 -- A map of a type's formal parameter names to their roles. This type's
@@ -43,23 +43,43 @@ instance Monoid RoleMap where
   mempty =
     RoleMap M.empty
 
+type RoleEnv = M.Map (Qualified (ProperName 'TypeName)) [Role]
+
+typeKindRoles :: TypeKind -> Maybe [Role]
+typeKindRoles = \case
+  DataType args _ ->
+    Just $ map (\(_, _, role) -> role) args
+  ExternData roles ->
+    Just roles
+  _ ->
+    Nothing
+
+getRoleEnv :: Environment -> RoleEnv
+getRoleEnv env =
+  M.mapMaybe (typeKindRoles . snd) (types env)
+
+updateRoleEnv
+  :: Qualified (ProperName 'TypeName)
+  -> [Role]
+  -> RoleEnv
+  -> (Any, RoleEnv)
+updateRoleEnv qualTyName roles' roleEnv =
+  let roles = fromMaybe (repeat Phantom) $ M.lookup qualTyName roleEnv
+      mostRestrictiveRoles = zipWith min roles roles'
+      didRolesChange = any (uncurry (<)) $ zip mostRestrictiveRoles roles
+  in (Any didRolesChange, M.insert qualTyName mostRestrictiveRoles roleEnv)
+
 -- |
 -- Lookup the roles for a type in the environment. If the type does not have
 -- roles (e.g. is a type synonym or a type variable), then this function
 -- returns an empty list.
 --
-lookupEnvRoles
+lookupRoles
   :: Environment
   -> Qualified (ProperName 'TypeName)
   -> [Role]
-lookupEnvRoles env tyName =
-  case fmap snd $ M.lookup tyName (types env) of
-    Just (DataType args _) ->
-      map (\(_, _, role) -> role) args
-    Just (ExternData roles) ->
-      roles
-    _ ->
-      []
+lookupRoles env tyName =
+  fromMaybe [] $ M.lookup tyName (types env) >>= typeKindRoles . snd
 
 -- | This function does the following:
 --
@@ -71,47 +91,92 @@ lookupEnvRoles env tyName =
 --
 checkRoles
   :: forall m
-   . (MonadError MultipleErrors m, MonadState CheckState m)
-  => ModuleName
+   . (MonadError MultipleErrors m)
+  => Environment
+  -> ModuleName
   -> ProperName 'TypeName
     -- ^ The name of the data type whose roles we are checking
   -> [(Text, Maybe SourceType)]
     -- ^ type parameters for the data type whose roles we are checking
   -> [DataConstructorDeclaration]
     -- ^ constructors of the data type whose roles we are checking
   -> m [Role]
-checkRoles moduleName tyName tyArgs ctors = do
-  let qualName = Qualified (Just moduleName) tyName
-  roleMaps <- traverse (walk mempty . snd) $ ctors >>= dataCtorFields
-  let
-    ctorRoles = getRoleMap $ mconcat roleMaps
-    inferredRoles = map (\(arg, _) -> fromMaybe Phantom (M.lookup arg ctorRoles)) tyArgs
-  env <- getEnv
-  rethrow (addHint (ErrorInRoleDeclaration tyName)) $ do
-    case M.lookup qualName (roleDeclarations env) of
-      Just declaredRoles -> do
-        let
-          k (var, _) inf dec =
-            if inf < dec
-              then throwError . errorMessage $ RoleMismatch var inf dec
-              else pure dec
-        sequence $ zipWith3 k tyArgs inferredRoles declaredRoles
-      Nothing ->
-        pure inferredRoles
+checkRoles env moduleName tyName tyArgs ctors =
+  checkDataBindingGroupRoles env moduleName [(tyName, tyArgs, ctors)] tyName tyArgs
+
+type DataDeclaration =
+  ( ProperName 'TypeName
+  , [(Text, Maybe SourceType)]
+  , [DataConstructorDeclaration]
+  )
+
+checkDataBindingGroupRoles
+  :: forall m
+   . (MonadError MultipleErrors m)
+  => Environment
+  -> ModuleName
+  -> [DataDeclaration]
+  -> ProperName 'TypeName
+  -> [(Text, Maybe SourceType)]
+  -> m [Role]
+checkDataBindingGroupRoles env moduleName group =
+  let initialRoleEnv = M.union (roleDeclarations env) (getRoleEnv env)
+      inferredRoleEnv = inferDataBindingGroupRoles moduleName group initialRoleEnv
+  in \tyName tyArgs -> do
+    let qualTyName = Qualified (Just moduleName) tyName
+        inferredRoles = M.lookup qualTyName inferredRoleEnv
+    rethrow (addHint (ErrorInRoleDeclaration tyName)) $ do
+      case M.lookup qualTyName (roleDeclarations env) of
+        Just declaredRoles -> do
+          let
+            k (var, _) inf dec =
+              if inf < dec
+                then throwError . errorMessage $ RoleMismatch var inf dec
+                else pure dec
+          sequence $ zipWith3 k tyArgs (fromMaybe (repeat Phantom) inferredRoles) declaredRoles
+        Nothing ->
+          pure $ fromMaybe (Phantom <$ tyArgs) inferredRoles
+
+inferDataBindingGroupRoles
+  :: ModuleName
+  -> [DataDeclaration]
+  -> RoleEnv
+  -> RoleEnv
+inferDataBindingGroupRoles moduleName group roleEnv =
+  let (Any didRolesChange, roleEnv') = flip runState roleEnv $
+        mconcat <$> traverse (state . inferDataDeclarationRoles moduleName) group
+  in if didRolesChange
+     then inferDataBindingGroupRoles moduleName group roleEnv'
+     else roleEnv'
+
+-- |
+-- Infers roles for the given data type declaration, along with a flag to tell
+-- if more restrictive roles were added to the environment.
+--
+inferDataDeclarationRoles
+  :: ModuleName
+  -> DataDeclaration
+  -> RoleEnv
+  -> (Any, RoleEnv)
+inferDataDeclarationRoles moduleName (tyName, tyArgs, ctors) roleEnv =
+  let qualTyName = Qualified (Just moduleName) tyName
+      ctorRoles = getRoleMap . foldMap (walk mempty . snd) $ ctors >>= dataCtorFields
+      inferredRoles = map (\(arg, _) -> fromMaybe Phantom (M.lookup arg ctorRoles)) tyArgs
+  in updateRoleEnv qualTyName inferredRoles roleEnv
   where
   -- 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 -> m RoleMap
+  walk :: S.Set Text -> SourceType -> RoleMap
   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 =
-        pure mempty
+        mempty
     | otherwise =
-        pure $ RoleMap $ M.singleton v Representational
+        RoleMap $ M.singleton v Representational
   walk btvs (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
@@ -124,9 +189,7 @@ checkRoles moduleName tyName tyArgs ctors = do
     walk (S.insert tv btvs) t
   walk btvs (RCons _ _ thead ttail) = do
     -- For row types, we just walk along them and collect the results.
-    h <- walk btvs thead
-    t <- walk btvs ttail
-    pure (h <> t)
+    walk btvs thead <> walk btvs ttail
   walk btvs (KindedType _ t _k) =
     -- For kind-annotated types, discard the annotation and recurse on the
     -- type beneath.
@@ -146,26 +209,24 @@ checkRoles moduleName tyName tyArgs ctors = do
           --   its use of our parameters is important.
           -- * If the role is phantom, terminate, since the argument's use of
           --   our parameters is unimportant.
-          TypeConstructor _ t1Name -> do
-            env <- getEnv
+          TypeConstructor _ t1Name ->
             let
-              t1Roles = lookupEnvRoles env t1Name
+              t1Roles = fromMaybe (repeat Phantom) $ M.lookup t1Name roleEnv
               k role ti = case role of
                 Nominal ->
-                  pure $ freeNominals ti
+                  freeNominals ti
                 Representational ->
                   go ti
                 Phantom ->
-                  pure mempty
-            fmap mconcat (zipWithM k t1Roles t2s)
+                  mempty
+            in mconcat (zipWith k t1Roles 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.
           _ -> do
-            r <- go t1
-            pure (r <> foldMap freeNominals t2s)
+            go t1 <> foldMap freeNominals t2s
     | otherwise =
-        pure mempty
+        mempty
     where
       go = walk btvs
       -- Given a type, computes the list of free variables in that type

diff --git a/tests/purs/failing/CoercibleRoleMismatch4.out b/tests/purs/failing/CoercibleRoleMismatch4.out
@@ -0,0 +1,15 @@
+Error found:
+in module [33mMain[0m
+at tests/purs/failing/CoercibleRoleMismatch4.purs:4:1 - 4:19 (line 4, column 1 - line 4, column 19)
+
+  Role mismatch for the type parameter [33ma[0m:
+
+    The annotation says [33mrepresentational[0m but the role [33mnominal[0m is required.
+
+
+in role declaration for [33mF[0m
+in data binding group F, G
+
+See https://github.com/purescript/documentation/blob/master/errors/RoleMismatch.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/CoercibleRoleMismatch4.purs b/tests/purs/failing/CoercibleRoleMismatch4.purs
@@ -0,0 +1,8 @@
+-- @shouldFailWith RoleMismatch
+module Main where
+
+data F a = F (G a)
+type role F representational
+
+data G a = G (F a)
+type role G nominal
diff --git a/tests/purs/failing/CoercibleRoleMismatch5.out b/tests/purs/failing/CoercibleRoleMismatch5.out
@@ -0,0 +1,15 @@
+Error found:
+in module [33mMain[0m
+at tests/purs/failing/CoercibleRoleMismatch5.purs:4:1 - 4:21 (line 4, column 1 - line 4, column 21)
+
+  Role mismatch for the type parameter [33ma[0m:
+
+    The annotation says [33mphantom[0m but the role [33mrepresentational[0m is required.
+
+
+in role declaration for [33mF[0m
+in data binding group F, G
+
+See https://github.com/purescript/documentation/blob/master/errors/RoleMismatch.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/CoercibleRoleMismatch5.purs b/tests/purs/failing/CoercibleRoleMismatch5.purs
@@ -0,0 +1,7 @@
+-- @shouldFailWith RoleMismatch
+module Main where
+
+data F a = F a (G a)
+type role F phantom
+
+data G a = G (F a)
diff --git a/tests/purs/passing/Coercible.purs b/tests/purs/passing/Coercible.purs
@@ -163,4 +163,22 @@ type ContextualKeywords =
   , role :: String
   )
 
+data MutuallyRecursivePhantom1 a
+  = MutuallyRecursivePhantom1 (MutuallyRecursivePhantom2 a)
+
+data MutuallyRecursivePhantom2 a
+  = MutuallyRecursivePhantom2 (MutuallyRecursivePhantom1 a)
+
+mutuallyRecursivePhantom :: forall a b. MutuallyRecursivePhantom1 a -> MutuallyRecursivePhantom1 b
+mutuallyRecursivePhantom = coerce
+
+data MutuallyRecursiveRepresentational1 a
+  = MutuallyRecursiveRepresentational1 a (MutuallyRecursiveRepresentational2 a)
+
+data MutuallyRecursiveRepresentational2 a
+  = MutuallyRecursiveRepresentational2 (MutuallyRecursiveRepresentational1 a)
+
+mutuallyRecursiveRepresentational :: forall a. MutuallyRecursiveRepresentational1 a -> MutuallyRecursiveRepresentational1 (Id1 a)
+mutuallyRecursiveRepresentational = coerce
+
 main = log (coerce (NTString1 "Done") :: String)