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 #-}
{-# LANGUAGE TypeFamilies #-}

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 {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
import TcDeriv (DerivInfo)
import TcEvidence  ( tcCoercionKind, isEmptyTcEvBinds )
import TcUnify     ( checkConstraints )
import TcHsType
import TcMType
import TysWiredIn ( unitTy )
import TcType
import RnEnv( lookupConstructorFields )
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 Outputable
import Maybes
import Unify
import Util
import Pair
import SrcLoc
import ListSetOps
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 GhcRn]      -- Mutually-recursive groups in
                                            -- dependency order
                  -> TcM ( TcGblEnv         -- Input env extended by types and
                                            -- classes
                                            -- and their implicit Ids,DataCons
                         , [InstInfo GhcRn] -- Source-code instance decls info
                         , [DerivInfo]      -- data family deriving info
                         )
-- Fails if there are any errors
tcTyAndClassDecls tyclds_s
  -- The code recovers internally, but if anything gave rise to
  -- an error we'd better stop now, to avoid a cascade
  -- Type check each group in dependency order folding the global env
  = checkNoErrs $ fold_env [] [] tyclds_s
  where
    fold_env :: [InstInfo GhcRn]
             -> [DerivInfo]
             -> [TyClGroup GhcRn]
             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
    fold_env inst_info deriv_info []
      = do { gbl_env <- getGblEnv
           ; return (gbl_env, inst_info, deriv_info) }
    fold_env inst_info deriv_info (tyclds:tyclds_s)
      = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
           ; setGblEnv tcg_env $
               -- remaining groups are typechecked in the extended global env.
             fold_env (inst_info' ++ inst_info)
                      (deriv_info' ++ deriv_info)
                      tyclds_s }

tcTyClGroup :: TyClGroup GhcRn
            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
-- Typecheck one strongly-connected component of type, class, and instance decls
-- See Note [TyClGroups and dependency analysis] in HsDecls
tcTyClGroup (TyClGroup { group_tyclds = tyclds
                       , group_roles  = roles
                       , group_instds = instds })
  = do { let role_annots = mkRoleAnnotEnv roles

           -- Step 1: Typecheck the type/class declarations
       ; traceTc "-------- tcTyClGroup ------------" empty
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
       ; tyclss <- tcTyClDecls tyclds role_annots

           -- Step 1.5: Make sure we don't have any type synonym cycles
       ; traceTc "Starting synonym cycle check" (ppr tyclss)
       ; this_uid <- fmap thisPackage getDynFlags
       ; checkSynCycles this_uid tyclss tyclds
       ; traceTc "Done synonym cycle check" (ppr tyclss)

       ; traceTc "Starting family consistency check" (ppr tyclss)
       ; forM_ tyclss checkRecFamInstConsistency
       ; traceTc "Done family consistency" (ppr tyclss)

           -- Step 2: Perform the validity check on those types/classes
           -- We can do this now because we are done with the recursive knot
           -- Do it before Step 3 (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 3: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
       ; tcExtendTyConEnv tyclss $
    do { gbl_env <- tcAddImplicits tyclss
       ; setGblEnv gbl_env $
    do {
            -- Step 4: check instance declarations
       ; (gbl_env, inst_info, datafam_deriv_info) <- tcInstDecls1 instds

       ; return (gbl_env, inst_info, datafam_deriv_info) } } }

tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
tcTyClDecls tyclds role_annots
  = 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
            --
            -- NB: We have to be careful here to NOT eagerly unfold
            -- type synonyms, as we have not tested for type synonym
            -- loops yet and could fall into a black hole.
       ; fixM $ \ ~rec_tyclss -> do
           { tcg_env <- getGblEnv
           ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss

                 -- Populate environment with knot-tied ATyCon for TyCons
                 -- NB: if the decls mention any ill-staged data cons
                 -- (see Note [Recursion 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]
             tcExtendKindEnv (foldl extendEnvWithTcTyCon emptyNameEnv tc_tycons) $

                 -- Kind and type check declarations for this group
               mapM (tcTyClDecl roles) tyclds
           } }
  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 declarations,
      and extend the kind environment (which is in the TcLclEnv)

   2. Kind check the declarations

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.

Note: we don't treat type synonyms specially (we used to, in the past);
in particular, even if we have a type synonym cycle, we still kind check
it normally, and test for cycles later (checkSynCycles).  The reason
we can get away with this is because we have more systematic TYPE r
inference, which means that we can do unification between kinds that
aren't lifted (this historically was not true.)

The downside of not directly reading off the kinds off the RHS of
type synonyms in topological order is that we don't transparently
support making synonyms of types with higher-rank kinds.  But
you can always specify a CUSK directly to make this work out.
See tc269 for an example.

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]

-}


-- Note [Missed opportunity to retain higher-rank kinds]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- In 'kcTyClGroup', there is a missed opportunity to make kind
-- inference work in a few more cases.  The idea is analogous
-- to Note [Single function non-recursive binding special-case]:
--
--      * If we have an SCC with a single decl, which is non-recursive,
--        instead of creating a unification variable representing the
--        kind of the decl and unifying it with the rhs, we can just
--        read the type directly of the rhs.
--
--      * Furthermore, we can update our SCC analysis to ignore
--        dependencies on declarations which have CUSKs: we don't
--        have to kind-check these all at once, since we can use
--        the CUSK to initialize the kind environment.
--
-- Unfortunately this requires reworking a bit of the code in
-- 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
--
kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]

