zonkType, zonkTcPredType,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcKindToKind, zonkTcKind,
+ zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
readKindVar, writeKindVar
import FunDeps
import Name
import VarSet
+import ErrUtils
import DynFlags
import Util
+import Maybes
import ListSetOps
import UniqSupply
import Outputable
are used at the end of type checking
\begin{code}
+zonkTopTyVar :: TcTyVar -> TcM TcTyVar
+-- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
+-- to default the kind of ? and ?? etc to *. This is important to ensure that
+-- instance declarations match. For example consider
+-- instance Show (a->b)
+-- foo x = show (\_ -> True)
+-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
+-- and that won't match the typeKind (*) in the instance decl.
+--
+-- Because we are at top level, no further constraints are going to affect these
+-- type variables, so it's time to do it by hand. However we aren't ready
+-- to default them fully to () or whatever, because the type-class defaulting
+-- rules have yet to run.
+
+zonkTopTyVar tv
+ | k `eqKind` default_k = return tv
+ | otherwise
+ = do { tv' <- newFlexiTyVar default_k
+ ; writeMetaTyVar tv (mkTyVarTy tv')
+ ; return tv' }
+ where
+ k = tyVarKind tv
+ default_k = defaultKind k
+
zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
-- Check that instance inference will terminate (if we care)
-- For Haskell 98, checkValidTheta has already done that
; when (gla_exts && not undecidable_ok) $
- checkInstTermination theta inst_tys
+ mapM_ failWithTc (checkInstTermination inst_tys theta)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
}
where
- msg = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
+ msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+ undecidableMsg])
\end{code}
Termination test: each assertion in the context satisfies
\begin{code}
-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
- = do { mappM_ (check_nomore (fvTypes tys)) theta
- ; mappM_ (check_smaller (sizeTypes tys)) theta }
-
-check_nomore :: [TyVar] -> PredType -> TcM ()
-check_nomore fvs pred
- = checkTc (null (fvPred pred \\ fvs))
- (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
-
-check_smaller :: Int -> PredType -> TcM ()
-check_smaller n pred
- = checkTc (sizePred pred < n)
- (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+checkInstTermination :: [TcType] -> ThetaType -> [Message]
+checkInstTermination tys theta
+ = mapCatMaybes check theta
+ where
+ fvs = fvTypes tys
+ size = sizeTypes tys
+ check pred
+ | not (null (fvPred pred \\ fvs))
+ = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+ | sizePred pred >= size
+ = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+ | otherwise
+ = Nothing
predUndecErr pred msg = sep [msg,
nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]