{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

\section[TcMonoType]{Typechecking user-specified @MonoTypes@}
-}

{-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

module TcHsType (
        -- Type signatures
        kcClassSigType, tcClassSigType,
        tcHsSigType, tcHsSigWcType,
        tcHsPartialSigType,
        funsSigCtxt, addSigCtxt, pprSigCtxt,

        tcHsClsInstType,
        tcHsDeriv, tcDerivStrategy,
        tcHsTypeApp,
        UserTypeCtxt(..),
        bindImplicitTKBndrs_Tv, bindImplicitTKBndrs_Skol,
            bindImplicitTKBndrs_Q_Tv, bindImplicitTKBndrs_Q_Skol,
        bindExplicitTKBndrs_Tv, bindExplicitTKBndrs_Skol,
            bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
        ContextKind(..),

                -- Type checking type and class decls
        kcLookupTcTyCon, bindTyClTyVars,
        etaExpandAlgTyCon, tcbVisibilities,

          -- tyvars
        zonkAndScopedSort,

        -- Kind-checking types
        -- No kind generalisation, no checkValidType
        kcLHsQTyVars,
        tcWildCardBinders,
        tcHsLiftedType,   tcHsOpenType,
        tcHsLiftedTypeNC, tcHsOpenTypeNC,
        tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
        tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
        failIfEmitsConstraints,
        solveEqualities, -- useful re-export

        typeLevelMode, kindLevelMode,

        kindGeneralize, checkExpectedKind, RequireSaturation(..),
        reportFloatingKvs,

        -- Sort-checking kinds
        tcLHsKindSig, badKindSig,

        -- Zonking and promoting
        zonkPromoteType,

        -- Pattern type signatures
        tcHsPatSigType, tcPatSig,

        -- Error messages
        funAppCtxt, addTyConFlavCtxt
   ) where

#include "HsVersions.h"

import GhcPrelude

import HsSyn
import TcRnMonad
import TcEvidence
import TcEnv
import TcMType
import TcValidity
import TcUnify
import TcIface
import TcSimplify
import TcHsSyn
import TcErrors ( reportAllUnsolved )
import TcType
import Inst   ( tcInstTyBinders, tcInstTyBinder )
import TyCoRep( TyCoBinder(..), TyBinder, tyCoBinderArgFlag )  -- Used in etaExpandAlgTyCon
import Type
import TysPrim
import Coercion
import RdrName( lookupLocalRdrOcc )
import Var
import VarSet
import TyCon
import ConLike
import DataCon
import Class
import Name
import NameSet
import VarEnv
import TysWiredIn
import BasicTypes
import SrcLoc
import Constants ( mAX_CTUPLE_SIZE )
import ErrUtils( MsgDoc )
import Unique
import UniqSet
import Util
import UniqSupply
import Outputable
import FastString
import PrelNames hiding ( wildCardName )
import DynFlags ( WarningFlag (Opt_WarnPartialTypeSignatures) )
import qualified GHC.LanguageExtensions as LangExt

import Maybes
import Data.List ( find )
import Control.Monad

{-
        ----------------------------
                General notes
        ----------------------------

Unlike with expressions, type-checking types both does some checking and
desugars at the same time. This is necessary because we often want to perform
equality checks on the types right away, and it would be incredibly painful
to do this on un-desugared types. Luckily, desugared types are close enough
to HsTypes to make the error messages sane.

During type-checking, we perform as little validity checking as possible.
Generally, after type-checking, you will want to do validity checking, say
with TcValidity.checkValidType.

Validity checking
~~~~~~~~~~~~~~~~~
Some of the validity check could in principle be done by the kind checker,
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
  e.g.  type T k = k Int
        type S a = a
  Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
  and then S is saturated.  This is a GHC extension.

- Similarly, also a GHC extension, we look through synonyms before complaining
  about the form of a class or instance declaration

- Ambiguity checks involve functional dependencies

Also, in a mutually recursive group of types, we can't look at the TyCon until we've
finished building the loop.  So to keep things simple, we postpone most validity
checking until step (3).

%************************************************************************
%*                                                                      *
              Check types AND do validity checking
*                                                                      *
************************************************************************
-}

funsSigCtxt :: [Located Name] -> UserTypeCtxt
-- Returns FunSigCtxt, with no redundant-context-reporting,
-- form a list of located names
funsSigCtxt :: [Located Name] -> UserTypeCtxt
funsSigCtxt (L _ name1 :: Name
name1 : _) = Name -> Bool -> UserTypeCtxt
FunSigCtxt Name
name1 Bool
False
funsSigCtxt []              = String -> UserTypeCtxt
forall a. String -> a
panic "funSigCtxt"

addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt ctxt :: UserTypeCtxt
ctxt hs_ty :: LHsType GhcRn
hs_ty thing_inside :: TcM a
thing_inside
  = SrcSpan -> TcM a -> TcM a
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan (LHsType GhcRn -> SrcSpan
forall a. HasSrcSpan a => a -> SrcSpan
getLoc LHsType GhcRn
hs_ty) (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
    MsgDoc -> TcM a -> TcM a
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (UserTypeCtxt -> LHsType GhcRn -> MsgDoc
pprSigCtxt UserTypeCtxt
ctxt LHsType GhcRn
hs_ty) (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
    TcM a
thing_inside

pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
-- (pprSigCtxt ctxt <extra> <type>)
-- prints    In the type signature for 'f':
--              f :: <type>
-- The <extra> is either empty or "the ambiguity check for"
pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> MsgDoc
pprSigCtxt ctxt :: UserTypeCtxt
ctxt hs_ty :: LHsType GhcRn
hs_ty
  | Just n :: Name
n <- UserTypeCtxt -> Maybe Name
isSigMaybe UserTypeCtxt
ctxt
  = MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "In the type signature:")
       2 (Name -> MsgDoc
forall a. OutputableBndr a => a -> MsgDoc
pprPrefixOcc Name
n MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_ty)

  | Bool
otherwise
  = MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "In" MsgDoc -> MsgDoc -> MsgDoc
<+> UserTypeCtxt -> MsgDoc
pprUserTypeCtxt UserTypeCtxt
ctxt MsgDoc -> MsgDoc -> MsgDoc
<> MsgDoc
colon)
       2 (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_ty)

tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
-- This one is used when we have a LHsSigWcType, but in
-- a place where wildcards aren't allowed. The renamer has
-- already checked this, so we can simply ignore it.
tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
tcHsSigWcType ctxt :: UserTypeCtxt
ctxt sig_ty :: LHsSigWcType GhcRn
sig_ty = UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcHsSigType UserTypeCtxt
ctxt (LHsSigWcType GhcRn -> LHsSigType GhcRn
forall pass. LHsSigWcType pass -> LHsSigType pass
dropWildCards LHsSigWcType GhcRn
sig_ty)

kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
kcClassSigType skol_info :: SkolemInfo
skol_info names :: [Located Name]
names sig_ty :: LHsSigType GhcRn
sig_ty
  = TcM Type -> TcM ()
forall a. TcM a -> TcM ()
discardResult (TcM Type -> TcM ()) -> TcM Type -> TcM ()
forall a b. (a -> b) -> a -> b
$
    SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
tcClassSigType SkolemInfo
skol_info [Located Name]
names LHsSigType GhcRn
sig_ty
  -- tcClassSigType does a fair amount of extra work that we don't need,
  -- such as ordering quantified variables. But we absolutely do need
  -- to push the level when checking method types and solve local equalities,
  -- and so it seems easier just to call tcClassSigType than selectively
  -- extract the lines of code from tc_hs_sig_type that we really need.
  -- If we don't push the level, we get #16517, where GHC accepts
  --   class C a where
  --     meth :: forall k. Proxy (a :: k) -> ()
  -- Note that k is local to meth -- this is hogwash.

tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
-- Does not do validity checking
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
tcClassSigType skol_info :: SkolemInfo
skol_info names :: [Located Name]
names sig_ty :: LHsSigType GhcRn
sig_ty
  = UserTypeCtxt -> LHsType GhcRn -> TcM Type -> TcM Type
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt ([Located Name] -> UserTypeCtxt
funsSigCtxt [Located Name]
names) (LHsSigType GhcRn -> LHsType GhcRn
forall pass. LHsSigType pass -> LHsType pass
hsSigType LHsSigType GhcRn
sig_ty) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    (Bool, Type) -> Type
forall a b. (a, b) -> b
snd ((Bool, Type) -> Type)
-> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type) -> TcM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SkolemInfo
-> LHsSigType GhcRn
-> ContextKind
-> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
tc_hs_sig_type SkolemInfo
skol_info LHsSigType GhcRn
sig_ty (Type -> ContextKind
TheKind Type
liftedTypeKind)
       -- Do not zonk-to-Type, nor perform a validity check
       -- We are in a knot with the class and associated types
       -- Zonking and validity checking is done by tcClassDecl
       -- No need to fail here if the type has an error:
       --   If we're in the kind-checking phase, the solveEqualities
       --     in kcTyClGroup catches the error
       --   If we're in the type-checking phase, the solveEqualities
       --     in tcClassDecl1 gets it
       -- Failing fast here degrades the error message in, e.g., tcfail135:
       --   class Foo f where
       --     baa :: f a -> f
       -- If we fail fast, we're told that f has kind `k1` when we wanted `*`.
       -- It should be that f has kind `k2 -> *`, but we never get a chance
       -- to run the solver where the kind of f is touchable. This is
       -- painfully delicate.

tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
-- Does validity checking
-- See Note [Recipe for checking a signature]
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcHsSigType ctxt :: UserTypeCtxt
ctxt sig_ty :: LHsSigType GhcRn
sig_ty
  = UserTypeCtxt -> LHsType GhcRn -> TcM Type -> TcM Type
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt UserTypeCtxt
ctxt (LHsSigType GhcRn -> LHsType GhcRn
forall pass. LHsSigType pass -> LHsType pass
hsSigType LHsSigType GhcRn
sig_ty) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    do { String -> MsgDoc -> TcM ()
traceTc "tcHsSigType {" (LHsSigType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsSigType GhcRn
sig_ty)

          -- Generalise here: see Note [Kind generalisation]
       ; (insol :: Bool
insol, ty :: Type
ty) <- SkolemInfo
-> LHsSigType GhcRn
-> ContextKind
-> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
tc_hs_sig_type SkolemInfo
skol_info LHsSigType GhcRn
sig_ty
                                       (UserTypeCtxt -> ContextKind
expectedKindInCtxt UserTypeCtxt
ctxt)
       ; Type
ty <- Type -> TcM Type
zonkTcType Type
ty

       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
insol TcM ()
forall env a. IOEnv env a
failM
       -- See Note [Fail fast if there are insoluble kind equalities] in TcSimplify

       ; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
ty
       ; String -> MsgDoc -> TcM ()
traceTc "end tcHsSigType }" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
ty)
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty }
  where
    skol_info :: SkolemInfo
skol_info = UserTypeCtxt -> SkolemInfo
SigTypeSkol UserTypeCtxt
ctxt

tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
               -> ContextKind -> TcM (Bool, TcType)