-- Kind check this group, kind generalize, and return the resulting local env
-- This binds 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 decls
  = do  { mod <- getModule
        ; traceTc "kcTyClGroup" (text "module" <+> ppr mod $$ vcat (map ppr decls))

          -- Kind checking;
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
          -- See Note [Kind checking for type and class decls]

        ; lcl_env <- solveEqualities $
                     do { -- Step 1: Bind kind variables for all decls
                          initial_kinds <- getInitialKinds decls
                        ; traceTc "kcTyClGroup: initial kinds" $
                          ppr initial_kinds

                        -- Step 2: Set extended envt, kind-check the decls
                        ; tcExtendKindEnv initial_kinds $
                          do { mapM_ kcLTyClDecl decls
                             ; getLclEnv } }

        -- Step 3: 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
                 kc_tyvars   = tyConTyVars tc
                 kc_flav     = tyConFlavour tc
           ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders

           ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
           ; kc_res_kind'        <- zonkTcTypeToType env kc_res_kind

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

           ; return (mkTcTyCon name all_binders' kc_res_kind'
                               (tcTyConScopedTyVars tc)
                               kc_flav) }

    generaliseTCD :: TcTypeEnv
                  -> LTyClDecl GhcRn -> 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 GhcRn -> TcM TcTyCon
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name

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

--------------
mkTcTyConEnv :: TcTyCon -> TcTypeEnv
mkTcTyConEnv tc = unitNameEnv (getName tc) (ATcTyCon tc)

extendEnvWithTcTyCon :: TcTypeEnv -> TcTyCon -> TcTypeEnv
-- Makes a binding to put in the local envt, binding
-- a name to a TcTyCon
extendEnvWithTcTyCon env tc
  = extendNameEnv env (getName tc) (ATcTyCon tc)

--------------
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
--    See Note [Recursion and promoting data constructors]

mkPromotionErrorEnv decls
  = foldr (plusNameEnv . mk_prom_err_env . unLoc)
          emptyNameEnv decls

mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
    mkNameEnv [ (name, APromotionErr TyConPE)
              | L _ (FamilyDecl { fdLName = L _ name }) <- ats ]

mk_prom_err_env (DataDecl { tcdLName = L _ name
                          , tcdDataDefn = HsDataDefn { dd_cons = cons } })
  = unitNameEnv name (APromotionErr TyConPE)
    `plusNameEnv`
    mkNameEnv [ (con, APromotionErr RecDataConPE)
              | L _ con' <- cons, L _ con <- getConNames con' ]

mk_prom_err_env decl
  = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
    -- Works for family declarations too

--------------
getInitialKinds :: [LTyClDecl GhcRn] -> TcM (NameEnv TcTyThing)
-- Maps each tycon to its initial kind,
-- and each datacon to a suitable promotion error
--    tc :-> ATcTyCon (tc:initial_kind)
--    dc :-> APromotionErr RecDataConPE
--    See Note [Recursion and promoting data constructors]

getInitialKinds decls
  = tcExtendKindEnv promotion_err_env $
    do { tc_kinds <- mapM (addLocM getInitialKind) decls
       ; return (foldl plusNameEnv promotion_err_env tc_kinds) }
  where
    promotion_err_env = mkPromotionErrorEnv decls

getInitialKind :: TyClDecl GhcRn
               -> TcM (NameEnv TcTyThing)
-- Allocate a fresh kind variable for each TyCon and Class
-- For each tycon, return a NameEnv with
--      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
--
-- No family instances are passed to getInitialKinds

getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
  = do { let cusk = hsDeclHasCusk decl
       ; (tycon, inner_prs) <-
           kcHsTyVarBndrs name ClassFlavour cusk True ktvs $
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
              ; return (constraintKind, inner_prs) }
       ; return (extendEnvWithTcTyCon inner_prs tycon) }

getInitialKind decl@(DataDecl { tcdLName = L _ name
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_ND = new_or_data } })
  = do  { (tycon, _) <-
           kcHsTyVarBndrs name flav (hsDeclHasCusk decl) True ktvs $
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKindSig ksig
                           Nothing   -> return liftedTypeKind
              ; return (res_k, ()) }
        ; return (mkTcTyConEnv tycon) }
  where
    flav = case new_or_data of
             NewType  -> NewtypeFlavour
             DataType -> DataTypeFlavour

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

