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