-- Creating new evidence variables
newEvVar, newCoVar, newEvVars,
newWantedCoVar, writeWantedCoVar, readWantedCoVar,
- newIP, newDict, newSelfDict, isSelfDict,
+ newIP, newDict, newSilentGiven, isSilentEvVar,
newWantedEvVar, newWantedEvVars,
newTcEvBinds, addTcEvBind,
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
SourceTyCtxt(..), checkValidTheta,
- checkValidInstHead, checkValidInstance,
- checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
+ checkValidInstance,
+ checkValidTypeInst, checkTyFamFreeness,
arityErr,
growPredTyVars, growThetaTyVars, validDerivPred,
--------------------------------
-- Zonking
zonkType, mkZonkTcTyVar, zonkTcPredType,
- zonkTcTypeCarefully,
+ zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
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) }
-----------------
-newSelfDict :: Class -> [TcType] -> TcM DictId
--- Make a dictionary for "self". It behaves just like a normal DictId
--- except that it responds True to isSelfDict
+newSilentGiven :: PredType -> TcM EvVar
+-- Make a dictionary for a "silent" given dictionary
+-- Behaves just like any EvVar except that it responds True to isSilentDict
-- This is used only to suppress confusing error reports
-newSelfDict cls tys
+newSilentGiven (ClassP cls tys)
= do { uniq <- newUnique
- ; let name = mkSystemName uniq selfDictOcc
+ ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+newSilentGiven (EqPred ty1 ty2)
+ = do { uniq <- newUnique
+ ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
+ ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+newSilentGiven pred@(IParam {})
+ = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
-selfDictOcc :: OccName
-selfDictOcc = mkVarOcc "self"
-
-isSelfDict :: EvVar -> Bool
-isSelfDict v = isSystemName (Var.varName v)
+isSilentEvVar :: EvVar -> Bool
+isSilentEvVar v = isSystemName (Var.varName v)
-- Notice that all *other* evidence variables get Internal Names
\end{code}
| otherwise
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv {} -> return (TyVarTy tv)
+ SkolemTv {} -> return (TyVarTy tv)
FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
Flexi -> return (TyVarTy tv)
Indirect ty -> zonkType (zonk_tv env_tvs) ty }
zonkTcTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- SkolemTv {} -> return (TyVarTy tv)
+ SkolemTv {} -> return (TyVarTy tv)
FlatSkol ty -> zonkTcType ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
- Flexi -> return (TyVarTy tv)
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> return (TyVarTy tv)
Indirect ty -> zonkTcType ty }
zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
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]
- ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
+ 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_name = setNameUnique (tyVarName tv) uniq
- final_tv = mkSkolTyVar final_name 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_tv = mkSkolTyVar final_name final_kind skol_info
+ ; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
\end{code}
-- 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 )
how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
-check_pred_ty dflags _ pred@(EqPred ty1 ty2)
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
= do { -- Equational constraints are valid in all contexts if type
-- families are permitted
; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+ ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
+ (eqSuperClassErr pred)
-- Check the form of the argument types
; checkValidMonoType ty1
= vcat [ptext (sLit "In the context:") <+> pprTheta theta,
ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
+eqSuperClassErr :: PredType -> SDoc
+eqSuperClassErr pred
+ = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
+ 2 (ppr pred)
+
badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
-badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
-eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
- $$
- parens (ptext (sLit "Use -XTypeFamilies to permit this"))
+badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
+eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
+ $$
+ 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 :: [[PredType]] -> SDoc
We can also have instances for functions: @instance Foo (a -> b) ...@.
\begin{code}
-checkValidInstHead :: Type -> TcM (Class, [TcType])
-
-checkValidInstHead ty -- Should be a source type
- = case tcSplitPredTy_maybe ty of {
- Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
- Just pred ->
-
- case getClassPredTys_maybe pred of {
- Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
- Just (clas,tys) -> do
+checkValidInstHead :: Class -> [Type] -> TcM ()
+checkValidInstHead clas tys
+ = do { dflags <- getDOpts
- dflags <- getDOpts
- check_inst_head dflags clas tys
- return (clas, tys)
- }}
-
-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
+ -- If GlasgowExts then check at least one isn't a type variable
; checkTc (xopt Opt_TypeSynonymInstances dflags ||
all tcInstHeadTyNotSynonym tys)
- (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+ (instTypeErr pp_pred head_type_synonym_msg)
; checkTc (xopt Opt_FlexibleInstances dflags ||
all tcInstHeadTyAppAllTyVars tys)
- (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+ (instTypeErr pp_pred head_type_args_tyvars_msg)
; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
isSingleton tys)
- (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+ (instTypeErr pp_pred head_one_type_msg)
-- May not contain type family applications
; mapM_ checkTyFamFreeness tys
}
where
+ pp_pred = pprClassPred clas tys
head_type_synonym_msg = parens (
text "All instance types must be of the form (T t1 ... tn)" $$
text "where T is not a synonym." $$
head_type_args_tyvars_msg = parens (vcat [
text "All instance types must be of the form (T a1 ... an)",
- text "where a1 ... an are type *variables*,",
+ text "where a1 ... an are *distinct type variables*,",
text "and each type variable appears at most once in the instance head.",
text "Use -XFlexibleInstances if you want to disable this."])
%************************************************************************
\begin{code}
-checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
- -> TcM (Class, [TcType])
-checkValidInstance hs_type tyvars theta tau
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
+ -> Class -> [TcType] -> TcM ()
+checkValidInstance hs_type tyvars theta clas inst_tys
= setSrcSpan (getLoc hs_type) $
- do { (clas, inst_tys) <- setSrcSpan head_loc $
- checkValidInstHead tau
-
- ; undecidable_ok <- xoptM Opt_UndecidableInstances
-
- ; checkValidTheta InstThetaCtxt theta
+ do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
+ ; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
-- Check that instance inference will terminate (if we care)
-- For Haskell 98 this will already have been done by checkValidTheta,
-- but as we may be using other extensions we need to check.
- ; unless undecidable_ok $
+ ; undecidable_ok <- xoptM Opt_UndecidableInstances
+ ; unless undecidable_ok $
mapM_ addErrTc (checkInstTermination inst_tys theta)
-- 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
+ -- The location of the "head" of the instance
head_loc = case hs_type of
L _ (HsForAllTy _ _ _ (L loc _)) -> loc
L loc _ -> loc