getInitialKind decl@(SynDecl { tcdLName = L _ name
                             , tcdTyVars = ktvs
                             , tcdRhs = rhs })
  = do  { (tycon, _) <- kcHsTyVarBndrs name TypeSynonymFlavour
                            (hsDeclHasCusk decl)
                            True ktvs $
            do  { res_k <- case kind_annotation rhs of
                            Nothing -> newMetaKindVar
                            Just ksig -> tcLHsKindSig ksig
                ; return (res_k, ()) }
        ; return (mkTcTyConEnv tycon) }
  where
    -- Keep this synchronized with 'hsDeclHasCusk'.
    kind_annotation (L _ ty) = case ty of
        HsParTy lty     -> kind_annotation lty
        HsKindSig _ k   -> Just k
        _               -> Nothing

---------------------------------
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                       -> [LFamilyDecl GhcRn]
                       -> TcM TcTypeEnv
getFamDeclInitialKinds mb_cusk decls
  = do { tc_kinds <- mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
       ; return (foldr plusNameEnv emptyNameEnv tc_kinds) }

getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                      -> FamilyDecl GhcRn
                      -> TcM TcTypeEnv
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
  = do { (tycon, _) <-
           kcHsTyVarBndrs name flav cusk True ktvs $
           do { res_k <- case resultSig of
                      KindSig ki                        -> tcLHsKindSig ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ki
                      _ -- open type families have * return kind by default
                        | tcFlavourIsOpen flav     -> return liftedTypeKind
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
              ; return (res_k, ()) }
       ; return (mkTcTyConEnv tycon) }
  where
    cusk  = famDeclHasCusk mb_cusk decl
    flav  = case info of
      DataFamily         -> DataFamilyFlavour
      OpenTypeFamily     -> OpenTypeFamilyFlavour
      ClosedTypeFamily _ -> ClosedTypeFamilyFlavour

------------------------------------------------------------------------
kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
  -- See Note [Kind checking for type and class decls]
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $
    tcAddDeclCtxt decl $
    do { traceTc "kcTyClDecl {" (ppr (tyClDeclLName decl))
       ; kcTyClDecl decl
       ; traceTc "kcTyClDecl done }" (ppr (tyClDeclLName decl)) }

kcTyClDecl :: TyClDecl GhcRn -> 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, 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 $
    do  { _ <- tcHsContext ctxt
        ; mapM_ (wrapLocM kcConDecl) cons }

kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = lrhs })
  = kcTyClTyVars name $
    do  { syn_tc <- kcLookupTcTyCon name
        -- NB: check against the result kind that we allocated
        -- in getInitialKinds.
        ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }

kcTyClDecl (ClassDecl { tcdLName = L _ name
                      , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name $
    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
                                , 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 { fam_tc <- kcLookupTcTyCon fam_tc_name
           ; mapM_ (kcTyFamInstEqn (famTyConShape fam_tc)) eqns }
      _ -> return ()

-------------------
kcConDecl :: ConDecl GhcRn -> 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. (Similarly, the choice of PromotedDataConFlavour isn't
         -- particularly important.)
    do { _ <- kcHsTyVarBndrs (unLoc name) PromotedDataConFlavour
                             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
                -- Even though the data constructor's type is closed, we
                -- must still call tcGadtSigType, because that influences
                -- the inferred kind of the /type/ constructor.  Example:
                --    data T f a where
                --      MkT :: f a -> T f a
                -- If we don't look at MkT we won't get the correct kind
                -- for the type constructor T
         ; 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 :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
tcTyClDecl roles_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 roles_info decl }

  -- "type family" declarations
tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
  = tcFamDecl1 parent fd

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

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

tcTyClDecl1 _parent roles_info
            (ClassDecl { tcdLName = L _ class_name
            , tcdCtxt = ctxt, tcdMeths = meths
            , tcdFDs = fundeps, tcdSigs = sigs
            , tcdATs = ats, tcdATDefs = at_defs })
  = ASSERT( isNothing _parent )
    do { clas <- fixM $ \ clas ->
            -- We need the knot because 'clas' is passed into tcClassATs
            tcTyClTyVars class_name $ \ binders res_kind ->
            do { MASSERT( isConstraintKind res_kind )
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
               ; let tycon_name = class_name        -- We use the same name
                     roles = roles_info tycon_name  -- for TyCon and Class

               ; 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
               -- TODO: Allow us to distinguish between abstract class,
               -- and concrete class with no methods (maybe by
               -- specifying a trailing where or not
               ; is_boot <- tcIsHsBootOrSig
               ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
                          = Nothing
                          | otherwise
                          = Just (ctxt', at_stuff, sig_stuff, mindef)
               ; clas <- buildClass class_name binders roles fds' body
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
                                        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 GhcRn -> 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 $ \ binders res_kind -> do
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; (extra_binders, real_res_kind) <- tcDataKindSig False res_kind
  ; tc_rep_name <- newTyConRepName tc_name
  ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                              real_res_kind
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
  { traceTc "open type family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; inj' <- tcInjectivity binders inj
  ; let tycon = mkFamilyTyCon tc_name binders res_kind
                               (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
       ; (inj', binders, res_kind)
            <- tcTyClTyVars tc_name
               $ \ binders res_kind ->
               do { inj' <- tcInjectivity binders inj
                  ; return (inj', binders, res_kind) }