TcTyClsDecls.hs

{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1996-1998


TcTyClsDecls: Typecheck type and class declarations
-}

{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}

module TcTyClsDecls (
        tcTyAndClassDecls, tcAddImplicits,

        -- Functions used by TcInstDcls to check
        -- data/type family instance declarations
        kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
        tcFamTyPats, tcTyFamInstEqn, famTyConShape,
        tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
        wrongKindOfFamily, dataConCtxt
    ) where

#include "HsVersions.h"

import HsSyn
import HscTypes
import BuildTyCl
import TcRnMonad
import TcEnv
import TcValidity
import TcHsSyn
import TcTyDecls
import TcClassDcl
import TcUnify
import TcHsType
import TcMType
import TysWiredIn ( unitTy )
import TcType
import FamInst
import FamInstEnv
import Coercion
import Type
import TyCoRep   -- for checkValidRoles
import Kind
import Class
import CoAxiom
import TyCon
import DataCon
import Id
import Var
import VarEnv
import VarSet
import Module
import Name
import NameSet
import NameEnv
import RnEnv
import Outputable
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
import Unique
import BasicTypes
import qualified GHC.LanguageExtensions as LangExt

import Control.Monad
import Data.List

{-
************************************************************************
*                                                                      *
\subsection{Type checking for type and class declarations}
*                                                                      *
************************************************************************

Note [Grouping of type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
connected component of mutually dependent types and classes. We kind check and
type check each group separately to enhance kind polymorphism. Take the
following example:

  type Id a = a
  data X = X (Id Int)

If we were to kind check the two declarations together, we would give Id the
kind * -> *, since we apply it to an Int in the definition of X. But we can do
better than that, since Id really is kind polymorphic, and should get kind
forall (k::*). k -> k. Since it does not depend on anything else, it can be
kind-checked by itself, hence getting the most general kind. We then kind check
X, which works fine because we then know the polymorphic kind of Id, and simply
instantiate k to *.

Note [Check role annotations in a second pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Role inference potentially depends on the types of all of the datacons declared
in a mutually recursive group. The validity of a role annotation, in turn,
depends on the result of role inference. Because the types of datacons might
be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
*all* the tycons in a group for validity before checking *any* of the roles.
Thus, we take two passes over the resulting tycons, first checking for general
validity and then checking for valid role annotations.
-}

tcTyAndClassDecls :: [TyClGroup Name]   -- Mutually-recursive groups in dependency order
                  -> TcM TcGblEnv       -- Input env extended by types and classes
                                        -- and their implicit Ids,DataCons
-- Fails if there are any errors
tcTyAndClassDecls tyclds_s
  = checkNoErrs $       -- The code recovers internally, but if anything gave rise to
                        -- an error we'd better stop now, to avoid a cascade
    fold_env tyclds_s   -- Type check each group in dependency order folding the global env
  where
    fold_env :: [TyClGroup Name] -> TcM TcGblEnv
    fold_env [] = getGblEnv
    fold_env (tyclds:tyclds_s)
      = do { tcg_env <- tcTyClGroup tyclds
           ; setGblEnv tcg_env $ fold_env tyclds_s }
             -- remaining groups are typecheck in the extended global env

tcTyClGroup :: TyClGroup Name -> TcM TcGblEnv
-- Typecheck one strongly-connected component of type and class decls
tcTyClGroup tyclds
  = do {    -- Step 1: kind-check this group and returns the final
            -- (possibly-polymorphic) kind of each TyCon and Class
            -- See Note [Kind checking for type and class decls]
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))

            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
       ; let role_annots = extractRoleAnnots tyclds
             decls = group_tyclds tyclds
       ; tyclss <- fixM $ \ ~rec_tyclss -> do
           { is_boot   <- tcIsHsBootOrSig
           ; self_boot <- tcSelfBootInfo
           ; let rec_flags = calcRecFlags self_boot is_boot
                                          role_annots rec_tyclss

                 -- Populate environment with knot-tied ATyCon for TyCons
                 -- NB: if the decls mention any ill-staged data cons
                 -- (see Note [Recusion and promoting data constructors])
                 -- we will have failed already in kcTyClGroup, so no worries here
           ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $

                 -- Also extend the local type envt with bindings giving
                 -- the (polymorphic) kind of each knot-tied TyCon or Class
                 -- See Note [Type checking recursive type and class declarations]
             tcExtendKindEnv2 (map mkTcTyConPair tc_tycons)              $

                 -- Kind and type check declarations for this group
             mapM (tcTyClDecl rec_flags) decls }

           -- Step 3: Perform the validity check
           -- We can do this now because we are done with the recursive knot
           -- Do it before Step 4 (adding implicit things) because the latter
           -- expects well-formed TyCons
       ; traceTc "Starting validity check" (ppr tyclss)
       ; tyclss <- mapM checkValidTyCl tyclss
       ; traceTc "Done validity check" (ppr tyclss)
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]

           -- Step 4: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
       ; tcExtendTyConEnv tyclss $
         tcAddImplicits tyclss }
  where
    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                  , ppr (tyConBinders tc) <> comma
                                  , ppr (tyConResKind tc) ])

