--------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
- tcInstSigType,
+ tcInstType, tcInstSigType,
tcInstSkolTyVars, tcInstSkolType,
tcSkolSigType, tcSkolSigTyVars, occurCheckErr, execTcTyVarBinds,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
- SourceTyCtxt(..), checkValidTheta, checkFreeness,
+ SourceTyCtxt(..), checkValidTheta,
checkValidInstHead, checkValidInstance,
checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkKinds,
checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
import Var
-- others:
-import TcRnMonad -- TcType, amongst others
+import HsSyn -- HsType
+import TcRnMonad -- TcType, amongst others
import FunDeps
import Name
import VarEnv
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
- = return (TyVarTy tyvar)
-
- | otherwise -- Mutables
- = do { cts <- readMetaTyVar tyvar
- ; case cts of
- Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
- Indirect ty -> zonkType unbound_var_fn ty }
+ = ASSERT( isTcTyVar tyvar )
+ case tcTyVarDetails tyvar of
+ SkolemTv {} -> return (TyVarTy tyvar)
+ FlatSkol ty -> zonkType unbound_var_fn ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> unbound_var_fn tyvar
+ 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).
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 ()
-- with a decent error message
; check_valid_theta SigmaCtxt theta
; check_type rank ubx_tup tau -- Allow foralls to right of arrow
- ; checkFreeness tvs theta
; checkAmbiguity tvs theta (tyVarsOfType tau) }
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 }
even in a scope where b is in scope.
\begin{code}
-checkFreeness :: [Var] -> [PredType] -> TcM ()
-checkFreeness forall_tyvars theta
- = do { flexible_contexts <- doptM Opt_FlexibleContexts
- ; unless flexible_contexts $ mapM_ complain (filter is_free theta) }
- where
- is_free pred = not (isIPPred pred)
- && not (any bound_var (varSetElems (tyVarsOfPred pred)))
- bound_var ct_var = ct_var `elem` forall_tyvars
- complain pred = addErrTc (freeErr pred)
-
-freeErr :: PredType -> SDoc
-freeErr pred
- = 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}
checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
checkThetaCtxt ctxt theta
= vcat [ptext (sLit "In the context:") <+> pprTheta theta,
arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
arityErr kind name n m
= hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
- n_arguments <> comma, text "but has been given", int m]
+ n_arguments <> comma, text "but has been given",
+ if m==0 then text "none" else int m]
where
n_arguments | n == 0 = ptext (sLit "no arguments")
| n == 1 = ptext (sLit "1 argument")
%* *
%************************************************************************
-
\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.