newWantedCoVar, writeWantedCoVar, readWantedCoVar,
newIP, newDict, newSelfDict, isSelfDict,
- newWantedEvVar, newWantedEvVars,
- newKindConstraint,
+ newWantedEvVar, newWantedEvVars,
newTcEvBinds, addTcEvBind,
--------------------------------
-- Instantiation
tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
- tcInstType, tcInstSigType,
+ tcInstType, tcInstSigType, instMetaTyVar,
tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars,
--------------------------------
-- Zonking
zonkType, mkZonkTcTyVar, zonkTcPredType,
- zonkTcTypeCarefully,
+ zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKindToKind, zonkTcKind,
zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
+ zonkTcTypeAndSubst,
tcGetGlobalTyVars,
readKindVar, writeKindVar
newWantedCoVar :: TcType -> TcType -> TcM CoVar
newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
--- We used to create a mutable co-var
-{-
--- A wanted coercion variable is a MetaTyVar
--- that can be filled in with its binding
- = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; let name = mkSysTvName uniq (fsLit "c")
- kind = mkPredTy (EqPred ty1 ty2)
- ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
--}
-
--------------
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
; return (mkInternalName uniq occ loc) }
-----------------
-newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
--- Create a new wanted CoVar that constrains the type
--- to have the specified kind
-newKindConstraint ty kind
- = do { ty_k <- newFlexiTyVarTy kind
- ; co_var <- newWantedCoVar ty ty_k
- ; return (co_var, ty_k) }
-
------------------
newSelfDict :: Class -> [TcType] -> TcM DictId
-- Make a dictionary for "self". It behaves just like a normal DictId
-- except that it responds True to isSelfDict
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
newMetaTyVar meta_info kind
- = do { uniq <- newUnique
+ = do { uniq <- newMetaUnique
; ref <- newMutVar Flexi
; let name = mkSysTvName uniq fs
fs = case meta_info of
TauTv -> fsLit "t"
+ TcsTv -> fsLit "u"
SigTv _ -> fsLit "a"
; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
-- Make a new meta tyvar whose Name and Kind
-- come from an existing TyVar
instMetaTyVar meta_info tyvar
- = do { uniq <- newUnique
+ = do { uniq <- newMetaUnique
; ref <- newMutVar Flexi
; let name = setNameUnique (tyVarName tyvar) uniq
kind = tyVarKind tyvar
tcGetGlobalTyVars
= do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
; gbl_tvs <- readMutVar gtv_var
- ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs)
+ ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
; writeMutVar gtv_var gbl_tvs'
; return gbl_tvs' }
\end{code}
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
-zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
+zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
----------------- Types
zonkTcTypeCarefully :: TcType -> TcM TcType
+-- Do not zonk type variables free in the environment
zonkTcTypeCarefully ty
= do { env_tvs <- tcGetGlobalTyVars
- ; zonkType (zonkTcTyVarCarefully env_tvs) ty }
-
-
-zonkTcTyVarCarefully :: TcTyVarSet -> TcTyVar -> TcM TcType
--- Do not zonk type variables free in the environment
-zonkTcTyVarCarefully env_tvs tv
- | tv `elemVarSet` env_tvs
- = return (TyVarTy tv)
- | otherwise
- = ASSERT( isTcTyVar tv )
- case tcTyVarDetails tv of
- SkolemTv {} -> return (TyVarTy tv)
- FlatSkol ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
- Flexi -> return (TyVarTy tv)
- Indirect ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty }
+ ; zonkType (zonk_tv env_tvs) ty }
+ where
+ zonk_tv env_tvs tv
+ | tv `elemVarSet` env_tvs
+ = return (TyVarTy tv)
+ | otherwise
+ = ASSERT( isTcTyVar tv )
+ case tcTyVarDetails tv of
+ SkolemTv {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> return (TyVarTy tv)
+ Indirect ty -> zonkType (zonk_tv env_tvs) ty }
zonkTcType :: TcType -> TcM TcType
-- Simply look through all Flexis
SkolemTv {} -> return (TyVarTy tv)
FlatSkol ty -> zonkTcType ty
MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
- Flexi -> return (TyVarTy tv)
- Indirect ty -> zonkTcType ty }
+ ; case cts of
+ Flexi -> return (TyVarTy tv)
+ Indirect ty -> zonkTcType ty }
+
+zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
+-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
+zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
+ where
+ zonk_tv tv
+ = case tcTyVarDetails tv of
+ SkolemTv {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkType zonk_tv ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> zonk_flexi tv
+ Indirect ty -> zonkType zonk_tv ty }
+ zonk_flexi tv
+ = case lookupTyVar subst tv of
+ Just ty -> zonkType zonk_tv ty
+ Nothing -> return (TyVarTy tv)
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mapM zonkTcType tys
zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
--- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
---
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
-- default their kind (e.g. from OpenTypeKind to TypeKind)
--
-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
- | ASSERT2( isTcTyVar tv, ppr tv )
- isSkolemTyVar tv
- = do { kind <- zonkTcType (tyVarKind tv)
- ; return $ setTyVarKind tv kind
- }
+ = ASSERT2( isTcTyVar tv, ppr tv )
+ case tcTyVarDetails tv of
+ FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
+ SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+ ; return $ setTyVarKind tv kind }
-- It might be a skolem type variable,
-- for example from a user type signature
- | otherwise -- It's a meta-type-variable
- = do { details <- readMetaTyVar tv
-
- -- Create the new, frozen, skolem type variable
- -- We zonk to a skolem, not to a regular TcVar
- -- See Note [Zonking to Skolem]
+ MetaTv _ _ref ->
+#ifdef DEBUG
+ -- [Sept 04] Check for non-empty.
+ -- See note [Silly Type Synonym]
+ (readMutVar _ref >>= \cts ->
+ case cts of
+ Flexi -> return ()
+ Indirect ty -> WARN( True, ppr tv $$ ppr ty )
+ return ()) >>
+#endif
+ skolemiseUnboundMetaTyVar UnkSkol tv
+
+skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
+-- We have a Meta tyvar with a ref-cell inside it
+-- Skolemise it, including giving it a new Name, so that
+-- we are totally out of Meta-tyvar-land
+-- We create a skolem TyVar, not a regular TyVar
+-- See Note [Zonking to Skolem]
+skolemiseUnboundMetaTyVar skol_info tv
+ = ASSERT2( isMetaTyVar tv, ppr tv )
+ do { uniq <- newUnique -- Remove it from TcMetaTyVar unique land
; let final_kind = defaultKind (tyVarKind tv)
- final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
-
- -- Bind the meta tyvar to the new tyvar
- ; case details of
- Indirect ty -> WARN( True, ppr tv $$ ppr ty )
- return ()
- -- [Sept 04] I don't think this should happen
- -- See note [Silly Type Synonym]
-
- Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
-
- -- Return the new tyvar
+ final_name = setNameUnique (tyVarName tv) uniq
+ final_tv = mkSkolTyVar final_name final_kind skol_info
+ ; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
\end{code}
\begin{code}
zonkImplication :: Implication -> TcM Implication
-zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given
+zonkImplication implic@(Implic { ic_given = given
, ic_wanted = wanted })
- = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs)
- ; given' <- mapM zonkEvVar given
+ = do { given' <- mapM zonkEvVar given
; wanted' <- mapBagM zonkWanted wanted
- ; return (implic { ic_env_tvs = env_tvs', ic_given = given'
- , ic_wanted = wanted' }) }
+ ; return (implic { ic_given = given', ic_wanted = wanted' }) }
zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
-- type variable and zonks the kind too
-zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
- -- see zonkTcType, and zonkTcTypeToType
- -> TcType
- -> TcM Type
+zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
+ -> TcType -> TcM Type
zonkType zonk_tc_tyvar ty
= go ty
where
ty2' <- go ty2
return (EqPred ty1' ty2')
-mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
+mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
-> TcTyVar -> TcM TcType
mkZonkTcTyVar unbound_var_fn tyvar
= ASSERT( isTcTyVar tyvar )
case tcTyVarDetails tyvar of
- SkolemTv {} -> return (TyVarTy tyvar)
- FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
- Flexi -> unbound_var_fn tyvar
- Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
+ SkolemTv {} -> return (TyVarTy tyvar)
+ FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> unbound_var_fn tyvar
+ Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
-- Zonk the kind of a non-TC tyvar in case it is a coercion variable
-- (their kind contains types).
-- Checks that the type is valid for the given context
checkValidType ctxt ty = do
traceTc "checkValidType" (ppr ty)
- unboxed <- doptM Opt_UnboxedTuples
- rank2 <- doptM Opt_Rank2Types
- rankn <- doptM Opt_RankNTypes
- polycomp <- doptM Opt_PolymorphicComponents
+ unboxed <- xoptM Opt_UnboxedTuples
+ rank2 <- xoptM Opt_Rank2Types
+ rankn <- xoptM Opt_RankNTypes
+ polycomp <- xoptM Opt_PolymorphicComponents
let
gen_rank n | rankn = ArbitraryRank
| rank2 = Rank 2
checkTc (tyConArity tc <= length tys) arity_msg
-- See Note [Liberal type synonyms]
- ; liberal <- doptM Opt_LiberalTypeSynonyms
+ ; liberal <- xoptM Opt_LiberalTypeSynonyms
; if not liberal || isSynFamilyTyCon tc then
-- For H98 and synonym families, do check the type args
mapM_ (check_mono_type SynArgMonoType) tys
}
| isUnboxedTupleTyCon tc
- = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples
+ = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
- ; impred <- doptM Opt_ImpredicativeTypes
+ ; impred <- xoptM Opt_ImpredicativeTypes
; let rank' = if impred then ArbitraryRank else TyConArgMonoType
-- c.f. check_arg_type
-- However, args are allowed to be unlifted, or
-- Anyway, they are dealt with by a special case in check_tau_type
check_arg_type rank ty
- = do { impred <- doptM Opt_ImpredicativeTypes
+ = do { impred <- xoptM Opt_ImpredicativeTypes
; let rank' = case rank of -- Predictive => must be monotype
MustBeMonoType -> MustBeMonoType -- Monotype, regardless
_other | impred -> ArbitraryRank
check_pred_ty dflags _ pred@(EqPred ty1 ty2)
= do { -- Equational constraints are valid in all contexts if type
-- families are permitted
- ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+ ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
-- Check the form of the argument types
; checkValidMonoType ty1
-- checkInstTermination
_ -> flexible_contexts || all tyvar_head tys
where
- flexible_contexts = dopt Opt_FlexibleContexts dflags
- undecidable_ok = dopt Opt_UndecidableInstances dflags
+ flexible_contexts = xopt Opt_FlexibleContexts dflags
+ undecidable_ok = xopt Opt_UndecidableInstances dflags
-------------------------
tyvar_head :: Type -> Bool
check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
check_inst_head dflags clas tys
= do { -- If GlasgowExts then check at least one isn't a type variable
- ; checkTc (dopt Opt_TypeSynonymInstances dflags ||
+ ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
all tcInstHeadTyNotSynonym tys)
(instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
- ; checkTc (dopt Opt_FlexibleInstances dflags ||
+ ; checkTc (xopt Opt_FlexibleInstances dflags ||
all tcInstHeadTyAppAllTyVars tys)
(instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
- ; checkTc (dopt Opt_MultiParamTypeClasses dflags ||
+ ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
isSingleton tys)
(instTypeErr (pprClassPred clas tys) head_one_type_msg)
-- May not contain type family applications
do { (clas, inst_tys) <- setSrcSpan head_loc $
checkValidInstHead tau
- ; undecidable_ok <- doptM Opt_UndecidableInstances
+ ; undecidable_ok <- xoptM Opt_UndecidableInstances
; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
; checkValidMonoType rhs
-- we have a decidable instance unless otherwise permitted
- ; undecidable_ok <- doptM Opt_UndecidableInstances
+ ; undecidable_ok <- xoptM Opt_UndecidableInstances
; unless undecidable_ok $
mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
}
-- Size of a predicate
--
--- Equalities are a special case. The equality itself doesn't contribute to the
--- size and as we do not count class predicates, we have to start with one less.
--- This is easy to see considering that, given
--- class C a b | a -> b
--- type family F a
--- constraints (C a b) and (F a ~ b) are equivalent in size.
+-- We are considering whether *class* constraints terminate
+-- Once we get into an implicit parameter or equality we
+-- can't get back to a class constraint, so it's safe
+-- to say "size 0". See Trac #4200.
sizePred :: PredType -> Int
sizePred (ClassP _ tys') = sizeTypes tys'
-sizePred (IParam _ ty) = sizeType ty
-sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - 1
+sizePred (IParam {}) = 0
+sizePred (EqPred {}) = 0
\end{code}
projects / ghc-hetmet.git / blobdiff