-- Kind-checks/desugars an 'LHsSigType',
--   solve equalities,
--   and then kind-generalizes.
-- This will never emit constraints, as it uses solveEqualities interally.
-- No validity checking or zonking
-- Returns also a Bool indicating whether the type induced an insoluble constraint;
-- True <=> constraint is insoluble
tc_hs_sig_type :: SkolemInfo
-> LHsSigType GhcRn
-> ContextKind
-> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
tc_hs_sig_type skol_info :: SkolemInfo
skol_info hs_sig_type :: LHsSigType GhcRn
hs_sig_type ctxt_kind :: ContextKind
ctxt_kind
  | HsIB { hsib_ext :: forall pass thing. HsImplicitBndrs pass thing -> XHsIB pass thing
hsib_ext = XHsIB GhcRn (LHsType GhcRn)
sig_vars, hsib_body :: forall pass thing. HsImplicitBndrs pass thing -> thing
hsib_body = LHsType GhcRn
hs_ty } <- LHsSigType GhcRn
hs_sig_type
  = do { (tc_lvl :: TcLevel
tc_lvl, (wanted :: WantedConstraints
wanted, (spec_tkvs :: [TcTyVar]
spec_tkvs, ty :: Type
ty)))
              <- TcM (WantedConstraints, ([TcTyVar], Type))
-> TcM (TcLevel, (WantedConstraints, ([TcTyVar], Type)))
forall a. TcM a -> TcM (TcLevel, a)
pushTcLevelM                           (TcM (WantedConstraints, ([TcTyVar], Type))
 -> TcM (TcLevel, (WantedConstraints, ([TcTyVar], Type))))
-> TcM (WantedConstraints, ([TcTyVar], Type))
-> TcM (TcLevel, (WantedConstraints, ([TcTyVar], Type)))
forall a b. (a -> b) -> a -> b
$
                 String
-> TcM ([TcTyVar], Type)
-> TcM (WantedConstraints, ([TcTyVar], Type))
forall a. String -> TcM a -> TcM (WantedConstraints, a)
solveLocalEqualitiesX "tc_hs_sig_type" (TcM ([TcTyVar], Type)
 -> TcM (WantedConstraints, ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type)
-> TcM (WantedConstraints, ([TcTyVar], Type))
forall a b. (a -> b) -> a -> b
$
                 [Name] -> TcM Type -> TcM ([TcTyVar], Type)
forall a. [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Skol [Name]
XHsIB GhcRn (LHsType GhcRn)
sig_vars      (TcM Type -> TcM ([TcTyVar], Type))
-> TcM Type -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
                 do { Type
kind <- ContextKind -> TcM Type
newExpectedKind ContextKind
ctxt_kind

                    ; TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
hs_ty Type
kind }
       -- Any remaining variables (unsolved in the solveLocalEqualities)
       -- should be in the global tyvars, and therefore won't be quantified

       ; [TcTyVar]
spec_tkvs <- [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort [TcTyVar]
spec_tkvs
       ; let ty1 :: Type
ty1 = [TcTyVar] -> Type -> Type
mkSpecForAllTys [TcTyVar]
spec_tkvs Type
ty
       ; [TcTyVar]
kvs <- WantedConstraints -> Type -> TcM [TcTyVar]
kindGeneralizeLocal WantedConstraints
wanted Type
ty1
       ; SkolemInfo
-> Maybe MsgDoc
-> [TcTyVar]
-> TcLevel
-> WantedConstraints
-> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info Maybe MsgDoc
forall a. Maybe a
Nothing ([TcTyVar]
kvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
spec_tkvs)
                                  TcLevel
tc_lvl WantedConstraints
wanted

       ; (Bool, Type) -> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (WantedConstraints -> Bool
insolubleWC WantedConstraints
wanted, [TcTyVar] -> Type -> Type
mkInvForAllTys [TcTyVar]
kvs Type
ty1) }

tc_hs_sig_type _ (XHsImplicitBndrs _) _ = String -> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
forall a. String -> a
panic "tc_hs_sig_type"

tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where
--   we want to fully solve /all/ equalities, and report errors
-- Does zonking, but not validity checking because it's used
--   for things (like deriving and instances) that aren't
--   ordinary types
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType hs_sig_type :: LHsSigType GhcRn
hs_sig_type ctxt_kind :: ContextKind
ctxt_kind
  | HsIB { hsib_ext :: forall pass thing. HsImplicitBndrs pass thing -> XHsIB pass thing
hsib_ext = XHsIB GhcRn (LHsType GhcRn)
sig_vars, hsib_body :: forall pass thing. HsImplicitBndrs pass thing -> thing
hsib_body = LHsType GhcRn
hs_ty } <- LHsSigType GhcRn
hs_sig_type
  = do { String -> MsgDoc -> TcM ()
traceTc "tcTopLHsType {" (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_ty)
       ; (spec_tkvs :: [TcTyVar]
spec_tkvs, ty :: Type
ty)
              <- TcM ([TcTyVar], Type) -> TcM ([TcTyVar], Type)
forall a. TcM a -> TcM a
pushTcLevelM_                     (TcM ([TcTyVar], Type) -> TcM ([TcTyVar], Type))
-> TcM ([TcTyVar], Type) -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
                 TcM ([TcTyVar], Type) -> TcM ([TcTyVar], Type)
forall a. TcM a -> TcM a
solveEqualities                   (TcM ([TcTyVar], Type) -> TcM ([TcTyVar], Type))
-> TcM ([TcTyVar], Type) -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
                 [Name] -> TcM Type -> TcM ([TcTyVar], Type)
forall a. [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Skol [Name]
XHsIB GhcRn (LHsType GhcRn)
sig_vars (TcM Type -> TcM ([TcTyVar], Type))
-> TcM Type -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
                 do { Type
kind <- ContextKind -> TcM Type
newExpectedKind ContextKind
ctxt_kind
                    ; TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
hs_ty Type
kind }

       ; [TcTyVar]
spec_tkvs <- [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort [TcTyVar]
spec_tkvs
       ; let ty1 :: Type
ty1 = [TcTyVar] -> Type -> Type
mkSpecForAllTys [TcTyVar]
spec_tkvs Type
ty
       ; [TcTyVar]
kvs <- Type -> TcM [TcTyVar]
kindGeneralize Type
ty1
       ; Type
final_ty <- Type -> TcM Type
zonkTcTypeToType ([TcTyVar] -> Type -> Type
mkInvForAllTys [TcTyVar]
kvs Type
ty1)
       ; String -> MsgDoc -> TcM ()
traceTc "End tcTopLHsType }" ([MsgDoc] -> MsgDoc
vcat [LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_ty, Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
final_ty])
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
final_ty}

tcTopLHsType (XHsImplicitBndrs _) _ = String -> TcM Type
forall a. String -> a
panic "tcTopLHsType"

-----------------
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
--    returns ([k], C, [k, Int], [k->k])
-- Return values are fully zonked
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TcTyVar], (Class, [Type], [Type]))
tcHsDeriv hs_ty :: LHsSigType GhcRn
hs_ty
  = do { Type
ty <- TcM Type -> TcM Type
forall a. TcM a -> TcM a
checkNoErrs (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$  -- Avoid redundant error report
                              -- with "illegal deriving", below
               LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType LHsSigType GhcRn
hs_ty ContextKind
AnyKind
       ; let (tvs :: [TcTyVar]
tvs, pred :: Type
pred)    = Type -> ([TcTyVar], Type)
splitForAllTys Type
ty
             (kind_args :: [Type]
kind_args, _) = Type -> ([Type], Type)
splitFunTys (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
pred)
       ; case Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred of
           Just (cls :: Class
cls, tys :: [Type]
tys) -> ([TcTyVar], (Class, [Type], [Type]))
-> TcM ([TcTyVar], (Class, [Type], [Type]))
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tvs, (Class
cls, [Type]
tys, [Type]
kind_args))
           Nothing -> MsgDoc -> TcM ([TcTyVar], (Class, [Type], [Type]))
forall a. MsgDoc -> TcM a
failWithTc (String -> MsgDoc
text "Illegal deriving item" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (LHsSigType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsSigType GhcRn
hs_ty)) }

-- | Typecheck something within the context of a deriving strategy.
-- This is of particular importance when the deriving strategy is @via@.
-- For instance:
--
-- @
-- deriving via (S a) instance C (T a)
-- @
--
-- We need to typecheck @S a@, and moreover, we need to extend the tyvar
-- environment with @a@ before typechecking @C (T a)@, since @S a@ quantified
-- the type variable @a@.
tcDerivStrategy
  :: forall a.
     Maybe (DerivStrategy GhcRn) -- ^ The deriving strategy
  -> TcM ([TyVar], a) -- ^ The thing to typecheck within the context of the
                      -- deriving strategy, which might quantify some type
                      -- variables of its own.
  -> TcM (Maybe (DerivStrategy GhcTc), [TyVar], a)
     -- ^ The typechecked deriving strategy, all quantified tyvars, and
     -- the payload of the typechecked thing.
tcDerivStrategy :: Maybe (DerivStrategy GhcRn)
-> TcM ([TcTyVar], a)
-> TcM (Maybe (DerivStrategy GhcTc), [TcTyVar], a)
tcDerivStrategy mds :: Maybe (DerivStrategy GhcRn)
mds thing_inside :: TcM ([TcTyVar], a)
thing_inside
  = case Maybe (DerivStrategy GhcRn)
mds of
      Nothing -> Maybe (DerivStrategy GhcTc)
-> TcM (Maybe (DerivStrategy GhcTc), [TcTyVar], a)
forall mds. mds -> TcM (mds, [TcTyVar], a)
boring_case Maybe (DerivStrategy GhcTc)
forall a. Maybe a
Nothing
      Just ds :: DerivStrategy GhcRn
ds -> do (ds' :: DerivStrategy GhcTc
ds', tvs :: [TcTyVar]
tvs, thing :: a
thing) <- DerivStrategy GhcRn -> TcM (DerivStrategy GhcTc, [TcTyVar], a)
tc_deriv_strategy DerivStrategy GhcRn
ds
                    (Maybe (DerivStrategy GhcTc), [TcTyVar], a)
-> TcM (Maybe (DerivStrategy GhcTc), [TcTyVar], a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DerivStrategy GhcTc -> Maybe (DerivStrategy GhcTc)
forall a. a -> Maybe a
Just DerivStrategy GhcTc
ds', [TcTyVar]
tvs, a
thing)
  where
    tc_deriv_strategy :: DerivStrategy GhcRn
                      -> TcM (DerivStrategy GhcTc, [TyVar], a)
    tc_deriv_strategy :: DerivStrategy GhcRn -> TcM (DerivStrategy GhcTc, [TcTyVar], a)
tc_deriv_strategy StockStrategy    = DerivStrategy GhcTc -> TcM (DerivStrategy GhcTc, [TcTyVar], a)
forall mds. mds -> TcM (mds, [TcTyVar], a)
boring_case DerivStrategy GhcTc
forall pass. DerivStrategy pass
StockStrategy
    tc_deriv_strategy AnyclassStrategy = DerivStrategy GhcTc -> TcM (DerivStrategy GhcTc, [TcTyVar], a)
forall mds. mds -> TcM (mds, [TcTyVar], a)
boring_case DerivStrategy GhcTc
forall pass. DerivStrategy pass
AnyclassStrategy
    tc_deriv_strategy NewtypeStrategy  = DerivStrategy GhcTc -> TcM (DerivStrategy GhcTc, [TcTyVar], a)
forall mds. mds -> TcM (mds, [TcTyVar], a)
boring_case DerivStrategy GhcTc
forall pass. DerivStrategy pass
NewtypeStrategy
    tc_deriv_strategy (ViaStrategy ty :: XViaStrategy GhcRn
ty) = do
      Type
ty' <- TcM Type -> TcM Type
forall a. TcM a -> TcM a
checkNoErrs (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
             LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType XViaStrategy GhcRn
LHsSigType GhcRn
ty ContextKind
AnyKind
      let (via_tvs :: [TcTyVar]
via_tvs, via_pred :: Type
via_pred) = Type -> ([TcTyVar], Type)
splitForAllTys Type
ty'
      [TcTyVar]
-> TcM (DerivStrategy GhcTc, [TcTyVar], a)
-> TcM (DerivStrategy GhcTc, [TcTyVar], a)
forall r. [TcTyVar] -> TcM r -> TcM r
tcExtendTyVarEnv [TcTyVar]
via_tvs (TcM (DerivStrategy GhcTc, [TcTyVar], a)
 -> TcM (DerivStrategy GhcTc, [TcTyVar], a))
-> TcM (DerivStrategy GhcTc, [TcTyVar], a)
-> TcM (DerivStrategy GhcTc, [TcTyVar], a)
forall a b. (a -> b) -> a -> b
$ do
        (thing_tvs :: [TcTyVar]
thing_tvs, thing :: a
thing) <- TcM ([TcTyVar], a)
thing_inside
        (DerivStrategy GhcTc, [TcTyVar], a)
-> TcM (DerivStrategy GhcTc, [TcTyVar], a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (XViaStrategy GhcTc -> DerivStrategy GhcTc
forall pass. XViaStrategy pass -> DerivStrategy pass
ViaStrategy Type
XViaStrategy GhcTc
via_pred, [TcTyVar]
via_tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
thing_tvs, a
thing)

    boring_case :: mds -> TcM (mds, [TyVar], a)
    boring_case :: mds -> TcM (mds, [TcTyVar], a)
boring_case mds :: mds
mds = do
      (thing_tvs :: [TcTyVar]
thing_tvs, thing :: a
thing) <- TcM ([TcTyVar], a)
thing_inside
      (mds, [TcTyVar], a) -> TcM (mds, [TcTyVar], a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (mds
mds, [TcTyVar]
thing_tvs, a
thing)

tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
                -> LHsSigType GhcRn
                -> TcM Type
-- Like tcHsSigType, but for a class instance declaration
tcHsClsInstType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcHsClsInstType user_ctxt :: UserTypeCtxt
user_ctxt hs_inst_ty :: LHsSigType GhcRn
hs_inst_ty
  = SrcSpan -> TcM Type -> TcM Type
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan (LHsType GhcRn -> SrcSpan
forall a. HasSrcSpan a => a -> SrcSpan
getLoc (LHsSigType GhcRn -> LHsType GhcRn
forall pass. LHsSigType pass -> LHsType pass
hsSigType LHsSigType GhcRn
hs_inst_ty)) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    do { -- Fail eagerly if tcTopLHsType fails.  We are at top level so
         -- these constraints will never be solved later. And failing
         -- eagerly avoids follow-on errors when checkValidInstance
         -- sees an unsolved coercion hole
         Type
inst_ty <- TcM Type -> TcM Type
forall a. TcM a -> TcM a
checkNoErrs (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                    LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType LHsSigType GhcRn
hs_inst_ty (Type -> ContextKind
TheKind Type
constraintKind)
       ; UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
checkValidInstance UserTypeCtxt
user_ctxt LHsSigType GhcRn
hs_inst_ty Type
inst_ty
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
inst_ty }

----------------------------------------------
-- | Type-check a visible type application
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
-- See Note [Recipe for checking a signature] in TcHsType
tcHsTypeApp :: LHsWcType GhcRn -> Type -> TcM Type
tcHsTypeApp wc_ty :: LHsWcType GhcRn
wc_ty kind :: Type
kind
  | HsWC { hswc_ext :: forall pass thing. HsWildCardBndrs pass thing -> XHsWC pass thing
hswc_ext = XHsWC GhcRn (LHsType GhcRn)
sig_wcs, hswc_body :: forall pass thing. HsWildCardBndrs pass thing -> thing
hswc_body = LHsType GhcRn
hs_ty } <- LHsWcType GhcRn
wc_ty
  = do { Type
ty <- String -> TcM Type -> TcM Type
forall a. String -> TcM a -> TcM a
solveLocalEqualities "tcHsTypeApp" (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
               -- We are looking at a user-written type, very like a
               -- signature so we want to solve its equalities right now
               WarningFlag -> TcM Type -> TcM Type
forall gbl lcl a.
WarningFlag -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
unsetWOptM WarningFlag
Opt_WarnPartialTypeSignatures (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
               Extension -> TcM Type -> TcM Type
forall gbl lcl a. Extension -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
setXOptM Extension
LangExt.PartialTypeSignatures (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
               -- See Note [Wildcards in visible type application]
               [Name] -> ([(Name, TcTyVar)] -> TcM Type) -> TcM Type
forall a. [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcWildCardBinders [Name]
XHsWC GhcRn (LHsType GhcRn)
sig_wcs (([(Name, TcTyVar)] -> TcM Type) -> TcM Type)
-> ([(Name, TcTyVar)] -> TcM Type) -> TcM Type
forall a b. (a -> b) -> a -> b
$ \ _ ->
               LHsType GhcRn -> Type -> TcM Type
tcCheckLHsType LHsType GhcRn
hs_ty Type
kind
       -- We must promote here. Ex:
       --   f :: forall a. a
       --   g = f @(forall b. Proxy b -> ()) @Int ...
       -- After when processing the @Int, we'll have to check its kind
       -- against the as-yet-unknown kind of b. This check causes an assertion
       -- failure if we don't promote.
       ; Type
ty <- Type -> TcM Type
zonkPromoteType Type
ty
       ; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
TypeAppCtxt Type
ty
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty }
tcHsTypeApp (XHsWildCardBndrs _) _ = String -> TcM Type
forall a. String -> a
panic "tcHsTypeApp"

{- Note [Wildcards in visible type application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

A HsWildCardBndrs's hswc_ext now only includes named wildcards, so any unnamed
wildcards stay unchanged in hswc_body and when called in tcHsTypeApp, tcCheckLHsType
will call emitWildCardHoleConstraints on them. However, this would trigger
error/warning when an unnamed wildcard is passed in as a visible type argument,
which we do not want because users should be able to write @_ to skip a instantiating
a type variable variable without fuss. The solution is to switch the
PartialTypeSignatures flags here to let the typechecker know that it's checking
a '@_' and do not emit hole constraints on it.
See related Note [Wildcards in visible kind application]
and Note [The wildcard story for types] in HsTypes.hs

-}

{-
************************************************************************
*                                                                      *
            The main kind checker: no validity checks here
*                                                                      *
************************************************************************

        First a couple of simple wrappers for kcHsType
-}

---------------------------
tcHsOpenType, tcHsLiftedType,
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
-- Used for type signatures
-- Do not do validity checking
tcHsOpenType :: LHsType GhcRn -> TcM Type
tcHsOpenType ty :: LHsType GhcRn
ty   = LHsType GhcRn -> TcM Type -> TcM Type
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
ty (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$ LHsType GhcRn -> TcM Type
tcHsOpenTypeNC LHsType GhcRn
ty
tcHsLiftedType :: LHsType GhcRn -> TcM Type
tcHsLiftedType ty :: LHsType GhcRn
ty = LHsType GhcRn -> TcM Type -> TcM Type
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
ty (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$ LHsType GhcRn -> TcM Type
tcHsLiftedTypeNC LHsType GhcRn
ty

tcHsOpenTypeNC :: LHsType GhcRn -> TcM Type
tcHsOpenTypeNC   ty :: LHsType GhcRn
ty = do { Type
ek <- TcM Type
newOpenTypeKind
                         ; TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
ty Type
ek }
tcHsLiftedTypeNC :: LHsType GhcRn -> TcM Type
tcHsLiftedTypeNC ty :: LHsType GhcRn
ty = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
ty Type
liftedTypeKind

-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
tcCheckLHsType :: LHsType GhcRn -> Type -> TcM Type
tcCheckLHsType hs_ty :: LHsType GhcRn
hs_ty exp_kind :: Type
exp_kind
  = LHsType GhcRn -> TcM Type -> TcM Type
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
hs_ty (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
hs_ty Type
exp_kind

tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
-- Called from outside: set the context
tcLHsType :: LHsType GhcRn -> TcM (Type, Type)
tcLHsType ty :: LHsType GhcRn
ty = LHsType GhcRn -> TcM (Type, Type) -> TcM (Type, Type)
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
ty (TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
ty)

-- Like tcLHsType, but use it in a context where type synonyms and type families
-- do not need to be saturated, like in a GHCi :kind call
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (Type, Type)
tcLHsTypeUnsaturated ty :: LHsType GhcRn
ty = LHsType GhcRn -> TcM (Type, Type) -> TcM (Type, Type)
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
ty (TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
ty)
  where
    mode :: TcTyMode
mode = TcTyMode -> TcTyMode
allowUnsaturated TcTyMode
typeLevelMode

{-
************************************************************************
*                                                                      *
      Type-checking modes
*                                                                      *
************************************************************************

The kind-checker is parameterised by a TcTyMode, which contains some
information about where we're checking a type.

The renamer issues errors about what it can. All errors issued here must
concern things that the renamer can't handle.

-}

-- | Do we require type families to be saturated?
data RequireSaturation
  = YesSaturation
  | NoSaturation   -- e.g. during a call to GHCi's :kind

-- | Info about the context in which we're checking a type. Currently,
-- differentiates only between types and kinds, but this will likely
-- grow, at least to include the distinction between patterns and
-- not-patterns.
data TcTyMode
  = TcTyMode { TcTyMode -> TypeOrKind
mode_level :: TypeOrKind
             , TcTyMode -> RequireSaturation
mode_sat   :: RequireSaturation
             }
 -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
 -- in GHCi :kind calls

typeLevelMode :: TcTyMode
typeLevelMode :: TcTyMode
typeLevelMode = TcTyMode :: TypeOrKind -> RequireSaturation -> TcTyMode
TcTyMode { mode_level :: TypeOrKind
mode_level = TypeOrKind
TypeLevel, mode_sat :: RequireSaturation
mode_sat = RequireSaturation
YesSaturation }

kindLevelMode :: TcTyMode
kindLevelMode :: TcTyMode
kindLevelMode = TcTyMode :: TypeOrKind -> RequireSaturation -> TcTyMode
TcTyMode { mode_level :: TypeOrKind
mode_level = TypeOrKind
KindLevel, mode_sat :: RequireSaturation
mode_sat = RequireSaturation
YesSaturation }

allowUnsaturated :: TcTyMode -> TcTyMode
allowUnsaturated :: TcTyMode -> TcTyMode
allowUnsaturated mode :: TcTyMode
mode = TcTyMode
mode { mode_sat :: RequireSaturation
mode_sat = RequireSaturation
NoSaturation }

-- switch to kind level
kindLevel :: TcTyMode -> TcTyMode
kindLevel :: TcTyMode -> TcTyMode
kindLevel mode :: TcTyMode
mode = TcTyMode
mode { mode_level :: TypeOrKind
mode_level = TypeOrKind
KindLevel }

instance Outputable RequireSaturation where
  ppr :: RequireSaturation -> MsgDoc
ppr YesSaturation = String -> MsgDoc
text "YesSaturation"
  ppr NoSaturation  = String -> MsgDoc
text "NoSaturation"

instance Outputable TcTyMode where
  ppr :: TcTyMode -> MsgDoc
ppr = TypeOrKind -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TypeOrKind -> MsgDoc)
-> (TcTyMode -> TypeOrKind) -> TcTyMode -> MsgDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTyMode -> TypeOrKind
mode_level

{-
Note [Bidirectional type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In expressions, whenever we see a polymorphic identifier, say `id`, we are
free to instantiate it with metavariables, knowing that we can always
re-generalize with type-lambdas when necessary. For example:

  rank2 :: (forall a. a -> a) -> ()
  x = rank2 id

When checking the body of `x`, we can instantiate `id` with a metavariable.
Then, when we're checking the application of `rank2`, we notice that we really
need a polymorphic `id`, and then re-generalize over the unconstrained
metavariable.

In types, however, we're not so lucky, because *we cannot re-generalize*!
There is no lambda. So, we must be careful only to instantiate at the last
possible moment, when we're sure we're never going to want the lost polymorphism
again. This is done in calls to tcInstTyBinders.

To implement this behavior, we use bidirectional type checking, where we
explicitly think about whether we know the kind of the type we're checking
or not. Note that there is a difference between not knowing a kind and
knowing a metavariable kind: the metavariables are TauTvs, and cannot become
forall-quantified kinds. Previously (before dependent types), there were
no higher-rank kinds, and so we could instantiate early and be sure that
no types would have polymorphic kinds, and so we could always assume that
the kind of a type was a fresh metavariable. Not so anymore, thus the
need for two algorithms.

For HsType forms that can never be kind-polymorphic, we implement only the
"down" direction, where we safely assume a metavariable kind. For HsType forms
that *can* be kind-polymorphic, we implement just the "up" (functions with
"infer" in their name) version, as we gain nothing by also implementing the
"down" version.

Note [Future-proofing the type checker]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As discussed in Note [Bidirectional type checking], each HsType form is
handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
are mutually recursive, so that either one can work for any type former.
But, we want to make sure that our pattern-matches are complete. So,
we have a bunch of repetitive code just so that we get warnings if we're
missing any patterns.

Note [The tcType invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
(IT1) If    tc_ty = tc_hs_type hs_ty exp_kind
      then  tcTypeKind tc_ty = exp_kind
without any zonking needed.  The reason for this is that in
tcInferApps we see (F ty), and we kind-check 'ty' with an
expected-kind coming from F.  Then, to make the resulting application
well kinded --- see Note [The well-kinded type invariant] in TcType ---
we need the kind-checked 'ty' to have exactly the kind that F expects,
with no funny zonking nonsense in between.

The tcType invariant also applies to checkExpectedKind:

(IT2) if
        (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
      then
        tcTypeKind tc_ty = exp_ki

These other invariants are all necessary, too, as these functions
are used within tc_hs_type:

(IT3) If (ty, ki) <- tc_infer_hs_type ..., then tcTypeKind ty == ki.

(IT4) If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
      (In other words, the result kind of tc_infer_hs_type is zonked.)

(IT5) If (ty, ki) <- tcTyVar ..., then tcTypeKind ty == ki.

(IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
      (In other words, the result kind of tcTyVar is zonked.)

-}

------------------------------------------
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type mode :: TcTyMode
mode (L span :: SrcSpan
span ty :: HsType GhcRn
ty)
  = SrcSpan -> TcM (Type, Type) -> TcM (Type, Type)
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
span (TcM (Type, Type) -> TcM (Type, Type))
-> TcM (Type, Type) -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$
    do { (ty' :: Type
ty', kind :: Type
kind) <- TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type TcTyMode
mode HsType GhcRn
ty
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Type
kind) }

-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type mode :: TcTyMode
mode (HsParTy _ t :: LHsType GhcRn
t)          = TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
t
tc_infer_hs_type mode :: TcTyMode
mode (HsTyVar _ _ (L _ tv :: IdP GhcRn
tv)) = TcTyMode -> Name -> TcM (Type, Type)
tcTyVar TcTyMode
mode Name
IdP GhcRn
tv

tc_infer_hs_type mode :: TcTyMode
mode e :: HsType GhcRn
e@(HsAppTy {}) = TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tcTyApp TcTyMode
mode HsType GhcRn
e
tc_infer_hs_type mode :: TcTyMode
mode e :: HsType GhcRn
e@(HsAppKindTy {}) = TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tcTyApp TcTyMode
mode HsType GhcRn
e

tc_infer_hs_type mode :: TcTyMode
mode (HsOpTy _ lhs :: LHsType GhcRn
lhs lhs_op :: GenLocated SrcSpan (IdP GhcRn)
lhs_op@(L _ hs_op :: IdP GhcRn
hs_op) rhs :: LHsType GhcRn
rhs)
  | Bool -> Bool
not (Name
IdP GhcRn
hs_op Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey)
  = do { (op :: Type
op, op_kind :: Type
op_kind) <- TcTyMode -> Name -> TcM (Type, Type)
tcTyVar TcTyMode
mode Name
IdP GhcRn
hs_op
       ; TcTyMode
-> LHsType GhcRn
-> Type
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
tcTyApps TcTyMode
mode (SrcSpanLess (LHsType GhcRn) -> LHsType GhcRn
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsType GhcRn) -> LHsType GhcRn)
-> SrcSpanLess (LHsType GhcRn) -> LHsType GhcRn
forall a b. (a -> b) -> a -> b
$ XTyVar GhcRn
-> PromotionFlag -> GenLocated SrcSpan (IdP GhcRn) -> HsType GhcRn
forall pass.
XTyVar pass -> PromotionFlag -> Located (IdP pass) -> HsType pass
HsTyVar XTyVar GhcRn
NoExt
noExt PromotionFlag
NotPromoted GenLocated SrcSpan (IdP GhcRn)
lhs_op) Type
op Type
op_kind
                       [LHsType GhcRn -> LHsTypeArg GhcRn
forall tm ty. tm -> HsArg tm ty
HsValArg LHsType GhcRn
lhs, LHsType GhcRn -> LHsTypeArg GhcRn
forall tm ty. tm -> HsArg tm ty
HsValArg LHsType GhcRn
rhs] }

tc_infer_hs_type mode :: TcTyMode
mode (HsKindSig _ ty :: LHsType GhcRn
ty sig :: LHsType GhcRn
sig)
  = do { Type
sig' <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig UserTypeCtxt
KindSigCtxt LHsType GhcRn
sig
                 -- We must typecheck the kind signature, and solve all
                 -- its equalities etc; from this point on we may do
                 -- things like instantiate its foralls, so it needs
                 -- to be fully determined (Trac #14904)
       ; String -> MsgDoc -> TcM ()
traceTc "tc_infer_hs_type:sig" (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
ty MsgDoc -> MsgDoc -> MsgDoc
$$ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
sig')
       ; Type
ty' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
sig'
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Type
sig') }

-- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
-- the splice location to the typechecker. Here we skip over it in order to have
-- the same kind inferred for a given expression whether it was produced from
-- splices or not.
--
-- See Note [Delaying modFinalizers in untyped splices].
tc_infer_hs_type mode :: TcTyMode
mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty :: HsType GhcRn
ty)))
  = TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type TcTyMode
mode HsType GhcRn
ty

tc_infer_hs_type mode :: TcTyMode
mode (HsDocTy _ ty :: LHsType GhcRn
ty _) = TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
ty
tc_infer_hs_type _    (XHsType (NHsCoreTy ty))
  = do { Type
ty <- Type -> TcM Type
zonkTcType Type
ty  -- (IT3) and (IT4) of Note [The tcType invariant]
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty) }

tc_infer_hs_type _ (HsExplicitListTy _ _ tys :: [LHsType GhcRn]
tys)
  | [LHsType GhcRn] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LHsType GhcRn]
tys  -- this is so that we can use visible kind application with '[]
              -- e.g ... '[] @Bool
  = (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type
mkTyConTy TyCon
promotedNilDataCon,
            [TcTyVar] -> Type -> Type
mkSpecForAllTys [TcTyVar
alphaTyVar] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkListTy Type
alphaTy)

tc_infer_hs_type mode :: TcTyMode
mode other_ty :: HsType GhcRn
other_ty
  = do { Type
kv <- TcM Type
newMetaKindVar
       ; Type
ty' <- TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_hs_type TcTyMode
mode HsType GhcRn
other_ty Type
kv
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Type
kv) }

------------------------------------------
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type mode :: TcTyMode
mode (L span :: SrcSpan
span ty :: HsType GhcRn
ty) exp_kind :: Type
exp_kind
  = SrcSpan -> TcM Type -> TcM Type
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
span (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_hs_type TcTyMode
mode HsType GhcRn
ty Type
exp_kind

------------------------------------------
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
            -> TcM TcType
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> Type -> TcM Type
tc_fun_type mode :: TcTyMode
mode ty1 :: LHsType GhcRn
ty1 ty2 :: LHsType GhcRn
ty2 exp_kind :: Type
exp_kind = case TcTyMode -> TypeOrKind
mode_level TcTyMode
mode of
  TypeLevel ->
    do { Type
arg_k <- TcM Type
newOpenTypeKind
       ; Type
res_k <- TcM Type
newOpenTypeKind
       ; Type
ty1' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty1 Type
arg_k
       ; Type
ty2' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty2 Type
res_k
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (HsType GhcRn -> MsgDoc) -> HsType GhcRn -> MsgDoc
forall a b. (a -> b) -> a -> b
$ XFunTy GhcRn -> LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn
forall pass.
XFunTy pass -> LHsType pass -> LHsType pass -> HsType pass
HsFunTy XFunTy GhcRn
NoExt
noExt LHsType GhcRn
ty1 LHsType GhcRn
ty2) (Type -> Type -> Type
mkFunTy Type
ty1' Type
ty2')
                           Type
liftedTypeKind Type
exp_kind }
  KindLevel ->  -- no representation polymorphism in kinds. yet.
    do { Type
ty1' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty1 Type
liftedTypeKind
       ; Type
ty2' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty2 Type
liftedTypeKind
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (HsType GhcRn -> MsgDoc) -> HsType GhcRn -> MsgDoc
forall a b. (a -> b) -> a -> b
$ XFunTy GhcRn -> LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn
forall pass.
XFunTy pass -> LHsType pass -> LHsType pass -> HsType pass
HsFunTy XFunTy GhcRn
NoExt
noExt LHsType GhcRn
ty1 LHsType GhcRn
ty2) (Type -> Type -> Type
mkFunTy Type
ty1' Type
ty2')
                           Type
liftedTypeKind Type
exp_kind }

------------------------------------------
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
-- See Note [The tcType invariant]
-- See Note [Bidirectional type checking]

tc_hs_type :: TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_hs_type mode :: TcTyMode
mode (HsParTy _ ty :: LHsType GhcRn
ty)   exp_kind :: Type
exp_kind = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind
tc_hs_type mode :: TcTyMode
mode (HsDocTy _ ty :: LHsType GhcRn
ty _) exp_kind :: Type
exp_kind = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind
tc_hs_type _ ty :: HsType GhcRn
ty@(HsBangTy _ bang :: HsSrcBang
bang _) _
    -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
    -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
    -- bangs are invalid, so fail. (#7210, #14761)
    = do { let bangError :: String -> TcM Type
bangError err :: String
err = MsgDoc -> TcM Type
forall a. MsgDoc -> TcM a
failWith (MsgDoc -> TcM Type) -> MsgDoc -> TcM Type
forall a b. (a -> b) -> a -> b
$
                 String -> MsgDoc
text "Unexpected" MsgDoc -> MsgDoc -> MsgDoc
<+> String -> MsgDoc
text String
err MsgDoc -> MsgDoc -> MsgDoc
<+> String -> MsgDoc
text "annotation:" MsgDoc -> MsgDoc -> MsgDoc
<+> HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty MsgDoc -> MsgDoc -> MsgDoc
$$
                 String -> MsgDoc
text String
err MsgDoc -> MsgDoc -> MsgDoc
<+> String -> MsgDoc
text "annotation cannot appear nested inside a type"
         ; case HsSrcBang
bang of
             HsSrcBang _ SrcUnpack _           -> String -> TcM Type
bangError "UNPACK"
             HsSrcBang _ SrcNoUnpack _         -> String -> TcM Type
bangError "NOUNPACK"
             HsSrcBang _ NoSrcUnpack SrcLazy   -> String -> TcM Type
bangError "laziness"
             HsSrcBang _ _ _                   -> String -> TcM Type
bangError "strictness" }
tc_hs_type _ ty :: HsType GhcRn
ty@(HsRecTy {})      _
      -- Record types (which only show up temporarily in constructor
      -- signatures) should have been removed by now
    = MsgDoc -> TcM Type
forall a. MsgDoc -> TcM a
failWithTc (String -> MsgDoc
text "Record syntax is illegal here:" MsgDoc -> MsgDoc -> MsgDoc
<+> HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)

-- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
-- Here we get rid of it and add the finalizers to the global environment
-- while capturing the local environment.
--
-- See Note [Delaying modFinalizers in untyped splices].
tc_hs_type mode :: TcTyMode
mode (HsSpliceTy _ (HsSpliced _ mod_finalizers :: ThModFinalizers
mod_finalizers (HsSplicedTy ty :: HsType GhcRn
ty)))
           exp_kind :: Type
exp_kind
  = do ThModFinalizers -> TcM ()
addModFinalizersWithLclEnv ThModFinalizers
mod_finalizers
       TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_hs_type TcTyMode
mode HsType GhcRn
ty Type
exp_kind

-- This should never happen; type splices are expanded by the renamer
tc_hs_type _ ty :: HsType GhcRn
ty@(HsSpliceTy {}) _exp_kind :: Type
_exp_kind
  = MsgDoc -> TcM Type
forall a. MsgDoc -> TcM a
failWithTc (String -> MsgDoc
text "Unexpected type splice:" MsgDoc -> MsgDoc -> MsgDoc
<+> HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)

---------- Functions and applications
tc_hs_type mode :: TcTyMode
mode (HsFunTy _ ty1 :: LHsType GhcRn
ty1 ty2 :: LHsType GhcRn
ty2) exp_kind :: Type
exp_kind
  = TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> Type -> TcM Type
tc_fun_type TcTyMode
mode LHsType GhcRn
ty1 LHsType GhcRn
ty2 Type
exp_kind

tc_hs_type mode :: TcTyMode
mode (HsOpTy _ ty1 :: LHsType GhcRn
ty1 (L _ op :: IdP GhcRn
op) ty2 :: LHsType GhcRn
ty2) exp_kind :: Type
exp_kind
  | Name
IdP GhcRn
op Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey
  = TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> Type -> TcM Type
tc_fun_type TcTyMode
mode LHsType GhcRn
ty1 LHsType GhcRn
ty2 Type
exp_kind

--------- Foralls
tc_hs_type mode :: TcTyMode
mode forall :: HsType GhcRn
forall@(HsForAllTy { hst_bndrs :: forall pass. HsType pass -> [LHsTyVarBndr pass]
hst_bndrs = [LHsTyVarBndr GhcRn]
hs_tvs, hst_body :: forall pass. HsType pass -> LHsType pass
hst_body = LHsType GhcRn
ty }) exp_kind :: Type
exp_kind
  = do { (tclvl :: TcLevel
tclvl, wanted :: WantedConstraints
wanted, (tvs' :: [TcTyVar]
tvs', ty' :: Type
ty'))
            <- TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type))
forall a. TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndCaptureConstraints (TcM ([TcTyVar], Type)
 -> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type))
forall a b. (a -> b) -> a -> b
$
               [LHsTyVarBndr GhcRn] -> TcM Type -> TcM ([TcTyVar], Type)
forall a. [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Skol [LHsTyVarBndr GhcRn]
hs_tvs (TcM Type -> TcM ([TcTyVar], Type))
-> TcM Type -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
               TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind
    -- Do not kind-generalise here!  See Note [Kind generalisation]
    -- Why exp_kind?  See Note [Body kind of HsForAllTy]
       ; let bndrs :: [TyVarBinder]
bndrs       = ArgFlag -> [TcTyVar] -> [TyVarBinder]
mkTyVarBinders ArgFlag
Specified [TcTyVar]
tvs'
             skol_info :: SkolemInfo
skol_info   = MsgDoc -> SkolemInfo
ForAllSkol (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
forall)
             m_telescope :: Maybe MsgDoc
m_telescope = MsgDoc -> Maybe MsgDoc
forall a. a -> Maybe a
Just ([MsgDoc] -> MsgDoc
sep ((LHsTyVarBndr GhcRn -> MsgDoc) -> [LHsTyVarBndr GhcRn] -> [MsgDoc]
forall a b. (a -> b) -> [a] -> [b]
map LHsTyVarBndr GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsTyVarBndr GhcRn]
hs_tvs))

       ; SkolemInfo
-> Maybe MsgDoc
-> [TcTyVar]
-> TcLevel
-> WantedConstraints
-> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info Maybe MsgDoc
m_telescope [TcTyVar]
tvs' TcLevel
tclvl WantedConstraints
wanted

       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBinder] -> Type -> Type
mkForAllTys [TyVarBinder]
bndrs Type
ty') }

tc_hs_type mode :: TcTyMode
mode (HsQualTy { hst_ctxt :: forall pass. HsType pass -> LHsContext pass
hst_ctxt = LHsContext GhcRn
ctxt, hst_body :: forall pass. HsType pass -> LHsType pass
hst_body = LHsType GhcRn
ty }) exp_kind :: Type
exp_kind
  | [LHsType GhcRn] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (LHsContext GhcRn -> SrcSpanLess (LHsContext GhcRn)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsContext GhcRn
ctxt)
  = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind

  | Bool
otherwise
  = do { [Type]
ctxt' <- TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context TcTyMode
mode LHsContext GhcRn
ctxt

         -- See Note [Body kind of a HsQualTy]
       ; Type
ty' <- if Type -> Bool
tcIsConstraintKind Type
exp_kind
                then TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
constraintKind
                else do { Type
ek <- TcM Type
newOpenTypeKind
                                -- The body kind (result of the function)
                                -- can be TYPE r, for any r, hence newOpenTypeKind
                        ; Type
ty' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
ek
                        ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
ty) Type
ty' Type
liftedTypeKind Type
exp_kind }

       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type -> Type
mkPhiTy [Type]
ctxt' Type
ty') }

--------- Lists, arrays, and tuples
tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsListTy _ elt_ty :: LHsType GhcRn
elt_ty) exp_kind :: Type
exp_kind
  = do { Type
tau_ty <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
elt_ty Type
liftedTypeKind
       ; TyCon -> TcM ()
checkWiredInTyCon TyCon
listTyCon
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) (Type -> Type
mkListTy Type
tau_ty) Type
liftedTypeKind Type
exp_kind }

-- See Note [Distinguishing tuple kinds] in HsTypes
-- See Note [Inferring tuple kinds]
tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys :: [LHsType GhcRn]
hs_tys) exp_kind :: Type
exp_kind
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
  | Just tup_sort :: TupleSort
tup_sort <- Type -> Maybe TupleSort
tupKindSort_maybe Type
exp_kind
  = String -> MsgDoc -> TcM ()
traceTc "tc_hs_type tuple" ([LHsType GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsType GhcRn]
hs_tys) TcM () -> TcM Type -> TcM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
    HsType GhcRn
-> TcTyMode -> TupleSort -> [LHsType GhcRn] -> Type -> TcM Type
tc_tuple HsType GhcRn
rn_ty TcTyMode
mode TupleSort
tup_sort [LHsType GhcRn]
hs_tys Type
exp_kind
  | Bool
otherwise
  = do { String -> MsgDoc -> TcM ()
traceTc "tc_hs_type tuple 2" ([LHsType GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsType GhcRn]
hs_tys)
       ; (tys :: [Type]
tys, kinds :: [Type]
kinds) <- (LHsType GhcRn -> TcM (Type, Type))
-> [LHsType GhcRn]
-> IOEnv (Env TcGblEnv TcLclEnv) ([Type], [Type])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode) [LHsType GhcRn]
hs_tys
       ; [Type]
kinds <- (Type -> TcM Type) -> [Type] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> TcM Type
zonkTcType [Type]
kinds
           -- Infer each arg type separately, because errors can be
           -- confusing if we give them a shared kind.  Eg Trac #7410
           -- (Either Int, Int), we do not want to get an error saying
           -- "the second argument of a tuple should have kind *->*"

       ; let (arg_kind :: Type
arg_kind, tup_sort :: TupleSort
tup_sort)
               = case [ (Type
k,TupleSort
s) | Type
k <- [Type]
kinds
                              , Just s :: TupleSort
s <- [Type -> Maybe TupleSort
tupKindSort_maybe Type
k] ] of
                    ((k :: Type
k,s :: TupleSort
s) : _) -> (Type
k,TupleSort
s)
                    [] -> (Type
liftedTypeKind, TupleSort
BoxedTuple)
         -- In the [] case, it's not clear what the kind is, so guess *

       ; [Type]
tys' <- [TcM Type] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ SrcSpan -> TcM Type -> TcM Type
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                            HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
hs_ty) Type
ty Type
kind Type
arg_kind
                          | ((L loc :: SrcSpan
loc hs_ty :: HsType GhcRn
hs_ty),ty :: Type
ty,kind :: Type
kind) <- [LHsType GhcRn]
-> [Type] -> [Type] -> [(LHsType GhcRn, Type, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [LHsType GhcRn]
hs_tys [Type]
tys [Type]
kinds ]

       ; HsType GhcRn
-> TcTyMode -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple HsType GhcRn
rn_ty TcTyMode
mode TupleSort
tup_sort [Type]
tys' ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type -> Type
forall a b. a -> b -> a
const Type
arg_kind) [Type]
tys') Type
exp_kind }


tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTupleTy _ hs_tup_sort :: HsTupleSort
hs_tup_sort tys :: [LHsType GhcRn]
tys) exp_kind :: Type
exp_kind
  = HsType GhcRn
-> TcTyMode -> TupleSort -> [LHsType GhcRn] -> Type -> TcM Type
tc_tuple HsType GhcRn
rn_ty TcTyMode
mode TupleSort
tup_sort [LHsType GhcRn]
tys Type
exp_kind
  where
    tup_sort :: TupleSort
tup_sort = case HsTupleSort
hs_tup_sort of  -- Fourth case dealt with above
                  HsUnboxedTuple    -> TupleSort
UnboxedTuple
                  HsBoxedTuple      -> TupleSort
BoxedTuple
                  HsConstraintTuple -> TupleSort
ConstraintTuple
                  _                 -> String -> TupleSort
forall a. String -> a
panic "tc_hs_type HsTupleTy"

tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsSumTy _ hs_tys :: [LHsType GhcRn]
hs_tys) exp_kind :: Type
exp_kind
  = do { let arity :: Int
arity = [LHsType GhcRn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LHsType GhcRn]
hs_tys
       ; [Type]
arg_kinds <- (LHsType GhcRn -> TcM Type) -> [LHsType GhcRn] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\_ -> TcM Type
newOpenTypeKind) [LHsType GhcRn]
hs_tys
       ; [Type]
tau_tys   <- (LHsType GhcRn -> Type -> TcM Type)
-> [LHsType GhcRn] -> [Type] -> TcM [Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode) [LHsType GhcRn]
hs_tys [Type]
arg_kinds
       ; let arg_reps :: [Type]
arg_reps = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Type -> Type
Type -> Type
kindRep [Type]
arg_kinds
             arg_tys :: [Type]
arg_tys  = [Type]
arg_reps [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tau_tys
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty)
                           (TyCon -> [Type] -> Type
mkTyConApp (Int -> TyCon
sumTyCon Int
arity) [Type]
arg_tys)
                           ([Type] -> Type
unboxedSumKind [Type]
arg_reps)
                           Type
exp_kind
       }

--------- Promoted lists and tuples
tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsExplicitListTy _ _ tys :: [LHsType GhcRn]
tys) exp_kind :: Type
exp_kind
  = do { [(Type, Type)]
tks <- (LHsType GhcRn -> TcM (Type, Type))
-> [LHsType GhcRn] -> IOEnv (Env TcGblEnv TcLclEnv) [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode) [LHsType GhcRn]
tys
       ; (taus' :: [Type]
taus', kind :: Type
kind) <- [LHsType GhcRn] -> [(Type, Type)] -> TcM ([Type], Type)
unifyKinds [LHsType GhcRn]
tys [(Type, Type)]
tks
       ; let ty :: Type
ty = ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type -> Type -> Type
mk_cons Type
kind) (Type -> Type
mk_nil Type
kind) [Type]
taus')
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) Type
ty (Type -> Type
mkListTy Type
kind) Type
exp_kind }
  where
    mk_cons :: Type -> Type -> Type -> Type
mk_cons k :: Type
k a :: Type
a b :: Type
b = TyCon -> [Type] -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
consDataCon) [Type
k, Type
a, Type
b]
    mk_nil :: Type -> Type
mk_nil  k :: Type
k     = TyCon -> [Type] -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
nilDataCon) [Type
k]

tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsExplicitTupleTy _ tys :: [LHsType GhcRn]
tys) exp_kind :: Type
exp_kind
  -- using newMetaKindVar means that we force instantiations of any polykinded
  -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
  = do { [Type]
ks   <- Int -> TcM Type -> TcM [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
arity TcM Type
newMetaKindVar
       ; [Type]
taus <- (LHsType GhcRn -> Type -> TcM Type)
-> [LHsType GhcRn] -> [Type] -> TcM [Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode) [LHsType GhcRn]
tys [Type]
ks
       ; let kind_con :: TyCon
kind_con   = Boxity -> Int -> TyCon
tupleTyCon           Boxity
Boxed Int
arity
             ty_con :: TyCon
ty_con     = Boxity -> Int -> TyCon
promotedTupleDataCon Boxity
Boxed Int
arity
             tup_k :: Type
tup_k      = TyCon -> [Type] -> Type
mkTyConApp TyCon
kind_con [Type]
ks
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) (TyCon -> [Type] -> Type
mkTyConApp TyCon
ty_con ([Type]
ks [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
taus)) Type
tup_k Type
exp_kind }
  where
    arity :: Int
arity = [LHsType GhcRn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LHsType GhcRn]
tys

--------- Constraint types
tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsIParamTy _ (L _ n :: HsIPName
n) ty :: LHsType GhcRn
ty) exp_kind :: Type
exp_kind
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; Type
ty' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
liftedTypeKind
       ; let n' :: Type
n' = FastString -> Type
mkStrLitTy (FastString -> Type) -> FastString -> Type
forall a b. (a -> b) -> a -> b
$ HsIPName -> FastString
hsIPNameFS HsIPName
n
       ; Class
ipClass <- Name -> TcM Class
tcLookupClass Name
ipClassName
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) (Class -> [Type] -> Type
mkClassPred Class
ipClass [Type
n',Type
ty'])
           Type
constraintKind Type
exp_kind }

tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsStarTy _ _) exp_kind :: Type
exp_kind
  -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
  -- handle it in 'coreView' and 'tcView'.
  = HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) Type
liftedTypeKind Type
liftedTypeKind Type
exp_kind

--------- Literals
tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTyLit _ (HsNumTy _ n :: Integer
n)) exp_kind :: Type
exp_kind
  = do { TyCon -> TcM ()
checkWiredInTyCon TyCon
typeNatKindCon
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) (Integer -> Type
mkNumLitTy Integer
n) Type
typeNatKind Type
exp_kind }

tc_hs_type mode :: TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTyLit _ (HsStrTy _ s :: FastString
s)) exp_kind :: Type
exp_kind
  = do { TyCon -> TcM ()
checkWiredInTyCon TyCon
typeSymbolKindCon
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) (FastString -> Type
mkStrLitTy FastString
s) Type
typeSymbolKind Type
exp_kind }

--------- Potentially kind-polymorphic types: call the "up" checker
-- See Note [Future-proofing the type checker]
tc_hs_type mode :: TcTyMode
mode ty :: HsType GhcRn
ty@(HsTyVar {})   ek :: Type
ek = HasDebugCallStack => TcTyMode -> HsType GhcRn -> Type -> TcM Type
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek TcTyMode
mode HsType GhcRn
ty Type
ek
tc_hs_type mode :: TcTyMode
mode ty :: HsType GhcRn
ty@(HsAppTy {})   ek :: Type
ek = HasDebugCallStack => TcTyMode -> HsType GhcRn -> Type -> TcM Type
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek TcTyMode
mode HsType GhcRn
ty Type
ek
tc_hs_type mode :: TcTyMode
mode ty :: HsType GhcRn
ty@(HsAppKindTy{}) ek :: Type
ek = HasDebugCallStack => TcTyMode -> HsType GhcRn -> Type -> TcM Type
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek TcTyMode
mode HsType GhcRn
ty Type
ek
tc_hs_type mode :: TcTyMode
mode ty :: HsType GhcRn
ty@(HsOpTy {})    ek :: Type
ek = HasDebugCallStack => TcTyMode -> HsType GhcRn -> Type -> TcM Type
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek TcTyMode
mode HsType GhcRn
ty Type
ek
tc_hs_type mode :: TcTyMode
mode ty :: HsType GhcRn
ty@(HsKindSig {}) ek :: Type
ek = HasDebugCallStack => TcTyMode -> HsType GhcRn -> Type -> TcM Type
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek TcTyMode
mode HsType GhcRn
ty Type
ek
tc_hs_type mode :: TcTyMode
mode ty :: HsType GhcRn
ty@(XHsType (NHsCoreTy{})) ek :: Type
ek = HasDebugCallStack => TcTyMode -> HsType GhcRn -> Type -> TcM Type
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek TcTyMode
mode HsType GhcRn
ty Type
ek

tc_hs_type mode :: TcTyMode
mode wc :: HsType GhcRn
wc@(HsWildCardTy _) exp_kind :: Type
exp_kind
  = do { Type
wc_ty <- TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcWildCardOcc TcTyMode
mode HsType GhcRn
wc Type
exp_kind
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion -> Type
mkNakedCastTy Type
wc_ty (Type -> Coercion
mkTcNomReflCo Type
exp_kind))
         -- Take care here! Even though the coercion is Refl,
         -- we still need it to establish Note [The tcType invariant]
       }

tcWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
tcWildCardOcc :: TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcWildCardOcc mode :: TcTyMode
mode wc :: HsType GhcRn
wc exp_kind :: Type
exp_kind
  = do { TcTyVar
wc_tv <- TcM TcTyVar
newWildTyVar
          -- The wildcard's kind should be an un-filled-in meta tyvar
       ; SrcSpan
loc <- TcRn SrcSpan
getSrcSpanM
       ; Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
       ; let name :: Name
name = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq (String -> OccName
mkTyVarOcc "_") SrcSpan
loc
       ; Bool
part_tysig <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.PartialTypeSignatures
       ; Bool
warning <- WarningFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. WarningFlag -> TcRnIf gbl lcl Bool
woptM WarningFlag
Opt_WarnPartialTypeSignatures
       -- See Note [Wildcards in visible kind application]
       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
part_tysig Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
warning)
             ([(Name, TcTyVar)] -> TcM ()
emitWildCardHoleConstraints [(Name
name,TcTyVar
wc_tv)])
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
wc) (TcTyVar -> Type
mkTyVarTy TcTyVar
wc_tv)
                           (TcTyVar -> Type
tyVarKind TcTyVar
wc_tv) Type
exp_kind }

{- Note [Wildcards in visible kind application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are cases where users might want to pass in a wildcard as a visible kind
argument, for instance:

data T :: forall k1 k2. k1 → k2 → Type where
  MkT :: T a b
x :: T @_ @Nat False n
x = MkT

So we should allow '@_' without emitting any hole constraints, and
regardless of whether PartialTypeSignatures is enabled or not. But how would
the typechecker know which '_' is being used in VKA and which is not when it
calls emitWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
but instead give every unnamed wildcard a fresh wild tyvar in tcWildCardOcc.
And whenever we see a '@', we automatically turn on PartialTypeSignatures and
turn off hole constraint warnings, and never call emitWildCardHoleConstraints
under these conditions.
See related Note [Wildcards in visible type application] here and
Note [The wildcard story for types] in HsTypes.hs

-}
---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_infer_hs_type_ek mode :: TcTyMode
mode hs_ty :: HsType GhcRn
hs_ty ek :: Type
ek
  = do { (ty :: Type
ty, k :: Type
k) <- TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type TcTyMode
mode HsType GhcRn
hs_ty
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
hs_ty) Type
ty Type
k Type
ek }

---------------------------
tupKindSort_maybe :: TcKind -> Maybe TupleSort
tupKindSort_maybe :: Type -> Maybe TupleSort
tupKindSort_maybe k :: Type
k
  | Just (k' :: Type
k', _) <- Type -> Maybe (Type, Coercion)
splitCastTy_maybe Type
k = Type -> Maybe TupleSort
tupKindSort_maybe Type
k'
  | Just k' :: Type
k'      <- Type -> Maybe Type
tcView Type
k            = Type -> Maybe TupleSort
tupKindSort_maybe Type
k'
  | Type -> Bool
tcIsConstraintKind Type
k = TupleSort -> Maybe TupleSort
forall a. a -> Maybe a
Just TupleSort
ConstraintTuple
  | Type -> Bool
tcIsLiftedTypeKind Type
k   = TupleSort -> Maybe TupleSort
forall a. a -> Maybe a
Just TupleSort
BoxedTuple
  | Bool
otherwise            = Maybe TupleSort
forall a. Maybe a
Nothing

tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
tc_tuple :: HsType GhcRn
-> TcTyMode -> TupleSort -> [LHsType GhcRn] -> Type -> TcM Type
tc_tuple rn_ty :: HsType GhcRn
rn_ty mode :: TcTyMode
mode tup_sort :: TupleSort
tup_sort tys :: [LHsType GhcRn]
tys exp_kind :: Type
exp_kind
  = do { [Type]
arg_kinds <- case TupleSort
tup_sort of
           BoxedTuple      -> [Type] -> TcM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Type -> [Type]
forall a. Int -> a -> [a]
nOfThem Int
arity Type
liftedTypeKind)
           UnboxedTuple    -> (LHsType GhcRn -> TcM Type) -> [LHsType GhcRn] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\_ -> TcM Type
newOpenTypeKind) [LHsType GhcRn]
tys
           ConstraintTuple -> [Type] -> TcM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Type -> [Type]
forall a. Int -> a -> [a]
nOfThem Int
arity Type
constraintKind)
       ; [Type]
tau_tys <- (LHsType GhcRn -> Type -> TcM Type)
-> [LHsType GhcRn] -> [Type] -> TcM [Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode) [LHsType GhcRn]
tys [Type]
arg_kinds
       ; HsType GhcRn
-> TcTyMode -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple HsType GhcRn
rn_ty TcTyMode
mode TupleSort
tup_sort [Type]
tau_tys [Type]
arg_kinds Type
exp_kind }
  where
    arity :: Int
arity   = [LHsType GhcRn] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LHsType GhcRn]
tys

finish_tuple :: HsType GhcRn
             -> TcTyMode
             -> TupleSort
             -> [TcType]    -- ^ argument types
             -> [TcKind]    -- ^ of these kinds
             -> TcKind      -- ^ expected kind of the whole tuple
             -> TcM TcType
finish_tuple :: HsType GhcRn
-> TcTyMode -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple rn_ty :: HsType GhcRn
rn_ty mode :: TcTyMode
mode tup_sort :: TupleSort
tup_sort tau_tys :: [Type]
tau_tys tau_kinds :: [Type]
tau_kinds exp_kind :: Type
exp_kind
  = do { String -> MsgDoc -> TcM ()
traceTc "finish_tuple" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_kind MsgDoc -> MsgDoc -> MsgDoc
$$ [Type] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Type]
tau_kinds MsgDoc -> MsgDoc -> MsgDoc
$$ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind)
       ; let arg_tys :: [Type]
arg_tys  = case TupleSort
tup_sort of
                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
                 UnboxedTuple    -> [Type]
tau_reps [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tau_tys
                 BoxedTuple      -> [Type]
tau_tys
                 ConstraintTuple -> [Type]
tau_tys
       ; TyCon
tycon <- case TupleSort
tup_sort of
           ConstraintTuple
             | Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
mAX_CTUPLE_SIZE
                         -> MsgDoc -> TcRn TyCon
forall a. MsgDoc -> TcM a
failWith (Int -> MsgDoc
bigConstraintTuple Int
arity)
             | Bool
otherwise -> Name -> TcRn TyCon
tcLookupTyCon (Int -> Name
cTupleTyConName Int
arity)
           BoxedTuple    -> do { let tc :: TyCon
tc = Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
arity
                               ; TyCon -> TcM ()
checkWiredInTyCon TyCon
tc
                               ; TyCon -> TcRn TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc }
           UnboxedTuple  -> TyCon -> TcRn TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return (Boxity -> Int -> TyCon
tupleTyCon Boxity
Unboxed Int
arity)
       ; HasDebugCallStack =>
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
rn_ty) (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
arg_tys) Type
res_kind Type
exp_kind }
  where
    arity :: Int
arity = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tau_tys
    tau_reps :: [Type]
tau_reps = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Type -> Type
Type -> Type
kindRep [Type]
tau_kinds
    res_kind :: Type
res_kind = case TupleSort
tup_sort of
                 UnboxedTuple    -> [Type] -> Type
unboxedTupleKind [Type]
tau_reps
                 BoxedTuple      -> Type
liftedTypeKind
                 ConstraintTuple -> Type
constraintKind

bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple :: Int -> MsgDoc
bigConstraintTuple arity :: Int
arity
  = MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "Constraint tuple arity too large:" MsgDoc -> MsgDoc -> MsgDoc
<+> Int -> MsgDoc
int Int
arity
          MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
parens (String -> MsgDoc
text "max arity =" MsgDoc -> MsgDoc -> MsgDoc
<+> Int -> MsgDoc
int Int
mAX_CTUPLE_SIZE))
       2 (String -> MsgDoc
text "Instead, use a nested tuple")

---------------------------
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. Always consumes all the arguments,
-- using matchExpectedFunKind as necessary.
-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.-
-- These kinds should be used to instantiate invisible kind variables;
-- they come from an enclosing class for an associated type/data family.
tcInferApps :: TcTyMode
            -> LHsType GhcRn        -- ^ Function (for printing only)
            -> TcType               -- ^ Function
            -> TcKind               -- ^ Function kind (zonked)
            -> [LHsTypeArg GhcRn]   -- ^ Args
            -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
-- Precondition: tcTypeKind fun_ty = fun_ki
--    Reason: we will return a type application like (fun_ty arg1 ... argn),
--            and that type must be well-kinded
--            See Note [The tcType invariant]
-- Postcondition: Result kind is zonked.
tcInferApps :: TcTyMode
-> LHsType GhcRn
-> Type
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
tcInferApps mode :: TcTyMode
mode orig_hs_ty :: LHsType GhcRn
orig_hs_ty fun_ty :: Type
fun_ty fun_ki :: Type
fun_ki orig_hs_args :: [LHsTypeArg GhcRn]
orig_hs_args
  = do { String -> MsgDoc -> TcM ()
traceTc "tcInferApps {" (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
orig_hs_ty MsgDoc -> MsgDoc -> MsgDoc
$$ [LHsTypeArg GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsTypeArg GhcRn]
orig_hs_args MsgDoc -> MsgDoc -> MsgDoc
$$ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
fun_ki)
       ; (f_args :: Type
f_args, res_k :: Type
res_k) <- Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go 1 TCvSubst
empty_subst Type
fun_ty [TyBinder]
orig_ki_binders Type
orig_inner_ki [LHsTypeArg GhcRn]
orig_hs_args
       ; String -> MsgDoc -> TcM ()
traceTc "tcInferApps }" MsgDoc
empty
       ; Type
res_k <- Type -> TcM Type
zonkTcType Type
res_k  -- Uphold (IT4) of Note [The tcType invariant]
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
f_args, Type
res_k) }
  where
    empty_subst :: TCvSubst
empty_subst                      = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                                       Type -> VarSet
tyCoVarsOfType Type
fun_ki
    (orig_ki_binders :: [TyBinder]
orig_ki_binders, orig_inner_ki :: Type
orig_inner_ki) = Type -> ([TyBinder], Type)
tcSplitPiTys Type
fun_ki

    go :: Int             -- the # of the next argument
       -> TCvSubst        -- instantiating substitution
       -> TcType          -- function applied to some args
       -> [TyBinder]      -- binders in function kind (both vis. and invis.)
       -> TcKind          -- function kind body (not a Pi-type)
       -> [LHsTypeArg GhcRn] -- un-type-checked args
       -> TcM (TcType, TcKind)  -- same as overall return type

      -- no user-written args left. We're done!
    go :: Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go _ subst :: TCvSubst
subst fun :: Type
fun ki_binders :: [TyBinder]
ki_binders inner_ki :: Type
inner_ki []
      = (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Type
fun
               , HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
nakedSubstTy TCvSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [TyBinder] -> Type -> Type
mkPiTys [TyBinder]
ki_binders Type
inner_ki)
                 -- nakedSubstTy: see Note [The well-kinded type invariant]
    go n :: Int
n subst :: TCvSubst
subst fun :: Type
fun all_kindbinder :: [TyBinder]
all_kindbinder inner_ki :: Type
inner_ki (HsArgPar _:args :: [LHsTypeArg GhcRn]
args)
      = Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
n TCvSubst
subst Type
fun [TyBinder]
all_kindbinder Type
inner_ki [LHsTypeArg GhcRn]
args
      -- The function's kind has a binder. Is it visible or invisible?
    go n :: Int
n subst :: TCvSubst
subst fun :: Type
fun all_kindbinder :: [TyBinder]
all_kindbinder@(ki_binder :: TyBinder
ki_binder:ki_binders :: [TyBinder]
ki_binders) inner_ki :: Type
inner_ki
       all_args :: [LHsTypeArg GhcRn]
all_args@(arg :: LHsTypeArg GhcRn
arg:args :: [LHsTypeArg GhcRn]
args)
      | ArgFlag
Specified <- TyBinder -> ArgFlag
tyCoBinderArgFlag TyBinder
ki_binder
      , HsTypeArg _ ki :: LHsType GhcRn
ki <- LHsTypeArg GhcRn
arg
         -- Invisible and specified binder with visible kind argument
         = do { String -> MsgDoc -> TcM ()
traceTc "tcInferApps (vis kind app)" ([MsgDoc] -> MsgDoc
vcat [ TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder, LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
ki
                                                     , Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyBinder -> Type
tyBinderType TyBinder
ki_binder)
                                                     , TCvSubst -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TCvSubst
subst, ArgFlag -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyBinder -> ArgFlag
tyCoBinderArgFlag TyBinder
ki_binder) ])
                  ; let exp_kind :: Type
exp_kind = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
nakedSubstTy TCvSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TyBinder -> Type
tyBinderType TyBinder
ki_binder
                    -- nakedSubstTy: see Note [The well-kinded type invariant]
                  ; Type
arg' <- MsgDoc -> TcM Type -> TcM Type
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (LHsType GhcRn -> LHsType GhcRn -> Int -> MsgDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> MsgDoc
funAppCtxt LHsType GhcRn
orig_hs_ty LHsType GhcRn
ki Int
n) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                            WarningFlag -> TcM Type -> TcM Type
forall gbl lcl a.
WarningFlag -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
unsetWOptM WarningFlag
Opt_WarnPartialTypeSignatures (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                            Extension -> TcM Type -> TcM Type
forall gbl lcl a. Extension -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
setXOptM Extension
LangExt.PartialTypeSignatures (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                            -- see Note [Wildcards in visible kind application]
                            TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type (TcTyMode -> TcTyMode
kindLevel TcTyMode
mode) LHsType GhcRn
ki Type
exp_kind
                  ; String -> MsgDoc -> TcM ()
traceTc "tcInferApps (vis kind app)" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind)
                  ; let subst' :: TCvSubst
subst' = TCvSubst -> TyBinder -> Type -> TCvSubst
extendTvSubstBinderAndInScope TCvSubst
subst TyBinder
ki_binder Type
arg'
                  ; Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) TCvSubst
subst'
                       (Type -> Type -> Type
mkNakedAppTy Type
fun Type
arg')
                       [TyBinder]
ki_binders Type
inner_ki [LHsTypeArg GhcRn]
args }

      | TyBinder -> Bool
isInvisibleBinder TyBinder
ki_binder
          -- Instantiate if not specified or if there is no kind application
      = do { String -> MsgDoc -> TcM ()
traceTc "tcInferApps (invis normal app)" (TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder MsgDoc -> MsgDoc -> MsgDoc
$$ TCvSubst -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TCvSubst
subst MsgDoc -> MsgDoc -> MsgDoc
$$ ArgFlag -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyBinder -> ArgFlag
tyCoBinderArgFlag TyBinder
ki_binder))
           ; (subst' :: TCvSubst
subst', arg' :: Type
arg') <- Maybe (VarEnv Type) -> TCvSubst -> TyBinder -> TcM (TCvSubst, Type)
tcInstTyBinder Maybe (VarEnv Type)
forall a. Maybe a
Nothing TCvSubst
subst TyBinder
ki_binder
           ; Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
n TCvSubst
subst' (Type -> Type -> Type
mkNakedAppTy Type
fun Type
arg')
                        [TyBinder]
ki_binders Type
inner_ki [LHsTypeArg GhcRn]
all_args }

      | Bool
