mutable type variables
\begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
module TcMType (
TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, checkValidInstance, checkAmbiguity,
checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
- arityErr,
+ validDerivPred, arityErr,
--------------------------------
-- Zonking
(_,dups) = removeDups tcCmpPred theta
-------------------------
+check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
check_pred_ty dflags ctxt pred@(ClassP cls tys)
= do { -- Class predicates are valid in all contexts
; checkTc (arity == n_tys) arity_err
check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
-------------------------
+check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
check_class_pred_tys dflags ctxt tys
= case ctxt of
TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
complain pred = addErrTc (freeErr pred)
freeErr pred
- = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
- ptext SLIT("are already in scope"),
- nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
- ]
+ = sep [ ptext SLIT("All of the type variables in the constraint") <+>
+ quotes (pprPred pred)
+ , ptext SLIT("are already in scope") <+>
+ ptext SLIT("(at least one must be universally quantified here)")
+ , nest 4 $
+ ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
+ ]
\end{code}
\begin{code}
badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
$$
- parens (ptext SLIT("Use -ftype-families to permit this"))
+ parens (ptext SLIT("Use -XTypeFamilies to permit this"))
predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
%************************************************************************
%* *
-\subsection{Checking type instance well-formedness and termination}
+ Checking the context of a derived instance declaration
+%* *
+%************************************************************************
+
+Note [Exotic derived instance contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a 'derived' instance declaration, we *infer* the context. It's a
+bit unclear what rules we should apply for this; the Haskell report is
+silent. Obviously, constraints like (Eq a) are fine, but what about
+ data T f a = MkT (f a) deriving( Eq )
+where we'd get an Eq (f a) constraint. That's probably fine too.
+
+One could go further: consider
+ data T a b c = MkT (Foo a b c) deriving( Eq )
+ instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
+
+Notice that this instance (just) satisfies the Paterson termination
+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.
+
+However, this seems pretty exotic, and it's quite tricky to allow
+this, and yet give sensible error messages in the (much more common)
+case where we really want that instance decl for C.
+
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
+
+Here is another example:
+ data Fix f = In (f (Fix f)) deriving( Eq )
+Here, if we are prepared to allow -fallow-undecidable-instances we
+could derive the instance
+ instance Eq (f (Fix f)) => Eq (Fix f)
+but this is so delicate that I don't think it should happen inside
+'deriving'. If you want this, write it yourself!
+
+NB: if you want to lift this condition, make sure you still meet the
+termination conditions! If not, the deriving mechanism generates
+larger and larger constraints. Example:
+ data Succ a = S a
+ data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ. First we'll generate
+ instance (Show (Succ a), Show a) => Show (Seq a)
+and then
+ instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+and so on. Instead we want to complain of no instance for (Show (Succ a)).
+
+The bottom line
+~~~~~~~~~~~~~~~
+Allow constraints which consist only of type variables, with no repeats.
+
+\begin{code}
+validDerivPred :: PredType -> Bool
+validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
+ where fvs = fvTypes tys
+validDerivPred otehr = False
+\end{code}
+
+%************************************************************************
+%* *
+ Checking type instance well-formedness and termination
%* *
%************************************************************************
sizePred (ClassP _ tys') = sizeTypes tys'
sizePred (IParam _ ty) = sizeType ty
sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2
-
--- Type family instances occuring in a type after expanding synonyms
-tyFamInsts :: Type -> [(TyCon, [Type])]
-tyFamInsts ty
- | Just exp_ty <- tcView ty = tyFamInsts exp_ty
-tyFamInsts (TyVarTy _) = []
-tyFamInsts (TyConApp tc tys)
- | isOpenSynTyCon tc = [(tc, tys)]
- | otherwise = concat (map tyFamInsts tys)
-tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
-tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2
-tyFamInsts (ForAllTy _ ty) = tyFamInsts ty
\end{code}