zipRecTyClss :: [TcTyCon]
             -> [TyCon]           -- Knot-tied
             -> [(Name,TyThing)]
-- Build a name-TyThing mapping for the TyCons bound by decls
-- being careful not to look at the knot-tied [TyThing]
-- The TyThings in the result list must have a visible ATyCon,
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
  where
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons

    add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
    add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)

    add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
    add_one_tc tc env = extendNameEnv env (tyConName tc) tc

    get name = case lookupNameEnv rec_tc_env name of
                 Just tc -> tc
                 other   -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)

{-
************************************************************************
*                                                                      *
                Kind checking
*                                                                      *
************************************************************************

Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

   1. Make up a kind variable for each parameter of the *data* type, class,
      and closed type family decls, and extend the kind environment (which is
      in the TcLclEnv)

   2. Dependency-analyse the type *synonyms* (which must be non-recursive),
      and kind-check them in dependency order.  Extend the kind envt.

   3. Kind check the data type and class decls

We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:

  class C a where
     op :: D b => a -> b -> b

  class D c where
     bop :: (Monad c) => ...

Here, the kind of the locally-polymorphic type variable "b"
depends on *all the uses of class D*.  For example, the use of
Monad c in bop's type signature means that D must have kind Type->Type.

However type synonyms work differently.  They can have kinds which don't
just involve (->) and *:
        type R = Int#           -- Kind #
        type S a = Array# a     -- Kind * -> #
        type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
and a kind variable can't unify with UnboxedTypeKind.

So we must infer the kinds of type synonyms from their right-hand
sides *first* and then use them, whereas for the mutually recursive
data types D we bring into scope kind bindings D -> k, where k is a
kind variable, and do inference.

NB: synonyms can be mutually recursive with data type declarations though!
   type T = D -> D
   data D = MkD Int T

Open type families
~~~~~~~~~~~~~~~~~~
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

The kind of an open type family is solely determinded by its kind signature;
hence, only kind signatures participate in the construction of the initial
kind environment (as constructed by `getInitialKind'). In fact, we ignore
instances of families altogether in the following. However, we need to include
the kinds of *associated* families into the construction of the initial kind
environment. (This is handled by `allDecls').


See also Note [Kind checking recursive type and class declarations]

-}

kcTyClGroup :: TyClGroup Name -> TcM [TcTyCon]
-- Kind check this group, kind generalize, and return the resulting local env
-- This bindds the TyCons and Classes of the group, but not the DataCons
-- See Note [Kind checking for type and class decls]
-- Third return value is Nothing if the tycon be unsaturated; otherwise,
-- the arity
kcTyClGroup (TyClGroup { group_tyclds = decls })
  = do  { mod <- getModule
        ; traceTc "kcTyClGroup" (text "module" <+> ppr mod $$ vcat (map ppr decls))

          -- Kind checking;
          --    1. Bind kind variables for non-synonyms
          --    2. Kind-check synonyms, and bind kinds of those synonyms
          --    3. Kind-check non-synonyms
          --    4. Generalise the inferred kinds
          -- See Note [Kind checking for type and class decls]

        ; lcl_env <- solveEqualities $
          do {
               -- Step 1: Bind kind variables for non-synonyms
               let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
             ; initial_kinds <- getInitialKinds non_syn_decls
             ; traceTc "kcTyClGroup: initial kinds" $
               vcat (map pp_initial_kind initial_kinds)

             -- Step 2: Set initial envt, kind-check the synonyms
             ; lcl_env <- tcExtendKindEnv2 initial_kinds $
                          kcSynDecls (calcSynCycles syn_decls)

             -- Step 3: Set extended envt, kind-check the non-synonyms
             ; setLclEnv lcl_env $
               mapM_ kcLTyClDecl non_syn_decls

             ; return lcl_env }

             -- Step 4: generalisation
             -- Kind checking done for this group
             -- Now we have to kind generalize the flexis
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls

        ; traceTc "kcTyClGroup result" (vcat (map pp_res res))
        ; return res }

  where
    generalise :: TcTypeEnv -> Name -> TcM TcTyCon
    -- For polymorphic things this is a no-op
    generalise kind_env name
      = do { let tc = case lookupNameEnv kind_env name of
                        Just (ATcTyCon tc) -> tc
                        _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
                 kc_binders  = tyConBinders tc
                 kc_res_kind = tyConResKind tc
           ; kvs <- kindGeneralize (mkForAllTys kc_binders kc_res_kind)
           ; (kc_binders', kc_res_kind') <- zonkTcKindToKind kc_binders kc_res_kind

                      -- Make sure kc_kind' has the final, zonked kind variables
           ; traceTc "Generalise kind" $
             vcat [ ppr name, ppr kc_binders, ppr kc_res_kind
                  , ppr kvs, ppr kc_binders', ppr kc_res_kind' ]

           ; return (mkTcTyCon name
                               (mkNamedBinders Invisible kvs ++ kc_binders')
                               kc_res_kind'
                               (mightBeUnsaturatedTyCon tc)) }

    generaliseTCD :: TcTypeEnv
                  -> LTyClDecl Name -> TcM [TcTyCon]
    generaliseTCD kind_env (L _ decl)
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

      | FamDecl { tcdFam = fam } <- decl
      = do { res <- generaliseFamDecl kind_env fam
           ; return [res] }

      | otherwise
      = do { res <- generalise kind_env (tcdName decl)
           ; return [res] }

    generaliseFamDecl :: TcTypeEnv
                      -> FamilyDecl Name -> TcM TcTyCon
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name

    pp_initial_kind (name, ATcTyCon tc)
      = ppr name <+> dcolon <+> ppr (tyConKind tc)
    pp_initial_kind pair
      = ppr pair

    pp_res tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

mkTcTyConPair :: TcTyCon -> (Name, TcTyThing)
-- Makes a binding to put in the local envt, binding
-- a name to a TcTyCon
mkTcTyConPair tc
  = (getName tc, ATcTyCon tc)

mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
mk_thing_env [] = []
mk_thing_env (decl : decls)
  | L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
  = (nm, APromotionErr ClassPE) :
    (map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
    (mk_thing_env decls)

  | otherwise
  = (tcdName (unLoc decl), APromotionErr TyConPE) :
    (mk_thing_env decls)

getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
getInitialKinds decls
  = tcExtendKindEnv2 (mk_thing_env decls) $
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }

getInitialKind :: TyClDecl Name
               -> TcM [(Name, TcTyThing)]    -- Mixture of ATcTyCon and APromotionErr
-- Allocate a fresh kind variable for each TyCon and Class
-- For each tycon, return   (name, ATcTyCon (TcCyCon with kind k))
--                 where k is the kind of tc, derived from the LHS
--                       of the definition (and probably including
--                       kind unification variables)
--      Example: data T a b = ...
--      return (T, kv1 -> kv2 -> kv3)
--
-- This pass deals with (ie incorporates into the kind it produces)
--   * The kind signatures on type-variable binders
--   * The result kinds signature on a TyClDecl
--
-- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
--    See Note [ARecDataCon: Recursion and promoting data constructors]
--
-- No family instances are passed to getInitialKinds

getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
  = do { (cl_binders, cl_kind, inner_prs) <-
           kcHsTyVarBndrs cusk False True ktvs $
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
              ; return (constraintKind, inner_prs) }
       ; cl_binders <- mapM zonkTcTyBinder cl_binders
       ; cl_kind    <- zonkTcType cl_kind
       ; let main_pr = mkTcTyConPair (mkTcTyCon name cl_binders cl_kind True)
       ; return (main_pr : inner_prs) }
  where
    cusk = hsDeclHasCusk decl

getInitialKind decl@(DataDecl { tcdLName = L _ name
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_cons = cons } })
  = do  { (decl_binders, decl_kind, _) <-
           kcHsTyVarBndrs (hsDeclHasCusk decl) False True ktvs $
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
              ; return (res_k, ()) }
        ; decl_binders <- mapM zonkTcTyBinder decl_binders
        ; decl_kind    <- zonkTcType decl_kind
        ; let main_pr = mkTcTyConPair (mkTcTyCon name decl_binders decl_kind True)
              inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                          | L _ con' <- cons, con <- getConNames con' ]
        ; return (main_pr : inner_prs) }

