--------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
- tcInstSigTyVars,
- tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
+ tcInstSigType,
+ tcInstSkolTyVars, tcInstSkolType,
+ tcSkolSigType, tcSkolSigTyVars, occurCheckErr, execTcTyVarBinds,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance,
- checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
+ checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkKinds,
checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
+ growPredTyVars, growTyVars, growThetaTyVars,
--------------------------------
-- Zonking
import Var
-- others:
-import TcRnMonad -- TcType, amongst others
+import HsSyn -- HsType
+import TcRnMonad -- TcType, amongst others
import FunDeps
import Name
import VarEnv
import ErrUtils
import DynFlags
import Util
+import Bag
import Maybes
import ListSetOps
import UniqSupply
--------------
+Execute a bag of type variable bindings.
+
+\begin{code}
+execTcTyVarBinds :: TcTyVarBinds -> TcM ()
+execTcTyVarBinds = mapM_ execTcTyVarBind . bagToList
+ where
+ execTcTyVarBind (TcTyVarBind tv ty)
+ = do { ASSERTM2( do { details <- readMetaTyVar tv
+ ; return (isFlexi details) }, ppr tv )
+ ; ty' <- if isCoVar tv
+ then return ty
+ else do { maybe_ty <- checkTauTvUpdate tv ty
+ ; case maybe_ty of
+ Nothing -> pprPanic "TcRnMonad.execTcTyBind"
+ (ppr tv <+> text ":=" <+> ppr ty)
+ Just ty' -> return ty'
+ }
+ ; writeMetaTyVar tv ty'
+ }
+\end{code}
+
Error mesages in case of kind mismatch.
\begin{code}
newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
newCoVars spec
= do { us <- newUniqueSupply
- ; return [ mkCoVar (mkSysTvName uniq (fsLit "co"))
+ ; return [ mkCoVar (mkSysTvName uniq (fsLit "co_kv"))
(mkCoKind ty1 ty2)
| ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
| tv <- tyvars ]
-tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: SkolemInfo -> (Name -> SrcSpan) -> TyVar -> TcM TcTyVar
-- Instantiate the tyvar, using
-- * the occ-name and kind of the supplied tyvar,
-- * the unique from the monad,
-- * the location either from the tyvar (mb_loc = Nothing)
-- or from mb_loc (Just loc)
-tcInstSkolTyVar info mb_loc tyvar
+tcInstSkolTyVar info get_loc tyvar
= do { uniq <- newUnique
; let old_name = tyVarName tyvar
kind = tyVarKind tyvar
- loc = mb_loc `orElse` getSrcSpan old_name
+ loc = get_loc old_name
new_name = mkInternalName uniq (nameOccName old_name) loc
; return (mkSkolTyVar new_name kind info) }
-- Get the location from the monad
tcInstSkolTyVars info tyvars
= do { span <- getSrcSpanM
- ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
+ ; mapM (tcInstSkolTyVar info (const span)) tyvars }
tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+
+tcInstSigType :: Bool -> SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigType use_skols skol_info ty
+ = tcInstType (mapM inst_tyvar) ty
+ where
+ inst_tyvar | use_skols = tcInstSkolTyVar skol_info getSrcSpan
+ | otherwise = instMetaTyVar (SigTv skol_info)
\end{code}
return ()
| otherwise
= ASSERT( isMetaTyVar tyvar )
- -- TOM: It should also work for coercions
- -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
- do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
+ ASSERT2( isCoVar tyvar || typeKind ty `isSubKind` tyVarKind tyvar,
+ (ppr tyvar <+> ppr (tyVarKind tyvar))
+ $$ (ppr ty <+> ppr (typeKind ty)) )
+ do { if debugIsOn then do { details <- readMetaTyVar tyvar;
+-- FIXME ; ASSERT2( not (isFlexi details), ppr tyvar )
+ ; WARN( not (isFlexi details), ppr tyvar )
+ return () }
+ else return ()
+
+ ; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty)
; writeMutVar (metaTvRef tyvar) (Indirect ty) }
- where
- _k1 = tyVarKind tyvar
- _k2 = typeKind ty
\end{code}
%************************************************************************
\begin{code}
-tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with skolems or meta SigTvs; depending on use_skols
--- Always take location info from the supplied tyvars
-tcInstSigTyVars use_skols skol_info tyvars
- | use_skols
- = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
-
- | otherwise
- = mapM (instMetaTyVar (SigTv skol_info)) tyvars
-
zonkSigTyVar :: TcTyVar -> TcM TcTyVar
zonkSigTyVar sig_tv
| isSkolemTyVar sig_tv
--
-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
- | ASSERT( isTcTyVar tv )
- isSkolemTyVar tv = return tv
+ | ASSERT2( isTcTyVar tv, ppr tv )
+ isSkolemTyVar tv
+ = do { kind <- zonkTcType (tyVarKind tv)
+ ; return $ setTyVarKind tv kind
+ }
-- It might be a skolem type variable,
-- for example from a user type signature
-- The two interesting cases!
go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
- | otherwise = return (TyVarTy tyvar)
+ | otherwise = liftM TyVarTy $
+ zonkTyVar unbound_var_fn tyvar
-- Ordinary (non Tc) tyvars occur inside quantified types
go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
ty' <- go ty
- return (ForAllTy tyvar ty')
+ tyvar' <- zonkTyVar unbound_var_fn tyvar
+ return (ForAllTy tyvar' ty')
go_pred (ClassP c tys) = do tys' <- mapM go tys
return (ClassP c tys')
ty2' <- go ty2
return (EqPred ty1' ty2')
-zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
+zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
-> TcTyVar -> TcM TcType
zonk_tc_tyvar unbound_var_fn tyvar
| not (isMetaTyVar tyvar) -- Skolems
; case cts of
Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
Indirect ty -> zonkType unbound_var_fn ty }
+
+-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their
+-- kind contains types).
+--
+zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
+ -> TyVar -> TcM TyVar
+zonkTyVar unbound_var_fn tv
+ | isCoVar tv
+ = do { kind <- zonkType unbound_var_fn (tyVarKind tv)
+ ; return $ setTyVarKind tv kind
+ }
+ | otherwise = return tv
\end{code}
| otherwise = Rank n
rank
= case ctxt of
- GenPatCtxt -> MustBeMonoType
DefaultDeclCtxt-> MustBeMonoType
ResSigCtxt -> MustBeMonoType
LamPatSigCtxt -> gen_rank 0
BindPatSigCtxt -> gen_rank 0
TySynCtxt _ -> gen_rank 0
+ GenPatCtxt -> gen_rank 1
+ -- This one is a bit of a hack
+ -- See the forall-wrapping in TcClassDcl.mkGenericInstance
+
ExprSigCtxt -> gen_rank 1
FunSigCtxt _ -> gen_rank 1
ConArgCtxt _ | polycomp -> gen_rank 2
-- We are given the type of the entire
-- constructor, hence rank 1
| otherwise -> gen_rank 1
+
ForSigCtxt _ -> gen_rank 1
SpecInstCtxt -> gen_rank 1
+ ThBrackCtxt -> gen_rank 1
actual_kind = typeKind ty
kind_ok = case ctxt of
TySynCtxt _ -> True -- Any kind will do
+ ThBrackCtxt -> True -- Any kind will do
ResSigCtxt -> isSubOpenTypeKind actual_kind
ExprSigCtxt -> isSubOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ubx_tup = case ctxt of
TySynCtxt _ | unboxed -> UT_Ok
ExprSigCtxt | unboxed -> UT_Ok
+ ThBrackCtxt | unboxed -> UT_Ok
_ -> UT_NotOk
- -- Check that the thing has kind Type, and is lifted if necessary
- checkTc kind_ok (kindErr actual_kind)
-
-- Check the internal validity of the type itself
check_type rank ubx_tup ty
+ -- Check that the thing has kind Type, and is lifted if necessary
+ -- Do this second, becuase we can't usefully take the kind of an
+ -- ill-formed type such as (a~Int)
+ checkTc kind_ok (kindErr actual_kind)
+
traceTc (text "checkValidType done" <+> ppr ty)
checkValidMonoType :: Type -> TcM ()
data Rank = ArbitraryRank -- Any rank ok
| MustBeMonoType -- Monotype regardless of flags
| TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
+ | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
| Rank Int -- Rank n, but could be more with -XRankNTypes
decRank :: Rank -> Rank -- Function arguments
where
(tvs, theta, tau) = tcSplitSigmaTy ty
--- Naked PredTys don't usually show up, but they can as a result of
--- {-# SPECIALISE instance Ord Char #-}
--- The Right Thing would be to fix the way that SPECIALISE instance pragmas
--- are handled, but the quick thing is just to permit PredTys here.
-check_type _ _ (PredTy sty)
- = do { dflags <- getDOpts
- ; check_pred_ty dflags TypeCtxt sty }
+-- Naked PredTys should, I think, have been rejected before now
+check_type _ _ ty@(PredTy {})
+ = failWithTc (text "Predicate used as a type:" <+> ppr ty)
check_type _ _ (TyVarTy _) = return ()
+
check_type rank _ (FunTy arg_ty res_ty)
= do { check_type (decRank rank) UT_NotOk arg_ty
; check_type rank UT_Ok res_ty }
; liberal <- doptM Opt_LiberalTypeSynonyms
; if not liberal || isOpenSynTyCon tc then
-- For H98 and synonym families, do check the type args
- mapM_ (check_mono_type TyConArgMonoType) tys
+ mapM_ (check_mono_type SynArgMonoType) tys
else -- In the liberal case (only for closed syns), expand then check
case tcView ty of
check_arg_type rank ty
= do { impred <- doptM Opt_ImpredicativeTypes
- ; let rank' = if impred then ArbitraryRank -- Arg of tycon can have arby rank, regardless
- else case rank of -- Predictive => must be monotype
- MustBeMonoType -> MustBeMonoType
- _ -> TyConArgMonoType
+ ; let rank' = case rank of -- Predictive => must be monotype
+ MustBeMonoType -> MustBeMonoType -- Monotype, regardless
+ _other | impred -> ArbitraryRank
+ | otherwise -> TyConArgMonoType
-- Make sure that MustBeMonoType is propagated,
-- so that we don't suggest -XImpredicativeTypes in
-- (Ord (forall a.a)) => a -> a
+ -- and so that if it Must be a monotype, we check that it is!
; check_type rank' UT_NotOk ty
; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
suggestion = case rank of
Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
+ SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
_ -> empty -- Polytype is always illegal
unliftedArgErr, ubxArgTyErr :: Type -> SDoc
arity_err = arityErr "Class" class_name arity n_tys
how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
+check_pred_ty _ (ClassSCCtxt _) (EqPred _ _)
+ = -- We do not yet support superclass equalities.
+ failWithTc $
+ sep [ ptext (sLit "The current implementation of type families does not")
+ , ptext (sLit "support equality constraints in superclass contexts.")
+ , ptext (sLit "They are planned for a future release.")
+ ]
+
check_pred_ty dflags _ pred@(EqPred ty1 ty2)
= do { -- Equational constraints are valid in all contexts if type
-- families are permitted
= mapM_ complain (filter is_ambig theta)
where
complain pred = addErrTc (ambigErr pred)
- extended_tau_vars = grow theta tau_tyvars
+ extended_tau_vars = growThetaTyVars theta tau_tyvars
-- See Note [Implicit parameters and ambiguity] in TcSimplify
is_ambig pred = isClassPred pred &&
= sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
ptext (sLit "must be reachable from the type after the '=>'"))]
+
+--------------------------
+-- For this 'grow' stuff see Note [Growing the tau-tvs using constraints] in Inst
+
+growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
+-- Finds a fixpoint
+growThetaTyVars theta tvs
+ | null theta = tvs
+ | otherwise = fixVarSet mk_next tvs
+ where
+ mk_next tvs = foldr growPredTyVars tvs theta
+
+
+growPredTyVars :: TcPredType -> TyVarSet -> TyVarSet
+-- Here is where the special case for inplicit parameters happens
+growPredTyVars (IParam _ ty) tvs = tvs `unionVarSet` tyVarsOfType ty
+growPredTyVars pred tvs = growTyVars (tyVarsOfPred pred) tvs
+
+growTyVars :: TyVarSet -> TyVarSet -> TyVarSet
+growTyVars new_tvs tvs
+ | new_tvs `intersectsVarSet` tvs = tvs `unionVarSet` new_tvs
+ | otherwise = tvs
\end{code}
In addition, GHC insists that at least one type variable
%* *
%************************************************************************
-
\begin{code}
-checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
-checkValidInstance tyvars theta clas inst_tys
- = do { undecidable_ok <- doptM Opt_UndecidableInstances
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
+ -> TcM (Class, [TcType])
+checkValidInstance hs_type tyvars theta tau
+ = setSrcSpan (getLoc hs_type) $
+ do { (clas, inst_tys) <- setSrcSpan head_loc $
+ checkValidInstHead tau
+
+ ; undecidable_ok <- doptM Opt_UndecidableInstances
; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
+
+ ; return (clas, inst_tys)
}
where
msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
undecidableMsg])
+
+ -- The location of the "head" of the instance
+ head_loc = case hs_type of
+ L _ (HsForAllTy _ _ _ (L loc _)) -> loc
+ L loc _ -> loc
\end{code}
Termination test: the so-called "Paterson conditions" (see Section 5 of
conditions. Then we *could* derive an instance decl like this:
instance (C Int a, Eq b, Eq c) => Eq (T a b c)
-
even though there is no instance for (C Int a), because there just
*might* be an instance for, say, (C Int Bool) at a site where we
need the equality instance for T's.
sizeTypes :: [Type] -> Int
sizeTypes xs = sum (map sizeType xs)
+-- 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.
sizePred :: PredType -> Int
sizePred (ClassP _ tys') = sizeTypes tys'
sizePred (IParam _ ty) = sizeType ty
-sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2
+sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - 1
\end{code}