%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
%
Analysis functions over data types. Specficially, detecting recursive types.
This stuff is only used for source-code decls; it's recorded in interface
files for imported data types.
\begin{code}
module TcTyDecls(
calcRecFlags, RecTyInfo(..),
calcSynCycles, calcClassCycles,
RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots
) where
#include "HsVersions.h"
import TypeRep
import HsSyn
import Class
import Type
import Kind
import HscTypes
import TyCon
import DataCon
import Var
import Name
import NameEnv
import VarEnv
import VarSet
import NameSet
import Coercion ( ltRole )
import Avail
import Digraph
import BasicTypes
import SrcLoc
import Outputable
import UniqSet
import Util
import Maybes
import Data.List
import Control.Applicative (Applicative(..))
import Control.Monad
\end{code}
%************************************************************************
%* *
Cycles in class and type synonym declarations
%* *
%************************************************************************
Checking for class-decl loops is easy, because we don't allow class decls
in interface files.
We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
so we don't check for loops that involve them. So we only look for synonym
loops in the module being compiled.
We check for type synonym and class cycles on the *source* code.
Main reasons:
a) Otherwise we'd need a special function to extract type-synonym tycons
from a type, whereas we already have the free vars pinned on the decl
b) If we checked for type synonym loops after building the TyCon, we
can't do a hoistForAllTys on the type synonym rhs, (else we fall into
a black hole) which seems unclean. Apart from anything else, it'd mean
that a type-synonym rhs could have for-alls to the right of an arrow,
which means adding new cases to the validity checker
Indeed, in general, checking for cycles beforehand means we need to
be less careful about black holes through synonym cycles.
The main disadvantage is that a cycle that goes via a type synonym in an
.hi-boot file can lead the compiler into a loop, because it assumes that cycles
only occur entirely within the source code of the module being compiled.
But hi-boot files are trusted anyway, so this isn't much worse than (say)
a kind error.
[ NOTE ----------------------------------------------
If we reverse this decision, this comment came from tcTyDecl1, and should
go back there
-- dsHsType, not tcHsKindedType, to avoid a loop. tcHsKindedType does hoisting,
-- which requires looking through synonyms... and therefore goes into a loop
-- on (erroneously) recursive synonyms.
-- Solution: do not hoist synonyms, because they'll be hoisted soon enough
-- when they are substituted
We'd also need to add back in this definition
synTyConsOfType :: Type -> [TyCon]
-- Does not look through type synonyms at all
-- Return a list of synonym tycons
synTyConsOfType ty
= nameEnvElts (go ty)
where
go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
go (TyVarTy v) = emptyNameEnv
go (TyConApp tc tys) = go_tc tc tys
go (AppTy a b) = go a `plusNameEnv` go b
go (FunTy a b) = go a `plusNameEnv` go b
go (ForAllTy _ ty) = go ty
go_tc tc tys | isSynTyCon tc = extendNameEnv (go_s tys) (tyConName tc) tc
| otherwise = go_s tys
go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
---------------------------------------- END NOTE ]
\begin{code}
mkSynEdges :: [LTyClDecl Name] -> [(LTyClDecl Name, Name, [Name])]
mkSynEdges syn_decls = [ (ldecl, name, nameSetToList fvs)
| ldecl@(L _ (SynDecl { tcdLName = L _ name
, tcdFVs = fvs })) <- syn_decls ]
calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
\end{code}
Note [Superclass cycle check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can't allow cycles via superclasses because it would result in the
type checker looping when it canonicalises a class constraint (superclasses
are added during canonicalisation). More precisely, given a constraint
C ty1 .. tyn
we want to instantiate all of C's superclasses, transitively, and
that set must be finite. So if
class (D b, E b a) => C a b
then when we encounter the constraint
C ty1 ty2
we'll instantiate the superclasses
(D ty2, E ty2 ty1)
and then *their* superclasses, and so on. This set must be finite!
It is OK for superclasses to be type synonyms for other classes, so
must "look through" type synonyms. Eg
type X a = C [a]
class X a => C a -- No! Recursive superclass!
We want definitions such as:
class C cls a where cls a => a -> a
class C D a => D a where
to be accepted, even though a naive acyclicity check would reject the
program as having a cycle between D and its superclass. Why? Because
when we instantiate
D ty1
we get the superclas
C D ty1
and C has no superclasses, so we have terminated with a finite set.
More precisely, the rule is this: the superclasses sup_C of a class C
are rejected iff:
C \elem expand(sup_C)
Where expand is defined as follows:
(1) expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
(2) expand(D ty1 ... tyN) = {D}
\union sup_D[ty1/x1, ..., tyP/xP]
\union expand(ty(P+1)) ... \union expand(tyN)
where (D x1 ... xM) is a class, P = min(M,N)
(3) expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
where T is not a class
Eqn (1) is conservative; when there's a type variable at the head,
look in all the argument types. Eqn (2) expands superclasses; the
third component of the union is like Eqn (1). Eqn (3) happens mainly
when the context is a (constraint) tuple, such as (Eq a, Show a).
Furthermore, expand always looks through type synonyms.
\begin{code}
calcClassCycles :: Class -> [[TyCon]]
calcClassCycles cls
= nubBy eqAsCycle $
expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
where
eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
cycles xs = take n . map (take n) . tails . cycle $ xs
where n = length xs
expandTheta :: UniqSet Class
-> [TyCon]
-> ThetaType
-> [[TyCon]]
-> [[TyCon]]
expandTheta _ _ [] = id
expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
expandType seen path (TyConApp tc tys)
| Just cls <- tyConClass_maybe tc
, let (env, remainder) = papp (classTyVars cls) tys
rest_tys = either (const []) id remainder
= if cls `elementOfUniqSet` seen
then (reverse (classTyCon cls:path):)
. flip (foldr (expandType seen path)) tys
else expandTheta (addOneToUniqSet seen cls) (tc:path)
(substTys (mkTopTvSubst env) (classSCTheta cls))
. flip (foldr (expandType seen path)) rest_tys
| Just (tvs, rhs) <- synTyConDefn_maybe tc
, let (env, remainder) = papp tvs tys
rest_tys = either (const []) id remainder
= expandType seen (tc:path) (substTy (mkTopTvSubst env) rhs)
. flip (foldr (expandType seen path)) rest_tys
| otherwise
= flip (foldr (expandType seen path)) tys
expandType _ _ (TyVarTy {}) = id
expandType _ _ (LitTy {}) = id
expandType seen path (AppTy t1 t2) = expandType seen path t1 . expandType seen path t2
expandType seen path (FunTy t1 t2) = expandType seen path t1 . expandType seen path t2
expandType seen path (ForAllTy _tv t) = expandType seen path t
papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
papp [] tys = ([], Right tys)
papp tvs [] = ([], Left tvs)
papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
where (env, remainder) = papp tvs tys
\end{code}
%************************************************************************
%* *
Deciding which type constructors are recursive
%* *
%************************************************************************
Identification of recursive TyCons
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
@TyThing@s.
Identifying a TyCon as recursive serves two purposes
1. Avoid infinite types. Non-recursive newtypes are treated as
"transparent", like type synonyms, after the type checker. If we did
this for all newtypes, we'd get infinite types. So we figure out for
each newtype whether it is "recursive", and add a coercion if so. In
effect, we are trying to "cut the loops" by identifying a loop-breaker.
2. Avoid infinite unboxing. This is nothing to do with newtypes.
Suppose we have
data T = MkT Int T
f (MkT x t) = f t
Well, this function diverges, but we don't want the strictness analyser
to diverge. But the strictness analyser will diverge because it looks
deeper and deeper into the structure of T. (I believe there are
examples where the function does something sane, and the strictness
analyser still diverges, but I can't see one now.)
Now, concerning (1), the FC2 branch currently adds a coercion for ALL
newtypes. I did this as an experiment, to try to expose cases in which
the coercions got in the way of optimisations. If it turns out that we
can indeed always use a coercion, then we don't risk recursive types,
and don't need to figure out what the loop breakers are.
For newtype *families* though, we will always have a coercion, so they
are always loop breakers! So you can easily adjust the current
algorithm by simply treating all newtype families as loop breakers (and
indeed type families). I think.
For newtypes, we label some as "recursive" such that
INVARIANT: there is no cycle of non-recursive newtypes
In any loop, only one newtype need be marked as recursive; it is
a "loop breaker". Labelling more than necessary as recursive is OK,
provided the invariant is maintained.
A newtype M.T is defined to be "recursive" iff
(a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
(b) it is declared in a source file, but that source file has a
companion hi-boot file which declares the type
or (c) one can get from T's rhs to T via type
synonyms, or non-recursive newtypes *in M*
e.g. newtype T = MkT (T -> Int)
(a) is conservative; declarations in hi-boot files are always
made loop breakers. That's why in (b) we can restrict attention
to tycons in M, because any loops through newtypes outside M
will be broken by those newtypes
(b) ensures that a newtype is not treated as a loop breaker in one place
and later as a non-loop-breaker. This matters in GHCi particularly, when
a newtype T might be embedded in many types in the environment, and then
T's source module is compiled. We don't want T's recursiveness to change.
The "recursive" flag for algebraic data types is irrelevant (never consulted)
for types with more than one constructor.
An algebraic data type M.T is "recursive" iff
it has just one constructor, and
(a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
(b) it is declared in a source file, but that source file has a
companion hi-boot file which declares the type
or (c) one can get from its arg types to T via type synonyms,
or by non-recursive newtypes or non-recursive product types in M
e.g. data T = MkT (T -> Int) Bool
Just like newtype in fact
A type synonym is recursive if one can get from its
right hand side back to it via type synonyms. (This is
reported as an error.)
A class is recursive if one can get from its superclasses
back to it. (This is an error too.)
Hi-boot types
~~~~~~~~~~~~~
A data type read from an hi-boot file will have an AbstractTyCon as its AlgTyConRhs
and will respond True to isAbstractTyCon. The idea is that we treat these as if one
could get from these types to anywhere. So when we see
module Baz where
import {-# SOURCE #-} Foo( T )
newtype S = MkS T
then we mark S as recursive, just in case. What that means is that if we see
import Baz( S )
newtype R = MkR S
then we don't need to look inside S to compute R's recursiveness. Since S is imported
(not from an hi-boot file), one cannot get from R back to S except via an hi-boot file,
and that means that some data type will be marked recursive along the way. So R is
unconditionly non-recursive (i.e. there'll be a loop breaker elsewhere if necessary)
This in turn means that we grovel through fewer interface files when computing
recursiveness, because we need only look at the type decls in the module being
compiled, plus the outer structure of directly-mentioned types.
\begin{code}
data RecTyInfo = RTI { rti_promotable :: Bool
, rti_roles :: Name -> [Role]
, rti_is_rec :: Name -> RecFlag }
calcRecFlags :: ModDetails -> Bool
-> RoleAnnots -> [TyThing] -> RecTyInfo
calcRecFlags boot_details is_boot mrole_env tyclss
= RTI { rti_promotable = is_promotable
, rti_roles = roles
, rti_is_rec = is_rec }
where
rec_tycon_names = mkNameSet (map tyConName all_tycons)
all_tycons = mapCatMaybes getTyCon tyclss
is_promotable = all (isPromotableTyCon rec_tycon_names) all_tycons
roles = inferRoles is_boot mrole_env all_tycons
is_rec n | n `elemNameSet` rec_names = Recursive
| otherwise = NonRecursive
boot_name_set = availsToNameSet (md_exports boot_details)
rec_names = boot_name_set `unionNameSets`
nt_loop_breakers `unionNameSets`
prod_loop_breakers
single_con_tycons = [ tc | tc <- all_tycons
, not (tyConName tc `elemNameSet` boot_name_set)
, isSingleton (tyConDataCons tc) ]
(new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
is_rec_nt tc = tyConName tc `elemNameSet` nt_loop_breakers
nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
mk_nt_edges nt
= concatMap (mk_nt_edges1 nt) (tyConsOfType (new_tc_rhs nt))
mk_nt_edges1 _ tc
| tc `elem` new_tycons = [tc]
| otherwise = []
prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
mk_prod_edges tc
= concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (tyConsOfType ty)
mk_prod_edges2 ptc tc
| tc `elem` prod_tycons = [tc]
| tc `elem` new_tycons = if is_rec_nt tc
then []
else mk_prod_edges1 ptc (new_tc_rhs tc)
| otherwise = []
new_tc_rhs :: TyCon -> Type
new_tc_rhs tc = snd (newTyConRhs tc)
getTyCon :: TyThing -> Maybe TyCon
getTyCon (ATyCon tc) = Just tc
getTyCon _ = Nothing
findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
findLoopBreakers deps
= go [(tc,tc,ds) | (tc,ds) <- deps]
where
go edges = [ name
| CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
name <- tyConName tc : go edges']
\end{code}
%************************************************************************
%* *
Promotion calculation
%* *
%************************************************************************
See Note [Checking whether a group is promotable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only want to promote a TyCon if all its data constructors
are promotable; it'd be very odd to promote some but not others.
But the data constructors may mention this or other TyCons.
So we treat the recursive uses as all OK (ie promotable) and
do one pass to check that each TyCon is promotable.
Currently type synonyms are not promotable, though that
could change.
\begin{code}
isPromotableTyCon :: NameSet -> TyCon -> Bool
isPromotableTyCon rec_tycons tc
= isAlgTyCon tc
&& ok_kind (tyConKind tc)
&& case algTyConRhs tc of
DataTyCon { data_cons = cs } -> all ok_con cs
NewTyCon { data_con = c } -> ok_con c
AbstractTyCon {} -> False
DataFamilyTyCon {} -> False
where
ok_kind kind = all isLiftedTypeKind args && isLiftedTypeKind res
where
(args, res) = splitKindFunTys kind
ok_con con = all (isLiftedTypeKind . tyVarKind) ex_tvs
&& null eq_spec
&& null theta
&& all (isPromotableType rec_tycons) orig_arg_tys
where
(_, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig con
isPromotableType :: NameSet -> Type -> Bool
isPromotableType rec_tcs con_arg_ty
= go con_arg_ty
where
go (TyConApp tc tys) = tys `lengthIs` tyConArity tc
&& (tyConName tc `elemNameSet` rec_tcs
|| isJust (promotableTyCon_maybe tc))
&& all go tys
go (FunTy arg res) = go arg && go res
go (TyVarTy {}) = True
go _ = False
\end{code}
%************************************************************************
%* *
Role annotations
%* *
%************************************************************************
\begin{code}
type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
extractRoleAnnots :: TyClGroup Name -> RoleAnnots
extractRoleAnnots (TyClGroup { group_roles = roles })
= mkNameEnv [ (tycon, role_annot)
| role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
emptyRoleAnnots :: RoleAnnots
emptyRoleAnnots = emptyNameEnv
lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
lookupRoleAnnots = lookupNameEnv
\end{code}
%************************************************************************
%* *
Role inference
%* *
%************************************************************************
Note [Role inference]
~~~~~~~~~~~~~~~~~~~~~
The role inference algorithm datatype definitions to infer the roles on the
parameters. Although these roles are stored in the tycons, we can perform this
algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
roles field! Ah, the magic of laziness.
First, we choose appropriate initial roles. For families and classes, roles
(including initial roles) are N. For datatypes, we start with the role in the
role annotation (if any), or otherwise use Phantom. This is done in
initialRoleEnv1.
The function irGroup then propagates role information until it reaches a
fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
monad RoleM, which is a combination reader and state monad. In its state are
the current RoleEnv, which gets updated by role propagation, and an update
bit, which we use to know whether or not we've reached the fixpoint. The
environment of RoleM contains the tycon whose parameters we are inferring, and
a VarEnv from parameters to their positions, so we can update the RoleEnv.
Between tycons, this reader information is missing; it is added by
addRoleInferenceInfo.
There are two kinds of tycons to consider: algebraic ones (excluding classes)
and type synonyms. (Remember, families don't participate -- all their parameters
are N.) An algebraic tycon processes each of its datacons, in turn. Note that
a datacon's universally quantified parameters might be different from the parent
tycon's parameters, so we use the datacon's univ parameters in the mapping from
vars to positions. Note also that we don't want to infer roles for existentials
(they're all at N, too), so we put them in the set of local variables. As an
optimisation, we skip any tycons whose roles are already all Nominal, as there
nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
irType walks through a type, looking for uses of a variable of interest and
propagating role information. Because anything used under a phantom position
is at phantom and anything used under a nominal position is at nominal, the
irType function can assume that anything it sees is at representational. (The
other possibilities are pruned when they're encountered.)
The rest of the code is just plumbing.
How do we know that this algorithm is correct? It should meet the following
specification:
Let Z be a role context -- a mapping from variables to roles. The following
rules define the property (Z |- t : r), where t is a type and r is a role:
Z(a) = r' r' <= r
------------------------- RCVar
Z |- a : r
---------- RCConst
Z |- T : r -- T is a type constructor
Z |- t1 : r
Z |- t2 : N
-------------- RCApp
Z |- t1 t2 : r
forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
roles(T) = r_1 .. r_n
---------------------------------------------------- RCDApp
Z |- T t_1 .. t_n : R
Z, a:N |- t : r
---------------------- RCAll
Z |- forall a:k.t : r
We also have the following rules:
For all datacon_i in type T, where a_1 .. a_n are universally quantified
and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
then roles(T) = r_1 .. r_n
roles(->) = R, R
roles(~#) = N, N
With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
called from checkValidTycon.
Note [Role-checking data constructor arguments]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data T a where
MkT :: Eq b => F a -> (a->a) -> T (G a)
Then we want to check the roles at which 'a' is used
in MkT's type. We want to work on the user-written type,
so we need to take into account
* the arguments: (F a) and (a->a)
* the context: C a b
* the result type: (G a) -- this is in the eq_spec
\begin{code}
type RoleEnv = NameEnv [Role]
inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
inferRoles is_boot annots tycons
= let role_env = initialRoleEnv is_boot annots tycons
role_env' = irGroup role_env tycons in
\name -> case lookupNameEnv role_env' name of
Just roles -> roles
Nothing -> pprPanic "inferRoles" (ppr name)
initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
map (initialRoleEnv1 is_boot annots)
initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
initialRoleEnv1 is_boot annots_env tc
| isFamilyTyCon tc = (name, map (const Nominal) tyvars)
| isAlgTyCon tc
|| isSynTyCon tc = (name, default_roles)
| otherwise = pprPanic "initialRoleEnv1" (ppr tc)
where name = tyConName tc
tyvars = tyConTyVars tc
(kvs, tvs) = span isKindVar tyvars
role_annots
= case lookupNameEnv annots_env name of
Just (L _ (RoleAnnotDecl _ annots))
| annots `equalLength` tvs -> map unLoc annots
_ -> map (const Nothing) tvs
default_roles = map (const Nominal) kvs ++
zipWith orElse role_annots (repeat default_role)
default_role
| isClassTyCon tc = Nominal
| is_boot = Representational
| otherwise = Phantom
irGroup :: RoleEnv -> [TyCon] -> RoleEnv
irGroup env tcs
= let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
if update
then irGroup env' tcs
else env'
irTyCon :: TyCon -> RoleM ()
irTyCon tc
| isAlgTyCon tc
= do { old_roles <- lookupRoles tc
; unless (all (== Nominal) old_roles) $
do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
; addRoleInferenceInfo tc_name (tyConTyVars tc) $
mapM_ (irType emptyVarSet) (tyConStupidTheta tc)
; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
| Just (SynonymTyCon ty) <- synTyConRhs_maybe tc
= addRoleInferenceInfo tc_name (tyConTyVars tc) $
irType emptyVarSet ty
| otherwise
= return ()
where
tc_name = tyConName tc
irClass :: Name -> Class -> RoleM ()
irClass tc_name cls
= addRoleInferenceInfo tc_name cls_tvs $
mapM_ ir_at (classATs cls)
where
cls_tvs = classTyVars cls
cls_tv_set = mkVarSet cls_tvs
ir_at at_tc
= mapM_ (updateRole Nominal) (varSetElems nvars)
where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
irDataCon :: Name -> DataCon -> RoleM ()
irDataCon tc_name datacon
= addRoleInferenceInfo tc_name univ_tvs $
mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
where
(univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
ex_var_set = mkVarSet ex_tvs
irType :: VarSet -> Type -> RoleM ()
irType = go
where
go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
updateRole Representational tv
go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
go lcls (TyConApp tc tys)
= do { roles <- lookupRolesX tc
; zipWithM_ (go_app lcls) roles tys }
go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
go _ (LitTy {}) = return ()
go_app _ Phantom _ = return ()
go_app lcls Nominal ty = mark_nominal lcls ty
go_app lcls Representational ty = go lcls ty
mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
mapM_ (updateRole Nominal) (varSetElems nvars)
lookupRolesX :: TyCon -> RoleM [Role]
lookupRolesX tc
= do { roles <- lookupRoles tc
; return $ roles ++ repeat Nominal }
lookupRoles :: TyCon -> RoleM [Role]
lookupRoles tc
= do { env <- getRoleEnv
; case lookupNameEnv env (tyConName tc) of
Just roles -> return roles
Nothing -> return $ tyConRoles tc }
updateRole :: Role -> TyVar -> RoleM ()
updateRole role tv
= do { var_ns <- getVarNs
; case lookupVarEnv var_ns tv of
{ Nothing -> pprPanic "updateRole" (ppr tv)
; Just n -> do
{ name <- getTyConName
; updateRoleEnv name n role }}}
data RoleInferenceState = RIS { role_env :: RoleEnv
, update :: Bool }
type VarPositions = VarEnv Int
data RoleInferenceInfo = RII { var_ns :: VarPositions
, name :: Name }
newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
-> RoleInferenceState
-> (a, RoleInferenceState) }
instance Functor RoleM where
fmap = liftM
instance Applicative RoleM where
pure = return
(<*>) = ap
instance Monad RoleM where
return x = RM $ \_ state -> (x, state)
a >>= f = RM $ \m_info state -> let (a', state') = unRM a m_info state in
unRM (f a') m_info state'
runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
runRoleM env thing = (env', update)
where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state
state = RIS { role_env = env, update = False }
addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
addRoleInferenceInfo name tvs thing
= RM $ \_nothing state -> ASSERT( isNothing _nothing )
unRM thing (Just info) state
where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
getRoleEnv :: RoleM RoleEnv
getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
getVarNs :: RoleM VarPositions
getVarNs = RM $ \m_info state ->
case m_info of
Nothing -> panic "getVarNs"
Just (RII { var_ns = var_ns }) -> (var_ns, state)
getTyConName :: RoleM Name
getTyConName = RM $ \m_info state ->
case m_info of
Nothing -> panic "getTyConName"
Just (RII { name = name }) -> (name, state)
updateRoleEnv :: Name -> Int -> Role -> RoleM ()
updateRoleEnv name n role
= RM $ \_ state@(RIS { role_env = role_env }) -> ((),
case lookupNameEnv role_env name of
Nothing -> pprPanic "updateRoleEnv" (ppr name)
Just roles -> let (before, old_role : after) = splitAt n roles in
if role `ltRole` old_role
then let roles' = before ++ role : after
role_env' = extendNameEnv role_env name roles' in
RIS { role_env = role_env', update = True }
else state )
\end{code}