1{-# LANGUAGE TypeApplications #-} 2 3-- | 4-- Role inference 5-- 6module Language.PureScript.TypeChecker.Roles 7 ( lookupRoles 8 , checkRoles 9 , checkDataBindingGroupRoles 10 ) where 11 12import Prelude.Compat 13 14import Control.Monad.Error.Class (MonadError(..)) 15import Control.Monad.State (MonadState(..), runState, state) 16import Data.Coerce (coerce) 17import qualified Data.Map as M 18import Data.Maybe (fromMaybe) 19import qualified Data.Set as S 20import Data.Semigroup (Any(..)) 21import Data.Text (Text) 22 23import Language.PureScript.Environment 24import Language.PureScript.Errors 25import Language.PureScript.Names 26import Language.PureScript.Roles 27import Language.PureScript.Types 28 29-- | 30-- A map of a type's formal parameter names to their roles. This type's 31-- @Semigroup@ and @Monoid@ instances preserve the least-permissive role 32-- ascribed to any given variable, as defined by the @Role@ type's @Ord@ 33-- instance. That is, a variable that has been marked as @Nominal@ can not 34-- later be marked @Representational@, and so on. 35newtype RoleMap = RoleMap { getRoleMap :: M.Map Text Role } 36 37instance Semigroup RoleMap where 38 (<>) = 39 coerce @(M.Map Text Role -> _ -> _) @(RoleMap -> _ -> _) (M.unionWith min) 40 41instance Monoid RoleMap where 42 mempty = 43 RoleMap M.empty 44 45type RoleEnv = M.Map (Qualified (ProperName 'TypeName)) [Role] 46 47typeKindRoles :: TypeKind -> Maybe [Role] 48typeKindRoles = \case 49 DataType _ args _ -> 50 Just $ map (\(_, _, role) -> role) args 51 ExternData roles -> 52 Just roles 53 _ -> 54 Nothing 55 56getRoleEnv :: Environment -> RoleEnv 57getRoleEnv env = 58 M.mapMaybe (typeKindRoles . snd) (types env) 59 60updateRoleEnv 61 :: Qualified (ProperName 'TypeName) 62 -> [Role] 63 -> RoleEnv 64 -> (Any, RoleEnv) 65updateRoleEnv qualTyName roles' roleEnv = 66 let roles = fromMaybe (repeat Phantom) $ M.lookup qualTyName roleEnv 67 mostRestrictiveRoles = zipWith min roles roles' 68 didRolesChange = any (uncurry (<)) $ zip mostRestrictiveRoles roles 69 in (Any didRolesChange, M.insert qualTyName mostRestrictiveRoles roleEnv) 70 71-- | 72-- Lookup the roles for a type in the environment. If the type does not have 73-- roles (e.g. is a type synonym or a type variable), then this function 74-- returns an empty list. 75-- 76lookupRoles 77 :: Environment 78 -> Qualified (ProperName 'TypeName) 79 -> [Role] 80lookupRoles env tyName = 81 fromMaybe [] $ M.lookup tyName (types env) >>= typeKindRoles . snd 82 83-- | This function does the following: 84-- 85-- * Infers roles for the given data type declaration 86-- 87-- * Compares the inferred roles to the explicitly declared roles (if any) and 88-- ensures that the explicitly declared roles are not more permissive than 89-- the inferred ones 90-- 91checkRoles 92 :: forall m 93 . (MonadError MultipleErrors m) 94 => Environment 95 -> ModuleName 96 -> ProperName 'TypeName 97 -- ^ The name of the data type whose roles we are checking 98 -> [(Text, Maybe SourceType)] 99 -- ^ type parameters for the data type whose roles we are checking 100 -> [DataConstructorDeclaration] 101 -- ^ constructors of the data type whose roles we are checking 102 -> m [Role] 103checkRoles env moduleName tyName tyArgs ctors = 104 checkDataBindingGroupRoles env moduleName [(tyName, tyArgs, ctors)] tyName tyArgs 105 106type DataDeclaration = 107 ( ProperName 'TypeName 108 , [(Text, Maybe SourceType)] 109 , [DataConstructorDeclaration] 110 ) 111 112checkDataBindingGroupRoles 113 :: forall m 114 . (MonadError MultipleErrors m) 115 => Environment 116 -> ModuleName 117 -> [DataDeclaration] 118 -> ProperName 'TypeName 119 -> [(Text, Maybe SourceType)] 120 -> m [Role] 121checkDataBindingGroupRoles env moduleName group = 122 let initialRoleEnv = M.union (roleDeclarations env) (getRoleEnv env) 123 inferredRoleEnv = inferDataBindingGroupRoles moduleName group initialRoleEnv 124 in \tyName tyArgs -> do 125 let qualTyName = Qualified (Just moduleName) tyName 126 inferredRoles = M.lookup qualTyName inferredRoleEnv 127 rethrow (addHint (ErrorInRoleDeclaration tyName)) $ do 128 case M.lookup qualTyName (roleDeclarations env) of 129 Just declaredRoles -> do 130 let 131 k (var, _) inf dec = 132 if inf < dec 133 then throwError . errorMessage $ RoleMismatch var inf dec 134 else pure dec 135 sequence $ zipWith3 k tyArgs (fromMaybe (repeat Phantom) inferredRoles) declaredRoles 136 Nothing -> 137 pure $ fromMaybe (Phantom <$ tyArgs) inferredRoles 138 139inferDataBindingGroupRoles 140 :: ModuleName 141 -> [DataDeclaration] 142 -> RoleEnv 143 -> RoleEnv 144inferDataBindingGroupRoles moduleName group roleEnv = 145 let (Any didRolesChange, roleEnv') = flip runState roleEnv $ 146 mconcat <$> traverse (state . inferDataDeclarationRoles moduleName) group 147 in if didRolesChange 148 then inferDataBindingGroupRoles moduleName group roleEnv' 149 else roleEnv' 150 151-- | 152-- Infers roles for the given data type declaration, along with a flag to tell 153-- if more restrictive roles were added to the environment. 154-- 155inferDataDeclarationRoles 156 :: ModuleName 157 -> DataDeclaration 158 -> RoleEnv 159 -> (Any, RoleEnv) 160inferDataDeclarationRoles moduleName (tyName, tyArgs, ctors) roleEnv = 161 let qualTyName = Qualified (Just moduleName) tyName 162 ctorRoles = getRoleMap . foldMap (walk mempty . snd) $ ctors >>= dataCtorFields 163 inferredRoles = map (\(arg, _) -> fromMaybe Phantom (M.lookup arg ctorRoles)) tyArgs 164 in updateRoleEnv qualTyName inferredRoles roleEnv 165 where 166 -- This function is named @walk@ to match the specification given in the 167 -- "Role inference" section of the paper "Safe Zero-cost Coercions for 168 -- Haskell". 169 walk :: S.Set Text -> SourceType -> RoleMap 170 walk btvs (TypeVar _ v) 171 -- A type variable standing alone (e.g. @a@ in @data D a b = D a@) is 172 -- representational, _unless_ it has been bound by a quantifier, in which 173 -- case it is not actually a parameter to the type (e.g. @z@ in 174 -- @data T z = T (forall z. z -> z)@). 175 | S.member v btvs = 176 mempty 177 | otherwise = 178 RoleMap $ M.singleton v Representational 179 walk btvs (ForAll _ tv _ t _) = 180 -- We can walk under universal quantifiers as long as we make note of the 181 -- variables that they bind. For instance, given a definition 182 -- @data T z = T (forall z. z -> z)@, we will make note that @z@ is bound 183 -- by a quantifier so that we do not mark @T@'s parameter as 184 -- representational later on. Similarly, given a definition like 185 -- @data D a = D (forall r. r -> a)@, we'll mark @r@ as bound so that it 186 -- doesn't appear as a spurious parameter to @D@ when we complete 187 -- inference. 188 walk (S.insert tv btvs) t 189 walk btvs (ConstrainedType _ Constraint{..} t) = 190 -- For constrained types, mark all free variables in the constraint 191 -- arguments as nominal and recurse on the type beneath the constraint. 192 walk btvs t <> foldMap (freeNominals btvs) constraintArgs 193 walk btvs (RCons _ _ thead ttail) = do 194 -- For row types, we just walk along them and collect the results. 195 walk btvs thead <> walk btvs ttail 196 walk btvs (KindedType _ t _k) = 197 -- For kind-annotated types, discard the annotation and recurse on the 198 -- type beneath. 199 walk btvs t 200 walk btvs t 201 | (t1, _, t2s) <- unapplyTypes t 202 , not $ null t2s = 203 case t1 of 204 -- If the type is an application of a type constructor to some 205 -- arguments, recursively infer the roles of the type constructor's 206 -- arguments. For each (role, argument) pair: 207 -- 208 -- - If the role is nominal, mark all free variables in the argument 209 -- as nominal also, since they cannot be coerced if the 210 -- argument's nominality is to be preserved. 211 -- 212 -- - If the role is representational, recurse on the argument, since 213 -- its use of our parameters is important. 214 -- 215 -- - If the role is phantom, terminate, since the argument's use of 216 -- our parameters is unimportant. 217 TypeConstructor _ t1Name -> 218 let 219 t1Roles = fromMaybe (repeat Phantom) $ M.lookup t1Name roleEnv 220 k role ti = case role of 221 Nominal -> 222 freeNominals btvs ti 223 Representational -> 224 go ti 225 Phantom -> 226 mempty 227 in mconcat (zipWith k t1Roles t2s) 228 -- If the type is an application of any other type-level term, walk 229 -- that term to collect its roles and mark all free variables in 230 -- its argument as nominal. 231 _ -> do 232 go t1 <> foldMap (freeNominals btvs) t2s 233 | otherwise = 234 mempty 235 where 236 go = walk btvs 237 238-- Given a type, computes the list of free variables in that type 239-- (taking into account those bound in @walk@) and returns a @RoleMap@ 240-- ascribing a nominal role to each of those variables. 241freeNominals :: S.Set Text -> SourceType -> RoleMap 242freeNominals btvs x = 243 let ftvs = filter (flip S.notMember btvs) (freeTypeVariables x) 244 in RoleMap (M.fromList $ map (, Nominal) ftvs) 245