getInitialKind (FamDecl { tcdFam = decl })
  = getFamDeclInitialKind Nothing decl

getInitialKind decl@(SynDecl {})
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                       -> [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds mb_cusk decls
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
    concatMapM (addLocM (getFamDeclInitialKind mb_cusk)) decls

getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                      -> FamilyDecl Name
                      -> TcM [(Name, TcTyThing)]
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
  = do { (fam_binders, fam_kind, _) <-
           kcHsTyVarBndrs cusk open True ktvs $
           do { res_k <- case resultSig of
                      KindSig ki                        -> tcLHsKind ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki
                      _ -- open type families have * return kind by default
                        | open                     -> return liftedTypeKind
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
              ; return (res_k, ()) }
       ; fam_binders <- mapM zonkTcTyBinder fam_binders
       ; fam_kind    <- zonkTcType fam_kind
       ; return [ mkTcTyConPair (mkTcTyCon name fam_binders fam_kind unsat) ] }
  where
    cusk  = famDeclHasCusk mb_cusk decl
    (open, unsat) = case info of
      DataFamily         -> (True,  True)
      OpenTypeFamily     -> (True,  False)
      ClosedTypeFamily _ -> (False, False)

----------------
kcSynDecls :: [SCC (LTyClDecl Name)]
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
kcSynDecls (group : groups)
  = do  { tc <- kcSynDecl1 group
        ; traceTc "kcSynDecl" (ppr tc <+> dcolon <+> ppr (tyConKind tc))
        ; tcExtendKindEnv2 [ mkTcTyConPair tc ] $
          kcSynDecls groups }

kcSynDecl1 :: SCC (LTyClDecl Name)
           -> TcM TcTyCon -- Kind bindings
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons

kcSynDecl :: TyClDecl Name -> TcM TcTyCon
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
                        , tcdRhs = rhs })
  -- Returns a possibly-unzonked kind
  = tcAddDeclCtxt decl $
    do { (syn_binders, syn_kind, _) <-
           kcHsTyVarBndrs (hsDeclHasCusk decl) False True hs_tvs $
           do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
              ; (_, rhs_kind) <- tcLHsType rhs
              ; traceTc "kcd2" (ppr name)
              ; return (rhs_kind, ()) }
       ; return (mkTcTyCon name syn_binders syn_kind False) }
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)

