remove empty dir
[ghc-hetmet.git] / ghc / compiler / typecheck / TcTyDecls.lhs
index b684d2e..4ce5fed 100644 (file)
 %
-% (c) The AQUA Project, Glasgow University, 1996
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
 %
-\section[TcTyDecls]{Typecheck type declarations}
 
-\begin{code}
-#include "HsVersions.h"
+Analysis functions over data types.  Specficially
+       a) detecting recursive types
+       b) computing argument variances
 
-module TcTyDecls (
-       tcTyDecl,
-       tcConDecl,
-       mkDataBinds
-    ) where
+This stuff is only used for source-code decls; it's recorded in interface
+files for imported data types.
 
-IMP_Ubiq(){-uitous-}
-
-import HsSyn           ( TyDecl(..), ConDecl(..), BangType(..), HsExpr(..), 
-                         Match(..), GRHSsAndBinds(..), GRHS(..), OutPat(..), 
-                         HsBinds(..), HsLit, Stmt, Qualifier, ArithSeqInfo,
-                         PolyType, Fake, InPat,
-                         Bind(..), MonoBinds(..), Sig, 
-                         MonoType )
-import RnHsSyn         ( RenamedTyDecl(..), RenamedConDecl(..),
-                         RnName{-instance Outputable-}
-                       )
-import TcHsSyn         ( mkHsTyLam, mkHsDictLam, tcIdType,
-                         SYN_IE(TcHsBinds), TcIdOcc(..)
-                       )
-import Inst            ( newDicts, InstOrigin(..), Inst )
-import TcMonoType      ( tcMonoTypeKind, tcMonoType, tcPolyType, tcContext )
-import TcSimplify      ( tcSimplifyThetas )
-import TcType          ( tcInstTyVars, tcInstType, tcInstId )
-import TcEnv           ( tcLookupTyCon, tcLookupTyVar, tcLookupClass,
-                         newLocalId, newLocalIds, tcLookupClassByKey
-                       )
-import TcMonad         hiding ( rnMtoTcM )
-import TcKind          ( TcKind, unifyKind, mkTcArrowKind, mkTcTypeKind )
-
-import PprType         ( GenClass, GenType{-instance Outputable-},
-                         GenTyVar{-instance Outputable-}{-ToDo:possibly rm-}
-                       )
-import Class           ( GenClass{-instance Eq-}, classInstEnv )
-import Id              ( mkDataCon, dataConSig, mkRecordSelId, idType,
-                         dataConFieldLabels, dataConStrictMarks,
-                         StrictnessMark(..),
-                         GenId{-instance NamedThing-}
-                       )
-import FieldLabel
-import Kind            ( Kind, mkArrowKind, mkBoxedTypeKind )
-import SpecEnv         ( SpecEnv, nullSpecEnv )
-import Name            ( nameSrcLoc, isLocallyDefinedName, getSrcLoc,
-                         Name{-instance Ord3-}
-                       )
-import Outputable      ( Outputable(..), interpp'SP )
-import Pretty
-import TyCon           ( TyCon, NewOrData(..), mkSynTyCon, mkDataTyCon, isDataTyCon, 
-                         isNewTyCon, isSynTyCon, tyConDataCons
-                       )
-import Type            ( GenType, -- instances
-                         typeKind, getTyVar, tyVarsOfTypes, eqTy, splitSigmaTy,
-                         applyTyCon, mkTyVarTys, mkForAllTys, mkFunTy,
-                         splitFunTy, mkTyVarTy, getTyVar_maybe
-                       )
-import TyVar           ( tyVarKind, elementOfTyVarSet, GenTyVar{-instance Eq-} )
-import Unique          ( Unique {- instance Eq -}, evalClassKey )
-import UniqSet         ( emptyUniqSet, mkUniqSet, uniqSetToList, unionManyUniqSets, SYN_IE(UniqSet) )
-import Util            ( equivClasses, zipEqual, nOfThem, panic, assertPanic )
-\end{code}
 
 \begin{code}
-tcTyDecl :: RenamedTyDecl -> TcM s TyCon
-\end{code}
+module TcTyDecls(
+        calcTyConArgVrcs,
+       calcRecFlags, 
+       calcClassCycles, calcSynCycles
+    ) where
 
-Type synonym decls
-~~~~~~~~~~~~~~~~~~
+#include "HsVersions.h"
 
-\begin{code}
-tcTyDecl (TySynonym tycon_name tyvar_names rhs src_loc)
-  = tcAddSrcLoc src_loc $
-    tcAddErrCtxt (tySynCtxt tycon_name) $
-
-       -- Look up the pieces
-    tcLookupTyCon tycon_name                   `thenNF_Tc` \ (tycon_kind,  _, rec_tycon) ->
-    mapAndUnzipNF_Tc tcLookupTyVar tyvar_names `thenNF_Tc` \ (tyvar_kinds, rec_tyvars) ->
-
-       -- Look at the rhs
-    tcMonoTypeKind rhs                         `thenTc` \ (rhs_kind, rhs_ty) ->
-
-       -- Unify tycon kind with (k1->...->kn->rhs)
-    unifyKind tycon_kind
-       (foldr mkTcArrowKind rhs_kind tyvar_kinds)
-                                               `thenTc_`
-    let
-       -- Getting the TyCon's kind is a bit of a nuisance.  We can't use the tycon_kind,
-       -- because that's a TcKind and may not yet be fully unified with other kinds.
-       -- We could have augmented the tycon environment with a knot-tied kind,
-       -- but the simplest thing to do seems to be to get the Kind by (lazily)
-       -- looking at the tyvars and rhs_ty.
-       result_kind, final_tycon_kind :: Kind   -- NB not TcKind!
-       result_kind      = typeKind rhs_ty
-       final_tycon_kind = foldr (mkArrowKind . tyVarKind) result_kind rec_tyvars
-
-       -- Construct the tycon
-       tycon = mkSynTyCon (getName tycon_name)
-                          final_tycon_kind
-                          (length tyvar_names)
-                          rec_tyvars
-                          rhs_ty
-    in
-    returnTc tycon
+import TypeRep          ( Type(..), TyNote(..), PredType(..) )  -- friend
+import HsSyn           ( TyClDecl(..), HsPred(..), LTyClDecl, isClassDecl )
+import RnHsSyn         ( extractHsTyNames )
+import Type            ( predTypeRep, tcView )
+import HscTypes                ( TyThing(..), ModDetails(..) )
+import TyCon            ( TyCon, ArgVrcs, tyConArity, tyConDataCons, tyConTyVars,
+                          synTyConDefn, isSynTyCon, isAlgTyCon, 
+                         tyConName, isNewTyCon, isProductTyCon, tyConArgVrcs, newTyConRhs )
+import Class           ( classTyCon )
+import DataCon          ( dataConOrigArgTys )
+import Var              ( TyVar )
+import VarSet
+import Name            ( Name, isTyVarName )
+import NameEnv
+import NameSet
+import Digraph                 ( SCC(..), stronglyConnComp, stronglyConnCompR )
+import BasicTypes      ( RecFlag(..) )
+import SrcLoc          ( Located(..), unLoc )
+import Outputable
 \end{code}
 
-Algebraic data and newtype decls
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-\begin{code}
-tcTyDecl (TyData context tycon_name tyvar_names con_decls derivings pragmas src_loc)
-  = tcTyDataOrNew DataType context tycon_name tyvar_names con_decls derivings pragmas src_loc
-
-tcTyDecl (TyNew context tycon_name tyvar_names con_decl derivings pragmas src_loc)
-  = tcTyDataOrNew NewType  context tycon_name tyvar_names con_decl  derivings pragmas src_loc
-
-
-tcTyDataOrNew data_or_new context tycon_name tyvar_names con_decls derivings pragmas src_loc
-  = tcAddSrcLoc src_loc $
-    tcAddErrCtxt (tyDataCtxt tycon_name) $
-
-       -- Lookup the pieces
-    tcLookupTyCon tycon_name                   `thenNF_Tc` \ (tycon_kind, _, rec_tycon) ->
-    mapAndUnzipNF_Tc tcLookupTyVar tyvar_names `thenNF_Tc` \ (tyvar_kinds, rec_tyvars) ->
-    tc_derivs derivings                                `thenNF_Tc` \ derived_classes ->
-
-       -- Typecheck the context
-    tcContext context                          `thenTc` \ ctxt ->
-
-       -- Unify tycon kind with (k1->...->kn->Type)
-    unifyKind tycon_kind
-       (foldr mkTcArrowKind mkTcTypeKind tyvar_kinds)
-                                               `thenTc_`
-
-       -- Walk the condecls
-    mapTc (tcConDecl rec_tycon rec_tyvars ctxt) con_decls
-                                               `thenTc` \ con_ids ->
-    let
-       -- Construct the tycon
-       final_tycon_kind :: Kind                -- NB not TcKind!
-       final_tycon_kind = foldr (mkArrowKind . tyVarKind) mkBoxedTypeKind rec_tyvars
-
-       tycon = mkDataTyCon (getName tycon_name)
-                           final_tycon_kind
-                           rec_tyvars
-                           ctxt
-                           con_ids
-                           derived_classes
-                           data_or_new
-    in
-    returnTc tycon
-
-tc_derivs Nothing   = returnNF_Tc []
-tc_derivs (Just ds) = mapNF_Tc tc_deriv ds
-
-tc_deriv name
-  = tcLookupClass name `thenNF_Tc` \ (_, clas) ->
-    returnNF_Tc clas
-\end{code}
 
-Generating constructor/selector bindings for data declarations
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+%************************************************************************
+%*                                                                     *
+       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 have extractHsTyNames already
+
+  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 (PredTy (IParam _ ty))    = go ty      
+     go (PredTy (ClassP cls tys)) = go_s tys   -- Ignore class
+     go (NoteTy _ ty)            = go ty       
+     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}
-mkDataBinds :: [TyCon] -> TcM s ([Id], TcHsBinds s)
-mkDataBinds [] = returnTc ([], EmptyBinds)
-mkDataBinds (tycon : tycons) 
-  | isSynTyCon tycon = mkDataBinds tycons
-  | otherwise       = mkDataBinds_one tycon    `thenTc` \ (ids1, b1) ->
-                      mkDataBinds tycons       `thenTc` \ (ids2, b2) ->
-                      returnTc (ids1++ids2, b1 `ThenBinds` b2)
-
-mkDataBinds_one tycon
-  = ASSERT( isDataTyCon tycon || isNewTyCon tycon )
-    mapAndUnzipTc mkConstructor data_cons              `thenTc` \ (con_ids, con_binds) ->      
-    mapAndUnzipTc (mkRecordSelector tycon) groups      `thenTc` \ (sel_ids, sel_binds) ->
-    returnTc (con_ids ++ sel_ids, 
-             SingleBind $ NonRecBind $
-             foldr AndMonoBinds 
-                   (foldr AndMonoBinds EmptyMonoBinds sel_binds)
-                   con_binds
-    )
+calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
+calcSynCycles decls
+  = stronglyConnComp syn_edges
   where
