{-# LANGUAGE CPP #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Gen.HsType (
kcClassSigType, tcClassSigType,
tcHsSigType, tcHsSigWcType,
tcHsPartialSigType,
tcStandaloneKindSig,
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(..),
bindTyClTyVars, tcFamTyPats,
etaExpandAlgTyCon, tcbVisibilities,
zonkAndScopedSort,
InitialKindStrategy(..),
SAKS_or_CUSK(..),
kcDeclHeader,
tcNamedWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated,
tcCheckLHsType,
tcHsMbContext, tcHsContext, tcLHsPredType,
kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
tcLHsKindSig, checkDataKindSig, DataSort(..),
checkClassKindSig,
tcMult,
tcHsPatSigType,
funAppCtxt, addTyConFlavCtxt
) where
#include "GhclibHsVersions.h"
import GHC.Prelude
import GHC.Hs
import GHC.Rename.Utils
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Origin
import GHC.Core.Predicate
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.TcMType
import GHC.Tc.Validity
import GHC.Tc.Utils.Unify
import GHC.IfaceToCore
import GHC.Tc.Solver
import GHC.Tc.Utils.Zonk
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBindersN,
tcInstInvisibleTyBinder )
import GHC.Core.Type
import GHC.Builtin.Types.Prim
import GHC.Types.Name.Env
import GHC.Types.Name.Reader( lookupLocalRdrOcc )
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Core.TyCon
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Core.Class
import GHC.Types.Name
import GHC.Types.Var.Env
import GHC.Builtin.Types
import GHC.Types.Basic
import GHC.Types.SrcLoc
import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Utils.Misc
import GHC.Types.Unique.Supply
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.FastString
import GHC.Builtin.Names hiding ( wildCardName )
import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import GHC.Parser.Annotation
import GHC.Data.Maybe
import GHC.Data.Bag( unitBag )
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 (GenLocated SrcSpan (HsType GhcRn) -> SrcSpan
forall l e. GenLocated l e -> l
getLoc GenLocated SrcSpan (HsType GhcRn)
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
<+> GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
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 (GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
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 (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 })
= UserTypeCtxt -> LHsType GhcRn -> TcM () -> TcM ()
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt ([Located Name] -> UserTypeCtxt
funsSigCtxt [Located Name]
names) LHsType GhcRn
hs_ty (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { (TcLevel
tc_lvl, WantedConstraints
wanted, ([TcTyVar]
spec_tkvs, Type
_))
<- String
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type))
forall a. String -> TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndSolveEqualitiesX String
"kcClassSigType" (TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, 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
$
LHsType GhcRn -> Type -> TcM Type
tcLHsType LHsType GhcRn
hs_ty Type
liftedTypeKind
; SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info [TcTyVar]
spec_tkvs TcLevel
tc_lvl WantedConstraints
wanted }
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 (p :: Pass). LHsSigType (GhcPass p) -> LHsType (GhcPass p)
hsSigType LHsSigType GhcRn
sig_ty) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
do { (Implication
implic, Type
ty) <- SkolemInfo
-> LHsSigType GhcRn -> ContextKind -> TcM (Implication, Type)
tc_hs_sig_type SkolemInfo
skol_info LHsSigType GhcRn
sig_ty (Type -> ContextKind
TheKind Type
liftedTypeKind)
; Implication -> TcM ()
emitImplication Implication
implic
; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty }
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 (p :: Pass). LHsSigType (GhcPass p) -> LHsType (GhcPass p)
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 {" (HsImplicitBndrs GhcRn (GenLocated SrcSpan (HsType GhcRn)) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsImplicitBndrs GhcRn (GenLocated SrcSpan (HsType GhcRn))
LHsSigType GhcRn
sig_ty)
; (Implication
implic, Type
ty) <- SkolemInfo
-> LHsSigType GhcRn -> ContextKind -> TcM (Implication, Type)
tc_hs_sig_type SkolemInfo
skol_info LHsSigType GhcRn
sig_ty (UserTypeCtxt -> ContextKind
expectedKindInCtxt UserTypeCtxt
ctxt)
; WantedConstraints -> TcM ()
emitFlatConstraints (Bag Implication -> WantedConstraints
mkImplicWC (Implication -> Bag Implication
forall a. a -> Bag a
unitBag Implication
implic))
; Type
ty <- Type -> TcM Type
zonkTcType Type
ty
; 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 (Implication, TcType)
tc_hs_sig_type :: SkolemInfo
-> LHsSigType GhcRn -> ContextKind -> TcM (Implication, 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))
<- String
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type))
forall a. String -> TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndSolveEqualitiesX String
"tc_hs_sig_type" (TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, 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
; LHsType GhcRn -> Type -> TcM Type
tcLHsType 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]
kindGeneralizeSome WantedConstraints
wanted Type
ty1
; Implication
implic <- SkolemInfo
-> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfo
skol_info ([TcTyVar]
kvs [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
spec_tkvs) TcLevel
tc_lvl WantedConstraints
wanted
; (Implication, Type) -> TcM (Implication, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
implic, [TcTyVar] -> Type -> Type
mkInfForAllTys [TcTyVar]
kvs Type
ty1) }
tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Type)
tcStandaloneKindSig (L _ kisig) = case StandaloneKindSig GhcRn
kisig of
StandaloneKindSig XStandaloneKindSig GhcRn
_ (L _ name) LHsSigType GhcRn
ksig ->
let ctxt :: UserTypeCtxt
ctxt = Name -> UserTypeCtxt
StandaloneKindSigCtxt Name
name in
UserTypeCtxt
-> LHsType GhcRn -> TcM (Name, Type) -> TcM (Name, Type)
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt UserTypeCtxt
ctxt (LHsSigType GhcRn -> LHsType GhcRn
forall (p :: Pass). LHsSigType (GhcPass p) -> LHsType (GhcPass p)
hsSigType LHsSigType GhcRn
ksig) (TcM (Name, Type) -> TcM (Name, Type))
-> TcM (Name, Type) -> TcM (Name, Type)
forall a b. (a -> b) -> a -> b
$
do { let mode :: TcTyMode
mode = TypeOrKind -> TcTyMode
mkMode TypeOrKind
KindLevel
; Type
kind <- TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
tc_top_lhs_type TcTyMode
mode LHsSigType GhcRn
ksig (UserTypeCtxt -> ContextKind
expectedKindInCtxt UserTypeCtxt
ctxt)
; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
kind
; (Name, Type) -> TcM (Name, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, Type
kind) }
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType LHsSigType GhcRn
hs_ty ContextKind
ctxt_kind
= TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
tc_top_lhs_type (TypeOrKind -> TcTyMode
mkMode TypeOrKind
TypeLevel) LHsSigType GhcRn
hs_ty ContextKind
ctxt_kind
tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
tc_top_lhs_type TcTyMode
mode 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 {" (GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_ty)
; (TcLevel
tclvl, WantedConstraints
wanted, ([TcTyVar]
spec_tkvs, Type
ty))
<- String
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type))
forall a. String -> TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndSolveEqualitiesX String
"tc_top_lhs_type" (TcM ([TcTyVar], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], Type)))
-> TcM ([TcTyVar], Type)
-> TcM (TcLevel, 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
mode LHsType GhcRn
hs_ty Type
kind }
; [TcTyVar]
spec_tkvs <- [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort [TcTyVar]
spec_tkvs
; SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
reportUnsolvedEqualities SkolemInfo
InstSkol [TcTyVar]
spec_tkvs TcLevel
tclvl WantedConstraints
wanted
; let ty1 :: Type
ty1 = [TcTyVar] -> Type -> Type
mkSpecForAllTys [TcTyVar]
spec_tkvs Type
ty
; [TcTyVar]
kvs <- Type -> TcM [TcTyVar]
kindGeneralizeAll Type
ty1
; Type
final_ty <- Type -> TcM Type
zonkTcTypeToType ([TcTyVar] -> Type -> Type
mkInfForAllTys [TcTyVar]
kvs Type
ty1)
; String -> MsgDoc -> TcM ()
traceTc String
"End tcTopLHsType }" ([MsgDoc] -> MsgDoc
vcat [GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
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}
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 r. TcM r -> TcM r
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
([Scaled Type]
kind_args, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind 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, (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled 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 (HsImplicitBndrs GhcRn (GenLocated SrcSpan (HsType GhcRn)) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsImplicitBndrs GhcRn (GenLocated SrcSpan (HsType GhcRn))
LHsSigType GhcRn
hs_ty)) }
tcDerivStrategy ::
Maybe (LDerivStrategy GhcRn)
-> TcM (Maybe (LDerivStrategy GhcTc), [TyVar])
tcDerivStrategy :: Maybe (LDerivStrategy GhcRn)
-> TcM (Maybe (LDerivStrategy GhcTc), [TcTyVar])
tcDerivStrategy Maybe (LDerivStrategy GhcRn)
mb_lds
= case Maybe (LDerivStrategy GhcRn)
mb_lds of
Maybe (LDerivStrategy GhcRn)
Nothing -> Maybe (Located (DerivStrategy GhcTc))
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
forall ds. ds -> TcM (ds, [TcTyVar])
boring_case Maybe (Located (DerivStrategy GhcTc))
forall a. Maybe a
Nothing
Just (L loc ds) ->
SrcSpan
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar]))
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
forall a b. (a -> b) -> a -> b
$ do
(DerivStrategy GhcTc
ds', [TcTyVar]
tvs) <- DerivStrategy GhcRn -> TcM (DerivStrategy GhcTc, [TcTyVar])
tc_deriv_strategy DerivStrategy GhcRn
ds
(Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
-> TcM (Maybe (Located (DerivStrategy GhcTc)), [TcTyVar])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located (DerivStrategy GhcTc)
-> Maybe (Located (DerivStrategy GhcTc))
forall a. a -> Maybe a
Just (SrcSpan -> DerivStrategy GhcTc -> Located (DerivStrategy GhcTc)
forall l e. l -> e -> GenLocated l e
L SrcSpan
loc DerivStrategy GhcTc
ds'), [TcTyVar]
tvs)
where
tc_deriv_strategy :: DerivStrategy GhcRn
-> TcM (DerivStrategy GhcTc, [TyVar])
tc_deriv_strategy :: DerivStrategy GhcRn -> TcM (DerivStrategy GhcTc, [TcTyVar])
tc_deriv_strategy DerivStrategy GhcRn
StockStrategy = DerivStrategy GhcTc -> TcM (DerivStrategy GhcTc, [TcTyVar])
forall ds. ds -> TcM (ds, [TcTyVar])
boring_case DerivStrategy GhcTc
forall pass. DerivStrategy pass
StockStrategy
tc_deriv_strategy DerivStrategy GhcRn
AnyclassStrategy = DerivStrategy GhcTc -> TcM (DerivStrategy GhcTc, [TcTyVar])
forall ds. ds -> TcM (ds, [TcTyVar])
boring_case DerivStrategy GhcTc
forall pass. DerivStrategy pass
AnyclassStrategy
tc_deriv_strategy DerivStrategy GhcRn
NewtypeStrategy = DerivStrategy GhcTc -> TcM (DerivStrategy GhcTc, [TcTyVar])
forall ds. ds -> TcM (ds, [TcTyVar])
boring_case DerivStrategy GhcTc
forall pass. DerivStrategy pass
NewtypeStrategy
tc_deriv_strategy (ViaStrategy XViaStrategy GhcRn
ty) = do
Type
ty' <- TcM Type -> TcM Type
forall r. TcM r -> TcM r
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'
(DerivStrategy GhcTc, [TcTyVar])
-> TcM (DerivStrategy GhcTc, [TcTyVar])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (XViaStrategy GhcTc -> DerivStrategy GhcTc
forall pass. XViaStrategy pass -> DerivStrategy pass
ViaStrategy Type
XViaStrategy GhcTc
via_pred, [TcTyVar]
via_tvs)
boring_case :: ds -> TcM (ds, [TyVar])
boring_case :: ds -> TcM (ds, [TcTyVar])
boring_case ds
ds = (ds, [TcTyVar]) -> TcM (ds, [TcTyVar])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ds
ds, [])
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 (GenLocated SrcSpan (HsType GhcRn) -> SrcSpan
forall l e. GenLocated l e -> l
getLoc (LHsSigType GhcRn -> LHsType GhcRn
forall (p :: Pass). LHsSigType (GhcPass p) -> LHsType (GhcPass p)
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 r. TcM r -> TcM r
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 { TcTyMode
mode <- TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
TypeLevel HoleMode
HM_VTA
; Type
ty <- 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
$
String -> TcM Type -> TcM Type
forall a. String -> TcM a -> TcM a
solveEqualities String
"tcHsTypeApp" (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
tcNamedWildCardBinders [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)]
_ ->
TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
hs_ty Type
kind
; Type -> TcM ()
kindGeneralizeNone Type
ty
; Type
ty <- Type -> TcM Type
zonkTcType Type
ty
; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
TypeAppCtxt Type
ty
; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty }
tcFamTyPats :: TyCon
-> HsTyPats GhcRn
-> TcM (TcType, TcKind)
tcFamTyPats :: TyCon -> HsTyPats GhcRn -> TcM (Type, Type)
tcFamTyPats TyCon
fam_tc HsTyPats GhcRn
hs_pats
= do { String -> MsgDoc -> TcM ()
traceTc String
"tcFamTyPats {" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ TyCon -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyCon
fam_tc, String -> MsgDoc
text String
"arity:" MsgDoc -> MsgDoc -> MsgDoc
<+> Int -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Int
fam_arity ]
; TcTyMode
mode <- TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
TypeLevel HoleMode
HM_FamPat
; let fun_ty :: Type
fun_ty = TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc []
; (Type
fam_app, Type
res_kind) <- TcTyMode
-> LHsType GhcRn -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
tcInferTyApps TcTyMode
mode GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
lhs_fun Type
fun_ty HsTyPats GhcRn
hs_pats
; String -> MsgDoc -> TcM ()
traceTc String
"End tcFamTyPats }" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ TyCon -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyCon
fam_tc, String -> MsgDoc
text String
"res_kind:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_kind ]
; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
fam_app, Type
res_kind) }
where
fam_name :: Name
fam_name = TyCon -> Name
tyConName TyCon
fam_tc
fam_arity :: Int
fam_arity = TyCon -> Int
tyConArity TyCon
fam_tc
lhs_fun :: GenLocated SrcSpan (HsType GhcRn)
lhs_fun = HsType GhcRn -> GenLocated SrcSpan (HsType GhcRn)
forall e. e -> Located e
noLoc (XTyVar GhcRn -> PromotionFlag -> LIdP GhcRn -> HsType GhcRn
forall pass.
XTyVar pass -> PromotionFlag -> LIdP pass -> HsType pass
HsTyVar NoExtField
XTyVar GhcRn
noExtField PromotionFlag
NotPromoted (Name -> Located Name
forall e. e -> Located e
noLoc Name
fam_name))
tcHsOpenType, tcHsLiftedType,
tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
tcHsOpenType :: LHsType GhcRn -> TcM Type
tcHsOpenType LHsType GhcRn
hs_ty = 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
$ LHsType GhcRn -> TcM Type
tcHsOpenTypeNC LHsType GhcRn
hs_ty
tcHsLiftedType :: LHsType GhcRn -> TcM Type
tcHsLiftedType LHsType GhcRn
hs_ty = 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
$ LHsType GhcRn -> TcM Type
tcHsLiftedTypeNC LHsType GhcRn
hs_ty
tcHsOpenTypeNC :: LHsType GhcRn -> TcM Type
tcHsOpenTypeNC LHsType GhcRn
hs_ty = do { Type
ek <- TcM Type
newOpenTypeKind; LHsType GhcRn -> Type -> TcM Type
tcLHsType LHsType GhcRn
hs_ty Type
ek }
tcHsLiftedTypeNC :: LHsType GhcRn -> TcM Type
tcHsLiftedTypeNC LHsType GhcRn
hs_ty = LHsType GhcRn -> Type -> TcM Type
tcLHsType LHsType GhcRn
hs_ty Type
liftedTypeKind
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM Type
tcCheckLHsType LHsType GhcRn
hs_ty ContextKind
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
$
do { Type
ek <- ContextKind -> TcM Type
newExpectedKind ContextKind
exp_kind
; LHsType GhcRn -> Type -> TcM Type
tcLHsType LHsType GhcRn
hs_ty Type
ek }
tcInferLHsType :: LHsType GhcRn -> TcM TcType
tcInferLHsType :: LHsType GhcRn -> TcM Type
tcInferLHsType LHsType GhcRn
hs_ty
= do { (Type
ty,Type
_kind) <- LHsType GhcRn -> TcM (Type, Type)
tcInferLHsTypeKind LHsType GhcRn
hs_ty
; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty }
tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeKind :: LHsType GhcRn -> TcM (Type, Type)
tcInferLHsTypeKind lhs_ty :: LHsType GhcRn
lhs_ty@(L loc hs_ty)
= LHsType GhcRn -> TcM (Type, Type) -> TcM (Type, Type)
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
lhs_ty (TcM (Type, Type) -> TcM (Type, Type))
-> TcM (Type, Type) -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$
SrcSpan -> TcM (Type, Type) -> TcM (Type, Type)
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM (Type, Type) -> TcM (Type, Type))
-> TcM (Type, Type) -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$
do { (Type
res_ty, Type
res_kind) <- TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type (TypeOrKind -> TcTyMode
mkMode TypeOrKind
TypeLevel) HsType GhcRn
hs_ty
; Type -> Type -> TcM (Type, Type)
tcInstInvisibleTyBinders Type
res_ty Type
res_kind }
tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (Type, Type)
tcInferLHsTypeUnsaturated LHsType GhcRn
hs_ty
= LHsType GhcRn -> TcM (Type, Type) -> TcM (Type, Type)
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
hs_ty (TcM (Type, Type) -> TcM (Type, Type))
-> TcM (Type, Type) -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$
do { TcTyMode
mode <- TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
TypeLevel HoleMode
HM_Sig
; case HsType GhcRn -> Maybe (LHsType GhcRn, HsTyPats GhcRn)
splitHsAppTys (GenLocated SrcSpan (HsType GhcRn) -> HsType GhcRn
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_ty) of
Just (LHsType GhcRn
hs_fun_ty, HsTyPats GhcRn
hs_args)
-> do { (Type
fun_ty, Type
_ki) <- TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tcInferTyAppHead TcTyMode
mode LHsType GhcRn
hs_fun_ty
; TcTyMode
-> LHsType GhcRn -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
tcInferTyApps_nosat TcTyMode
mode LHsType GhcRn
hs_fun_ty Type
fun_ty HsTyPats GhcRn
hs_args }
Maybe (LHsType GhcRn, HsTyPats GhcRn)
Nothing -> TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
hs_ty }
tcMult :: HsArrow GhcRn -> TcM Mult
tcMult :: HsArrow GhcRn -> TcM Type
tcMult HsArrow GhcRn
hc = TcTyMode -> HsArrow GhcRn -> TcM Type
tc_mult (TypeOrKind -> TcTyMode
mkMode TypeOrKind
TypeLevel) HsArrow GhcRn
hc
data TcTyMode
= TcTyMode { TcTyMode -> TypeOrKind
mode_tyki :: TypeOrKind
, TcTyMode -> Maybe (TcLevel, HoleMode)
mode_holes :: Maybe (TcLevel, HoleMode)
}
data HoleMode = HM_Sig
| HM_FamPat
| HM_VTA
mkMode :: TypeOrKind -> TcTyMode
mkMode :: TypeOrKind -> TcTyMode
mkMode TypeOrKind
tyki = TcTyMode :: TypeOrKind -> Maybe (TcLevel, HoleMode) -> TcTyMode
TcTyMode { mode_tyki :: TypeOrKind
mode_tyki = TypeOrKind
tyki, mode_holes :: Maybe (TcLevel, HoleMode)
mode_holes = Maybe (TcLevel, HoleMode)
forall a. Maybe a
Nothing }
mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
tyki HoleMode
hm
= do { TcLevel
lvl <- TcM TcLevel
getTcLevel
; TcTyMode -> TcM TcTyMode
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyMode :: TypeOrKind -> Maybe (TcLevel, HoleMode) -> TcTyMode
TcTyMode { mode_tyki :: TypeOrKind
mode_tyki = TypeOrKind
tyki
, mode_holes :: Maybe (TcLevel, HoleMode)
mode_holes = (TcLevel, HoleMode) -> Maybe (TcLevel, HoleMode)
forall a. a -> Maybe a
Just (TcLevel
lvl,HoleMode
hm) }) }
kindLevel :: TcTyMode -> TcTyMode
kindLevel :: TcTyMode -> TcTyMode
kindLevel TcTyMode
mode = TcTyMode
mode { mode_tyki :: TypeOrKind
mode_tyki = TypeOrKind
KindLevel }
instance Outputable HoleMode where
ppr :: HoleMode -> MsgDoc
ppr HoleMode
HM_Sig = String -> MsgDoc
text String
"HM_Sig"
ppr HoleMode
HM_FamPat = String -> MsgDoc
text String
"HM_FamPat"
ppr HoleMode
HM_VTA = String -> MsgDoc
text String
"HM_VTA"
instance Outputable TcTyMode where
ppr :: TcTyMode -> MsgDoc
ppr (TcTyMode { mode_tyki :: TcTyMode -> TypeOrKind
mode_tyki = TypeOrKind
tyki, mode_holes :: TcTyMode -> Maybe (TcLevel, HoleMode)
mode_holes = Maybe (TcLevel, HoleMode)
hm })
= String -> MsgDoc
text String
"TcTyMode" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
braces ([MsgDoc] -> MsgDoc
sep [ TypeOrKind -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TypeOrKind
tyki MsgDoc -> MsgDoc -> MsgDoc
<> MsgDoc
comma
, Maybe (TcLevel, HoleMode) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Maybe (TcLevel, HoleMode)
hm ])
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 span 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
$
TcTyMode -> HsType GhcRn -> TcM (Type, Type)
tc_infer_hs_type TcTyMode
mode HsType GhcRn
ty
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 =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
hs_ty Type
ty Type
k Type
ek }
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 HsType GhcRn
ty
| Just (LHsType GhcRn
hs_fun_ty, HsTyPats GhcRn
hs_args) <- HsType GhcRn -> Maybe (LHsType GhcRn, HsTyPats GhcRn)
splitHsAppTys HsType GhcRn
ty
= do { (Type
fun_ty, Type
_ki) <- TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tcInferTyAppHead TcTyMode
mode LHsType GhcRn
hs_fun_ty
; TcTyMode
-> LHsType GhcRn -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
tcInferTyApps TcTyMode
mode LHsType GhcRn
hs_fun_ty Type
fun_ty HsTyPats GhcRn
hs_args }
tc_infer_hs_type TcTyMode
mode (HsKindSig XKindSig GhcRn
_ LHsType GhcRn
ty LHsType GhcRn
sig)
= do { let mode' :: TcTyMode
mode' = TcTyMode
mode { mode_tyki :: TypeOrKind
mode_tyki = TypeOrKind
KindLevel }
; Type
sig' <- TcTyMode -> UserTypeCtxt -> LHsType GhcRn -> TcM Type
tc_lhs_kind_sig TcTyMode
mode' UserTypeCtxt
KindSigCtxt LHsType GhcRn
sig
; String -> MsgDoc -> TcM ()
traceTc String
"tc_infer_hs_type:sig" (GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
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 TcLclEnv
env <- TcRnIf TcGblEnv TcLclEnv TcLclEnv
forall gbl lcl. TcRnIf gbl lcl lcl
getLclEnv
let subst_prs :: [(Unique, TcTyVar)]
subst_prs :: [(Unique, TcTyVar)]
subst_prs = [ (Name -> Unique
forall a. Uniquable a => a -> Unique
getUnique Name
nm, TcTyVar
tv)
| ATyVar Name
nm TcTyVar
tv <- NameEnv TcTyThing -> [TcTyThing]
forall a. NameEnv a -> [a]
nameEnvElts (TcLclEnv -> NameEnv TcTyThing
tcl_env TcLclEnv
env) ]
subst :: TCvSubst
subst = InScopeSet -> TvSubstEnv -> TCvSubst
mkTvSubst
(VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [TcTyVar] -> VarSet
mkVarSet ([TcTyVar] -> VarSet) -> [TcTyVar] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Unique, TcTyVar) -> TcTyVar) -> [(Unique, TcTyVar)] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Unique, TcTyVar) -> TcTyVar
forall a b. (a, b) -> b
snd [(Unique, TcTyVar)]
subst_prs)
([(Unique, Type)] -> TvSubstEnv
forall elt key. [(Unique, elt)] -> UniqFM key elt
listToUFM_Directly ([(Unique, Type)] -> TvSubstEnv) -> [(Unique, Type)] -> TvSubstEnv
forall a b. (a -> b) -> a -> b
$ ((Unique, TcTyVar) -> (Unique, Type))
-> [(Unique, TcTyVar)] -> [(Unique, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((TcTyVar -> Type) -> (Unique, TcTyVar) -> (Unique, Type)
forall a b c. (a -> b) -> (c, a) -> (c, b)
liftSnd TcTyVar -> Type
mkTyVarTy) [(Unique, TcTyVar)]
subst_prs)
ty' :: Type
ty' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst 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)
| [GenLocated SrcSpan (HsType GhcRn)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GenLocated SrcSpan (HsType GhcRn)]
[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) }
tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
tcLHsType :: LHsType GhcRn -> Type -> TcM Type
tcLHsType LHsType GhcRn
hs_ty Type
exp_kind
= TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type (TypeOrKind -> TcTyMode
mkMode TypeOrKind
TypeLevel) LHsType GhcRn
hs_ty Type
exp_kind
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode (L span 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_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
_ HsArrow GhcRn
mult LHsType GhcRn
ty1 LHsType GhcRn
ty2) Type
exp_kind
= TcTyMode
-> HsArrow GhcRn
-> LHsType GhcRn
-> LHsType GhcRn
-> Type
-> TcM Type
tc_fun_type TcTyMode
mode HsArrow GhcRn
mult LHsType GhcRn
ty1 LHsType GhcRn
ty2 Type
exp_kind
tc_hs_type TcTyMode
mode (HsOpTy XOpTy GhcRn
_ LHsType GhcRn
ty1 (L _ op) LHsType GhcRn
ty2) Type
exp_kind
| Name
op Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey
= TcTyMode
-> HsArrow GhcRn
-> LHsType GhcRn
-> LHsType GhcRn
-> Type
-> TcM Type
tc_fun_type TcTyMode
mode (IsUnicodeSyntax -> HsArrow GhcRn
forall pass. IsUnicodeSyntax -> HsArrow pass
HsUnrestrictedArrow IsUnicodeSyntax
NormalSyntax) LHsType GhcRn
ty1 LHsType GhcRn
ty2 Type
exp_kind
tc_hs_type TcTyMode
mode forall :: HsType GhcRn
forall@(HsForAllTy { hst_tele :: forall pass. HsType pass -> HsForAllTelescope pass
hst_tele = HsForAllTelescope GhcRn
tele, hst_body :: forall pass. HsType pass -> LHsType pass
hst_body = LHsType GhcRn
ty }) Type
exp_kind
= do { (TcLevel
tclvl, WantedConstraints
wanted, ([TcTyVarBinder]
tv_bndrs, Type
ty'))
<- TcM ([TcTyVarBinder], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVarBinder], Type))
forall a. TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndCaptureConstraints (TcM ([TcTyVarBinder], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVarBinder], Type)))
-> TcM ([TcTyVarBinder], Type)
-> TcM (TcLevel, WantedConstraints, ([TcTyVarBinder], Type))
forall a b. (a -> b) -> a -> b
$
TcTyMode
-> HsForAllTelescope GhcRn
-> TcM Type
-> TcM ([TcTyVarBinder], Type)
forall a.
TcTyMode
-> HsForAllTelescope GhcRn -> TcM a -> TcM ([TcTyVarBinder], a)
bindExplicitTKTele_Skol_M TcTyMode
mode HsForAllTelescope GhcRn
tele (TcM Type -> TcM ([TcTyVarBinder], Type))
-> TcM Type -> TcM ([TcTyVarBinder], 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 skol_info :: SkolemInfo
skol_info = MsgDoc -> MsgDoc -> SkolemInfo
ForAllSkol (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
forall) (MsgDoc -> SkolemInfo) -> MsgDoc -> SkolemInfo
forall a b. (a -> b) -> a -> b
$ [MsgDoc] -> MsgDoc
sep ([MsgDoc] -> MsgDoc) -> [MsgDoc] -> MsgDoc
forall a b. (a -> b) -> a -> b
$ case HsForAllTelescope GhcRn
tele of
HsForAllVis { hsf_vis_bndrs :: forall pass. HsForAllTelescope pass -> [LHsTyVarBndr () pass]
hsf_vis_bndrs = [LHsTyVarBndr () GhcRn]
hs_tvs } ->
(Located (HsTyVarBndr () GhcRn) -> MsgDoc)
-> [Located (HsTyVarBndr () GhcRn)] -> [MsgDoc]
forall a b. (a -> b) -> [a] -> [b]
map Located (HsTyVarBndr () GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Located (HsTyVarBndr () GhcRn)]
[LHsTyVarBndr () GhcRn]
hs_tvs
HsForAllInvis { hsf_invis_bndrs :: forall pass.
HsForAllTelescope pass -> [LHsTyVarBndr Specificity pass]
hsf_invis_bndrs = [LHsTyVarBndr Specificity GhcRn]
hs_tvs } ->
(Located (HsTyVarBndr Specificity GhcRn) -> MsgDoc)
-> [Located (HsTyVarBndr Specificity GhcRn)] -> [MsgDoc]
forall a b. (a -> b) -> [a] -> [b]
map Located (HsTyVarBndr Specificity GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Located (HsTyVarBndr Specificity GhcRn)]
[LHsTyVarBndr Specificity GhcRn]
hs_tvs
skol_tvs :: [TcTyVar]
skol_tvs = [TcTyVarBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcTyVarBinder]
tv_bndrs
; Implication
implic <- SkolemInfo
-> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfo
skol_info [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; Implication -> TcM ()
emitImplication Implication
implic
; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVarBinder] -> Type -> Type
mkForAllTys [TcTyVarBinder]
tv_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
rn_ty }) Type
exp_kind
| [GenLocated SrcSpan (HsType GhcRn)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (GenLocated SrcSpan [GenLocated SrcSpan (HsType GhcRn)]
-> [GenLocated SrcSpan (HsType GhcRn)]
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan [GenLocated SrcSpan (HsType GhcRn)]
LHsContext GhcRn
ctxt)
= TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
rn_ty Type
exp_kind
| Type -> Bool
tcIsConstraintKind Type
exp_kind
= do { [Type]
ctxt' <- TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context TcTyMode
mode LHsContext GhcRn
ctxt
; Type
ty' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
rn_ty Type
constraintKind
; Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type -> Type
mkPhiTy [Type]
ctxt' Type
ty') }
| Bool
otherwise
= do { [Type]
ctxt' <- TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context TcTyMode
mode LHsContext GhcRn
ctxt
; Type
ek <- TcM Type
newOpenTypeKind
; Type
ty' <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
rn_ty Type
ek
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind (GenLocated SrcSpan (HsType GhcRn) -> HsType GhcRn
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
rn_ty) ([Type] -> Type -> Type
mkPhiTy [Type]
ctxt' Type
ty')
Type
liftedTypeKind Type
exp_kind }
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 =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind 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" ([GenLocated SrcSpan (HsType GhcRn)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [GenLocated SrcSpan (HsType GhcRn)]
[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" ([GenLocated SrcSpan (HsType GhcRn)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
hs_tys)
; ([Type]
tys, [Type]
kinds) <- (GenLocated SrcSpan (HsType GhcRn) -> TcM (Type, Type))
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType GhcRn)]
[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 =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
hs_ty Type
ty Type
kind Type
arg_kind
| ((L SrcSpan
loc HsType GhcRn
hs_ty),Type
ty,Type
kind) <- [GenLocated SrcSpan (HsType GhcRn)]
-> [Type]
-> [Type]
-> [(GenLocated SrcSpan (HsType GhcRn), Type, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
hs_tys [Type]
tys [Type]
kinds ]
; HsType GhcRn -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple HsType GhcRn
rn_ty 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
HsUnboxedTuple [LHsType GhcRn]
tys) Type
exp_kind
= HsType GhcRn
-> TcTyMode -> TupleSort -> [LHsType GhcRn] -> Type -> TcM Type
tc_tuple HsType GhcRn
rn_ty TcTyMode
mode TupleSort
UnboxedTuple [LHsType GhcRn]
tys Type
exp_kind
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 = [GenLocated SrcSpan (HsType GhcRn)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
hs_tys
; [Type]
arg_kinds <- (GenLocated SrcSpan (HsType GhcRn) -> TcM Type)
-> [GenLocated SrcSpan (HsType GhcRn)] -> TcM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\GenLocated SrcSpan (HsType GhcRn)
_ -> TcM Type
newOpenTypeKind) [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
hs_tys
; [Type]
tau_tys <- (GenLocated SrcSpan (HsType GhcRn) -> Type -> TcM Type)
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType GhcRn)]
[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
sum_ty :: Type
sum_ty = TyCon -> [Type] -> Type
mkTyConApp (Int -> TyCon
sumTyCon Int
arity) [Type]
arg_tys
sum_kind :: Type
sum_kind = [Type] -> Type
unboxedSumKind [Type]
arg_reps
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
rn_ty Type
sum_ty Type
sum_kind 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 <- (GenLocated SrcSpan (HsType GhcRn) -> TcM (Type, Type))
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType GhcRn)]
[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 =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind 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 <- (GenLocated SrcSpan (HsType GhcRn) -> Type -> TcM Type)
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType GhcRn)]
[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
; Int -> TcM ()
checkTupSize Int
arity
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind 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 = [GenLocated SrcSpan (HsType GhcRn)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
tys
tc_hs_type TcTyMode
mode rn_ty :: HsType GhcRn
rn_ty@(HsIParamTy XIParamTy GhcRn
_ (L _ n) LHsType GhcRn
ty) Type
exp_kind
= do { MASSERT( isTypeLevel (mode_tyki 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 =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
rn_ty (Class -> [Type] -> Type
mkClassPred Class
ipClass [Type
n',Type
ty'])
Type
constraintKind Type
exp_kind }
tc_hs_type TcTyMode
_ rn_ty :: HsType GhcRn
rn_ty@(HsStarTy XStarTy GhcRn
_ Bool
_) Type
exp_kind
= HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
rn_ty Type
liftedTypeKind Type
liftedTypeKind Type
exp_kind
tc_hs_type TcTyMode
_ rn_ty :: HsType GhcRn
rn_ty@(HsTyLit XTyLit GhcRn
_ (HsNumTy SourceText
_ Integer
n)) Type
exp_kind
= do { TyCon -> TcM ()
checkWiredInTyCon TyCon
naturalTyCon
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
rn_ty (Integer -> Type
mkNumLitTy Integer
n) Type
naturalTy Type
exp_kind }
tc_hs_type TcTyMode
_ rn_ty :: HsType GhcRn
rn_ty@(HsTyLit XTyLit GhcRn
_ (HsStrTy SourceText
_ FastString
s)) Type
exp_kind
= do { TyCon -> TcM ()
checkWiredInTyCon TyCon
typeSymbolKindCon
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind 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 ty :: HsType GhcRn
ty@(HsWildCardTy XWildCardTy GhcRn
_) Type
ek = TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcAnonWildCardOcc TcTyMode
mode HsType GhcRn
ty Type
ek
tc_mult :: TcTyMode -> HsArrow GhcRn -> TcM Mult
tc_mult :: TcTyMode -> HsArrow GhcRn -> TcM Type
tc_mult TcTyMode
mode HsArrow GhcRn
ty = TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode (HsArrow GhcRn -> LHsType GhcRn
arrowToHsType HsArrow GhcRn
ty) Type
multiplicityTy
tc_fun_type :: TcTyMode -> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> TcKind
-> TcM TcType
tc_fun_type :: TcTyMode
-> HsArrow GhcRn
-> LHsType GhcRn
-> LHsType GhcRn
-> Type
-> TcM Type
tc_fun_type TcTyMode
mode HsArrow GhcRn
mult LHsType GhcRn
ty1 LHsType GhcRn
ty2 Type
exp_kind = case TcTyMode -> TypeOrKind
mode_tyki 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
; Type
mult' <- TcTyMode -> HsArrow GhcRn -> TcM Type
tc_mult TcTyMode
mode HsArrow GhcRn
mult
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind (XFunTy GhcRn
-> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn
forall pass.
XFunTy pass
-> HsArrow pass -> LHsType pass -> LHsType pass -> HsType pass
HsFunTy NoExtField
XFunTy GhcRn
noExtField HsArrow GhcRn
mult LHsType GhcRn
ty1 LHsType GhcRn
ty2) (Type -> Type -> Type -> Type
mkVisFunTy Type
mult' 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
; Type
mult' <- TcTyMode -> HsArrow GhcRn -> TcM Type
tc_mult TcTyMode
mode HsArrow GhcRn
mult
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind (XFunTy GhcRn
-> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> HsType GhcRn
forall pass.
XFunTy pass
-> HsArrow pass -> LHsType pass -> LHsType pass -> HsType pass
HsFunTy NoExtField
XFunTy GhcRn
noExtField HsArrow GhcRn
mult LHsType GhcRn
ty1 LHsType GhcRn
ty2) (Type -> Type -> Type -> Type
mkVisFunTy Type
mult' Type
ty1' Type
ty2')
Type
liftedTypeKind Type
exp_kind }
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]
replicate Int
arity Type
liftedTypeKind)
TupleSort
UnboxedTuple -> Int -> TcM Type -> TcM [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
arity TcM Type
newOpenTypeKind
TupleSort
ConstraintTuple -> [Type] -> TcM [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Type -> [Type]
forall a. Int -> a -> [a]
replicate Int
arity Type
constraintKind)
; [Type]
tau_tys <- (GenLocated SrcSpan (HsType GhcRn) -> Type -> TcM Type)
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
tys [Type]
arg_kinds
; HsType GhcRn -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple HsType GhcRn
rn_ty TupleSort
tup_sort [Type]
tau_tys [Type]
arg_kinds Type
exp_kind }
where
arity :: Int
arity = [GenLocated SrcSpan (HsType GhcRn)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
tys
finish_tuple :: HsType GhcRn
-> TupleSort
-> [TcType]
-> [TcKind]
-> TcKind
-> TcM TcType
finish_tuple :: HsType GhcRn -> TupleSort -> [Type] -> [Type] -> Type -> TcM Type
finish_tuple HsType GhcRn
rn_ty TupleSort
tup_sort [Type]
tau_tys [Type]
tau_kinds Type
exp_kind = do
String -> MsgDoc -> TcM ()
traceTc String
"finish_tuple" (TupleSort -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TupleSort
tup_sort 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)
case TupleSort
tup_sort of
TupleSort
ConstraintTuple
| [Type
tau_ty] <- [Type]
tau_tys
-> Type -> Type -> TcM Type
check_expected_kind Type
tau_ty Type
constraintKind
| Bool
otherwise
-> do let tycon :: TyCon
tycon = Int -> TyCon
cTupleTyCon Int
arity
Int -> TcM ()
checkCTupSize Int
arity
Type -> Type -> TcM Type
check_expected_kind (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
tau_tys) Type
constraintKind
TupleSort
BoxedTuple -> do
let tycon :: TyCon
tycon = Boxity -> Int -> TyCon
tupleTyCon Boxity
Boxed Int
arity
Int -> TcM ()
checkTupSize Int
arity
TyCon -> TcM ()
checkWiredInTyCon TyCon
tycon
Type -> Type -> TcM Type
check_expected_kind (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
tau_tys) Type
liftedTypeKind
TupleSort
UnboxedTuple -> do
let tycon :: TyCon
tycon = Boxity -> Int -> TyCon
tupleTyCon Boxity
Unboxed Int
arity
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
arg_tys :: [Type]
arg_tys = [Type]
tau_reps [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
tau_tys
res_kind :: Type
res_kind = [Type] -> Type
unboxedTupleKind [Type]
tau_reps
Int -> TcM ()
checkTupSize Int
arity
Type -> Type -> TcM Type
check_expected_kind (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
arg_tys) Type
res_kind
where
arity :: Int
arity = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tau_tys
check_expected_kind :: Type -> Type -> TcM Type
check_expected_kind Type
ty Type
act_kind =
HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
rn_ty Type
ty Type
act_kind Type
exp_kind
splitHsAppTys :: HsType GhcRn -> Maybe (LHsType GhcRn, [LHsTypeArg GhcRn])
splitHsAppTys :: HsType GhcRn -> Maybe (LHsType GhcRn, HsTyPats GhcRn)
splitHsAppTys HsType GhcRn
hs_ty
| HsType GhcRn -> Bool
is_app HsType GhcRn
hs_ty = (GenLocated SrcSpan (HsType GhcRn),
[HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))])
-> Maybe
(GenLocated SrcSpan (HsType GhcRn),
[HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))])
forall a. a -> Maybe a
Just (GenLocated SrcSpan (HsType GhcRn)
-> [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> (GenLocated SrcSpan (HsType GhcRn),
[HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))])
forall pass.
(XTyVar pass ~ NoExtField, XAppKindTy pass ~ SrcSpan,
XRec pass (HsType pass) ~ GenLocated SrcSpan (HsType pass),
XRec pass (IdP pass) ~ GenLocated SrcSpan (IdP pass)) =>
GenLocated SrcSpan (HsType pass)
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> (GenLocated SrcSpan (HsType pass),
[HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))])
go (HsType GhcRn -> GenLocated SrcSpan (HsType GhcRn)
forall e. e -> Located e
noLoc HsType GhcRn
hs_ty) [])
| Bool
otherwise = Maybe (LHsType GhcRn, HsTyPats GhcRn)
forall a. Maybe a
Nothing
where
is_app :: HsType GhcRn -> Bool
is_app :: HsType GhcRn -> Bool
is_app (HsAppKindTy {}) = Bool
True
is_app (HsAppTy {}) = Bool
True
is_app (HsOpTy XOpTy GhcRn
_ LHsType GhcRn
_ (L _ op) LHsType GhcRn
_) = Bool -> Bool
not (Name
op Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey)
is_app (HsTyVar {}) = Bool
True
is_app (HsParTy XParTy GhcRn
_ (L _ ty)) = HsType GhcRn -> Bool
is_app HsType GhcRn
ty
is_app HsType GhcRn
_ = Bool
False
go :: GenLocated SrcSpan (HsType pass)
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> (GenLocated SrcSpan (HsType pass),
[HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))])
go (L SrcSpan
_ (HsAppTy XAppTy pass
_ XRec pass (HsType pass)
f XRec pass (HsType pass)
a)) [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as = GenLocated SrcSpan (HsType pass)
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> (GenLocated SrcSpan (HsType pass),
[HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))])
go GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
f (GenLocated SrcSpan (HsType pass)
-> HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
forall tm ty. tm -> HsArg tm ty
HsValArg GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
a HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
forall a. a -> [a] -> [a]
: [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as)
go (L SrcSpan
_ (HsAppKindTy XAppKindTy pass
l XRec pass (HsType pass)
ty XRec pass (HsType pass)
k)) [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as = GenLocated SrcSpan (HsType pass)
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> (GenLocated SrcSpan (HsType pass),
[HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))])
go GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
ty (SrcSpan
-> GenLocated SrcSpan (HsType pass)
-> HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
forall tm ty. SrcSpan -> ty -> HsArg tm ty
HsTypeArg SrcSpan
XAppKindTy pass
l GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
k HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
forall a. a -> [a] -> [a]
: [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as)
go (L SrcSpan
sp (HsParTy XParTy pass
_ XRec pass (HsType pass)
f)) [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as = GenLocated SrcSpan (HsType pass)
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> (GenLocated SrcSpan (HsType pass),
[HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))])
go GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
f (SrcSpan
-> HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
forall tm ty. SrcSpan -> HsArg tm ty
HsArgPar SrcSpan
sp HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
forall a. a -> [a] -> [a]
: [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as)
go (L SrcSpan
_ (HsOpTy XOpTy pass
_ XRec pass (HsType pass)
l op :: XRec pass (IdP pass)
op@(L sp _) XRec pass (HsType pass)
r)) [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as
= ( SrcSpan -> HsType pass -> GenLocated SrcSpan (HsType pass)
forall l e. l -> e -> GenLocated l e
L SrcSpan
sp (XTyVar pass -> PromotionFlag -> XRec pass (IdP pass) -> HsType pass
forall pass.
XTyVar pass -> PromotionFlag -> LIdP pass -> HsType pass
HsTyVar NoExtField
XTyVar pass
noExtField PromotionFlag
NotPromoted XRec pass (IdP pass)
op)
, GenLocated SrcSpan (HsType pass)
-> HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
forall tm ty. tm -> HsArg tm ty
HsValArg GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
l HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
forall a. a -> [a] -> [a]
: GenLocated SrcSpan (HsType pass)
-> HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
forall tm ty. tm -> HsArg tm ty
HsValArg GenLocated SrcSpan (HsType pass)
XRec pass (HsType pass)
r HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
-> [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
forall a. a -> [a] -> [a]
: [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as )
go GenLocated SrcSpan (HsType pass)
f [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as = (GenLocated SrcSpan (HsType pass)
f, [HsArg
(GenLocated SrcSpan (HsType pass))
(GenLocated SrcSpan (HsType pass))]
as)
tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tcInferTyAppHead TcTyMode
mode (L _ (HsTyVar _ _ (L _ tv)))
= TcTyMode -> Name -> TcM (Type, Type)
tcTyVar TcTyMode
mode Name
tv
tcInferTyAppHead TcTyMode
mode LHsType GhcRn
ty
= TcTyMode -> LHsType GhcRn -> TcM (Type, Type)
tc_infer_lhs_type TcTyMode
mode LHsType GhcRn
ty
tcInferTyApps, tcInferTyApps_nosat
:: TcTyMode
-> LHsType GhcRn
-> TcType
-> [LHsTypeArg GhcRn]
-> TcM (TcType, TcKind)
tcInferTyApps :: TcTyMode
-> LHsType GhcRn -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
tcInferTyApps TcTyMode
mode LHsType GhcRn
hs_ty Type
fun HsTyPats GhcRn
hs_args
= do { (Type
f_args, Type
res_k) <- TcTyMode
-> LHsType GhcRn -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
tcInferTyApps_nosat TcTyMode
mode LHsType GhcRn
hs_ty Type
fun HsTyPats GhcRn
hs_args
; Type -> Type -> TcM (Type, Type)
saturateFamApp Type
f_args Type
res_k }
tcInferTyApps_nosat :: TcTyMode
-> LHsType GhcRn -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
tcInferTyApps_nosat TcTyMode
mode LHsType GhcRn
orig_hs_ty Type
fun HsTyPats GhcRn
orig_hs_args
= do { String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps {" (GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
orig_hs_ty MsgDoc -> MsgDoc -> MsgDoc
$$ [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
orig_hs_args)
; (Type
f_args, Type
res_k) <- Int
-> Type
-> [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> TcM (Type, Type)
go_init Int
1 Type
fun [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
orig_hs_args
; String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps }" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
f_args MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_k)
; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
f_args, Type
res_k) }
where
go_init :: Int
-> Type
-> [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> TcM (Type, Type)
go_init Int
n Type
fun [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
all_args
= Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go Int
n Type
fun TCvSubst
empty_subst Type
fun_ki [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
all_args
where
fun_ki :: Type
fun_ki = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun
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
go :: Int
-> TcType
-> TCvSubst
-> TcKind
-> [LHsTypeArg GhcRn]
-> TcM (TcType, TcKind)
go :: Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go Int
n Type
fun TCvSubst
subst Type
fun_ki HsTyPats GhcRn
all_args = case ([HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
all_args, Type -> Maybe (TyBinder, Type)
tcSplitPiTy_maybe Type
fun_ki) of
([], Maybe (TyBinder, Type)
_) -> (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
fun, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
fun_ki)
(HsArgPar SrcSpan
_ : [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
args, Maybe (TyBinder, Type)
_) -> Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go Int
n Type
fun TCvSubst
subst Type
fun_ki [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
args
(HsTypeArg SrcSpan
_ GenLocated SrcSpan (HsType GhcRn)
hs_ki_arg : [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
hs_args, Just (TyBinder
ki_binder, Type
inner_ki)) ->
case TyBinder
ki_binder of
Named (Bndr TcTyVar
_ ArgFlag
Inferred) -> TyBinder -> Type -> TcM (Type, Type)
instantiate TyBinder
ki_binder Type
inner_ki
Anon AnonArgFlag
InvisArg Scaled Type
_ -> TyBinder -> Type -> TcM (Type, Type)
instantiate TyBinder
ki_binder Type
inner_ki
Named (Bndr TcTyVar
_ ArgFlag
Specified) ->
do { String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps (vis kind app)"
([MsgDoc] -> MsgDoc
vcat [ TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder, GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
hs_ki_arg
, 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
substTy TCvSubst
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TyBinder -> Type
tyBinderType TyBinder
ki_binder
; TcTyMode
arg_mode <- TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
KindLevel HoleMode
HM_VTA
; Type
ki_arg <- MsgDoc -> TcM Type -> TcM Type
forall a. MsgDoc -> TcM a -> TcM a
addErrCtxt (GenLocated SrcSpan (HsType GhcRn)
-> GenLocated SrcSpan (HsType GhcRn) -> Int -> MsgDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> MsgDoc
funAppCtxt GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
orig_hs_ty GenLocated SrcSpan (HsType GhcRn)
hs_ki_arg 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
arg_mode GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_ki_arg Type
exp_kind
; String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps (vis kind app)" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind)
; (TCvSubst
subst', Type
fun') <- TCvSubst -> Type -> TyBinder -> Type -> TcM (TCvSubst, Type)
mkAppTyM TCvSubst
subst Type
fun TyBinder
ki_binder Type
ki_arg
; Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Type
fun' TCvSubst
subst' Type
inner_ki [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
hs_args }
TyBinder
_ -> GenLocated SrcSpan (HsType GhcRn) -> Type -> TcM (Type, Type)
forall a a a. (Outputable a, Outputable a) => a -> a -> TcRn a
ty_app_err GenLocated SrcSpan (HsType GhcRn)
hs_ki_arg (Type -> TcM (Type, Type)) -> Type -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$ HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
fun_ki
(HsTypeArg SrcSpan
_ GenLocated SrcSpan (HsType GhcRn)
ki_arg : [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
_, Maybe (TyBinder, Type)
Nothing) -> TcM (Type, Type) -> TcM (Type, Type)
try_again_after_substing_or (TcM (Type, Type) -> TcM (Type, Type))
-> TcM (Type, Type) -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$
GenLocated SrcSpan (HsType GhcRn) -> Type -> TcM (Type, Type)
forall a a a. (Outputable a, Outputable a) => a -> a -> TcRn a
ty_app_err GenLocated SrcSpan (HsType GhcRn)
ki_arg Type
substed_fun_ki
(HsValArg GenLocated SrcSpan (HsType GhcRn)
arg : [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
args, Just (TyBinder
ki_binder, Type
inner_ki))
| TyBinder -> Bool
isInvisibleBinder TyBinder
ki_binder
-> TyBinder -> Type -> TcM (Type, Type)
instantiate TyBinder
ki_binder Type
inner_ki
| Bool
otherwise
-> do { String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps (vis normal app)"
([MsgDoc] -> MsgDoc
vcat [ TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder
, GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
arg
, 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
substTy 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 (GenLocated SrcSpan (HsType GhcRn)
-> GenLocated SrcSpan (HsType GhcRn) -> Int -> MsgDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> MsgDoc
funAppCtxt GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
orig_hs_ty GenLocated SrcSpan (HsType GhcRn)
arg 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 GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
arg Type
exp_kind
; String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps (vis normal app) 2" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind)
; (TCvSubst
subst', Type
fun') <- TCvSubst -> Type -> TyBinder -> Type -> TcM (TCvSubst, Type)
mkAppTyM TCvSubst
subst Type
fun TyBinder
ki_binder Type
arg'
; Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Type
fun' TCvSubst
subst' Type
inner_ki [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
args }
(HsValArg GenLocated SrcSpan (HsType GhcRn)
_ : [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
_, Maybe (TyBinder, Type)
Nothing)
-> TcM (Type, Type) -> TcM (Type, Type)
try_again_after_substing_or (TcM (Type, Type) -> TcM (Type, Type))
-> TcM (Type, Type) -> TcM (Type, Type)
forall a b. (a -> b) -> a -> b
$
do { let arrows_needed :: Int
arrows_needed = [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> Int
forall tm ty. [HsArg tm ty] -> Int
n_initial_val_args [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
all_args
; Coercion
co <- GenLocated SrcSpan (HsType GhcRn) -> Int -> Type -> TcM Coercion
forall fun. Outputable fun => fun -> Int -> Type -> TcM Coercion
matchExpectedFunKind GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_ty Int
arrows_needed Type
substed_fun_ki
; Type
fun' <- Type -> TcM Type
zonkTcType (Type
fun Type -> Coercion -> Type
`mkTcCastTy` Coercion
co)
; String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps (no binder)" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[MsgDoc] -> MsgDoc
vcat [ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
fun MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
fun_ki
, Int -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Int
arrows_needed
, Coercion -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Coercion
co
, Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
fun' MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc
dcolon MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun')]
; Int
-> Type
-> [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> TcM (Type, Type)
go_init Int
n Type
fun' [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
all_args }
where
instantiate :: TyBinder -> Type -> TcM (Type, Type)
instantiate TyBinder
ki_binder Type
inner_ki
= do { String -> MsgDoc -> TcM ()
traceTc String
"tcInferTyApps (need to instantiate)"
([MsgDoc] -> MsgDoc
vcat [ TyBinder -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TyBinder
ki_binder, TCvSubst -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TCvSubst
subst])
; (TCvSubst
subst', Type
arg') <- TCvSubst -> TyBinder -> TcM (TCvSubst, Type)
tcInstInvisibleTyBinder TCvSubst
subst TyBinder
ki_binder
; Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go Int
n (Type -> Type -> Type
mkAppTy Type
fun Type
arg') TCvSubst
subst' Type
inner_ki HsTyPats GhcRn
all_args }
try_again_after_substing_or :: TcM (Type, Type) -> TcM (Type, Type)
try_again_after_substing_or TcM (Type, Type)
fallthrough
| Bool -> Bool
not (TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst)
= Int
-> Type -> TCvSubst -> Type -> HsTyPats GhcRn -> TcM (Type, Type)
go Int
n Type
fun TCvSubst
zapped_subst Type
substed_fun_ki HsTyPats GhcRn
all_args
| Bool
otherwise
= TcM (Type, Type)
fallthrough
zapped_subst :: TCvSubst
zapped_subst = TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst
substed_fun_ki :: Type
substed_fun_ki = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
fun_ki
hs_ty :: LHsType GhcRn
hs_ty = LHsType GhcRn -> HsTyPats GhcRn -> LHsType GhcRn
appTypeToArg LHsType GhcRn
orig_hs_ty (Int
-> [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
-> [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
forall a. Int -> [a] -> [a]
take (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [HsArg
(GenLocated SrcSpan (HsType GhcRn))
(GenLocated SrcSpan (HsType GhcRn))]
HsTyPats GhcRn
orig_hs_args)
n_initial_val_args :: [HsArg tm ty] -> Arity
n_initial_val_args :: [HsArg tm ty] -> Int
n_initial_val_args (HsValArg {} : [HsArg tm ty]
args) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [HsArg tm ty] -> Int
forall tm ty. [HsArg tm ty] -> Int
n_initial_val_args [HsArg tm ty]
args
n_initial_val_args (HsArgPar {} : [HsArg tm ty]
args) = [HsArg tm ty] -> Int
forall tm ty. [HsArg tm ty] -> Int
n_initial_val_args [HsArg tm ty]
args
n_initial_val_args [HsArg tm ty]
_ = Int
0
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)
mkAppTyM :: TCvSubst
-> TcType -> TyCoBinder
-> TcType
-> TcM (TCvSubst, TcType)
mkAppTyM :: TCvSubst -> Type -> TyBinder -> Type -> TcM (TCvSubst, Type)
mkAppTyM TCvSubst
subst Type
fun TyBinder
ki_binder Type
arg
|
TyConApp TyCon
tc [Type]
args <- Type
fun
, TyCon -> Bool
isTypeSynonymTyCon TyCon
tc
, [Type]
args [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` (TyCon -> Int
tyConArity TyCon
tc Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
, (TcTyVar -> Bool) -> [TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcTyVar -> Bool
isTrickyTvBinder (TyCon -> [TcTyVar]
tyConTyVars TyCon
tc)
= do { Type
arg' <- Type -> TcM Type
zonkTcType Type
arg
; [Type]
args' <- [Type] -> TcM [Type]
zonkTcTypes [Type]
args
; let subst' :: TCvSubst
subst' = case TyBinder
ki_binder of
Anon {} -> TCvSubst
subst
Named (Bndr TcTyVar
tv ArgFlag
_) -> TCvSubst -> TcTyVar -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst TcTyVar
tv Type
arg'
; (TCvSubst, Type) -> TcM (TCvSubst, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst', TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ([Type]
args' [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
arg'])) }
mkAppTyM TCvSubst
subst Type
fun (Anon {}) Type
arg
= (TCvSubst, Type) -> TcM (TCvSubst, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst
subst, Type -> Type -> Type
mk_app_ty Type
fun Type
arg)
mkAppTyM TCvSubst
subst Type
fun (Named (Bndr TcTyVar
tv ArgFlag
_)) Type
arg
= do { Type
arg' <- if TcTyVar -> Bool
isTrickyTvBinder TcTyVar
tv
then
Type -> TcM Type
zonkTcType Type
arg
else Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
arg
; (TCvSubst, Type) -> TcM (TCvSubst, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ( TCvSubst -> TcTyVar -> Type -> TCvSubst
extendTvSubstAndInScope TCvSubst
subst TcTyVar
tv Type
arg'
, Type -> Type -> Type
mk_app_ty Type
fun Type
arg' ) }
mk_app_ty :: TcType -> TcType -> TcType
mk_app_ty :: Type -> Type -> Type
mk_app_ty Type
fun Type
arg
= ASSERT2( isPiTy fun_kind
, ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg )
Type -> Type -> Type
mkAppTy Type
fun Type
arg
where
fun_kind :: Type
fun_kind = HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind Type
fun
isTrickyTvBinder :: TcTyVar -> Bool
isTrickyTvBinder :: TcTyVar -> Bool
isTrickyTvBinder TcTyVar
tv = Type -> Bool
isPiTy (TcTyVar -> Type
tyVarKind TcTyVar
tv)
saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
saturateFamApp :: Type -> Type -> TcM (Type, Type)
saturateFamApp Type
ty Type
kind
| Just (TyCon
tc, [Type]
args) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
ty
, TyCon -> Bool
mustBeSaturated TyCon
tc
, let n_to_inst :: Int
n_to_inst = 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
= do { ([Type]
extra_args, Type
ki') <- Int -> Type -> TcM ([Type], Type)
tcInstInvisibleTyBindersN Int
n_to_inst Type
kind
; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty Type -> [Type] -> Type
`mkTcAppTys` [Type]
extra_args, Type
ki') }
| Bool
otherwise
= (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Type
kind)
appTypeToArg :: LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
appTypeToArg :: LHsType GhcRn -> HsTyPats GhcRn -> LHsType GhcRn
appTypeToArg LHsType GhcRn
f [] = LHsType GhcRn
f
appTypeToArg LHsType GhcRn
f (HsValArg LHsType GhcRn
arg : HsTyPats GhcRn
args) = LHsType GhcRn -> HsTyPats 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) HsTyPats GhcRn
args
appTypeToArg LHsType GhcRn
f (HsArgPar SrcSpan
_ : HsTyPats GhcRn
args) = LHsType GhcRn -> HsTyPats GhcRn -> LHsType GhcRn
appTypeToArg LHsType GhcRn
f HsTyPats GhcRn
args
appTypeToArg LHsType GhcRn
f (HsTypeArg SrcSpan
l LHsType GhcRn
arg : HsTyPats GhcRn
args)
= LHsType GhcRn -> HsTyPats GhcRn -> LHsType GhcRn
appTypeToArg (XAppKindTy GhcRn -> LHsType GhcRn -> LHsType GhcRn -> LHsType GhcRn
forall (p :: Pass).
XAppKindTy (GhcPass p)
-> LHsType (GhcPass p)
-> LHsType (GhcPass p)
-> LHsType (GhcPass p)
mkHsAppKindTy SrcSpan
XAppKindTy GhcRn
l LHsType GhcRn
f LHsType GhcRn
arg) HsTyPats GhcRn
args
checkExpectedKind :: HasDebugCallStack
=> HsType GhcRn
-> TcType
-> TcKind
-> TcKind
-> TcM TcType
checkExpectedKind :: HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
hs_ty Type
ty Type
act_kind Type
exp_kind
= do { String -> MsgDoc -> TcM ()
traceTc String
"checkExpectedKind" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
ty MsgDoc -> MsgDoc -> MsgDoc
$$ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
act_kind)
; ([Type]
new_args, Type
act_kind') <- Int -> Type -> TcM ([Type], Type)
tcInstInvisibleTyBindersN 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 (HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
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 [ HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
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
"exp_kind:" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
exp_kind ]
; let res_ty :: Type
res_ty = Type
ty Type -> [Type] -> Type
`mkTcAppTys` [Type]
new_args
; if Type
act_kind' HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
exp_kind
then Type -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
res_ty
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 -> TcM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
res_ty Type -> Coercion -> Type
`mkTcCastTy` Coercion
co_k) } }
where
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
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 LHsContext GhcRn
cxt = TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context (TypeOrKind -> TcTyMode
mkMode TypeOrKind
TypeLevel) LHsContext GhcRn
cxt
tcLHsPredType :: LHsType GhcRn -> TcM PredType
tcLHsPredType :: LHsType GhcRn -> TcM Type
tcLHsPredType LHsType GhcRn
pred = TcTyMode -> LHsType GhcRn -> TcM Type
tc_lhs_pred (TypeOrKind -> TcTyMode
mkMode TypeOrKind
TypeLevel) LHsType GhcRn
pred
tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [Type]
tc_hs_context TcTyMode
mode LHsContext GhcRn
ctxt = (GenLocated SrcSpan (HsType GhcRn) -> TcM Type)
-> [GenLocated SrcSpan (HsType 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) (GenLocated SrcSpan [GenLocated SrcSpan (HsType GhcRn)]
-> [GenLocated SrcSpan (HsType GhcRn)]
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan [GenLocated SrcSpan (HsType GhcRn)]
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 -> (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar -> Type
mkTyVarTy TcTyVar
tv, TcTyVar -> Type
tyVarKind TcTyVar
tv)
ATcTyCon TyCon
tc_tc
-> do { TyCon -> TcM ()
check_tc TyCon
tc_tc
; (Type, Type) -> TcM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type
mkTyConTy TyCon
tc_tc, TyCon -> Type
tyConKind TyCon
tc_tc) }
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, [Scaled Type]
_, Type
_) = DataCon
-> ([TcTyVar], [TcTyVar], [EqSpec], [Type], [Scaled Type], Type)
dataConFullSig DataCon
dc
; String -> MsgDoc -> TcM ()
traceTc String
"tcTyVar" (DataCon -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr DataCon
dc MsgDoc -> MsgDoc -> MsgDoc
<+> [Type] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Type]
theta MsgDoc -> MsgDoc -> MsgDoc
$$ Maybe Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr ([Type] -> Maybe Type
dc_theta_illegal_constraint [Type]
theta))
; 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_tyki 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 (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
isEqPred)
addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt (L _ (HsWildCardTy _)) TcM a
thing = TcM a
thing
addTypeCtxt (L _ 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)
tcNamedWildCardBinders :: [Name]
-> ([(Name, TcTyVar)] -> TcM a)
-> TcM a
tcNamedWildCardBinders :: [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcNamedWildCardBinders [Name]
wc_names [(Name, TcTyVar)] -> TcM a
thing_inside
= do { [TcTyVar]
wcs <- (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newNamedWildTyVar [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 }
newNamedWildTyVar :: Name -> TcM TcTyVar
newNamedWildTyVar :: Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newNamedWildTyVar Name
_name
= do { Type
kind <- TcM Type
newMetaKindVar
; TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
newMetaDetails MetaInfo
TauTv
; Name
wc_name <- FastString -> TcM Name
newMetaTyVarName (String -> FastString
fsLit String
"w")
; let tyvar :: TcTyVar
tyvar = Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
wc_name Type
kind TcTyVarDetails
details
; String -> MsgDoc -> TcM ()
traceTc String
"newWildTyVar" (TcTyVar -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyVar
tyvar)
; TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tyvar }
tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcAnonWildCardOcc (TcTyMode { mode_holes :: TcTyMode -> Maybe (TcLevel, HoleMode)
mode_holes = Just (TcLevel
hole_lvl, HoleMode
hole_mode) })
HsType GhcRn
ty Type
exp_kind
= do { TcTyVarDetails
kv_details <- TcLevel -> TcM TcTyVarDetails
newTauTvDetailsAtLevel TcLevel
hole_lvl
; Name
kv_name <- FastString -> TcM Name
newMetaTyVarName (String -> FastString
fsLit String
"k")
; TcTyVarDetails
wc_details <- TcLevel -> TcM TcTyVarDetails
newTauTvDetailsAtLevel TcLevel
hole_lvl
; Name
wc_name <- FastString -> TcM Name
newMetaTyVarName (String -> FastString
fsLit String
wc_nm)
; let kv :: TcTyVar
kv = Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
kv_name Type
liftedTypeKind TcTyVarDetails
kv_details
wc_kind :: Type
wc_kind = TcTyVar -> Type
mkTyVarTy TcTyVar
kv
wc_tv :: TcTyVar
wc_tv = Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
wc_name Type
wc_kind TcTyVarDetails
wc_details
; String -> MsgDoc -> TcM ()
traceTc String
"tcAnonWildCardOcc" (TcLevel -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcLevel
hole_lvl MsgDoc -> MsgDoc -> MsgDoc
<+> Bool -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Bool
emit_holes)
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
emit_holes (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
TcTyVar -> TcM ()
emitAnonTypeHole TcTyVar
wc_tv
; HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind HsType GhcRn
ty (TcTyVar -> Type
mkTyVarTy TcTyVar
wc_tv) Type
wc_kind Type
exp_kind }
where
wc_nm :: String
wc_nm = case HoleMode
hole_mode of
HoleMode
HM_Sig -> String
"w"
HoleMode
HM_FamPat -> String
"_"
HoleMode
HM_VTA -> String
"w"
emit_holes :: Bool
emit_holes = case HoleMode
hole_mode of
HoleMode
HM_Sig -> Bool
True
HoleMode
HM_FamPat -> Bool
False
HoleMode
HM_VTA -> Bool
False
tcAnonWildCardOcc TcTyMode
mode HsType GhcRn
ty Type
_
= String -> MsgDoc -> TcM Type
forall a. HasCallStack => String -> MsgDoc -> a
pprPanic String
"tcWildCardOcc" (TcTyMode -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr TcTyMode
mode MsgDoc -> MsgDoc -> MsgDoc
$$ HsType GhcRn -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr HsType GhcRn
ty)
data InitialKindStrategy
= InitialKindCheck SAKS_or_CUSK
| InitialKindInfer
data SAKS_or_CUSK
= SAKS Kind
| CUSK
instance Outputable SAKS_or_CUSK where
ppr :: SAKS_or_CUSK -> MsgDoc
ppr (SAKS Type
k) = String -> MsgDoc
text String
"SAKS" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
k
ppr SAKS_or_CUSK
CUSK = String -> MsgDoc
text String
"CUSK"
kcDeclHeader
:: InitialKindStrategy
-> Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TcTyCon
(InitialKindCheck SAKS_or_CUSK
msig) = SAKS_or_CUSK
-> Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TyCon
kcCheckDeclHeader SAKS_or_CUSK
msig
kcDeclHeader InitialKindStrategy
InitialKindInfer = Name
-> TyConFlavour -> LHsQTyVars GhcRn -> TcM ContextKind -> TcM TyCon
kcInferDeclHeader
kcCheckDeclHeader
:: SAKS_or_CUSK
-> Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TcTyCon
(SAKS Type
sig) = Type
-> Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TyCon
kcCheckDeclHeader_sig Type
sig
kcCheckDeclHeader SAKS_or_CUSK
CUSK = Name
-> TyConFlavour -> LHsQTyVars GhcRn -> TcM ContextKind -> TcM TyCon
kcCheckDeclHeader_cusk
kcCheckDeclHeader_cusk
:: Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TcTyCon
Name
name TyConFlavour
flav
(HsQTvs { hsq_ext :: forall pass. LHsQTyVars pass -> XHsQTvs pass
hsq_ext = XHsQTvs GhcRn
kv_ns
, hsq_explicit :: forall pass. LHsQTyVars pass -> [LHsTyVarBndr () pass]
hsq_explicit = [LHsTyVarBndr () GhcRn]
hs_tvs }) TcM ContextKind
kc_res_ki
= Name -> TyConFlavour -> TcM TyCon -> TcM TyCon
forall a. Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt Name
name TyConFlavour
flav (TcM TyCon -> TcM TyCon) -> TcM TyCon -> TcM TyCon
forall a b. (a -> b) -> a -> b
$
do { (TcLevel
tclvl, WantedConstraints
wanted, ([TcTyVar]
scoped_kvs, ([TcTyVar]
tc_tvs, Type
res_kind)))
<- String
-> TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM (TcLevel, WantedConstraints, ([TcTyVar], ([TcTyVar], Type)))
forall a. String -> TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndSolveEqualitiesX String
"kcCheckDeclHeader_cusk" (TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM
(TcLevel, WantedConstraints, ([TcTyVar], ([TcTyVar], Type))))
-> TcM ([TcTyVar], ([TcTyVar], Type))
-> TcM (TcLevel, WantedConstraints, ([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]
XHsQTvs GhcRn
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
$
ContextKind -> TcM Type
newExpectedKind (ContextKind -> TcM Type) -> TcM ContextKind -> TcM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TcM ContextKind
kc_res_ki
; 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 non_tc_candidates :: [TcTyVar]
non_tc_candidates = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TcTyVar -> Bool) -> TcTyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTyVar -> Bool
isTcTyVar) (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet ([Type] -> VarSet
tyCoVarsOfTypes [Type]
all_kinds))
candidates :: CandidatesQTvs
candidates = CandidatesQTvs
candidates' { dv_kvs :: DTyVarSet
dv_kvs = CandidatesQTvs -> DTyVarSet
dv_kvs CandidatesQTvs
candidates' DTyVarSet -> [TcTyVar] -> DTyVarSet
`extendDVarSetList` [TcTyVar]
non_tc_candidates }
inf_candidates :: CandidatesQTvs
inf_candidates = CandidatesQTvs
candidates CandidatesQTvs -> [TcTyVar] -> CandidatesQTvs
`delCandidates` [TcTyVar]
spec_req_tkvs
; [TcTyVar]
inferred <- CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars CandidatesQTvs
inf_candidates
; [TcTyVar]
scoped_kvs <- (TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
zonkTyCoVarKind [TcTyVar]
scoped_kvs
; [TcTyVar]
tc_tvs <- (TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) 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
-> [TyConBinder]
-> Type
-> [(Name, TcTyVar)]
-> Bool
-> TyConFlavour
-> TyCon
mkTcTyCon Name
name [TyConBinder]
final_tc_binders Type
res_kind [(Name, TcTyVar)]
all_tv_prs
Bool
True
TyConFlavour
flav
; SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
reportUnsolvedEqualities SkolemInfo
skol_info ([TyConBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyConBinder]
final_tc_binders)
TcLevel
tclvl WantedConstraints
wanted
; TyCon -> TcM ()
checkTyConTelescope TyCon
tycon
; String -> MsgDoc -> TcM ()
traceTc String
"kcCheckDeclHeader_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]
XHsQTvs GhcRn
kv_ns
, String -> MsgDoc
text String
"hs_tvs" MsgDoc -> MsgDoc -> MsgDoc
<+> [Located (HsTyVarBndr () GhcRn)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Located (HsTyVarBndr () GhcRn)]
[LHsTyVarBndr () GhcRn]
hs_tvs
, 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 -> TcM TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tycon }
where
skol_info :: SkolemInfo
skol_info = TyConFlavour -> Name -> SkolemInfo
TyConSkol TyConFlavour
flav Name
name
ctxt_kind :: ContextKind
ctxt_kind | TyConFlavour -> Bool
tcFlavourIsOpen TyConFlavour
flav = Type -> ContextKind
TheKind Type
liftedTypeKind
| Bool
otherwise = ContextKind
AnyKind
kcInferDeclHeader
:: Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TcTyCon
Name
name TyConFlavour
flav
(HsQTvs { hsq_ext :: forall pass. LHsQTyVars pass -> XHsQTvs pass
hsq_ext = XHsQTvs GhcRn
kv_ns
, hsq_explicit :: forall pass. LHsQTyVars pass -> [LHsTyVarBndr () pass]
hsq_explicit = [LHsTyVarBndr () GhcRn]
hs_tvs }) TcM ContextKind
kc_res_ki
= Name -> TyConFlavour -> TcM TyCon -> TcM TyCon
forall a. Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt Name
name TyConFlavour
flav (TcM TyCon -> TcM TyCon) -> TcM TyCon -> TcM TyCon
forall a b. (a -> b) -> a -> b
$
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]
XHsQTvs GhcRn
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
$
ContextKind -> TcM Type
newExpectedKind (ContextKind -> TcM Type) -> TcM ContextKind -> TcM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TcM ContextKind
kc_res_ki
; let
tc_binders :: [TyConBinder]
tc_binders = AnonArgFlag -> [TcTyVar] -> [TyConBinder]
mkAnonTyConBinders AnonArgFlag
VisArg [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
-> [TyConBinder]
-> Type
-> [(Name, TcTyVar)]
-> Bool
-> TyConFlavour
-> TyCon
mkTcTyCon Name
name [TyConBinder]
tc_binders Type
res_kind [(Name, TcTyVar)]
all_tv_prs
Bool
False
TyConFlavour
flav
; String -> MsgDoc -> TcM ()
traceTc String
"kcInferDeclHeader: 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]
XHsQTvs GhcRn
kv_ns, [Located (HsTyVarBndr () GhcRn)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Located (HsTyVarBndr () GhcRn)]
[LHsTyVarBndr () GhcRn]
hs_tvs
, [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 -> TcM 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
kcCheckDeclHeader_sig
:: Kind
-> Name
-> TyConFlavour
-> LHsQTyVars GhcRn
-> TcM ContextKind
-> TcM TcTyCon
Type
kisig Name
name TyConFlavour
flav
(HsQTvs { hsq_ext :: forall pass. LHsQTyVars pass -> XHsQTvs pass
hsq_ext = XHsQTvs GhcRn
implicit_nms
, hsq_explicit :: forall pass. LHsQTyVars pass -> [LHsTyVarBndr () pass]
hsq_explicit = [LHsTyVarBndr () GhcRn]
explicit_nms }) TcM ContextKind
kc_res_ki
= Name -> TyConFlavour -> TcM TyCon -> TcM TyCon
forall a. Name -> TyConFlavour -> TcM a -> TcM a
addTyConFlavCtxt Name
name TyConFlavour
flav (TcM TyCon -> TcM TyCon) -> TcM TyCon -> TcM TyCon
forall a b. (a -> b) -> a -> b
$
do {
let ([ZippedBinder]
zipped_binders, [Located (HsTyVarBndr () GhcRn)]
excess_bndrs, Type
kisig') = Type
-> [LHsTyVarBndr () GhcRn]
-> ([ZippedBinder], [LHsTyVarBndr () GhcRn], Type)
zipBinders Type
kisig [LHsTyVarBndr () GhcRn]
explicit_nms
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Located (HsTyVarBndr () GhcRn)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Located (HsTyVarBndr () GhcRn)]
excess_bndrs) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ MsgDoc -> TcM ()
forall a. MsgDoc -> TcM a
failWithTc (Type -> [LHsTyVarBndr () GhcRn] -> MsgDoc
tooManyBindersErr Type
kisig' [Located (HsTyVarBndr () GhcRn)]
[LHsTyVarBndr () GhcRn]
excess_bndrs)
; ([TyConBinder]
vis_tcbs, [[(Name, TcTyVar)]] -> [(Name, TcTyVar)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [(Name, TcTyVar)]
explicit_tv_prs) <- (ZippedBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)]))
-> [ZippedBinder]
-> IOEnv
(Env TcGblEnv TcLclEnv) ([TyConBinder], [[(Name, TcTyVar)]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM ZippedBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
zipped_to_tcb [ZippedBinder]
zipped_binders
; (TcLevel
tclvl, WantedConstraints
wanted, ([TcTyVar]
implicit_tvs, ([TyBinder]
invis_binders, Type
r_ki)))
<- String
-> TcM ([TcTyVar], ([TyBinder], Type))
-> TcM
(TcLevel, WantedConstraints, ([TcTyVar], ([TyBinder], Type)))
forall a. String -> TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndSolveEqualitiesX String
"kcCheckDeclHeader_sig" (TcM ([TcTyVar], ([TyBinder], Type))
-> TcM
(TcLevel, WantedConstraints, ([TcTyVar], ([TyBinder], Type))))
-> TcM ([TcTyVar], ([TyBinder], Type))
-> TcM
(TcLevel, WantedConstraints, ([TcTyVar], ([TyBinder], Type)))
forall a b. (a -> b) -> a -> b
$
[Name]
-> TcM ([TyBinder], Type) -> TcM ([TcTyVar], ([TyBinder], Type))
forall a. [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Tv [Name]
XHsQTvs GhcRn
implicit_nms (TcM ([TyBinder], Type) -> TcM ([TcTyVar], ([TyBinder], Type)))
-> TcM ([TyBinder], Type) -> TcM ([TcTyVar], ([TyBinder], Type))
forall a b. (a -> b) -> a -> b
$
[(Name, TcTyVar)]
-> TcM ([TyBinder], Type) -> TcM ([TyBinder], Type)
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
explicit_tv_prs (TcM ([TyBinder], Type) -> TcM ([TyBinder], Type))
-> TcM ([TyBinder], Type) -> TcM ([TyBinder], Type)
forall a b. (a -> b) -> a -> b
$
do {
(ZippedBinder -> TcM ()) -> [ZippedBinder] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ZippedBinder -> TcM ()
check_zipped_binder [ZippedBinder]
zipped_binders
; ContextKind
ctx_k <- TcM ContextKind
kc_res_ki
; Maybe Type
m_res_ki <- case ContextKind
ctx_k of
ContextKind
AnyKind -> Maybe Type -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
ContextKind
_ -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type)
-> TcM Type -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ContextKind -> TcM Type
newExpectedKind ContextKind
ctx_k
; let ([TyBinder]
invis_binders, Type
r_ki) = Type -> Maybe Type -> ([TyBinder], Type)
split_invis Type
kisig' Maybe Type
m_res_ki
; Maybe Type -> (Type -> TcM ()) -> TcM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenIsJust Maybe Type
m_res_ki ((Type -> TcM ()) -> TcM ()) -> (Type -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \Type
res_ki ->
TcM Coercion -> TcM ()
forall a. TcM a -> TcM ()
discardResult (TcM Coercion -> TcM ()) -> TcM Coercion -> TcM ()
forall a b. (a -> b) -> a -> b
$
Maybe MsgDoc -> Type -> Type -> TcM Coercion
unifyKind Maybe MsgDoc
forall a. Maybe a
Nothing Type
r_ki Type
res_ki
; ([TyBinder], Type) -> TcM ([TyBinder], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyBinder]
invis_binders, Type
r_ki) }
; [TcTyVar]
implicit_tvs <- (TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HasDebugCallStack =>
TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
zonkTcTyVarToTyVar [TcTyVar]
implicit_tvs
; [TyConBinder]
invis_tcbs <- (TyBinder -> IOEnv (Env TcGblEnv TcLclEnv) TyConBinder)
-> [TyBinder] -> IOEnv (Env TcGblEnv TcLclEnv) [TyConBinder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TyBinder -> IOEnv (Env TcGblEnv TcLclEnv) TyConBinder
invis_to_tcb [TyBinder]
invis_binders
; let tcbs :: [TyConBinder]
tcbs = [TyConBinder]
vis_tcbs [TyConBinder] -> [TyConBinder] -> [TyConBinder]
forall a. [a] -> [a] -> [a]
++ [TyConBinder]
invis_tcbs
implicit_tv_prs :: [(Name, TcTyVar)]
implicit_tv_prs = [Name]
XHsQTvs GhcRn
implicit_nms [Name] -> [TcTyVar] -> [(Name, TcTyVar)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcTyVar]
implicit_tvs
all_tv_prs :: [(Name, TcTyVar)]
all_tv_prs = [(Name, TcTyVar)]
implicit_tv_prs [(Name, TcTyVar)] -> [(Name, TcTyVar)] -> [(Name, TcTyVar)]
forall a. [a] -> [a] -> [a]
++ [(Name, TcTyVar)]
explicit_tv_prs
tc :: TyCon
tc = Name
-> [TyConBinder]
-> Type
-> [(Name, TcTyVar)]
-> Bool
-> TyConFlavour
-> TyCon
mkTcTyCon Name
name [TyConBinder]
tcbs Type
r_ki [(Name, TcTyVar)]
all_tv_prs Bool
True TyConFlavour
flav
skol_info :: SkolemInfo
skol_info = TyConFlavour -> Name -> SkolemInfo
TyConSkol TyConFlavour
flav Name
name
; SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
reportUnsolvedEqualities SkolemInfo
skol_info ([TyConBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyConBinder]
tcbs) TcLevel
tclvl WantedConstraints
wanted
; String -> MsgDoc -> TcM ()
traceTc String
"kcCheckDeclHeader_sig done:" (MsgDoc -> TcM ()) -> MsgDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$ [MsgDoc] -> MsgDoc
vcat
[ String -> MsgDoc
text String
"tyConName = " MsgDoc -> MsgDoc -> MsgDoc
<+> Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyCon -> Name
tyConName TyCon
tc)
, String -> MsgDoc
text String
"kisig =" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
debugPprType Type
kisig
, String -> MsgDoc
text String
"tyConKind =" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
debugPprType (TyCon -> Type
tyConKind TyCon
tc)
, String -> MsgDoc
text String
"tyConBinders = " MsgDoc -> MsgDoc -> MsgDoc
<+> [TyConBinder] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyCon -> [TyConBinder]
tyConBinders TyCon
tc)
, String -> MsgDoc
text String
"tcTyConScopedTyVars" MsgDoc -> MsgDoc -> MsgDoc
<+> [(Name, TcTyVar)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr (TyCon -> [(Name, TcTyVar)]
tcTyConScopedTyVars TyCon
tc)
, String -> MsgDoc
text String
"tyConResKind" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
debugPprType (TyCon -> Type
tyConResKind TyCon
tc)
]
; TyCon -> TcM TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc }
where
zipped_to_tcb :: ZippedBinder -> TcM (TyConBinder, [(Name, TcTyVar)])
zipped_to_tcb :: ZippedBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
zipped_to_tcb ZippedBinder
zb = case ZippedBinder
zb of
ZippedBinder (Named (Bndr TcTyVar
v ArgFlag
Specified)) Maybe (LHsTyVarBndr () GhcRn)
Nothing ->
(TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgFlag -> TcTyVar -> TyConBinder
mkNamedTyConBinder ArgFlag
Specified TcTyVar
v, [])
ZippedBinder (Named (Bndr TcTyVar
v ArgFlag
Inferred)) Maybe (LHsTyVarBndr () GhcRn)
Nothing ->
(TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgFlag -> TcTyVar -> TyConBinder
mkNamedTyConBinder ArgFlag
Inferred TcTyVar
v, [])
ZippedBinder (Anon AnonArgFlag
InvisArg Scaled Type
bndr_ki) Maybe (LHsTyVarBndr () GhcRn)
Nothing -> do
Name
name <- OccName -> TcM Name
forall gbl lcl. OccName -> TcRnIf gbl lcl Name
newSysName (FastString -> OccName
mkTyVarOccFS (String -> FastString
fsLit String
"ev"))
let tv :: TcTyVar
tv = Name -> Type -> TcTyVar
mkTyVar Name
name (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
bndr_ki)
(TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall (m :: * -> *) a. Monad m => a -> m a
return (AnonArgFlag -> TcTyVar -> TyConBinder
mkAnonTyConBinder AnonArgFlag
InvisArg TcTyVar
tv, [])
ZippedBinder (Anon AnonArgFlag
VisArg Scaled Type
bndr_ki) (Just LHsTyVarBndr () GhcRn
b) ->
(TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)]))
-> (TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall a b. (a -> b) -> a -> b
$
let v_name :: Name
v_name = Located (HsTyVarBndr () GhcRn) -> Name
forall a. NamedThing a => a -> Name
getName Located (HsTyVarBndr () GhcRn)
LHsTyVarBndr () GhcRn
b
tv :: TcTyVar
tv = Name -> Type -> TcTyVar
mkTyVar Name
v_name (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled Type
bndr_ki)
tcb :: TyConBinder
tcb = AnonArgFlag -> TcTyVar -> TyConBinder
mkAnonTyConBinder AnonArgFlag
VisArg TcTyVar
tv
in (TyConBinder
tcb, [(Name
v_name, TcTyVar
tv)])
ZippedBinder (Named (Bndr TcTyVar
v ArgFlag
Required)) (Just LHsTyVarBndr () GhcRn
b) ->
(TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)]))
-> (TyConBinder, [(Name, TcTyVar)])
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall a b. (a -> b) -> a -> b
$
let v_name :: Name
v_name = Located (HsTyVarBndr () GhcRn) -> Name
forall a. NamedThing a => a -> Name
getName Located (HsTyVarBndr () GhcRn)
LHsTyVarBndr () GhcRn
b
tcb :: TyConBinder
tcb = ArgFlag -> TcTyVar -> TyConBinder
mkNamedTyConBinder ArgFlag
Required TcTyVar
v
in (TyConBinder
tcb, [(Name
v_name, TcTyVar
v)])
ZippedBinder
_ -> String
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
forall a. String -> a
panic String
"goVis: invalid ZippedBinder"
invis_to_tcb :: TyCoBinder -> TcM TyConBinder
invis_to_tcb :: TyBinder -> IOEnv (Env TcGblEnv TcLclEnv) TyConBinder
invis_to_tcb TyBinder
tb = do
(TyConBinder
tcb, [(Name, TcTyVar)]
stv) <- ZippedBinder
-> IOEnv (Env TcGblEnv TcLclEnv) (TyConBinder, [(Name, TcTyVar)])
zipped_to_tcb (TyBinder -> Maybe (LHsTyVarBndr () GhcRn) -> ZippedBinder
ZippedBinder TyBinder
tb Maybe (LHsTyVarBndr () GhcRn)
forall a. Maybe a
Nothing)
MASSERT(null stv)
TyConBinder -> IOEnv (Env TcGblEnv TcLclEnv) TyConBinder
forall (m :: * -> *) a. Monad m => a -> m a
return TyConBinder
tcb
check_zipped_binder :: ZippedBinder -> TcM ()
check_zipped_binder :: ZippedBinder -> TcM ()
check_zipped_binder (ZippedBinder TyBinder
_ Maybe (LHsTyVarBndr () GhcRn)
Nothing) = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
check_zipped_binder (ZippedBinder TyBinder
tb (Just LHsTyVarBndr () GhcRn
b)) =
case Located (HsTyVarBndr () GhcRn) -> HsTyVarBndr () GhcRn
forall l e. GenLocated l e -> e
unLoc Located (HsTyVarBndr () GhcRn)
LHsTyVarBndr () GhcRn
b of
UserTyVar XUserTyVar GhcRn
_ ()
_ LIdP GhcRn
_ -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
KindedTyVar XKindedTyVar GhcRn
_ ()
_ LIdP GhcRn
v LHsType GhcRn
v_hs_ki -> do
Type
v_ki <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig (Name -> UserTypeCtxt
TyVarBndrKindCtxt (Located Name -> Name
forall l e. GenLocated l e -> e
unLoc Located Name
LIdP GhcRn
v)) LHsType GhcRn
v_hs_ki
TcM Coercion -> TcM ()
forall a. TcM a -> TcM ()
discardResult (TcM Coercion -> TcM ()) -> TcM Coercion -> TcM ()
forall a b. (a -> b) -> a -> b
$
Maybe MsgDoc -> Type -> Type -> TcM Coercion
unifyKind (MsgDoc -> Maybe MsgDoc
forall a. a -> Maybe a
Just (Located Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Located Name
LIdP GhcRn
v))
(TyBinder -> Type
tyBinderType TyBinder
tb)
Type
v_ki
split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind)
split_invis :: Type -> Maybe Type -> ([TyBinder], Type)
split_invis Type
sig_ki Maybe Type
Nothing =
Type -> ([TyBinder], Type)
splitPiTysInvisible Type
sig_ki
split_invis Type
sig_ki (Just Type
res_ki) =
let n_res_invis_bndrs :: Int
n_res_invis_bndrs = Type -> Int
invisibleTyBndrCount Type
res_ki
n_sig_invis_bndrs :: Int
n_sig_invis_bndrs = Type -> Int
invisibleTyBndrCount Type
sig_ki
n_inst :: Int
n_inst = Int
n_sig_invis_bndrs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n_res_invis_bndrs
in Int -> Type -> ([TyBinder], Type)
splitPiTysInvisibleN Int
n_inst Type
sig_ki
data ZippedBinder =
ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn))
zipBinders
:: Kind
-> [LHsTyVarBndr () GhcRn]
-> ([ZippedBinder],
[LHsTyVarBndr () GhcRn],
Kind)
zipBinders :: Type
-> [LHsTyVarBndr () GhcRn]
-> ([ZippedBinder], [LHsTyVarBndr () GhcRn], Type)
zipBinders = [ZippedBinder]
-> Type
-> [Located (HsTyVarBndr () GhcRn)]
-> ([ZippedBinder], [Located (HsTyVarBndr () GhcRn)], Type)
zip_binders []
where
zip_binders :: [ZippedBinder]
-> Type
-> [Located (HsTyVarBndr () GhcRn)]
-> ([ZippedBinder], [Located (HsTyVarBndr () GhcRn)], Type)
zip_binders [ZippedBinder]
acc Type
ki [] = ([ZippedBinder] -> [ZippedBinder]
forall a. [a] -> [a]
reverse [ZippedBinder]
acc, [], Type
ki)
zip_binders [ZippedBinder]
acc Type
ki (Located (HsTyVarBndr () GhcRn)
b:[Located (HsTyVarBndr () GhcRn)]
bs) =
case Type -> Maybe (TyBinder, Type)
tcSplitPiTy_maybe Type
ki of
Maybe (TyBinder, Type)
Nothing -> ([ZippedBinder] -> [ZippedBinder]
forall a. [a] -> [a]
reverse [ZippedBinder]
acc, Located (HsTyVarBndr () GhcRn)
bLocated (HsTyVarBndr () GhcRn)
-> [Located (HsTyVarBndr () GhcRn)]
-> [Located (HsTyVarBndr () GhcRn)]
forall a. a -> [a] -> [a]
:[Located (HsTyVarBndr () GhcRn)]
bs, Type
ki)
Just (TyBinder
tb, Type
ki') ->
let
(ZippedBinder
zb, [Located (HsTyVarBndr () GhcRn)]
bs') | Bool
zippable = (TyBinder -> Maybe (LHsTyVarBndr () GhcRn) -> ZippedBinder
ZippedBinder TyBinder
tb (Located (HsTyVarBndr () GhcRn)
-> Maybe (Located (HsTyVarBndr () GhcRn))
forall a. a -> Maybe a
Just Located (HsTyVarBndr () GhcRn)
b), [Located (HsTyVarBndr () GhcRn)]
bs)
| Bool
otherwise = (TyBinder -> Maybe (LHsTyVarBndr () GhcRn) -> ZippedBinder
ZippedBinder TyBinder
tb Maybe (LHsTyVarBndr () GhcRn)
forall a. Maybe a
Nothing, Located (HsTyVarBndr () GhcRn)
bLocated (HsTyVarBndr () GhcRn)
-> [Located (HsTyVarBndr () GhcRn)]
-> [Located (HsTyVarBndr () GhcRn)]
forall a. a -> [a] -> [a]
:[Located (HsTyVarBndr () GhcRn)]
bs)
zippable :: Bool
zippable =
case TyBinder
tb of
Named (Bndr TcTyVar
_ (Invisible Specificity
_)) -> Bool
False
Named (Bndr TcTyVar
_ ArgFlag
Required) -> Bool
True
Anon AnonArgFlag
InvisArg Scaled Type
_ -> Bool
False
Anon AnonArgFlag
VisArg Scaled Type
_ -> Bool
True
in
[ZippedBinder]
-> Type
-> [Located (HsTyVarBndr () GhcRn)]
-> ([ZippedBinder], [Located (HsTyVarBndr () GhcRn)], Type)
zip_binders (ZippedBinder
zbZippedBinder -> [ZippedBinder] -> [ZippedBinder]
forall a. a -> [a] -> [a]
:[ZippedBinder]
acc) Type
ki' [Located (HsTyVarBndr () GhcRn)]
bs'
tooManyBindersErr :: Kind -> [LHsTyVarBndr () GhcRn] -> SDoc
tooManyBindersErr :: Type -> [LHsTyVarBndr () GhcRn] -> MsgDoc
tooManyBindersErr Type
ki [LHsTyVarBndr () GhcRn]
bndrs =
MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text String
"Not a function kind:")
Int
4 (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
ki) MsgDoc -> MsgDoc -> MsgDoc
$$
MsgDoc -> Int -> MsgDoc -> MsgDoc
hang (String -> MsgDoc
text String
"but extra binders found:")
Int
4 ([MsgDoc] -> MsgDoc
fsep ((Located (HsTyVarBndr () GhcRn) -> MsgDoc)
-> [Located (HsTyVarBndr () GhcRn)] -> [MsgDoc]
forall a b. (a -> b) -> [a] -> [b]
map Located (HsTyVarBndr () GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Located (HsTyVarBndr () GhcRn)]
[LHsTyVarBndr () GhcRn]
bndrs))
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 (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_Q_Skol :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Q_Skol = (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX ((Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newImplicitTyVarQ Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedSkolemTyVar)
bindImplicitTKBndrs_Q_Tv :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Q_Tv = (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX ((Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newImplicitTyVarQ Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedTyVarTyVar)
bindImplicitTKBndrs_Skol :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Skol = (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedSkolemTyVar
bindImplicitTKBndrs_Tv :: [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrs_Tv = (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
cloneFlexiKindedTyVarTyVar
bindImplicitTKBndrsX
:: (Name -> TcM TcTyVar)
-> [Name]
-> TcM a
-> TcM ([TcTyVar], a)
bindImplicitTKBndrsX :: (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM a -> TcM ([TcTyVar], a)
bindImplicitTKBndrsX Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv [Name]
tv_names TcM a
thing_inside
= do { [TcTyVar]
tkvs <- (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [Name] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv [Name]
tv_names
; 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)
; a
res <- [(Name, TcTyVar)] -> TcM a -> TcM a
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv ([Name]
tv_names [Name] -> [TcTyVar] -> [(Name, TcTyVar)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcTyVar]
tkvs)
TcM a
thing_inside
; ([TcTyVar], a) -> TcM ([TcTyVar], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar]
tkvs, a
res) }
newImplicitTyVarQ :: (Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
newImplicitTyVarQ :: (Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newImplicitTyVarQ Name -> IOEnv (Env TcGblEnv TcLclEnv) 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 -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv
Maybe TcTyThing
_ -> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
name }
newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
newFlexiKindedTyVar :: (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedTyVar Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
name
= do { Type
kind <- TcM Type
newMetaKindVar
; Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
name Type
kind }
newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
newFlexiKindedSkolemTyVar :: Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedSkolemTyVar = (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedTyVar Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newSkolemTyVar
newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
newFlexiKindedTyVarTyVar :: Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedTyVarTyVar = (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedTyVar Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newTyVarTyVar
cloneFlexiKindedTyVarTyVar :: Name -> TcM TyVar
cloneFlexiKindedTyVarTyVar :: Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
cloneFlexiKindedTyVarTyVar = (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newFlexiKindedTyVar Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
cloneTyVarTyVar
bindExplicitTKTele_Skol_M
:: TcTyMode
-> HsForAllTelescope GhcRn
-> TcM a
-> TcM ([TcTyVarBinder], a)
bindExplicitTKTele_Skol_M :: TcTyMode
-> HsForAllTelescope GhcRn -> TcM a -> TcM ([TcTyVarBinder], a)
bindExplicitTKTele_Skol_M TcTyMode
mode HsForAllTelescope GhcRn
tele TcM a
thing_inside = case HsForAllTelescope GhcRn
tele of
HsForAllVis { hsf_vis_bndrs :: forall pass. HsForAllTelescope pass -> [LHsTyVarBndr () pass]
hsf_vis_bndrs = [LHsTyVarBndr () GhcRn]
bndrs }
-> do { ([VarBndr TcTyVar ()]
req_tv_bndrs, a
thing) <- TcTyMode
-> [LHsTyVarBndr () GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar ()], a)
forall flag a.
OutputableBndrFlag flag =>
TcTyMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Skol_M TcTyMode
mode [LHsTyVarBndr () GhcRn]
bndrs TcM a
thing_inside
; ([TcTyVarBinder], a) -> TcM ([TcTyVarBinder], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VarBndr TcTyVar ()] -> [TcTyVarBinder]
forall a. [VarBndr a ()] -> [VarBndr a ArgFlag]
tyVarReqToBinders [VarBndr TcTyVar ()]
req_tv_bndrs, a
thing) }
HsForAllInvis { hsf_invis_bndrs :: forall pass.
HsForAllTelescope pass -> [LHsTyVarBndr Specificity pass]
hsf_invis_bndrs = [LHsTyVarBndr Specificity GhcRn]
bndrs }
-> do { ([VarBndr TcTyVar Specificity]
inv_tv_bndrs, a
thing) <- TcTyMode
-> [LHsTyVarBndr Specificity GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar Specificity], a)
forall flag a.
OutputableBndrFlag flag =>
TcTyMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Skol_M TcTyMode
mode [LHsTyVarBndr Specificity GhcRn]
bndrs TcM a
thing_inside
; ([TcTyVarBinder], a) -> TcM ([TcTyVarBinder], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VarBndr TcTyVar Specificity] -> [TcTyVarBinder]
forall a. [VarBndr a Specificity] -> [VarBndr a ArgFlag]
tyVarSpecToBinders [VarBndr TcTyVar Specificity]
inv_tv_bndrs, a
thing) }
bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
:: (OutputableBndrFlag flag)
=> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TyVar flag], a)
bindExplicitTKBndrs_Skol_M, bindExplicitTKBndrs_Tv_M
:: (OutputableBndrFlag flag)
=> TcTyMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TyVar flag], a)
bindExplicitTKBndrs_Skol :: [LHsTyVarBndr flag GhcRn]
-> TcM a -> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Skol = (HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
forall flag a.
OutputableBndrFlag flag =>
(HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrsX (TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall flag.
TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsTyVarBndr (TypeOrKind -> TcTyMode
mkMode TypeOrKind
KindLevel) Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newSkolemTyVar)
bindExplicitTKBndrs_Skol_M :: TcTyMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Skol_M TcTyMode
mode = (HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
forall flag a.
OutputableBndrFlag flag =>
(HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrsX (TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall flag.
TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsTyVarBndr (TcTyMode -> TcTyMode
kindLevel TcTyMode
mode) Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newSkolemTyVar)
bindExplicitTKBndrs_Tv :: [LHsTyVarBndr flag GhcRn]
-> TcM a -> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Tv = (HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
forall flag a.
OutputableBndrFlag flag =>
(HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrsX (TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall flag.
TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsTyVarBndr (TypeOrKind -> TcTyMode
mkMode TypeOrKind
KindLevel) Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
cloneTyVarTyVar)
bindExplicitTKBndrs_Tv_M :: TcTyMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Tv_M TcTyMode
mode = (HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
forall flag a.
OutputableBndrFlag flag =>
(HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrsX (TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall flag.
TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsTyVarBndr (TcTyMode -> TcTyMode
kindLevel TcTyMode
mode) Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
cloneTyVarTyVar)
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 -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr () GhcRn] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr () GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX_Q (ContextKind
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr () GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsQTyVarBndr ContextKind
ctxt_kind Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newSkolemTyVar)
bindExplicitTKBndrs_Q_Tv :: ContextKind
-> [LHsTyVarBndr () GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrs_Q_Tv ContextKind
ctxt_kind = (HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr () GhcRn] -> TcM a -> TcM ([TcTyVar], a)
forall a.
(HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr () GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX_Q (ContextKind
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr () GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsQTyVarBndr ContextKind
ctxt_kind Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newTyVarTyVar)
bindExplicitTKBndrsX_Q
:: (HsTyVarBndr () GhcRn -> TcM TcTyVar)
-> [LHsTyVarBndr () GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
bindExplicitTKBndrsX_Q :: (HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr () GhcRn] -> TcM a -> TcM ([TcTyVar], a)
bindExplicitTKBndrsX_Q HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tc_tv [LHsTyVarBndr () GhcRn]
hs_tvs TcM a
thing_inside
= do { ([VarBndr TcTyVar ()]
tv_bndrs,a
res) <- (HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr () GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar ()], a)
forall flag a.
OutputableBndrFlag flag =>
(HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrsX HsTyVarBndr () GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tc_tv [LHsTyVarBndr () GhcRn]
hs_tvs TcM a
thing_inside
; ([TcTyVar], a) -> TcM ([TcTyVar], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VarBndr TcTyVar ()] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [VarBndr TcTyVar ()]
tv_bndrs,a
res) }
bindExplicitTKBndrsX :: (OutputableBndrFlag flag)
=> (HsTyVarBndr flag GhcRn -> TcM TyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TyVar flag], a)
bindExplicitTKBndrsX :: (HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrsX HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tc_tv [LHsTyVarBndr flag GhcRn]
hs_tvs TcM a
thing_inside
= do { String -> MsgDoc -> TcM ()
traceTc String
"bindExplicTKBndrs" ([Located (HsTyVarBndr flag GhcRn)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [Located (HsTyVarBndr flag GhcRn)]
[LHsTyVarBndr flag GhcRn]
hs_tvs)
; [Located (HsTyVarBndr flag GhcRn)]
-> TcM ([VarBndr TcTyVar flag], a)
go [Located (HsTyVarBndr flag GhcRn)]
[LHsTyVarBndr flag GhcRn]
hs_tvs }
where
go :: [Located (HsTyVarBndr flag GhcRn)]
-> TcM ([VarBndr TcTyVar flag], a)
go [] = do { a
res <- TcM a
thing_inside
; ([VarBndr TcTyVar flag], a) -> TcM ([VarBndr TcTyVar flag], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], a
res) }
go (L SrcSpan
_ HsTyVarBndr flag GhcRn
hs_tv : [Located (HsTyVarBndr flag GhcRn)]
hs_tvs)
= do { TcTyVar
tv <- HsTyVarBndr flag GhcRn -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tc_tv HsTyVarBndr flag GhcRn
hs_tv
; ([VarBndr TcTyVar flag]
tvs,a
res) <- [(Name, TcTyVar)]
-> TcM ([VarBndr TcTyVar flag], a)
-> TcM ([VarBndr TcTyVar flag], a)
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(HsTyVarBndr flag GhcRn -> IdP GhcRn
forall flag (p :: Pass).
HsTyVarBndr flag (GhcPass p) -> IdP (GhcPass p)
hsTyVarName HsTyVarBndr flag GhcRn
hs_tv, TcTyVar
tv)] (TcM ([VarBndr TcTyVar flag], a)
-> TcM ([VarBndr TcTyVar flag], a))
-> TcM ([VarBndr TcTyVar flag], a)
-> TcM ([VarBndr TcTyVar flag], a)
forall a b. (a -> b) -> a -> b
$
[Located (HsTyVarBndr flag GhcRn)]
-> TcM ([VarBndr TcTyVar flag], a)
go [Located (HsTyVarBndr flag GhcRn)]
hs_tvs
; ([VarBndr TcTyVar flag], a) -> TcM ([VarBndr TcTyVar flag], a)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar -> flag -> VarBndr TcTyVar flag
forall var argf. var -> argf -> VarBndr var argf
Bndr TcTyVar
tv (HsTyVarBndr flag GhcRn -> flag
forall flag (pass :: Pass). HsTyVarBndr flag (GhcPass pass) -> flag
hsTyVarBndrFlag HsTyVarBndr flag GhcRn
hs_tv)VarBndr TcTyVar flag
-> [VarBndr TcTyVar flag] -> [VarBndr TcTyVar flag]
forall a. a -> [a] -> [a]
:[VarBndr TcTyVar flag]
tvs, a
res) }
tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr flag GhcRn -> TcM TcTyVar
tcHsTyVarBndr :: TcTyMode
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr flag GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsTyVarBndr TcTyMode
_ Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv (UserTyVar XUserTyVar GhcRn
_ flag
_ (L _ tv_nm))
= do { Type
kind <- TcM Type
newMetaKindVar
; Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
tv_nm Type
kind }
tcHsTyVarBndr TcTyMode
mode Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv (KindedTyVar XKindedTyVar GhcRn
_ flag
_ (L _ tv_nm) LHsType GhcRn
lhs_kind)
= do { Type
kind <- TcTyMode -> UserTypeCtxt -> LHsType GhcRn -> TcM Type
tc_lhs_kind_sig TcTyMode
mode (Name -> UserTypeCtxt
TyVarBndrKindCtxt Name
tv_nm) LHsType GhcRn
lhs_kind
; Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
tv_nm Type
kind }
tcHsQTyVarBndr :: ContextKind
-> (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr () GhcRn -> TcM TcTyVar
tcHsQTyVarBndr :: ContextKind
-> (Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> HsTyVarBndr () GhcRn
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
tcHsQTyVarBndr ContextKind
ctxt_kind Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv (UserTyVar XUserTyVar GhcRn
_ ()
_ (L _ tv_nm))
= do { Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe Name
tv_nm
; case Maybe TcTyThing
mb_tv of
Just (ATyVar Name
_ TcTyVar
tv) -> TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) 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 -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
tv_nm Type
kind } }
tcHsQTyVarBndr ContextKind
_ Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv (KindedTyVar XKindedTyVar GhcRn
_ ()
_ (L _ tv_nm) LHsType GhcRn
lhs_kind)
= do { Type
kind <- UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig (Name -> UserTypeCtxt
TyVarBndrKindCtxt Name
tv_nm) LHsType GhcRn
lhs_kind
; Maybe TcTyThing
mb_tv <- Name -> TcM (Maybe TcTyThing)
tcLookupLcl_maybe 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 MsgDoc -> Type -> Type -> TcM Coercion
unifyKind (MsgDoc -> Maybe MsgDoc
forall a. a -> Maybe a
Just (Name -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Name
tv_nm))
Type
kind (TcTyVar -> Type
tyVarKind TcTyVar
tv)
; TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
tv }
Maybe TcTyThing
_ -> Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
new_tv Name
tv_nm Type
kind }
bindTyClTyVars :: Name
-> (TcTyCon -> [TyConBinder] -> Kind -> TcM a) -> TcM a
bindTyClTyVars :: Name -> (TyCon -> [TyConBinder] -> Type -> TcM a) -> TcM a
bindTyClTyVars Name
tycon_name TyCon -> [TyConBinder] -> Type -> TcM a
thing_inside
= do { TyCon
tycon <- HasDebugCallStack => Name -> TcM TyCon
Name -> TcM TyCon
tcLookupTcTyCon 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 MsgDoc -> MsgDoc -> MsgDoc
$$ [(Name, TcTyVar)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [(Name, TcTyVar)]
scoped_prs)
; [(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
$
TyCon -> [TyConBinder] -> Type -> TcM a
thing_inside TyCon
tycon [TyConBinder]
binders Type
res_kind }
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort [TcTyVar]
spec_tkvs
= do { [TcTyVar]
spec_tkvs <- (TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar)
-> [TcTyVar] -> TcM [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
zonkAndSkolemise [TcTyVar]
spec_tkvs
; [TcTyVar] -> TcM [TcTyVar]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar] -> [TcTyVar]
scopedSort [TcTyVar]
spec_tkvs) }
kindGeneralizeSome :: WantedConstraints
-> TcType
-> TcM [KindVar]
kindGeneralizeSome :: WantedConstraints -> Type -> TcM [TcTyVar]
kindGeneralizeSome WantedConstraints
wanted Type
kind_or_type
= do {
; CandidatesQTvs
dvs <- Type -> TcM CandidatesQTvs
candidateQTyVarsOfKind Type
kind_or_type
; CandidatesQTvs
dvs <- WantedConstraints -> CandidatesQTvs -> TcM CandidatesQTvs
filterConstrainedCandidates WantedConstraints
wanted CandidatesQTvs
dvs
; CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars CandidatesQTvs
dvs }
filterConstrainedCandidates
:: WantedConstraints
-> CandidatesQTvs
-> TcM CandidatesQTvs
filterConstrainedCandidates :: WantedConstraints -> CandidatesQTvs -> TcM CandidatesQTvs
filterConstrainedCandidates WantedConstraints
wanted CandidatesQTvs
dvs
| WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted
= CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dvs
| Bool
otherwise
= do { VarSet
wc_tvs <- VarSet -> TcM VarSet
zonkTyCoVarsAndFV (WantedConstraints -> VarSet
tyCoVarsOfWC WantedConstraints
wanted)
; let (VarSet
to_promote, CandidatesQTvs
dvs') = CandidatesQTvs -> (TcTyVar -> Bool) -> (VarSet, CandidatesQTvs)
partitionCandidates CandidatesQTvs
dvs (TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
wc_tvs)
; Bool
_ <- VarSet -> TcRnIf TcGblEnv TcLclEnv Bool
promoteTyVarSet VarSet
to_promote
; CandidatesQTvs -> TcM CandidatesQTvs
forall (m :: * -> *) a. Monad m => a -> m a
return CandidatesQTvs
dvs' }
kindGeneralizeAll :: TcType -> TcM [KindVar]
kindGeneralizeAll :: Type -> TcM [TcTyVar]
kindGeneralizeAll Type
kind_or_type
= do { String -> MsgDoc -> TcM ()
traceTc String
"kindGeneralizeAll" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind_or_type)
; CandidatesQTvs
dvs <- Type -> TcM CandidatesQTvs
candidateQTyVarsOfKind Type
kind_or_type
; CandidatesQTvs -> TcM [TcTyVar]
quantifyTyVars CandidatesQTvs
dvs }
kindGeneralizeNone :: TcType
-> TcM ()
kindGeneralizeNone :: Type -> TcM ()
kindGeneralizeNone Type
kind_or_type
= do { String -> MsgDoc -> TcM ()
traceTc String
"kindGeneralizeNone" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind_or_type)
; CandidatesQTvs
dvs <- Type -> TcM CandidatesQTvs
candidateQTyVarsOfKind Type
kind_or_type
; Bool
_ <- VarSet -> TcRnIf TcGblEnv TcLclEnv Bool
promoteTyVarSet (CandidatesQTvs -> VarSet
candidateKindVars CandidatesQTvs
dvs)
; () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }
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 AnonArgFlag
af Scaled 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 (Scaled Type -> Type
forall a. Scaled a -> a
scaledThing Scaled 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 (AnonArgFlag -> TyConBndrVis
AnonTCB AnonArgFlag
af)
(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)
data DataSort
= DataDeclSort NewOrData
| DataInstanceSort NewOrData
| DataFamilySort
checkDataKindSig :: DataSort -> Kind
-> TcM ()
checkDataKindSig :: DataSort -> Type -> TcM ()
checkDataKindSig DataSort
data_sort Type
kind
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; String -> MsgDoc -> TcM ()
traceTc String
"checkDataKindSig" (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind)
; Bool -> MsgDoc -> TcM ()
checkTc (DynFlags -> Bool
is_TYPE_or_Type DynFlags
dflags Bool -> Bool -> Bool
|| Bool
is_kind_var)
(DynFlags -> MsgDoc
err_msg DynFlags
dflags) }
where
res_kind :: Type
res_kind = ([TyBinder], Type) -> Type
forall a b. (a, b) -> b
snd (Type -> ([TyBinder], Type)
tcSplitPiTys Type
kind)
pp_dec :: SDoc
pp_dec :: MsgDoc
pp_dec = String -> MsgDoc
text (String -> MsgDoc) -> String -> MsgDoc
forall a b. (a -> b) -> a -> b
$
case DataSort
data_sort of
DataDeclSort NewOrData
DataType -> String
"Data type"
DataDeclSort NewOrData
NewType -> String
"Newtype"
DataInstanceSort NewOrData
DataType -> String
"Data instance"
DataInstanceSort NewOrData
NewType -> String
"Newtype instance"
DataSort
DataFamilySort -> String
"Data family"
is_newtype :: Bool
is_newtype :: Bool
is_newtype =
case DataSort
data_sort of
DataDeclSort NewOrData
new_or_data -> NewOrData
new_or_data NewOrData -> NewOrData -> Bool
forall a. Eq a => a -> a -> Bool
== NewOrData
NewType
DataInstanceSort NewOrData
new_or_data -> NewOrData
new_or_data NewOrData -> NewOrData -> Bool
forall a. Eq a => a -> a -> Bool
== NewOrData
NewType
DataSort
DataFamilySort -> Bool
False
is_data_family :: Bool
is_data_family :: Bool
is_data_family =
case DataSort
data_sort of
DataDeclSort{} -> Bool
False
DataInstanceSort{} -> Bool
False
DataSort
DataFamilySort -> Bool
True
tYPE_ok :: DynFlags -> Bool
tYPE_ok :: DynFlags -> Bool
tYPE_ok DynFlags
dflags =
(Bool
is_newtype Bool -> Bool -> Bool
&& Extension -> DynFlags -> Bool
xopt Extension
LangExt.UnliftedNewtypes DynFlags
dflags)
Bool -> Bool -> Bool
|| Bool
is_data_family
is_TYPE :: Bool
is_TYPE :: Bool
is_TYPE = Type -> Bool
tcIsRuntimeTypeKind Type
res_kind
is_Type :: Bool
is_Type :: Bool
is_Type = Type -> Bool
tcIsLiftedTypeKind Type
res_kind
is_TYPE_or_Type :: DynFlags -> Bool
is_TYPE_or_Type :: DynFlags -> Bool
is_TYPE_or_Type DynFlags
dflags | DynFlags -> Bool
tYPE_ok DynFlags
dflags = Bool
is_TYPE
| Bool
otherwise = Bool
is_Type
is_kind_var :: Bool
is_kind_var :: Bool
is_kind_var | Bool
is_data_family = Maybe (TcTyVar, Coercion) -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe (TcTyVar, Coercion)
tcGetCastedTyVar_maybe Type
res_kind)
| Bool
otherwise = Bool
False
err_msg :: DynFlags -> SDoc
err_msg :: DynFlags -> MsgDoc
err_msg DynFlags
dflags =
[MsgDoc] -> MsgDoc
sep [ ([MsgDoc] -> MsgDoc
sep [ MsgDoc
pp_dec MsgDoc -> MsgDoc -> MsgDoc
<+>
String -> MsgDoc
text String
"has non-" MsgDoc -> MsgDoc -> MsgDoc
<>
(if DynFlags -> Bool
tYPE_ok DynFlags
dflags then String -> MsgDoc
text String
"TYPE" else Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
liftedTypeKind)
, (if Bool
is_data_family then String -> MsgDoc
text String
"and non-variable" else MsgDoc
empty) MsgDoc -> MsgDoc -> MsgDoc
<+>
String -> MsgDoc
text String
"return kind" MsgDoc -> MsgDoc -> MsgDoc
<+> MsgDoc -> MsgDoc
quotes (Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
res_kind) ])
, if Bool -> Bool
not (DynFlags -> Bool
tYPE_ok DynFlags
dflags) Bool -> Bool -> Bool
&& Bool
is_TYPE Bool -> Bool -> Bool
&& Bool
is_newtype Bool -> Bool -> Bool
&&
Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.UnliftedNewtypes DynFlags
dflags)
then String -> MsgDoc
text String
"Perhaps you intended to use UnliftedNewtypes"
else MsgDoc
empty ]
checkClassKindSig :: Kind -> TcM ()
checkClassKindSig :: Type -> TcM ()
checkClassKindSig Type
kind = Bool -> MsgDoc -> TcM ()
checkTc (Type -> Bool
tcIsConstraintKind Type
kind) MsgDoc
err_msg
where
err_msg :: SDoc
err_msg :: MsgDoc
err_msg =
String -> MsgDoc
text String
"Kind signature on a class must end with" MsgDoc -> MsgDoc -> MsgDoc
<+> Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
constraintKind MsgDoc -> MsgDoc -> MsgDoc
$$
String -> MsgDoc
text String
"unobscured by type families"
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 AnonArgFlag
af Scaled Type
_ -> AnonArgFlag -> TyConBndrVis
AnonTCB AnonArgFlag
af 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,InvisTVBinder)]
, TcThetaType
, TcType )
tcHsPartialSigType :: UserTypeCtxt
-> LHsSigWcType GhcRn
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [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 Specificity GhcRn]
explicit_hs_tvs, L _ hs_ctxt, LHsType GhcRn
hs_tau) <- LHsType GhcRn
-> ([LHsTyVarBndr Specificity GhcRn], LHsContext GhcRn,
LHsType GhcRn)
forall (p :: Pass).
LHsType (GhcPass p)
-> ([LHsTyVarBndr Specificity (GhcPass p)], LHsContext (GhcPass p),
LHsType (GhcPass p))
splitLHsSigmaTyInvis LHsType GhcRn
hs_ty
= UserTypeCtxt
-> LHsType GhcRn
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
forall a. UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
addSigCtxt UserTypeCtxt
ctxt LHsType GhcRn
hs_ty (TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type))
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
forall a b. (a -> b) -> a -> b
$
do { TcTyMode
mode <- TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
TypeLevel HoleMode
HM_Sig
; ([TcTyVar]
implicit_tvs, ([VarBndr TcTyVar Specificity]
explicit_tvbndrs, ([(Name, TcTyVar)]
wcs, Maybe Type
wcx, [Type]
theta, Type
tau)))
<- String
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a. String -> TcM a -> TcM a
solveEqualities String
"tcHsPartialSigType" (TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a b. (a -> b) -> a -> b
$
[Name]
-> ([(Name, TcTyVar)]
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a. [Name] -> ([(Name, TcTyVar)] -> TcM a) -> TcM a
tcNamedWildCardBinders [Name]
XHsWC GhcRn (LHsSigType GhcRn)
sig_wcs (([(Name, TcTyVar)]
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> ([(Name, TcTyVar)]
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a b. (a -> b) -> a -> b
$ \ [(Name, TcTyVar)]
wcs ->
[Name]
-> TcM
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(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
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))))
-> TcM
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))
-> TcM
([TcTyVar],
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
forall a b. (a -> b) -> a -> b
$
TcTyMode
-> [LHsTyVarBndr Specificity GhcRn]
-> TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
-> TcM
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))
forall flag a.
OutputableBndrFlag flag =>
TcTyMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TcTyVar flag], a)
bindExplicitTKBndrs_Tv_M TcTyMode
mode [LHsTyVarBndr Specificity GhcRn]
explicit_hs_tvs (TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
-> TcM
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type)))
-> TcM ([(Name, TcTyVar)], Maybe Type, [Type], Type)
-> TcM
([VarBndr TcTyVar Specificity],
([(Name, TcTyVar)], Maybe Type, [Type], Type))
forall a b. (a -> b) -> a -> b
$
do {
([Type]
theta, Maybe Type
wcx) <- TcTyMode -> [LHsType GhcRn] -> TcM ([Type], Maybe Type)
tcPartialContext TcTyMode
mode [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
hs_ctxt
; Type
ek <- TcM Type
newOpenTypeKind
; Type
tau <- LHsType GhcRn -> TcM Type -> TcM Type
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
hs_tau (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
hs_tau Type
ek
; ([(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 implicit_tvbndrs :: [VarBndr TcTyVar Specificity]
implicit_tvbndrs = (TcTyVar -> VarBndr TcTyVar Specificity)
-> [TcTyVar] -> [VarBndr TcTyVar Specificity]
forall a b. (a -> b) -> [a] -> [b]
map (Specificity -> TcTyVar -> VarBndr TcTyVar Specificity
forall vis. vis -> TcTyVar -> VarBndr TcTyVar vis
mkTyVarBinder Specificity
SpecifiedSpec) [TcTyVar]
implicit_tvs
; Type -> TcM ()
kindGeneralizeNone ([VarBndr TcTyVar Specificity] -> Type -> Type
mkInvisForAllTys [VarBndr TcTyVar Specificity]
implicit_tvbndrs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[VarBndr TcTyVar Specificity] -> Type -> Type
mkInvisForAllTys [VarBndr TcTyVar Specificity]
explicit_tvbndrs (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
mkPhiTy [Type]
theta (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
Type
tau)
; ((Name, TcTyVar) -> TcM ()) -> [(Name, TcTyVar)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, TcTyVar) -> TcM ()
emitNamedTypeHole [(Name, TcTyVar)]
wcs
; [VarBndr TcTyVar Specificity]
implicit_tvbndrs <- (VarBndr TcTyVar Specificity
-> IOEnv (Env TcGblEnv TcLclEnv) (VarBndr TcTyVar Specificity))
-> [VarBndr TcTyVar Specificity]
-> IOEnv (Env TcGblEnv TcLclEnv) [VarBndr TcTyVar Specificity]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VarBndr TcTyVar Specificity
-> IOEnv (Env TcGblEnv TcLclEnv) (VarBndr TcTyVar Specificity)
forall spec. VarBndr TcTyVar spec -> TcM (VarBndr TcTyVar spec)
zonkInvisTVBinder [VarBndr TcTyVar Specificity]
implicit_tvbndrs
; [VarBndr TcTyVar Specificity]
explicit_tvbndrs <- (VarBndr TcTyVar Specificity
-> IOEnv (Env TcGblEnv TcLclEnv) (VarBndr TcTyVar Specificity))
-> [VarBndr TcTyVar Specificity]
-> IOEnv (Env TcGblEnv TcLclEnv) [VarBndr TcTyVar Specificity]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VarBndr TcTyVar Specificity
-> IOEnv (Env TcGblEnv TcLclEnv) (VarBndr TcTyVar Specificity)
forall spec. VarBndr TcTyVar spec -> TcM (VarBndr TcTyVar spec)
zonkInvisTVBinder [VarBndr TcTyVar Specificity]
explicit_tvbndrs
; [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 tv_prs :: [(Name, VarBndr TcTyVar Specificity)]
tv_prs = ([Name]
XHsIB GhcRn (LHsType GhcRn)
implicit_hs_tvs [Name]
-> [VarBndr TcTyVar Specificity]
-> [(Name, VarBndr TcTyVar Specificity)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [VarBndr TcTyVar Specificity]
implicit_tvbndrs)
[(Name, VarBndr TcTyVar Specificity)]
-> [(Name, VarBndr TcTyVar Specificity)]
-> [(Name, VarBndr TcTyVar Specificity)]
forall a. [a] -> [a] -> [a]
++ ([LHsTyVarBndr Specificity GhcRn] -> [IdP GhcRn]
forall flag (p :: Pass).
[LHsTyVarBndr flag (GhcPass p)] -> [IdP (GhcPass p)]
hsLTyVarNames [LHsTyVarBndr Specificity GhcRn]
explicit_hs_tvs [Name]
-> [VarBndr TcTyVar Specificity]
-> [(Name, VarBndr TcTyVar Specificity)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [VarBndr TcTyVar Specificity]
explicit_tvbndrs)
; String -> MsgDoc -> TcM ()
traceTc String
"tcHsPartialSigType" ([(Name, VarBndr TcTyVar Specificity)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [(Name, VarBndr TcTyVar Specificity)]
tv_prs)
; ([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
-> TcM
([(Name, TcTyVar)], Maybe Type,
[(Name, VarBndr TcTyVar Specificity)], [Type], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, TcTyVar)]
wcs, Maybe Type
wcx, [(Name, VarBndr TcTyVar Specificity)]
tv_prs, [Type]
theta, Type
tau) }
tcPartialContext :: TcTyMode -> HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
tcPartialContext :: TcTyMode -> [LHsType GhcRn] -> TcM ([Type], Maybe Type)
tcPartialContext TcTyMode
mode [LHsType GhcRn]
hs_theta
| Just ([GenLocated SrcSpan (HsType GhcRn)]
hs_theta1, GenLocated SrcSpan (HsType GhcRn)
hs_ctxt_last) <- [GenLocated SrcSpan (HsType GhcRn)]
-> Maybe
([GenLocated SrcSpan (HsType GhcRn)],
GenLocated SrcSpan (HsType GhcRn))
forall a. [a] -> Maybe ([a], a)
snocView [GenLocated SrcSpan (HsType GhcRn)]
[LHsType GhcRn]
hs_theta
, L wc_loc ty@(HsWildCardTy _) <- LHsType GhcRn -> LHsType GhcRn
forall (p :: Pass). LHsType (GhcPass p) -> LHsType (GhcPass p)
ignoreParens GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_ctxt_last
= do { Type
wc_tv_ty <- SrcSpan -> TcM Type -> TcM Type
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
wc_loc (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
TcTyMode -> HsType GhcRn -> Type -> TcM Type
tcAnonWildCardOcc TcTyMode
mode HsType GhcRn
ty Type
constraintKind
; [Type]
theta <- (GenLocated SrcSpan (HsType GhcRn) -> TcM Type)
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType 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 <- (GenLocated SrcSpan (HsType GhcRn) -> TcM Type)
-> [GenLocated SrcSpan (HsType 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) [GenLocated SrcSpan (HsType GhcRn)]
[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
-> HsPatSigType GhcRn
-> TcM ( [(Name, TcTyVar)]
, [(Name, TcTyVar)]
, TcType)
tcHsPatSigType :: UserTypeCtxt
-> HsPatSigType GhcRn
-> TcM ([(Name, TcTyVar)], [(Name, TcTyVar)], Type)
tcHsPatSigType UserTypeCtxt
ctxt
(HsPS { hsps_ext :: forall pass. HsPatSigType pass -> XHsPS pass
hsps_ext = HsPSRn { hsps_nwcs = sig_wcs, hsps_imp_tvs = sig_ns }
, hsps_body :: forall pass. HsPatSigType pass -> LHsType pass
hsps_body = LHsType GhcRn
hs_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 { [(Name, TcTyVar)]
sig_tkv_prs <- (Name -> IOEnv (Env TcGblEnv TcLclEnv) (Name, TcTyVar))
-> [Name] -> IOEnv (Env TcGblEnv TcLclEnv) [(Name, TcTyVar)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> IOEnv (Env TcGblEnv TcLclEnv) (Name, TcTyVar)
new_implicit_tv [Name]
sig_ns
; TcTyMode
mode <- TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode TypeOrKind
TypeLevel HoleMode
HM_Sig
; ([(Name, TcTyVar)]
wcs, Type
sig_ty)
<- LHsType GhcRn
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a. LHsType GhcRn -> TcM a -> TcM a
addTypeCtxt LHsType GhcRn
hs_ty (TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type))
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a b. (a -> b) -> a -> b
$
String
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall a. String -> TcM a -> TcM a
solveEqualities 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
tcNamedWildCardBinders [Name]
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 ->
[(Name, TcTyVar)]
-> TcM ([(Name, TcTyVar)], Type) -> TcM ([(Name, TcTyVar)], Type)
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
sig_tkv_prs (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
ek <- TcM Type
newOpenTypeKind
; Type
sig_ty <- TcTyMode -> LHsType GhcRn -> Type -> TcM Type
tc_lhs_type TcTyMode
mode LHsType GhcRn
hs_ty Type
ek
; ([(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 ()) -> [(Name, TcTyVar)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, TcTyVar) -> TcM ()
emitNamedTypeHole [(Name, TcTyVar)]
wcs
; Type -> TcM ()
kindGeneralizeNone Type
sig_ty
; Type
sig_ty <- Type -> TcM Type
zonkTcType Type
sig_ty
; UserTypeCtxt -> Type -> TcM ()
checkValidType UserTypeCtxt
ctxt Type
sig_ty
; String -> MsgDoc -> TcM ()
traceTc String
"tcHsPatSigType" ([(Name, TcTyVar)] -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr [(Name, TcTyVar)]
sig_tkv_prs)
; ([(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)]
sig_tkv_prs, Type
sig_ty) }
where
new_implicit_tv :: Name -> IOEnv (Env TcGblEnv TcLclEnv) (Name, TcTyVar)
new_implicit_tv Name
name
= do { Type
kind <- TcM Type
newMetaKindVar
; TcTyVar
tv <- case UserTypeCtxt
ctxt of
RuleSigCtxt {} -> Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newSkolemTyVar Name
name Type
kind
UserTypeCtxt
_ -> Name -> Type -> IOEnv (Env TcGblEnv TcLclEnv) TcTyVar
newPatSigTyVar Name
name Type
kind
; (Name, TcTyVar) -> IOEnv (Env TcGblEnv TcLclEnv) (Name, TcTyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, TcTyVar
tv) }
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 :: GenLocated SrcSpan (HsType GhcRn) -> (Type, Type) -> TcM Type
check GenLocated SrcSpan (HsType GhcRn)
rn_ty (Type
ty, Type
act_kind)
= HasDebugCallStack =>
HsType GhcRn -> Type -> Type -> Type -> TcM Type
HsType GhcRn -> Type -> Type -> Type -> TcM Type
checkExpectedKind (GenLocated SrcSpan (HsType GhcRn) -> HsType GhcRn
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan (HsType GhcRn)
rn_ty) Type
ty Type
act_kind Type
kind
; [Type]
tys' <- (GenLocated SrcSpan (HsType GhcRn) -> (Type, Type) -> TcM Type)
-> [GenLocated SrcSpan (HsType GhcRn)]
-> [(Type, Type)]
-> TcM [Type]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM GenLocated SrcSpan (HsType GhcRn) -> (Type, Type) -> TcM Type
check [GenLocated SrcSpan (HsType GhcRn)]
[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) }
tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig :: UserTypeCtxt -> LHsType GhcRn -> TcM Type
tcLHsKindSig UserTypeCtxt
ctxt LHsType GhcRn
hs_kind
= TcTyMode -> UserTypeCtxt -> LHsType GhcRn -> TcM Type
tc_lhs_kind_sig (TypeOrKind -> TcTyMode
mkMode TypeOrKind
KindLevel) UserTypeCtxt
ctxt LHsType GhcRn
hs_kind
tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsType GhcRn -> TcM Type
tc_lhs_kind_sig TcTyMode
mode UserTypeCtxt
ctxt LHsType GhcRn
hs_kind
= do { Type
kind <- 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 (GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_kind)) (TcM Type -> TcM Type) -> TcM Type -> TcM Type
forall a b. (a -> b) -> a -> b
$
String -> TcM Type -> TcM Type
forall a. String -> TcM a -> TcM a
solveEqualities String
"tcLHsKindSig" (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
hs_kind Type
liftedTypeKind
; String -> MsgDoc -> TcM ()
traceTc String
"tcLHsKindSig" (GenLocated SrcSpan (HsType GhcRn) -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr GenLocated SrcSpan (HsType GhcRn)
LHsType GhcRn
hs_kind MsgDoc -> MsgDoc -> MsgDoc
$$ Type -> MsgDoc
forall a. Outputable a => a -> MsgDoc
ppr Type
kind)
; Type -> TcM ()
kindGeneralizeNone Type
kind
; Type
kind <- Type -> TcM Type
zonkTcType 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 }
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
_ -> String -> MsgDoc
text String
"it is defined and used in the same recursive group"
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) ]