------------------------------------------------------------------------
kcLTyClDecl :: LTyClDecl Name -> TcM ()
  -- See Note [Kind checking for type and class decls]
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

kcTyClDecl :: TyClDecl Name -> TcM ()
-- This function is used solely for its side effect on kind variables
-- NB kind signatures on the type variables and
--    result kind signature have already been dealt with
--    by getInitialKind, so we can ignore them here.

kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
  = mapM_ (wrapLocM kcConDecl) cons
    -- hs_tvs and dd_kindSig already dealt with in getInitialKind
    -- If dd_kindSig is Just, this must be a GADT-style decl,
    --        (see invariants of DataDefn declaration)
    -- so (a) we don't need to bring the hs_tvs into scope, because the
    --        ConDecls bind all their own variables
    --    (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it

  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
  = kcTyClTyVars name hs_tvs $
    do  { _ <- tcHsContext ctxt
        ; mapM_ (wrapLocM kcConDecl) cons }

kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)

kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
                       , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name hs_tvs $
    do  { _ <- tcHsContext ctxt
        ; mapM_ (wrapLocM kc_sig)     sigs }
  where
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
    kc_sig _                        = return ()

kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                , fdTyVars = hs_tvs
                                , fdInfo   = fd_info }))
-- closed type families look at their equations, but other families don't
-- do anything here
  = case fd_info of
      ClosedTypeFamily (Just eqns) ->
        do { (tc_binders, tc_res_kind) <- kcLookupKind fam_tc_name
           ; let fam_tc_shape = ( fam_tc_name
                                , length $ hsQTvExplicit hs_tvs
                                , tc_binders
                                , tc_res_kind )
           ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
      _ -> return ()

-------------------
kcConDecl :: ConDecl Name -> TcM ()
kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
                      , con_cxt = ex_ctxt, con_details = details })
  = addErrCtxt (dataConCtxtName [name]) $
         -- the 'False' says that the existentials don't have a CUSK, as the
         -- concept doesn't really apply here. We just need to bring the variables
         -- into scope.
    do { _ <- kcHsTyVarBndrs False False False ((fromMaybe emptyLHsQTvs ex_tvs)) $
              do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                 ; return (panic "kcConDecl", ()) }
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
       ; return () }