otherwise -- if binder is visible
         = case LHsTypeArg GhcRn
arg of
             HsValArg ty :: LHsType GhcRn
ty -- check the next argument
               -> do { String -> MsgDoc -> TcM ()
traceTc "tcInferApps (vis normal app)"
                         ([MsgDoc] -> MsgDoc
vcat [ TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder
                               , LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
ty
                               , Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyBinder -> Type
tyBinderType TyBinder
ki_binder)
                               , TCvSubst -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TCvSubst
subst ])
                     ; let exp_kind :: Type
exp_kind = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
nakedSubstTy TCvSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TyBinder -> Type
tyBinderType TyBinder
ki_binder
                     -- nakedSubstTy: see Note [The well-kinded type invariant]
                     ; Type
arg' <- MsgDoc -> TcM Type -> TcM Type
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (LHsType GhcRn -> LHsType GhcRn -> Int -> MsgDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> MsgDoc
funAppCtxt LHsType GhcRn
orig_hs_ty LHsType GhcRn
ty Int
n) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                               TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind
                     ; String -> MsgDoc -> TcM ()
traceTc "tcInferApps (vis normal app)" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind)
                     ; let subst' :: TCvSubst
subst' = TCvSubst -> TyBinder -> Type -> TCvSubst
extendTvSubstBinderAndInScope TCvSubst
subst TyBinder
ki_binder Type
arg'
                     ; Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) TCvSubst
subst'
                          (Type -> Type -> Type
mkNakedAppTy Type
fun Type
arg')
                          [TyBinder]
ki_binders Type
inner_ki [LHsTypeArg GhcRn]
args }
            -- error if the argument is a kind application
             HsTypeArg _ ki :: LHsType GhcRn
ki -> do { String -> MsgDoc -> TcM ()
traceTc "tcInferApps (error)"
                                    ([MsgDoc] -> MsgDoc
vcat [ TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder
                                          , LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
ki
                                          , Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyBinder -> Type
tyBinderType TyBinder
ki_binder)
                                          , TCvSubst -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TCvSubst
subst
                                          , Bool -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyBinder -> Bool
isInvisibleBinder TyBinder
ki_binder) ])
                                  ; LHsType GhcRn -> Type -> TcM (Type, Type)
forall a a a. (Outputable a, Outputable a) => a -> a -> TcRn a
ty_app_err LHsType GhcRn
ki (Type -> TcM (Type, Type)) -> Type -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$ HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
nakedSubstTy TCvSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                                                  [TyBinder] -> Type -> Type
mkPiTys [TyBinder]
all_kindbinder Type
inner_ki }

             HsArgPar _ -> String -> TcM (Type, Type)
forall a. String -> a
panic "tcInferApps"  -- handled in separate clause of "go"

       -- We've run out of known binders in the functions's kind.
    go n :: Int
n subst :: TCvSubst
subst fun :: Type
fun [] inner_ki :: Type
inner_ki all_args :: [LHsTypeArg GhcRn]
all_args@(arg :: LHsTypeArg GhcRn
arg:args :: [LHsTypeArg GhcRn]
args)
      | Bool -> Bool
not ([TyBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyBinder]
new_ki_binders)
         -- But, after substituting, we have more binders.
      = Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
n TCvSubst
zapped_subst Type
fun [TyBinder]
new_ki_binders Type
new_inner_ki [LHsTypeArg GhcRn]
all_args

      | Bool
otherwise
      = case LHsTypeArg GhcRn
arg of
        (HsValArg _)
         -- Even after substituting, still no binders. Use matchExpectedFunKind
         -> do { String -> MsgDoc -> TcM ()
traceTc "tcInferApps (no binder)" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
new_inner_ki MsgDoc -> MsgDoc -> MsgDoc
$$ TCvSubst -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TCvSubst
zapped_subst)
               ; (co :: Coercion
co, arg_k :: Type
arg_k, res_k :: Type
res_k) <- LHsType GhcRn -> Type -> TcM (Coercion, Type, Type)
forall fun.
Outputable fun =>
fun -> Type -> TcM (Coercion, Type, Type)
matchExpectedFunKind LHsType GhcRn
hs_ty Type
substed_inner_ki
               ; let new_in_scope :: VarSet
new_in_scope = [Type] -> VarSet
tyCoVarsOfTypes [Type
arg_k, Type
res_k]
                     subst' :: TCvSubst
subst'       = TCvSubst
zapped_subst TCvSubst -> VarSet -> TCvSubst
`extendTCvInScopeSet` VarSet
new_in_scope
               ; Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
n TCvSubst
subst'
                    (Type
fun Type -> Coercion -> Type
`mkNakedCastTy` Coercion
co)  -- See Note [The well-kinded type invariant]
                    [Type -> TyBinder
mkAnonBinder Type
arg_k]
                    Type
res_k [LHsTypeArg GhcRn]
all_args }
        (HsTypeArg _ ki :: LHsType GhcRn
ki) -> LHsType GhcRn -> Type -> TcM (Type, Type)
forall a a a. (Outputable a, Outputable a) => a -> a -> TcRn a
ty_app_err LHsType GhcRn
ki Type
substed_inner_ki
        (HsArgPar _) -> Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
n TCvSubst
subst Type
fun [] Type
inner_ki [LHsTypeArg GhcRn]
args
      where
        substed_inner_ki :: Type
substed_inner_ki               = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
inner_ki
        (new_ki_binders :: [TyBinder]
new_ki_binders, new_inner_ki :: Type
new_inner_ki) = Type -> ([TyBinder], Type)
tcSplitPiTys Type
substed_inner_ki
        zapped_subst :: TCvSubst
zapped_subst                   = TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst
        hs_ty :: LHsType GhcRn
hs_ty = LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg LHsType GhcRn
orig_hs_ty (Int -> [LHsTypeArg GhcRn] -> [LHsTypeArg GhcRn]
forall a. Int -> [a] -> [a]
take (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [LHsTypeArg GhcRn]
orig_hs_args)

    ty_app_err :: a -> a -> TcRn a
ty_app_err arg :: a
arg ty :: a
ty = MsgDoc -> TcRn a
forall a. MsgDoc -> TcM a
failWith (MsgDoc -> TcRn a) -> MsgDoc -> TcRn a
forall a b. (a -> b) -> a -> b
$ String -> MsgDoc
text "Cannot apply function of kind" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (a -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr a
ty)
                           MsgDoc -> MsgDoc -> MsgDoc
$$ String -> MsgDoc
text "to visible kind argument" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (a -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr a
arg)

appTypeToArg :: LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg :: LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg f :: LHsType GhcRn
f [] = LHsType GhcRn
f
appTypeToArg f :: LHsType GhcRn
f (HsValArg arg :: LHsType GhcRn
arg : args :: [LHsTypeArg GhcRn]
args) = LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg (LHsType GhcRn -> LHsType GhcRn -> LHsType GhcRn
forall (p :: Pass).
LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p)
mkHsAppTy LHsType GhcRn
f LHsType GhcRn
arg) [LHsTypeArg GhcRn]
args
appTypeToArg f :: LHsType GhcRn
f (HsTypeArg l :: SrcSpan
l arg :: LHsType GhcRn
arg : args :: [LHsTypeArg GhcRn]
args)
  = LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg (XAppKindTy GhcRn -> LHsType GhcRn -> LHsType GhcRn -> LHsType GhcRn
forall (p :: Pass).
XAppKindTy (GhcPass p)
-> LHsType (GhcPass p)
-> LHsType (GhcPass p)
-> LHsType (GhcPass p)
mkHsAppKindTy SrcSpan
XAppKindTy GhcRn
l LHsType GhcRn
f LHsType GhcRn
arg) [LHsTypeArg GhcRn]
args
appTypeToArg f :: LHsType GhcRn
f (HsArgPar _ : arg :: [LHsTypeArg GhcRn]
arg) = LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg LHsType GhcRn
f [LHsTypeArg GhcRn]
arg

-- | Applies a type to a list of arguments.
-- Always consumes all the arguments, using 'matchExpectedFunKind' as
-- necessary. If you wish to apply a type to a list of HsTypes, this is
-- your function.
-- Used for type-checking types only.
tcTyApps :: TcTyMode
         -> LHsType GhcRn        -- ^ Function (for printing only)
         -> TcType               -- ^ Function
         -> TcKind               -- ^ Function kind (zonked)
         -> [LHsTypeArg GhcRn]   -- ^ Args
         -> TcM (TcType, TcKind) -- ^ (f args, result kind)   result kind is zonked
-- Precondition: see precondition for tcInferApps
tcTyApps :: TcTyMode
-> LHsType GhcRn
-> Type
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
tcTyApps mode :: TcTyMode
mode orig_hs_ty :: LHsType GhcRn
orig_hs_ty fun_ty :: Type
fun_ty fun_ki :: Type
fun_ki args :: [LHsTypeArg GhcRn]
args
  = do { (ty' :: Type
ty', ki' :: Type
ki') <- TcTyMode
-> LHsType GhcRn
-> Type
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
tcInferApps TcTyMode
mode LHsType GhcRn
orig_hs_ty Type
fun_ty Type
fun_ki [LHsTypeArg GhcRn]
args
       ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty' Type -> Coercion -> Type
`mkNakedCastTy` Type -> Coercion
mkNomReflCo Type
ki', Type
ki') }
          -- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]

tcTyApp :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind) -- only HsAppTy or HsAppKindTy
tcTyApp :: TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tcTyApp mode :: TcTyMode
mode e :: HsType GhcRn
e
  = do { let (hs_fun_ty :: LHsType GhcRn
hs_fun_ty, hs_args :: [LHsTypeArg GhcRn]
hs_args) = HsType GhcRn -> (LHsType GhcRn, [LHsTypeArg GhcRn])
splitHsAppTys HsType GhcRn
e
       ; (fun_ty :: Type
fun_ty, fun_kind :: Type
fun_kind) <- TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
hs_fun_ty
          -- NB: (IT4) of Note [The tcType invariant] ensures that fun_kind is zonked
       ; TcTyMode
-> LHsType GhcRn
-> Type
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
tcTyApps TcTyMode
mode LHsType GhcRn
hs_fun_ty Type
fun_ty Type
fun_kind [LHsTypeArg GhcRn]
hs_args }
--------------------------
-- Internally-callable version of checkExpectedKind
checkExpectedKindMode :: HasDebugCallStack
                      => TcTyMode
                      -> SDoc        -- type we're checking
                      -> TcType      -- type we're checking
                      -> TcKind      -- kind of that type
                      -> TcKind      -- expected kind
                      -> TcM TcType
checkExpectedKindMode :: TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode mode :: TcTyMode
mode = HasDebugCallStack =>
RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKind (TcTyMode -> RequireSaturation
mode_sat TcTyMode
mode)

-- | This instantiates invisible arguments for the type being checked if it must
-- be saturated and is not yet saturated. It then calls and uses the result
-- from checkExpectedKindX to build the final type
-- Obeys Note [The tcType invariant]
checkExpectedKind :: HasDebugCallStack
                  => RequireSaturation  -- ^ Do we require all type families to be saturated?
                  -> SDoc           -- ^ type we're checking (for printing)
                  -> TcType         -- ^ type we're checking
                  -> TcKind         -- ^ the known kind of that type
                  -> TcKind         -- ^ the expected kind
                  -> TcM TcType
checkExpectedKind :: RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKind sat :: RequireSaturation
sat hs_ty :: MsgDoc
hs_ty ty :: Type
ty act :: Type
act exp :: Type
exp
  = do { (new_ty :: Type
new_ty, new_act :: Type
new_act) <- case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
           Just (tc :: TyCon
tc, args :: [Type]
args)
             -- if the family tycon must be saturated and is not yet satured
             -- If we don't do this, we get #11246
             | RequireSaturation
YesSaturation <- RequireSaturation
sat
             , Bool -> Bool
not (TyCon -> Bool
mightBeUnsaturatedTyCon TyCon
tc) Bool -> Bool -> Bool
&& [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< TyCon -> Int
tyConArity TyCon
tc
             -> do {
                   -- we need to instantiate all invisible arguments up until saturation
                   (tc_args :: [Type]
tc_args, kind :: Type
kind) <- ([TyBinder], Type) -> TcM ([Type], Type)
HasDebugCallStack => ([TyBinder], Type) -> TcM ([Type], Type)
tcInstTyBinders (Int -> Type -> ([TyBinder], Type)
splitPiTysInvisibleN
                                                        (TyCon -> Int
tyConArity TyCon
tc Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args)
                                                        Type
act)
                   ; let tc_ty :: Type
tc_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ [Type]
args [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tc_args
                   ; String -> MsgDoc -> TcM ()
traceTc "checkExpectedKind:satTyFam" ([MsgDoc] -> MsgDoc
vcat [ TyCon -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyCon
tc MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act
                                                   , Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind ])
                   ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tc_ty, Type
kind) }
           _ -> (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Type
act)
       ; (new_args :: [Type]
new_args, co_k :: Coercion
co_k) <- HasDebugCallStack =>
MsgDoc -> Type -> Type -> TcM ([Type], Coercion)
MsgDoc -> Type -> Type -> TcM ([Type], Coercion)
checkExpectedKindX MsgDoc
hs_ty Type
new_act Type
exp
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
new_ty Type -> [Type] -> Type
`mkNakedAppTys` [Type]
new_args Type -> Coercion -> Type
`mkNakedCastTy` Coercion
co_k) }

checkExpectedKindX :: HasDebugCallStack
                   => SDoc                 -- HsType whose kind we're checking
                   -> TcKind               -- the known kind of that type, k
                   -> TcKind               -- the expected kind, exp_kind
                   -> TcM ([TcType], TcCoercionN)
    -- (the new args, the coercion)
-- Instantiate a kind (if necessary) and then call unifyType
--      (checkExpectedKind ty act_kind exp_kind)
-- checks that the actual kind act_kind is compatible
--      with the expected kind exp_kind
checkExpectedKindX :: MsgDoc -> Type -> Type -> TcM ([Type], Coercion)
checkExpectedKindX pp_hs_ty :: MsgDoc
pp_hs_ty act_kind :: Type
act_kind exp_kind :: Type
exp_kind
  = do { -- We need to make sure that both kinds have the same number of implicit
         -- foralls out front. If the actual kind has more, instantiate accordingly.
         -- Otherwise, just pass the type & kind through: the errors are caught
         -- in unifyType.
         let n_exp_invis_bndrs :: Int
n_exp_invis_bndrs = Type -> Int
invisibleTyBndrCount Type
exp_kind
             n_act_invis_bndrs :: Int
n_act_invis_bndrs = Type -> Int
invisibleTyBndrCount Type
act_kind
             n_to_inst :: Int
n_to_inst         = Int
n_act_invis_bndrs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n_exp_invis_bndrs
       ; (new_args :: [Type]
new_args, act_kind' :: Type
act_kind') <- ([TyBinder], Type) -> TcM ([Type], Type)
HasDebugCallStack => ([TyBinder], Type) -> TcM ([Type], Type)
tcInstTyBinders (Int -> Type -> ([TyBinder], Type)
splitPiTysInvisibleN Int
n_to_inst Type
act_kind)

       ; let origin :: CtOrigin
origin = TypeEqOrigin :: Type -> Type -> Maybe MsgDoc -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: Type
uo_actual   = Type
act_kind'
                                   , uo_expected :: Type
uo_expected = Type
exp_kind
                                   , uo_thing :: Maybe MsgDoc
uo_thing    = MsgDoc -> Maybe MsgDoc
forall a. a -> Maybe a
Just MsgDoc
pp_hs_ty
                                   , uo_visible :: Bool
uo_visible  = Bool
True } -- the hs_ty is visible

       ; String -> MsgDoc -> TcM ()
traceTc "checkExpectedKindX" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [MsgDoc] -> MsgDoc
vcat [ MsgDoc
pp_hs_ty
              , String -> MsgDoc
text "act_kind:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act_kind
              , String -> MsgDoc
text "act_kind':" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act_kind'
              , String -> MsgDoc
text "exp_kind:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind ]

       ; if Type
act_kind' HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
exp_kind
         then ([Type], Coercion) -> TcM ([Type], Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
new_args, Type -> Coercion
mkTcNomReflCo Type
exp_kind)  -- This is very common
         else do { Coercion
co_k <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
KindLevel CtOrigin
origin Type
act_kind' Type
exp_kind
                 ; String -> MsgDoc -> TcM ()
traceTc "checkExpectedKind" ([MsgDoc] -> MsgDoc
vcat [ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act_kind
                                                     , Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind
                                                     , Coercion -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Coercion
co_k ])
                      -- See Note [The tcType invariant]
                ; ([Type], Coercion) -> TcM ([Type], Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
new_args, Coercion
co_k) } }

---------------------------
tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [Type]
tcHsMbContext Nothing    = [Type] -> TcM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return []
tcHsMbContext (Just cxt :: LHsContext GhcRn
cxt) = LHsContext GhcRn -> TcM [Type]
tcHsContext LHsContext GhcRn
cxt

tcHsContext :: LHsContext GhcRn -> TcM [PredType]
tcHsContext :: LHsContext GhcRn -> TcM [Type]
tcHsContext = TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context TcTyMode
typeLevelMode

tcLHsPredType :: LHsType GhcRn -> TcM PredType
tcLHsPredType :: LHsType GhcRn -> TcM Type
tcLHsPredType = TcTyMode -> LHsType GhcRn -> TcM Type
tc_lhs_pred TcTyMode
typeLevelMode

tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context mode :: TcTyMode
mode ctxt :: LHsContext GhcRn
ctxt = (LHsType GhcRn -> TcM Type) -> [LHsType GhcRn] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TcTyMode -> LHsType GhcRn -> TcM Type
tc_lhs_pred TcTyMode
mode) (LHsContext GhcRn -> SrcSpanLess (LHsContext GhcRn)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsContext GhcRn
ctxt)

tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM Type
tc_lhs_pred mode :: TcTyMode
mode pred :: LHsType GhcRn
pred = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
pred Type
constraintKind

---------------------------
tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
tcTyVar :: TcTyMode -> Name -> TcM (Type, Type)
tcTyVar mode :: TcTyMode
mode name :: Name
name         -- Could be a tyvar, a tycon, or a datacon
  = do { String -> MsgDoc -> TcM ()
traceTc "lk1" (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name)
       ; TcTyThing
thing <- Name -> TcM TcTyThing
tcLookup Name
name
       ; case TcTyThing
thing of
           ATyVar _ tv :: TcTyVar
tv -> -- Important: zonk before returning
                          -- We may have the application ((a::kappa) b)
                          -- where kappa is already unified to (k1 -> k2)
                          -- Then we want to see that arrow.  Best done
                          -- here because we are also maintaining
                          -- Note [The tcType invariant], so we don't just
                          -- want to zonk the kind, leaving the TyVar
                          -- un-zonked  (Trac #14873)
                          do { Type
ty <- TcTyVar -> TcM Type
zonkTcTyVar TcTyVar
tv
                             ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
ty) }

           ATcTyCon tc_tc :: TyCon
tc_tc
             -> do { -- See Note [GADT kind self-reference]
                     Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeOrKind -> Bool
isTypeLevel (TcTyMode -> TypeOrKind
mode_level TcTyMode
mode))
                            (Name -> PromotionErr -> TcM ()
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
TyConPE)
                   ; TyCon -> TcM ()
check_tc TyCon
tc_tc
                   ; Type
tc_kind <- Type -> TcM Type
zonkTcType (TyCon -> Type
tyConKind TyCon
tc_tc)
                        -- (IT6) of Note [The tcType invariant]
                   ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type
mkTyConTy TyCon
tc_tc Type -> Coercion -> Type
`mkNakedCastTy` Type -> Coercion
mkNomReflCo Type
tc_kind, Type
tc_kind) }
                        -- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]

           AGlobal (ATyCon tc :: TyCon
tc)
             -> do { TyCon -> TcM ()
check_tc TyCon
tc
                   ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type
mkTyConTy TyCon
tc, TyCon -> Type
tyConKind TyCon
tc) }

           AGlobal (AConLike (RealDataCon dc :: DataCon
dc))
             -> do { Bool
data_kinds <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DataKinds
                   ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
data_kinds Bool -> Bool -> Bool
|| DataCon -> Bool
specialPromotedDc DataCon
dc) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
                       Name -> PromotionErr -> TcM ()
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
NoDataKindsDC
                   ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TyCon -> Bool
isFamInstTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc)) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
                       -- see Trac #15245
                       Name -> PromotionErr -> TcM ()
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
FamDataConPE
                   ; let (_, _, _, theta :: [Type]
theta, _, _) = DataCon -> ([TcTyVar], [TcTyVar], [EqSpec], [Type], [Type], Type)
dataConFullSig DataCon
dc
                   ; case [Type] -> Maybe Type
dc_theta_illegal_constraint [Type]
theta of
                       Just pred :: Type
pred -> Name -> PromotionErr -> TcM ()
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name (PromotionErr -> TcM ()) -> PromotionErr -> TcM ()
forall a b. (a -> b) -> a -> b
$
                                    Type -> PromotionErr
ConstrainedDataConPE Type
pred
                       Nothing   -> () -> TcM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                   ; let tc :: TyCon
tc = DataCon -> TyCon
promoteDataCon DataCon
dc
                   ; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [], TyCon -> Type
tyConKind TyCon
tc) }

           APromotionErr err :: PromotionErr
err -> Name -> PromotionErr -> TcM (Type, Type)
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
err

           _  -> String -> TcTyThing -> Name -> TcM (Type, Type)
forall a. String -> TcTyThing -> Name -> TcM a
wrongThingErr "type" TcTyThing
thing Name
name }
  where
    check_tc :: TyCon -> TcM ()
    check_tc :: TyCon -> TcM ()
check_tc tc :: TyCon
tc = do { Bool
data_kinds   <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DataKinds
                     ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeOrKind -> Bool
isTypeLevel (TcTyMode -> TypeOrKind
mode_level TcTyMode
mode) Bool -> Bool -> Bool
||
                               Bool
data_kinds Bool -> Bool -> Bool
||
                               TyCon -> Bool
isKindTyCon TyCon
tc) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
                       Name -> PromotionErr -> TcM ()
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
NoDataKindsTC }

    -- We cannot promote a data constructor with a context that contains
    -- constraints other than equalities, so error if we find one.
    -- See Note [Constraints handled in types] in Inst.
    dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
    dc_theta_illegal_constraint :: [Type] -> Maybe Type
dc_theta_illegal_constraint = (Type -> Bool) -> [Type] -> Maybe Type
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Type -> Bool
go
      where
        go :: PredType -> Bool
        go :: Type -> Bool
go pred :: Type
pred | Just tc :: TyCon
tc <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
pred
                = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$  TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
                      Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
                | Bool
otherwise = Bool
True