-    data_cons = tyConDataCons tycon
-    fields = [ (con, field) | con   <- data_cons,
-                             field <- dataConFieldLabels con
-            ]
-
-       -- groups is list of fields that share a common name
-    groups = equivClasses cmp_name fields
-    cmp_name (_, field1) (_, field2) 
-       = fieldLabelName field1 `cmp` fieldLabelName field2
-\end{code}
+    syn_edges = [ (ldecl, unLoc (tcdLName decl), 
+                         mk_syn_edges (tcdSynRhs decl))
+               | ldecl@(L _ decl) <- decls ]
+
+    mk_syn_edges rhs = [ tc | tc <- nameSetToList (extractHsTyNames rhs), 
+                             not (isTyVarName tc) ]
 
-We're going to build a constructor that looks like:
 
-       data (Data a, C b) =>  T a b = T1 !a !Int b
+calcClassCycles :: [LTyClDecl Name] -> [[LTyClDecl Name]]
+calcClassCycles decls
+  = [decls | CyclicSCC decls <- stronglyConnComp cls_edges]
+  where
+    cls_edges = [ (ldecl, unLoc (tcdLName decl),       
+                         mk_cls_edges (unLoc (tcdCtxt decl)))
+               | ldecl@(L _ decl) <- decls, isClassDecl decl ]
 
