module TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
newFlexiTyVar,
newFlexiTyVarTy,
newFlexiTyVarTys,
newOpenFlexiTyVarTy,
newMetaKindVar, newMetaKindVars,
cloneMetaTyVar,
newFmvTyVar, newFskTyVar,
readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
ExpType(..), ExpSigmaType, ExpRhoType,
mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe,
writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType,
tauifyExpType,
genInstSkolTyVarsX,
newEvVar, newEvVars, newDict,
newWanted, newWanteds,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
newTcEvBinds, addTcEvBind,
newCoercionHole, fillCoercionHole, isFilledCoercionHole,
unpackCoercionHole, unpackCoercionHole_maybe,
checkCoercionHole,
newMetaTyVars, newMetaTyVarX, newMetaSigTyVars,
newSigTyVar,
tcInstType,
tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
tcInstSigTyVarsLoc, tcInstSigTyVars,
tcInstSkolType,
tcSkolDFunType, tcSuperSkolTyVars,
instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
zonkTidyTcType, zonkTidyOrigin,
mkTypeErrorThing, mkTypeErrorThingArgs,
tidyEvVar, tidyCt, tidySkolemInfo,
skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType,
quantifyTyVars, quantifyZonkedTyVars,
defaultKindVar,
zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper,
zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
tcGetGlobalTyCoVars
) where
#include "HsVersions.h"
import TyCoRep
import TcType
import Type
import Kind
import Coercion
import Class
import Var
import TcRnMonad
import TcEvidence
import Id
import Name
import VarSet
import TysWiredIn
import TysPrim
import VarEnv
import PrelNames
import Util
import Outputable
import FastString
import SrcLoc
import Bag
import Pair
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Maybes
import Data.List ( mapAccumL, partition )
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
; 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
else EvVarDest <$> newEvVar pty
return $ CtWanted { ctev_dest = d
, ctev_pred = pty
, ctev_loc = loc }
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
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
; loc <- getCtLocM origin (Just t_or_k)
; emitSimple $ mkNonCanonical $
CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
; return (mkHoleCo hole role ty1 ty2) }
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_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 "cobox")
IrredPred _ -> mkVarOccFS (fsLit "irred")
newCoercionHole :: TcM CoercionHole
newCoercionHole
= do { u <- newUnique
; traceTc "New coercion hole:" (ppr u)
; ref <- newMutVar Nothing
; return $ CoercionHole u ref }
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
fillCoercionHole (CoercionHole u ref) co
= do {
#ifdef DEBUG
; cts <- readTcRef ref
; whenIsJust cts $ \old_co ->
pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
#endif
; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
; writeTcRef ref (Just co) }
isFilledCoercionHole :: CoercionHole -> TcM Bool
isFilledCoercionHole (CoercionHole _ 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 _ ref) = readTcRef ref
checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
checkCoercionHole co h r t1 t2
| debugIsOn
= do { t1 <- zonkTcType t1
; t2 <- zonkTcType t2
; let (Pair _t1 _t2, _role) = coercionKindRole co
; return $
ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
, (text "Bad coercion hole" <+>
ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
, ppr co, ppr t1, ppr t2
, ppr r ]) )
co }
| otherwise
= return co
newOpenInferExpType :: TcM ExpType
newOpenInferExpType
= do { rr <- newFlexiTyVarTy runtimeRepTy
; u <- newUnique
; tclvl <- getTcLevel
; let ki = tYPE rr
; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
; ref <- newMutVar Nothing
; return (Infer u tclvl ki ref) }
readExpType_maybe :: ExpType -> TcM (Maybe TcType)
readExpType_maybe (Check ty) = return (Just ty)
readExpType_maybe (Infer _ _ _ 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) }
writeExpType :: ExpType -> TcType -> TcM ()
writeExpType (Infer u tc_lvl ki ref) ty
| debugIsOn
= do { ki1 <- zonkTcType (typeKind ty)
; ki2 <- zonkTcType ki
; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
; lvl_now <- getTcLevel
; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now )
; cts <- readTcRef ref
; case cts of
Just already_there -> pprPanic "writeExpType"
(vcat [ ppr u
, ppr ty
, ppr already_there ])
Nothing -> write }
| otherwise
= write
where
write = do { traceTc "Filling ExpType" $
ppr u <+> text ":=" <+> ppr ty
; writeTcRef ref (Just ty) }
writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2)
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 exp_ty = do { ty <- expTypeToType exp_ty
; return (Check ty) }
expTypeToType :: ExpType -> TcM TcType
expTypeToType (Check ty) = return ty
expTypeToType (Infer u tc_lvl ki ref)
= do { uniq <- newUnique
; tv_ref <- newMutVar Flexi
; let details = MetaTv { mtv_info = TauTv
, mtv_ref = tv_ref
, mtv_tclvl = tc_lvl }
name = mkMetaTyVarName uniq (fsLit "t")
tau_tv = mkTcTyVar name ki details
tau = mkTyVarTy tau_tv
; writeMutVar ref (Just tau)
; traceTc "Forcing ExpType to be monomorphic:"
(ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau)
; return tau }
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-> TcType
-> TcM ([TcTyVar], TcThetaType, TcType)
tcInstType inst_tyvars ty
= case tcSplitForAllTys ty 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)
; return (tyvars', theta, tau) }
tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
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
tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
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
; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
mkTcSkolTyVar loc overlappable uniq old_name kind
= mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
kind
(SkolemTv overlappable)
tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
-> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
tcInstSigTyVars
= instSkolTyCoVars mk_tv
where
mk_tv uniq old_name kind
= mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
freshenTyVarBndrs = instSkolTyCoVars mk_tv
where
mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
where
mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
-> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
-> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
-> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
= do { uniq <- newUnique
; let new_tcv = mk_tcv uniq old_name kind
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
; let name = mkSysTvName uniq (fsLit "fsk")
; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
mkMetaTyVarName :: Unique -> FastString -> Name
mkMetaTyVarName uniq str = mkSysTvName uniq str
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
= do { details <- newMetaDetails SigTv
; return (mkTcTyVar name kind details) }
newFmvTyVar :: TcType -> TcM TcTyVar
newFmvTyVar fam_ty
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; cur_lvl <- getTcLevel
; let details = MetaTv { mtv_info = FlatMetaTv
, mtv_ref = ref
, mtv_tclvl = fmvTcLevel cur_lvl }
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)
; return (mkTcTyVar name' (tyVarKind tv) details') }
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef 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 (metaTvRef 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_kind <- zonkTcType ty_kind
; ASSERT2( isFlexi meta_details,
hang (text "Double update of meta tyvar")
2 (ppr tyvar $$ ppr meta_details) )
traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
; writeMutVar ref (Indirect ty)
; when ( not (isPredTy tv_kind)
&& not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
$ WARN( True, hang (text "Ill-kinded update to meta tyvar")
2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
<+> text ":="
<+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
(return ()) }
where
tv_kind = tyVarKind tyvar
ty_kind = typeKind ty
genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
-> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
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"
SigTv -> fsLit "a"
; details <- newMetaDetails meta_info
; return (mkTcTyVar name kind details) }
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)
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
= do { rr <- newFlexiTyVarTy runtimeRepTy
; newFlexiTyVarTy (tYPE rr) }
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
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
new_meta_tv_x info subst tyvar
= do { uniq <- newUnique
; details <- newMetaDetails info
; let name = mkSystemName uniq (getOccName tyvar)
kind = substTyUnchecked subst (tyVarKind tyvar)
new_tv = mkTcTyVar name kind details
subst1 = extendTvSubstWithClone subst tyvar new_tv
; return (subst1, new_tv) }
quantifyTyVars, quantifyZonkedTyVars
:: TcTyCoVarSet
-> Pair TcTyCoVarSet
-> TcM [TcTyVar]
quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
= do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
zonkTyCoVarsAndFV nondep_tkvs
; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
; quantifyZonkedTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs) }
quantifyZonkedTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
= do { let all_cvs = filterVarSet isCoVar $
dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
dep_kvs = varSetElemsWellScoped $
dep_tkvs `minusVarSet` gbl_tvs
`minusVarSet` (closeOverKinds all_cvs)
nondep_tvs = varSetElemsWellScoped $
nondep_tkvs `minusVarSet` gbl_tvs
; poly_kinds <- xoptM LangExt.PolyKinds
; dep_vars2 <- if poly_kinds
then return dep_kvs
else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
is_meta kv = isTcTyVar kv && isMetaTyVar kv
; mapM_ defaultKindVar meta_kvs
; return skolem_kvs }
; let quant_vars = dep_vars2 ++ nondep_tvs
; traceTc "quantifyTyVars"
(vcat [ text "globals:" <+> ppr gbl_tvs
, text "nondep:" <+> ppr nondep_tvs
, text "dep:" <+> ppr dep_kvs
, text "dep2:" <+> ppr dep_vars2
, text "quant_vars:" <+> ppr quant_vars ])
; mapMaybeM zonk_quant quant_vars }
where
zonk_quant tkv
| isTcTyVar tkv = zonkQuantifiedTyVar tkv
| otherwise = return $ Just tkv
zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
where left_only :: Either a b -> Maybe a
left_only (Left x) = Just x
left_only (Right _) = Nothing
zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
zonkQuantifiedTyVarOrType tv
= case tcTyVarDetails tv of
SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
; return $ Left $ setTyVarKind tv kind }
MetaTv { mtv_ref = ref } ->
do when debugIsOn $ do
cts <- readMutVar ref
case cts of
Flexi -> return ()
Indirect ty -> WARN( True, ppr tv $$ ppr ty )
return ()
if isRuntimeRepVar tv
then do { writeMetaTyVar tv ptrRepLiftedTy
; return (Right ptrRepLiftedTy) }
else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
_other -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
defaultKindVar :: TcTyVar -> TcM Kind
defaultKindVar kv
| ASSERT( isMetaTyVar kv )
isRuntimeRepVar kv
= writeMetaTyVar kv ptrRepLiftedTy >> return ptrRepLiftedTy
| isStarKind (tyVarKind kv)
= writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
| otherwise
= do { 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" ])
; return (mkTyVarTy kv) }
where
(_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
skolemiseUnboundMetaTyVar tv details
= ASSERT2( isMetaTyVar tv, ppr tv )
do { 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 }
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' }
zonkTcTypeInKnot :: TcType -> TcM TcType
zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
zonkTcTypeAndFV ty
= tyCoVarsOfType <$> zonkTcTypeInKnot ty
zonkTcTypeAndSplitDepVars :: TcType -> TcM (Pair TyCoVarSet)
zonkTcTypeAndSplitDepVars ty
= splitDepVarsOfType <$> zonkTcTypeInKnot ty
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM (Pair TyCoVarSet)
zonkTcTypesAndSplitDepVars tys
= splitDepVarsOfTypes <$> mapM zonkTcTypeInKnot 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 (varSetElems 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, wc_insol = insol })
= do { simple' <- zonkSimples simple
; implic' <- mapBagM zonkImplication implic
; insol' <- zonkSimples insol
; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
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
= do { fl' <- zonkCtEvidence (cc_ev 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) = do { ty <- readExpType ty
; ty' <- zonkTcType ty
; return (SigSkol cx (mkCheckExpType ty')) }
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') }
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 }
where
hole :: () -> CoercionHole -> Role -> Type -> Type
-> TcM Coercion
hole _ h r t1 t2
= do { contents <- unpackCoercionHole_maybe h
; case contents of
Just co -> do { co <- zonkCo co
; checkCoercionHole co h r t1 t2 }
Nothing -> do { t1 <- zonkTcType t1
; t2 <- zonkTcType t2
; return $ mkHoleCo h r t1 t2 } }
zonkTcType :: TcType -> TcM TcType
zonkTcType = mapType zonkTcTypeMapper ()
zonkCo :: Coercion -> TcM Coercion
zonkCo = mapCoercion zonkTcTypeMapper ()
zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
zonkTcTyCoVarBndr tyvar
= ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTvBndr tyvar )
updateTyVarKindM zonkTcType tyvar
zonkTcTyBinder :: TcTyBinder -> TcM TcTyBinder
zonkTcTyBinder (Anon ty) = Anon <$> zonkTcType ty
zonkTcTyBinder (Named tv vis) = Named <$> zonkTcTyCoVarBndr tv <*> pure vis
zonkTcTyVar :: TcTyVar -> TcM TcType
zonkTcTyVar tv
| isTcTyVar tv
= case tcTyVarDetails tv of
SkolemTv {} -> zonk_kind_and_return
RuntimeUnk {} -> zonk_kind_and_return
FlatSkol ty -> zonkTcType ty
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) }
zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType env ty = do { ty' <- zonkTcType ty
; return (tidyOpenType env ty') }
mkTypeErrorThing :: TcType -> ErrorThing
mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ repSplitAppTys ty)
zonkTidyTcType
mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
mkTypeErrorThingArgs ty num_args
= ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
zonkTidyTcType
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
, uo_thing = m_thing })
= do { (env1, act') <- zonkTidyTcType env act
; mb_exp <- readExpType_maybe exp
; (env2, exp') <- case mb_exp of
Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty
Nothing -> return (env1, exp)
; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
; return ( env3, orig { uo_actual = act'
, uo_expected = exp'
, uo_thing = m_thing' }) }
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)
zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
-> TcM (TidyEnv, Maybe ErrorThing)
zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
= do { (env', thing') <- zonker env thing
; return (env', Just $ ErrorThing thing' n_args zonker) }
zonkTidyErrorThing env Nothing
= return (env, Nothing)
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) = SigSkol cx (mkCheckExpType $
tidyType env $
checkingExpType "tidySkolemInfo" ty)
tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty)
tidySkolemInfo _ info = info