{-
Note [GADT kind self-reference]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

A promoted type cannot be used in the body of that type's declaration.
Trac #11554 shows this example, which made GHC loop:

  import Data.Kind
  data P (x :: k) = Q
  data A :: Type where
    B :: forall (a :: A). P a -> A

In order to check the constructor B, we need to have the promoted type A, but in
order to get that promoted type, B must first be checked. To prevent looping, a
TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
Any ATcTyCon is a TyCon being defined in the current recursive group (see data
type decl for TcTyThing), and all such TyCons are illegal in kinds.

Trac #11962 proposes checking the head of a data declaration separately from
its constructors. This would allow the example above to pass.

Note [Body kind of a HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The body of a forall is usually a type, but in principle
there's no reason to prohibit *unlifted* types.
In fact, GHC can itself construct a function with an
unboxed tuple inside a for-all (via CPR analysis; see
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
kind Constraint.

It's tempting to check that the body kind is either * or #. But this is
wrong. For example:

  class C a b
  newtype N = Mk Foo deriving (C a)

We're doing newtype-deriving for C. But notice how `a` isn't in scope in
the predicate `C a`. So we quantify, yielding `forall a. C a` even though
`C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
convenient. Bottom line: don't check for * or # here.

Note [Body kind of a HsQualTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If ctxt is non-empty, the HsQualTy really is a /function/, so the
kind of the result really is '*', and in that case the kind of the
body-type can be lifted or unlifted.

However, consider
    instance Eq a => Eq [a] where ...
or
    f :: (Eq a => Eq [a]) => blah
Here both body-kind of the HsQualTy is Constraint rather than *.
Rather crudely we tell the difference by looking at exp_kind. It's
very convenient to typecheck instance types like any other HsSigType.

Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
better to reject in checkValidType.  If we say that the body kind
should be '*' we risk getting TWO error messages, one saying that Eq
[a] doens't have kind '*', and one saying that we need a Constraint to
the left of the outer (=>).

How do we figure out the right body kind?  Well, it's a bit of a
kludge: I just look at the expected kind.  If it's Constraint, we
must be in this instance situation context. It's a kludge because it
wouldn't work if any unification was involved to compute that result
kind -- but it isn't.  (The true way might be to use the 'mode'
parameter, but that seemed like a sledgehammer to crack a nut.)

Note [Inferring tuple kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
we try to figure out whether it's a tuple of kind * or Constraint.
  Step 1: look at the expected kind
  Step 2: infer argument kinds

If after Step 2 it's not clear from the arguments that it's
Constraint, then it must be *.  Once having decided that we re-check
the Check the arguments again to give good error messages
in eg. `(Maybe, Maybe)`

Note that we will still fail to infer the correct kind in this case:

  type T a = ((a,a), D a)
  type family D :: Constraint -> Constraint

While kind checking T, we do not yet know the kind of D, so we will default the
kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.

Note [Desugaring types]
~~~~~~~~~~~~~~~~~~~~~~~
The type desugarer is phase 2 of dealing with HsTypes.  Specifically:

  * It transforms from HsType to Type

  * It zonks any kinds.  The returned type should have no mutable kind
    or type variables (hence returning Type not TcType):
      - any unconstrained kind variables are defaulted to (Any *) just
        as in TcHsSyn.
      - there are no mutable type variables because we are
        kind-checking a type
    Reason: the returned type may be put in a TyCon or DataCon where
    it will never subsequently be zonked.

You might worry about nested scopes:
        ..a:kappa in scope..
            let f :: forall b. T '[a,b] -> Int
In this case, f's type could have a mutable kind variable kappa in it;
and we might then default it to (Any *) when dealing with f's type
signature.  But we don't expect this to happen because we can't get a
lexically scoped type variable with a mutable kind variable in it.  A
delicate point, this.  If it becomes an issue we might need to
distinguish top-level from nested uses.

Moreover
  * it cannot fail,
  * it does no unifications
  * it does no validity checking, except for structural matters, such as
        (a) spurious ! annotations.
        (b) a class used as a type

Note [Kind of a type splice]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider these terms, each with TH type splice inside:
     [| e1 :: Maybe $(..blah..) |]
     [| e2 :: $(..blah..) |]
When kind-checking the type signature, we'll kind-check the splice
$(..blah..); we want to give it a kind that can fit in any context,
as if $(..blah..) :: forall k. k.

In the e1 example, the context of the splice fixes kappa to *.  But
in the e2 example, we'll desugar the type, zonking the kind unification
variables as we go.  When we encounter the unconstrained kappa, we
want to default it to '*', not to (Any *).

Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-}

addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
        -- Wrap a context around only if we want to show that contexts.
        -- Omit invisible ones and ones user's won't grok
addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt (L _ (HsWildCardTy _)) thing :: TcM a
thing = TcM a
thing   -- "In the type '_'" just isn't helpful.
addTypeCtxt (L _ ty :: HsType GhcRn
ty) thing :: TcM a
thing
  = MsgDoc -> TcM a -> TcM a
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt MsgDoc
doc TcM a
thing
  where
    doc :: MsgDoc
doc = String -> MsgDoc
text "In the type" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)

{-
************************************************************************
*                                                                      *
                Type-variable binders
%*                                                                      *
%************************************************************************

Note [Dependent LHsQTyVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We track (in the renamer) which explicitly bound variables in a
LHsQTyVars are manifestly dependent; only precisely these variables
may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars
can produce the right TyConBinders, and tell Anon vs. Required.

Example   data T k1 (a:k1) (b:k2) c
               = MkT (Proxy a) (Proxy b) (Proxy c)

Here
  (a:k1),(b:k2),(c:k3)
       are Anon     (explicitly specified as a binder, not used
                     in the kind of any other binder
  k1   is Required  (explicitly specifed as a binder, but used
                     in the kind of another binder i.e. dependently)
  k2   is Specified (not explicitly bound, but used in the kind
                     of another binder)
  k3   in Inferred  (not lexically in scope at all, but inferred
                     by kind inference)
and
  T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *

See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
in TyCoRep.

kcLHsQTyVars uses the hsq_dependent field to decide whether
k1, a, b, c should be Required or Anon.

Earlier, thought it would work simply to do a free-variable check
during kcLHsQTyVars, but this is bogus, because there may be
unsolved equalities about. And we don't want to eagerly solve the
equalities, because we may get further information after
kcLHsQTyVars is called.  (Recall that kcLHsQTyVars is called
only from getInitialKind.)
This is what implements the rule that all variables intended to be
dependent must be manifestly so.

Sidenote: It's quite possible that later, we'll consider (t -> s)
as a degenerate case of some (pi (x :: t) -> s) and then this will
all get more permissive.

Note [Keeping scoped variables in order: Explicit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the user writes `forall a b c. blah`, we bring a, b, and c into
scope and then check blah. In the process of checking blah, we might
learn the kinds of a, b, and c, and these kinds might indicate that
b depends on c, and thus that we should reject the user-written type.

One approach to doing this would be to bring each of a, b, and c into
scope, one at a time, creating an implication constraint and
bumping the TcLevel for each one. This would work, because the kind
of, say, b would be untouchable when c is in scope (and the constraint
couldn't float out because c blocks it). However, it leads to terrible
error messages, complaining about skolem escape. While it is indeed
a problem of skolem escape, we can do better.

Instead, our approach is to bring the block of variables into scope
all at once, creating one implication constraint for the lot. The
user-written variables are skolems in the implication constraint. In
TcSimplify.setImplicationStatus, we check to make sure that the ordering
is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
Then, in TcErrors, we report if there is a bad telescope. This way,
we can report a suggested ordering to the user if there is a problem.

Note [Keeping scoped variables in order: Implicit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the user implicitly quantifies over variables (say, in a type
signature), we need to come up with some ordering on these variables.
This is done by bumping the TcLevel, bringing the tyvars into scope,
and then type-checking the thing_inside. The constraints are all
wrapped in an implication, which is then solved. Finally, we can
zonk all the binders and then order them with scopedSort.

It's critical to solve before zonking and ordering in order to uncover
any unifications. You might worry that this eager solving could cause
trouble elsewhere. I don't think it will. Because it will solve only
in an increased TcLevel, it can't unify anything that was mentioned
elsewhere. Additionally, we require that the order of implicitly
quantified variables is manifest by the scope of these variables, so
we're not going to learn more information later that will help order
these variables.

Note [Recipe for checking a signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Checking a user-written signature requires several steps:

 1. Generate constraints.
 2. Solve constraints.
 3. Zonk.
 4. Promote tyvars and/or kind-generalize.
 5. Zonk.
 6. Check validity.

There may be some surprises in here:

Step 2 is necessary for two reasons: most signatures also bring
implicitly quantified variables into scope, and solving is necessary
to get these in the right order (see Note [Keeping scoped variables in
order: Implicit]). Additionally, solving is necessary in order to
kind-generalize correctly.

In Step 4, we have to deal with the fact that metatyvars generated
in the type may have a bumped TcLevel, because explicit foralls
raise the TcLevel. To avoid these variables from ever being visible
in the surrounding context, we must obey the following dictum:

  Every metavariable in a type must either be
    (A) promoted
    (B) generalized, or
    (C) zapped to Any

If a variable is generalized, then it becomes a skolem and no longer
has a proper TcLevel. (I'm ignoring the TcLevel on a skolem here, as
it's not really in play here.) On the other hand, if it is not
generalized (because we're not generalizing the construct -- e.g., pattern
sig -- or because the metavars are constrained -- see kindGeneralizeLocal)
we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables]
in TcType.

For more about (C), see Note [Naughty quantification candidates] in TcMType.

After promoting/generalizing, we need to zonk *again* because both
promoting and generalizing fill in metavariables.

To avoid the double-zonk, we do two things:
 1. When we're not generalizing:
    zonkPromoteType and friends zonk and promote at the same time.
    Accordingly, the function does steps 3-5 all at once, preventing
    the need for multiple traversals.

 2. When we are generalizing:
    kindGeneralize does not require a zonked type -- it zonks as it
    gathers free variables. So this way effectively sidesteps step 3.
-}

tcWildCardBinders :: [Name]
                  -> ([(Name, TcTyVar)] -> TcM a)
                  -> TcM a
tcWildCardBinders :: [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcWildCardBinders wc_names :: [Name]
wc_names thing_inside :: [(Name, TcTyVar)] -> TcM a
thing_inside
  = do { [TcTyVar]
wcs <- (Name -> TcM TcTyVar) -> [Name] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TcM TcTyVar -> Name -> TcM TcTyVar
forall a b. a -> b -> a
const TcM TcTyVar
newWildTyVar) [Name]
wc_names
       ; let wc_prs :: [(Name, TcTyVar)]
wc_prs = [Name]
wc_names [Name] -> [TcTyVar] -> [(Name, TcTyVar)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcTyVar]
wcs
       ; [(Name, TcTyVar)] -> TcM a -> TcM a
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
wc_prs (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         [(Name, TcTyVar)] -> TcM a
thing_inside [(Name, TcTyVar)]
wc_prs }

newWildTyVar :: TcM TcTyVar
-- ^ New unification variable for a wildcard
newWildTyVar :: TcM TcTyVar
newWildTyVar
  = do { Type
kind <- TcM Type
newMetaKindVar
       ; Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
newUnique
       ; TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
TauTv
       ; let name :: Name
name = Unique -> FastString -> Name
mkSysTvName Unique
uniq (String -> FastString
fsLit "_")
             tyvar :: TcTyVar
tyvar = (Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details)
       ; String -> MsgDoc -> TcM ()
traceTc "newWildTyVar" (TcTyVar -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyVar
tyvar)
       ; TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tyvar }

{- *********************************************************************
*                                                                      *
             Kind inference for type declarations
*                                                                      *
********************************************************************* -}

{- Note [The initial kind of a type constructor]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
kcLHsQTyVars is responsible for getting the initial kind of
a type constructor.

It has two cases:

 * The TyCon has a CUSK.  In that case, find the full, final,
   poly-kinded kind of the TyCon.  It's very like a term-level
   binding where we have a complete type signature for the
   function.

 * It does not have a CUSK.  Find a monomorphic kind, with
   unification variables in it; they will be generalised later.
   It's very like a term-level binding where we do not have
   a type signature (or, more accurately, where we have a
   partial type signature), so we infer the type and generalise.
-}


------------------------------
-- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
-- user-supplied kind signature (CUSK), generalise the result.
-- Used in 'getInitialKind' (for tycon kinds and other kinds)
-- and in kind-checking (but not for tycon kinds, which are checked with
-- tcTyClDecls). See Note [CUSKs: complete user-supplied kind signatures]
-- in HsDecls.
--
-- This function does not do telescope checking.
kcLHsQTyVars :: Name              -- ^ of the thing being checked
             -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
             -> Bool              -- ^ True <=> the decl being checked has a CUSK
             -> LHsQTyVars GhcRn
             -> TcM Kind          -- ^ The result kind
             -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
kcLHsQTyVars :: Name
-> TyConFlavour
-> Bool
-> LHsQTyVars GhcRn
-> TcM Type
-> TcRn TyCon
kcLHsQTyVars name :: Name
name flav :: TyConFlavour
flav cusk :: Bool
cusk tvs :: LHsQTyVars GhcRn
tvs thing_inside :: TcM Type
thing_inside
  | Bool
cusk      = Name -> TyConFlavour -> LHsQTyVars GhcRn -> TcM Type -> TcRn TyCon
kcLHsQTyVars_Cusk    Name
name TyConFlavour
flav LHsQTyVars GhcRn
tvs TcM Type
thing_inside
  | Bool
otherwise = Name -> TyConFlavour -> LHsQTyVars GhcRn -> TcM Type -> TcRn TyCon
kcLHsQTyVars_NonCusk Name
name TyConFlavour
flav LHsQTyVars GhcRn
tvs TcM Type
thing_inside


kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk
    :: Name              -- ^ of the thing being checked
    -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
    -> LHsQTyVars GhcRn
    -> TcM Kind          -- ^ The result kind
    -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon

------------------------------
kcLHsQTyVars_Cusk :: Name -> TyConFlavour -> LHsQTyVars GhcRn -> TcM Type -> TcRn TyCon
kcLHsQTyVars_Cusk name :: Name
name flav :: TyConFlavour
flav
  user_tyvars :: LHsQTyVars GhcRn
user_tyvars@(HsQTvs { hsq_ext :: forall pass. LHsQTyVars pass -> XHsQTvs pass
hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
                                           , hsq_dependent = dep_names }
                      , hsq_explicit :: forall pass. LHsQTyVars pass -> [LHsTyVarBndr pass]
hsq_explicit = [LHsTyVarBndr GhcRn]
hs_tvs }) thing_inside :: TcM Type
thing_inside
  -- CUSK case
  -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
  = Name -> TyConFlavour -> TcRn TyCon -> TcRn TyCon
forall a. Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt Name
name TyConFlavour
flav (TcRn TyCon -> TcRn TyCon) -> TcRn TyCon -> TcRn TyCon
forall a b. (a -> b) -> a -> b
$
    do { (scoped_kvs :: [TcTyVar]
scoped_kvs, (tc_tvs :: [TcTyVar]
tc_tvs, res_kind :: Type
res_kind))
           <- TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM ([TcTyVar], ([TcTyVar], Type))
forall a. TcM a -> TcM a
pushTcLevelM_                               (TcM ([TcTyVar], ([TcTyVar], Type))
 -> TcM ([TcTyVar], ([TcTyVar], Type)))
-> TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM ([TcTyVar], ([TcTyVar], Type))
forall a b. (a -> b) -> a -> b
$
              TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM ([TcTyVar], ([TcTyVar], Type))
forall a. TcM a -> TcM a
solveEqualities                             (TcM ([TcTyVar], ([TcTyVar], Type))
 -> TcM ([TcTyVar], ([TcTyVar], Type)))
-> TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM ([TcTyVar], ([TcTyVar], Type))
forall a b. (a -> b) -> a -> b
$
              [Name]
-> TcM ([TcTyVar], Type) -> TcM ([TcTyVar], ([TcTyVar], Type))
forall a. [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Q_Skol [Name]
kv_ns            (TcM ([TcTyVar], Type) -> TcM ([TcTyVar], ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type) -> TcM ([TcTyVar], ([TcTyVar], Type))
forall a b. (a -> b) -> a -> b
$
              ContextKind
-> [LHsTyVarBndr GhcRn] -> TcM Type -> TcM ([TcTyVar], Type)
forall a.
ContextKind -> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Q_Skol ContextKind
ctxt_kind [LHsTyVarBndr GhcRn]
hs_tvs (TcM Type -> TcM ([TcTyVar], Type))
-> TcM Type -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
              TcM Type
thing_inside

           -- Now, because we're in a CUSK,
           -- we quantify over the mentioned kind vars
       ; let spec_req_tkvs :: [TcTyVar]
spec_req_tkvs = [TcTyVar]
scoped_kvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tc_tvs
             all_kinds :: [Type]
all_kinds     = Type
res_kind Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (TcTyVar -> Type) -> [TcTyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> Type
tyVarKind [TcTyVar]
spec_req_tkvs

       ; CandidatesQTvs
candidates <- [Type] -> TcM CandidatesQTvs
candidateQTyVarsOfKinds [Type]
all_kinds
             -- 'candidates' are all the variables that we are going to
             -- skolemise and then quantify over.  We do not include spec_req_tvs
             -- because they are /already/ skolems

       ; let inf_candidates :: CandidatesQTvs
inf_candidates = CandidatesQTvs
candidates CandidatesQTvs -> [TcTyVar] -> CandidatesQTvs
`delCandidates` [TcTyVar]
spec_req_tkvs

       ; [TcTyVar]
inferred <- VarSet -> CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars VarSet
emptyVarSet CandidatesQTvs
inf_candidates
                     -- NB: 'inferred' comes back sorted in dependency order

       ; [TcTyVar]
scoped_kvs <- (TcTyVar -> TcM TcTyVar) -> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> TcM TcTyVar
zonkTyCoVarKind [TcTyVar]
scoped_kvs
       ; [TcTyVar]
tc_tvs     <- (TcTyVar -> TcM TcTyVar) -> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> TcM TcTyVar
zonkTyCoVarKind [TcTyVar]
tc_tvs
       ; Type
res_kind   <- Type -> TcM Type
zonkTcType           Type
res_kind

       ; let mentioned_kv_set :: VarSet
mentioned_kv_set = CandidatesQTvs -> VarSet
candidateKindVars CandidatesQTvs
candidates
             specified :: [TcTyVar]
specified        = [TcTyVar] -> [TcTyVar]
scopedSort [TcTyVar]
scoped_kvs
                                -- NB: maintain the L-R order of scoped_kvs

             final_tc_binders :: [TyConBinder]
final_tc_binders =  ArgFlag -> [TcTyVar] -> [TyConBinder]
mkNamedTyConBinders ArgFlag
Inferred  [TcTyVar]
inferred
                              [TyConBinder] -> [TyConBinder] -> [TyConBinder]
forall a. [a] -> [a] -> [a]
++ ArgFlag -> [TcTyVar] -> [TyConBinder]
mkNamedTyConBinders ArgFlag
Specified [TcTyVar]
specified
                              [TyConBinder] -> [TyConBinder] -> [TyConBinder]
forall a. [a] -> [a] -> [a]
++ (TcTyVar -> TyConBinder) -> [TcTyVar] -> [TyConBinder]
forall a b. (a -> b) -> [a] -> [b]
map (VarSet -> TcTyVar -> TyConBinder
mkRequiredTyConBinder VarSet
mentioned_kv_set) [TcTyVar]
tc_tvs

             all_tv_prs :: [(Name, TcTyVar)]
all_tv_prs = [TcTyVar] -> [(Name, TcTyVar)]
mkTyVarNamePairs ([TcTyVar]
scoped_kvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tc_tvs)
             tycon :: TyCon
tycon = Name
-> MsgDoc
-> [TyConBinder]
-> Type
-> [(Name, TcTyVar)]
-> Bool
-> TyConFlavour
-> TyCon
mkTcTyCon Name
name (LHsQTyVars GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsQTyVars GhcRn
user_tyvars)
                               [TyConBinder]
final_tc_binders
                               Type
res_kind
                               [(Name, TcTyVar)]
all_tv_prs
                               Bool
True {- it is generalised -} TyConFlavour
flav
         -- If the ordering from
         -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls
         -- doesn't work, we catch it here, before an error cascade
       ; TyCon -> TcM ()
checkValidTelescope TyCon
tycon

          -- If any of the specified tyvars aren't actually mentioned in a binder's
          -- kind (or the return kind), then we're in the CUSK case from
          -- Note [Free-floating kind vars]
       ; let unmentioned_kvs :: [TcTyVar]
unmentioned_kvs   = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
mentioned_kv_set) [TcTyVar]
specified
       ; Name -> TyConFlavour -> [TcTyVar] -> [TcTyVar] -> TcM ()
reportFloatingKvs Name
name TyConFlavour
flav ((TyConBinder -> TcTyVar) -> [TyConBinder] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map TyConBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar [TyConBinder]
final_tc_binders) [TcTyVar]
unmentioned_kvs


       ; String -> MsgDoc -> TcM ()
traceTc "kcLHsQTyVars: cusk" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [MsgDoc] -> MsgDoc
vcat [ String -> MsgDoc
text "name" MsgDoc -> MsgDoc -> MsgDoc
<+> Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name
              , String -> MsgDoc
text "kv_ns" MsgDoc -> MsgDoc -> MsgDoc
<+> [Name] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Name]
kv_ns
              , String -> MsgDoc
text "hs_tvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [LHsTyVarBndr GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsTyVarBndr GhcRn]
hs_tvs
              , String -> MsgDoc
text "dep_names" MsgDoc -> MsgDoc -> MsgDoc
<+> NameSet -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr NameSet
dep_names
              , String -> MsgDoc
text "scoped_kvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
scoped_kvs
              , String -> MsgDoc
text "tc_tvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
tc_tvs
              , String -> MsgDoc
text "res_kind" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_kind
              , String -> MsgDoc
text "candidates" MsgDoc -> MsgDoc -> MsgDoc
<+> CandidatesQTvs -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr CandidatesQTvs
candidates
              , String -> MsgDoc
text "inferred" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
inferred
              , String -> MsgDoc
text "specified" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
specified
              , String -> MsgDoc
text "final_tc_binders" MsgDoc -> MsgDoc -> MsgDoc
<+> [TyConBinder] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TyConBinder]
final_tc_binders
              , String -> MsgDoc
text "mkTyConKind final_tc_bndrs res_kind"
                MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr ([TyConBinder] -> Type -> Type
mkTyConKind [TyConBinder]
final_tc_binders Type
res_kind)
              , String -> MsgDoc
text "all_tv_prs" MsgDoc -> MsgDoc -> MsgDoc
<+> [(Name, TcTyVar)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [(Name, TcTyVar)]
all_tv_prs ]

       ; TyCon -> TcRn TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tycon }
  where
    ctxt_kind :: ContextKind
ctxt_kind | TyConFlavour -> Bool
tcFlavourIsOpen TyConFlavour
flav = Type -> ContextKind
TheKind Type
liftedTypeKind
              | Bool
otherwise            = ContextKind
AnyKind

kcLHsQTyVars_Cusk _ _ (XLHsQTyVars _) _ = String -> TcRn TyCon
forall a. String -> a
panic "kcLHsQTyVars"

------------------------------
kcLHsQTyVars_NonCusk :: Name -> TyConFlavour -> LHsQTyVars GhcRn -> TcM Type -> TcRn TyCon
kcLHsQTyVars_NonCusk name :: Name
name flav :: TyConFlavour
flav
  user_tyvars :: LHsQTyVars GhcRn
user_tyvars@(HsQTvs { hsq_ext :: forall pass. LHsQTyVars pass -> XHsQTvs pass
hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
                                           , hsq_dependent = dep_names }
                      , hsq_explicit :: forall pass. LHsQTyVars pass -> [LHsTyVarBndr pass]
hsq_explicit = [LHsTyVarBndr GhcRn]
hs_tvs }) thing_inside :: TcM Type
thing_inside
  -- Non_CUSK case
  -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
  = do { (scoped_kvs :: [TcTyVar]
scoped_kvs, (tc_tvs :: [TcTyVar]
tc_tvs, res_kind :: Type
res_kind))
           -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
           -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
           <- [Name]
-> TcM ([TcTyVar], Type) -> TcM ([TcTyVar], ([TcTyVar], Type))
forall a. [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Q_Tv [Name]
kv_ns            (TcM ([TcTyVar], Type) -> TcM ([TcTyVar], ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type) -> TcM ([TcTyVar], ([TcTyVar], Type))
forall a b. (a -> b) -> a -> b
$
              ContextKind
-> [LHsTyVarBndr GhcRn] -> TcM Type -> TcM ([TcTyVar], Type)
forall a.
ContextKind -> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Q_Tv ContextKind
ctxt_kind [LHsTyVarBndr GhcRn]
hs_tvs (TcM Type -> TcM ([TcTyVar], Type))
-> TcM Type -> TcM ([TcTyVar], Type)
forall a b. (a -> b) -> a -> b
$
              TcM Type
thing_inside
              -- Why "_Tv" not "_Skol"? See third wrinkle in
              -- Note [Inferring kinds for type declarations] in TcTyClsDecls,

       ; let   -- NB: Don't add scoped_kvs to tyConTyVars, because they
               -- might unify with kind vars in other types in a mutually
               -- recursive group.
               -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
             tc_binders :: [TyConBinder]
tc_binders = (LHsTyVarBndr GhcRn -> TcTyVar -> TyConBinder)
-> [LHsTyVarBndr GhcRn] -> [TcTyVar] -> [TyConBinder]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith LHsTyVarBndr GhcRn -> TcTyVar -> TyConBinder
mk_tc_binder [LHsTyVarBndr GhcRn]
hs_tvs [TcTyVar]
tc_tvs
               -- Also, note that tc_binders has the tyvars from only the
               -- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
               -- in TcTyClsDecls
             tycon :: TyCon
tycon = Name
-> MsgDoc
-> [TyConBinder]
-> Type
-> [(Name, TcTyVar)]
-> Bool
-> TyConFlavour
-> TyCon
mkTcTyCon Name
name (LHsQTyVars GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsQTyVars GhcRn
user_tyvars) [TyConBinder]
tc_binders Type
res_kind
                               ([TcTyVar] -> [(Name, TcTyVar)]
mkTyVarNamePairs ([TcTyVar]
scoped_kvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
tc_tvs))
                               Bool
False -- not yet generalised
                               TyConFlavour
flav

       ; String -> MsgDoc -> TcM ()
traceTc "kcLHsQTyVars: not-cusk" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [MsgDoc] -> MsgDoc
vcat [ Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name, [Name] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Name]
kv_ns, [LHsTyVarBndr GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsTyVarBndr GhcRn]
hs_tvs, NameSet -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr NameSet
dep_names
              , [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
scoped_kvs
              , [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
tc_tvs, Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr ([TyConBinder] -> Type -> Type
mkTyConKind [TyConBinder]
tc_binders Type
res_kind) ]
       ; TyCon -> TcRn TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tycon }
  where
    ctxt_kind :: ContextKind
ctxt_kind | TyConFlavour -> Bool
tcFlavourIsOpen TyConFlavour
flav = Type -> ContextKind
TheKind Type
liftedTypeKind
              | Bool
otherwise            = ContextKind
AnyKind

    mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
    -- See Note [Dependent LHsQTyVars]
    mk_tc_binder :: LHsTyVarBndr GhcRn -> TcTyVar -> TyConBinder
mk_tc_binder hs_tv :: LHsTyVarBndr GhcRn
hs_tv tv :: TcTyVar
tv
       | LHsTyVarBndr GhcRn -> IdP GhcRn
forall pass. LHsTyVarBndr pass -> IdP pass
hsLTyVarName LHsTyVarBndr GhcRn
hs_tv Name -> NameSet -> Bool
`elemNameSet` NameSet
dep_names
       = ArgFlag -> TcTyVar -> TyConBinder
mkNamedTyConBinder ArgFlag
Required TcTyVar
tv
       | Bool
otherwise
       = TcTyVar -> TyConBinder
mkAnonTyConBinder TcTyVar
tv

kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = String -> TcRn TyCon
forall a. String -> a
panic "kcLHsQTyVars"


{- Note [Kind-checking tyvar binders for associated types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind-checking the type-variable binders for associated
   data/newtype decls
   family decls
we behave specially for type variables that are already in scope;
that is, bound by the enclosing class decl.  This is done in
kcLHsQTyVarBndrs:
  * The use of tcImplicitQTKBndrs
  * The tcLookupLocal_maybe code in kc_hs_tv

See Note [Associated type tyvar names] in Class and
    Note [TyVar binders for associated decls] in HsDecls

We must do the same for family instance decls, where the in-scope
variables may be bound by the enclosing class instance decl.
Hence the use of tcImplicitQTKBndrs in tcFamTyPatsAndGen.

Note [Kind variable ordering for associated types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What should be the kind of `T` in the following example? (#15591)

  class C (a :: Type) where
    type T (x :: f a)

As per Note [Ordering of implicit variables] in RnTypes, we want to quantify
the kind variables in left-to-right order of first occurrence in order to
support visible kind application. But we cannot perform this analysis on just
T alone, since its variable `a` actually occurs /before/ `f` if you consider
the fact that `a` was previously bound by the parent class `C`. That is to say,
the kind of `T` should end up being:

  T :: forall a f. f a -> Type

(It wouldn't necessarily be /wrong/ if the kind ended up being, say,
forall f a. f a -> Type, but that would not be as predictable for users of
visible kind application.)

In contrast, if `T` were redefined to be a top-level type family, like `T2`
below:

  type family T2 (x :: f (a :: Type))

Then `a` first appears /after/ `f`, so the kind of `T2` should be:

  T2 :: forall f a. f a -> Type

In order to make this distinction, we need to know (in kcLHsQTyVars) which
type variables have been bound by the parent class (if there is one). With
the class-bound variables in hand, we can ensure that we always quantify
these first.
-}


{- *********************************************************************
*                                                                      *
             Expected kinds
*                                                                      *
********************************************************************* -}

-- | Describes the kind expected in a certain context.
data ContextKind = TheKind Kind   -- ^ a specific kind
                 | AnyKind        -- ^ any kind will do
                 | OpenKind       -- ^ something of the form @TYPE _@

-----------------------
newExpectedKind :: ContextKind -> TcM Kind
newExpectedKind :: ContextKind -> TcM Type
newExpectedKind (TheKind k :: Type
k) = Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
k
newExpectedKind AnyKind     = TcM Type
newMetaKindVar
newExpectedKind OpenKind    = TcM Type
newOpenTypeKind

-----------------------
expectedKindInCtxt :: UserTypeCtxt -> ContextKind
-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt :: UserTypeCtxt -> ContextKind
expectedKindInCtxt (TySynCtxt _)   = ContextKind
AnyKind
expectedKindInCtxt ThBrackCtxt     = ContextKind
AnyKind
expectedKindInCtxt (GhciCtxt {})   = ContextKind
AnyKind
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in TcEnv
expectedKindInCtxt DefaultDeclCtxt     = ContextKind
AnyKind
expectedKindInCtxt TypeAppCtxt         = ContextKind
AnyKind
expectedKindInCtxt (ForSigCtxt _)      = Type -> ContextKind
TheKind Type
liftedTypeKind
expectedKindInCtxt (InstDeclCtxt {})   = Type -> ContextKind
TheKind Type
constraintKind
expectedKindInCtxt SpecInstCtxt        = Type -> ContextKind
TheKind Type
constraintKind
expectedKindInCtxt _                   = ContextKind
OpenKind


{- *********************************************************************
*                                                                      *
             Bringing type variables into scope
*                                                                      *
********************************************************************* -}

--------------------------------------
-- Implicit binders
--------------------------------------

bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
  bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
  :: [Name]
  -> TcM a
  -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Skol :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Skol   = (Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX Name -> TcM TcTyVar
newFlexiKindedSkolemTyVar
bindImplicitTKBndrs_Tv :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Tv     = (Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX Name -> TcM TcTyVar
newFlexiKindedTyVarTyVar
bindImplicitTKBndrs_Q_Skol :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Q_Skol = (Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX ((Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
newImplicitTyVarQ Name -> TcM TcTyVar
newFlexiKindedSkolemTyVar)
bindImplicitTKBndrs_Q_Tv :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Q_Tv   = (Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX ((Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
newImplicitTyVarQ Name -> TcM TcTyVar
newFlexiKindedTyVarTyVar)

bindImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
                    -> [Name]
                    -> TcM a
                    -> TcM ([TcTyVar], a)   -- these tyvars are dependency-ordered
-- * Guarantees to call solveLocalEqualities to unify
--   all constraints from thing_inside.
--
-- * Returned TcTyVars have the supplied HsTyVarBndrs,
--   but may be in different order to the original [Name]
--   (because of sorting to respect dependency)
--
-- * Returned TcTyVars have zonked kinds
--   See Note [Keeping scoped variables in order: Implicit]
bindImplicitTKBndrsX :: (Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX new_tv :: Name -> TcM TcTyVar
new_tv tv_names :: [Name]
tv_names thing_inside :: TcM a
thing_inside
  = do { [TcTyVar]
tkvs <- (Name -> TcM TcTyVar) -> [Name] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> TcM TcTyVar
new_tv [Name]
tv_names
       ; a
result <- [TcTyVar] -> TcM a -> TcM a
forall r. [TcTyVar] -> TcM r -> TcM r
tcExtendTyVarEnv [TcTyVar]
tkvs TcM a
thing_inside
       ; String -> MsgDoc -> TcM ()
traceTc "bindImplicitTKBndrs" ([Name] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Name]
tv_names MsgDoc -> MsgDoc -> MsgDoc
$$ [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
tkvs)
       ; ([TcTyVar], a) -> TcM ([TcTyVar], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tkvs, a
result) }

newImplicitTyVarQ :: (Name -> TcM TcTyVar) ->  Name -> TcM TcTyVar
-- Behave like new_tv, except that if the tyvar is in scope, use it
newImplicitTyVarQ :: (Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
newImplicitTyVarQ new_tv :: Name -> TcM TcTyVar
new_tv name :: Name
name
  = do { Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe Name
name
       ; case Maybe TcTyThing
mb_tv of
           Just (ATyVar _ tv :: TcTyVar
tv) -> TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv
           _ -> Name -> TcM TcTyVar
new_tv Name
name }

newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
newFlexiKindedTyVar :: (Name -> Type -> TcM TcTyVar) -> Name -> TcM TcTyVar
newFlexiKindedTyVar new_tv :: Name -> Type -> TcM TcTyVar
new_tv name :: Name
name
  = do { Type
kind <- TcM Type
newMetaKindVar
       ; Name -> Type -> TcM TcTyVar
new_tv Name
name Type
kind }

newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
newFlexiKindedSkolemTyVar :: Name -> TcM TcTyVar
newFlexiKindedSkolemTyVar = (Name -> Type -> TcM TcTyVar) -> Name -> TcM TcTyVar
newFlexiKindedTyVar Name -> Type -> TcM TcTyVar
newSkolemTyVar

newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
newFlexiKindedTyVarTyVar :: Name -> TcM TcTyVar
newFlexiKindedTyVarTyVar = (Name -> Type -> TcM TcTyVar) -> Name -> TcM TcTyVar
newFlexiKindedTyVar Name -> Type -> TcM TcTyVar
newTyVarTyVar

--------------------------------------
-- Explicit binders
--------------------------------------

bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
    :: [LHsTyVarBndr GhcRn]
    -> TcM a
    -> TcM ([TcTyVar], a)

bindExplicitTKBndrs_Skol :: [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Skol = (HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX ((Name -> Type -> TcM TcTyVar) -> HsTyVarBndr GhcRn -> TcM TcTyVar
tcHsTyVarBndr Name -> Type -> TcM TcTyVar
newSkolemTyVar)
bindExplicitTKBndrs_Tv :: [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Tv   = (HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX ((Name -> Type -> TcM TcTyVar) -> HsTyVarBndr GhcRn -> TcM TcTyVar
tcHsTyVarBndr Name -> Type -> TcM TcTyVar
newTyVarTyVar)

bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
    :: ContextKind
    -> [LHsTyVarBndr GhcRn]
    -> TcM a
    -> TcM ([TcTyVar], a)

bindExplicitTKBndrs_Q_Skol :: ContextKind -> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Q_Skol ctxt_kind :: ContextKind
ctxt_kind = (HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX (ContextKind
-> (Name -> Type -> TcM TcTyVar)
-> HsTyVarBndr GhcRn
-> TcM TcTyVar
tcHsQTyVarBndr ContextKind
ctxt_kind Name -> Type -> TcM TcTyVar
newSkolemTyVar)
bindExplicitTKBndrs_Q_Tv :: ContextKind -> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Q_Tv   ctxt_kind :: ContextKind
ctxt_kind = (HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX (ContextKind
-> (Name -> Type -> TcM TcTyVar)
-> HsTyVarBndr GhcRn
-> TcM TcTyVar
tcHsQTyVarBndr ContextKind
ctxt_kind Name -> Type -> TcM TcTyVar
newTyVarTyVar)

-- | Used during the "kind-checking" pass in TcTyClsDecls only,
-- and even then only for data-con declarations.
bindExplicitTKBndrsX
    :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
    -> [LHsTyVarBndr GhcRn]
    -> TcM a
    -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX tc_tv :: HsTyVarBndr GhcRn -> TcM TcTyVar
tc_tv hs_tvs :: [LHsTyVarBndr GhcRn]
hs_tvs thing_inside :: TcM a
thing_inside
  = do { String -> MsgDoc -> TcM ()
traceTc "bindExplicTKBndrs" ([LHsTyVarBndr GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsTyVarBndr GhcRn]
hs_tvs)
       ; [LHsTyVarBndr GhcRn] -> TcM ([TcTyVar], a)
go [LHsTyVarBndr GhcRn]
hs_tvs }
  where
    go :: [LHsTyVarBndr GhcRn] -> TcM ([TcTyVar], a)
go [] = do { a
res <- TcM a
thing_inside
               ; ([TcTyVar], a) -> TcM ([TcTyVar], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], a
res) }
    go (L _ hs_tv :: HsTyVarBndr GhcRn
hs_tv : hs_tvs :: [LHsTyVarBndr GhcRn]
hs_tvs)
       = do { TcTyVar
tv <- HsTyVarBndr GhcRn -> TcM TcTyVar
tc_tv HsTyVarBndr GhcRn
hs_tv
            ; (tvs :: [TcTyVar]
tvs, res :: a
res) <- [TcTyVar] -> TcM ([TcTyVar], a) -> TcM ([TcTyVar], a)
forall r. [TcTyVar] -> TcM r -> TcM r
tcExtendTyVarEnv [TcTyVar
tv] ([LHsTyVarBndr GhcRn] -> TcM ([TcTyVar], a)
go [LHsTyVarBndr GhcRn]
hs_tvs)
            ; ([TcTyVar], a) -> TcM ([TcTyVar], a)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar
tvTcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
:[TcTyVar]
tvs, a
res) }

-----------------
tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
              -> HsTyVarBndr GhcRn -> TcM TcTyVar
-- Returned TcTyVar has the same name; no cloning
tcHsTyVarBndr :: (Name -> Type -> TcM TcTyVar) -> HsTyVarBndr GhcRn -> TcM TcTyVar
tcHsTyVarBndr new_tv :: Name -> Type -> TcM TcTyVar
new_tv (UserTyVar _ (L _ tv_nm :: IdP GhcRn
tv_nm))
  = do { Type
kind <- TcM Type
newMetaKindVar
       ; Name -> Type -> TcM TcTyVar
new_tv Name
IdP GhcRn
tv_nm Type
kind }
tcHsTyVarBndr new_tv :: Name -> Type -> TcM TcTyVar
new_tv (KindedTyVar _ (L _ tv_nm :: IdP GhcRn
tv_nm) lhs_kind :: LHsType GhcRn
lhs_kind)
  = do { Type
kind <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig (Name -> UserTypeCtxt
TyVarBndrKindCtxt Name
IdP GhcRn
tv_nm) LHsType GhcRn
lhs_kind
       ; Name -> Type -> TcM TcTyVar
new_tv Name
IdP GhcRn
tv_nm Type
kind }
tcHsTyVarBndr _ (XTyVarBndr _) = String -> TcM TcTyVar
forall a. String -> a
panic "tcHsTyVarBndr"

-----------------
tcHsQTyVarBndr :: ContextKind
               -> (Name -> Kind -> TcM TyVar)
               -> HsTyVarBndr GhcRn -> TcM TcTyVar
-- Just like tcHsTyVarBndr, but also
--   - uses the in-scope TyVar from class, if it exists
--   - takes a ContextKind to use for the no-sig case
tcHsQTyVarBndr :: ContextKind
-> (Name -> Type -> TcM TcTyVar)
-> HsTyVarBndr GhcRn
-> TcM TcTyVar
tcHsQTyVarBndr ctxt_kind :: ContextKind
ctxt_kind new_tv :: Name -> Type -> TcM TcTyVar
new_tv (UserTyVar _ (L _ tv_nm :: IdP GhcRn
tv_nm))
  = do { Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe Name
IdP GhcRn
tv_nm
       ; case Maybe TcTyThing
mb_tv of
           Just (ATyVar _ tv :: TcTyVar
tv) -> TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv
           _ -> do { Type
kind <- ContextKind -> TcM Type
newExpectedKind ContextKind
ctxt_kind
                   ; Name -> Type -> TcM TcTyVar
new_tv Name
IdP GhcRn
tv_nm Type
kind } }

tcHsQTyVarBndr _ new_tv :: Name -> Type -> TcM TcTyVar
new_tv (KindedTyVar _ (L _ tv_nm :: IdP GhcRn
tv_nm) lhs_kind :: LHsType GhcRn
lhs_kind)
  = do { Type
kind <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig (Name -> UserTypeCtxt
TyVarBndrKindCtxt Name
IdP GhcRn
tv_nm) LHsType GhcRn
lhs_kind
       ; Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe Name
IdP GhcRn
tv_nm
       ; case Maybe TcTyThing
mb_tv of
           Just (ATyVar _ tv :: TcTyVar
tv)
             -> do { TcM Coercion -> TcM ()
forall a. TcM a -> TcM ()
discardResult (TcM Coercion -> TcM ()) -> TcM Coercion -> TcM ()
forall a b. (a -> b) -> a -> b
$ Maybe (HsType GhcRn) -> Type -> Type -> TcM Coercion
unifyKind (HsType GhcRn -> Maybe (HsType GhcRn)
forall a. a -> Maybe a
Just HsType GhcRn
hs_tv)
                                        Type
kind (TcTyVar -> Type
tyVarKind TcTyVar
tv)
                       -- This unify rejects:
                       --    class C (m :: * -> *) where
                       --      type F (m :: *) = ...
                   ; TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv }

           _ -> Name -> Type -> TcM TcTyVar
new_tv Name
IdP GhcRn
tv_nm Type
kind }
  where
    hs_tv :: HsType GhcRn
hs_tv = XTyVar GhcRn
-> PromotionFlag -> GenLocated SrcSpan (IdP GhcRn) -> HsType GhcRn
forall pass.
XTyVar pass -> PromotionFlag -> Located (IdP pass) -> HsType pass
HsTyVar XTyVar GhcRn
NoExt
noExt PromotionFlag
NotPromoted (SrcSpanLess (Located Name) -> Located Name
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc SrcSpanLess (Located Name)
IdP GhcRn
tv_nm)
            -- Used for error messages only

tcHsQTyVarBndr _ _ (XTyVarBndr _) = String -> TcM TcTyVar
forall a. String -> a
panic "tcHsTyVarBndr"


--------------------------------------
-- Binding type/class variables in the
-- kind-checking and typechecking phases
--------------------------------------

bindTyClTyVars :: Name
               -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
-- ^ Used for the type variables of a type or class decl
-- in the "kind checking" and "type checking" pass,
-- but not in the initial-kind run.
bindTyClTyVars :: Name -> ([TyConBinder] -> Type -> TcM a) -> TcM a
bindTyClTyVars tycon_name :: Name
tycon_name thing_inside :: [TyConBinder] -> Type -> TcM a
thing_inside
  = do { TyCon
tycon <- Name -> TcRn TyCon
kcLookupTcTyCon Name
tycon_name
       ; let scoped_prs :: [(Name, TcTyVar)]
scoped_prs = TyCon -> [(Name, TcTyVar)]
tcTyConScopedTyVars TyCon
tycon
             res_kind :: Type
res_kind   = TyCon -> Type
tyConResKind TyCon
tycon
             binders :: [TyConBinder]
binders    = TyCon -> [TyConBinder]
tyConBinders TyCon
tycon
       ; String -> MsgDoc -> TcM ()
traceTc "bindTyClTyVars" (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
tycon_name MsgDoc -> MsgDoc -> MsgDoc
<+> [TyConBinder] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TyConBinder]
binders)
       ; [(Name, TcTyVar)] -> TcM a -> TcM a
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
scoped_prs (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         [TyConBinder] -> Type -> TcM a
thing_inside [TyConBinder]
binders Type
res_kind }

-- getInitialKind has made a suitably-shaped kind for the type or class
-- Look it up in the local environment. This is used only for tycons
-- that we're currently type-checking, so we're sure to find a TcTyCon.
kcLookupTcTyCon :: Name -> TcM TcTyCon
kcLookupTcTyCon :: Name -> TcRn TyCon
kcLookupTcTyCon nm :: Name
nm
  = do { TcTyThing
tc_ty_thing <- Name -> TcM TcTyThing
tcLookup Name
nm
       ; TyCon -> TcRn TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> TcRn TyCon) -> TyCon -> TcRn TyCon
forall a b. (a -> b) -> a -> b
$ case TcTyThing
tc_ty_thing of
           ATcTyCon tc :: TyCon
tc -> TyCon
tc
           _           -> String -> MsgDoc -> TyCon
forall a. HasCallStack => String -> MsgDoc -> a
pprPanic "kcLookupTcTyCon" (TcTyThing -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyThing
tc_ty_thing) }


{- *********************************************************************
*                                                                      *
             Kind generalisation
*                                                                      *
********************************************************************* -}

zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort spec_tkvs :: [TcTyVar]
spec_tkvs
  = do { [TcTyVar]
spec_tkvs <- (TcTyVar -> TcM TcTyVar) -> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> TcM TcTyVar
zonkTcTyCoVarBndr [TcTyVar]
spec_tkvs
          -- Use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv

       -- Do a stable topological sort, following
       -- Note [Ordering of implicit variables] in RnTypes
       ; [TcTyVar] -> TcM [TcTyVar]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar] -> [TcTyVar]
scopedSort [TcTyVar]
spec_tkvs) }

kindGeneralize :: TcType -> TcM [KindVar]
-- Quantify the free kind variables of a kind or type
-- In the latter case the type is closed, so it has no free
-- type variables.  So in both cases, all the free vars are kind vars
-- Input needn't be zonked. All variables to be quantified must
-- have a TcLevel higher than the ambient TcLevel.
-- NB: You must call solveEqualities or solveLocalEqualities before
-- kind generalization
--
-- NB: this function is just a specialised version of
--        kindGeneralizeLocal emptyWC kind_or_type
--
kindGeneralize :: Type -> TcM [TcTyVar]
kindGeneralize kind_or_type :: Type
kind_or_type
  = do { Type
kt <- Type -> TcM Type
zonkTcType Type
kind_or_type
       ; String -> MsgDoc -> TcM ()
traceTc "kindGeneralise1" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kt)
       ; CandidatesQTvs
dvs <- Type -> TcM CandidatesQTvs
candidateQTyVarsOfKind Type
kind_or_type
       ; VarSet
gbl_tvs <- TcM VarSet
tcGetGlobalTyCoVars -- Already zonked
       ; String -> MsgDoc -> TcM ()
traceTc "kindGeneralize" ([MsgDoc] -> MsgDoc
vcat [ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind_or_type
                                        , CandidatesQTvs -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr CandidatesQTvs
dvs ])
       ; VarSet -> CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars VarSet
gbl_tvs CandidatesQTvs
dvs }

-- | This variant of 'kindGeneralize' refuses to generalize over any
-- variables free in the given WantedConstraints. Instead, it promotes
-- these variables into an outer TcLevel. All variables to be quantified must
-- have a TcLevel higher than the ambient TcLevel. See also
-- Note [Promoting unification variables] in TcSimplify
kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
kindGeneralizeLocal :: WantedConstraints -> Type -> TcM [TcTyVar]
kindGeneralizeLocal wanted :: WantedConstraints
wanted kind_or_type :: Type
kind_or_type
  = do {
       -- This bit is very much like decideMonoTyVars in TcSimplify,
       -- but constraints are so much simpler in kinds, it is much
       -- easier here. (In particular, we never quantify over a
       -- constraint in a type.)
       ; VarSet
constrained <- VarSet -> TcM VarSet
zonkTyCoVarsAndFV (WantedConstraints -> VarSet
tyCoVarsOfWC WantedConstraints
wanted)
       ; (_, constrained :: VarSet
constrained) <- VarSet -> TcM (Bool, VarSet)
promoteTyVarSet VarSet
constrained

       ; VarSet
gbl_tvs <- TcM VarSet
tcGetGlobalTyCoVars -- Already zonked
       ; let mono_tvs :: VarSet
mono_tvs = VarSet
gbl_tvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
constrained

         -- use the "Kind" variant here, as any types we see
         -- here will already have all type variables quantified;
         -- thus, every free variable is really a kv, never a tv.
       ; CandidatesQTvs
dvs <- Type -> TcM CandidatesQTvs
candidateQTyVarsOfKind Type
kind_or_type

       ; String -> MsgDoc -> TcM ()
traceTc "kindGeneralizeLocal" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [MsgDoc] -> MsgDoc
vcat [ String -> MsgDoc
text "Wanted:" MsgDoc -> MsgDoc -> MsgDoc
<+> WantedConstraints -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr WantedConstraints
wanted
              , String -> MsgDoc
text "Kind or type:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind_or_type
              , String -> MsgDoc
text "tcvs of wanted:" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
pprTyVars (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet (WantedConstraints -> VarSet
tyCoVarsOfWC WantedConstraints
wanted))
              , String -> MsgDoc
text "constrained:" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
pprTyVars (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet VarSet
constrained)
              , String -> MsgDoc
text "mono_tvs:" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
pprTyVars (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet VarSet
mono_tvs)
              , String -> MsgDoc
text "dvs:" MsgDoc -> MsgDoc -> MsgDoc
<+> CandidatesQTvs -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr CandidatesQTvs
dvs ]

       ; VarSet -> CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars VarSet
mono_tvs CandidatesQTvs
dvs }

{- Note [Levels and generalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  f x = e
with no type signature. We are currently at level i.
We must
  * Push the level to level (i+1)
  * Allocate a fresh alpha[i+1] for the result type
  * Check that e :: alpha[i+1], gathering constraint WC
  * Solve WC as far as possible
  * Zonking the result type alpha[i+1], say to beta[i-1] -> gamma[i]
  * Find the free variables with level > i, in this case gamma[i]
  * Skolemise those free variables and quantify over them, giving
       f :: forall g. beta[i-1] -> g
  * Emit the residiual constraint wrapped in an implication for g,
    thus   forall g. WC

All of this happens for types too.  Consider
  f :: Int -> (forall a. Proxy a -> Int)

Note [Kind generalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~
We do kind generalisation only at the outer level of a type signature.
For example, consider
  T :: forall k. k -> *
  f :: (forall a. T a -> Int) -> Int
When kind-checking f's type signature we generalise the kind at
the outermost level, thus:
  f1 :: forall k. (forall (a:k). T k a -> Int) -> Int  -- YES!
and *not* at the inner forall:
  f2 :: (forall k. forall (a:k). T k a -> Int) -> Int  -- NO!
Reason: same as for HM inference on value level declarations,
we want to infer the most general type.  The f2 type signature
would be *less applicable* than f1, because it requires a more
polymorphic argument.

NB: There are no explicit kind variables written in f's signature.
When there are, the renamer adds these kind variables to the list of
variables bound by the forall, so you can indeed have a type that's
higher-rank in its kind. But only by explicit request.

Note [Kinds of quantified type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcTyVarBndrsGen quantifies over a specified list of type variables,
*and* over the kind variables mentioned in the kinds of those tyvars.

Note that we must zonk those kinds (obviously) but less obviously, we
must return type variables whose kinds are zonked too. Example
    (a :: k7)  where  k7 := k9 -> k9
We must return
    [k9, a:k9->k9]
and NOT
    [k9, a:k7]
Reason: we're going to turn this into a for-all type,
   forall k9. forall (a:k7). blah
which the type checker will then instantiate, and instantiate does not
look through unification variables!

Hence using zonked_kinds when forming tvs'.

-}

-----------------------------------
etaExpandAlgTyCon :: [TyConBinder]
                  -> Kind
                  -> TcM ([TyConBinder], Kind)
-- GADT decls can have a (perhaps partial) kind signature
--      e.g.  data T a :: * -> * -> * where ...
-- This function makes up suitable (kinded) TyConBinders for the
-- argument kinds.  E.g. in this case it might return
--   ([b::*, c::*], *)
-- Never emits constraints.
-- It's a little trickier than you might think: see
-- Note [TyConBinders for the result kind signature of a data type]
etaExpandAlgTyCon :: [TyConBinder] -> Type -> TcM ([TyConBinder], Type)
etaExpandAlgTyCon tc_bndrs :: [TyConBinder]
tc_bndrs kind :: Type
kind
  = do  { SrcSpan
loc     <- TcRn SrcSpan
getSrcSpanM
        ; UniqSupply
uniqs   <- TcRnIf TcGblEnv TcLclEnv UniqSupply
forall gbl lcl. TcRnIf gbl lcl UniqSupply
newUniqueSupply
        ; LocalRdrEnv
rdr_env <- RnM LocalRdrEnv
getLocalRdrEnv
        ; let new_occs :: [OccName]
new_occs = [ OccName
occ
                         | String
str <- [String]
allNameStrings
                         , let occ :: OccName
occ = NameSpace -> String -> OccName
mkOccName NameSpace
tvName String
str
                         , Maybe Name -> Bool
forall a. Maybe a -> Bool
isNothing (LocalRdrEnv -> OccName -> Maybe Name
lookupLocalRdrOcc LocalRdrEnv
rdr_env OccName
occ)
                         -- Note [Avoid name clashes for associated data types]
                         , Bool -> Bool
not (OccName
occ OccName -> [OccName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [OccName]
lhs_occs) ]
              new_uniqs :: [Unique]
new_uniqs = UniqSupply -> [Unique]
uniqsFromSupply UniqSupply
uniqs
              subst :: TCvSubst
subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet ([TcTyVar] -> VarSet
mkVarSet [TcTyVar]
lhs_tvs))
        ; ([TyConBinder], Type) -> TcM ([TyConBinder], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpan
-> [OccName]
-> [Unique]
-> TCvSubst
-> [TyConBinder]
-> Type
-> ([TyConBinder], Type)
go SrcSpan
loc [OccName]
new_occs [Unique]
new_uniqs TCvSubst
subst [] Type
kind) }
  where
    lhs_tvs :: [TcTyVar]
lhs_tvs  = (TyConBinder -> TcTyVar) -> [TyConBinder] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map TyConBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar [TyConBinder]
tc_bndrs
    lhs_occs :: [OccName]
lhs_occs = (TcTyVar -> OccName) -> [TcTyVar] -> [OccName]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> OccName
forall a. NamedThing a => a -> OccName
getOccName [TcTyVar]
lhs_tvs

    go :: SrcSpan
-> [OccName]
-> [Unique]
-> TCvSubst
-> [TyConBinder]
-> Type
-> ([TyConBinder], Type)
go loc :: SrcSpan
loc occs :: [OccName]
occs uniqs :: [Unique]
uniqs subst :: TCvSubst
subst acc :: [TyConBinder]
acc kind :: Type
kind
      = case Type -> Maybe (TyBinder, Type)
splitPiTy_maybe Type
kind of
          Nothing -> ([TyConBinder] -> [TyConBinder]
forall a. [a] -> [a]
reverse [TyConBinder]
acc, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
kind)

          Just (Anon arg :: Type
arg, kind' :: Type
kind')
            -> SrcSpan
-> [OccName]
-> [Unique]
-> TCvSubst
-> [TyConBinder]
-> Type
-> ([TyConBinder], Type)
go SrcSpan
loc [OccName]
occs' [Unique]
uniqs' TCvSubst
subst' (TyConBinder
tcb TyConBinder -> [TyConBinder] -> [TyConBinder]
forall a. a -> [a] -> [a]
: [TyConBinder]
acc) Type
kind'
            where
              arg' :: Type
arg'   = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
arg
              tv :: TcTyVar
tv     = Name -> Type -> TcTyVar
mkTyVar (Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
uniq OccName
occ SrcSpan
loc) Type
arg'
              subst' :: TCvSubst
subst' = TCvSubst -> TcTyVar -> TCvSubst
extendTCvInScope TCvSubst
subst TcTyVar
tv
              tcb :: TyConBinder
tcb    = TcTyVar -> TyConBndrVis -> TyConBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TcTyVar
tv TyConBndrVis
AnonTCB
              (uniq :: Unique
uniq:uniqs' :: [Unique]
uniqs') = [Unique]
uniqs
              (occ :: OccName
occ:occs' :: [OccName]
occs')   = [OccName]
occs

          Just (Named (Bndr tv :: TcTyVar
tv vis :: ArgFlag
vis), kind' :: Type
kind')
            -> SrcSpan
-> [OccName]
-> [Unique]
-> TCvSubst
-> [TyConBinder]
-> Type
-> ([TyConBinder], Type)
go SrcSpan
loc [OccName]
occs [Unique]
uniqs TCvSubst
subst' (TyConBinder
tcb TyConBinder -> [TyConBinder] -> [TyConBinder]
forall a. a -> [a] -> [a]
: [TyConBinder]
acc) Type
kind'
            where
              (subst' :: TCvSubst
subst', tv' :: TcTyVar
tv') = HasCallStack => TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar)
TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar)
substTyVarBndr TCvSubst
subst TcTyVar
tv
              tcb :: TyConBinder
tcb = TcTyVar -> TyConBndrVis -> TyConBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TcTyVar
tv' (ArgFlag -> TyConBndrVis
NamedTCB ArgFlag
vis)

badKindSig :: Bool -> Kind -> SDoc
badKindSig :: Bool -> Type -> MsgDoc
badKindSig check_for_type :: Bool
check_for_type kind :: Type
kind
 = MsgDoc -> Int -> MsgDoc -> MsgDoc
hang ([MsgDoc] -> MsgDoc
sep [ String -> MsgDoc
text "Kind signature on data type declaration has non-*"
             , (if Bool
check_for_type then MsgDoc
empty else String -> MsgDoc
text "and non-variable") MsgDoc -> MsgDoc -> MsgDoc
<+>
               String -> MsgDoc
text "return kind" ])
        2 (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind)

tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
-- Result is in 1-1 correpondence with orig_args
tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
tcbVisibilities tc :: TyCon
tc orig_args :: [Type]
orig_args
  = Type -> TCvSubst -> [Type] -> [TyConBndrVis]
go (TyCon -> Type
tyConKind TyCon
tc) TCvSubst
init_subst [Type]
orig_args
  where
    init_subst :: TCvSubst
init_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes [Type]
orig_args))
    go :: Type -> TCvSubst -> [Type] -> [TyConBndrVis]
go _ _ []
      = []

    go fun_kind :: Type
fun_kind subst :: TCvSubst
subst all_args :: [Type]
all_args@(arg :: Type
arg : args :: [Type]
args)
      | Just (tcb :: TyBinder
tcb, inner_kind :: Type
inner_kind) <- Type -> Maybe (TyBinder, Type)
splitPiTy_maybe Type
fun_kind
      = case TyBinder
tcb of
          Anon _              -> TyConBndrVis
AnonTCB      TyConBndrVis -> [TyConBndrVis] -> [TyConBndrVis]
forall a. a -> [a] -> [a]
: Type -> TCvSubst -> [Type] -> [TyConBndrVis]
go Type
inner_kind TCvSubst
subst  [Type]
args
          Named (Bndr tv :: TcTyVar
tv vis :: ArgFlag
vis) -> ArgFlag -> TyConBndrVis
NamedTCB ArgFlag
vis TyConBndrVis -> [TyConBndrVis] -> [TyConBndrVis]
forall a. a -> [a] -> [a]
: Type -> TCvSubst -> [Type] -> [TyConBndrVis]
go Type
inner_kind TCvSubst
subst' [Type]
args
                 where
                    subst' :: TCvSubst
subst' = TCvSubst -> TcTyVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst TcTyVar
tv Type
arg

      | Bool -> Bool
not (TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst)
      = Type -> TCvSubst -> [Type] -> [TyConBndrVis]
go (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
fun_kind) TCvSubst
init_subst [Type]
all_args

      | Bool
otherwise
      = String -> MsgDoc -> [TyConBndrVis]
forall a. HasCallStack => String -> MsgDoc -> a
pprPanic "addTcbVisibilities" (TyCon -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyCon
tc MsgDoc -> MsgDoc -> MsgDoc
<+> [Type] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Type]
orig_args)


{- Note [TyConBinders for the result kind signature of a data type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given
  data T (a::*) :: * -> forall k. k -> *
we want to generate the extra TyConBinders for T, so we finally get
  (a::*) (b::*) (k::*) (c::k)
The function etaExpandAlgTyCon generates these extra TyConBinders from
the result kind signature.

We need to take care to give the TyConBinders
  (a) OccNames that are fresh (because the TyConBinders of a TyCon
      must have distinct OccNames

  (b) Uniques that are fresh (obviously)

For (a) we need to avoid clashes with the tyvars declared by
the user before the "::"; in the above example that is 'a'.
And also see Note [Avoid name clashes for associated data types].

For (b) suppose we have
   data T :: forall k. k -> forall k. k -> *
where the two k's are identical even up to their uniques.  Surprisingly,
this can happen: see Trac #14515.

It's reasonably easy to solve all this; just run down the list with a
substitution; hence the recursive 'go' function.  But it has to be
done.

Note [Avoid name clashes for associated data types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider    class C a b where
               data D b :: * -> *
When typechecking the decl for D, we'll invent an extra type variable
for D, to fill out its kind.  Ideally we don't want this type variable
to be 'a', because when pretty printing we'll get
            class C a b where
               data D b a0
(NB: the tidying happens in the conversion to IfaceSyn, which happens
as part of pretty-printing a TyThing.)

That's why we look in the LocalRdrEnv to see what's in scope. This is
important only to get nice-looking output when doing ":info C" in GHCi.
It isn't essential for correctness.


************************************************************************
*                                                                      *
             Partial signatures
*                                                                      *
************************************************************************

-}

tcHsPartialSigType
  :: UserTypeCtxt
  -> LHsSigWcType GhcRn       -- The type signature
  -> TcM ( [(Name, TcTyVar)]  -- Wildcards
         , Maybe TcType       -- Extra-constraints wildcard
         , [Name]             -- Original tyvar names, in correspondence with ...
         , [TcTyVar]          -- ... Implicitly and explicitly bound type variables
         , TcThetaType        -- Theta part
         , TcType )           -- Tau part
-- See Note [Recipe for checking a signature]
tcHsPartialSigType :: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
tcHsPartialSigType ctxt :: UserTypeCtxt
ctxt sig_ty :: LHsSigWcType GhcRn
sig_ty
  | HsWC { hswc_ext :: forall pass thing. HsWildCardBndrs pass thing -> XHsWC pass thing
hswc_ext  = XHsWC GhcRn (LHsSigType GhcRn)
sig_wcs,         hswc_body :: forall pass thing. HsWildCardBndrs pass thing -> thing
hswc_body = LHsSigType GhcRn
ib_ty } <- LHsSigWcType GhcRn
sig_ty
  , HsIB { hsib_ext :: forall pass thing. HsImplicitBndrs pass thing -> XHsIB pass thing
hsib_ext = XHsIB GhcRn (LHsType GhcRn)
implicit_hs_tvs
         , hsib_body :: forall pass thing. HsImplicitBndrs pass thing -> thing
hsib_body = LHsType GhcRn
hs_ty } <- LHsSigType GhcRn
ib_ty
  , (explicit_hs_tvs :: [LHsTyVarBndr GhcRn]
explicit_hs_tvs, L _ hs_ctxt :: [LHsType GhcRn]
hs_ctxt, hs_tau :: LHsType GhcRn
hs_tau) <- LHsType GhcRn
-> ([LHsTyVarBndr GhcRn], LHsContext GhcRn, LHsType GhcRn)
forall pass.
LHsType pass
-> ([LHsTyVarBndr pass], LHsContext pass, LHsType pass)
splitLHsSigmaTy LHsType GhcRn
hs_ty
  = UserTypeCtxt
-> LHsType GhcRn
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt UserTypeCtxt
ctxt LHsType GhcRn
hs_ty (TcM
   ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
 -> TcM
      ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type))
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall a b. (a -> b) -> a -> b
$
    do { (implicit_tvs :: [TcTyVar]
implicit_tvs, (explicit_tvs :: [TcTyVar]
explicit_tvs, (wcs :: [(Name, TcTyVar)]
wcs, wcx :: Maybe Type
wcx, theta :: [Type]
theta, tau :: Type
tau)))
            <- [Name]
-> ([(Name, TcTyVar)]
    -> TcM
         ([TcTyVar],
          ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
     ([TcTyVar],
      ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a. [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcWildCardBinders [Name]
XHsWC GhcRn (LHsSigType GhcRn)
sig_wcs (([(Name, TcTyVar)]
  -> TcM
       ([TcTyVar],
        ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))))
 -> TcM
      ([TcTyVar],
       ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> ([(Name, TcTyVar)]
    -> TcM
         ([TcTyVar],
          ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
     ([TcTyVar],
      ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a b. (a -> b) -> a -> b
$ \ wcs :: [(Name, TcTyVar)]
wcs ->
               [Name]
-> TcM ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))
-> TcM
     ([TcTyVar],
      ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a. [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Tv [Name]
XHsIB GhcRn (LHsType GhcRn)
implicit_hs_tvs       (TcM ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))
 -> TcM
      ([TcTyVar],
       ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))
-> TcM
     ([TcTyVar],
      ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a b. (a -> b) -> a -> b
$
               [LHsTyVarBndr GhcRn]
-> TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
-> TcM ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))
forall a. [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Tv [LHsTyVarBndr GhcRn]
explicit_hs_tvs       (TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
 -> TcM ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type)))
-> TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
-> TcM ([TcTyVar], ([(Name, TcTyVar)], Maybe Type, [Type], Type))
forall a b. (a -> b) -> a -> b
$
               do {   -- Instantiate the type-class context; but if there
                      -- is an extra-constraints wildcard, just discard it here
                    (theta :: [Type]
theta, wcx :: Maybe Type
wcx) <- [LHsType GhcRn] -> TcM ([Type], Maybe Type)
tcPartialContext [LHsType GhcRn]
hs_ctxt

                  ; Type
tau <- LHsType GhcRn -> TcM Type
tcHsOpenType LHsType GhcRn
hs_tau

                  ; ([(Name, TcTyVar)], Maybe Type, [Type], Type)
-> TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, TcTyVar)]
wcs, Maybe Type
wcx, [Type]
theta, Type
tau) }

         -- We must return these separately, because all the zonking below
         -- might change the name of a TyVarTv. This, in turn, causes trouble
         -- in partial type signatures that bind scoped type variables, as
         -- we bring the wrong name into scope in the function body.
         -- Test case: partial-sigs/should_compile/LocalDefinitionBug
       ; let tv_names :: [Name]
tv_names = (TcTyVar -> Name) -> [TcTyVar] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> Name
tyVarName ([TcTyVar]
implicit_tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
explicit_tvs)

       -- Spit out the wildcards (including the extra-constraints one)
       -- as "hole" constraints, so that they'll be reported if necessary
       -- See Note [Extra-constraint holes in partial type signatures]
       ; [(Name, TcTyVar)] -> TcM ()
emitWildCardHoleConstraints [(Name, TcTyVar)]
wcs

         -- The TyVarTvs created above will sometimes have too high a TcLevel
         -- (note that they are generated *after* bumping the level in
         -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
         -- is still important here, because the kinds of these variables
         -- do indeed need to have the higher level, so they can unify
         -- with other local type variables. But, now that we've type-checked
         -- everything (and solved equalities in the tcImplicit call)
         -- we need to promote the TyVarTvs so we don't violate the TcLevel
         -- invariant
       ; [TcTyVar]
implicit_tvs <- [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort [TcTyVar]
implicit_tvs
       ; [TcTyVar]
explicit_tvs <- (TcTyVar -> TcM TcTyVar) -> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> TcM TcTyVar
zonkTcTyCoVarBndr [TcTyVar]
explicit_tvs
       ; [Type]
theta        <- (Type -> TcM Type) -> [Type] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> TcM Type
zonkTcType [Type]
theta
       ; Type
tau          <- Type -> TcM Type
zonkTcType Type
tau

       ; let all_tvs :: [TcTyVar]
all_tvs = [TcTyVar]
implicit_tvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
explicit_tvs

       ; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt ([TcTyVar] -> Type -> Type
mkSpecForAllTys [TcTyVar]
all_tvs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type -> Type
mkPhiTy [Type]
theta Type
tau)

       ; String -> MsgDoc -> TcM ()
traceTc "tcHsPartialSigType" ([TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
all_tvs)
       ; ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, TcTyVar)]
wcs, Maybe Type
wcx, [Name]
tv_names, [TcTyVar]
all_tvs, [Type]
theta, Type
tau) }

tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs _)) = String
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall a. String -> a
panic "tcHsPartialSigType"
tcHsPartialSigType _ (XHsWildCardBndrs _) = String
-> TcM
     ([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall a. String -> a
panic "tcHsPartialSigType"

tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
tcPartialContext :: [LHsType GhcRn] -> TcM ([Type], Maybe Type)
tcPartialContext hs_theta :: [LHsType GhcRn]
hs_theta
  | Just (hs_theta1 :: [LHsType GhcRn]
hs_theta1, hs_ctxt_last :: LHsType GhcRn
hs_ctxt_last) <- [LHsType GhcRn] -> Maybe ([LHsType GhcRn], LHsType GhcRn)
forall a. [a] -> Maybe ([a], a)
snocView [LHsType GhcRn]
hs_theta
  , L _ wc :: HsType GhcRn
wc@(HsWildCardTy _) <- LHsType GhcRn -> LHsType GhcRn
forall pass. LHsType pass -> LHsType pass
ignoreParens LHsType GhcRn
hs_ctxt_last
  = do { Type
wc_tv_ty <- TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcWildCardOcc TcTyMode
typeLevelMode HsType GhcRn
wc Type
constraintKind
       ; [Type]
theta <- (LHsType GhcRn -> TcM Type) -> [LHsType GhcRn] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM LHsType GhcRn -> TcM Type
tcLHsPredType [LHsType GhcRn]
hs_theta1
       ; ([Type], Maybe Type) -> TcM ([Type], Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
theta, Type -> Maybe Type
forall a. a -> Maybe a
Just Type
wc_tv_ty) }
  | Bool
otherwise
  = do { [Type]
theta <- (LHsType GhcRn -> TcM Type) -> [LHsType GhcRn] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM LHsType GhcRn -> TcM Type
tcLHsPredType [LHsType GhcRn]
hs_theta
       ; ([Type], Maybe Type) -> TcM ([Type], Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
theta, Maybe Type
forall a. Maybe a
Nothing) }

{- Note [Extra-constraint holes in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  f :: (_) => a -> a
  f x = ...

* The renamer leaves '_' untouched.

* Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
  tcWildCardBinders.

* TcBinds.chooseInferredQuantifiers fills in that hole TcTyVar
  with the inferred constraints, e.g. (Eq a, Show a)

* TcErrors.mkHoleError finally reports the error.

An annoying difficulty happens if there are more than 62 inferred
constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
Where do we find the TyCon?  For good reasons we only have constraint
tuples up to 62 (see Note [How tuples work] in TysWiredIn).  So how
can we make a 70-tuple?  This was the root cause of Trac #14217.

It's incredibly tiresome, because we only need this type to fill
in the hole, to communicate to the error reporting machinery.  Nothing
more.  So I use a HACK:

* I make an /ordinary/ tuple of the constraints, in
  TcBinds.chooseInferredQuantifiers. This is ill-kinded because
  ordinary tuples can't contain constraints, but it works fine. And for
  ordinary tuples we don't have the same limit as for constraint
  tuples (which need selectors and an assocated class).

* Because it is ill-kinded, it trips an assert in writeMetaTyVar,
  so now I disable the assertion if we are writing a type of
  kind Constraint.  (That seldom/never normally happens so we aren't
  losing much.)

Result works fine, but it may eventually bite us.


************************************************************************
*                                                                      *
      Pattern signatures (i.e signatures that occur in patterns)
*                                                                      *
********************************************************************* -}

tcHsPatSigType :: UserTypeCtxt
               -> LHsSigWcType GhcRn          -- The type signature
               -> TcM ( [(Name, TcTyVar)]     -- Wildcards
                      , [(Name, TcTyVar)]     -- The new bit of type environment, binding
                                              -- the scoped type variables
                      , TcType)       -- The type
-- Used for type-checking type signatures in
-- (a) patterns           e.g  f (x::Int) = e
-- (b) RULE forall bndrs  e.g. forall (x::Int). f x = x
--
-- This may emit constraints
-- See Note [Recipe for checking a signature]
tcHsPatSigType :: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType ctxt :: UserTypeCtxt
ctxt sig_ty :: LHsSigWcType GhcRn
sig_ty
  | HsWC { hswc_ext :: forall pass thing. HsWildCardBndrs pass thing -> XHsWC pass thing
hswc_ext = XHsWC GhcRn (LHsSigType GhcRn)
sig_wcs,   hswc_body :: forall pass thing. HsWildCardBndrs pass thing -> thing
hswc_body = LHsSigType GhcRn
ib_ty } <- LHsSigWcType GhcRn
sig_ty
  , HsIB { hsib_ext :: forall pass thing. HsImplicitBndrs pass thing -> XHsIB pass thing
hsib_ext = XHsIB GhcRn (LHsType GhcRn)
sig_vars
         , hsib_body :: forall pass thing. HsImplicitBndrs pass thing -> thing
hsib_body = LHsType GhcRn
hs_ty } <- LHsSigType GhcRn
ib_ty
  = UserTypeCtxt
-> LHsType GhcRn
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt UserTypeCtxt
ctxt LHsType GhcRn
hs_ty (TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
 -> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall a b. (a -> b) -> a -> b
$
    do { [TcTyVar]
sig_tkvs <- (Name -> TcM TcTyVar) -> [Name] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> TcM TcTyVar
new_implicit_tv [Name]
XHsIB GhcRn (LHsType GhcRn)
sig_vars
       ; (wcs :: [(Name, TcTyVar)]
wcs, sig_ty :: Type
sig_ty)
            <- String
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a. String -> TcM a -> TcM a
solveLocalEqualities "tcHsPatSigType" (TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a b. (a -> b) -> a -> b
$
                 -- Always solve local equalities if possible,
                 -- else casts get in the way of deep skolemisation
                 -- (Trac #16033)
               [Name]
-> ([(Name, TcTyVar)] -> TcM ([(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], Type)
forall a. [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcWildCardBinders [Name]
XHsWC GhcRn (LHsSigType GhcRn)
sig_wcs  (([(Name, TcTyVar)] -> TcM ([(Name, TcTyVar)], Type))
 -> TcM ([(Name, TcTyVar)], Type))
-> ([(Name, TcTyVar)] -> TcM ([(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], Type)
forall a b. (a -> b) -> a -> b
$ \ wcs :: [(Name, TcTyVar)]
wcs ->
               [TcTyVar]
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall r. [TcTyVar] -> TcM r -> TcM r
tcExtendTyVarEnv [TcTyVar]
sig_tkvs                           (TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a b. (a -> b) -> a -> b
$
               do { Type
sig_ty <- LHsType GhcRn -> TcM Type
tcHsOpenType LHsType GhcRn
hs_ty
                  ; ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, TcTyVar)]
wcs, Type
sig_ty) }

        ; [(Name, TcTyVar)] -> TcM ()
emitWildCardHoleConstraints [(Name, TcTyVar)]
wcs

          -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
          -- contains a forall). Promote these.
          -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
          -- When we instantiate x, we have to compare the kind of the argument
          -- to a's kind, which will be a metavariable.
        ; Type
sig_ty <- Type -> TcM Type
zonkPromoteType Type
sig_ty
        ; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
sig_ty

        ; let tv_pairs :: [(Name, TcTyVar)]
tv_pairs = [TcTyVar] -> [(Name, TcTyVar)]
mkTyVarNamePairs [TcTyVar]
sig_tkvs

        ; String -> MsgDoc -> TcM ()
traceTc "tcHsPatSigType" ([Name] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Name]
XHsIB GhcRn (LHsType GhcRn)
sig_vars)
        ; ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, TcTyVar)]
wcs, [(Name, TcTyVar)]
tv_pairs, Type
sig_ty) }
  where
    new_implicit_tv :: Name -> TcM TcTyVar
new_implicit_tv name :: Name
name = do { Type
kind <- TcM Type
newMetaKindVar
                              ; Name -> Type -> TcM TcTyVar
new_tv Name
name Type
kind }

    new_tv :: Name -> Type -> TcM TcTyVar
new_tv = case UserTypeCtxt
ctxt of
               RuleSigCtxt {} -> Name -> Type -> TcM TcTyVar
newSkolemTyVar
               _              -> Name -> Type -> TcM TcTyVar
newTauTyVar
      -- See Note [Pattern signature binders]


tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = String -> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall a. String -> a
panic "tcHsPatSigType"
tcHsPatSigType _ (XHsWildCardBndrs _)          = String -> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall a. String -> a
panic "tcHsPatSigType"

tcPatSig :: Bool                    -- True <=> pattern binding
         -> LHsSigWcType GhcRn
         -> ExpSigmaType
         -> TcM (TcType,            -- The type to use for "inside" the signature
                 [(Name,TcTyVar)],  -- The new bit of type environment, binding
                                    -- the scoped type variables
                 [(Name,TcTyVar)],  -- The wildcards
                 HsWrapper)         -- Coercion due to unification with actual ty
                                    -- Of shape:  res_ty ~ sig_ty
tcPatSig :: Bool
-> LHsSigWcType GhcRn
-> ExpSigmaType
-> TcM (Type, [(Name, TcTyVar)], [(Name, TcTyVar)], HsWrapper)
tcPatSig in_pat_bind :: Bool
in_pat_bind sig :: LHsSigWcType GhcRn
sig res_ty :: ExpSigmaType
res_ty
 = do  { (sig_wcs :: [(Name, TcTyVar)]
sig_wcs, sig_tvs :: [(Name, TcTyVar)]
sig_tvs, sig_ty :: Type
sig_ty) <- UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType UserTypeCtxt
PatSigCtxt LHsSigWcType GhcRn
sig
        -- sig_tvs are the type variables free in 'sig',
        -- and not already in scope. These are the ones
        -- that should be brought into scope

        ; if [(Name, TcTyVar)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, TcTyVar)]
sig_tvs then do {
                -- Just do the subsumption check and return
                  HsWrapper
wrap <- (TidyEnv -> TcM (TidyEnv, MsgDoc))
-> TcM HsWrapper -> TcM HsWrapper
forall a. (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a
addErrCtxtM (Type -> TidyEnv -> TcM (TidyEnv, MsgDoc)
mk_msg Type
sig_ty) (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
                          CtOrigin -> UserTypeCtxt -> ExpSigmaType -> Type -> TcM HsWrapper
tcSubTypeET CtOrigin
PatSigOrigin UserTypeCtxt
PatSigCtxt ExpSigmaType
res_ty Type
sig_ty
                ; (Type, [(Name, TcTyVar)], [(Name, TcTyVar)], HsWrapper)
-> TcM (Type, [(Name, TcTyVar)], [(Name, TcTyVar)], HsWrapper)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
sig_ty, [], [(Name, TcTyVar)]
sig_wcs, HsWrapper
wrap)
        } else do
                -- Type signature binds at least one scoped type variable

                -- A pattern binding cannot bind scoped type variables
                -- It is more convenient to make the test here
                -- than in the renamer
        { Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
in_pat_bind (MsgDoc -> TcM ()
addErr ([(Name, TcTyVar)] -> MsgDoc
patBindSigErr [(Name, TcTyVar)]
sig_tvs))

                -- Check that all newly-in-scope tyvars are in fact
                -- constrained by the pattern.  This catches tiresome
                -- cases like
                --      type T a = Int
                --      f :: Int -> Int
                --      f (x :: T a) = ...
                -- Here 'a' doesn't get a binding.  Sigh
        ; let bad_tvs :: [TcTyVar]
bad_tvs = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut (TcTyVar -> VarSet -> Bool
`elemVarSet` Type -> VarSet
exactTyCoVarsOfType Type
sig_ty)
                                  (Type -> [TcTyVar]
tyCoVarsOfTypeList Type
sig_ty)
        ; Bool -> MsgDoc -> TcM ()
checkTc ([TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
bad_tvs) (Type -> [TcTyVar] -> MsgDoc
badPatTyVarTvs Type
sig_ty [TcTyVar]
bad_tvs)

        -- Now do a subsumption check of the pattern signature against res_ty
        ; HsWrapper
wrap <- (TidyEnv -> TcM (TidyEnv, MsgDoc))
-> TcM HsWrapper -> TcM HsWrapper
forall a. (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a
addErrCtxtM (Type -> TidyEnv -> TcM (TidyEnv, MsgDoc)
mk_msg Type
sig_ty) (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
                  CtOrigin -> UserTypeCtxt -> ExpSigmaType -> Type -> TcM HsWrapper
tcSubTypeET CtOrigin
PatSigOrigin UserTypeCtxt
PatSigCtxt ExpSigmaType
res_ty Type
sig_ty

        -- Phew!
        ; (Type, [(Name, TcTyVar)], [(Name, TcTyVar)], HsWrapper)
-> TcM (Type, [(Name, TcTyVar)], [(Name, TcTyVar)], HsWrapper)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
sig_ty, [(Name, TcTyVar)]
sig_tvs, [(Name, TcTyVar)]
sig_wcs, HsWrapper
wrap)
        } }
  where
    mk_msg :: Type -> TidyEnv -> TcM (TidyEnv, MsgDoc)
mk_msg sig_ty :: Type
sig_ty tidy_env :: TidyEnv
tidy_env
       = do { (tidy_env :: TidyEnv
tidy_env, sig_ty :: Type
sig_ty) <- TidyEnv -> Type -> TcM (TidyEnv, Type)
zonkTidyTcType TidyEnv
tidy_env Type
sig_ty
            ; Type
res_ty <- ExpSigmaType -> TcM Type
readExpType ExpSigmaType
res_ty   -- should be filled in by now
            ; (tidy_env :: TidyEnv
tidy_env, res_ty :: Type
res_ty) <- TidyEnv -> Type -> TcM (TidyEnv, Type)
zonkTidyTcType TidyEnv
tidy_env Type
res_ty
            ; let msg :: MsgDoc
msg = [MsgDoc] -> MsgDoc
vcat [ MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "When checking that the pattern signature:")
                                  4 (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
sig_ty)
                             , Int -> MsgDoc -> MsgDoc
nest 2 (MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "fits the type of its context:")
                                          2 (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_ty)) ]
            ; (TidyEnv, MsgDoc) -> TcM (TidyEnv, MsgDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, MsgDoc
msg) }

patBindSigErr :: [(Name,TcTyVar)] -> SDoc
patBindSigErr :: [(Name, TcTyVar)] -> MsgDoc
patBindSigErr sig_tvs :: [(Name, TcTyVar)]
sig_tvs
  = MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "You cannot bind scoped type variable" MsgDoc -> MsgDoc -> MsgDoc
<> [(Name, TcTyVar)] -> MsgDoc
forall a. [a] -> MsgDoc
plural [(Name, TcTyVar)]
sig_tvs
          MsgDoc -> MsgDoc -> MsgDoc
<+> [Name] -> MsgDoc
forall a. Outputable a => [a] -> MsgDoc
pprQuotedList (((Name, TcTyVar) -> Name) -> [(Name, TcTyVar)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TcTyVar) -> Name
forall a b. (a, b) -> a
fst [(Name, TcTyVar)]
sig_tvs))
       2 (String -> MsgDoc
text "in a pattern binding signature")

{- Note [Pattern signature binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See also Note [Type variables in the type environment] in TcRnTypes.
Consider

  data T where
    MkT :: forall a. a -> (a -> Int) -> T

  f :: T -> ...
  f (MkT x (f :: b -> c)) = <blah>

Here
 * The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk',
   It must be a skolem so that that it retains its identity, and
   TcErrors.getSkolemInfo can thereby find the binding site for the skolem.

 * The type signature pattern (f :: b -> c) makes freshs meta-tyvars
   beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the
   environment

 * Then unification makes beta := a_sk, gamma := Int
   That's why we must make beta and gamma a MetaTv,
   not a SkolemTv, so that it can unify to a_sk (or Int, respectively).

 * Finally, in '<blah>' we have the envt "b" :-> beta, "c" :-> gamma,
   so we return the pairs ("b" :-> beta, "c" :-> gamma) from tcHsPatSigType,

Another example (Trac #13881):
   fl :: forall (l :: [a]). Sing l -> Sing l
   fl (SNil :: Sing (l :: [y])) = SNil
When we reach the pattern signature, 'l' is in scope from the
outer 'forall':
   "a" :-> a_sk :: *
   "l" :-> l_sk :: [a_sk]
We make up a fresh meta-TauTv, y_sig, for 'y', and kind-check
the pattern signature
   Sing (l :: [y])
That unifies y_sig := a_sk.  We return from tcHsPatSigType with
the pair ("y" :-> y_sig).

For RULE binders, though, things are a bit different (yuk).
  RULE "foo" forall (x::a) (y::[a]).  f x y = ...
Here this really is the binding site of the type variable so we'd like
to use a skolem, so that we get a complaint if we unify two of them
together.  Hence the new_tv function in tcHsPatSigType.


************************************************************************
*                                                                      *
        Checking kinds
*                                                                      *
************************************************************************

-}

unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
unifyKinds :: [LHsType GhcRn] -> [(Type, Type)] -> TcM ([Type], Type)
unifyKinds rn_tys :: [LHsType GhcRn]
rn_tys act_kinds :: [(Type, Type)]
act_kinds
  = do { Type
kind <- TcM Type
newMetaKindVar
       ; let check :: LHsType GhcRn -> (Type, Type) -> TcM Type
check rn_ty :: LHsType GhcRn
rn_ty (ty :: Type
ty, act_kind :: Type
act_kind) = HasDebugCallStack =>
RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKind RequireSaturation
YesSaturation (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (HsType GhcRn -> MsgDoc) -> HsType GhcRn -> MsgDoc
forall a b. (a -> b) -> a -> b
$ LHsType GhcRn -> SrcSpanLess (LHsType GhcRn)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsType GhcRn
rn_ty) Type
ty Type
act_kind Type
kind
       ; [Type]
tys' <- (LHsType GhcRn -> (Type, Type) -> TcM Type)
-> [LHsType GhcRn] -> [(Type, Type)] -> TcM [Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM LHsType GhcRn -> (Type, Type) -> TcM Type
check [LHsType GhcRn]
rn_tys [(Type, Type)]
act_kinds
       ; ([Type], Type) -> TcM ([Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
tys', Type
kind) }

{-
************************************************************************
*                                                                      *
    Promotion
*                                                                      *
************************************************************************
-}

-- | Whenever a type is about to be added to the environment, it's necessary
-- to make sure that any free meta-tyvars in the type are promoted to the
-- current TcLevel. (They might be at a higher level due to the level-bumping
-- in tcExplicitTKBndrs, for example.) This function both zonks *and*
-- promotes. Why at the same time? See Note [Recipe for checking a signature]
zonkPromoteType :: TcType -> TcM TcType
zonkPromoteType :: Type -> TcM Type
zonkPromoteType = TyCoMapper () TcM -> () -> Type -> TcM Type
forall (m :: * -> *) env.
Monad m =>
TyCoMapper env m -> env -> Type -> m Type
mapType TyCoMapper () TcM
zonkPromoteMapper ()

-- cf. TcMType.zonkTcTypeMapper
zonkPromoteMapper :: TyCoMapper () TcM
zonkPromoteMapper :: TyCoMapper () TcM
zonkPromoteMapper = TyCoMapper :: forall env (m :: * -> *).
Bool
-> (env -> TcTyVar -> m Type)
-> (env -> TcTyVar -> m Coercion)
-> (env -> CoercionHole -> m Coercion)
-> (env -> TcTyVar -> ArgFlag -> m (env, TcTyVar))
-> (TyCon -> m TyCon)
-> TyCoMapper env m
TyCoMapper { tcm_smart :: Bool
tcm_smart    = Bool
True
                               , tcm_tyvar :: () -> TcTyVar -> TcM Type
tcm_tyvar    = (TcTyVar -> TcM Type) -> () -> TcTyVar -> TcM Type
forall a b. a -> b -> a
const TcTyVar -> TcM Type
zonkPromoteTcTyVar
                               , tcm_covar :: () -> TcTyVar -> TcM Coercion
tcm_covar    = (TcTyVar -> TcM Coercion) -> () -> TcTyVar -> TcM Coercion
forall a b. a -> b -> a
const TcTyVar -> TcM Coercion
covar
                               , tcm_hole :: () -> CoercionHole -> TcM Coercion
tcm_hole     = (CoercionHole -> TcM Coercion)
-> () -> CoercionHole -> TcM Coercion
forall a b. a -> b -> a
const CoercionHole -> TcM Coercion
hole
                               , tcm_tycobinder :: () -> TcTyVar -> ArgFlag -> TcM ((), TcTyVar)
tcm_tycobinder = (TcTyVar -> ArgFlag -> TcM ((), TcTyVar))
-> () -> TcTyVar -> ArgFlag -> TcM ((), TcTyVar)
forall a b. a -> b -> a
const TcTyVar -> ArgFlag -> TcM ((), TcTyVar)
tybinder
                               , tcm_tycon :: TyCon -> TcRn TyCon
tcm_tycon    = TyCon -> TcRn TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return }
  where
    covar :: TcTyVar -> TcM Coercion
covar cv :: TcTyVar
cv
      = TcTyVar -> Coercion
mkCoVarCo (TcTyVar -> Coercion) -> TcM TcTyVar -> TcM Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind TcTyVar
cv

    hole :: CoercionHole -> TcM Coercion
    hole :: CoercionHole -> TcM Coercion
hole h :: CoercionHole
h
      = do { Maybe Coercion
contents <- CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe CoercionHole
h
           ; case Maybe Coercion
contents of
               Just co :: Coercion
co -> do { Coercion
co <- Coercion -> TcM Coercion
zonkPromoteCoercion Coercion
co
                             ; TcTyVar -> Coercion -> TcM Coercion
checkCoercionHole TcTyVar
cv Coercion
co }
               Nothing -> do { TcTyVar
cv' <- TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind TcTyVar
cv
                             ; Coercion -> TcM Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ CoercionHole -> Coercion
mkHoleCo (CoercionHole -> TcTyVar -> CoercionHole
setCoHoleCoVar CoercionHole
h TcTyVar
cv') } }
      where
        cv :: TcTyVar
cv = CoercionHole -> TcTyVar
coHoleCoVar CoercionHole
h

    tybinder :: TyVar -> ArgFlag -> TcM ((), TyVar)
    tybinder :: TcTyVar -> ArgFlag -> TcM ((), TcTyVar)
tybinder tv :: TcTyVar
tv _flag :: ArgFlag
_flag = ((), ) (TcTyVar -> ((), TcTyVar)) -> TcM TcTyVar -> TcM ((), TcTyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind TcTyVar
tv

zonkPromoteTcTyVar :: TyCoVar -> TcM TcType
zonkPromoteTcTyVar :: TcTyVar -> TcM Type
zonkPromoteTcTyVar tv :: TcTyVar
tv
  | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
  = do { let ref :: IORef MetaDetails
ref = TcTyVar -> IORef MetaDetails
metaTyVarRef TcTyVar
tv
       ; MetaDetails
contents <- IORef MetaDetails -> TcRnIf TcGblEnv TcLclEnv MetaDetails
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef MetaDetails
ref
       ; case MetaDetails
contents of
           Flexi -> do { (_, promoted_tv :: TcTyVar
promoted_tv) <- TcTyVar -> TcM (Bool, TcTyVar)
promoteTyVar TcTyVar
tv
                       ; TcTyVar -> Type
mkTyVarTy (TcTyVar -> Type) -> TcM TcTyVar -> TcM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind TcTyVar
promoted_tv }
           Indirect ty :: Type
ty -> Type -> TcM Type
zonkPromoteType Type
ty }

  | TcTyVar -> Bool
isTcTyVar TcTyVar
tv Bool -> Bool -> Bool
&& TcTyVar -> Bool
isSkolemTyVar TcTyVar
tv  -- NB: isSkolemTyVar says "True" to pure TyVars
  = do { TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
       ; TcTyVar -> Type
mkTyVarTy (TcTyVar -> Type) -> TcM TcTyVar -> TcM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind (TcLevel -> TcTyVar -> TcTyVar
promoteSkolem TcLevel
tc_lvl TcTyVar
tv) }

  | Bool
otherwise
  = TcTyVar -> Type
mkTyVarTy (TcTyVar -> Type) -> TcM TcTyVar -> TcM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind TcTyVar
tv

zonkPromoteTyCoVarKind :: TyCoVar -> TcM TyCoVar
zonkPromoteTyCoVarKind :: TcTyVar -> TcM TcTyVar
zonkPromoteTyCoVarKind = (Type -> TcM Type) -> TcTyVar -> TcM TcTyVar
forall (m :: * -> *).
Monad m =>
(Type -> m Type) -> TcTyVar -> m TcTyVar
updateTyVarKindM Type -> TcM Type
zonkPromoteType

zonkPromoteCoercion :: Coercion -> TcM Coercion
zonkPromoteCoercion :: Coercion -> TcM Coercion
zonkPromoteCoercion = TyCoMapper () TcM -> () -> Coercion -> TcM Coercion
forall (m :: * -> *) env.
Monad m =>
TyCoMapper env m -> env -> Coercion -> m Coercion
mapCoercion TyCoMapper () TcM
zonkPromoteMapper ()

{-
************************************************************************
*                                                                      *
        Sort checking kinds
*                                                                      *
************************************************************************

tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
It does sort checking and desugaring at the same time, in one single pass.
-}

tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig :: UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig ctxt :: UserTypeCtxt
ctxt hs_kind :: LHsType GhcRn
hs_kind
-- See  Note [Recipe for checking a signature] in TcHsType
-- Result is zonked
  = do { Type
kind <- String -> TcM Type -> TcM Type
forall a. String -> TcM a -> TcM a
solveLocalEqualities "tcLHsKindSig" (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
                 TcTyMode -> LHsType GhcRn -> TcM Type
tc_lhs_kind TcTyMode
kindLevelMode LHsType GhcRn
hs_kind
       ; String -> MsgDoc -> TcM ()
traceTc "tcLHsKindSig" (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_kind MsgDoc -> MsgDoc -> MsgDoc
$$ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind)
       -- No generalization, so we must promote
       ; Type
kind <- Type -> TcM Type
zonkPromoteType Type
kind
         -- This zonk is very important in the case of higher rank kinds
         -- E.g. Trac #13879    f :: forall (p :: forall z (y::z). <blah>).
         --                          <more blah>
         --      When instantiating p's kind at occurrences of p in <more blah>
         --      it's crucial that the kind we instantiate is fully zonked,
         --      else we may fail to substitute properly

       ; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
kind
       ; String -> MsgDoc -> TcM ()
traceTc "tcLHsKindSig2" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind)
       ; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
kind }

tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
tc_lhs_kind :: TcTyMode -> LHsType GhcRn -> TcM Type
tc_lhs_kind mode :: TcTyMode
mode k :: LHsType GhcRn
k
  = MsgDoc -> TcM Type -> TcM Type
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (String -> MsgDoc
text "In the kind" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
k)) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
    TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type (TcTyMode -> TcTyMode
kindLevel TcTyMode
mode) LHsType GhcRn
k Type
liftedTypeKind

promotionErr :: Name -> PromotionErr -> TcM a
promotionErr :: Name -> PromotionErr -> TcM a
promotionErr name :: Name
name err :: PromotionErr
err
  = MsgDoc -> TcM a
forall a. MsgDoc -> TcM a
failWithTc (MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (PromotionErr -> MsgDoc
pprPECategory PromotionErr
err MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name) MsgDoc -> MsgDoc -> MsgDoc
<+> String -> MsgDoc
text "cannot be used here")
                   2 (MsgDoc -> MsgDoc
parens MsgDoc
reason))
  where
    reason :: MsgDoc
reason = case PromotionErr
err of
               ConstrainedDataConPE pred :: Type
pred
                              -> String -> MsgDoc
text "it has an unpromotable context"
                                 MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
pred)
               FamDataConPE   -> String -> MsgDoc
text "it comes from a data family instance"
               NoDataKindsTC  -> String -> MsgDoc
text "perhaps you intended to use DataKinds"
               NoDataKindsDC  -> String -> MsgDoc
text "perhaps you intended to use DataKinds"
               PatSynPE       -> String -> MsgDoc
text "pattern synonyms cannot be promoted"
               PatSynExPE     -> [MsgDoc] -> MsgDoc
sep [ String -> MsgDoc
text "the existential variables of a pattern synonym"
                                     , String -> MsgDoc
text "signature do not scope over the pattern" ]
               _ -> String -> MsgDoc
text "it is defined and used in the same recursive group"

{-
************************************************************************
*                                                                      *
                Scoped type variables
*                                                                      *
************************************************************************
-}

badPatTyVarTvs :: TcType -> [TyVar] -> SDoc
badPatTyVarTvs :: Type -> [TcTyVar] -> MsgDoc
badPatTyVarTvs sig_ty :: Type
sig_ty bad_tvs :: [TcTyVar]
bad_tvs
  = [MsgDoc] -> MsgDoc
vcat [ [MsgDoc] -> MsgDoc
fsep [String -> MsgDoc
text "The type variable" MsgDoc -> MsgDoc -> MsgDoc
<> [TcTyVar] -> MsgDoc
forall a. [a] -> MsgDoc
plural [TcTyVar]
bad_tvs,
                 MsgDoc -> MsgDoc
quotes ((TcTyVar -> MsgDoc) -> [TcTyVar] -> MsgDoc
forall a. (a -> MsgDoc) -> [a] -> MsgDoc
pprWithCommas TcTyVar -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
bad_tvs),
                 String -> MsgDoc
text "should be bound by the pattern signature" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
sig_ty),
                 String -> MsgDoc
text "but are actually discarded by a type synonym" ]
         , String -> MsgDoc
text "To fix this, expand the type synonym"
         , String -> MsgDoc
text "[Note: I hope to lift this restriction in due course]" ]

{-
************************************************************************
*                                                                      *
          Error messages and such
*                                                                      *
************************************************************************
-}


{- Note [Free-floating kind vars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  data S a = MkS (Proxy (a :: k))

According to the rules around implicitly-bound kind variables,
that k scopes over the whole declaration. The renamer grabs
it and adds it to the hsq_implicits field of the HsQTyVars of the
tycon.  So we get
   S :: forall {k}. k -> Type

That's fine.  But consider this variant:
  data T = MkT (forall (a :: k). Proxy a)
  -- from test ghci/scripts/T7873

This is not an existential datatype, but a higher-rank one (the forall
to the right of MkT). Again, 'k' scopes over the whole declaration,
but we do not want to get
   T :: forall {k}. Type
Why not? Because the kind variable isn't fixed by anything. For
a variable like k to be implicit, it needs to be mentioned in the kind
of a tycon tyvar. But it isn't.

Rejecting T depends on whether or not the datatype has a CUSK.

Non-CUSK (handled in TcTyClsDecls.kcTyClGroup (generalise)):
   When generalising the TyCon we check that every Specified 'k'
   appears free in the kind of the TyCon; that is, in the kind of
   one of its Required arguments, or the result kind.

CUSK (handled in TcHsType.kcLHsQTyVars, the CUSK case):
   When we determine the tycon's final, never-to-be-changed kind
   in kcLHsQTyVars, we check to make sure all implicitly-bound kind
   vars are indeed mentioned in a kind somewhere. If not, error.

We also perform free-floating kind var analysis for type family instances
(see #13985). Here is an interesting example:

    type family   T :: k
    type instance T = (Nothing :: Maybe a)

Upon a cursory glance, it may appear that the kind variable `a` is
free-floating above, since there are no (visible) LHS patterns in `T`. However,
there is an *invisible* pattern due to the return kind, so inside of GHC, the
instance looks closer to this:

    type family T @k :: k
    type instance T @(Maybe a) = (Nothing :: Maybe a)

Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
fact not free-floating. Contrast that with this example:

    type instance T = Proxy (Nothing :: Maybe a)

This would looks like this inside of GHC:

    type instance T @(*) = Proxy (Nothing :: Maybe a)

So this time, `a` is neither bound by a visible nor invisible type pattern on
the LHS, so it would be reported as free-floating.

Finally, here's one more brain-teaser (from #9574). In the example below:

    class Funct f where
      type Codomain f :: *
    instance Funct ('KProxy :: KProxy o) where
      type Codomain 'KProxy = NatTr (Proxy :: o -> *)

As it turns out, `o` is not free-floating in this example. That is because `o`
bound by the kind signature of the LHS type pattern 'KProxy. To make this more
obvious, one can also write the instance like so:

    instance Funct ('KProxy :: KProxy o) where
      type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
-}

-- See Note [Free-floating kind vars]
reportFloatingKvs :: Name         -- of the tycon
                  -> TyConFlavour -- What sort of TyCon it is
                  -> [TcTyVar]    -- all tyvars, not necessarily zonked
                  -> [TcTyVar]    -- floating tyvars
                  -> TcM ()
reportFloatingKvs :: Name -> TyConFlavour -> [TcTyVar] -> [TcTyVar] -> TcM ()
reportFloatingKvs tycon_name :: Name
tycon_name flav :: TyConFlavour
flav all_tvs :: [TcTyVar]
all_tvs bad_tvs :: [TcTyVar]
bad_tvs
  = Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
bad_tvs) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$  -- don't bother zonking if there's no error
    do { [TcTyVar]
all_tvs <- (TcTyVar -> TcM TcTyVar) -> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HasDebugCallStack => TcTyVar -> TcM TcTyVar
TcTyVar -> TcM TcTyVar
zonkTcTyVarToTyVar [TcTyVar]
all_tvs
       ; [TcTyVar]
bad_tvs <- (TcTyVar -> TcM TcTyVar) -> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HasDebugCallStack => TcTyVar -> TcM TcTyVar
TcTyVar -> TcM TcTyVar
zonkTcTyVarToTyVar [TcTyVar]
bad_tvs
       ; let (tidy_env :: TidyEnv
tidy_env, tidy_all_tvs :: [TcTyVar]
tidy_all_tvs) = TidyEnv -> [TcTyVar] -> (TidyEnv, [TcTyVar])
tidyOpenTyCoVars TidyEnv
emptyTidyEnv [TcTyVar]
all_tvs
             tidy_bad_tvs :: [TcTyVar]
tidy_bad_tvs             = (TcTyVar -> TcTyVar) -> [TcTyVar] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (TidyEnv -> TcTyVar -> TcTyVar
tidyTyCoVarOcc TidyEnv
tidy_env) [TcTyVar]
bad_tvs
       ; (TcTyVar -> TcM ()) -> [TcTyVar] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([TcTyVar] -> TcTyVar -> TcM ()
report [TcTyVar]
tidy_all_tvs) [TcTyVar]
tidy_bad_tvs }
  where
    report :: [TcTyVar] -> TcTyVar -> TcM ()
report tidy_all_tvs :: [TcTyVar]
tidy_all_tvs tidy_bad_tv :: TcTyVar
tidy_bad_tv
      = MsgDoc -> TcM ()
addErr (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
        [MsgDoc] -> MsgDoc
vcat [ String -> MsgDoc
text "Kind variable" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (TcTyVar -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyVar
tidy_bad_tv) MsgDoc -> MsgDoc -> MsgDoc
<+>
               String -> MsgDoc
text "is implicitly bound in" MsgDoc -> MsgDoc -> MsgDoc
<+> TyConFlavour -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyConFlavour
flav
             , MsgDoc -> MsgDoc
quotes (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
tycon_name) MsgDoc -> MsgDoc -> MsgDoc
<> MsgDoc
comma MsgDoc -> MsgDoc -> MsgDoc
<+>
               String -> MsgDoc
text "but does not appear as the kind of any"
             , String -> MsgDoc
text "of its type variables. Perhaps you meant"
             , String -> MsgDoc
text "to bind it explicitly somewhere?"
             , Bool -> MsgDoc -> MsgDoc
ppWhen (Bool -> Bool
not ([TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tidy_all_tvs)) (MsgDoc -> MsgDoc) -> MsgDoc -> MsgDoc
forall a b. (a -> b) -> a -> b
$
                 MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text "Type variables with inferred kinds:")
                 2 ([TcTyVar] -> MsgDoc
ppr_tv_bndrs [TcTyVar]
tidy_all_tvs) ]

    ppr_tv_bndrs :: [TcTyVar] -> MsgDoc
ppr_tv_bndrs tvs :: [TcTyVar]
tvs = [MsgDoc] -> MsgDoc
sep ((TcTyVar -> MsgDoc) -> [TcTyVar] -> [MsgDoc]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> MsgDoc
pp_tv [TcTyVar]
tvs)
    pp_tv :: TcTyVar -> MsgDoc
pp_tv tv :: TcTyVar
tv         = MsgDoc -> MsgDoc
parens (TcTyVar -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyVar
tv MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TcTyVar -> Type
tyVarKind TcTyVar
tv))

-- | If the inner action emits constraints, report them as errors and fail;
-- otherwise, propagates the return value. Useful as a wrapper around
-- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
-- another chance to solve constraints
failIfEmitsConstraints :: TcM a -> TcM a
failIfEmitsConstraints :: TcM a -> TcM a
failIfEmitsConstraints thing_inside :: TcM a
thing_inside
  = TcM a -> TcM a
forall a. TcM a -> TcM a
checkNoErrs (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$  -- We say that we fail if there are constraints!
                   -- c.f same checkNoErrs in solveEqualities
    do { (res :: a
res, lie :: WantedConstraints
lie) <- TcM a -> TcM (a, WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints TcM a
thing_inside
       ; WantedConstraints -> TcM ()
reportAllUnsolved WantedConstraints
lie
       ; a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res
       }

-- | Make an appropriate message for an error in a function argument.
-- Used for both expressions and types.
funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
funAppCtxt :: fun -> arg -> Int -> MsgDoc
funAppCtxt fun :: fun
fun arg :: arg
arg arg_no :: Int
arg_no
  = MsgDoc -> Int -> MsgDoc -> MsgDoc
hang ([MsgDoc] -> MsgDoc
hsep [ String -> MsgDoc
text "In the", Int -> MsgDoc
speakNth Int
arg_no, PtrString -> MsgDoc
ptext (String -> PtrString
sLit "argument of"),
                    MsgDoc -> MsgDoc
quotes (fun -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr fun
fun) MsgDoc -> MsgDoc -> MsgDoc
<> String -> MsgDoc
text ", namely"])
       2 (MsgDoc -> MsgDoc
quotes (arg -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr arg
arg))

-- | Add a "In the data declaration for T" or some such.
addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt name :: Name
name flav :: TyConFlavour
flav
  = MsgDoc -> TcM a -> TcM a
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (MsgDoc -> TcM a -> TcM a) -> MsgDoc -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$ [MsgDoc] -> MsgDoc
hsep [ String -> MsgDoc
text "In the", TyConFlavour -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyConFlavour
flav
                      , String -> MsgDoc
text "declaration for", MsgDoc -> MsgDoc
quotes (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name) ]