{-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module TcHsType (
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(..),
kcLookupTcTyCon, bindTyClTyVars,
etaExpandAlgTyCon, tcbVisibilities,
zonkAndScopedSort,
kcLHsQTyVars,
tcWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
failIfEmitsConstraints,
solveEqualities,
typeLevelMode, kindLevelMode,
kindGeneralize, checkExpectedKind, RequireSaturation(..),
reportFloatingKvs,
tcLHsKindSig, badKindSig,
zonkPromoteType,
tcHsPatSigType, tcPatSig,
funAppCtxt, addTyConFlavCtxt
) where
#include "GhclibHsVersions.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 )
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
funsSigCtxt :: [Located Name] -> UserTypeCtxt
funsSigCtxt :: [Located Name] -> UserTypeCtxt
funsSigCtxt (L SrcSpan
_ Name
name1 : [Located Name]
_) = Name -> Bool -> UserTypeCtxt
FunSigCtxt Name
name1 Bool
False
funsSigCtxt [] = String -> UserTypeCtxt
forall a. String -> a
panic String
"funSigCtxt"
addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt UserTypeCtxt
ctxt LHsType GhcRn
hs_ty 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 :: UserTypeCtxt -> LHsType GhcRn -> MsgDoc
pprSigCtxt UserTypeCtxt
ctxt LHsType GhcRn
hs_ty
| Just Name
n <- UserTypeCtxt -> Maybe Name
isSigMaybe UserTypeCtxt
ctxt
= MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text String
"In the type signature:")
Int
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 String
"In" MsgDoc -> MsgDoc -> MsgDoc
<+> UserTypeCtxt -> MsgDoc
pprUserTypeCtxt UserTypeCtxt
ctxt MsgDoc -> MsgDoc -> MsgDoc
<> MsgDoc
colon)
Int
2 (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_ty)
tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
tcHsSigWcType UserTypeCtxt
ctxt 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 SkolemInfo
skol_info [Located Name]
names 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 :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
tcClassSigType SkolemInfo
skol_info [Located Name]
names 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)
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcHsSigType UserTypeCtxt
ctxt 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 String
"tcHsSigType {" (LHsSigType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsSigType GhcRn
sig_ty)
; (Bool
insol, 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
; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
ty
; String -> MsgDoc -> TcM ()
traceTc String
"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)
tc_hs_sig_type :: SkolemInfo
-> LHsSigType GhcRn
-> ContextKind
-> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
tc_hs_sig_type SkolemInfo
skol_info LHsSigType GhcRn
hs_sig_type 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 { (TcLevel
tc_lvl, (WantedConstraints
wanted, ([TcTyVar]
spec_tkvs, 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 String
"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 }
; [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 SkolemInfo
_ (XHsImplicitBndrs XXHsImplicitBndrs GhcRn (LHsType GhcRn)
_) ContextKind
_ = String -> IOEnv (Env TcGblEnv TcLclEnv) (Bool, Type)
forall a. String -> a
panic String
"tc_hs_sig_type"
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType LHsSigType GhcRn
hs_sig_type 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 String
"tcTopLHsType {" (LHsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsType GhcRn
hs_ty)
; ([TcTyVar]
spec_tkvs, 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 String
"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 XXHsImplicitBndrs GhcRn (LHsType GhcRn)
_) ContextKind
_ = String -> TcM Type
forall a. String -> a
panic String
"tcTopLHsType"
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TcTyVar], (Class, [Type], [Type]))
tcHsDeriv 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
$
LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType LHsSigType GhcRn
hs_ty ContextKind
AnyKind
; let ([TcTyVar]
tvs, Type
pred) = Type -> ([TcTyVar], Type)
splitForAllTys Type
ty
([Type]
kind_args, Type
_) = Type -> ([Type], Type)
splitFunTys (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
pred)
; case Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred of
Just (Class
cls, [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))
Maybe (Class, [Type])
Nothing -> MsgDoc -> TcM ([TcTyVar], (Class, [Type], [Type]))
forall a. MsgDoc -> TcM a
failWithTc (String -> MsgDoc
text String
"Illegal deriving item" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (LHsSigType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr LHsSigType GhcRn
hs_ty)) }
tcDerivStrategy
:: forall a.
Maybe (DerivStrategy GhcRn)
-> TcM ([TyVar], a)
-> TcM (Maybe (DerivStrategy GhcTc), [TyVar], a)
tcDerivStrategy :: Maybe (DerivStrategy GhcRn)
-> TcM ([TcTyVar], a)
-> TcM (Maybe (DerivStrategy GhcTc), [TcTyVar], a)
tcDerivStrategy Maybe (DerivStrategy GhcRn)
mds TcM ([TcTyVar], a)
thing_inside
= case Maybe (DerivStrategy GhcRn)
mds of
Maybe (DerivStrategy GhcRn)
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 DerivStrategy GhcRn
ds -> do (DerivStrategy GhcTc
ds', [TcTyVar]
tvs, 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 DerivStrategy GhcRn
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 DerivStrategy GhcRn
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 DerivStrategy GhcRn
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 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 LHsSigType GhcRn
XViaStrategy GhcRn
ty ContextKind
AnyKind
let ([TcTyVar]
via_tvs, 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
([TcTyVar]
thing_tvs, 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 XViaStrategy GhcTc
Type
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 = do
([TcTyVar]
thing_tvs, 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
-> LHsSigType GhcRn
-> TcM Type
tcHsClsInstType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcHsClsInstType UserTypeCtxt
user_ctxt 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 {
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 }
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
tcHsTypeApp :: LHsWcType GhcRn -> Type -> TcM Type
tcHsTypeApp LHsWcType GhcRn
wc_ty 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 String
"tcHsTypeApp" (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
$
[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
$ \ [(Name, TcTyVar)]
_ ->
LHsType GhcRn -> Type -> TcM Type
tcCheckLHsType LHsType GhcRn
hs_ty Type
kind
; 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 XXHsWildCardBndrs GhcRn (LHsType GhcRn)
_) Type
_ = String -> TcM Type
forall a. String -> a
panic String
"tcHsTypeApp"
tcHsOpenType, tcHsLiftedType,
tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
tcHsOpenType :: LHsType GhcRn -> TcM Type
tcHsOpenType 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 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 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 LHsType GhcRn
ty = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
typeLevelMode LHsType GhcRn
ty Type
liftedTypeKind
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
tcCheckLHsType :: LHsType GhcRn -> Type -> TcM Type
tcCheckLHsType LHsType GhcRn
hs_ty 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)
tcLHsType :: LHsType GhcRn -> TcM (Type, Type)
tcLHsType 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)
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (Type, Type)
tcLHsTypeUnsaturated 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
data RequireSaturation
= YesSaturation
| NoSaturation
data TcTyMode
= TcTyMode { TcTyMode -> TypeOrKind
mode_level :: TypeOrKind
, TcTyMode -> RequireSaturation
mode_sat :: RequireSaturation
}
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 TcTyMode
mode = TcTyMode
mode { mode_sat :: RequireSaturation
mode_sat = RequireSaturation
NoSaturation }
kindLevel :: TcTyMode -> TcTyMode
kindLevel :: TcTyMode -> TcTyMode
kindLevel TcTyMode
mode = TcTyMode
mode { mode_level :: TypeOrKind
mode_level = TypeOrKind
KindLevel }
instance Outputable RequireSaturation where
ppr :: RequireSaturation -> MsgDoc
ppr RequireSaturation
YesSaturation = String -> MsgDoc
text String
"YesSaturation"
ppr RequireSaturation
NoSaturation = String -> MsgDoc
text String
"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
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode (L SrcSpan
span 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 { (Type
ty', 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) }
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type TcTyMode
mode (HsParTy XParTy GhcRn
_ LHsType GhcRn
t) = TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
t
tc_infer_hs_type TcTyMode
mode (HsTyVar XTyVar GhcRn
_ PromotionFlag
_ (L SrcSpan
_ IdP GhcRn
tv)) = TcTyMode -> Name -> TcM (Type, Type)
tcTyVar TcTyMode
mode IdP GhcRn
Name
tv
tc_infer_hs_type TcTyMode
mode e :: HsType GhcRn
e@(HsAppTy {}) = TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tcTyApp TcTyMode
mode HsType GhcRn
e
tc_infer_hs_type TcTyMode
mode e :: HsType GhcRn
e@(HsAppKindTy {}) = TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tcTyApp TcTyMode
mode HsType GhcRn
e
tc_infer_hs_type TcTyMode
mode (HsOpTy XOpTy GhcRn
_ LHsType GhcRn
lhs lhs_op :: GenLocated SrcSpan (IdP GhcRn)
lhs_op@(L SrcSpan
_ IdP GhcRn
hs_op) LHsType GhcRn
rhs)
| Bool -> Bool
not (IdP GhcRn
Name
hs_op Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey)
= do { (Type
op, Type
op_kind) <- TcTyMode -> Name -> TcM (Type, Type)
tcTyVar TcTyMode
mode IdP GhcRn
Name
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 NoExt
XTyVar GhcRn
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 TcTyMode
mode (HsKindSig XKindSig GhcRn
_ LHsType GhcRn
ty LHsType GhcRn
sig)
= do { Type
sig' <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig UserTypeCtxt
KindSigCtxt LHsType GhcRn
sig
; String -> MsgDoc -> TcM ()
traceTc String
"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') }
tc_infer_hs_type TcTyMode
mode (HsSpliceTy XSpliceTy GhcRn
_ (HsSpliced XSpliced GhcRn
_ ThModFinalizers
_ (HsSplicedTy HsType GhcRn
ty)))
= TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type TcTyMode
mode HsType GhcRn
ty
tc_infer_hs_type TcTyMode
mode (HsDocTy XDocTy GhcRn
_ LHsType GhcRn
ty LHsDocString
_) = TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
ty
tc_infer_hs_type TcTyMode
_ (XHsType (NHsCoreTy ty))
= do { Type
ty <- Type -> TcM Type
zonkTcType Type
ty
; (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 TcTyMode
_ (HsExplicitListTy XExplicitListTy GhcRn
_ PromotionFlag
_ [LHsType GhcRn]
tys)
| [LHsType GhcRn] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LHsType GhcRn]
tys
= (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 TcTyMode
mode 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 TcTyMode
mode (L SrcSpan
span HsType GhcRn
ty) 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 TcTyMode
mode LHsType GhcRn
ty1 LHsType GhcRn
ty2 Type
exp_kind = case TcTyMode -> TypeOrKind
mode_level TcTyMode
mode of
TypeOrKind
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 NoExt
XFunTy GhcRn
noExt LHsType GhcRn
ty1 LHsType GhcRn
ty2) (Type -> Type -> Type
mkFunTy Type
ty1' Type
ty2')
Type
liftedTypeKind Type
exp_kind }
TypeOrKind
KindLevel ->
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 NoExt
XFunTy GhcRn
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
tc_hs_type :: TcTyMode -> HsType GhcRn -> Type -> TcM Type
tc_hs_type TcTyMode
mode (HsParTy XParTy GhcRn
_ LHsType GhcRn
ty) Type
exp_kind = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind
tc_hs_type TcTyMode
mode (HsDocTy XDocTy GhcRn
_ LHsType GhcRn
ty LHsDocString
_) Type
exp_kind = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
ty Type
exp_kind
tc_hs_type TcTyMode
_ ty :: HsType GhcRn
ty@(HsBangTy XBangTy GhcRn
_ HsSrcBang
bang LHsType GhcRn
_) Type
_
= do { let bangError :: String -> TcM Type
bangError 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 String
"Unexpected" MsgDoc -> MsgDoc -> MsgDoc
<+> String -> MsgDoc
text String
err MsgDoc -> MsgDoc -> MsgDoc
<+> String -> MsgDoc
text String
"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 String
"annotation cannot appear nested inside a type"
; case HsSrcBang
bang of
HsSrcBang SourceText
_ SrcUnpackedness
SrcUnpack SrcStrictness
_ -> String -> TcM Type
bangError String
"UNPACK"
HsSrcBang SourceText
_ SrcUnpackedness
SrcNoUnpack SrcStrictness
_ -> String -> TcM Type
bangError String
"NOUNPACK"
HsSrcBang SourceText
_ SrcUnpackedness
NoSrcUnpack SrcStrictness
SrcLazy -> String -> TcM Type
bangError String
"laziness"
HsSrcBang SourceText
_ SrcUnpackedness
_ SrcStrictness
_ -> String -> TcM Type
bangError String
"strictness" }
tc_hs_type TcTyMode
_ ty :: HsType GhcRn
ty@(HsRecTy {}) Type
_
= MsgDoc -> TcM Type
forall a. MsgDoc -> TcM a
failWithTc (String -> MsgDoc
text String
"Record syntax is illegal here:" MsgDoc -> MsgDoc -> MsgDoc
<+> HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)
tc_hs_type TcTyMode
mode (HsSpliceTy XSpliceTy GhcRn
_ (HsSpliced XSpliced GhcRn
_ ThModFinalizers
mod_finalizers (HsSplicedTy HsType GhcRn
ty)))
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
tc_hs_type TcTyMode
_ ty :: HsType GhcRn
ty@(HsSpliceTy {}) Type
_exp_kind
= MsgDoc -> TcM Type
forall a. MsgDoc -> TcM a
failWithTc (String -> MsgDoc
text String
"Unexpected type splice:" MsgDoc -> MsgDoc -> MsgDoc
<+> HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)
tc_hs_type TcTyMode
mode (HsFunTy XFunTy GhcRn
_ LHsType GhcRn
ty1 LHsType GhcRn
ty2) 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 TcTyMode
mode (HsOpTy XOpTy GhcRn
_ LHsType GhcRn
ty1 (L SrcSpan
_ IdP GhcRn
op) LHsType GhcRn
ty2) Type
exp_kind
| IdP GhcRn
Name
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
tc_hs_type 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 }) Type
exp_kind
= do { (TcLevel
tclvl, WantedConstraints
wanted, ([TcTyVar]
tvs', 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
; 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 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 }) 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
; 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
; 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') }
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsListTy XListTy GhcRn
_ LHsType GhcRn
elt_ty) 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 }
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTupleTy XTupleTy GhcRn
_ HsTupleSort
HsBoxedOrConstraintTuple [LHsType GhcRn]
hs_tys) Type
exp_kind
| Just TupleSort
tup_sort <- Type -> Maybe TupleSort
tupKindSort_maybe Type
exp_kind
= String -> MsgDoc -> TcM ()
traceTc String
"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 String
"tc_hs_type tuple 2" ([LHsType GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsType GhcRn]
hs_tys)
; ([Type]
tys, [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
; let (Type
arg_kind, TupleSort
tup_sort)
= case [ (Type
k,TupleSort
s) | Type
k <- [Type]
kinds
, Just TupleSort
s <- [Type -> Maybe TupleSort
tupKindSort_maybe Type
k] ] of
((Type
k,TupleSort
s) : [(Type, TupleSort)]
_) -> (Type
k,TupleSort
s)
[] -> (Type
liftedTypeKind, TupleSort
BoxedTuple)
; [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 SrcSpan
loc HsType GhcRn
hs_ty),Type
ty,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 TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTupleTy XTupleTy GhcRn
_ HsTupleSort
hs_tup_sort [LHsType GhcRn]
tys) 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
HsTupleSort
HsUnboxedTuple -> TupleSort
UnboxedTuple
HsTupleSort
HsBoxedTuple -> TupleSort
BoxedTuple
HsTupleSort
HsConstraintTuple -> TupleSort
ConstraintTuple
HsTupleSort
_ -> String -> TupleSort
forall a. String -> a
panic String
"tc_hs_type HsTupleTy"
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsSumTy XSumTy GhcRn
_ [LHsType GhcRn]
hs_tys) 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 (\LHsType GhcRn
_ -> 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
}
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsExplicitListTy XExplicitListTy GhcRn
_ PromotionFlag
_ [LHsType GhcRn]
tys) 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
; ([Type]
taus', 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 Type
k Type
a Type
b = TyCon -> [Type] -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
consDataCon) [Type
k, Type
a, Type
b]
mk_nil :: Type -> Type
mk_nil Type
k = TyCon -> [Type] -> Type
mkTyConApp (DataCon -> TyCon
promoteDataCon DataCon
nilDataCon) [Type
k]
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsExplicitTupleTy XExplicitTupleTy GhcRn
_ [LHsType GhcRn]
tys) Type
exp_kind
= 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
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsIParamTy XIParamTy GhcRn
_ (L SrcSpan
_ HsIPName
n) LHsType GhcRn
ty) 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 TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsStarTy XStarTy GhcRn
_ Bool
_) Type
exp_kind
= 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
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTyLit XTyLit GhcRn
_ (HsNumTy SourceText
_ Integer
n)) 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 TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsTyLit XTyLit GhcRn
_ (HsStrTy SourceText
_ FastString
s)) 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 }
tc_hs_type TcTyMode
mode ty :: HsType GhcRn
ty@(HsTyVar {}) 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 TcTyMode
mode ty :: HsType GhcRn
ty@(HsAppTy {}) 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 TcTyMode
mode ty :: HsType GhcRn
ty@(HsAppKindTy{}) 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 TcTyMode
mode ty :: HsType GhcRn
ty@(HsOpTy {}) 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 TcTyMode
mode ty :: HsType GhcRn
ty@(HsKindSig {}) 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 TcTyMode
mode ty :: HsType GhcRn
ty@(XHsType (NHsCoreTy{})) 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 TcTyMode
mode wc :: HsType GhcRn
wc@(HsWildCardTy XWildCardTy GhcRn
_) 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))
}
tcWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
tcWildCardOcc :: TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcWildCardOcc TcTyMode
mode HsType GhcRn
wc Type
exp_kind
= do { TcTyVar
wc_tv <- TcM TcTyVar
newWildTyVar
; 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 String
"_") 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
; 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 }
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 TcTyMode
mode HsType GhcRn
hs_ty Type
ek
= do { (Type
ty, 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 Type
k
| Just (Type
k', Coercion
_) <- Type -> Maybe (Type, Coercion)
splitCastTy_maybe Type
k = Type -> Maybe TupleSort
tupKindSort_maybe Type
k'
| Just 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 HsType GhcRn
rn_ty TcTyMode
mode TupleSort
tup_sort [LHsType GhcRn]
tys Type
exp_kind
= do { [Type]
arg_kinds <- case TupleSort
tup_sort of
TupleSort
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)
TupleSort
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 (\LHsType GhcRn
_ -> TcM Type
newOpenTypeKind) [LHsType GhcRn]
tys
TupleSort
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]
-> [TcKind]
-> TcKind
-> TcM TcType
finish_tuple :: HsType GhcRn
-> TcTyMode -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple HsType GhcRn
rn_ty TcTyMode
mode TupleSort
tup_sort [Type]
tau_tys [Type]
tau_kinds Type
exp_kind
= do { String -> MsgDoc -> TcM ()
traceTc String
"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
TupleSort
UnboxedTuple -> [Type]
tau_reps [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tau_tys
TupleSort
BoxedTuple -> [Type]
tau_tys
TupleSort
ConstraintTuple -> [Type]
tau_tys
; TyCon
tycon <- case TupleSort
tup_sort of
TupleSort
ConstraintTuple
| Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
mAX_CTUPLE_SIZE
-> MsgDoc -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall a. MsgDoc -> TcM a
failWith (Int -> MsgDoc
bigConstraintTuple Int
arity)
| Bool
otherwise -> Name -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
tcLookupTyCon (Int -> Name
cTupleTyConName Int
arity)
TupleSort
BoxedTuple -> do { let tc :: TyCon
tc = Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
arity
; TyCon -> TcM ()
checkWiredInTyCon TyCon
tc
; TyCon -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc }
TupleSort
UnboxedTuple -> TyCon -> IOEnv (Env TcGblEnv TcLclEnv) 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
TupleSort
UnboxedTuple -> [Type] -> Type
unboxedTupleKind [Type]
tau_reps
TupleSort
BoxedTuple -> Type
liftedTypeKind
TupleSort
ConstraintTuple -> Type
constraintKind
bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple :: Int -> MsgDoc
bigConstraintTuple Int
arity
= MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text String
"Constraint tuple arity too large:" MsgDoc -> MsgDoc -> MsgDoc
<+> Int -> MsgDoc
int Int
arity
MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
parens (String -> MsgDoc
text String
"max arity =" MsgDoc -> MsgDoc -> MsgDoc
<+> Int -> MsgDoc
int Int
mAX_CTUPLE_SIZE))
Int
2 (String -> MsgDoc
text String
"Instead, use a nested tuple")
tcInferApps :: TcTyMode
-> LHsType GhcRn
-> TcType
-> TcKind
-> [LHsTypeArg GhcRn]
-> TcM (TcType, TcKind)
tcInferApps :: 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]
orig_hs_args
= do { String -> MsgDoc -> TcM ()
traceTc String
"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)
; (Type
f_args, Type
res_k) <- Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
1 TCvSubst
empty_subst Type
fun_ty [TyBinder]
orig_ki_binders Type
orig_inner_ki [LHsTypeArg GhcRn]
orig_hs_args
; String -> MsgDoc -> TcM ()
traceTc String
"tcInferApps }" MsgDoc
empty
; Type
res_k <- Type -> TcM Type
zonkTcType Type
res_k
; (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
([TyBinder]
orig_ki_binders, Type
orig_inner_ki) = Type -> ([TyBinder], Type)
tcSplitPiTys Type
fun_ki
go :: Int
-> TCvSubst
-> TcType
-> [TyBinder]
-> TcKind
-> [LHsTypeArg GhcRn]
-> TcM (TcType, TcKind)
go :: Int
-> TCvSubst
-> Type
-> [TyBinder]
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
go Int
_ TCvSubst
subst Type
fun [TyBinder]
ki_binders 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)
go Int
n TCvSubst
subst Type
fun [TyBinder]
all_kindbinder Type
inner_ki (HsArgPar SrcSpan
_:[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
go Int
n TCvSubst
subst Type
fun all_kindbinder :: [TyBinder]
all_kindbinder@(TyBinder
ki_binder:[TyBinder]
ki_binders) Type
inner_ki
all_args :: [LHsTypeArg GhcRn]
all_args@(LHsTypeArg GhcRn
arg:[LHsTypeArg GhcRn]
args)
| ArgFlag
Specified <- TyBinder -> ArgFlag
tyCoBinderArgFlag TyBinder
ki_binder
, HsTypeArg SrcSpan
_ LHsType GhcRn
ki <- LHsTypeArg GhcRn
arg
= do { String -> MsgDoc -> TcM ()
traceTc String
"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
; 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
$
TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type (TcTyMode -> TcTyMode
kindLevel TcTyMode
mode) LHsType GhcRn
ki Type
exp_kind
; String -> MsgDoc -> TcM ()
traceTc String
"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
+Int
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
= do { String -> MsgDoc -> TcM ()
traceTc String
"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))
; (TCvSubst
subst', 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
= case LHsTypeArg GhcRn
arg of
HsValArg LHsType GhcRn
ty
-> do { String -> MsgDoc -> TcM ()
traceTc String
"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
; 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 String
"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
+Int
1) TCvSubst
subst'
(Type -> Type -> Type
mkNakedAppTy Type
fun Type
arg')
[TyBinder]
ki_binders Type
inner_ki [LHsTypeArg GhcRn]
args }
HsTypeArg SrcSpan
_ LHsType GhcRn
ki -> do { String -> MsgDoc -> TcM ()
traceTc String
"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 SrcSpan
_ -> String -> TcM (Type, Type)
forall a. String -> a
panic String
"tcInferApps"
go Int
n TCvSubst
subst Type
fun [] Type
inner_ki all_args :: [LHsTypeArg GhcRn]
all_args@(LHsTypeArg GhcRn
arg:[LHsTypeArg GhcRn]
args)
| Bool -> Bool
not ([TyBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyBinder]
new_ki_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 LHsType GhcRn
_)
-> do { String -> MsgDoc -> TcM ()
traceTc String
"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)
; (Coercion
co, Type
arg_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)
[Type -> TyBinder
mkAnonBinder Type
arg_k]
Type
res_k [LHsTypeArg GhcRn]
all_args }
(HsTypeArg SrcSpan
_ 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 SrcSpan
_) -> 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
([TyBinder]
new_ki_binders, 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
-Int
1) [LHsTypeArg GhcRn]
orig_hs_args)
ty_app_err :: a -> a -> TcRn a
ty_app_err a
arg 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 String
"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 String
"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 LHsType GhcRn
f [] = LHsType GhcRn
f
appTypeToArg LHsType GhcRn
f (HsValArg LHsType GhcRn
arg : [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 LHsType GhcRn
f (HsTypeArg SrcSpan
l LHsType GhcRn
arg : [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 XAppKindTy GhcRn
SrcSpan
l LHsType GhcRn
f LHsType GhcRn
arg) [LHsTypeArg GhcRn]
args
appTypeToArg LHsType GhcRn
f (HsArgPar SrcSpan
_ : [LHsTypeArg GhcRn]
arg) = LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg LHsType GhcRn
f [LHsTypeArg GhcRn]
arg
tcTyApps :: TcTyMode
-> LHsType GhcRn
-> TcType
-> TcKind
-> [LHsTypeArg GhcRn]
-> TcM (TcType, TcKind)
tcTyApps :: TcTyMode
-> LHsType GhcRn
-> Type
-> Type
-> [LHsTypeArg GhcRn]
-> TcM (Type, Type)
tcTyApps TcTyMode
mode LHsType GhcRn
orig_hs_ty Type
fun_ty Type
fun_ki [LHsTypeArg GhcRn]
args
= do { (Type
ty', 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') }
tcTyApp :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
tcTyApp :: TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tcTyApp TcTyMode
mode HsType GhcRn
e
= do { let (LHsType GhcRn
hs_fun_ty, [LHsTypeArg GhcRn]
hs_args) = HsType GhcRn -> (LHsType GhcRn, [LHsTypeArg GhcRn])
splitHsAppTys HsType GhcRn
e
; (Type
fun_ty, Type
fun_kind) <- TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
hs_fun_ty
; 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 }
checkExpectedKindMode :: HasDebugCallStack
=> TcTyMode
-> SDoc
-> TcType
-> TcKind
-> TcKind
-> TcM TcType
checkExpectedKindMode :: TcTyMode -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKindMode TcTyMode
mode = HasDebugCallStack =>
RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKind (TcTyMode -> RequireSaturation
mode_sat TcTyMode
mode)
checkExpectedKind :: HasDebugCallStack
=> RequireSaturation
-> SDoc
-> TcType
-> TcKind
-> TcKind
-> TcM TcType
checkExpectedKind :: RequireSaturation -> MsgDoc -> Type -> Type -> Type -> TcM Type
checkExpectedKind RequireSaturation
sat MsgDoc
hs_ty Type
ty Type
act Type
exp
= do { (Type
new_ty, Type
new_act) <- case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
tc, [Type]
args)
| 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 {
([Type]
tc_args, 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 String
"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) }
Maybe (TyCon, [Type])
_ -> (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Type
act)
; ([Type]
new_args, 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
-> TcKind
-> TcKind
-> TcM ([TcType], TcCoercionN)
checkExpectedKindX :: MsgDoc -> Type -> Type -> TcM ([Type], Coercion)
checkExpectedKindX MsgDoc
pp_hs_ty Type
act_kind Type
exp_kind
= do {
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
; ([Type]
new_args, 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 }
; String -> MsgDoc -> TcM ()
traceTc String
"checkExpectedKindX" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ MsgDoc
pp_hs_ty
, String -> MsgDoc
text String
"act_kind:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act_kind
, String -> MsgDoc
text String
"act_kind':" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act_kind'
, String -> MsgDoc
text String
"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)
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 String
"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 ])
; ([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 Maybe (LHsContext GhcRn)
Nothing = [Type] -> TcM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return []
tcHsMbContext (Just 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 TcTyMode
mode 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 TcTyMode
mode 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)
tcTyVar :: TcTyMode -> Name -> TcM (Type, Type)
tcTyVar TcTyMode
mode Name
name
= do { String -> MsgDoc -> TcM ()
traceTc String
"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 Name
_ TcTyVar
tv ->
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 TyCon
tc_tc
-> do {
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)
; (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) }
AGlobal (ATyCon 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 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
$
Name -> PromotionErr -> TcM ()
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
FamDataConPE
; let ([TcTyVar]
_, [TcTyVar]
_, [EqSpec]
_, [Type]
theta, [Type]
_, Type
_) = DataCon -> ([TcTyVar], [TcTyVar], [EqSpec], [Type], [Type], Type)
dataConFullSig DataCon
dc
; case [Type] -> Maybe Type
dc_theta_illegal_constraint [Type]
theta of
Just 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
Maybe Type
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 PromotionErr
err -> Name -> PromotionErr -> TcM (Type, Type)
forall a. Name -> PromotionErr -> TcM a
promotionErr Name
name PromotionErr
err
TcTyThing
_ -> String -> TcTyThing -> Name -> TcM (Type, Type)
forall a. String -> TcTyThing -> Name -> TcM a
wrongThingErr String
"type" TcTyThing
thing Name
name }
where
check_tc :: TyCon -> TcM ()
check_tc :: TyCon -> TcM ()
check_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 }
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 Type
pred | Just 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
addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt (L SrcSpan
_ (HsWildCardTy XWildCardTy GhcRn
_)) TcM a
thing = TcM a
thing
addTypeCtxt (L SrcSpan
_ HsType GhcRn
ty) 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 String
"In the type" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)
tcWildCardBinders :: [Name]
-> ([(Name, TcTyVar)] -> TcM a)
-> TcM a
tcWildCardBinders :: [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcWildCardBinders [Name]
wc_names [(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
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 String
"_")
tyvar :: TcTyVar
tyvar = (Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details)
; String -> MsgDoc -> TcM ()
traceTc String
"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 }
kcLHsQTyVars :: Name
-> TyConFlavour
-> Bool
-> LHsQTyVars GhcRn
-> TcM Kind
-> TcM TcTyCon
kcLHsQTyVars :: Name
-> TyConFlavour
-> Bool
-> LHsQTyVars GhcRn
-> TcM Type
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
kcLHsQTyVars Name
name TyConFlavour
flav Bool
cusk LHsQTyVars GhcRn
tvs TcM Type
thing_inside
| Bool
cusk = Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM Type
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
kcLHsQTyVars_Cusk Name
name TyConFlavour
flav LHsQTyVars GhcRn
tvs TcM Type
thing_inside
| Bool
otherwise = Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM Type
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
kcLHsQTyVars_NonCusk Name
name TyConFlavour
flav LHsQTyVars GhcRn
tvs TcM Type
thing_inside
kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk
:: Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM Kind
-> TcM TcTyCon
kcLHsQTyVars_Cusk :: Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM Type
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
kcLHsQTyVars_Cusk Name
name 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 }) TcM Type
thing_inside
= Name
-> TyConFlavour
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall a. Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt Name
name TyConFlavour
flav (IOEnv (Env TcGblEnv TcLclEnv) TyCon
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon)
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall a b. (a -> b) -> a -> b
$
do { ([TcTyVar]
scoped_kvs, ([TcTyVar]
tc_tvs, 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
; 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
; 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
; [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
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 TyConFlavour
flav
; TyCon -> TcM ()
checkValidTelescope TyCon
tycon
; 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 String
"kcLHsQTyVars: cusk" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ String -> MsgDoc
text String
"name" MsgDoc -> MsgDoc -> MsgDoc
<+> Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name
, String -> MsgDoc
text String
"kv_ns" MsgDoc -> MsgDoc -> MsgDoc
<+> [Name] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Name]
kv_ns
, String -> MsgDoc
text String
"hs_tvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [LHsTyVarBndr GhcRn] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [LHsTyVarBndr GhcRn]
hs_tvs
, String -> MsgDoc
text String
"dep_names" MsgDoc -> MsgDoc -> MsgDoc
<+> NameSet -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr NameSet
dep_names
, String -> MsgDoc
text String
"scoped_kvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
scoped_kvs
, String -> MsgDoc
text String
"tc_tvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
tc_tvs
, String -> MsgDoc
text String
"res_kind" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_kind
, String -> MsgDoc
text String
"candidates" MsgDoc -> MsgDoc -> MsgDoc
<+> CandidatesQTvs -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr CandidatesQTvs
candidates
, String -> MsgDoc
text String
"inferred" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
inferred
, String -> MsgDoc
text String
"specified" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TcTyVar]
specified
, String -> MsgDoc
text String
"final_tc_binders" MsgDoc -> MsgDoc -> MsgDoc
<+> [TyConBinder] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [TyConBinder]
final_tc_binders
, String -> MsgDoc
text String
"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 String
"all_tv_prs" MsgDoc -> MsgDoc -> MsgDoc
<+> [(Name, TcTyVar)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [(Name, TcTyVar)]
all_tv_prs ]
; TyCon -> IOEnv (Env TcGblEnv TcLclEnv) 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 Name
_ TyConFlavour
_ (XLHsQTyVars XXLHsQTyVars GhcRn
_) TcM Type
_ = String -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall a. String -> a
panic String
"kcLHsQTyVars"
kcLHsQTyVars_NonCusk :: Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM Type
-> IOEnv (Env TcGblEnv TcLclEnv) TyCon
kcLHsQTyVars_NonCusk Name
name 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 }) TcM Type
thing_inside
= do { ([TcTyVar]
scoped_kvs, ([TcTyVar]
tc_tvs, Type
res_kind))
<- [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
; let
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
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
TyConFlavour
flav
; String -> MsgDoc -> TcM ()
traceTc String
"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 -> IOEnv (Env TcGblEnv TcLclEnv) 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
mk_tc_binder :: LHsTyVarBndr GhcRn -> TcTyVar -> TyConBinder
mk_tc_binder LHsTyVarBndr GhcRn
hs_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 Name
_ TyConFlavour
_ (XLHsQTyVars XXLHsQTyVars GhcRn
_) TcM Type
_ = String -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall a. String -> a
panic String
"kcLHsQTyVars"
data ContextKind = TheKind Kind
| AnyKind
| OpenKind
newExpectedKind :: ContextKind -> TcM Kind
newExpectedKind :: ContextKind -> TcM Type
newExpectedKind (TheKind Type
k) = Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
k
newExpectedKind ContextKind
AnyKind = TcM Type
newMetaKindVar
newExpectedKind ContextKind
OpenKind = TcM Type
newOpenTypeKind
expectedKindInCtxt :: UserTypeCtxt -> ContextKind
expectedKindInCtxt :: UserTypeCtxt -> ContextKind
expectedKindInCtxt (TySynCtxt Name
_) = ContextKind
AnyKind
expectedKindInCtxt UserTypeCtxt
ThBrackCtxt = ContextKind
AnyKind
expectedKindInCtxt (GhciCtxt {}) = ContextKind
AnyKind
expectedKindInCtxt UserTypeCtxt
DefaultDeclCtxt = ContextKind
AnyKind
expectedKindInCtxt UserTypeCtxt
TypeAppCtxt = ContextKind
AnyKind
expectedKindInCtxt (ForSigCtxt Name
_) = Type -> ContextKind
TheKind Type
liftedTypeKind
expectedKindInCtxt (InstDeclCtxt {}) = Type -> ContextKind
TheKind Type
constraintKind
expectedKindInCtxt UserTypeCtxt
SpecInstCtxt = Type -> ContextKind
TheKind Type
constraintKind
expectedKindInCtxt UserTypeCtxt
_ = ContextKind
OpenKind
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)
-> [Name]
-> TcM a
-> TcM ([TcTyVar], a)
bindImplicitTKBndrsX :: (Name -> TcM TcTyVar) -> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX Name -> TcM TcTyVar
new_tv [Name]
tv_names 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 String
"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
newImplicitTyVarQ :: (Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
newImplicitTyVarQ Name -> TcM TcTyVar
new_tv Name
name
= do { Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe Name
name
; case Maybe TcTyThing
mb_tv of
Just (ATyVar Name
_ TcTyVar
tv) -> TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv
Maybe TcTyThing
_ -> Name -> TcM TcTyVar
new_tv Name
name }
newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
newFlexiKindedTyVar :: (Name -> Type -> TcM TcTyVar) -> Name -> TcM TcTyVar
newFlexiKindedTyVar Name -> Type -> TcM TcTyVar
new_tv 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
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 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 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)
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 HsTyVarBndr GhcRn -> TcM TcTyVar
tc_tv [LHsTyVarBndr GhcRn]
hs_tvs TcM a
thing_inside
= do { String -> MsgDoc -> TcM ()
traceTc String
"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 SrcSpan
_ HsTyVarBndr GhcRn
hs_tv : [LHsTyVarBndr GhcRn]
hs_tvs)
= do { TcTyVar
tv <- HsTyVarBndr GhcRn -> TcM TcTyVar
tc_tv HsTyVarBndr GhcRn
hs_tv
; ([TcTyVar]
tvs, 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
tcHsTyVarBndr :: (Name -> Type -> TcM TcTyVar) -> HsTyVarBndr GhcRn -> TcM TcTyVar
tcHsTyVarBndr Name -> Type -> TcM TcTyVar
new_tv (UserTyVar XUserTyVar GhcRn
_ (L SrcSpan
_ IdP GhcRn
tv_nm))
= do { Type
kind <- TcM Type
newMetaKindVar
; Name -> Type -> TcM TcTyVar
new_tv IdP GhcRn
Name
tv_nm Type
kind }
tcHsTyVarBndr Name -> Type -> TcM TcTyVar
new_tv (KindedTyVar XKindedTyVar GhcRn
_ (L SrcSpan
_ IdP GhcRn
tv_nm) LHsType GhcRn
lhs_kind)
= do { Type
kind <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig (Name -> UserTypeCtxt
TyVarBndrKindCtxt IdP GhcRn
Name
tv_nm) LHsType GhcRn
lhs_kind
; Name -> Type -> TcM TcTyVar
new_tv IdP GhcRn
Name
tv_nm Type
kind }
tcHsTyVarBndr Name -> Type -> TcM TcTyVar
_ (XTyVarBndr XXTyVarBndr GhcRn
_) = String -> TcM TcTyVar
forall a. String -> a
panic String
"tcHsTyVarBndr"
tcHsQTyVarBndr :: ContextKind
-> (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr GhcRn -> TcM TcTyVar
tcHsQTyVarBndr :: ContextKind
-> (Name -> Type -> TcM TcTyVar)
-> HsTyVarBndr GhcRn
-> TcM TcTyVar
tcHsQTyVarBndr ContextKind
ctxt_kind Name -> Type -> TcM TcTyVar
new_tv (UserTyVar XUserTyVar GhcRn
_ (L SrcSpan
_ IdP GhcRn
tv_nm))
= do { Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe IdP GhcRn
Name
tv_nm
; case Maybe TcTyThing
mb_tv of
Just (ATyVar Name
_ TcTyVar
tv) -> TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv
Maybe TcTyThing
_ -> do { Type
kind <- ContextKind -> TcM Type
newExpectedKind ContextKind
ctxt_kind
; Name -> Type -> TcM TcTyVar
new_tv IdP GhcRn
Name
tv_nm Type
kind } }
tcHsQTyVarBndr ContextKind
_ Name -> Type -> TcM TcTyVar
new_tv (KindedTyVar XKindedTyVar GhcRn
_ (L SrcSpan
_ IdP GhcRn
tv_nm) LHsType GhcRn
lhs_kind)
= do { Type
kind <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig (Name -> UserTypeCtxt
TyVarBndrKindCtxt IdP GhcRn
Name
tv_nm) LHsType GhcRn
lhs_kind
; Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe IdP GhcRn
Name
tv_nm
; case Maybe TcTyThing
mb_tv of
Just (ATyVar Name
_ 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)
; TcTyVar -> TcM TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv }
Maybe TcTyThing
_ -> Name -> Type -> TcM TcTyVar
new_tv IdP GhcRn
Name
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 NoExt
XTyVar GhcRn
noExt PromotionFlag
NotPromoted (SrcSpanLess (Located Name) -> Located Name
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc IdP GhcRn
SrcSpanLess (Located Name)
tv_nm)
tcHsQTyVarBndr ContextKind
_ Name -> Type -> TcM TcTyVar
_ (XTyVarBndr XXTyVarBndr GhcRn
_) = String -> TcM TcTyVar
forall a. String -> a
panic String
"tcHsTyVarBndr"
bindTyClTyVars :: Name
-> ([TyConBinder] -> Kind -> TcM a) -> TcM a
bindTyClTyVars :: Name -> ([TyConBinder] -> Type -> TcM a) -> TcM a
bindTyClTyVars Name
tycon_name [TyConBinder] -> Type -> TcM a
thing_inside
= do { TyCon
tycon <- Name -> IOEnv (Env TcGblEnv TcLclEnv) 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 String
"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 }
kcLookupTcTyCon :: Name -> TcM TcTyCon
kcLookupTcTyCon :: Name -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
kcLookupTcTyCon Name
nm
= do { TcTyThing
tc_ty_thing <- Name -> TcM TcTyThing
tcLookup Name
nm
; TyCon -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> IOEnv (Env TcGblEnv TcLclEnv) TyCon)
-> TyCon -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall a b. (a -> b) -> a -> b
$ case TcTyThing
tc_ty_thing of
ATcTyCon TyCon
tc -> TyCon
tc
TcTyThing
_ -> String -> MsgDoc -> TyCon
forall a. HasCallStack => String -> MsgDoc -> a
pprPanic String
"kcLookupTcTyCon" (TcTyThing -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyThing
tc_ty_thing) }
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort [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
; [TcTyVar] -> TcM [TcTyVar]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar] -> [TcTyVar]
scopedSort [TcTyVar]
spec_tkvs) }
kindGeneralize :: TcType -> TcM [KindVar]
kindGeneralize :: Type -> TcM [TcTyVar]
kindGeneralize Type
kind_or_type
= do { Type
kt <- Type -> TcM Type
zonkTcType Type
kind_or_type
; String -> MsgDoc -> TcM ()
traceTc String
"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
; String -> MsgDoc -> TcM ()
traceTc String
"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 }
kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
kindGeneralizeLocal :: WantedConstraints -> Type -> TcM [TcTyVar]
kindGeneralizeLocal WantedConstraints
wanted Type
kind_or_type
= do {
; VarSet
constrained <- VarSet -> TcM VarSet
zonkTyCoVarsAndFV (WantedConstraints -> VarSet
tyCoVarsOfWC WantedConstraints
wanted)
; (Bool
_, VarSet
constrained) <- VarSet -> TcM (Bool, VarSet)
promoteTyVarSet VarSet
constrained
; VarSet
gbl_tvs <- TcM VarSet
tcGetGlobalTyCoVars
; let mono_tvs :: VarSet
mono_tvs = VarSet
gbl_tvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
constrained
; CandidatesQTvs
dvs <- Type -> TcM CandidatesQTvs
candidateQTyVarsOfKind Type
kind_or_type
; String -> MsgDoc -> TcM ()
traceTc String
"kindGeneralizeLocal" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ String -> MsgDoc
text String
"Wanted:" MsgDoc -> MsgDoc -> MsgDoc
<+> WantedConstraints -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr WantedConstraints
wanted
, String -> MsgDoc
text String
"Kind or type:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind_or_type
, String -> MsgDoc
text String
"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 String
"constrained:" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
pprTyVars (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet VarSet
constrained)
, String -> MsgDoc
text String
"mono_tvs:" MsgDoc -> MsgDoc -> MsgDoc
<+> [TcTyVar] -> MsgDoc
pprTyVars (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet VarSet
mono_tvs)
, String -> MsgDoc
text String
"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 }
etaExpandAlgTyCon :: [TyConBinder]
-> Kind
-> TcM ([TyConBinder], Kind)
etaExpandAlgTyCon :: [TyConBinder] -> Type -> TcM ([TyConBinder], Type)
etaExpandAlgTyCon [TyConBinder]
tc_bndrs 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)
, 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 SrcSpan
loc [OccName]
occs [Unique]
uniqs TCvSubst
subst [TyConBinder]
acc Type
kind
= case Type -> Maybe (TyBinder, Type)
splitPiTy_maybe Type
kind of
Maybe (TyBinder, Type)
Nothing -> ([TyConBinder] -> [TyConBinder]
forall a. [a] -> [a]
reverse [TyConBinder]
acc, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
kind)
Just (Anon Type
arg, 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
(Unique
uniq:[Unique]
uniqs') = [Unique]
uniqs
(OccName
occ:[OccName]
occs') = [OccName]
occs
Just (Named (Bndr TcTyVar
tv ArgFlag
vis), 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
(TCvSubst
subst', 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 Bool
check_for_type Type
kind
= MsgDoc -> Int -> MsgDoc -> MsgDoc
hang ([MsgDoc] -> MsgDoc
sep [ String -> MsgDoc
text String
"Kind signature on data type declaration has non-*"
, (if Bool
check_for_type then MsgDoc
empty else String -> MsgDoc
text String
"and non-variable") MsgDoc -> MsgDoc -> MsgDoc
<+>
String -> MsgDoc
text String
"return kind" ])
Int
2 (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind)
tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
tcbVisibilities TyCon
tc [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 Type
_ TCvSubst
_ []
= []
go Type
fun_kind TCvSubst
subst all_args :: [Type]
all_args@(Type
arg : [Type]
args)
| Just (TyBinder
tcb, Type
inner_kind) <- Type -> Maybe (TyBinder, Type)
splitPiTy_maybe Type
fun_kind
= case TyBinder
tcb of
Anon Type
_ -> TyConBndrVis
AnonTCB TyConBndrVis -> [TyConBndrVis] -> [TyConBndrVis]
forall a. a -> [a] -> [a]
: Type -> TCvSubst -> [Type] -> [TyConBndrVis]
go Type
inner_kind TCvSubst
subst [Type]
args
Named (Bndr TcTyVar
tv 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 String
"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)
tcHsPartialSigType
:: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ( [(Name, TcTyVar)]
, Maybe TcType
, [Name]
, [TcTyVar]
, TcThetaType
, TcType )
tcHsPartialSigType :: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM
([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
tcHsPartialSigType UserTypeCtxt
ctxt 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
, ([LHsTyVarBndr GhcRn]
explicit_hs_tvs, L SrcSpan
_ [LHsType GhcRn]
hs_ctxt, 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 { ([TcTyVar]
implicit_tvs, ([TcTyVar]
explicit_tvs, ([(Name, TcTyVar)]
wcs, Maybe Type
wcx, [Type]
theta, 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
$ \ [(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 {
([Type]
theta, 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) }
; 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)
; [(Name, TcTyVar)] -> TcM ()
emitWildCardHoleConstraints [(Name, TcTyVar)]
wcs
; [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 String
"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 UserTypeCtxt
_ (HsWC XHsWC GhcRn (LHsSigType GhcRn)
_ (XHsImplicitBndrs XXHsImplicitBndrs GhcRn (LHsType GhcRn)
_)) = String
-> TcM
([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall a. String -> a
panic String
"tcHsPartialSigType"
tcHsPartialSigType UserTypeCtxt
_ (XHsWildCardBndrs XXHsWildCardBndrs GhcRn (LHsSigType GhcRn)
_) = String
-> TcM
([(Name, TcTyVar)], Maybe Type, [Name], [TcTyVar], [Type], Type)
forall a. String -> a
panic String
"tcHsPartialSigType"
tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
tcPartialContext :: [LHsType GhcRn] -> TcM ([Type], Maybe Type)
tcPartialContext [LHsType GhcRn]
hs_theta
| Just ([LHsType GhcRn]
hs_theta1, LHsType GhcRn
hs_ctxt_last) <- [LHsType GhcRn] -> Maybe ([LHsType GhcRn], LHsType GhcRn)
forall a. [a] -> Maybe ([a], a)
snocView [LHsType GhcRn]
hs_theta
, L SrcSpan
_ wc :: HsType GhcRn
wc@(HsWildCardTy XWildCardTy GhcRn
_) <- 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) }
tcHsPatSigType :: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ( [(Name, TcTyVar)]
, [(Name, TcTyVar)]
, TcType)
tcHsPatSigType :: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType UserTypeCtxt
ctxt 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
; ([(Name, TcTyVar)]
wcs, Type
sig_ty)
<- String
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a. String -> TcM a -> TcM a
solveLocalEqualities String
"tcHsPatSigType" (TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a b. (a -> b) -> a -> b
$
[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
$ \ [(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
; 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 String
"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 = 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
UserTypeCtxt
_ -> Name -> Type -> TcM TcTyVar
newTauTyVar
tcHsPatSigType UserTypeCtxt
_ (HsWC XHsWC GhcRn (LHsSigType GhcRn)
_ (XHsImplicitBndrs XXHsImplicitBndrs GhcRn (LHsType GhcRn)
_)) = String -> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall a. String -> a
panic String
"tcHsPatSigType"
tcHsPatSigType UserTypeCtxt
_ (XHsWildCardBndrs XXHsWildCardBndrs GhcRn (LHsSigType GhcRn)
_) = String -> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
forall a. String -> a
panic String
"tcHsPatSigType"
tcPatSig :: Bool
-> LHsSigWcType GhcRn
-> ExpSigmaType
-> TcM (TcType,
[(Name,TcTyVar)],
[(Name,TcTyVar)],
HsWrapper)
tcPatSig :: Bool
-> LHsSigWcType GhcRn
-> ExpSigmaType
-> TcM (Type, [(Name, TcTyVar)], [(Name, TcTyVar)], HsWrapper)
tcPatSig Bool
in_pat_bind LHsSigWcType GhcRn
sig ExpSigmaType
res_ty
= do { ([(Name, TcTyVar)]
sig_wcs, [(Name, TcTyVar)]
sig_tvs, Type
sig_ty) <- UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType UserTypeCtxt
PatSigCtxt LHsSigWcType GhcRn
sig
; if [(Name, TcTyVar)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, TcTyVar)]
sig_tvs then do {
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
{ 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))
; 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)
; 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_tvs, [(Name, TcTyVar)]
sig_wcs, HsWrapper
wrap)
} }
where
mk_msg :: Type -> TidyEnv -> TcM (TidyEnv, MsgDoc)
mk_msg Type
sig_ty TidyEnv
tidy_env
= do { (TidyEnv
tidy_env, 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
; (TidyEnv
tidy_env, 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 String
"When checking that the pattern signature:")
Int
4 (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
sig_ty)
, Int -> MsgDoc -> MsgDoc
nest Int
2 (MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text String
"fits the type of its context:")
Int
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 [(Name, TcTyVar)]
sig_tvs
= MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text String
"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))
Int
2 (String -> MsgDoc
text String
"in a pattern binding signature")
unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
unifyKinds :: [LHsType GhcRn] -> [(Type, Type)] -> TcM ([Type], Type)
unifyKinds [LHsType GhcRn]
rn_tys [(Type, Type)]
act_kinds
= do { Type
kind <- TcM Type
newMetaKindVar
; let check :: LHsType GhcRn -> (Type, Type) -> TcM Type
check LHsType GhcRn
rn_ty (Type
ty, 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) }
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 ()
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 -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
tcm_tycon = TyCon -> IOEnv (Env TcGblEnv TcLclEnv) TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return }
where
covar :: TcTyVar -> TcM Coercion
covar 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 CoercionHole
h
= do { Maybe Coercion
contents <- CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe CoercionHole
h
; case Maybe Coercion
contents of
Just Coercion
co -> do { Coercion
co <- Coercion -> TcM Coercion
zonkPromoteCoercion Coercion
co
; TcTyVar -> Coercion -> TcM Coercion
checkCoercionHole TcTyVar
cv Coercion
co }
Maybe Coercion
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 TcTyVar
tv 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 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
MetaDetails
Flexi -> do { (Bool
_, 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 Type
ty -> Type -> TcM Type
zonkPromoteType Type
ty }
| TcTyVar -> Bool
isTcTyVar TcTyVar
tv Bool -> Bool -> Bool
&& TcTyVar -> Bool
isSkolemTyVar TcTyVar
tv
= 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 ()
tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig :: UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig UserTypeCtxt
ctxt LHsType GhcRn
hs_kind
= do { Type
kind <- String -> TcM Type -> TcM Type
forall a. String -> TcM a -> TcM a
solveLocalEqualities String
"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 String
"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)
; Type
kind <- Type -> TcM Type
zonkPromoteType Type
kind
; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
kind
; String -> MsgDoc -> TcM ()
traceTc String
"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 TcTyMode
mode LHsType GhcRn
k
= MsgDoc -> TcM Type -> TcM Type
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (String -> MsgDoc
text String
"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 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 String
"cannot be used here")
Int
2 (MsgDoc -> MsgDoc
parens MsgDoc
reason))
where
reason :: MsgDoc
reason = case PromotionErr
err of
ConstrainedDataConPE Type
pred
-> String -> MsgDoc
text String
"it has an unpromotable context"
MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
pred)
PromotionErr
FamDataConPE -> String -> MsgDoc
text String
"it comes from a data family instance"
PromotionErr
NoDataKindsTC -> String -> MsgDoc
text String
"perhaps you intended to use DataKinds"
PromotionErr
NoDataKindsDC -> String -> MsgDoc
text String
"perhaps you intended to use DataKinds"
PromotionErr
PatSynPE -> String -> MsgDoc
text String
"pattern synonyms cannot be promoted"
PromotionErr
PatSynExPE -> [MsgDoc] -> MsgDoc
sep [ String -> MsgDoc
text String
"the existential variables of a pattern synonym"
, String -> MsgDoc
text String
"signature do not scope over the pattern" ]
PromotionErr
_ -> String -> MsgDoc
text String
"it is defined and used in the same recursive group"
badPatTyVarTvs :: TcType -> [TyVar] -> SDoc
badPatTyVarTvs :: Type -> [TcTyVar] -> MsgDoc
badPatTyVarTvs Type
sig_ty [TcTyVar]
bad_tvs
= [MsgDoc] -> MsgDoc
vcat [ [MsgDoc] -> MsgDoc
fsep [String -> MsgDoc
text String
"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 String
"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 String
"but are actually discarded by a type synonym" ]
, String -> MsgDoc
text String
"To fix this, expand the type synonym"
, String -> MsgDoc
text String
"[Note: I hope to lift this restriction in due course]" ]
reportFloatingKvs :: Name
-> TyConFlavour
-> [TcTyVar]
-> [TcTyVar]
-> TcM ()
reportFloatingKvs :: Name -> TyConFlavour -> [TcTyVar] -> [TcTyVar] -> TcM ()
reportFloatingKvs Name
tycon_name TyConFlavour
flav [TcTyVar]
all_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
$
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 (TidyEnv
tidy_env, [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 [TcTyVar]
tidy_all_tvs TcTyVar
tidy_bad_tv
= MsgDoc -> TcM ()
addErr (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ String -> MsgDoc
text String
"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 String
"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 String
"but does not appear as the kind of any"
, String -> MsgDoc
text String
"of its type variables. Perhaps you meant"
, String -> MsgDoc
text String
"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 String
"Type variables with inferred kinds:")
Int
2 ([TcTyVar] -> MsgDoc
ppr_tv_bndrs [TcTyVar]
tidy_all_tvs) ]
ppr_tv_bndrs :: [TcTyVar] -> MsgDoc
ppr_tv_bndrs [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 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))
failIfEmitsConstraints :: TcM a -> TcM a
failIfEmitsConstraints :: TcM a -> TcM a
failIfEmitsConstraints 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
$
do { (a
res, 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
}
funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
funAppCtxt :: fun -> arg -> Int -> MsgDoc
funAppCtxt fun
fun arg
arg Int
arg_no
= MsgDoc -> Int -> MsgDoc -> MsgDoc
hang ([MsgDoc] -> MsgDoc
hsep [ String -> MsgDoc
text String
"In the", Int -> MsgDoc
speakNth Int
arg_no, PtrString -> MsgDoc
ptext (String -> PtrString
sLit String
"argument of"),
MsgDoc -> MsgDoc
quotes (fun -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr fun
fun) MsgDoc -> MsgDoc -> MsgDoc
<> String -> MsgDoc
text String
", namely"])
Int
2 (MsgDoc -> MsgDoc
quotes (arg -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr arg
arg))
addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt Name
name 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 String
"In the", TyConFlavour -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyConFlavour
flav
, String -> MsgDoc
text String
"declaration for", MsgDoc -> MsgDoc
quotes (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
name) ]