-       T1 = /\ a b -> 
-            \d1::Data a, d2::C b ->
-            \p q r -> case p of { p ->
-                      case q of { q ->
-                      HsCon T1 [a,b] [p,q,r]}}
+    mk_cls_edges ctxt = [ cls | L _ (HsClassP cls _) <- ctxt ]
+\end{code}
 
-Notice that
 
-* d2 is thrown away --- a context in a data decl is used to make sure
-  one *could* construct dictionaries at the site the constructor
-  is used, but the dictionary isn't actually used.
+%************************************************************************
+%*                                                                     *
+       Deciding which type constructors are recursive
+%*                                                                     *
+%************************************************************************
+
+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 isHiBootTyCon. 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.
 
-* We have to check that we can construct Data dictionaries for
-  the types a and Int.  Once we've done that we can throw d1 away too.
+\begin{code}
+calcRecFlags :: ModDetails -> [TyThing] -> (Name -> RecFlag)
+-- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
+-- Any type constructors in boot_names are automatically considered loop breakers
+calcRecFlags boot_details tyclss
+  = is_rec
+  where
+    is_rec n | n `elemNameSet` rec_names = Recursive
+            | otherwise                 = NonRecursive
+
+    boot_name_set = md_exports boot_details
+    rec_names = boot_name_set    `unionNameSets` 
+               nt_loop_breakers  `unionNameSets`
+               prod_loop_breakers
+
+    all_tycons = [ tc | tycls <- tyclss,
+                          -- Recursion of newtypes/data types can happen via 
+                          -- the class TyCon, so tyclss includes the class tycons
+                       let tc = getTyCon tycls,
+                       not (tyConName tc `elemNameSet` boot_name_set) ]
+                          -- Remove the boot_name_set because they are going 
+                          -- to be loop breakers regardless.
+
+       -------------------------------------------------
+       --                      NOTE
+       -- These edge-construction loops rely on
+       -- every loop going via tyclss, the types and classes
+       -- in the module being compiled.  Stuff in interface 
+       -- files should be correctly marked.  If not (e.g. a
+       -- type synonym in a hi-boot file) we can get an infinite
+       -- loop.  We could program round this, but it'd make the code
+       -- rather less nice, so I'm not going to do that yet.
+
+       --------------- Newtypes ----------------------
+    new_tycons = filter isNewTyCon all_tycons
+    nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
+    is_rec_nt tc = tyConName tc  `elemNameSet` nt_loop_breakers
+       -- is_rec_nt is a locally-used helper function
+
+    nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
+
+    mk_nt_edges nt     -- Invariant: nt is a newtype
+       = concatMap (mk_nt_edges1 nt) (tcTyConsOfType (new_tc_rhs nt))
+                       -- tyConsOfType looks through synonyms
+
+    mk_nt_edges1 nt tc 
+       | tc `elem` new_tycons = [tc]           -- Loop
+               -- At this point we know that either it's a local *data* type,
+               -- or it's imported.  Either way, it can't form part of a newtype cycle
+       | otherwise = []
+
+       --------------- Product types ----------------------
+       -- The "prod_tycons" are the non-newtype products
+    prod_tycons = [tc | tc <- all_tycons, 
+                       not (isNewTyCon tc), isProductTyCon tc]
+    prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
+
+    prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
+       
+    mk_prod_edges tc   -- Invariant: tc is a product tycon
+       = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
+
+    mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (tcTyConsOfType ty)
+
+    mk_prod_edges2 ptc tc 
+       | tc `elem` prod_tycons   = [tc]                -- Local product
+       | tc `elem` new_tycons    = if is_rec_nt tc     -- Local newtype
+                                   then []
+                                   else mk_prod_edges1 ptc (new_tc_rhs tc)
+               -- At this point we know that either it's a local non-product data type,
+               -- or it's imported.  Either way, it can't form part of a cycle
+       | otherwise = []
+                       
+new_tc_rhs tc = snd (newTyConRhs tc)   -- Ignore the type variables
+
+getTyCon (ATyCon tc) = tc
+getTyCon (AClass cl) = classTyCon cl
+
+findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
+-- Finds a set of tycons that cut all loops
+findLoopBreakers deps
+  = go [(tc,tc,ds) | (tc,ds) <- deps]
+  where
+    go edges = [ name
+              | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompR edges,
+                name <- tyConName tc : go edges']
+\end{code}
 
-* We use (case p of ...) to evaluate p, rather than "seq" because
-  all that matters is that the arguments are evaluated.  "seq" is 
-  very careful to preserve evaluation order, which we don't need
-  to be here.
+These two functions know about type representations, so they could be
+in Type or TcType -- but they are very specialised to this module, so 
+I've chosen to put them here.
 
 \begin{code}
-mkConstructor con_id
-  | not (isLocallyDefinedName (getName con_id))
-  = returnTc (con_id, EmptyMonoBinds)
-
-  | otherwise  -- It is locally defined
-  = tcInstId con_id                    `thenNF_Tc` \ (tc_tyvars, tc_theta, tc_tau) ->
-    newDicts DataDeclOrigin tc_theta   `thenNF_Tc` \ (_, dicts) ->
-    let
-       (tc_arg_tys, tc_result_ty) = splitFunTy tc_tau
-       n_args = length tc_arg_tys
-    in
-    newLocalIds (nOfThem n_args SLIT("con")) tc_arg_tys        `thenNF_Tc` \ args ->
-
-       -- Check that all the types of all the strict arguments are in Eval
-    tcLookupClassByKey evalClassKey    `thenNF_Tc` \ eval_clas ->
-    let
-       (_,theta,tau) = splitSigmaTy (idType con_id)
-       (arg_tys, _)  = splitFunTy tau
-       strict_marks  = dataConStrictMarks con_id
-       eval_theta    = [ (eval_clas,arg_ty) 
-                       | (arg_ty, MarkedStrict) <- zipEqual "strict_args" 
-                                                       arg_tys strict_marks
-                       ]
-    in
-    tcSimplifyThetas classInstEnv theta eval_theta     `thenTc` \ eval_theta' ->
-    checkTc (null eval_theta')
-           (missingEvalErr con_id eval_theta')         `thenTc_`
-
-       -- Build the data constructor
-    let
-       con_rhs = mkHsTyLam tc_tyvars $
-                 mkHsDictLam dicts $
-                 mk_pat_match args $
-                 mk_case (zipEqual "strict_args" args strict_marks) $
-                 HsCon con_id (mkTyVarTys tc_tyvars) (map HsVar args)
-
-       mk_pat_match []         body = body
-       mk_pat_match (arg:args) body = HsLam $
-                                      PatMatch (VarPat arg) $
-                                      SimpleMatch (mk_pat_match args body)
-
-       mk_case [] body = body
-       mk_case ((arg,MarkedStrict):args) body = HsCase (HsVar arg) 
-                                                        [PatMatch (VarPat arg) $
-                                                         SimpleMatch (mk_case args body)]
-                                                        src_loc
-       mk_case (_:args) body = mk_case args body
-
-       src_loc = nameSrcLoc (getName con_id)
-    in
-
-    returnTc (con_id, VarMonoBind (RealId con_id) con_rhs)              
+tcTyConsOfType :: Type -> [TyCon]
+-- tcTyConsOfType looks through all synonyms, but not through any newtypes.  
+-- When it finds a Class, it returns the class TyCon.  The reaons it's here
+-- (not in Type.lhs) is because it is newtype-aware.
+tcTyConsOfType ty 
+  = nameEnvElts (go ty)
+  where
+     go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
+     go ty | Just ty' <- tcView ty = go ty'
+     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 (PredTy (IParam _ ty))     = go ty
+     go (PredTy (ClassP cls tys))  = go_tc (classTyCon cls) tys
+     go (ForAllTy _ ty)                   = go ty
+
+     go_tc tc tys = extendNameEnv (go_s tys) (tyConName tc) tc
+     go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
 \end{code}
 
-We're going to build a record selector that looks like this:
 
-       data T a b c = T1 { op :: a, ...}
-                    | T2 { op :: a, ...}
-                    | T3
+%************************************************************************
+%*                                                                     *
+       Compuing TyCon argument variances
+%*                                                                     *
+%************************************************************************
 
-       sel :: forall a b c. T a b c -> a
-       sel = /\ a b c -> \ T1 { sel = x } -> x
-                           T2 { sel = 2 } -> x
+Computing the tyConArgVrcs info
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Note that the selector Id itself is used as the field
-label; it has to be an Id, you see!
+@tyConArgVrcs@ gives a list of (occPos,occNeg) flags, one for each
+tyvar.  For @AlgTyCon@s and @SynTyCon@s, this info must be precomputed
+separately.  Note that this is information about occurrences of type
+variables, not usages of term variables.
 
-\begin{code}
-mkRecordSelector tycon fields@((first_con, first_field_label) : other_fields)
-               -- These fields all have the same name, but are from
-               -- different constructors in the data type
-  = let
-       field_ty   = fieldLabelType first_field_label
-       field_name = fieldLabelName first_field_label
-       other_tys  = [fieldLabelType fl | (_, fl) <- other_fields]
-       (tyvars, _, _, _) = dataConSig first_con
-        data_ty  = applyTyCon tycon (mkTyVarTys tyvars)
-       -- tyvars of first_con may be free in field_ty
-    in
-   
-       -- Check that all the fields in the group have the same type
-       -- This check assumes that all the constructors of a given
-       -- data type use the same type variables
-    checkTc (all (eqTy field_ty) other_tys)
-           (fieldTypeMisMatch field_name)      `thenTc_`
-    
-       -- Create an Id for the field itself
-    tcInstTyVars tyvars                        `thenNF_Tc` \ (tyvars', tyvar_tys, tenv) ->
-    tcInstType tenv field_ty           `thenNF_Tc` \ field_ty' ->
-    let
-      data_ty' = applyTyCon tycon tyvar_tys
-    in
-    newLocalId SLIT("x") field_ty'     `thenNF_Tc` \ field_id ->
-    newLocalId SLIT("r") data_ty'      `thenNF_Tc` \ record_id ->
-
-       -- Now build the selector
-    let
-      selector_ty :: Type
-      selector_ty  = mkForAllTys tyvars $      
-                    mkFunTy data_ty $
-                    field_ty
-      
-      selector_id :: Id
-      selector_id = mkRecordSelId first_field_label selector_ty
-
-       -- HsSyn is dreadfully verbose for defining the selector!
-      selector_rhs = mkHsTyLam tyvars' $
-                    HsLam $
-                    PatMatch (VarPat record_id) $
-                    SimpleMatch $
-                    selector_body
-
-      selector_body = HsCase (HsVar record_id) (map mk_match fields) (getSrcLoc tycon)
-
-      mk_match (con_id, field_label) 
-       = PatMatch (RecPat con_id data_ty' [(selector_id, VarPat field_id, False)]) $
-         SimpleMatch $
-         HsVar field_id
-    in
-    returnTc (selector_id, if isLocallyDefinedName (getName tycon)
-                          then VarMonoBind (RealId selector_id) selector_rhs
-                          else EmptyMonoBinds)
-\end{code}
+The function @calcTyConArgVrcs@ must be passed a list of *algebraic or
+syntycons only* such that all tycons referred to (by mutual recursion)
+appear in the list.  The fixpointing will be done on this set of
+tycons as a whole.  It returns a list of @tyconVrcInfo@ data, ready to
+be (knot-tyingly?) stuck back into the appropriate fields.
 
-Constructors
-~~~~~~~~~~~~
 \begin{code}
-tcConDecl :: TyCon -> [TyVar] -> [(Class,Type)] -> RenamedConDecl -> TcM s Id
-
-tcConDecl tycon tyvars ctxt (ConDecl name btys src_loc)
-  = tcDataCon tycon tyvars ctxt name btys src_loc
-
-tcConDecl tycon tyvars ctxt (ConOpDecl bty1 op bty2 src_loc)
-  = tcDataCon tycon tyvars ctxt op [bty1,bty2] src_loc
-
-tcConDecl tycon tyvars ctxt (NewConDecl name ty src_loc)
-  = tcAddSrcLoc src_loc        $
-    tcMonoType ty `thenTc` \ arg_ty ->
-    let
-      data_con = mkDataCon (getName name)
-                          [NotMarkedStrict]
-                          [{- No labelled fields -}]
-                          tyvars
-                          ctxt
-                          [arg_ty]
-                          tycon
-                       -- nullSpecEnv
-    in
-    returnTc data_con
-
-tcConDecl tycon tyvars ctxt (RecConDecl name fields src_loc)
-  = tcAddSrcLoc src_loc        $
-    mapTc tcField fields       `thenTc` \ field_label_infos_s ->
-    let
-      field_label_infos = concat field_label_infos_s
-      stricts           = [strict | (_, _, strict) <- field_label_infos]
-      arg_tys          = [ty     | (_, ty, _)     <- field_label_infos]
-
-      field_labels      = [ mkFieldLabel (getName name) ty tag 
-                         | ((name, ty, _), tag) <- field_label_infos `zip` allFieldLabelTags ]
-
-      data_con = mkDataCon (getName name)
-                          stricts
-                          field_labels
-                          tyvars
-                          (thinContext arg_tys ctxt)
-                          arg_tys
-                          tycon
-                       -- nullSpecEnv
-    in
-    returnTc data_con
-
-tcField (field_label_names, bty)
-  = tcPolyType (get_pty bty)   `thenTc` \ field_ty ->
-    returnTc [(name, field_ty, get_strictness bty) | name <- field_label_names]
-
-tcDataCon tycon tyvars ctxt name btys src_loc
-  = tcAddSrcLoc src_loc        $
-    let
-       stricts = map get_strictness btys
-       tys     = map get_pty btys
-    in
-    mapTc tcPolyType tys `thenTc` \ arg_tys ->
-    let
-      data_con = mkDataCon (getName name)
-                          stricts
-                          [{- No field labels -}]
-                          tyvars
-                          (thinContext arg_tys ctxt)
-                          arg_tys
-                          tycon
-                       -- nullSpecEnv
-    in
-    returnTc data_con
-
--- The context for a data constructor should be limited to
--- the type variables mentioned in the arg_tys
-thinContext arg_tys ctxt
-  = filter in_arg_tys ctxt
+calcTyConArgVrcs :: [TyThing] -> Name -> ArgVrcs
+-- Gives arg variances for TyCons, 
+-- including the class TyCon of a class
+calcTyConArgVrcs tyclss
+  = get_vrc
   where
-      arg_tyvars = tyVarsOfTypes arg_tys
-      in_arg_tys (clas,ty) = getTyVar "tcDataCon" ty `elementOfTyVarSet` arg_tyvars
-  
-get_strictness (Banged   _) = MarkedStrict
-get_strictness (Unbanged _) = NotMarkedStrict
-
-get_pty (Banged ty)   = ty
-get_pty (Unbanged ty) = ty
+    tycons = map getTyCon tyclss
+
+       -- We should only look up things that are in the map
+    get_vrc n = case lookupNameEnv final_oi n of
+                 Just (_, pms) -> pms
+                 Nothing -> pprPanic "calcVrcs" (ppr n)
+
+       -- We are going to fold over this map,
+       -- so we need the TyCon in the range
+    final_oi :: NameEnv (TyCon, ArgVrcs)
+    final_oi = tcaoFix initial_oi
+
+    initial_oi :: NameEnv (TyCon, ArgVrcs)
+    initial_oi = mkNameEnv [(tyConName tc, (tc, initial tc))
+                          | tc <- tycons]
+    initial tc = replicate (tyConArity tc) (False,False)
+
+    tcaoFix :: NameEnv (TyCon, ArgVrcs)   -- initial ArgVrcs per tycon
+           -> NameEnv (TyCon, ArgVrcs)   -- fixpointed ArgVrcs per tycon
+    tcaoFix oi 
+       | changed   = tcaoFix oi'
+       | otherwise = oi'
+       where
+        (changed,oi') = foldNameEnv iterate (False,oi) oi
+
+    iterate (tc, pms) (changed,oi')
+      =        (changed || (pms /= pms'),
+        extendNameEnv oi' (tyConName tc) (tc, pms'))
+      where
+       pms' = tcaoIter oi' tc  -- seq not simult
+
+    tcaoIter :: NameEnv (TyCon, ArgVrcs)  -- reference ArgVrcs (initial)
+            -> TyCon                     -- tycon to update
+            -> ArgVrcs                   -- new ArgVrcs for tycon
+
+    tcaoIter oi tc | isAlgTyCon tc
+      = map (\v -> anyVrc (vrcInTy (lookup oi) v) argtys) vs
+      where
+               data_cons = tyConDataCons tc
+               vs        = tyConTyVars tc
+               argtys    = concatMap dataConOrigArgTys data_cons       -- Rep? or Orig?
+
+    tcaoIter oi tc | isSynTyCon tc
+      = let (tyvs,ty) = synTyConDefn tc
+                        -- we use the already-computed result for tycons not in this SCC
+        in  map (\v -> vrcInTy (lookup oi) v ty) tyvs
+
+    lookup oi tc = case lookupNameEnv oi (tyConName tc) of
+                       Just (_, pms) -> pms
+                       Nothing       -> tyConArgVrcs tc
+        -- We use the already-computed result for tycons not in this SCC
 \end{code}
 
 
+Variance of tyvars in a type
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A general variance-check function.  We pass a function for determining
+the @ArgVrc@s of a tycon; when fixpointing this refers to the current
+value; otherwise this should be looked up from the tycon's own
+tyConArgVrcs.  Again, it knows the representation of Types.
+
+\begin{code}
+vrcInTy :: (TyCon -> ArgVrcs)  -- function to get argVrcs of a tycon (break out of recursion)
+        -> TyVar               -- tyvar to check Vrcs of
+        -> Type                -- type to check for occ in
+        -> (Bool,Bool)         -- (occurs positively, occurs negatively)
+
+vrcInTy fao v (NoteTy (FTVNote ftv) ty) = if elemVarSet v ftv
+                                         then vrcInTy fao v ty
+                                         else (False,False)
+                       -- note that ftv cannot be calculated as occPos||occNeg,
+                       -- since if a tyvar occurs only as unused tyconarg,
+                       -- occPos==occNeg==False, but ftv=True
+
+vrcInTy fao v (TyVarTy v')              = if v==v'
+                                         then (True,False)
+                                         else (False,False)
+
+vrcInTy fao v (AppTy ty1 ty2)           = if vrcInTy fao v ty2 /= (False,False)
+                                          then (True,True)
+                                          else vrcInTy fao v ty1
+                        -- ty1 is probably unknown (or it would have been beta-reduced);
+                        -- hence if v occurs in ty2 at all then it could occur with
+                        -- either variance.  Otherwise it occurs as it does in ty1.
+
+vrcInTy fao v (FunTy ty1 ty2)           = negVrc (vrcInTy fao v ty1)
+                                          `orVrc`
+                                          vrcInTy fao v ty2
+                                        
+vrcInTy fao v (ForAllTy v' ty)          = if v==v'
+                                         then (False,False)
+                                         else vrcInTy fao v ty
+
+vrcInTy fao v (TyConApp tc tys)         = let pms1 = map (vrcInTy fao v) tys
+                                             pms2 = fao tc
+                                         in  orVrcs (zipWith timesVrc pms1 pms2)
+
+vrcInTy fao v (PredTy st) = vrcInTy fao v (predTypeRep st)
+\end{code}
+
+Variance algebra
+~~~~~~~~~~~~~~~~
 
-Errors and contexts
-~~~~~~~~~~~~~~~~~~~
 \begin{code}
-tySynCtxt tycon_name sty
-  = ppCat [ppStr "In the type declaration for", ppr sty tycon_name]
+orVrc :: (Bool,Bool) -> (Bool,Bool) -> (Bool,Bool)
+orVrc (p1,m1) (p2,m2) = (p1||p2,m1||m2)
 
-tyDataCtxt tycon_name sty
-  = ppCat [ppStr "In the data declaration for", ppr sty tycon_name]
+orVrcs :: [(Bool,Bool)] -> (Bool,Bool)
+orVrcs = foldl orVrc (False,False)
 
-tyNewCtxt tycon_name sty
-  = ppCat [ppStr "In the newtype declaration for", ppr sty tycon_name]
+negVrc :: (Bool,Bool) -> (Bool,Bool)
+negVrc (p1,m1) = (m1,p1)
 
-fieldTypeMisMatch field_name sty
-  = ppSep [ppStr "Declared types differ for field", ppr sty field_name]
+anyVrc :: (a -> (Bool,Bool)) -> [a] -> (Bool,Bool)
+anyVrc p as = foldl (\ pm a -> pm `orVrc` p a)
+                    (False,False) as
 
-missingEvalErr con eval_theta sty
-  = ppCat [ppStr "Missing Eval context for constructor", 
-          ppQuote (ppr sty con),
-          ppStr ":", ppr sty eval_theta]
+timesVrc :: (Bool,Bool) -> (Bool,Bool) -> (Bool,Bool)
+timesVrc (p1,m1) (p2,m2) = (p1 && p2 || m1 && m2,
+                           p1 && m2 || m1 && p2)
 \end{code}