module TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
newFlexiTyVar,
newFlexiTyVarTy,
newFlexiTyVarTys,
newOpenFlexiTyVarTy, newOpenTypeKind,
newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
cloneMetaTyVar,
newFmvTyVar, newFskTyVar,
readMetaTyVar, writeMetaTyVar,
newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
ExpType(..), ExpSigmaType, ExpRhoType,
mkCheckExpType,
newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
readExpType, readExpType_maybe,
expTypeToType, checkingExpType_maybe, checkingExpType,
tauifyExpType, inferResultToType,
genInstSkolTyVarsX,
newEvVar, newEvVars, newDict,
newWanted, newWanteds, cloneWanted, cloneSimple, cloneWC,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
newCoercionHole, fillCoercionHole, isFilledCoercionHole,
unpackCoercionHole, unpackCoercionHole_maybe,
checkCoercionHole,
newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
newMetaSigTyVars, newMetaSigTyVarX,
newSigTyVar, newSkolemTyVar, newWildCardX,
tcInstType,
tcInstSkolTyVars,tcInstSkolTyVarsX,
tcInstSuperSkolTyVarsX,
tcSkolDFunType, tcSuperSkolTyVars,
instSkolTyCoVarsX, freshenTyVarBndrs, freshenCoVarBndrsX,
zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
tidyEvVar, tidyCt, tidySkolemInfo,
skolemiseRuntimeUnk,
zonkTcTyVar, zonkTcTyVars,
zonkTcTyVarToTyVar, zonkSigTyVarPairs,
zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkTyCoVarsAndFVList,
zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
zonkQuantifiedTyVar, defaultTyVar,
quantifyTyVars,
zonkTcTyCoVarBndr, zonkTcTyVarBinder,
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper,
zonkEvVar, zonkWC, zonkSimples,
zonkId, zonkCoVar,
zonkCt, zonkSkolemInfo,
tcGetGlobalTyCoVars,
ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
) where
#include "HsVersions.h"
import GhcPrelude
import TyCoRep
import TcType
import Type
import Coercion
import Class
import Var
import TcRnMonad
import TcEvidence
import Id
import Name
import VarSet
import TysWiredIn
import TysPrim
import VarEnv
import NameEnv
import PrelNames
import Util
import Outputable
import FastString
import SrcLoc
import Bag
import Pair
import UniqSet
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Maybes
import Data.List ( mapAccumL )
import Control.Arrow ( second )
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ
kind_var_occ :: OccName
kind_var_occ = mkOccName tvName "k"
newMetaKindVar :: TcM TcKind
newMetaKindVar = do { uniq <- newUnique
; details <- newMetaDetails TauTv
; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
; traceTc "newMetaKindVar" (ppr kv)
; return (mkTyVarTy kv) }
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta
newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
newEvVar ty = do { name <- newSysName (predTypeOccName ty)
; return (mkLocalIdOrCoVar name ty) }
newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
newWanted orig t_or_k pty
= do loc <- getCtLocM orig t_or_k
d <- if isEqPred pty then HoleDest <$> newCoercionHole pty
else EvVarDest <$> newEvVar pty
return $ CtWanted { ctev_dest = d
, ctev_pred = pty
, ctev_nosh = WDeriv
, ctev_loc = loc }
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
cloneWanted :: Ct -> TcM CtEvidence
cloneWanted ct
= newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
where
ev = ctEvidence ct
cloneSimple :: Ct -> TcM Ct
cloneSimple = fmap mkNonCanonical . cloneWanted
cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
= do { simples' <- mapBagM cloneSimple simples
; implics' <- mapBagM clone_implic implics
; return (wc { wc_simple = simples', wc_impl = implics' }) }
where
clone_implic implic@(Implic { ic_wanted = inner_wanted })
= do { inner_wanted' <- cloneWC inner_wanted
; return (implic { ic_wanted = inner_wanted' }) }
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
emitWanted origin pty
= do { ev <- newWanted origin Nothing pty
; emitSimple $ mkNonCanonical ev
; return $ ctEvTerm ev }
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2
= do { hole <- newCoercionHole pty
; loc <- getCtLocM origin (Just t_or_k)
; emitSimple $ mkNonCanonical $
CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
, ctev_nosh = WDeriv, ctev_loc = loc }
; return (HoleCo hole) }
where
pty = mkPrimEqPredRole role ty1 ty2
emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
emitWantedEvVar origin ty
= do { new_cv <- newEvVar ty
; loc <- getCtLocM origin Nothing
; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
, ctev_pred = ty
, ctev_nosh = WDeriv
, ctev_loc = loc }
; emitSimple $ mkNonCanonical ctev
; return new_cv }
emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
emitWantedEvVars orig = mapM (emitWantedEvVar orig)
newDict :: Class -> [TcType] -> TcM DictId
newDict cls tys
= do { name <- newSysName (mkDictOcc (getOccName cls))
; return (mkLocalId name (mkClassPred cls tys)) }
predTypeOccName :: PredType -> OccName
predTypeOccName ty = case classifyPredType ty of
ClassPred cls _ -> mkDictOcc (getOccName cls)
EqPred {} -> mkVarOccFS (fsLit "co")
IrredPred {} -> mkVarOccFS (fsLit "irred")
ForAllPred {} -> mkVarOccFS (fsLit "df")
newCoercionHole :: TcPredType -> TcM CoercionHole
newCoercionHole pred_ty
= do { co_var <- newEvVar pred_ty
; traceTc "New coercion hole:" (ppr co_var)
; ref <- newMutVar Nothing
; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
= do {
#if defined(DEBUG)
; cts <- readTcRef ref
; whenIsJust cts $ \old_co ->
pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
#endif
; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
; writeTcRef ref (Just co) }
isFilledCoercionHole :: CoercionHole -> TcM Bool
isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
unpackCoercionHole :: CoercionHole -> TcM Coercion
unpackCoercionHole hole
= do { contents <- unpackCoercionHole_maybe hole
; case contents of
Just co -> return co
Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
checkCoercionHole cv co
| debugIsOn
= do { cv_ty <- zonkTcType (varType cv)
; return $
ASSERT2( ok cv_ty
, (text "Bad coercion hole" <+>
ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
, ppr cv_ty ]) )
co }
| otherwise
= return co
where
(Pair t1 t2, role) = coercionKindRole co
ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
= t1 `eqType` cv_t1
&& t2 `eqType` cv_t2
&& role == eqRelRole cv_rel
| otherwise
= False
newInferExpTypeNoInst :: TcM ExpSigmaType
newInferExpTypeNoInst = newInferExpType False
newInferExpTypeInst :: TcM ExpRhoType
newInferExpTypeInst = newInferExpType True
newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
= do { u <- newUnique
; tclvl <- getTcLevel
; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
; ref <- newMutVar Nothing
; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
, ir_ref = ref, ir_inst = inst })) }
readExpType_maybe :: ExpType -> TcM (Maybe TcType)
readExpType_maybe (Check ty) = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
readExpType :: ExpType -> TcM TcType
readExpType exp_ty
= do { mb_ty <- readExpType_maybe exp_ty
; case mb_ty of
Just ty -> return ty
Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }
checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe (Check ty) = Just ty
checkingExpType_maybe _ = Nothing
checkingExpType :: String -> ExpType -> TcType
checkingExpType _ (Check ty) = ty
checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
tauifyExpType :: ExpType -> TcM ExpType
tauifyExpType (Check ty) = return (Check ty)
tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
; return (Check ty) }
expTypeToType :: ExpType -> TcM TcType
expTypeToType (Check ty) = return ty
expTypeToType (Infer inf_res) = inferResultToType inf_res
inferResultToType :: InferResult -> TcM Type
inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
, ir_ref = ref })
= do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
; writeMutVar ref (Just tau)
; traceTc "Forcing ExpType to be monomorphic:"
(ppr u <+> text ":=" <+> ppr tau)
; return tau }
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-> Id
-> TcM ([(Name, TcTyVar)], TcThetaType, TcType)
tcInstType inst_tyvars id
= case tcSplitForAllTys (idType id) of
([], rho) -> let
(theta, tau) = tcSplitPhiTy rho
in
return ([], theta, tau)
(tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
tv_prs = map tyVarName tyvars `zip` tyvars'
; return (tv_prs, theta, tau) }
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
tcSkolDFunType dfun
= do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
; return (map snd tv_prs, theta, tau) }
tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
= (extendTvSubstWithClone subst tv new_tv, new_tv)
where
kind = substTyUnchecked subst (tyVarKind tv)
new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX = tcInstSkolTyVars' False
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVars' overlappable subst tvs
= do { loc <- getSrcSpanM
; lvl <- getTcLevel
; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
mkTcSkolTyVar tc_lvl loc overlappable old_name kind
= do { uniq <- newUnique
; let name = mkInternalName uniq (getOccName old_name) loc
; return (mkTcTyVar name kind details) }
where
details = SkolemTv (pushTcLevel tc_lvl) overlappable
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
freshenTyVarBndrs = instSkolTyCoVars mk_tv
where
mk_tv old_name kind
= do { uniq <- newUnique
; return (mkTyVar (setNameUnique old_name uniq) kind) }
freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
where
mk_cv old_name kind
= do { uniq <- newUnique
; return (mkCoVar (setNameUnique old_name uniq) kind) }
type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
instSkolTyCoVars :: TcTyCoVarMaker gbl lcl -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
instSkolTyCoVarsX :: TcTyCoVarMaker gbl lcl
-> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
-> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
= do { new_tcv <- mk_tcv old_name kind
; let subst1 | isTyVar new_tcv
= extendTvSubstWithClone subst tycovar new_tcv
| otherwise
= extendCvSubstWithClone subst tycovar new_tcv
; return (subst1, new_tcv) }
where
old_name = tyVarName tycovar
kind = substTyUnchecked subst (tyVarKind tycovar)
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; tclvl <- getTcLevel
; let details = MetaTv { mtv_info = FlatSkolTv
, mtv_ref = ref
, mtv_tclvl = tclvl }
name = mkMetaTyVarName uniq (fsLit "fsk")
; return (mkTcTyVar name (typeKind fam_ty) details) }
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
= do { details <- newMetaDetails SigTv
; let tyvar = mkTcTyVar name kind details
; traceTc "newSigTyVar" (ppr tyvar)
; return tyvar }
newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
newSkolemTyVar name kind = do { lvl <- getTcLevel
; return (mkTcTyVar name kind (SkolemTv lvl False)) }
newFmvTyVar :: TcType -> TcM TcTyVar
newFmvTyVar fam_ty
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; tclvl <- getTcLevel
; let details = MetaTv { mtv_info = FlatMetaTv
, mtv_ref = ref
, mtv_tclvl = tclvl }
name = mkMetaTyVarName uniq (fsLit "s")
; return (mkTcTyVar name (typeKind fam_ty) details) }
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
= do { ref <- newMutVar Flexi
; tclvl <- getTcLevel
; return (MetaTv { mtv_info = info
, mtv_ref = ref
, mtv_tclvl = tclvl }) }
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
= ASSERT( isTcTyVar tv )
do { uniq <- newUnique
; ref <- newMutVar Flexi
; let name' = setNameUnique (tyVarName tv) uniq
details' = case tcTyVarDetails tv of
details@(MetaTv {}) -> details { mtv_ref = ref }
_ -> pprPanic "cloneMetaTyVar" (ppr tv)
tyvar = mkTcTyVar name' (tyVarKind tv) details'
; traceTc "cloneMetaTyVar" (ppr tyvar)
; return tyvar }
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTyVarRef tyvar)
isFilledMetaTyVar :: TyVar -> TcM Bool
isFilledMetaTyVar tv
| MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
= do { details <- readMutVar ref
; return (isIndirect details) }
| otherwise = return False
isUnfilledMetaTyVar :: TyVar -> TcM Bool
isUnfilledMetaTyVar tv
| MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
= do { details <- readMutVar ref
; return (isFlexi details) }
| otherwise = return False
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
writeMetaTyVar tyvar ty
| not debugIsOn
= writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
| not (isTcTyVar tyvar)
= WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
return ()
| MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
= writeMetaTyVarRef tyvar ref ty
| otherwise
= WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
return ()
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
writeMetaTyVarRef tyvar ref ty
| not debugIsOn
= do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
<+> text ":=" <+> ppr ty)
; writeTcRef ref (Indirect ty) }
| otherwise
= do { meta_details <- readMutVar ref;
; zonked_tv_kind <- zonkTcType tv_kind
; zonked_ty <- zonkTcType ty
; let zonked_ty_kind = typeKind zonked_ty
kind_check_ok = tcIsConstraintKind zonked_tv_kind
|| tcEqKind zonked_ty_kind zonked_tv_kind
kind_msg = hang (text "Ill-kinded update to meta tyvar")
2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
<+> text ":="
<+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )
; MASSERT2( level_check_ok, level_check_msg )
; MASSERT2( kind_check_ok, kind_msg )
; writeMutVar ref (Indirect ty) }
where
tv_kind = tyVarKind tyvar
tv_lvl = tcTyVarLevel tyvar
ty_lvl = tcTypeLevel ty
level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl)
level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty
double_upd_msg details = hang (text "Double update of meta tyvar")
2 (ppr tyvar $$ ppr details)
genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
-> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
genInstSkolTyVarsX loc subst tvs
= instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
mkMetaTyVarName :: Unique -> FastString -> Name
mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
newAnonMetaTyVar meta_info kind
= do { uniq <- newUnique
; let name = mkMetaTyVarName uniq s
s = case meta_info of
TauTv -> fsLit "t"
FlatMetaTv -> fsLit "fmv"
FlatSkolTv -> fsLit "fsk"
SigTv -> fsLit "a"
; details <- newMetaDetails meta_info
; let tyvar = mkTcTyVar name kind details
; traceTc "newAnonMetaTyVar" (ppr tyvar)
; return tyvar }
cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
cloneAnonMetaTyVar info tv kind
= do { uniq <- newUnique
; details <- newMetaDetails info
; let name = mkSystemName uniq (getOccName tv)
tyvar = mkTcTyVar name kind details
; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
; return tyvar }
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
newFlexiTyVarTy :: Kind -> TcM TcType
newFlexiTyVarTy kind = do
tc_tyvar <- newFlexiTyVar kind
return (mkTyVarTy tc_tyvar)
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
= do { rr <- newFlexiTyVarTy runtimeRepTy
; return (tYPE rr) }
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
= do { kind <- newOpenTypeKind
; newFlexiTyVarTy kind }
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX subst tv
= do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
new_meta_tv_x info subst tv
= do { new_tv <- cloneAnonMetaTyVar info tv substd_kind
; let subst1 = extendTvSubstWithClone subst tv new_tv
; return (subst1, new_tv) }
where
substd_kind = substTyUnchecked subst (tyVarKind tv)
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; let name = mkMetaTyVarName uniq (fsLit "p")
details = MetaTv { mtv_info = TauTv
, mtv_ref = ref
, mtv_tclvl = tc_lvl }
; return (mkTyVarTy (mkTcTyVar name kind details)) }
quantifyTyVars
:: TcTyCoVarSet
-> CandidatesQTvs
-> TcM [TcTyVar]
quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
= do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
; let dep_kvs = dVarSetElemsWellScoped $
dep_tkvs `dVarSetMinusVarSet` gbl_tvs
nondep_tvs = dVarSetElems $
(nondep_tkvs `minusDVarSet` dep_tkvs)
`dVarSetMinusVarSet` gbl_tvs
; poly_kinds <- xoptM LangExt.PolyKinds
; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
; let final_qtvs = dep_kvs' ++ nondep_tvs'
; traceTc "quantifyTyVars"
(vcat [ text "globals:" <+> ppr gbl_tvs
, text "nondep:" <+> pprTyVars nondep_tvs
, text "dep:" <+> pprTyVars dep_kvs
, text "dep_kvs'" <+> pprTyVars dep_kvs'
, text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
; let co_vars = filter isCoVar final_qtvs
; MASSERT2( null co_vars, ppr co_vars )
; return final_qtvs }
where
zonk_quant default_kind tkv
| not (isTyVar tkv)
= return Nothing
| not (isTcTyVar tkv)
= return (Just tkv)
| otherwise
= do { deflt_done <- defaultTyVar default_kind tkv
; case deflt_done of
True -> return Nothing
False -> do { tv <- zonkQuantifiedTyVar tkv
; return (Just tv) } }
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
zonkQuantifiedTyVar tv
= case tcTyVarDetails tv of
SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
; return (setTyVarKind tv kind) }
MetaTv {} -> skolemiseUnboundMetaTyVar tv
_other -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
defaultTyVar :: Bool
-> TcTyVar
-> TcM Bool
defaultTyVar default_kind tv
| not (isMetaTyVar tv)
= return False
| isSigTyVar tv
= return False
| isRuntimeRepVar tv
= do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
; writeMetaTyVar tv liftedRepTy
; return True }
| default_kind
= do { default_kind_var tv
; return True }
| otherwise
= return False
where
default_kind_var :: TyVar -> TcM ()
default_kind_var kv
| isLiftedTypeKind (tyVarKind kv)
= do { traceTc "Defaulting a kind var to *" (ppr kv)
; writeMetaTyVar kv liftedTypeKind }
| otherwise
= addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
, text "of kind:" <+> ppr (tyVarKind kv')
, text "Perhaps enable PolyKinds or add a kind signature" ])
where
(_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar
skolemiseRuntimeUnk tv
= skolemise_tv tv RuntimeUnk
skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
skolemiseUnboundMetaTyVar tv
= skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False)
skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar
skolemise_tv tv details
= ASSERT2( isMetaTyVar tv, ppr tv )
do { when debugIsOn (check_empty tv)
; span <- getSrcSpanM
; kind <- zonkTcType (tyVarKind tv)
; let uniq = getUnique tv
tv_name = getOccName tv
final_name = mkInternalName uniq tv_name span
final_tv = mkTcTyVar final_name kind details
; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
where
check_empty tv
= when debugIsOn $
do { cts <- readMetaTyVar tv
; case cts of
Flexi -> return ()
Indirect ty -> WARN( True, ppr tv $$ ppr ty )
return () }
tcGetGlobalTyCoVars :: TcM TcTyVarSet
tcGetGlobalTyCoVars
= do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
; gbl_tvs <- readMutVar gtv_var
; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
; writeMutVar gtv_var gbl_tvs'
; return gbl_tvs' }
zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
zonkTcTypeAndFV ty
= tyCoVarsOfTypeDSet <$> zonkTcType ty
zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
zonkTcTypeAndSplitDepVars ty
= candidateQTyVarsOfType <$> zonkTcType ty
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
zonkTcTypesAndSplitDepVars tys
= candidateQTyVarsOfTypes <$> mapM zonkTcType tys
zonkTyCoVar :: TyCoVar -> TcM TcType
zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
| isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
| otherwise = ASSERT2( isCoVar tv, ppr tv )
mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
zonkTyCoVarsAndFV tycovars =
tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars)
zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar]
zonkTyCoVarsAndFVList tycovars =
tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
; return (setTyVarKind tv kind') }
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mapM zonkTcType tys
zonkImplication :: Implication -> TcM Implication
zonkImplication implic@(Implic { ic_skols = skols
, ic_given = given
, ic_wanted = wanted
, ic_info = info })
= do { skols' <- mapM zonkTcTyCoVarBndr skols
; given' <- mapM zonkEvVar given
; info' <- zonkSkolemInfo info
; wanted' <- zonkWCRec wanted
; return (implic { ic_skols = skols'
, ic_given = given'
, ic_wanted = wanted'
, ic_info = info' }) }
zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
; return (setVarType var ty') }
zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC wc = zonkWCRec wc
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
= do { simple' <- zonkSimples simple
; implic' <- mapBagM zonkImplication implic
; return (WC { wc_simple = simple', wc_impl = implic' }) }
zonkSimples :: Cts -> TcM Cts
zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
; traceTc "zonkSimples done:" (ppr cts')
; return cts' }
zonkCt' :: Ct -> TcM Ct
zonkCt' ct = zonkCt ct
zonkCt :: Ct -> TcM Ct
zonkCt ct@(CHoleCan { cc_ev = ev })
= do { ev' <- zonkCtEvidence ev
; return $ ct { cc_ev = ev' } }
zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
= do { ev' <- zonkCtEvidence ev
; args' <- mapM zonkTcType args
; return $ ct { cc_ev = ev', cc_tyargs = args' } }
zonkCt ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs })
= do { ev' <- zonkCtEvidence ev
; tv_ty' <- zonkTcTyVar tv
; case getTyVar_maybe tv_ty' of
Just tv' -> do { rhs' <- zonkTcType rhs
; return ct { cc_ev = ev'
, cc_tyvar = tv'
, cc_rhs = rhs' } }
Nothing -> return (mkNonCanonical ev') }
zonkCt ct@(CIrredCan { cc_ev = ev })
= do { ev' <- zonkCtEvidence ev
; return (ct { cc_ev = ev' }) }
zonkCt ct
= ASSERT( not (isCFunEqCan ct) )
do { fl' <- zonkCtEvidence (ctEvidence ct)
; return (mkNonCanonical fl') }
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred'}) }
zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
= do { pred' <- zonkTcType pred
; let dest' = case dest of
EvVarDest ev -> EvVarDest $ setVarType ev pred'
HoleDest h -> HoleDest h
; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred' }) }
zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty
; return (SigSkol cx ty' tv_prs) }
zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
; return (InferSkol ntys') }
where
do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
zonkSkolemInfo skol_info = return skol_info
zonkId :: TcId -> TcM TcId
zonkId id
= do { ty' <- zonkTcType (idType id)
; return (Id.setIdType id ty') }
zonkCoVar :: CoVar -> TcM CoVar
zonkCoVar = zonkId
zonkTcTypeMapper :: TyCoMapper () TcM
zonkTcTypeMapper = TyCoMapper
{ tcm_smart = True
, tcm_tyvar = const zonkTcTyVar
, tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
, tcm_hole = hole
, tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv
, tcm_tycon = return }
where
hole :: () -> CoercionHole -> TcM Coercion
hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
= do { contents <- readTcRef ref
; case contents of
Just co -> do { co' <- zonkCo co
; checkCoercionHole cv co' }
Nothing -> do { cv' <- zonkCoVar cv
; return $ HoleCo (hole { ch_co_var = cv' }) } }
zonkTcType :: TcType -> TcM TcType
zonkTcType = mapType zonkTcTypeMapper ()
zonkCo :: Coercion -> TcM Coercion
zonkCo = mapCoercion zonkTcTypeMapper ()
zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
zonkTcTyCoVarBndr tyvar
| isSigTyVar tyvar
= tcGetTyVar "zonkTcTyCoVarBndr SigTv" <$> zonkTcTyVar tyvar
| otherwise
= ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar )
updateTyVarKindM zonkTcType tyvar
zonkTcTyVarBinder :: TyVarBndr TcTyVar vis -> TcM (TyVarBndr TcTyVar vis)
zonkTcTyVarBinder (TvBndr tv vis)
= do { tv' <- zonkTcTyCoVarBndr tv
; return (TvBndr tv' vis) }
zonkTcTyVar :: TcTyVar -> TcM TcType
zonkTcTyVar tv
| isTcTyVar tv
= case tcTyVarDetails tv of
SkolemTv {} -> zonk_kind_and_return
RuntimeUnk {} -> zonk_kind_and_return
MetaTv { mtv_ref = ref }
-> do { cts <- readMutVar ref
; case cts of
Flexi -> zonk_kind_and_return
Indirect ty -> zonkTcType ty }
| otherwise
= zonk_kind_and_return
where
zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
; return (mkTyVarTy z_tv) }
zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
zonkTcTyVarToTyVar tv
= do { ty <- zonkTcTyVar tv
; let tv' = case tcGetTyVar_maybe ty of
Just tv' -> tv'
Nothing -> pprPanic "zonkTcTyVarToTyVar"
(ppr tv $$ ppr ty)
; return tv' }
zonkSigTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
zonkSigTyVarPairs prs
= mapM do_one prs
where
do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
; return (nm, tv') }
zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType env ty = do { ty' <- zonkTcType ty
; return (tidyOpenType env ty') }
zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
zonkTidyTcTypes = zonkTidyTcTypes' []
where zonkTidyTcTypes' zs env [] = return (env, reverse zs)
zonkTidyTcTypes' zs env (ty:tys)
= do { (env', ty') <- zonkTidyTcType env ty
; zonkTidyTcTypes' (ty':zs) env' tys }
zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin env (GivenOrigin skol_info)
= do { skol_info1 <- zonkSkolemInfo skol_info
; let skol_info2 = tidySkolemInfo env skol_info1
; return (env, GivenOrigin skol_info2) }
zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
, uo_expected = exp })
= do { (env1, act') <- zonkTidyTcType env act
; (env2, exp') <- zonkTidyTcType env1 exp
; return ( env2, orig { uo_actual = act'
, uo_expected = exp' }) }
zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
= do { (env1, ty1') <- zonkTidyTcType env ty1
; (env2, m_ty2') <- case m_ty2 of
Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
Nothing -> return (env1, Nothing)
; (env3, orig') <- zonkTidyOrigin env2 orig
; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
= do { (env1, p1') <- zonkTidyTcType env p1
; (env2, p2') <- zonkTidyTcType env1 p2
; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
= do { (env1, p1') <- zonkTidyTcType env p1
; (env2, p2') <- zonkTidyTcType env1 p2
; (env3, o1') <- zonkTidyOrigin env2 o1
; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
zonkTidyOrigin env orig = return (env, orig)
tidyCt :: TidyEnv -> Ct -> Ct
tidyCt env ct
= case ct of
CHoleCan { cc_ev = ev }
-> ct { cc_ev = tidy_ev env ev }
_ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
where
tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
tidy_ev env ctev@(CtGiven { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidy_ev env ctev@(CtWanted { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidy_ev env ctev@(CtDerived { ctev_pred = pred })
= ctev { ctev_pred = tidyType env pred }
tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty)
tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
tidySkolemInfo _ info = info
tidySigSkol :: TidyEnv -> UserTypeCtxt
-> TcType -> [(Name,TcTyVar)] -> SkolemInfo
tidySigSkol env cx ty tv_prs
= SigSkol cx (tidy_ty env ty) tv_prs'
where
tv_prs' = mapSnd (tidyTyVarOcc env) tv_prs
inst_env = mkNameEnv tv_prs'
tidy_ty env (ForAllTy (TvBndr tv vis) ty)
= ForAllTy (TvBndr tv' vis) (tidy_ty env' ty)
where
(env', tv') = tidy_tv_bndr env tv
tidy_ty env (FunTy arg res)
= FunTy (tidyType env arg) (tidy_ty env res)
tidy_ty env ty = tidyType env ty
tidy_tv_bndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidy_tv_bndr env@(occ_env, subst) tv
| Just tv' <- lookupNameEnv inst_env (tyVarName tv)
= ((occ_env, extendVarEnv subst tv tv'), tv')
| otherwise
= tidyTyCoVarBndr env tv
ensureNotLevPoly :: Type
-> SDoc
-> TcM ()
ensureNotLevPoly ty doc
= whenNoErrs $
checkForLevPoly doc ty
checkForLevPoly :: SDoc -> Type -> TcM ()
checkForLevPoly = checkForLevPolyX addErr
checkForLevPolyX :: Monad m
=> (SDoc -> m ())
-> SDoc -> Type -> m ()
checkForLevPolyX add_err extra ty
| isTypeLevPoly ty
= add_err (formatLevPolyErr ty $$ extra)
| otherwise
= return ()
formatLevPolyErr :: Type
-> SDoc
formatLevPolyErr ty
= hang (text "A levity-polymorphic type is not allowed here:")
2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty
, text "Kind:" <+> pprWithTYPE tidy_ki ])
where
(tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
tidy_ki = tidyType tidy_env (typeKind ty)