X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=ef4ad34c7da5ef8baf1ebc7839efd02c7ef8a867;hp=b31a4cc41ee09150d93175ff7f5adc03b344f06b;hb=a3bab0506498db41853543558c52a4fda0d183af;hpb=2072edcfe180f617d8f9f8990f682589c4e35082 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index b31a4cc..ef4ad34 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -26,16 +26,15 @@ module TcMType ( -- Creating new evidence variables newEvVar, newCoVar, newEvVars, newWantedCoVar, writeWantedCoVar, readWantedCoVar, - newIP, newDict, newSelfDict, isSelfDict, + newIP, newDict, newSilentGiven, isSilentEvVar, - newWantedEvVar, newWantedEvVars, - newKindConstraint, + newWantedEvVar, newWantedEvVars, newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstSigTyVars, - tcInstType, tcInstSigType, + tcInstType, tcInstSigType, instMetaTyVar, tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -43,15 +42,15 @@ module TcMType ( -- 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, @@ -135,17 +134,6 @@ newWantedEvVars theta = mapM newWantedEvVar theta 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 @@ -175,29 +163,23 @@ newName occ ; return (mkInternalName uniq occ loc) } ----------------- -newKindConstraint :: Type -> Kind -> TcM (CoVar, Type) --- Create a new wanted CoVar that constrains the type --- to have the specified kind -newKindConstraint ty kind - = do { ty_k <- newFlexiTyVarTy kind - ; co_var <- newWantedCoVar ty ty_k - ; return (co_var, ty_k) } - ------------------ -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} @@ -300,11 +282,12 @@ tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv) newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar -- Make a new meta tyvar out of thin air newMetaTyVar meta_info kind - = do { uniq <- newUnique + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = mkSysTvName uniq fs fs = case meta_info of TauTv -> fsLit "t" + TcsTv -> fsLit "u" SigTv _ -> fsLit "a" ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } @@ -312,7 +295,7 @@ instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar -- Make a new meta tyvar whose Name and Kind -- come from an existing TyVar instMetaTyVar meta_info tyvar - = do { uniq <- newUnique + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = setNameUnique (tyVarName tyvar) uniq kind = tyVarKind tyvar @@ -497,10 +480,10 @@ zonkTcTypeCarefully ty | 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 } @@ -513,11 +496,11 @@ zonkTcTyVar :: TcTyVar -> TcM TcType 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 @@ -557,8 +540,6 @@ zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] 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) @@ -569,45 +550,49 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- 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] + 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_tv = mkSkolTyVar (tyVarName tv) 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_name = setNameUnique (tyVarName tv) uniq + final_tv = mkSkolTyVar final_name final_kind skol_info + ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} \begin{code} zonkImplication :: Implication -> TcM Implication -zonkImplication implic@(Implic { ic_untch = env_tvs, ic_given = given +zonkImplication implic@(Implic { ic_given = given , ic_wanted = wanted }) - = do { env_tvs' <- zonkTcTyVarsAndFV env_tvs - ; given' <- mapM zonkEvVar given + = do { given' <- mapM zonkEvVar given ; wanted' <- mapBagM zonkWanted wanted - ; return (implic { ic_untch = env_tvs', ic_given = given' - , ic_wanted = wanted' }) } + ; return (implic { ic_given = given', ic_wanted = wanted' }) } zonkEvVar :: EvVar -> TcM EvVar zonkEvVar var = do { ty' <- zonkTcType (varType var) @@ -702,10 +687,8 @@ simplifier knows how to deal with. -- 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 @@ -745,7 +728,7 @@ zonkType zonk_tc_tyvar ty 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 ) @@ -1155,10 +1138,12 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) 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 @@ -1315,11 +1300,16 @@ checkThetaCtxt ctxt theta = 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 @@ -1352,34 +1342,20 @@ compiled elsewhere). In these cases, we let them go through anyway. 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 -> +checkValidInstHead :: Class -> [Type] -> TcM () +checkValidInstHead clas tys + = do { dflags <- getDOpts - case getClassPredTys_maybe pred of { - Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; - Just (clas,tys) -> do - - 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 @@ -1392,6 +1368,7 @@ check_inst_head dflags clas 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." $$ @@ -1399,7 +1376,7 @@ check_inst_head dflags clas tys 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."]) @@ -1421,35 +1398,30 @@ instTypeErr pp_ty msg %************************************************************************ \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