kcConDecl (ConDeclGADT { con_names = names
                       , con_type = ty })
  = addErrCtxt (dataConCtxtName names) $
      do { _ <- tcGadtSigType (ppr names) (unLoc $ head names) ty
         ; return () }


{-
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't want to allow promotion in a strongly connected component
when kind checking.

Consider:
  data T f = K (f (K Any))

When kind checking the `data T' declaration the local env contains the
mappings:
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr

APromotionErr is only used for DataCons, and only used during type checking
in tcTyClGroup.


************************************************************************
*                                                                      *
\subsection{Type checking}
*                                                                      *
************************************************************************

Note [Type checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this point we have completed *kind-checking* of a mutually
recursive group of type/class decls (done in kcTyClGroup). However,
we discarded the kind-checked types (eg RHSs of data type decls);
note that kcTyClDecl returns ().  There are two reasons:

  * It's convenient, because we don't have to rebuild a
    kinded HsDecl (a fairly elaborate type)

  * It's necessary, because after kind-generalisation, the
    TyCons/Classes may now be kind-polymorphic, and hence need
    to be given kind arguments.

Example:
       data T f a = MkT (f a) (T f a)
During kind-checking, we give T the kind T :: k1 -> k2 -> *
and figure out constraints on k1, k2 etc. Then we generalise
to get   T :: forall k. (k->*) -> k -> *
So now the (T f a) in the RHS must be elaborated to (T k f a).

However, during tcTyClDecl of T (above) we will be in a recursive
"knot". So we aren't allowed to look at the TyCon T itself; we are only
allowed to put it (lazily) in the returned structures.  But when
kind-checking the RHS of T's decl, we *do* need to know T's kind (so
that we can correctly elaboarate (T k f a).  How can we get T's kind
without looking at T?  Delicate answer: during tcTyClDecl, we extend

  *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
  *Local*  env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)

Then:

  * During TcHsType.kcTyVar we look in the *local* env, to get the
    known kind for T.

  * But in TcHsType.ds_type (and ds_var_app in particular) we look in
    the *global* env to get the TyCon. But we must be careful not to
    force the TyCon or we'll get a loop.

This fancy footwork (with two bindings for T) is only necessary for the
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.

See also Note [Kind checking recursive type and class declarations]

Note [Kind checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before we can type-check the decls, we must kind check them. This
is done by establishing an "initial kind", which is a rather uninformed
guess at a tycon's kind (by counting arguments, mainly) and then
using this initial kind for recursive occurrences.

The initial kind is stored in exactly the same way during kind-checking
as it is during type-checking (Note [Type checking recursive type and class
declarations]): in the *local* environment, with ATcTyCon. But we still
must store *something* in the *global* environment. Even though we
discard the result of kind-checking, we sometimes need to produce error
messages. These error messages will want to refer to the tycons being
checked, except that they don't exist yet, and it would be Terribly
Annoying to get the error messages to refer back to HsSyn. So we
create a TcTyCon and put it in the global env. This tycon can
print out its name and knows its kind,
but any other action taken on it will panic. Note
that TcTyCons are *not* knot-tied, unlike the rather valid but
knot-tied ones that occur during type-checking.

Note [Declarations for wired-in things]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For wired-in things we simply ignore the declaration
and take the wired-in information.  That avoids complications.
e.g. the need to make the data constructor worker name for
     a constraint tuple match the wired-in one
-}

tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM TyCon
tcTyClDecl rec_info (L loc decl)
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)

  | otherwise
  = setSrcSpan loc $ tcAddDeclCtxt decl $
    do { traceTc "tcTyAndCl-x" (ppr decl)
       ; tcTyClDecl1 Nothing rec_info decl }

  -- "type family" declarations
tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM TyCon
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
  = tcFamDecl1 parent fd

  -- "type" synonym declaration
tcTyClDecl1 _parent rec_info
            (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
  = ASSERT( isNothing _parent )
    tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind ->
    tcTySynRhs rec_info tc_name (kvs' ++ tvs') binders res_kind rhs

  -- "data/newtype" declaration
tcTyClDecl1 _parent rec_info
            (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
  = ASSERT( isNothing _parent )
    tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_binders res_kind ->
    tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_binders res_kind defn

tcTyClDecl1 _parent rec_info
            (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
            , tcdCtxt = ctxt, tcdMeths = meths
            , tcdFDs = fundeps, tcdSigs = sigs
            , tcdATs = ats, tcdATDefs = at_defs })
  = ASSERT( isNothing _parent )
    do { clas <- fixM $ \ clas ->
            tcTyClTyVars class_name tvs $ \ kvs' tvs' binders res_kind ->
            do { MASSERT( isConstraintKind res_kind )
                 -- This little knot is just so we can get
                 -- hold of the name of the class TyCon, which we
                 -- need to look up its recursiveness
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$
                                          ppr tvs' $$ ppr binders)
               ; let tycon_name = tyConName (classTyCon clas)
                     tc_isrec = rti_is_rec rec_info tycon_name
                     roles = rti_roles rec_info tycon_name

               ; ctxt' <- solveEqualities $ tcHsContext ctxt
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
               ; sig_stuff <- tcClassSigs class_name sigs meths
               ; at_stuff <- tcClassATs class_name clas ats at_defs
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
               ; clas <- buildClass
                            class_name (kvs' ++ tvs') roles ctxt' binders
                            fds' at_stuff
                            sig_stuff mindef tc_isrec
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$
                                        ppr fds')
               ; return clas }

         ; return (classTyCon clas) }
  where
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
                                ; return (tvs1', tvs2') }

tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
  | DataFamily <- fam_info
  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; (extra_tvs, extra_binders, real_res_kind) <- tcDataKindSig res_kind
  ; tc_rep_name <- newTyConRepName tc_name
  ; let final_tvs = (kvs' ++ tvs') `chkAppend` extra_tvs -- we may not need these
        tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                              real_res_kind final_tvs
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do
  { traceTc "open type family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; let all_tvs = kvs' ++ tvs'
  ; inj' <- tcInjectivity all_tvs inj
  ; let tycon = mkFamilyTyCon tc_name binders res_kind all_tvs
                               (resultVariableName sig) OpenSynFamilyTyCon
                               parent inj'
  ; return tycon }

  | ClosedTypeFamily mb_eqns <- fam_info
  = -- Closed type families are a little tricky, because they contain the definition
    -- of both the type family and the equations for a CoAxiom.
    do { traceTc "Closed type family:" (ppr tc_name)
         -- the variables in the header scope only over the injectivity
         -- declaration but this is not involved here
       ; (tvs', inj', binders, res_kind)
            <- tcTyClTyVars tc_name tvs
               $ \ kvs' tvs' binders res_kind ->
               do { let all_tvs = kvs' ++ tvs'
                  ; inj' <- tcInjectivity all_tvs inj
                  ; return (all_tvs, inj', binders, res_kind) }

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

         -- If Nothing, this is an abstract family in a hs-boot file;
         -- but eqns might be empty in the Just case as well
       ; case mb_eqns of
           Nothing   ->
               return $ mkFamilyTyCon tc_name binders res_kind tvs'
                                      (resultVariableName sig)
                                      AbstractClosedSynFamilyTyCon parent
                                      inj'
           Just eqns -> do {

         -- Process the equations, creating CoAxBranches
       ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, binders, res_kind)

       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
         -- Do not attempt to drop equations dominated by earlier
         -- ones here; in the case of mutual recursion with a data
         -- type, we get a knot-tying failure.  Instead we check
         -- for this afterwards, in TcValidity.checkValidCoAxiom
         -- Example: tc265

         -- Create a CoAxiom, with the correct src location. It is Vitally
         -- Important that we do not pass the branches into
         -- newFamInstAxiomName. They have types that have been zonked inside
         -- the knot and we will die if we look at them. This is OK here
         -- because there will only be one axiom, so we don't need to
         -- differentiate names.
         -- See [Zonking inside the knot] in TcHsType
       ; co_ax_name <- newFamInstAxiomName tc_lname []

       ; let mb_co_ax
              | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
              | otherwise = Just (