module TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
newFlexiTyVar,
newFlexiTyVarTy,
newFlexiTyVarTys,
newReturnTyVar, newReturnTyVarTy,
newMetaKindVar, newMetaKindVars,
mkTcTyVarName, cloneMetaTyVar,
newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
newEvVar, newEvVars, newEq, newDict,
newTcEvBinds, addTcEvBind,
newSimpleWanted, newSimpleWanteds,
tcInstTyVars, newSigTyVar,
tcInstType,
tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
tcInstSigTyVarsLoc, tcInstSigTyVars,
tcInstSkolType,
tcSkolDFunType, tcSuperSkolTyVars,
instSkolTyVars, freshenTyVarBndrs,
zonkTcPredType, zonkTidyTcType, zonkTidyOrigin,
tidyEvVar, tidyCt, tidySkolemInfo,
skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
zonkQuantifiedTyVar, quantifyTyVars,
zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar,
zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
tcGetGlobalTyVars,
newWildcardVar, newWildcardVarMetaKind
) where
#include "HsVersions.h"
import TypeRep
import TcType
import Type
import Class
import Var
import VarEnv
import TcRnMonad
import Id
import Name
import VarSet
import PrelNames
import DynFlags
import Util
import Outputable
import FastString
import SrcLoc
import Bag
import Control.Monad
import Data.List ( partition, mapAccumL )
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 False)
; let kv = mkTcTyVar (mkKindName uniq) superKind 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 -> TcM EvVar
newEvVar ty = do { name <- newSysName (predTypeOccName ty)
; return (mkLocalId name ty) }
newEq :: TcType -> TcType -> TcM EvVar
newEq ty1 ty2
= do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
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")
TuplePred _ -> mkVarOccFS (fsLit "tup")
IrredPred _ -> mkVarOccFS (fsLit "irred")
newSimpleWanted :: CtOrigin -> PredType -> TcM Ct
newSimpleWanted orig pty
= do loc <- getCtLoc orig
v <- newEvVar pty
return $ mkNonCanonical $
CtWanted { ctev_evar = v
, ctev_pred = pty
, ctev_loc = loc }
newSimpleWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
newSimpleWanteds orig = mapM (newSimpleWanted orig)
tcInstType :: ([TyVar] -> TcM (TvSubst, [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 (substTy subst rho)
; return (tyvars', theta, tau) }
tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
= (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
where
kind = substTy subst (tyVarKind tv)
new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVars' False emptyTvSubst
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTvSubst
tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVars' overlappable subst tvs
= do { loc <- getSrcSpanM
; instSkolTyVarsX (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 (TvSubst, [TcTyVar])
tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
tcInstSigTyVars
= instSkolTyVars 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 (TvSubst, [TyVar])
freshenTyVarBndrs = instSkolTyVars mk_tv
where
mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
instSkolTyVars :: (Unique -> Name -> Kind -> TyVar)
-> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
instSkolTyVars mk_tv = instSkolTyVarsX mk_tv emptyTvSubst
instSkolTyVarsX :: (Unique -> Name -> Kind -> TyVar)
-> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
instSkolTyVarsX mk_tv = mapAccumLM (instSkolTyVarX mk_tv)
instSkolTyVarX :: (Unique -> Name -> Kind -> TyVar)
-> TvSubst -> TyVar -> TcRnIf gbl lcl (TvSubst, TyVar)
instSkolTyVarX mk_tv subst tyvar
= do { uniq <- newUnique
; let new_tv = mk_tv uniq old_name kind
; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
where
old_name = tyVarName tyvar
kind = substTy subst (tyVarKind tyvar)
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
newMetaTyVar meta_info kind
= do { uniq <- newUnique
; let name = mkTcTyVarName uniq s
s = case meta_info of
ReturnTv -> fsLit "r"
TauTv True -> fsLit "w"
TauTv False -> fsLit "t"
FlatMetaTv -> fsLit "fmv"
SigTv -> fsLit "a"
; details <- newMetaDetails meta_info
; return (mkTcTyVar name kind details) }
newNamedMetaTyVar :: Name -> MetaInfo -> Kind -> TcM TcTyVar
newNamedMetaTyVar name meta_info kind
= do { details <- newMetaDetails meta_info
; return (mkTcTyVar name kind details) }
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
= do { uniq <- newUnique
; let name' = setNameUnique name uniq
; details <- newMetaDetails SigTv
; return (mkTcTyVar name' kind 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') }
mkTcTyVarName :: Unique -> FastString -> Name
mkTcTyVarName uniq str = mkSysTvName uniq str
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef tyvar)
isFilledMetaTyVar :: TyVar -> TcM Bool
isFilledMetaTyVar tv
| not (isTcTyVar tv) = return False
| MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
= do { details <- readMutVar ref
; return (isIndirect details) }
| otherwise = return False
isUnfilledMetaTyVar :: TyVar -> TcM Bool
isUnfilledMetaTyVar tv
| not (isTcTyVar tv) = return False
| 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 <+> text ":=" <+> ppr ty)
; writeMutVar ref (Indirect ty) }
| otherwise
= do { meta_details <- readMutVar ref;
; zonked_tv_kind <- zonkTcKind tv_kind
; zonked_ty_kind <- zonkTcKind 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 `tcIsSubKind` 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
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newMetaTyVar (TauTv False) kind
newFlexiTyVarTy :: Kind -> TcM TcType
newFlexiTyVarTy kind = do
tc_tyvar <- newFlexiTyVar kind
return (TyVarTy tc_tyvar)
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
newReturnTyVar :: Kind -> TcM TcTyVar
newReturnTyVar kind = newMetaTyVar ReturnTv kind
newReturnTyVarTy :: Kind -> TcM TcType
newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind
tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
tcInstTyVarX subst tyvar
= do { uniq <- newUnique
; details <- newMetaDetails (TauTv False)
; let name = mkSystemName uniq (getOccName tyvar)
kind = substTy subst (tyVarKind tyvar)
new_tv = mkTcTyVar name kind details
; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
quantifyTyVars gbl_tvs tkvs
= do { tkvs <- zonkTyVarsAndFV tkvs
; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
; let (kvs, tvs) = partitionVarSet isKindVar (closeOverKinds tkvs `minusVarSet` gbl_tvs)
kvs2 = varSetElems kvs
qtvs = varSetElems tvs
; poly_kinds <- xoptM Opt_PolyKinds
; qkvs <- if poly_kinds
then return kvs2
else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
is_meta kv = isTcTyVar kv && isMetaTyVar kv
; mapM_ defaultKindVarToStar meta_kvs
; return skolem_kvs }
; mapM zonk_quant (qkvs ++ qtvs) }
where
zonk_quant tkv
| isTcTyVar tkv = zonkQuantifiedTyVar tkv
| otherwise = return tkv
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
zonkQuantifiedTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
; return $ 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 ()
skolemiseUnboundMetaTyVar tv vanillaSkolemTv
_other -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
defaultKindVarToStar :: TcTyVar -> TcM Kind
defaultKindVarToStar kv
= do { ASSERT( isKindVar kv && isMetaTyVar kv )
writeMetaTyVar kv liftedTypeKind
; return liftedTypeKind }
skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
skolemiseUnboundMetaTyVar tv details
= ASSERT2( isMetaTyVar tv, ppr tv )
do { span <- getSrcSpanM
; uniq <- newUnique
; kind <- zonkTcKind (tyVarKind tv)
; let tv_name = getOccName tv
new_tv_name = if isWildcardVar tv
then generaliseWildcardVarName tv_name
else tv_name
final_name = mkInternalName uniq new_tv_name span
final_kind = defaultKind kind
final_tv = mkTcTyVar final_name final_kind details
; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
where
generaliseWildcardVarName :: OccName -> OccName
generaliseWildcardVarName name | startsWithUnderscore name
= mkOccNameFS (occNameSpace name) (appendFS (fsLit "w") (occNameFS name))
generaliseWildcardVarName name = name
tcGetGlobalTyVars :: TcM TcTyVarSet
tcGetGlobalTyVars
= do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
; gbl_tvs <- readMutVar gtv_var
; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
; writeMutVar gtv_var gbl_tvs'
; return gbl_tvs' }
where
zonkTcTypeAndFV :: TcType -> TcM TyVarSet
zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
zonkTyVar :: TyVar -> TcM TcType
zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
| otherwise = return (mkTyVarTy tv)
zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
zonkTyVarKind :: TyVar -> TcM TyVar
zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
; return (setTyVarKind tv kind') }
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mapM zonkTcType tys
zonkTcThetaType :: TcThetaType -> TcM TcThetaType
zonkTcThetaType theta = mapM zonkTcPredType theta
zonkTcPredType :: TcPredType -> TcM TcPredType
zonkTcPredType = zonkTcType
zonkImplication :: Implication -> TcM (Bag Implication)
zonkImplication implic@(Implic { ic_skols = skols
, ic_given = given
, ic_wanted = wanted
, ic_info = info })
= do { skols' <- mapM zonkTcTyVarBndr skols
; given' <- mapM zonkEvVar given
; info' <- zonkSkolemInfo info
; wanted' <- zonkWCRec wanted
; if isEmptyWC wanted'
then return emptyBag
else return $ unitBag $
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' <- flatMapBagM 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 })
= do { pred' <- zonkTcType pred
; return (ctev { ctev_pred = pred' }) }
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' <- zonkTcType ty
; return (SigSkol cx 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') }
zonkTcType :: TcType -> TcM TcType
zonkTcType ty
= go ty
where
go (TyConApp tc tys) = do tys' <- mapM go tys
return (TyConApp tc tys')
go (LitTy n) = return (LitTy n)
go (FunTy arg res) = do arg' <- go arg
res' <- go res
return (FunTy arg' res')
go (AppTy fun arg) = do fun' <- go fun
arg' <- go arg
return (mkAppTy fun' arg')
go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
| otherwise = TyVarTy <$> updateTyVarKindM go tyvar
go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
; ty' <- go ty
; return (ForAllTy tv' ty') }
zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
zonkTcTyVarBndr tyvar
= ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
updateTyVarKindM zonkTcType tyvar
zonkTcTyVar :: TcTyVar -> TcM TcType
zonkTcTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv ) do
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 }
where
zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
; return (TyVarTy z_tv) }
zonkTcKind :: TcKind -> TcM TcKind
zonkTcKind k = zonkTcType k
zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType env ty = do { ty' <- zonkTcType ty
; return (tidyOpenType env ty') }
zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin env (GivenOrigin skol_info)
= do { skol_info1 <- zonkSkolemInfo skol_info
; let (env1, skol_info2) = tidySkolemInfo env skol_info1
; return (env1, GivenOrigin skol_info2) }
zonkTidyOrigin env (TypeEqOrigin { uo_actual = act, uo_expected = exp })
= do { (env1, act') <- zonkTidyTcType env act
; (env2, exp') <- zonkTidyTcType env1 exp
; return ( env2, TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig)
= do { (env1, ty1') <- zonkTidyTcType env ty1
; (env2, ty2') <- zonkTidyTcType env1 ty2
; (env3, orig') <- zonkTidyOrigin env2 orig
; return (env3, KindEqOrigin ty1' ty2' orig') }
zonkTidyOrigin env (CoercibleOrigin ty1 ty2)
= do { (env1, ty1') <- zonkTidyTcType env ty1
; (env2, ty2') <- zonkTidyTcType env1 ty2
; return (env2, CoercibleOrigin ty1' ty2') }
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 -> (TidyEnv, SkolemInfo)
tidySkolemInfo env (SigSkol cx ty)
= (env', SigSkol cx ty')
where
(env', ty') = tidyOpenType env ty
tidySkolemInfo env (InferSkol ids)
= (env', InferSkol ids')
where
(env', ids') = mapAccumL do_one env ids
do_one env (name, ty) = (env', (name, ty'))
where
(env', ty') = tidyOpenType env ty
tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
= (env1, UnifyForAllSkol skol_tvs' ty')
where
env1 = tidyFreeTyVars env (tyVarsOfType ty `delVarSetList` skol_tvs)
(env2, skol_tvs') = tidyTyVarBndrs env1 skol_tvs
ty' = tidyType env2 ty
tidySkolemInfo env info = (env, info)
newWildcardVar :: Name -> Kind -> TcM TcTyVar
newWildcardVar name kind = newNamedMetaTyVar name (TauTv True) kind
newWildcardVarMetaKind :: Name -> TcM TcTyVar
newWildcardVarMetaKind name = do kind <- newMetaKindVar
newWildcardVar name kind
isWildcardVar :: TcTyVar -> Bool
isWildcardVar tv | isTcTyVar tv, MetaTv (TauTv True) _ _ <- tcTyVarDetails tv = True
isWildcardVar _ = False