diff --git a/compiler/basicTypes/Name.lhs b/compiler/basicTypes/Name.lhs index 1a8b8b3c324f9e3ad4f60f6994d2c5d38c46260d..70cf298a4f6e2405247849ed8b683d021e67d1a9 100644 --- a/compiler/basicTypes/Name.lhs +++ b/compiler/basicTypes/Name.lhs @@ -280,7 +280,7 @@ mkSystemVarName :: Unique -> FastString -> Name mkSystemVarName uniq fs = mkSystemName uniq (mkVarOccFS fs) mkSysTvName :: Unique -> FastString -> Name -mkSysTvName uniq fs = mkSystemName uniq (mkOccNameFS tvName fs) +mkSysTvName uniq fs = mkSystemName uniq (mkOccNameFS tvName fs) -- | Make a name for a foreign call mkFCallName :: Unique -> String -> Name diff --git a/compiler/basicTypes/OccName.lhs b/compiler/basicTypes/OccName.lhs index 439a2f88313129eb09c845f6cb0179ef28607c89..f02ae8d0da3f01042561c17f230021f28228ec7f 100644 --- a/compiler/basicTypes/OccName.lhs +++ b/compiler/basicTypes/OccName.lhs @@ -42,7 +42,7 @@ module OccName ( mkTyVarOcc, mkTyVarOccFS, mkTcOcc, mkTcOccFS, mkClsOcc, mkClsOccFS, - mkDFunOcc, + mkDFunOcc, mkTupleOcc, setOccNameSpace, @@ -720,7 +720,9 @@ tidyOccName in_scope occ@(OccName occ_sp fs) Just n -> -- Already used: make a new guess, -- change the guess base, and try again tidyOccName (extendOccEnv in_scope occ (n+1)) - (mkOccName occ_sp (unpackFS fs ++ show n)) + (mkOccName occ_sp (base_occ ++ show n)) + where + base_occ = reverse (dropWhile isDigit (reverse (unpackFS fs))) \end{code} %************************************************************************ diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index 010fb1ec26124bc27e040531095f9da4d5cc697b..79fad322b99359fa1eede8231b8786f848215824 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -50,7 +50,7 @@ module Var ( mkTyVar, mkTcTyVar, mkWildCoVar, -- ** Taking 'TyVar's apart - tyVarName, tyVarKind, tcTyVarDetails, + tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails, -- ** Modifying 'TyVar's setTyVarName, setTyVarUnique, setTyVarKind, @@ -283,6 +283,9 @@ mkTcTyVar name kind details tcTyVarDetails :: TyVar -> TcTyVarDetails tcTyVarDetails (TcTyVar { tc_tv_details = details }) = details tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var) + +setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar +setTcTyVarDetails tv details = tv { tc_tv_details = details } \end{code} %************************************************************************ diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 597a9a72f83c8f926c9023bb8fe7dbcbf06440b7..59f5669e3ede9765da30d81dff4541189e4bd8ca 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -576,13 +576,10 @@ type RttiInstantiation = [(TcTyVar, TyVar)] -- | Returns the instantiated type scheme ty', and the -- mapping from new (instantiated) -to- old (skolem) type variables --- We want this mapping just for old RuntimeUnkSkols, to avoid --- gratuitously changing their unique on every trip instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation) instScheme (tvs, ty) = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs - ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs - , isRuntimeUnkSkol tv] + ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs] ; return (substTy subst ty, rtti_inst) } applyRevSubst :: RttiInstantiation -> TR () @@ -1132,7 +1129,7 @@ zonkRttiType = zonkType (mkZonkTcTyVar zonk_unbound_meta) where zonk_unbound_meta tv = ASSERT( isTcTyVar tv ) - do { tv' <- skolemiseUnboundMetaTyVar RuntimeUnkSkol tv + do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk -- This is where RuntimeUnkSkols are born: -- otherwise-unconstrained unification variables are -- turned into RuntimeUnkSkols as they leave the diff --git a/compiler/main/HscTypes.lhs b/compiler/main/HscTypes.lhs index bb874bcf09a573186a29132e2ef1a31bd0a38d6b..5d53739d1fc784539bc0af29024b01cfcb3cf4c3 100644 --- a/compiler/main/HscTypes.lhs +++ b/compiler/main/HscTypes.lhs @@ -860,17 +860,21 @@ emptyModIface mod -- | Interactive context, recording information relevant to GHCi data InteractiveContext = InteractiveContext { - ic_toplev_scope :: [Module], -- ^ The context includes the "top-level" scope of + ic_toplev_scope :: [Module] -- ^ The context includes the "top-level" scope of -- these modules - ic_exports :: [(Module, Maybe (ImportDecl RdrName))], -- ^ The context includes just the exported parts of these + , ic_exports :: [(Module, Maybe (ImportDecl RdrName))] -- ^ The context includes just the exported parts of these -- modules - ic_rn_gbl_env :: GlobalRdrEnv, -- ^ The contexts' cached 'GlobalRdrEnv', built from + , ic_rn_gbl_env :: GlobalRdrEnv -- ^ The contexts' cached 'GlobalRdrEnv', built from -- 'ic_toplev_scope' and 'ic_exports' - ic_tmp_ids :: [Id] -- ^ Names bound during interaction with the user. - -- Later Ids shadow earlier ones with the same OccName. + , ic_tmp_ids :: [Id] -- ^ Names bound during interaction with the user. + -- Later Ids shadow earlier ones with the same OccName + -- Expressions are typed with these Ids in the envt + -- For runtime-debugging, these Ids may have free + -- TcTyVars of RuntimUnkSkol flavour, but no free TyVars + -- (because the typechecker doesn't expect that) #ifdef GHCI , ic_resume :: [Resume] -- ^ The stack of breakpoint contexts diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs index 696f612f6bd5479d0474ca89a563fae7668e16ac..8967c171e10d8eda05f1504dfe1b7f604cf5246b 100644 --- a/compiler/main/InteractiveEval.hs +++ b/compiler/main/InteractiveEval.hs @@ -546,7 +546,7 @@ bindLocalsAtBreakpoint hsc_env apStack Nothing = do exn_name = mkInternalName (getUnique exn_fs) (mkVarOccFS exn_fs) span e_fs = fsLit "e" e_name = mkInternalName (getUnique e_fs) (mkTyVarOccFS e_fs) span - e_tyvar = mkTcTyVar e_name liftedTypeKind (SkolemTv RuntimeUnkSkol) + e_tyvar = mkRuntimeUnkTyVar e_name liftedTypeKind exn_id = Id.mkVanillaGlobal exn_name (mkTyVarTy e_tyvar) ictxt0 = hsc_IC hsc_env @@ -572,12 +572,16 @@ bindLocalsAtBreakpoint hsc_env apStack (Just info) = do occs = modBreaks_vars breaks ! index span = modBreaks_locs breaks ! index - -- filter out any unboxed ids; we can't bind these at the prompt - let pointers = filter (\(id,_) -> isPointer id) vars + -- Filter out any unboxed ids; + -- we can't bind these at the prompt + pointers = filter (\(id,_) -> isPointer id) vars isPointer id | PtrRep <- idPrimRep id = True | otherwise = False - let (ids, offsets) = unzip pointers + (ids, offsets) = unzip pointers + + free_tvs = foldr (unionVarSet . tyVarsOfType . idType) + (tyVarsOfType result_ty) ids -- It might be that getIdValFromApStack fails, because the AP_STACK -- has been accidentally evaluated, or something else has gone wrong. @@ -589,15 +593,18 @@ bindLocalsAtBreakpoint hsc_env apStack (Just info) = do debugTraceMsg (hsc_dflags hsc_env) 1 $ text "Warning: _result has been evaluated, some bindings have been lost" - new_ids <- zipWithM mkNewId occs filtered_ids - let names = map idName new_ids + us <- mkSplitUniqSupply 'I' + let (us1, us2) = splitUniqSupply us + tv_subst = newTyVars us1 free_tvs + new_ids = zipWith3 (mkNewId tv_subst) occs filtered_ids (uniqsFromSupply us2) + names = map idName new_ids -- make an Id for _result. We use the Unique of the FastString "_result"; -- we don't care about uniqueness here, because there will only be one -- _result in scope at any time. let result_name = mkInternalName (getUnique result_fs) (mkVarOccFS result_fs) span - result_id = Id.mkVanillaGlobal result_name result_ty + result_id = Id.mkVanillaGlobal result_name (substTy tv_subst result_ty) -- for each Id we're about to bind in the local envt: -- - tidy the type variables @@ -619,20 +626,25 @@ bindLocalsAtBreakpoint hsc_env apStack (Just info) = do hsc_env1 <- rttiEnvironment hsc_env{ hsc_IC = ictxt1 } return (hsc_env1, if result_ok then result_name:names else names, span) where - mkNewId :: OccName -> Id -> IO Id - mkNewId occ id = do - us <- mkSplitUniqSupply 'I' - -- we need a fresh Unique for each Id we bind, because the linker + -- We need a fresh Unique for each Id we bind, because the linker -- state is single-threaded and otherwise we'd spam old bindings -- whenever we stop at a breakpoint. The InteractveContext is properly -- saved/restored, but not the linker state. See #1743, test break026. - let - uniq = uniqFromSupply us - loc = nameSrcSpan (idName id) - name = mkInternalName uniq occ loc - ty = idType id - new_id = Id.mkVanillaGlobalWithInfo name ty (idInfo id) - return new_id + mkNewId :: TvSubst -> OccName -> Id -> Unique -> Id + mkNewId tv_subst occ id uniq + = Id.mkVanillaGlobalWithInfo name ty (idInfo id) + where + loc = nameSrcSpan (idName id) + name = mkInternalName uniq occ loc + ty = substTy tv_subst (idType id) + + newTyVars :: UniqSupply -> TcTyVarSet -> TvSubst + -- Similarly, clone the type variables mentioned in the types + -- we have here, *and* make them all RuntimeUnk tyars + newTyVars us tvs + = mkTopTvSubst [ (tv, mkTyVarTy (mkRuntimeUnkTyVar name (tyVarKind tv))) + | (tv, uniq) <- varSetElems tvs `zip` uniqsFromSupply us + , let name = setNameUnique (tyVarName tv) uniq ] rttiEnvironment :: HscEnv -> IO HscEnv rttiEnvironment hsc_env@HscEnv{hsc_IC=ic} = do @@ -979,5 +991,7 @@ reconstructType hsc_env bound id = do hv <- Linker.getHValue hsc_env (varName id) cvReconstructType hsc_env bound (idType id) hv +mkRuntimeUnkTyVar :: Name -> Kind -> TyVar +mkRuntimeUnkTyVar name kind = mkTcTyVar name kind RuntimeUnk #endif /* GHCI */ diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs index 8855fdcbe94e4513c2e8cebe17367f484efc43a6..45584d9b411aa11039aab9b0ef571c26dfa6c051 100644 --- a/compiler/typecheck/FamInst.lhs +++ b/compiler/typecheck/FamInst.lhs @@ -178,8 +178,7 @@ checkForConflicts inst_envs famInst -- We use tcInstSkolType because we don't want to allocate -- fresh *meta* type variables. - ; skol_tvs <- tcInstSkolTyVars FamInstSkol - (tyConTyVars (famInstTyCon famInst)) + ; skol_tvs <- tcInstSkolTyVars (tyConTyVars (famInstTyCon famInst)) ; let conflicts = lookupFamInstEnvConflicts inst_envs famInst skol_tvs ; unless (null conflicts) $ conflictInstErr famInst (fst (head conflicts)) diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 1496ec5e172e08ee3de520f1f9b232084a25c59e..bbdf21bc3c06cee114db649147e37567899edd0d 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -18,13 +18,16 @@ module Inst ( tcSyntaxName, -- Simple functions over evidence variables - hasEqualities, + hasEqualities, unitImplication, - tyVarsOfWanteds, tyVarsOfWanted, tyVarsOfWantedEvVar, tyVarsOfWantedEvVars, + tyVarsOfWC, tyVarsOfBag, tyVarsOfEvVarXs, tyVarsOfEvVarX, tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication, - tidyWanteds, tidyWanted, tidyWantedEvVar, tidyWantedEvVars, - tidyEvVar, tidyImplication + tidyWantedEvVar, tidyWantedEvVars, tidyWC, + tidyEvVar, tidyImplication, tidyFlavoredEvVar, + + substWantedEvVar, substWantedEvVars, substFlavoredEvVar, + substEvVar, substImplication ) where #include "HsVersions.h" @@ -47,7 +50,7 @@ import Coercion import HscTypes import Id import Name -import Var ( Var, TyVar, EvVar, varType, setVarType ) +import Var import VarEnv import VarSet import PrelNames @@ -57,7 +60,7 @@ import Bag import Maybes import Util import Outputable -import Data.List +import Data.List( mapAccumL ) \end{code} @@ -75,7 +78,7 @@ emitWanteds origin theta = mapM (emitWanted origin) theta emitWanted :: CtOrigin -> TcPredType -> TcM EvVar emitWanted origin pred = do { loc <- getCtLoc origin ; ev <- newWantedEvVar pred - ; emitConstraint (WcEvVar (WantedEvVar ev loc)) + ; emitFlat (mkEvVarX ev loc) ; return ev } newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId) @@ -136,17 +139,16 @@ ToDo: this eta-abstraction plays fast and loose with termination, \begin{code} deeplySkolemise - :: SkolemInfo - -> TcSigmaType + :: TcSigmaType -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType) -deeplySkolemise skol_info ty +deeplySkolemise ty | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys - ; tvs1 <- mapM (tcInstSkolTyVar skol_info) tvs + ; tvs1 <- tcInstSkolTyVars tvs ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1) ; ev_vars1 <- newEvVars (substTheta subst theta) - ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise skol_info (substTy subst ty') + ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty') ; return ( mkWpLams ids1 <.> mkWpTyLams tvs1 <.> mkWpLams ev_vars1 @@ -415,7 +417,7 @@ addLocalInst home_ie ispec -- This is absurdly delicate. let dfun = instanceDFunId ispec - ; (tvs', theta', tau') <- tcInstSkolType UnkSkol (idType dfun) + ; (tvs', theta', tau') <- tcInstSkolType (idType dfun) ; let (cls, tys') = tcSplitDFunHead tau' dfun' = setIdType dfun (mkSigmaTy tvs' theta' tau') ispec' = setInstanceDFunId ispec dfun' @@ -477,6 +479,11 @@ addDictLoc ispec thing_inside %************************************************************************ \begin{code} +unitImplication :: Implication -> Bag Implication +unitImplication implic + | isEmptyWC (ic_wanted implic) = emptyBag + | otherwise = unitBag implic + hasEqualities :: [EvVar] -> Bool -- Has a bunch of canonical constraints (all givens) got any equalities in it? hasEqualities givens = any (has_eq . evVarPred) givens @@ -485,23 +492,22 @@ hasEqualities givens = any (has_eq . evVarPred) givens has_eq (IParam {}) = False has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls) ----------------- -tyVarsOfWanteds :: WantedConstraints -> TyVarSet -tyVarsOfWanteds = foldrBag (unionVarSet . tyVarsOfWanted) emptyVarSet - -tyVarsOfWanted :: WantedConstraint -> TyVarSet -tyVarsOfWanted (WcEvVar wev) = tyVarsOfWantedEvVar wev -tyVarsOfWanted (WcImplic impl) = tyVarsOfImplication impl +---------------- Getting free tyvars ------------------------- +tyVarsOfWC :: WantedConstraints -> TyVarSet +tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) + = tyVarsOfEvVarXs flat `unionVarSet` + tyVarsOfBag tyVarsOfImplication implic `unionVarSet` + tyVarsOfEvVarXs insol tyVarsOfImplication :: Implication -> TyVarSet -tyVarsOfImplication implic = tyVarsOfWanteds (ic_wanted implic) - `minusVarSet` (ic_skols implic) +tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted }) + = tyVarsOfWC wanted `minusVarSet` skols -tyVarsOfWantedEvVar :: WantedEvVar -> TyVarSet -tyVarsOfWantedEvVar (WantedEvVar ev _) = tyVarsOfEvVar ev +tyVarsOfEvVarX :: EvVarX a -> TyVarSet +tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev -tyVarsOfWantedEvVars :: Bag WantedEvVar -> TyVarSet -tyVarsOfWantedEvVars = foldrBag (unionVarSet . tyVarsOfWantedEvVar) emptyVarSet +tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet +tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX tyVarsOfEvVar :: EvVar -> TyVarSet tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev @@ -509,29 +515,94 @@ tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev tyVarsOfEvVars :: [EvVar] -> TyVarSet tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet ---------------- -tidyWanteds :: TidyEnv -> WantedConstraints -> WantedConstraints -tidyWanteds env = mapBag (tidyWanted env) +tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet +tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet + +---------------- Tidying ------------------------- +tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints +tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) + = WC { wc_flat = tidyWantedEvVars env flat + , wc_impl = mapBag (tidyImplication env) implic + , wc_insol = mapBag (tidyFlavoredEvVar env) insol } -tidyWanted :: TidyEnv -> WantedConstraint -> WantedConstraint -tidyWanted env (WcEvVar wev) = WcEvVar (tidyWantedEvVar env wev) -tidyWanted env (WcImplic implic) = WcImplic (tidyImplication env implic) +tidyImplication :: TidyEnv -> Implication -> Implication +tidyImplication env implic@(Implic { ic_skols = tvs + , ic_given = given + , ic_wanted = wanted + , ic_loc = loc }) + = implic { ic_skols = mkVarSet tvs' + , ic_given = map (tidyEvVar env1) given + , ic_wanted = tidyWC env1 wanted + , ic_loc = tidyGivenLoc env1 loc } + where + (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs) + +tidyEvVar :: TidyEnv -> EvVar -> EvVar +tidyEvVar env var = setVarType var (tidyType env (varType var)) tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar -tidyWantedEvVar env (WantedEvVar ev loc) = WantedEvVar (tidyEvVar env ev) loc +tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar tidyWantedEvVars env = mapBag (tidyWantedEvVar env) -tidyEvVar :: TidyEnv -> EvVar -> EvVar -tidyEvVar env v = setVarType v (tidyType env (varType v)) - -tidyImplication :: TidyEnv -> Implication -> Implication -tidyImplication env implic@(Implic { ic_skols = skols, ic_given = given - , ic_wanted = wanted }) - = implic { ic_skols = mkVarSet skols' - , ic_given = map (tidyEvVar env') given - , ic_wanted = tidyWanteds env' wanted } +tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar +tidyFlavoredEvVar env (EvVarX v fl) + = EvVarX (tidyEvVar env v) (tidyFlavor env fl) + +tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor +tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc) +tidyFlavor _ fl = fl + +tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc +tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt + +tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo +tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty) +tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids) +tidySkolemInfo _ info = info + +---------------- Substitution ------------------------- +substWC :: TvSubst -> WantedConstraints -> WantedConstraints +substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) + = WC { wc_flat = substWantedEvVars subst flat + , wc_impl = mapBag (substImplication subst) implic + , wc_insol = mapBag (substFlavoredEvVar subst) insol } + +substImplication :: TvSubst -> Implication -> Implication +substImplication subst implic@(Implic { ic_skols = tvs + , ic_given = given + , ic_wanted = wanted + , ic_loc = loc }) + = implic { ic_skols = mkVarSet tvs' + , ic_given = map (substEvVar subst1) given + , ic_wanted = substWC subst1 wanted + , ic_loc = substGivenLoc subst1 loc } where - (env', skols') = mapAccumL tidyTyVarBndr env (varSetElems skols) + (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs) + +substEvVar :: TvSubst -> EvVar -> EvVar +substEvVar subst var = setVarType var (substTy subst (varType var)) + +substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar +substWantedEvVars subst = mapBag (substWantedEvVar subst) + +substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar +substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l + +substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar +substFlavoredEvVar subst (EvVarX v fl) + = EvVarX (substEvVar subst v) (substFlavor subst fl) + +substFlavor :: TvSubst -> CtFlavor -> CtFlavor +substFlavor subst (Given loc) = Given (substGivenLoc subst loc) +substFlavor _ fl = fl + +substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc +substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt + +substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo +substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty) +substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids) +substSkolemInfo _ info = info \end{code} \ No newline at end of file diff --git a/compiler/typecheck/TcArrows.lhs b/compiler/typecheck/TcArrows.lhs index 53b3c97215cfd1a02330bd42b4da4111ab36ed3f..ae4a1e876125158fdc0d92e17e46b935503ed3ff 100644 --- a/compiler/typecheck/TcArrows.lhs +++ b/compiler/typecheck/TcArrows.lhs @@ -237,7 +237,7 @@ tc_cmd env cmd@(HsDo do_or_lc stmts body _ty) (cmd_stk, res_ty) tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty) = addErrCtxt (cmdCtxt cmd) $ do { cmds_w_tys <- zipWithM new_cmd_ty cmd_args [1..] - ; [w_tv] <- tcInstSkolTyVars ArrowSkol [alphaTyVar] + ; [w_tv] <- tcInstSkolTyVars [alphaTyVar] ; let w_ty = mkTyVarTy w_tv -- Just a convenient starting point -- a ((w,t1) .. tn) t diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index 9f11ade302005b8fe54f4e16980b8f5b2c6bcf0f..c9f2a2d3ca5fd7c8ba7722e2bc6d42ca9b0bf523 100644 --- a/compiler/typecheck/TcBinds.lhs +++ b/compiler/typecheck/TcBinds.lhs @@ -33,7 +33,6 @@ import Var import Name import NameSet import NameEnv -import VarSet import SrcLoc import Bag import ErrUtils @@ -388,11 +387,10 @@ tcPolyCheck :: TcSigInfo -> PragFun -- it binds a single variable, -- it has a signature, tcPolyCheck sig@(TcSigInfo { sig_id = id, sig_tvs = tvs, sig_scoped = scoped - , sig_theta = theta, sig_loc = loc }) + , sig_theta = theta, sig_tau = tau, sig_loc = loc }) prag_fn rec_tc bind_list = do { ev_vars <- newEvVars theta - - ; let skol_info = SigSkol (FunSigCtxt (idName id)) + ; let skol_info = SigSkol (FunSigCtxt (idName id)) (mkPhiTy theta tau) ; (ev_binds, (binds', [mono_info])) <- checkConstraints skol_info tvs ev_vars $ tcExtendTyVarEnv2 (scoped `zip` mkTyVarTys tvs) $ @@ -423,12 +421,8 @@ tcPolyInfer top_lvl mono sig_fn prag_fn rec_tc bind_list ; unifyCtxts [sig | (_, Just sig, _) <- mono_infos] - ; let get_tvs | isTopLevel top_lvl = tyVarsOfType - | otherwise = exactTyVarsOfType - -- See Note [Silly type synonym] in TcType - tau_tvs = foldr (unionVarSet . get_tvs . getMonoType) emptyVarSet mono_infos - - ; (qtvs, givens, ev_binds) <- simplifyInfer mono tau_tvs wanted + ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos] + ; (qtvs, givens, ev_binds) <- simplifyInfer top_lvl mono name_taus wanted ; exports <- mapM (mkExport prag_fn qtvs (map evVarPred givens)) mono_infos @@ -545,14 +539,13 @@ tcSpec poly_id prag@(SpecSig _ hs_ty inl) ; warnIf (not (isOverloadedTy poly_ty || isInlinePragma inl)) (ptext (sLit "SPECIALISE pragma for non-overloaded function") <+> quotes (ppr poly_id)) -- Note [SPECIALISE pragmas] - ; wrap <- tcSubType origin skol_info (idType poly_id) spec_ty + ; wrap <- tcSubType origin sig_ctxt (idType poly_id) spec_ty ; return (SpecPrag poly_id wrap inl) } where name = idName poly_id poly_ty = idType poly_id origin = SpecPragOrigin name sig_ctxt = FunSigCtxt name - skol_info = SigSkol sig_ctxt spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag) tcSpec _ prag = pprPanic "tcSpec" (ppr prag) @@ -700,9 +693,6 @@ type MonoBindInfo = (Name, Maybe TcSigInfo, TcId) -- Type signature (if any), and -- the monomorphic bound things -getMonoType :: MonoBindInfo -> TcTauType -getMonoType (_,_,mono_id) = idType mono_id - tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_infix = inf, fun_matches = matches }) | Just sig <- sig_fn name @@ -1049,7 +1039,10 @@ tcInstSig sig_fn use_skols name | Just (scoped_tvs, loc) <- sig_fn name = do { poly_id <- tcLookupId name -- Cannot fail; the poly ids are put into -- scope when starting the binding group - ; (tvs, theta, tau) <- tcInstSigType use_skols name (idType poly_id) + ; let poly_ty = idType poly_id + ; (tvs, theta, tau) <- if use_skols + then tcInstType tcInstSkolTyVars poly_ty + else tcInstType tcInstSigTyVars poly_ty ; let sig = TcSigInfo { sig_id = poly_id , sig_scoped = scoped_tvs , sig_tvs = tvs, sig_theta = theta, sig_tau = tau diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 60d1836ee1a82bcc3ee9d6b011b464b44432ca26..961bf45b76e631871da9dcf508768ae2f1ae48c1 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,11 +1,12 @@ \begin{code} module TcCanonical( - mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, canEq, + mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens, + canOccursCheck, canEq ) where #include "HsVersions.h" -import BasicTypes +import BasicTypes import Type import TcRnTypes @@ -18,17 +19,15 @@ import TypeRep import Name import Var import Outputable -import Control.Monad ( when, zipWithM ) +import Control.Monad ( unless, when, zipWithM, zipWithM_ ) import MonadUtils import Control.Applicative ( (<|>) ) import VarSet import Bag -import HsBinds - -import Control.Monad ( unless ) -import TcSMonad -- The TcS Monad +import HsBinds +import TcSMonad \end{code} Note [Canonicalisation] @@ -150,7 +149,7 @@ flatten fl (TyConApp tc tys) ; (ret_co, rhs_var, ct) <- if isGiven fl then do { rhs_var <- newFlattenSkolemTy fam_ty - ; cv <- newGivOrDerCoVar fam_ty rhs_var fam_co + ; cv <- newGivenCoVar fam_ty rhs_var fam_co ; let ct = CFunEqCan { cc_id = cv , cc_flavor = fl -- Given , cc_fun = tc @@ -216,7 +215,7 @@ flattenPred ctxt (EqPred ty1 ty2) \begin{code} canWanteds :: [WantedEvVar] -> TcS CanonicalCts -canWanteds = fmap andCCans . mapM (\(WantedEvVar ev loc) -> mkCanonical (Wanted loc) ev) +canWanteds = fmap andCCans . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev) canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens @@ -225,7 +224,10 @@ canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs) -mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts +mkCanonicalFEV :: FlavoredEvVar -> TcS CanonicalCts +mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev + +mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts mkCanonical fl ev = case evVarPred ev of ClassP clas tys -> canClass fl ev clas tys IParam ip ty -> canIP fl ev ip ty @@ -242,9 +244,9 @@ canClass fl v cn tys -- The cos are all identities if fl=Given, -- hence nothing to do else do { v' <- newDictVar cn xis -- D xis - ; if isWanted fl - then setDictBind v (EvCast v' dict_co) - else setDictBind v' (EvCast v (mkSymCoercion dict_co)) + ; when (isWanted fl) $ setDictBind v (EvCast v' dict_co) + ; when (isGiven fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co)) + -- NB: No more setting evidence for derived now ; return v' } -- Add the superclasses of this one here, See Note [Adding superclasses]. @@ -257,7 +259,6 @@ canClass fl v cn tys , cc_flavor = fl , cc_class = cn , cc_tyargs = xis }) } - \end{code} Note [Adding superclasses] @@ -272,30 +273,37 @@ For Givens: We add all their superclasses as Givens. For Wanteds: - Generally speaking, we want to be able to add derived - superclasses of unsolved wanteds, and wanteds that have been - partially being solved via an instance. This is important to be - able to simplify the inferred constraints more (and to allow - for recursive dictionaries, less importantly). + Generally speaking we want to be able to add superclasses of + wanteds for two reasons: - Example: Inferred wanted constraint is (Eq a, Ord a), but we'd - only like to quantify over Ord a, hence we would like to be - able to add the superclass of Ord a as Derived and use it to - solve the wanted Eq a. + (1) Oportunities for improvement. Example: + class (a ~ b) => C a b + Wanted constraint is: C alpha beta + We'd like to simply have C alpha alpha. Similar + situations arise in relation to functional dependencies. + + (2) To have minimal constraints to quantify over: + For instance, if our wanted constraint is (Eq a, Ord a) + we'd only like to quantify over Ord a. -For Deriveds: - Deriveds either arise as wanteds that have been partially - solved, or as superclasses of other wanteds or deriveds. Hence, - their superclasses must be already there so we must do nothing - at al. + To deal with (1) above we only add the superclasses of wanteds + which may lead to improvement, that is: equality superclasses or + superclasses with functional dependencies. + + We deal with (2) completely independently in TcSimplify. See + Note [Minimize by SuperClasses] in TcSimplify. + + + Moreover, in all cases the extra improvement constraints are + Derived. Derived constraints have an identity (for now), but + we don't do anything with their evidence. For instance they + are never used to rewrite other constraints. - DV: In fact, it is probably true that the canonicaliser is - *never* asked to canonicalise Derived dictionaries + See also [New Wanted Superclass Work] in TcInteract. -There is one disadvantage to this. Suppose the wanted constraints are -(Num a, Num a). Then we'll add all the superclasses of both during -canonicalisation, only to eliminate them later when they are -interacted. That seems like a waste of work. Still, it's simple. + +For Deriveds: + We do nothing. Here's an example that demonstrates why we chose to NOT add superclasses during simplification: [Comes from ticket #4497] @@ -317,26 +325,42 @@ By adding superclasses definitely only once, during canonicalisation, this situa happen. \begin{code} + newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts -- Returns superclasses, see Note [Adding superclasses] newSCWorkFromFlavored ev orig_flavor cls xis - | isEmptyVarSet (tyVarsOfTypes xis) - = return emptyCCan - | otherwise - = do { let (tyvars, sc_theta, _, _) = classBigSig cls - sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta - ; sc_vars <- zipWithM inst_one sc_theta1 [0..] + | isDerived orig_flavor + = return emptyCCan -- Deriveds don't yield more superclasses because we will + -- add them transitively in the case of wanteds. + + | isGiven orig_flavor + = do { let sc_theta = immSuperClasses cls xis + flavor = orig_flavor + ; sc_vars <- mapM newEvVar sc_theta + ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]] ; mkCanonicals flavor sc_vars } - -- NB: Since there is a call to mkCanonicals, - -- this will add *recursively* all superclasses - where - inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n) - flavor = case orig_flavor of - Given loc -> Given loc - Wanted loc -> Derived loc DerSC - Derived {} -> orig_flavor - -- NB: the non-immediate superclasses will show up as - -- Derived, and we want their superclasses too! + + | isEmptyVarSet (tyVarsOfTypes xis) + = return emptyCCan -- Wanteds with no variables yield no deriveds. + -- See Note [Improvement from Ground Wanteds] + + | otherwise -- Wanted case, just add those SC that can lead to improvement. + = do { let sc_rec_theta = transSuperClasses cls xis + impr_theta = filter is_improvement_pty sc_rec_theta + Wanted wloc = orig_flavor + ; der_ids <- mapM newDerivedId impr_theta + ; mkCanonicals (Derived wloc) der_ids } + + +is_improvement_pty :: PredType -> Bool +-- Either it's an equality, or has some functional dependency +is_improvement_pty (EqPred {}) = True +is_improvement_pty (ClassP cls _ty) = not $ null fundeps + where (_,fundeps,_,_,_,_) = classExtraBigSig cls +is_improvement_pty _ = False + + + canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts -- See Note [Canonical implicit parameter constraints] to see why we don't @@ -378,22 +402,29 @@ canEq fl cv ty1 (TyConApp fn tys) canEq fl cv s1 s2 | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2 - = do { (v1,v2,v3) <- if isWanted fl then - do { v1 <- newWantedCoVar t1a t2a - ; v2 <- newWantedCoVar t1b t2b - ; v3 <- newWantedCoVar t1c t2c - ; let res_co = mkCoPredCo (mkCoVarCoercion v1) - (mkCoVarCoercion v2) (mkCoVarCoercion v3) - ; setWantedCoBind cv res_co - ; return (v1,v2,v3) } - else let co_orig = mkCoVarCoercion cv - coa = mkCsel1Coercion co_orig - cob = mkCsel2Coercion co_orig - coc = mkCselRCoercion co_orig - in do { v1 <- newGivOrDerCoVar t1a t2a coa - ; v2 <- newGivOrDerCoVar t1b t2b cob - ; v3 <- newGivOrDerCoVar t1c t2c coc - ; return (v1,v2,v3) } + = do { (v1,v2,v3) + <- if isWanted fl then -- Wanted + do { v1 <- newWantedCoVar t1a t2a + ; v2 <- newWantedCoVar t1b t2b + ; v3 <- newWantedCoVar t1c t2c + ; let res_co = mkCoPredCo (mkCoVarCoercion v1) + (mkCoVarCoercion v2) (mkCoVarCoercion v3) + ; setWantedCoBind cv res_co + ; return (v1,v2,v3) } + else if isGiven fl then -- Given + let co_orig = mkCoVarCoercion cv + coa = mkCsel1Coercion co_orig + cob = mkCsel2Coercion co_orig + coc = mkCselRCoercion co_orig + in do { v1 <- newGivenCoVar t1a t2a coa + ; v2 <- newGivenCoVar t1b t2b cob + ; v3 <- newGivenCoVar t1c t2c coc + ; return (v1,v2,v3) } + else -- Derived + do { v1 <- newDerivedId (EqPred t1a t2a) + ; v2 <- newDerivedId (EqPred t1b t2b) + ; v3 <- newDerivedId (EqPred t1c t2c) + ; return (v1,v2,v3) } ; cc1 <- canEq fl v1 t1a t2a ; cc2 <- canEq fl v2 t1b t2b ; cc3 <- canEq fl v3 t1c t2c @@ -409,10 +440,18 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) ; setWantedCoBind cv $ mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv) ; return (argv,resv) } - else let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv) - in do { argv <- newGivOrDerCoVar s1 s2 arg - ; resv <- newGivOrDerCoVar t1 t2 res - ; return (argv,resv) } + + else if isGiven fl then + let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv) + in do { argv <- newGivenCoVar s1 s2 arg + ; resv <- newGivenCoVar t1 t2 res + ; return (argv,resv) } + + else -- Derived + do { argv <- newDerivedId (EqPred s1 s2) + ; resv <- newDerivedId (EqPred t1 t2) + ; return (argv,resv) } + ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations ; cc2 <- canEq fl resv t1 t2 ; return (cc1 `andCCan` cc2) } @@ -447,13 +486,20 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) , tc1 == tc2 , length tys1 == length tys2 = -- Generate equalities for each of the corresponding arguments - do { argsv <- if isWanted fl then + do { argsv + <- if isWanted fl then do { argsv <- zipWithM newWantedCoVar tys1 tys2 - ; setWantedCoBind cv $ mkTyConCoercion tc1 (map mkCoVarCoercion argsv) - ; return argsv } - else + ; setWantedCoBind cv $ + mkTyConCoercion tc1 (map mkCoVarCoercion argsv) + ; return argsv } + + else if isGiven fl then let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) - in zipWith3M newGivOrDerCoVar tys1 tys2 cos + in zipWith3M newGivenCoVar tys1 tys2 cos + + else -- Derived + zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2 + ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 } -- See Note [Equality between type applications] @@ -468,19 +514,26 @@ canEq fl cv ty1 ty2 ; setWantedCoBind cv $ mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2) ; return (cv1,cv2) } - else let co1 = mkLeftCoercion $ mkCoVarCoercion cv - co2 = mkRightCoercion $ mkCoVarCoercion cv - in do { cv1 <- newGivOrDerCoVar s1 s2 co1 - ; cv2 <- newGivOrDerCoVar t1 t2 co2 - ; return (cv1,cv2) } + + else if isGiven fl then + let co1 = mkLeftCoercion $ mkCoVarCoercion cv + co2 = mkRightCoercion $ mkCoVarCoercion cv + in do { cv1 <- newGivenCoVar s1 s2 co1 + ; cv2 <- newGivenCoVar t1 t2 co2 + ; return (cv1,cv2) } + else -- Derived + do { cv1 <- newDerivedId (EqPred s1 s2) + ; cv2 <- newDerivedId (EqPred t1 t2) + ; return (cv1,cv2) } + ; cc1 <- canEq fl cv1 s1 s2 ; cc2 <- canEq fl cv2 t1 t2 ; return (cc1 `andCCan` cc2) } -canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) +canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {}) | tcIsForAllTy s1, tcIsForAllTy s2, Wanted {} <- fl - = canEqFailure fl s1 s2 + = canEqFailure fl cv | otherwise = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2) ; return emptyCCan } @@ -488,12 +541,10 @@ canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) -- Finally expand any type synonym applications. canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2' -canEq fl _ ty1 ty2 = canEqFailure fl ty1 ty2 +canEq fl cv _ _ = canEqFailure fl cv -canEqFailure :: CtFlavor -> Type -> Type -> TcS CanonicalCts -canEqFailure fl ty1 ty2 - = do { addErrorTcS MisMatchError fl ty1 ty2 - ; return emptyCCan } +canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts +canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv)) \end{code} Note [Equality between type applications] @@ -681,11 +732,15 @@ canEqLeaf untch fl cv cls1 cls2 then do { cv' <- newWantedCoVar s2 s1 ; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv') ; return cv' } - else newGivOrDerCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv)) + else if isGiven fl then + newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv)) + else -- Derived + newDerivedId (EqPred s2 s1) ; canEqLeafOriented fl cv' cls2 s1 } | otherwise - = canEqLeafOriented fl cv cls1 s2 + = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2)) + ; canEqLeafOriented fl cv cls1 s2 } where re_orient = reOrient untch s1 = unClassify cls1 @@ -698,8 +753,8 @@ canEqLeafOriented :: CtFlavor -> CoVar canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 | let k1 = kindAppResult (tyConKind fn) tys1, let k2 = typeKind s2, - isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan - = addErrorTcS KindError fl (unClassify cls1) s2 >> return emptyCCan + not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan + = canEqFailure fl cv -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise @@ -712,22 +767,19 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 no_flattening_happened = isEmptyCCan ccs ; cv_new <- if no_flattening_happened then return cv else if isGiven fl then return cv - else do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2 + else if isWanted fl then + do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2 -- cv' : F xis ~ xi2 - ; let -- fun_co :: F xis1 ~ F tys1 + ; let -- fun_co :: F xis1 ~ F tys1 fun_co = mkTyConCoercion fn cos1 -- want_co :: F tys1 ~ s2 want_co = mkSymCoercion fun_co `mkTransCoercion` mkCoVarCoercion cv' `mkTransCoercion` co2 - -- der_co :: F xis1 ~ xi2 - der_co = fun_co - `mkTransCoercion` mkCoVarCoercion cv - `mkTransCoercion` mkSymCoercion co2 - ; if isWanted fl - then setWantedCoBind cv want_co - else setWantedCoBind cv' der_co - ; return cv' } + ; setWantedCoBind cv want_co + ; return cv' } + else -- Derived + newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2) ; let final_cc = CFunEqCan { cc_id = cv_new , cc_flavor = fl @@ -747,8 +799,8 @@ canEqLeafOriented _ cv (OtherCls ty1) ty2 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts -- Establish invariants of CTyEqCans canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 - | isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan - = addErrorTcS KindError fl (mkTyVarTy tv) s2 >> return emptyCCan + | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan + = canEqFailure fl cv -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2 @@ -756,17 +808,17 @@ canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 -- unfolded version of the RHS, if we had to -- unfold any type synonyms to get rid of tv. ; case mxi2' of { - Nothing -> addErrorTcS OccCheckError fl (mkTyVarTy tv) xi2 >> return emptyCCan ; + Nothing -> canEqFailure fl cv ; Just xi2' -> do { let no_flattening_happened = isEmptyCCan ccs2 ; cv_new <- if no_flattening_happened then return cv else if isGiven fl then return cv - else do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 - ; if isWanted fl - then setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co) - else setWantedCoBind cv' (mkCoVarCoercion cv `mkTransCoercion` - mkSymCoercion co) - ; return cv' } + else if isWanted fl then + do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 + ; setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co) + ; return cv' } + else -- Derived + newDerivedId (EqPred (mkTyVarTy tv) xi2') ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new , cc_flavor = fl diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs index 0f91f6b9e7a704b444fef7d2fe0244c2bb1d24ab..8db89b9c07abffd1168f8a3aa43bfc1e390ab4ea 100644 --- a/compiler/typecheck/TcClassDcl.lhs +++ b/compiler/typecheck/TcClassDcl.lhs @@ -168,10 +168,9 @@ tcClassDecl2 (L loc (ClassDecl {tcdLName = class_name, tcdSigs = sigs, -- default methods. Better to make separate AbsBinds for each ; let (tyvars, _, _, op_items) = classBigSig clas - rigid_info = ClsSkol clas - prag_fn = mkPragFun sigs default_binds + prag_fn = mkPragFun sigs default_binds sig_fn = mkSigFun sigs - clas_tyvars = tcSkolSigTyVars rigid_info tyvars + clas_tyvars = tcSuperSkolTyVars tyvars pred = mkClassPred clas (mkTyVarTys clas_tyvars) ; this_dict <- newEvVar pred diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs index c51f78645cdc2942fa961be99af257b9e38084b6..354e4b238aa07cabc3b11d3360c7ea3d203d791e 100644 --- a/compiler/typecheck/TcEnv.lhs +++ b/compiler/typecheck/TcEnv.lhs @@ -203,6 +203,7 @@ tcLookupFamInst tycon tys = do { env <- getGblEnv ; eps <- getEps ; let instEnv = (eps_fam_inst_env eps, tcg_fam_inst_env env) + ; traceTc "lookupFamInst" ((ppr tycon <+> ppr tys) $$ ppr instEnv) ; case lookupFamInstEnv instEnv tycon tys of [] -> return Nothing ((fam_inst, rep_tys):_) diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index c040473e65ee7157eb334008791479afcb47d636..f714943227dad386d0f552b15a438a2a04e7394c 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -1,8 +1,8 @@ \begin{code} module TcErrors( - reportUnsolved, reportUnsolvedDeriv, - reportUnsolvedWantedEvVars, warnDefaulting, - unifyCtxt, typeExtraInfoMsg, + reportUnsolved, + warnDefaulting, + unifyCtxt, flattenForAllErrorTcS, solverDepthErrorTcS @@ -23,7 +23,6 @@ import TyCon import Name import NameEnv import Id ( idType ) -import HsExpr ( pprMatchContext ) import Var import VarSet import VarEnv @@ -50,158 +49,26 @@ from the insts, or just whatever seems to be around in the monad just now? \begin{code} -reportUnsolved :: (Bag WantedEvVar, Bag Implication) -> Bag FrozenError -> TcM () -reportUnsolved (unsolved_flats, unsolved_implics) frozen_errors - | isEmptyBag unsolved && isEmptyBag frozen_errors +reportUnsolved :: WantedConstraints -> TcM () +reportUnsolved wanted + | isEmptyWC wanted = return () | otherwise - = do { frozen_errors_zonked <- mapBagM zonk_frozen frozen_errors - ; let frozen_tvs = tyVarsOfFrozen frozen_errors_zonked + = do { -- Zonk to un-flatten any flatten-skols + ; wanted <- zonkWC wanted - ; unsolved <- mapBagM zonkWanted unsolved - -- Zonk to un-flatten any flatten-skols ; env0 <- tcInitTidyEnv - ; let tidy_env = tidyFreeTyVars env0 $ - tyVarsOfWanteds unsolved `unionVarSet` frozen_tvs - - tidy_unsolved = tidyWanteds tidy_env unsolved - err_ctxt = CEC { cec_encl = [] + ; let tidy_env = tidyFreeTyVars env0 free_tvs + free_tvs = tyVarsOfWC wanted + err_ctxt = CEC { cec_encl = [] + , cec_insol = insolubleWC wanted , cec_extra = empty - , cec_tidy = tidy_env - } - - ; traceTc "reportUnsolved" (vcat [ - text "Unsolved constraints =" <+> ppr unsolved, - text "Frozen errors =" <+> ppr frozen_errors_zonked ]) + , cec_tidy = tidy_env } + tidy_wanted = tidyWC tidy_env wanted - ; let tidy_frozen_errors_zonked = tidyFrozen tidy_env frozen_errors_zonked + ; traceTc "reportUnsolved" (ppr tidy_wanted) - ; reportTidyFrozens tidy_env tidy_frozen_errors_zonked - ; reportTidyWanteds err_ctxt tidy_unsolved } - where - unsolved = Bag.mapBag WcEvVar unsolved_flats `unionBags` - Bag.mapBag WcImplic unsolved_implics - - zonk_frozen (FrozenError frknd fl ty1 ty2) - = do { ty1z <- zonkTcType ty1 - ; ty2z <- zonkTcType ty2 - ; return (FrozenError frknd fl ty1z ty2z) } - - tyVarsOfFrozen fr - = unionVarSets $ bagToList (mapBag tvs_of_frozen fr) - tvs_of_frozen (FrozenError _ _ ty1 ty2) = tyVarsOfTypes [ty1,ty2] - - tidyFrozen env fr = mapBag (tidy_frozen env) fr - tidy_frozen env (FrozenError frknd fl ty1 ty2) - = FrozenError frknd fl (tidyType env ty1) (tidyType env ty2) - -reportTidyFrozens :: TidyEnv -> Bag FrozenError -> TcM () -reportTidyFrozens tidy_env fr = mapBagM_ (reportTidyFrozen tidy_env) fr - -reportTidyFrozen :: TidyEnv -> FrozenError -> TcM () -reportTidyFrozen tidy_env err@(FrozenError _ fl _ty1 _ty2) - = do { let dec_errs = decompFrozenError err - init_err_ctxt = CEC { cec_encl = [] - , cec_extra = empty - , cec_tidy = tidy_env } - ; mapM_ (report_dec_err init_err_ctxt) dec_errs } - where - report_dec_err err_ctxt (ty1,ty2) - -- The only annoying thing here is that in the given case, - -- the ``Inaccessible code'' message will be printed once for - -- each decomposed equality. - = do { (tidy_env2,extra2) - <- if isGiven fl - then return (cec_tidy err_ctxt, inaccessible_msg) - else getWantedEqExtra emptyTvSubst (cec_tidy err_ctxt) loc_orig ty1 ty2 - ; let err_ctxt2 = err_ctxt { cec_tidy = tidy_env2 - , cec_extra = cec_extra err_ctxt $$ extra2 } - ; setCtFlavorLoc fl $ - reportEqErr err_ctxt2 ty1 ty2 - } - - loc_orig | Wanted loc <- fl = ctLocOrigin loc - | Derived loc _ <- fl = ctLocOrigin loc - | otherwise = pprPanic "loc_orig" empty - - inaccessible_msg - | Given loc <- fl - = hang (ptext (sLit "Inaccessible code in")) 2 (mk_what loc) - | otherwise = pprPanic "inaccessible_msg" empty - - mk_what loc - = case ctLocOrigin loc of - PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor") - <+> quotes (ppr dc) <> comma - , ptext (sLit "in") <+> pprMatchContext mc ] - other_skol -> pprSkolInfo other_skol - - -decompFrozenError :: FrozenError -> [(TcType,TcType)] --- Postcondition: will always return a non-empty list -decompFrozenError (FrozenError errk _fl ty1 ty2) - | OccCheckError <- errk - = dec_occ_check ty1 ty2 - | otherwise - = [(ty1,ty2)] - where dec_occ_check :: TcType -> TcType -> [(TcType,TcType)] - -- This error arises from an original: - -- a ~ Maybe a - -- But by now the a has been substituted away, eg: - -- Int ~ Maybe Int - -- Maybe b ~ Maybe (Maybe b) - dec_occ_check ty1 ty2 - | tcEqType ty1 ty2 = [] - dec_occ_check ty1@(TyVarTy {}) ty2 = [(ty1,ty2)] - dec_occ_check (FunTy s1 t1) (FunTy s2 t2) - = let errs1 = dec_occ_check s1 s2 - errs2 = dec_occ_check t1 t2 - in errs1 ++ errs2 - dec_occ_check ty1@(TyConApp fn1 tys1) ty2@(TyConApp fn2 tys2) - | fn1 == fn2 && length tys1 == length tys2 - , not (isSynFamilyTyCon fn1) - = concatMap (\(t1,t2) -> dec_occ_check t1 t2) (zip tys1 tys2) - | otherwise - = [(ty1,ty2)] - dec_occ_check ty1 ty2 - | Just (s1,t1) <- tcSplitAppTy_maybe ty1 - , Just (s2,t2) <- tcSplitAppTy_maybe ty2 - = let errs1 = dec_occ_check s1 s2 - errs2 = dec_occ_check t1 t2 - in errs1 ++ errs2 - dec_occ_check ty1 ty2 = [(ty1,ty2)] - -reportUnsolvedWantedEvVars :: Bag WantedEvVar -> TcM () -reportUnsolvedWantedEvVars wanteds - | isEmptyBag wanteds - = return () - | otherwise - = do { wanteds <- mapBagM zonkWantedEvVar wanteds - ; env0 <- tcInitTidyEnv - ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfWantedEvVars wanteds) - tidy_unsolved = tidyWantedEvVars tidy_env wanteds - err_ctxt = CEC { cec_encl = [] - , cec_extra = empty - , cec_tidy = tidy_env } - ; groupErrs (reportFlat err_ctxt) (bagToList tidy_unsolved) } - -reportUnsolvedDeriv :: [PredType] -> WantedLoc -> TcM () -reportUnsolvedDeriv unsolved loc - | null unsolved - = return () - | otherwise - = setCtLoc loc $ - do { unsolved <- zonkTcThetaType unsolved - ; env0 <- tcInitTidyEnv - ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfTheta unsolved) - tidy_unsolved = map (tidyPred tidy_env) unsolved - err_ctxt = CEC { cec_encl = [] - , cec_extra = alt_fix - , cec_tidy = tidy_env } - ; reportFlat err_ctxt tidy_unsolved (ctLocOrigin loc) } - where - alt_fix = vcat [ptext (sLit "Alternatively, use a standalone 'deriving instance' declaration,"), - nest 2 $ ptext (sLit "so you can specify the instance context yourself")] + ; reportTidyWanteds err_ctxt tidy_wanted } -------------------------------------------- -- Internal functions @@ -210,32 +77,49 @@ reportUnsolvedDeriv unsolved loc data ReportErrCtxt = CEC { cec_encl :: [Implication] -- Enclosing implications -- (innermost first) - , cec_tidy :: TidyEnv - , cec_extra :: SDoc -- Add this to each error message + , cec_tidy :: TidyEnv + , cec_extra :: SDoc -- Add this to each error message + , cec_insol :: Bool -- True <=> we are reporting insoluble errors only + -- Main effect: don't say "Cannot deduce..." + -- when reporting equality errors; see misMatchOrCND } reportTidyImplic :: ReportErrCtxt -> Implication -> TcM () reportTidyImplic ctxt implic + | BracketSkol <- ctLocOrigin (ic_loc implic) + , not insoluble -- For Template Haskell brackets report only + = return () -- definite errors. The whole thing will be re-checked + -- later when we plug it in, and meanwhile there may + -- certainly be un-satisfied constraints + + | otherwise = reportTidyWanteds ctxt' (ic_wanted implic) where - ctxt' = ctxt { cec_encl = implic : cec_encl ctxt } - + insoluble = ic_insol implic + ctxt' = ctxt { cec_encl = implic : cec_encl ctxt + , cec_insol = insoluble } + reportTidyWanteds :: ReportErrCtxt -> WantedConstraints -> TcM () -reportTidyWanteds ctxt unsolved - = do { let (flats, implics) = splitWanteds unsolved - (ambigs, non_ambigs) = partition is_ambiguous (bagToList flats) +reportTidyWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics }) + | cec_insol ctxt -- If there are any insolubles, report only them + -- because they are unconditionally wrong + -- Moreover, if any of the insolubles are givens, stop right there + -- ignoring nested errors, because the code is inaccessible + = do { let (given, other) = partitionBag (isGiven . evVarX) insols + insol_implics = filterBag ic_insol implics + ; if isEmptyBag given + then do { mapBagM_ (reportInsoluble ctxt) other + ; mapBagM_ (reportTidyImplic ctxt) insol_implics } + else mapBagM_ (reportInsoluble ctxt) given } + + | otherwise -- No insoluble ones + = ASSERT( isEmptyBag insols ) + do { let (ambigs, non_ambigs) = partition is_ambiguous (bagToList flats) (tv_eqs, others) = partition is_tv_eq non_ambigs ; groupErrs (reportEqErrs ctxt) tv_eqs ; when (null tv_eqs) $ groupErrs (reportFlat ctxt) others - ; traceTc "rtw" (vcat [ - text "unsolved =" <+> ppr unsolved, - text "tveqs =" <+> ppr tv_eqs, - text "others =" <+> ppr others, - text "ambigs =" <+> ppr ambigs , - text "implics =" <+> ppr implics]) - - ; when (null tv_eqs) $ mapBagM_ (reportTidyImplic ctxt) implics + ; mapBagM_ (reportTidyImplic ctxt) implics -- Only report ambiguity if no other errors (at all) happened -- See Note [Avoiding spurious errors] in TcSimplify @@ -246,7 +130,7 @@ reportTidyWanteds ctxt unsolved -- Report equalities of form (a~ty) first. They are usually -- skolem-equalities, and they cause confusing knock-on -- effects in other errors; see test T4093b. - is_tv_eq c | EqPred ty1 ty2 <- wantedEvVarPred c + is_tv_eq c | EqPred ty1 ty2 <- evVarOfPred c = tcIsTyVarTy ty1 || tcIsTyVarTy ty2 | otherwise = False @@ -258,7 +142,21 @@ reportTidyWanteds ctxt unsolved is_ambiguous d = isTyVarClassPred pred && not (tyVarsOfPred pred `subVarSet` skols) where - pred = wantedEvVarPred d + pred = evVarOfPred d + +reportInsoluble :: ReportErrCtxt -> FlavoredEvVar -> TcM () +reportInsoluble ctxt (EvVarX ev flav) + | EqPred ty1 ty2 <- evVarPred ev + = setCtFlavorLoc flav $ + do { let ctxt2 = ctxt { cec_extra = cec_extra ctxt $$ inaccessible_msg } + ; reportEqErr ctxt2 ty1 ty2 } + | otherwise + = pprPanic "reportInsoluble" (pprEvVarWithType ev) + where + inaccessible_msg | Given loc <- flav + = hang (ptext (sLit "Inaccessible code in")) + 2 (ppr (ctLocOrigin loc)) + | otherwise = empty reportFlat :: ReportErrCtxt -> [PredType] -> CtOrigin -> TcM () -- The [PredType] are already tidied @@ -285,21 +183,26 @@ groupErrs :: ([PredType] -> CtOrigin -> TcM ()) -- Deal with one group groupErrs _ [] = return () groupErrs report_err (wanted : wanteds) - = do { setCtLoc the_loc $ + = do { setCtLoc the_loc $ report_err the_vars (ctLocOrigin the_loc) ; groupErrs report_err others } where - the_loc = wantedEvVarLoc wanted + the_loc = evVarX wanted the_key = mk_key the_loc - the_vars = map wantedEvVarPred (wanted:friends) + the_vars = map evVarOfPred (wanted:friends) (friends, others) = partition is_friend wanteds - is_friend friend = mk_key (wantedEvVarLoc friend) == the_key + is_friend friend = mk_key (evVarX friend) `same_key` the_key + + mk_key :: WantedLoc -> (SrcSpan, CtOrigin) + mk_key loc = (ctLocSpan loc, ctLocOrigin loc) + + same_key (s1, o1) (s2, o2) = s1==s2 && o1 `same_orig` o2 + same_orig (OccurrenceOf n1) (OccurrenceOf n2) = n1==n2 + same_orig ScOrigin ScOrigin = True + same_orig DerivOrigin DerivOrigin = True + same_orig DefaultOrigin DefaultOrigin = True + same_orig _ _ = False - mk_key :: WantedLoc -> (SrcSpan, String) - mk_key loc = (ctLocSpan loc, showSDoc (ppr (ctLocOrigin loc))) - -- It may seem crude to compare the error messages, - -- but it makes sure that we combine just what the user sees, - -- and it avoids need equality on InstLocs. -- Add the "arising from..." part to a message about bunch of dicts addArising :: CtOrigin -> SDoc -> SDoc @@ -308,17 +211,17 @@ addArising orig msg = msg $$ nest 2 (pprArising orig) pprWithArising :: [WantedEvVar] -> (WantedLoc, SDoc) -- Print something like -- (Eq a) arising from a use of x at y --- (Show a) arising froma use of p at q --- Also return a location for the erroe message +-- (Show a) arising from a use of p at q +-- Also return a location for the error message pprWithArising [] = panic "pprWithArising" -pprWithArising [WantedEvVar ev loc] +pprWithArising [EvVarX ev loc] = (loc, pprEvVarTheta [ev] <+> pprArising (ctLocOrigin loc)) pprWithArising ev_vars = (first_loc, vcat (map ppr_one ev_vars)) where - first_loc = wantedEvVarLoc (head ev_vars) - ppr_one (WantedEvVar v loc) + first_loc = evVarX (head ev_vars) + ppr_one (EvVarX v loc) = parens (pprPred (evVarPred v)) <+> pprArisingAt loc addErrorReport :: ReportErrCtxt -> SDoc -> TcM () @@ -332,20 +235,21 @@ pprErrCtxtLoc ctxt vcat [ ptext (sLit "or") <+> ppr_skol orig | orig <- origs ] where ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc) - ppr_skol skol_info = pprSkolInfo skol_info + ppr_skol skol_info = ppr skol_info -getUserGivens :: ReportErrCtxt -> Maybe [EvVar] --- Just gs => Say "could not deduce ... from gs" --- Nothing => No interesting givens, say something else +getUserGivens :: ReportErrCtxt -> [([EvVar], GivenLoc)] +-- One item for each enclosing implication getUserGivens (CEC {cec_encl = ctxt}) - | null user_givens = Nothing - | otherwise = Just user_givens - where - givens = foldl (\gs ic -> ic_given ic ++ gs) [] ctxt - user_givens | opt_PprStyle_Debug = givens - | otherwise = filterOut isSilentEvVar givens + = reverse $ + [ (givens', loc) | Implic {ic_given = givens, ic_loc = loc} <- ctxt + , let givens' = get_user_givens givens + , not (null givens') ] + where + get_user_givens givens | opt_PprStyle_Debug = givens + | otherwise = filterOut isSilentEvVar givens -- In user mode, don't show the "silent" givens, used for -- the "self" dictionary and silent superclass arguments for dfuns + \end{code} @@ -358,13 +262,15 @@ getUserGivens (CEC {cec_encl = ctxt}) \begin{code} reportIPErrs :: ReportErrCtxt -> [PredType] -> CtOrigin -> TcM () reportIPErrs ctxt ips orig - = addErrorReport ctxt $ addArising orig msg + = addErrorReport ctxt msg where - msg | Just givens <- getUserGivens ctxt - = couldNotDeduce givens ips - | otherwise - = sep [ ptext (sLit "Unbound implicit parameter") <> plural ips + givens = getUserGivens ctxt + msg | null givens + = addArising orig $ + sep [ ptext (sLit "Unbound implicit parameter") <> plural ips , nest 2 (pprTheta ips) ] + | otherwise + = couldNotDeduce givens (ips, orig) \end{code} @@ -378,17 +284,27 @@ reportIPErrs ctxt ips orig reportEqErrs :: ReportErrCtxt -> [PredType] -> CtOrigin -> TcM () -- The [PredType] are already tidied reportEqErrs ctxt eqs orig - = mapM_ report_one eqs + = do { orig' <- zonkTidyOrigin ctxt orig + ; mapM_ (report_one orig') eqs } where - env0 = cec_tidy ctxt - report_one (EqPred ty1 ty2) - = do { (env1, extra) <- getWantedEqExtra emptyTvSubst env0 orig ty1 ty2 - ; let ctxt' = ctxt { cec_tidy = env1 - , cec_extra = extra $$ cec_extra ctxt } + report_one orig (EqPred ty1 ty2) + = do { let extra = getWantedEqExtra orig ty1 ty2 + ctxt' = ctxt { cec_extra = extra $$ cec_extra ctxt } ; reportEqErr ctxt' ty1 ty2 } - report_one pred + report_one _ pred = pprPanic "reportEqErrs" (ppr pred) +getWantedEqExtra :: CtOrigin -> TcType -> TcType -> SDoc +getWantedEqExtra (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp })) + ty1 ty2 + -- If the types in the error message are the same as the types we are unifying, + -- don't add the extra expected/actual message + | act `tcEqType` ty1 && exp `tcEqType` ty2 = empty + | exp `tcEqType` ty1 && act `tcEqType` ty2 = empty + | otherwise = mkExpectedActualMsg act exp + +getWantedEqExtra orig _ _ = pprArising orig + reportEqErr :: ReportErrCtxt -> TcType -> TcType -> TcM () -- ty1 and ty2 are already tidied reportEqErr ctxt ty1 ty2 @@ -410,7 +326,7 @@ reportTyVarEqErr ctxt tv1 ty2 = -- sk ~ alpha: swap reportTyVarEqErr ctxt tv2 ty1 - | not is_meta1 + | (not is_meta1) = -- sk ~ ty, where ty isn't a meta-tyvar: mis-match addErrorReport (addExtraInfo ctxt ty1 ty2) (misMatchOrCND ctxt ty1 ty2) @@ -445,7 +361,7 @@ reportTyVarEqErr ctxt tv1 ty2 then ptext (sLit "This (rigid, skolem) type variable is") else ptext (sLit "These (rigid, skolem) type variables are")) <+> ptext (sLit "bound by") - , nest 2 $ pprSkolInfo (ctLocOrigin implic_loc) ] ] + , nest 2 $ ppr (ctLocOrigin implic_loc) ] ] ; addErrTcM (env1, msg $$ extra1 $$ mkEnvSigMsg (ppr tv1) env_sigs) } -- Nastiest case: attempt to unify an untouchable variable @@ -457,7 +373,7 @@ reportTyVarEqErr ctxt tv1 ty2 extra = quotes (ppr tv1) <+> sep [ ptext (sLit "is untouchable") , ptext (sLit "inside the constraints") <+> pprEvVarTheta given - , ptext (sLit "bound at") <+> pprSkolInfo (ctLocOrigin implic_loc)] + , ptext (sLit "bound at") <+> ppr (ctLocOrigin implic_loc)] ; addErrorReport (addExtraInfo ctxt ty1 ty2) (msg $$ nest 2 extra) } | otherwise -- This can happen, by a recursive decomposition of frozen @@ -491,25 +407,39 @@ mkTyFunInfoMsg ty1 ty2 misMatchOrCND :: ReportErrCtxt -> TcType -> TcType -> SDoc misMatchOrCND ctxt ty1 ty2 - = case getUserGivens ctxt of - Just givens -> couldNotDeduce givens [EqPred ty1 ty2] - Nothing -> misMatchMsg ty1 ty2 + | cec_insol ctxt = misMatchMsg ty1 ty2 -- If the equality is unconditionally + -- insoluble, don't report the context + | null givens = misMatchMsg ty1 ty2 + | otherwise = couldNotDeduce givens ([EqPred ty1 ty2], orig) + where + givens = getUserGivens ctxt + orig = TypeEqOrigin (UnifyOrigin ty1 ty2) + +couldNotDeduce :: [([EvVar], GivenLoc)] -> (ThetaType, CtOrigin) -> SDoc +couldNotDeduce givens (wanteds, orig) + = vcat [ hang (ptext (sLit "Could not deduce") <+> pprTheta wanteds) + 2 (pprArising orig) + , vcat pp_givens ] + where + pp_givens + = case givens of + [] -> [] + (g:gs) -> ppr_given (ptext (sLit "from the context")) g + : map (ppr_given (ptext (sLit "or from"))) gs -couldNotDeduce :: [EvVar] -> [PredType] -> SDoc -couldNotDeduce givens wanteds - = sep [ ptext (sLit "Could not deduce") <+> pprTheta wanteds - , nest 2 $ ptext (sLit "from the context") - <+> pprEvVarTheta givens] + ppr_given herald (gs,loc) + = hang (herald <+> pprEvVarTheta gs) + 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc) + , ptext (sLit "at") <+> ppr (ctLocSpan loc)]) addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt -- Add on extra info about the types themselves -- NB: The types themselves are already tidied addExtraInfo ctxt ty1 ty2 - = ctxt { cec_tidy = env2 - , cec_extra = nest 2 (extra1 $$ extra2) $$ cec_extra ctxt } + = ctxt { cec_extra = nest 2 (extra1 $$ extra2) $$ cec_extra ctxt } where - (env1, extra1) = typeExtraInfoMsg (cec_tidy ctxt) ty1 - (env2, extra2) = typeExtraInfoMsg env1 ty2 + extra1 = typeExtraInfoMsg (cec_encl ctxt) ty1 + extra2 = typeExtraInfoMsg (cec_encl ctxt) ty2 misMatchMsg :: TcType -> TcType -> SDoc -- Types are already tidy misMatchMsg ty1 ty2 = sep [ ptext (sLit "Couldn't match type") <+> quotes (ppr ty1) @@ -524,26 +454,22 @@ kindErrorMsg ty1 ty2 k1 = typeKind ty1 k2 = typeKind ty2 -typeExtraInfoMsg :: TidyEnv -> Type -> (TidyEnv, SDoc) +typeExtraInfoMsg :: [Implication] -> Type -> SDoc -- Shows a bit of extra info about skolem constants -typeExtraInfoMsg env ty +typeExtraInfoMsg implics ty | Just tv <- tcGetTyVar_maybe ty , isTcTyVar tv - , isSkolemTyVar tv || isSigTyVar tv - , not (isUnkSkol tv) - , let (env1, tv1) = tidySkolemTyVar env tv - = (env1, pprSkolTvBinding tv1) + , isSkolemTyVar tv + = pprSkolTvBinding implics tv where -typeExtraInfoMsg env _ty = (env, empty) -- Normal case +typeExtraInfoMsg _ _ = empty -- Normal case -------------------- unifyCtxt :: EqOrigin -> TidyEnv -> TcM (TidyEnv, SDoc) unifyCtxt (UnifyOrigin { uo_actual = act_ty, uo_expected = exp_ty }) tidy_env - = do { act_ty' <- zonkTcType act_ty - ; exp_ty' <- zonkTcType exp_ty - ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty' - (env2, act_ty'') = tidyOpenType env1 act_ty' - ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') } + = do { (env1, act_ty') <- zonkTidyTcType tidy_env act_ty + ; (env2, exp_ty') <- zonkTidyTcType env1 exp_ty + ; return (env2, mkExpectedActualMsg act_ty' exp_ty') } mkExpectedActualMsg :: Type -> Type -> SDoc mkExpectedActualMsg act_ty exp_ty @@ -578,18 +504,19 @@ reportDictErrs ctxt wanteds orig where mk_no_inst_err :: [PredType] -> SDoc mk_no_inst_err wanteds - | Just givens <- getUserGivens ctxt - = vcat [ addArising orig $ couldNotDeduce givens wanteds - , show_fixes (fix1 : fixes2) ] - - | otherwise -- Top level + | null givens -- Top level = vcat [ addArising orig $ - ptext (sLit "No instance") <> plural wanteds - <+> ptext (sLit "for") <+> pprTheta wanteds - , show_fixes fixes2 ] + ptext (sLit "No instance") <> plural min_wanteds + <+> ptext (sLit "for") <+> pprTheta min_wanteds + , show_fixes (fixes2 ++ fixes3) ] + | otherwise + = vcat [ couldNotDeduce givens (min_wanteds, orig) + , show_fixes (fix1 : (fixes2 ++ fixes3)) ] where - fix1 = sep [ ptext (sLit "add") <+> pprTheta wanteds + givens = getUserGivens ctxt + min_wanteds = mkMinimalBySCs wanteds + fix1 = sep [ ptext (sLit "add") <+> pprTheta min_wanteds <+> ptext (sLit "to the context of") , nest 2 $ pprErrCtxtLoc ctxt ] @@ -599,10 +526,17 @@ reportDictErrs ctxt wanteds orig pprTheta instance_dicts]] _ -> [sep [ptext (sLit "add instance declarations for"), pprTheta instance_dicts]] - instance_dicts = filterOut isTyVarClassPred wanteds + fixes3 = case orig of + DerivOrigin -> [drv_fix] + _ -> [] + + instance_dicts = filterOut isTyVarClassPred min_wanteds -- Insts for which it is worth suggesting an adding an -- instance declaration. Exclude tyvar dicts. + drv_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration,"), + nest 2 $ ptext (sLit "so you can specify the instance context yourself")] + show_fixes :: [SDoc] -> SDoc show_fixes [] = empty show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), @@ -701,7 +635,7 @@ reportAmbigErrs ctxt skols ambigs -- Divide into groups that share a common set of ambiguous tyvars = mapM_ report (equivClasses cmp ambigs_w_tvs) where - ambigs_w_tvs = [ (d, varSetElems (tyVarsOfWantedEvVar d `minusVarSet` skols)) + ambigs_w_tvs = [ (d, varSetElems (tyVarsOfEvVarX d `minusVarSet` skols)) | d <- ambigs ] cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2 @@ -725,7 +659,7 @@ mkMonomorphismMsg :: ReportErrCtxt -> [TcTyVar] -> TcM (TidyEnv, SDoc) -- ASSUMPTION: the Insts are fully zonked mkMonomorphismMsg ctxt inst_tvs = do { dflags <- getDOpts - ; traceTc "Mono" (vcat (map pprSkolTvBinding inst_tvs)) + ; traceTc "Mono" (vcat (map (pprSkolTvBinding (cec_encl ctxt)) inst_tvs)) ; (tidy_env, docs) <- findGlobals ctxt (mkVarSet inst_tvs) ; return (tidy_env, mk_msg dflags docs) } where @@ -752,6 +686,35 @@ monomorphism_fix dflags -- if it is not already set! +pprSkolTvBinding :: [Implication] -> TcTyVar -> SDoc +-- Print info about the binding of a skolem tyvar, +-- or nothing if we don't have anything useful to say +pprSkolTvBinding implics tv + | isTcTyVar tv = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv) + | otherwise = quotes (ppr tv) <+> ppr_skol (getSkolemInfo implics tv) + where + ppr_details (SkolemTv {}) = ppr_skol (getSkolemInfo implics tv) + ppr_details (FlatSkol {}) = ptext (sLit "is a flattening type variable") + ppr_details (RuntimeUnk {}) = ptext (sLit "is an interactive-debugger skolem") + ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") + <+> quotes (ppr n) + ppr_details (MetaTv _ _) = ptext (sLit "is a meta type variable") + + + ppr_skol UnkSkol = ptext (sLit "is an unknown type variable") -- Unhelpful + ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type") + ppr_skol info = sep [ptext (sLit "is a rigid type variable bound by"), + sep [ppr info, + ptext (sLit "at") <+> ppr (getSrcLoc tv)]] + +getSkolemInfo :: [Implication] -> TcTyVar -> SkolemInfo +getSkolemInfo [] tv + = WARN( True, ptext (sLit "No skolem info:") <+> ppr tv ) + UnkSkol +getSkolemInfo (implic:implics) tv + | tv `elemVarSet` ic_skols implic = ctLocOrigin (ic_loc implic) + | otherwise = getSkolemInfo implics tv + ----------------------- -- findGlobals looks at the value environment and finds values whose -- types mention any of the offending type variables. It has to be @@ -787,27 +750,25 @@ findGlobals ctxt tvs find_thing :: TidyEnv -> (TcType -> Bool) -> TcTyThing -> TcM (TidyEnv, Maybe SDoc) find_thing tidy_env ignore_it (ATcId { tct_id = id }) - = do { id_ty <- zonkTcType (idType id) - ; if ignore_it id_ty then + = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env (idType id) + ; if ignore_it tidy_ty then return (tidy_env, Nothing) else do - { let (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty - msg = sep [ ppr id <+> dcolon <+> ppr tidy_ty + { let msg = sep [ ppr id <+> dcolon <+> ppr tidy_ty , nest 2 (parens (ptext (sLit "bound at") <+> ppr (getSrcLoc id)))] ; return (tidy_env', Just msg) } } find_thing tidy_env ignore_it (ATyVar tv ty) - = do { tv_ty <- zonkTcType ty - ; if ignore_it tv_ty then + = do { (tidy_env1, tidy_ty) <- zonkTidyTcType tidy_env ty + ; if ignore_it tidy_ty then return (tidy_env, Nothing) else do { let -- The name tv is scoped, so we don't need to tidy it - (tidy_env1, tidy_ty) = tidyOpenType tidy_env tv_ty msg = sep [ ptext (sLit "Scoped type variable") <+> quotes (ppr tv) <+> eq_stuff , nest 2 bound_at] - eq_stuff | Just tv' <- tcGetTyVar_maybe tv_ty + eq_stuff | Just tv' <- tcGetTyVar_maybe tidy_ty , getOccName tv == getOccName tv' = empty | otherwise = equals <+> ppr tidy_ty -- It's ok to use Type.getTyVar_maybe because ty is zonked by now @@ -817,16 +778,22 @@ find_thing tidy_env ignore_it (ATyVar tv ty) find_thing _ _ thing = pprPanic "find_thing" (ppr thing) -warnDefaulting :: [WantedEvVar] -> Type -> TcM () +warnDefaulting :: [FlavoredEvVar] -> Type -> TcM () warnDefaulting wanteds default_ty = do { warn_default <- doptM Opt_WarnTypeDefaults + ; env0 <- tcInitTidyEnv + ; let wanted_bag = listToBag wanteds + tidy_env = tidyFreeTyVars env0 $ + tyVarsOfEvVarXs wanted_bag + tidy_wanteds = mapBag (tidyFlavoredEvVar tidy_env) wanted_bag + (loc, ppr_wanteds) = pprWithArising (map get_wev (bagToList tidy_wanteds)) + warn_msg = hang (ptext (sLit "Defaulting the following constraint(s) to type") + <+> quotes (ppr default_ty)) + 2 ppr_wanteds ; setCtLoc loc $ warnTc warn_default warn_msg } where - -- Tidy them first - warn_msg = vcat [ ptext (sLit "Defaulting the following constraint(s) to type") <+> - quotes (ppr default_ty), - nest 2 ppr_wanteds ] - (loc, ppr_wanteds) = pprWithArising wanteds + get_wev (EvVarX ev (Wanted loc)) = EvVarX ev loc -- Yuk + get_wev ev = pprPanic "warnDefaulting" (ppr ev) \end{code} Note [Runtime skolems] @@ -843,7 +810,6 @@ are created by in RtClosureInspect.zonkRTTIType. %************************************************************************ \begin{code} - solverDepthErrorTcS :: Int -> [CanonicalCt] -> TcS a solverDepthErrorTcS depth stack | null stack -- Shouldn't happen unless you say -fcontext-stack=0 @@ -851,12 +817,11 @@ solverDepthErrorTcS depth stack | otherwise = wrapErrTcS $ setCtFlavorLoc (cc_flavor top_item) $ - do { env0 <- tcInitTidyEnv - ; let ev_vars = map cc_id stack - env1 = tidyFreeTyVars env0 free_tvs - free_tvs = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet ev_vars - extra = pprEvVars (map (tidyEvVar env1) ev_vars) - ; failWithTcM (env1, hang msg 2 extra) } + do { ev_vars <- mapM (zonkEvVar . cc_id) stack + ; env0 <- tcInitTidyEnv + ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfEvVars ev_vars) + tidy_ev_vars = map (tidyEvVar tidy_env) ev_vars + ; failWithTcM (tidy_env, hang msg 2 (pprEvVars tidy_ev_vars)) } where top_item = head stack msg = vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int depth @@ -881,43 +846,28 @@ flattenForAllErrorTcS fl ty _bad_eqs \begin{code} setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a -setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing -setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing -setCtFlavorLoc (Given loc) thing = setCtLoc loc thing - -getWantedEqExtra :: TvSubst -> TidyEnv -> CtOrigin -> TcType -> TcType - -> TcM (TidyEnv, SDoc) -getWantedEqExtra subst env0 (TypeEqOrigin item) ty1 ty2 - -- If the types in the error message are the same - -- as the types we are unifying (remember to zonk the latter) - -- don't add the extra expected/actual message - -- - -- The complication is that the types in the TypeEqOrigin must - -- (a) be zonked - -- (b) have any TcS-monad pending equalities applied to them - -- (hence the passed-in substitution) - = do { (env1, act) <- zonkSubstTidy env0 subst (uo_actual item) - ; (env2, exp) <- zonkSubstTidy env1 subst (uo_expected item) - ; if (act `tcEqType` ty1 && exp `tcEqType` ty2) - || (exp `tcEqType` ty1 && act `tcEqType` ty2) - then - return (env0, empty) - else - return (env2, mkExpectedActualMsg act exp) } - -getWantedEqExtra _ env0 orig _ _ - = return (env0, pprArising orig) - -zonkSubstTidy :: TidyEnv -> TvSubst -> TcType -> TcM (TidyEnv, TcType) --- In general, becore printing a type, we want to --- a) Zonk it. Even during constraint simplification this is --- is important, to un-flatten the flatten skolems in a type --- b) Substitute any solved unification variables. This is --- only important *during* solving, becuase after solving --- the substitution is expressed in the mutable type variables --- But during solving there may be constraint (F xi ~ ty) --- where the substitution has not been applied to the RHS -zonkSubstTidy env subst ty - = do { ty' <- zonkTcTypeAndSubst subst ty - ; return (tidyOpenType env ty') } +setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing +setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing +setCtFlavorLoc (Given loc) thing = setCtLoc loc thing +\end{code} + +%************************************************************************ +%* * + Tidying +%* * +%************************************************************************ + +\begin{code} +zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType) +zonkTidyTcType env ty = do { ty' <- zonkTcType ty + ; return (tidyOpenType env ty') } + +zonkTidyOrigin :: ReportErrCtxt -> CtOrigin -> TcM CtOrigin +zonkTidyOrigin ctxt (TypeEqOrigin (UnifyOrigin { uo_actual = act, uo_expected = exp })) + = do { (env1, act') <- zonkTidyTcType (cec_tidy ctxt) act + ; (_env2, exp') <- zonkTidyTcType env1 exp + ; return (TypeEqOrigin (UnifyOrigin { uo_actual = act', uo_expected = exp' })) } + -- Drop the returned env on the floor; we may conceivably thereby get + -- inconsistent naming between uses of this function +zonkTidyOrigin _ orig = return orig \end{code} diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index 297b4e884e924411667c44dd283f13a92c481604..3f5a258ed3648bb5ab174e01e027187300edf275 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -82,7 +82,7 @@ tcPolyExpr expr res_ty tcPolyExprNC expr res_ty = do { traceTc "tcPolyExprNC" (ppr res_ty) - ; (gen_fn, expr') <- tcGen (GenSkol res_ty) res_ty $ \ _ rho -> + ; (gen_fn, expr') <- tcGen GenSigCtxt res_ty $ \ _ rho -> tcMonoExprNC expr rho ; return (mkLHsWrap gen_fn expr') } @@ -191,7 +191,7 @@ tcExpr (ExprWithTySig expr sig_ty) res_ty -- Remember to extend the lexical type-variable environment ; (gen_fn, expr') - <- tcGen (SigSkol ExprSigCtxt) sig_tc_ty $ \ skol_tvs res_ty -> + <- tcGen ExprSigCtxt sig_tc_ty $ \ skol_tvs res_ty -> tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` mkTyVarTys skol_tvs) $ -- See Note [More instantiated than scoped] in TcBinds tcMonoExprNC expr res_ty @@ -819,7 +819,8 @@ tcApp fun args res_ty -- Typecheck the result, thereby propagating -- info (if any) from result into the argument types -- Both actual_res_ty and res_ty are deeply skolemised - ; co_res <- unifyType actual_res_ty res_ty + ; co_res <- addErrCtxt (funResCtxt fun) $ + unifyType actual_res_ty res_ty -- Typecheck the arguments ; args1 <- tcArgs fun args expected_arg_tys @@ -1384,6 +1385,10 @@ funAppCtxt fun arg arg_no quotes (ppr fun) <> text ", namely"]) 2 (quotes (ppr arg)) +funResCtxt :: LHsExpr Name -> SDoc +funResCtxt fun + = ptext (sLit "In the return type of a call of") <+> quotes (ppr fun) + badFieldTypes :: [(Name,TcType)] -> SDoc badFieldTypes prs = hang (ptext (sLit "Record update for insufficiently polymorphic field") diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index 5bc73338d20de5bb8f0df3bc61be6d062ee9f382..b7b572f82834be7eb0f4dbd8ef6cc48db9126961 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -1075,7 +1075,7 @@ zonkTypeCollecting unbound_tv_set = zonkType (mkZonkTcTyVar zonk_unbound_tyvar) where zonk_unbound_tyvar tv - = do { tv' <- zonkQuantifiedTyVar tv + = do { tv' <- zonkQuantifiedTyVar tv ; tv_set <- readMutVar unbound_tv_set ; writeMutVar unbound_tv_set (extendVarSet tv_set tv') ; return (mkTyVarTy tv') } diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index 43e58be31e860db38ced6c7e5e37a17be3e67778..71eb55ed6c07333d8c8da33d12a60716aac5268f 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -867,7 +867,7 @@ tcPatSig ctxt sig res_ty ; if null sig_tvs then do { -- The type signature binds no type variables, -- and hence is rigid, so use it to zap the res_ty - wrap <- tcSubType PatSigOrigin (SigSkol ctxt) res_ty sig_ty + wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty ; return (sig_ty, [], wrap) } else do { @@ -896,7 +896,7 @@ tcPatSig ctxt sig res_ty ; sig_tvs' <- tcInstSigTyVars sig_tvs ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty sig_tv_tys' = mkTyVarTys sig_tvs' - ; wrap <- tcSubType PatSigOrigin (SigSkol ctxt) res_ty sig_ty' + ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty' -- Check that each is bound to a distinct type variable, -- and one that is not already in scope diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index 1979c8d96b61522f234726f7b27e6afc19ed3c30..ab788d7eedc8d976d37e764731ce04b1e6a5c7c8 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -13,7 +13,6 @@ import TcBinds import TcTyClsDecls import TcClassDcl import TcPat( addInlinePrags ) -import TcSimplify( simplifyTop ) import TcRnMonad import TcMType import TcType @@ -621,7 +620,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) setSrcSpan loc $ addErrCtxt (instDeclCtxt2 (idType dfun_id)) $ do { -- Instantiate the instance decl with skolem constants - ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolSigType skol_info (idType dfun_id) + ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id) ; let (clas, inst_tys) = tcSplitDFunHead inst_head (class_tyvars, sc_theta, _, op_items) = classBigSig clas sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta @@ -633,16 +632,15 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) ; orig_ev_vars <- newEvVars orig_theta ; let dfun_ev_vars = silent_ev_vars ++ orig_ev_vars - ; (sc_binds, sc_dicts, sc_args) - <- mapAndUnzip3M (tcSuperClass n_ty_args dfun_ev_vars) sc_theta' + ; (sc_dicts, sc_args) + <- mapAndUnzipM (tcSuperClass n_ty_args dfun_ev_vars) sc_theta' -- Check that any superclasses gotten from a silent arguemnt -- can be deduced from the originally-specified dfun arguments ; ct_loc <- getCtLoc ScOrigin ; _ <- checkConstraints skol_info inst_tyvars orig_ev_vars $ - emitConstraints $ listToBag $ - [ WcEvVar (WantedEvVar sc ct_loc) - | sc <- sc_dicts, isSilentEvVar sc ] + emitFlats $ listToBag $ + [ mkEvVarX sc ct_loc | sc <- sc_dicts, isSilentEvVar sc ] -- Deal with 'SPECIALISE instance' pragmas -- See Note [SPECIALISE instance pragmas] @@ -698,7 +696,6 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) , abs_binds = unitBag dict_bind } ; return (unitBag (L loc main_bind) `unionBags` - unionManyBags sc_binds `unionBags` listToBag meth_binds) } where @@ -708,23 +705,17 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) loc = getSrcSpan dfun_id ------------------------------ -tcSuperClass :: Int -> [EvVar] -> PredType -> TcM (LHsBinds Id, Id, DFunArg CoreExpr) +tcSuperClass :: Int -> [EvVar] -> PredType -> TcM (EvVar, DFunArg CoreExpr) +-- All superclasses should be either +-- (a) be one of the arguments to the dfun, of +-- (b) be a constant, soluble at top level tcSuperClass n_ty_args ev_vars pred | Just (ev, i) <- find n_ty_args ev_vars - = return (emptyBag, ev, DFunLamArg i) + = return (ev, DFunLamArg i) | otherwise - = ASSERT2( isEmptyVarSet (tyVarsOfPred pred), ppr pred) - do { sc_dict <- newWantedEvVar pred - ; loc <- getCtLoc ScOrigin - ; ev_binds <- simplifyTop (unitBag (WcEvVar (WantedEvVar sc_dict loc))) - ; let ev_wrap = WpLet (EvBinds ev_binds) - sc_bind = mkVarBind sc_dict (noLoc $ (wrapId ev_wrap sc_dict)) - ; return (unitBag sc_bind, sc_dict, DFunConstArg (Var sc_dict)) } - -- It's very important to solve the superclass constraint *in isolation* - -- so that it isn't generated by superclass selection from something else - -- We then generate the (also rather degenerate) top-level binding: - -- sc_dict = let sc_dict = in sc_dict - -- where is generated by solving the implication constraint + = ASSERT2( isEmptyVarSet (tyVarsOfPred pred), ppr pred) -- Constant! + do { sc_dict <- emitWanted ScOrigin pred + ; return (sc_dict, DFunConstArg (Var sc_dict)) } where find _ [] = Nothing find i (ev:evs) | pred `tcEqPred` evVarPred ev = Just (ev, i) @@ -863,7 +854,7 @@ tcSpecInst dfun_id prag@(SpecInstSig hs_ty) ; (tyvars, theta, clas, tys) <- tcHsInstHead hs_ty ; let (_, spec_dfun_ty) = mkDictFunTy tyvars theta clas tys - ; co_fn <- tcSubType (SpecPragOrigin name) (SigSkol SpecInstCtxt) + ; co_fn <- tcSubType (SpecPragOrigin name) SpecInstCtxt (idType dfun_id) spec_dfun_ty ; return (SpecPrag dfun_id co_fn defaultInlinePragma) } where diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 30b1ae1924f34f35c89dfc861c20ed99c361f1ee..f9d3d97cdca23eee6c19fe67ce66b34b3cd3f4b4 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -1,7 +1,8 @@ \begin{code} module TcInteract ( - solveInteract, AtomicInert, tyVarsOfInert, - InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts + solveInteract, solveInteractGiven, solveInteractWanted, + AtomicInert, tyVarsOfInert, + InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, ) where #include "HsVersions.h" @@ -18,6 +19,7 @@ import Var import TcType import HsBinds +import Inst( tyVarsOfEvVar ) import InstEnv import Class import TyCon @@ -25,8 +27,6 @@ import Name import FunDeps -import Control.Monad ( when ) - import Coercion import Outputable @@ -36,7 +36,8 @@ import TcSMonad import Bag import qualified Data.Map as Map -import Control.Monad( unless ) +import Control.Monad( when ) + import FastString ( sLit ) import DynFlags \end{code} @@ -84,80 +85,89 @@ implication constraint (when in top-level inference mode). \begin{code} -data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts - -- Invariant: all Given or Derived +data CCanMap a = CCanMap { cts_given :: Map.Map a CanonicalCts + -- Invariant: all Given + , cts_derived :: Map.Map a CanonicalCts + -- Invariant: all Derived , cts_wanted :: Map.Map a CanonicalCts } -- Invariant: all Wanted + cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts -cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap) - where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap) +cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap) + where rest_wder = Map.fold unionBags rest_der (cts_wanted cmap) + rest_der = Map.fold unionBags emptyCCan (cts_derived cmap) emptyCCanMap :: CCanMap a -emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty } +emptyCCanMap = CCanMap { cts_given = Map.empty + , cts_derived = Map.empty, cts_wanted = Map.empty } updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a updCCanMap (a,ct) cmap = case cc_flavor ct of Wanted {} -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) } - _ - -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) } + Given {} + -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) } + Derived {} + -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) } where this_ct = singleCCan ct getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a) -- Gets the relevant constraints and returns the rest of the CCanMap getRelevantCts a cmap - = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap)) - (Map.findWithDefault emptyCCan a (cts_givder cmap)) + = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap) + , Map.findWithDefault emptyCCan a (cts_given cmap) + , Map.findWithDefault emptyCCan a (cts_derived cmap) ] residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap) - , cts_givder = Map.delete a (cts_givder cmap) } + , cts_given = Map.delete a (cts_given cmap) + , cts_derived = Map.delete a (cts_derived cmap) } in (relevant, residual_map) -extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a) --- Gets the wanted constraints and returns a residual CCanMap -extractUnsolvedCMap cmap = - let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap) - in (unsolved, cmap { cts_wanted = Map.empty}) +extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a) +-- Gets the wanted or derived constraints and returns a residual +-- CCanMap with only givens. +extractUnsolvedCMap cmap = + let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap) + derd = Map.fold unionBags emptyCCan (cts_derived cmap) + in (wntd `unionBags` derd, + cmap { cts_wanted = Map.empty, cts_derived = Map.empty }) + -- See Note [InertSet invariants] data InertSet = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan) - - , inert_dicts :: CCanMap Class -- Dictionaries only + , inert_dicts :: CCanMap Class -- Dictionaries only , inert_ips :: CCanMap (IPName Name) -- Implicit parameters - , inert_funeqs :: CCanMap TyCon -- Type family equalities only + , inert_frozen :: CanonicalCts + , inert_funeqs :: CCanMap TyCon -- Type family equalities only -- This representation allows us to quickly get to the relevant -- inert constraints when interacting a work item with the inert set. - - - , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already - -- and reside either in the worklist or in the inerts } tyVarsOfInert :: InertSet -> TcTyVarSet tyVarsOfInert (IS { inert_eqs = eqs , inert_dicts = dictmap , inert_ips = ipmap - , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts - where cts = eqs `andCCan` cCanMapToBag dictmap - `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap - -type FDImprovement = (PredType,PredType) -type FDImprovements = [(PredType,PredType)] + , inert_frozen = frozen + , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts + where + cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap + `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap instance Outputable InertSet where ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is)) - , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is))) + , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is))) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is))) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is))) + , vcat (map ppr (Bag.bagToList $ inert_frozen is)) ] emptyInert :: InertSet emptyInert = IS { inert_eqs = Bag.emptyBag + , inert_frozen = Bag.emptyBag , inert_dicts = emptyCCanMap , inert_ips = emptyCCanMap - , inert_funeqs = emptyCCanMap - , inert_fds = [] } + , inert_funeqs = emptyCCanMap } updInertSet :: InertSet -> AtomicInert -> InertSet updInertSet is item @@ -171,101 +181,27 @@ updInertSet is item | Just tc <- isCFunEqCan_Maybe item -- Function equality = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) } | otherwise - = pprPanic "Unknown form of constraint!" (ppr item) - -updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet -updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is } -updInertSetFDImprs is Nothing = is - -foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a --- Fold over the equalities of the inerts -foldISEqCtsM k z IS { inert_eqs = eqs } - = Bag.foldlBagM k z eqs - -foldISEqCts :: (a -> AtomicInert -> a) -> a -> InertSet -> a -foldISEqCts k z IS { inert_eqs = eqs } - = Bag.foldlBag k z eqs + = is { inert_frozen = inert_frozen is `Bag.snocBag` item } extractUnsolved :: InertSet -> (InertSet, CanonicalCts) --- Postcondition: the canonical cts returnd are the very same as the --- WantedEvVars in their canonical form. +-- Postcondition: the returned canonical cts are either Derived, or Wanted. extractUnsolved is@(IS {inert_eqs = eqs}) = let is_solved = is { inert_eqs = solved_eqs , inert_dicts = solved_dicts , inert_ips = solved_ips - , inert_funeqs = solved_funeqs } + , inert_frozen = emptyCCan + , inert_funeqs = solved_funeqs } in (is_solved, unsolved) - where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs + where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenCt) eqs (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is) (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is) (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is) - unsolved = unsolved_eqs `unionBags` + unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags` unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs - -haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool -haveBeenImproved [] _ _ = False -haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2' - | tcEqPred pty1 pty1' && tcEqPred pty2 pty2' - = True - | tcEqPred pty1 pty2' && tcEqPred pty2 pty1' - = True - | otherwise - = haveBeenImproved fdimprs pty1' pty2' - -getFDImprovements :: InertSet -> FDImprovements --- Return a list of the improvements that have kicked in so far -getFDImprovements = inert_fds - \end{code} -{-- DV: This note will go away! - -Note [Touchables and givens] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Touchable variables will never show up in givens which are inputs to -the solver. However, touchables may show up in givens generated by the flattener. -For example, - - axioms: - G Int ~ Char - F Char ~ Int - - wanted: - F (G alpha) ~w Int - -canonicalises to - - G alpha ~g b - F b ~w Int - -which can be put in the inert set. Suppose we also have a wanted - - alpha ~w Int - -We cannot rewrite the given G alpha ~g b using the wanted alpha ~w -Int. Instead, after reacting alpha ~w Int with the whole inert set, -we observe that we can solve it by unifying alpha with Int, so we mark -it as solved and put it back in the *work list*. [We also immediately unify -alpha := Int, without telling anyone, see trySpontaneousSolve function, to -avoid doing this in the end.] - -Later, because it is solved (given, in effect), we can use it to rewrite -G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually, -we will dispatch the remaining wanted constraints using the top-level axioms. - -Finally, note that after reacting a wanted equality with the entire inert set -we may end up with something like - - b ~w alpha - -which we should flip around to generate the solved constraint alpha ~s b. - --} - - - %********************************************************************* %* * * Main Interaction Solver * @@ -399,70 +335,106 @@ React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canoni -- returning an extended inert set. -- -- See Note [Touchables and givens]. -solveInteract :: InertSet -> Bag (CtFlavor,EvVar) -> TcS InertSet +solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet +solveInteractGiven inert gloc evs + = do { (_, inert_ret) <- solveInteract inert $ listToBag $ + map mk_given evs + ; return inert_ret } + where + flav = Given gloc + mk_given ev = mkEvVarX ev flav + +solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet +solveInteractWanted inert wvs + = do { (_,inert_ret) <- solveInteract inert $ listToBag $ + map wantedToFlavored wvs + ; return inert_ret } + +solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet) +-- Post: (True, inert_set) means we managed to discharge all constraints +-- without actually doing any interactions! +-- (False, inert_set) means some interactions occurred solveInteract inert ws = do { dyn_flags <- getDynFlags - ; sctx <- getTcSContext - - ; traceTcS "solveInteract, before clever canonicalization:" $ - ppr (mapBag (\(ct,ev) -> (ct,evVarPred ev)) ws) - - ; can_ws <- foldlBagM (tryPreSolveAndCanon sctx inert) emptyCCan ws - - ; traceTcS "solveInteract, after clever canonicalization:" $ - ppr can_ws - - ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert can_ws } - -tryPreSolveAndCanon :: SimplContext -> InertSet -> CanonicalCts -> (CtFlavor, EvVar) -> TcS CanonicalCts --- Checks if this constraint can be immediately solved from a constraint in the --- inert set or in the previously encountered CanonicalCts and only then --- canonicalise it. See Note [Avoiding the superclass explosion] -tryPreSolveAndCanon sctx is cts_acc (fl,ev_var) - | ClassP clas tys <- evVarPred ev_var - , not $ simplEqsOnly sctx -- And we *can* discharge constraints from other constraints - = do { let (relevant_inert_dicts,_) = getRelevantCts clas (inert_dicts is) - ; b <- dischargeFromCans (cts_acc `unionBags` relevant_inert_dicts) - (fl,ev_var,clas,tys) - ; extra_cts <- if b then return emptyCCan else mkCanonical fl ev_var - ; return (cts_acc `unionBags` extra_cts) } - | otherwise - = do { extra_cts <- mkCanonical fl ev_var - ; return (cts_acc `unionBags` extra_cts) } + ; sctx <- getTcSContext + + ; traceTcS "solveInteract, before clever canonicalization:" $ + vcat [ text "ws = " <+> ppr (mapBag (\(EvVarX ev ct) + -> (ct,evVarPred ev)) ws) + , text "inert = " <+> ppr inert ] + + ; (flag, inert_ret) <- foldlBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws + + ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $ + vcat [ text "No interaction happened = " <+> ppr flag + , text "inert_ret = " <+> ppr inert_ret ] + + ; return (flag, inert_ret) } + + +tryPreSolveAndInteract :: SimplContext + -> DynFlags + -> (Bool, InertSet) + -> FlavoredEvVar + -> TcS (Bool, InertSet) +-- Returns: True if it was able to discharge this constraint AND all previous ones +tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert) + flavev@(EvVarX ev_var fl) + = do { let inert_cts = get_inert_cts (evVarPred ev_var) + + ; this_one_discharged <- dischargeFromCCans inert_cts flavev + + ; if this_one_discharged + then return (all_previous_discharged, inert) -dischargeFromCans :: CanonicalCts -> (CtFlavor,EvVar,Class,[Type]) -> TcS Bool -dischargeFromCans cans (fl,ev,clas,tys) - = Bag.foldlBagM discharge_ct False cans - where discharge_ct :: Bool -> CanonicalCt -> TcS Bool + else do + { extra_cts <- mkCanonical fl ev_var + ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) + inert extra_cts + ; return (False, inert_ret) } } + + where + get_inert_cts (ClassP clas _) + | simplEqsOnly sctx = emptyCCan + | otherwise = fst (getRelevantCts clas (inert_dicts inert)) + get_inert_cts (IParam {}) + = emptyCCan -- We must not do the same thing for IParams, because (contrary + -- to dictionaries), work items /must/ override inert items. + -- See Note [Overriding implicit parameters] in TcInteract. + get_inert_cts (EqPred {}) + = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert) + +dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool +dischargeFromCCans cans (EvVarX ev fl) + = Bag.foldlBagM discharge_ct False cans + where discharge_ct :: Bool -> CanonicalCt -> TcS Bool discharge_ct True _ct = return True - discharge_ct False (CDictCan { cc_id = ev1, cc_flavor = fl1 - , cc_class = clas1, cc_tyargs = tys1 }) - | clas1 == clas - , (and $ zipWith tcEqType tys tys1) - , fl1 `canSolve` fl - = setEvBind ev (EvId ev1) >> return True + discharge_ct False ct + | evVarPred (cc_id ct) `tcEqPred` evVarPred ev + , cc_flavor ct `canSolve` fl + = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) + ; return True } + where set_ev_bind x y + | EqPred {} <- evVarPred y + = setEvBind x (EvCoercion (mkCoVarCoercion y)) + | otherwise = setEvBind x (EvId y) discharge_ct False _ct = return False \end{code} Note [Avoiding the superclass explosion] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Consider the example: - f = [(0,1,0,1,0)] -We have 5 wanted (Num alpha) constraints. If we simply try to canonicalize and add them -in our worklist, we will also get all of their superclasses as Derived, hence we will -have an inert set that contains 5*n constraints, where n is the number of superclasses -of of Num. That is bad for the additional reason that we keep *all* the Derived, even -for identical class constraints (for reasons related to recursive dictionaries). - -Instead, what we do with tryPreSolveAndCanon, is when we encounter a new constraint, -such as the second (Num alpha) above we very quickly see if it can be immediately -discharged by a class constraint in our inert set or the previous canonicals. If so, -we add nothing to the returned canonical constraints. - -For our particular example this will reduce the size of the inert set that we use from -5*n to just n. And hence the number of all possible interactions that we have to look -through is significantly smaller! +This note now is not as significant as it used to be because we no +longer add the superclasses of Wanted as Derived, except only if they +have equality superclasses or superclasses with functional +dependencies. The fear was that hundreds of identical wanteds would +give rise each to the same superclass or equality Derived's which +would lead to a blo-up in the number of interactions. + +Instead, what we do with tryPreSolveAndCanon, is when we encounter a +new constraint, we very quickly see if it can be immediately +discharged by a class constraint in our inert set or the previous +canonicals. If so, we add nothing to the returned canonical +constraints. \begin{code} solveOne :: InertSet -> WorkItem -> TcS InertSet @@ -630,13 +602,16 @@ trySpontaneousEqOneWay cv gw tv xi -- so we have its more specific kind in our hands ; if kxi `isSubKind` tyVarKind tv then solveWithIdentity cv gw tv xi - else if tyVarKind tv `isSubKind` kxi then + else return SPCantSolve +{- + else if tyVarKind tv `isSubKind` kxi then return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way -- This case covers the a_touchable :: * ~ b_untouchable :: ?? -- which has to be deferred or floated out for someone else to solve -- it in a scope where 'b' is no longer untouchable. else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors] ; return SPError } +-} } | otherwise -- Still can't solve, sig tyvar and non-variable rhs = return SPCantSolve @@ -650,8 +625,9 @@ trySpontaneousEqTwoWay cv gw tv1 tv2 | k2 `isSubKind` k1 = solveWithIdentity cv gw tv1 (mkTyVarTy tv2) | otherwise -- None is a subkind of the other, but they are both touchable! - = do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2) - ; return SPError } + = return SPCantSolve + -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2) + -- ; return SPError } where k1 = tyVarKind tv1 k2 = tyVarKind tv2 @@ -681,24 +657,24 @@ so this situation can't happen. Note [Spontaneous solving and kind compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note that our canonical constraints insist that *all* equalities (tv ~ +xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible* +the same kinds. ("compatible" means one is a subKind of the other.) -Note that our canonical constraints insist that only *given* equalities (tv ~ xi) -or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds. - - - We have to require this because: - Given equalities can be freely used to rewrite inside - other types or constraints. - - We do not have to do the same for wanteds because: - First, wanted equations (tv ~ xi) where tv is a touchable - unification variable may have kinds that do not agree (the - kind of xi must be a sub kind of the kind of tv). Second, any - potential kind mismatch will result in the constraint not - being soluble, which will be reported anyway. This is the - reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@ - will perform a kind compatibility check, and only then will - they proceed to @solveWithIdentity@. - -Caveat: + - It can't be *equal* kinds, because + b) wanted constraints don't necessarily have identical kinds + eg alpha::? ~ Int + b) a solved wanted constraint becomes a given + + - SPJ thinks that *given* constraints (tv ~ tau) always have that + tau has a sub-kind of tv; and when solving wanted constraints + in trySpontaneousEqTwoWay we re-orient to achieve this. + + - Note that the kind invariant is maintained by rewriting. + Eg wanted1 rewrites wanted2; if both were compatible kinds before, + wanted2 will be afterwards. Similarly givens. + +Caveat: - Givens from higher-rank, such as: type family T b :: * -> * -> * type instance T Bool = (->) @@ -746,18 +722,15 @@ solveWithIdentity cv wd tv xi text "Right Kind is : " <+> ppr (typeKind xi) ] - ; setWantedTyBind tv xi -- Set tv := xi_unflat - ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi + ; setWantedTyBind tv xi + ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi - ; case wd of Wanted {} -> setWantedCoBind cv xi - Derived {} -> setDerivedCoBind cv xi - _ -> pprPanic "Can't spontaneously solve given!" empty + ; when (isWanted wd) (setWantedCoBind cv xi) + -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)' ; return $ SPSolved (CTyEqCan { cc_id = cv_given , cc_flavor = mkGivenFlavor wd UnkSkol - , cc_tyvar = tv, cc_rhs = xi }) - } - + , cc_tyvar = tv, cc_rhs = xi }) } \end{code} @@ -785,8 +758,6 @@ data InteractResult , ir_new_work :: WorkList -- new work items to add to the WorkList - - , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in } -- What to do with the inert reactant. @@ -795,13 +766,10 @@ data InertAction = KeepInert | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult -mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing +mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult -mkIRStop keep newWork = return $ IR Stop keep newWork Nothing - -mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult -mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr) +mkIRStop keep newWork = return $ IR Stop keep newWork dischargeWorkItem :: Monad m => m InteractResult dischargeWorkItem = mkIRStop KeepInert emptyWorkList @@ -814,22 +782,18 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert --------------------------------------------------- --- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we --- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've +-- Interact a single WorkItem with the equalities of an inert set as +-- far as possible, i.e. until we get a Stop result from an individual +-- reaction (i.e. when the WorkItem is consumed), or until we've -- interact the WorkItem with the entire equalities of the InertSet interactWithInertEqsStage :: SimplifierStage interactWithInertEqsStage workItem inert - = foldISEqCtsM interactNext initITR inert - where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- Will fold over equalities - , inert_dicts = inert_dicts inert - , inert_ips = inert_ips inert - , inert_funeqs = inert_funeqs inert - , inert_fds = inert_fds inert - } - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } - + = Bag.foldlBagM interactNext initITR (inert_eqs inert) + where + initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan } + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } --------------------------------------------------- -- Interact a single WorkItem with *non-equality* constraints in the inert set. @@ -846,8 +810,12 @@ interactWithInertsStage workItem inert in Bag.foldlBagM interactNext initITR relevant where getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) - getISRelevant (CDictCan { cc_class = cls } ) is - = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is) + getISRelevant (CFrozenErr {}) is = (emptyCCan, is) + -- Nothing s relevant; we have alread interacted + -- it with the equalities in the inert set + + getISRelevant (CDictCan { cc_class = cls } ) is + = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is) in (relevant, is { inert_dicts = residual_map }) getISRelevant (CFunEqCan { cc_fun = tc } ) is = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is) @@ -870,14 +838,12 @@ interactNext :: StageResult -> AtomicInert -> TcS StageResult interactNext it inert | ContinueWith workItem <- sr_stop it = do { let inerts = sr_inerts it - fdimprs_old = getFDImprovements inerts - ; ir <- interactWithInert fdimprs_old inert workItem + ; ir <- interactWithInert inert workItem -- New inerts depend on whether we KeepInert or not and must -- be updated with FD improvement information from the interaction result (ir) - ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir) - upd_inert = case ir_inert_action ir of + ; let inerts_new = case ir_inert_action ir of KeepInert -> inerts `updInertSet` inert DropInert -> inerts KeepTransformedInert inert' -> inerts `updInertSet` inert' @@ -889,26 +855,13 @@ interactNext it inert = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert } -- Do a single interaction of two constraints. -interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult -interactWithInert fdimprs inert workitem +interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult +interactWithInert inert workitem = do { ctxt <- getTcSContext ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem - inert_ev = cc_id inert - work_ev = cc_id workitem - - -- Never interact a wanted and a derived where the derived's evidence - -- mentions the wanted evidence in an unguarded way. - -- See Note [Superclasses and recursive dictionaries] - -- and Note [New Wanted Superclass Work] - -- We don't have to do this for givens, as we fully know the evidence for them. - ; rec_ev_ok <- - case (cc_flavor inert, cc_flavor workitem) of - (Wanted {}, Derived {}) -> isGoodRecEv work_ev inert_ev - (Derived {}, Wanted {}) -> isGoodRecEv inert_ev work_ev - _ -> return True - - ; if is_allowed && rec_ev_ok then - doInteractWithInert fdimprs inert workitem + + ; if is_allowed then + doInteractWithInert inert workitem else noInteraction workitem } @@ -920,10 +873,10 @@ allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only allowedInteraction _ _ _ = True -------------------------------------------- -doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult +doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult -- Identical class constraints. -doInteractWithInert fdimprs +doInteractWithInert (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2) @@ -939,24 +892,16 @@ doInteractWithInert fdimprs eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc -- See Note [Efficient Orientation] - ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs - ; fd_work <- canWanteds wevvars - -- See Note [Generating extra equalities] - ; traceTcS "Checking if improvements existed." (ppr fdimprs) - ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then - -- Must keep going - mkIRContinue workItem KeepInert fd_work - else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2)) - ; mkIRStop_RecordImprovement KeepInert - (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2) - } - -- See Note [FunDep Reactions] + ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs + ; fd_work <- mapM mkCanonicalFEV derived_evs + -- See Note [Generating extra equalities] + + ; mkIRContinue workItem KeepInert (unionManyBags fd_work) } -- Class constraint and given equality: use the equality to rewrite -- the class constraint. -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) +doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfTypes xis @@ -965,8 +910,7 @@ doInteractWithInert _fdimprs -- interactWithEqsStage, so the dictionary is inert. ; mkIRContinue rewritten_dict KeepInert emptyWorkList } -doInteractWithInert _fdimprs - (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) +doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfTypes xis @@ -975,16 +919,14 @@ doInteractWithInert _fdimprs -- Class constraint and given equality: use the equality to rewrite -- the class constraint. -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) +doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty }) | ifl `canRewrite` wfl , tv `elemVarSet` tyVarsOfType ty = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) ; mkIRContinue rewritten_ip KeepInert emptyWorkList } -doInteractWithInert _fdimprs - (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) +doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi }) | wfl `canRewrite` ifl , tv `elemVarSet` tyVarsOfType ty @@ -996,8 +938,7 @@ doInteractWithInert _fdimprs -- that equates the type (this is "improvement"). -- However, we don't actually need the coercion evidence, -- so we just generate a fresh coercion variable that isn't used anywhere. -doInteractWithInert _fdimprs - (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) +doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 }) | nm1 == nm2 && isGiven wfl && isGiven ifl = -- See Note [Overriding implicit parameters] @@ -1023,8 +964,7 @@ doInteractWithInert _fdimprs -- we know about equalities. -- Inert: equality, work item: function equality -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) +doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi2 }) | ifl `canRewrite` wfl @@ -1034,8 +974,7 @@ doInteractWithInert _fdimprs -- Must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality -doInteractWithInert _fdimprs - (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc +doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 }) | wfl `canRewrite` ifl @@ -1051,8 +990,7 @@ doInteractWithInert _fdimprs -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] } -- At the end, which is *not* inert. So we should unfortunately DropInert here. -doInteractWithInert _fdimprs - (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 +doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , cc_tyargs = args1, cc_rhs = xi1 }) workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2 , cc_tyargs = args2, cc_rhs = xi2 }) @@ -1065,8 +1003,7 @@ doInteractWithInert _fdimprs where lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) -doInteractWithInert _fdimprs - (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) +doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 @@ -1084,8 +1021,20 @@ doInteractWithInert _fdimprs = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) ; mkIRContinue workItem DropInert rewritten_eq } +doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) + (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) + | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 + = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) + ; mkIRStop KeepInert rewritten_frozen } + +doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 }) + workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) + | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2 + = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) + ; mkIRContinue workItem DropInert rewritten_frozen } + -- Fall-through case for all other situations -doInteractWithInert _fdimprs _ workItem = noInteraction workItem +doInteractWithInert _ workItem = noInteraction workItem ------------------------- -- Equational Rewriting @@ -1098,7 +1047,9 @@ rewriteDict (cv,tv,xi) (dv,gw,cl,xis) ; dv' <- newDictVar cl args ; case gw of Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co)) - _given_or_derived -> setDictBind dv' (EvCast dv dict_co) + Given {} -> setDictBind dv' (EvCast dv dict_co) + Derived {} -> return () -- Derived dicts we don't set any evidence + ; return (CDictCan { cc_id = dv' , cc_flavor = gw , cc_class = cl @@ -1111,7 +1062,9 @@ rewriteIP (cv,tv,xi) (ipid,gw,nm,ty) ; ipid' <- newIPVar nm ty' ; case gw of Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co)) - _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co) + Given {} -> setIPBind ipid' (EvCast ipid ip_co) + Derived {} -> return () -- Derived ips: we don't set any evidence + ; return (CIPCan { cc_id = ipid' , cc_flavor = gw , cc_ip_nm = nm @@ -1131,9 +1084,11 @@ rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F ar fun_co `mkTransCoercion` mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co ; return cv2' } - _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2' $ + Given {} -> newGivenCoVar (mkTyConApp tc args') xi2' $ mkSymCoercion fun_co `mkTransCoercion` mkCoVarCoercion cv2 `mkTransCoercion` xi2_co + Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2') + ; return (CFunEqCan { cc_id = cv2' , cc_flavor = gw , cc_tyargs = args' @@ -1161,9 +1116,11 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) ; setWantedCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2' ; return cv2' } - _giv_or_der - -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $ + Given {} + -> newGivenCoVar (mkTyVarTy tv2) xi2' $ mkCoVarCoercion cv2 `mkTransCoercion` co2' + Derived {} + -> newDerivedId (EqPred (mkTyVarTy tv2) xi2') ; canEq gw cv2' (mkTyVarTy tv2) xi2' } @@ -1192,39 +1149,66 @@ rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) co1 `mkTransCoercion` mkCoVarCoercion cv2' ; return cv2' } (False,LeftComesFromInert) -> - newGivOrDerCoVar xi2 xi1 $ - mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 + if isGiven gw then + newGivenCoVar xi2 xi1 $ + mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 + else newDerivedId (EqPred xi2 xi1) (False,RightComesFromInert) -> - newGivOrDerCoVar xi1 xi2 $ - mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 - ; mkCanonical gw cv2' - } + if isGiven gw then + newGivenCoVar xi1 xi2 $ + mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 + else newDerivedId (EqPred xi1 xi2) + ; mkCanonical gw cv2' } -solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult +rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList +rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) + = do { cv2' <- + case fl2 of + Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b' + -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1] + ; setWantedCoBind cv2 $ + co2a' `mkTransCoercion` + mkCoVarCoercion cv2' `mkTransCoercion` + mkSymCoercion co2b' + ; return cv2' } + + Given {} -> newGivenCoVar ty2a' ty2b' $ + mkSymCoercion co2a' `mkTransCoercion` + mkCoVarCoercion cv2 `mkTransCoercion` + co2b' + + Derived {} -> newDerivedId (EqPred ty2a' ty2b') + ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) } + where + (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b + ty2a' = substTyWith [tv1] [xi1] ty2a + ty2b' = substTyWith [tv1] [xi1] ty2b + + co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1] + co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] + +solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult -- First argument inert, second argument workitem. They both represent -- wanted/given/derived evidence for the *same* predicate so we try here to -- discharge one directly from the other. -- -- Precondition: value evidence only (implicit parameters, classes) -- not coercion -solveOneFromTheOther (iid,ifl) workItem - -- Both derived needs a special case. You might think that we do not need - -- two evidence terms for the same claim. But, since the evidence is partial, - -- either evidence may do in some cases; see TcSMonad.isGoodRecEv. - -- See also Example 3 in Note [Superclasses and recursive dictionaries] - | isDerived ifl && isDerived wfl - = noInteraction workItem - +solveOneFromTheOther (iid,ifl) workItem | ifl `canSolve` wfl - = do { unless (isGiven wfl) $ setEvBind wid (EvId iid) + = do { when (isWanted wfl) $ setEvBind wid (EvId iid) -- Overwrite the binding, if one exists -- For Givens, which are lambda-bound, nothing to overwrite, ; dischargeWorkItem } - - | otherwise -- wfl `canSolve` ifl - = do { unless (isGiven ifl) $ setEvBind iid (EvId wid) + | wfl `canSolve` ifl + = do { when (isWanted ifl) $ setEvBind iid (EvId wid) ; mkIRContinue workItem DropInert emptyWorkList } + | otherwise -- One of the two is Derived, we can just throw it away, + -- preferrably the work item. + = if isDerived wfl then dischargeWorkItem + else mkIRContinue workItem DropInert emptyWorkList + where wfl = cc_flavor workItem wid = cc_id workItem @@ -1245,8 +1229,9 @@ our worklist. When we simplify a wanted constraint, if we first see a matching instance, we may produce new wanted work. To (1) avoid doing this work twice in the future and (2) to handle recursive dictionaries we may ``cache'' -this item as solved (in effect, given) into our inert set and with that add -its superclass constraints (as given) in our worklist. +this item as given into our inert set WITHOUT adding its superclass constraints, +otherwise we'd be in danger of creating a loop [In fact this was the exact reason +for doing the isGoodRecEv check in an older version of the type checker]. But now we have added partially solved constraints to the worklist which may interact with other wanteds. Consider the example: @@ -1257,17 +1242,12 @@ Example 1: instance Eq a => Foo [a] a --- fooDFun and wanted (Foo [t] t). We are first going to see that the instance matches -and create an inert set that includes the solved (Foo [t] t) and its -superclasses. +and create an inert set that includes the solved (Foo [t] t) but not its superclasses: d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3 - d2 :_g Eq t d2 := EvSuperClass d1 0 Our work list is going to contain a new *wanted* goal d3 :_w Eq t -It is wrong to react the wanted (Eq t) with the given (Eq t) because that would -construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert. -OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries, -at all? Consider +Ok, so how do we get recursive dictionaries, at all: Example 2: @@ -1584,7 +1564,8 @@ we keep the synonym-using RHS without expansion. \begin{code} -- If a work item has any form of interaction with top-level we get this data TopInteractResult - = NoTopInt -- No top-level interaction + = NoTopInt -- No top-level interaction + -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item)) | SomeTopInt { tir_new_work :: WorkList -- Sub-goals or new work (could be given, -- for superclasses) @@ -1621,10 +1602,9 @@ tryTopReact workitem else return NoTopInt } -allowedTopReaction :: Bool -> WorkItem -> Bool +allowedTopReaction :: Bool -> WorkItem -> Bool allowedTopReaction eqs_only (CDictCan {}) = not eqs_only -allowedTopReaction _ _ = True - +allowedTopReaction _ _ = True doTopReact :: WorkItem -> TcS TopInteractResult -- The work item does not react with the inert set, so try interaction with top-level instances @@ -1638,7 +1618,7 @@ doTopReact (CDictCan { cc_flavor = Given {} }) = return NoTopInt -- NB: Superclasses already added since it's canonical -- Derived dictionary: just look for functional dependencies -doTopReact workItem@(CDictCan { cc_flavor = Derived loc _ +doTopReact workItem@(CDictCan { cc_flavor = Derived loc , cc_class = cls, cc_tyargs = xis }) = do { fd_work <- findClassFunDeps cls xis loc ; if isEmptyWorkList fd_work then @@ -1654,15 +1634,9 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv) ; fd_work <- findClassFunDeps cls xis loc - ; if isEmptyWorkList fd_work then - return $ SomeTopInt - { tir_new_work = emptyWorkList - , tir_new_inert = ContinueWith workItem } - else -- More fundep work produced, just thow him back in the - -- worklist to prioritize the solution of fd equalities - return $ SomeTopInt - { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem - , tir_new_inert = Stop } } + ; return $ SomeTopInt + { tir_new_work = fd_work + , tir_new_inert = ContinueWith workItem } } GenInst wtvs ev_term -> -- Solved -- No need to do fundeps stuff here; the instance @@ -1674,12 +1648,12 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc ; if null wtvs -- Solved in one step and no new wanted work produced. -- i.e we directly matched a top-level instance - -- No point in caching this in 'inert' + -- No point in caching this in 'inert'; hence Stop then return $ SomeTopInt { tir_new_work = emptyWorkList , tir_new_inert = Stop } -- Solved and new wanted work produced, you may cache the - -- (tentatively solved) dictionary as Derived + -- (tentatively solved) dictionary as Given! (used to be: Derived) else do { let solved = makeSolvedByInst workItem ; return $ SomeTopInt { tir_new_work = inst_work @@ -1708,9 +1682,9 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl coe `mkTransCoercion` mkCoVarCoercion cv' ; return cv' } - _ -> newGivOrDerCoVar xi rhs_ty $ - mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe - + Given {} -> newGivenCoVar xi rhs_ty $ + mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe + Derived {} -> newDerivedId (EqPred xi rhs_ty) ; can_cts <- mkCanonical fl cv' ; return $ SomeTopInt can_cts Stop } _ @@ -1729,10 +1703,11 @@ findClassFunDeps cls xis loc = do { instEnvs <- getInstEnvs ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs) (ClassP cls xis, pprArisingAt loc) - ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs + ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs -- NB: fundeps generate some wanted equalities, but -- we don't use their evidence for anything - ; canWanteds wevvars } + ; cts <- mapM mkCanonicalFEV derived_evs + ; return $ unionManyBags cts } \end{code} @@ -1861,19 +1836,10 @@ We are choosing option 2 below but we might consider having a flag as well. Note [New Wanted Superclass Work] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Even in the case of wanted constraints, we add all of its superclasses as -new given work. There are several reasons for this: - a) to minimise error messages; - eg suppose we have wanted (Eq a, Ord a) - then we report only (Ord a) unsoluble - - b) to make the smallest number of constraints when *inferring* a type - (same Eq/Ord example) +Even in the case of wanted constraints, we may add some superclasses +as new given work. The reason is: - c) for recursive dictionaries we *must* add the superclasses - so that we can use them when solving a sub-problem - - d) To allow FD-like improvement for type families. Assume that + To allow FD-like improvement for type families. Assume that we have a class class C a b | a -> b and we have to solve the implication constraint: @@ -1899,7 +1865,11 @@ new given work. There are several reasons for this: equalities that have a touchable in their RHS, *in addition* to solving wanted equalities. -Here is another example where this is useful. +We also need to somehow use the superclasses to quantify over a minimal, +constraint see note [Minimize by Superclasses] in TcSimplify. + + +Finally, here is another example where this is useful. Example 1: ---------- @@ -1937,8 +1907,6 @@ NB: The desugarer needs be more clever to deal with equalities that participate in recursive dictionary bindings. \begin{code} - - data LookupInstResult = NoInstance | GenInst [WantedEvVar] EvTerm @@ -1966,7 +1934,7 @@ matchClassInst clas tys loc return (GenInst [] (EvDFunApp dfun_id tys [])) else do { ev_vars <- instDFunConstraints theta - ; let wevs = [WantedEvVar w loc | w <- ev_vars] + ; let wevs = [EvVarX w loc | w <- ev_vars] ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) } } } diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index ef4ad34c7da5ef8baf1ebc7839efd02c7ef8a867..b68fee5fcc2eb3cc160118de8e4846da9d316ee5 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -18,6 +18,7 @@ module TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, + mkTcTyVarName, newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, isFilledMetaTyVar, isFlexiMetaTyVar, @@ -34,9 +35,9 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstSigTyVars, - tcInstType, tcInstSigType, instMetaTyVar, - tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, + tcInstType, instMetaTyVar, + tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType, + tcSkolDFunType, tcSuperSkolTyVars, -------------------------------- -- Checking type validity @@ -50,15 +51,18 @@ module TcMType ( -------------------------------- -- Zonking zonkType, mkZonkTcTyVar, zonkTcPredType, - zonkTcTypeCarefully, skolemiseUnboundMetaTyVar, + zonkTcTypeCarefully, + skolemiseUnboundMetaTyVar, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, - zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar, + zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar, + zonkWC, zonkWantedEvVars, zonkTcTypeAndSubst, tcGetGlobalTyVars, + readKindVar, writeKindVar ) where @@ -89,10 +93,11 @@ import BasicTypes import SrcLoc import Outputable import FastString +import Unique( Unique ) import Bag import Control.Monad -import Data.List ( (\\) ) +import Data.List ( (\\) ) \end{code} @@ -207,62 +212,51 @@ tcInstType inst_tyvars ty ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars') -- Either the tyvars are freshly made, by inst_tyvars, - -- or (in the call from tcSkolSigType) any nested foralls - -- have different binders. Either way, zipTopTvSubst is ok + -- or any nested foralls have different binders. + -- Either way, zipTopTvSubst is ok ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) ; return (tyvars', theta, tau) } -mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar -mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) - -tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType) +tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type signature with skolem constants, but -- do *not* give them fresh names, because we want the name to -- be in the type environment: it is lexically scoped. -tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty +tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty -tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] +tcSuperSkolTyVars :: [TyVar] -> [TcTyVar] -- Make skolem constants, but do *not* give them new names, as above -tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info - | tv <- tyvars ] +-- Moreover, make them "super skolems"; see comments with superSkolemTv +tcSuperSkolTyVars tyvars + = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv + | tv <- tyvars ] -tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar +tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar -- Instantiate the tyvar, using -- * the occ-name and kind of the supplied tyvar, -- * the unique from the monad, -- * the location either from the tyvar (skol_info = SigSkol) --- or from the monad (otehrwise) -tcInstSkolTyVar skol_info tyvar +-- or from the monad (otherwise) +tcInstSkolTyVar overlappable tyvar = do { uniq <- newUnique - ; loc <- case skol_info of - SigSkol {} -> return (getSrcSpan old_name) - _ -> getSrcSpanM + ; loc <- getSrcSpanM ; let new_name = mkInternalName uniq occ loc - ; return (mkSkolTyVar new_name kind skol_info) } + ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) } where old_name = tyVarName tyvar occ = nameOccName old_name kind = tyVarKind tyvar -tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] --- Get the location from the monad -tcInstSkolTyVars info tyvars - = mapM (tcInstSkolTyVar info) tyvars +tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars -tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars + +tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type with fresh skolem constants -- Binding location comes from the monad -tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty - -tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType) --- Instantiate with skolems or meta SigTvs; depending on use_skols --- Always take location info from the supplied tyvars -tcInstSigType use_skols name ty - | use_skols - = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty - | otherwise - = tcInstType tcInstSigTyVars ty +tcInstSkolType ty = tcInstType tcInstSkolTyVars ty tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar] -- Make meta SigTv type variables for patten-bound scoped type varaibles @@ -284,20 +278,25 @@ newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newMetaTyVar meta_info kind = 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" + ; let name = mkTcTyVarName uniq s + s = case meta_info of + TauTv -> fsLit "t" + TcsTv -> fsLit "u" + SigTv _ -> fsLit "a" ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } +mkTcTyVarName :: Unique -> FastString -> Name +-- Make sure that fresh TcTyVar names finish with a digit +-- leaving the un-cluttered names free for user names +mkTcTyVarName uniq str = mkSysTvName uniq str + 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 <- newMetaUnique ; ref <- newMutVar Flexi - ; let name = setNameUnique (tyVarName tyvar) uniq + ; let name = mkSystemName uniq (getOccName tyvar) kind = tyVarKind tyvar ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } @@ -309,8 +308,6 @@ readWantedCoVar :: CoVar -> TcM MetaDetails readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar ) readMutVar (metaTvRef covar) - - isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable isFilledMetaTyVar tv @@ -467,7 +464,6 @@ zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars) ----------------- Types - zonkTcTypeCarefully :: TcType -> TcM TcType -- Do not zonk type variables free in the environment zonkTcTypeCarefully ty @@ -480,10 +476,11 @@ zonkTcTypeCarefully ty | otherwise = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkType (zonk_tv env_tvs) ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType (zonk_tv env_tvs) ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of Flexi -> return (TyVarTy tv) Indirect ty -> zonkType (zonk_tv env_tvs) ty } @@ -496,10 +493,11 @@ zonkTcTyVar :: TcTyVar -> TcM TcType zonkTcTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkTcType ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkTcType ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of Flexi -> return (TyVarTy tv) Indirect ty -> zonkTcType ty } @@ -509,10 +507,11 @@ zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty where zonk_tv tv = case tcTyVarDetails tv of - SkolemTv {} -> return (TyVarTy tv) - FlatSkol ty -> zonkType zonk_tv ty - MetaTv _ ref -> do { cts <- readMutVar ref - ; case cts of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType zonk_tv ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of Flexi -> zonk_flexi tv Indirect ty -> zonkType zonk_tv ty } zonk_flexi tv @@ -552,8 +551,8 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar zonkQuantifiedTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv) - SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv) + SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen? + do { kind <- zonkTcType (tyVarKind tv) ; return $ setTyVarKind tv kind } -- It might be a skolem type variable, -- for example from a user type signature @@ -565,23 +564,26 @@ zonkQuantifiedTyVar tv (readMutVar _ref >>= \cts -> case cts of Flexi -> return () - Indirect ty -> WARN( True, ppr tv $$ ppr ty ) + Indirect ty -> WARN( True, ppr tv $$ ppr ty ) return ()) >> #endif - skolemiseUnboundMetaTyVar UnkSkol tv - -skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar + skolemiseUnboundMetaTyVar tv vanillaSkolemTv + _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk + +skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> 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 +skolemiseUnboundMetaTyVar tv details = ASSERT2( isMetaTyVar tv, ppr tv ) - do { uniq <- newUnique -- Remove it from TcMetaTyVar unique land + do { span <- getSrcSpanM -- Get the location from "here" + -- ie where we are generalising + ; 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 skol_info + final_name = mkInternalName uniq (getOccName tv) span + final_tv = mkTcTyVar final_name final_kind details ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} @@ -589,24 +591,59 @@ skolemiseUnboundMetaTyVar skol_info tv \begin{code} zonkImplication :: Implication -> TcM Implication zonkImplication implic@(Implic { ic_given = given - , ic_wanted = wanted }) - = do { given' <- mapM zonkEvVar given - ; wanted' <- mapBagM zonkWanted wanted - ; return (implic { ic_given = given', ic_wanted = wanted' }) } + , ic_wanted = wanted + , ic_loc = loc }) + = do { -- No need to zonk the skolems + ; given' <- mapM zonkEvVar given + ; loc' <- zonkGivenLoc loc + ; wanted' <- zonkWC wanted + ; return (implic { ic_given = given' + , ic_wanted = wanted' + , ic_loc = loc' }) } zonkEvVar :: EvVar -> TcM EvVar zonkEvVar var = do { ty' <- zonkTcType (varType var) ; return (setVarType var ty') } -zonkWanted :: WantedConstraint -> TcM WantedConstraint -zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') } -zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') } +zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar +zonkFlavoredEvVar (EvVarX ev fl) + = do { ev' <- zonkEvVar ev + ; fl' <- zonkFlavor fl + ; return (EvVarX ev' fl') } + +zonkWC :: WantedConstraints -> TcM WantedConstraints +zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) + = do { flat' <- zonkWantedEvVars flat + ; implic' <- mapBagM zonkImplication implic + ; insol' <- mapBagM zonkFlavoredEvVar insol + ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) } + +zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar) +zonkWantedEvVars = mapBagM zonkWantedEvVar zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar -zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) } +zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) } + +zonkFlavor :: CtFlavor -> TcM CtFlavor +zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') } +zonkFlavor fl = return fl + +zonkGivenLoc :: GivenLoc -> TcM GivenLoc +-- GivenLocs may have unification variables inside them! +zonkGivenLoc (CtLoc skol_info span ctxt) + = do { skol_info' <- zonkSkolemInfo skol_info + ; return (CtLoc skol_info' span ctxt) } + +zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo +zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty + ; return (SigSkol cx ty') } +zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys + ; return (InferSkol ntys') } + where + do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') } +zonkSkolemInfo skol_info = return skol_info \end{code} - Note [Silly Type Synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: @@ -734,6 +771,7 @@ mkZonkTcTyVar unbound_var_fn tyvar = ASSERT( isTcTyVar tyvar ) case tcTyVarDetails tyvar of SkolemTv {} -> return (TyVarTy tyvar) + RuntimeUnk {} -> return (TyVarTy tyvar) FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty MetaTv _ ref -> do { cts <- readMutVar ref ; case cts of @@ -844,7 +882,9 @@ checkValidType ctxt ty = do ForSigCtxt _ -> gen_rank 1 SpecInstCtxt -> gen_rank 1 - ThBrackCtxt -> gen_rank 1 + ThBrackCtxt -> gen_rank 1 + GenSigCtxt -> panic "checkValidType" + -- Can't happen; GenSigCtxt not used for *user* sigs actual_kind = typeKind ty diff --git a/compiler/typecheck/TcMatches.lhs b/compiler/typecheck/TcMatches.lhs index 46b67da9be0db0b97d2bd7c2ac176342933b9fca..24533608cc1817b36495d21ae1668c19eedb72e6 100644 --- a/compiler/typecheck/TcMatches.lhs +++ b/compiler/typecheck/TcMatches.lhs @@ -73,7 +73,7 @@ tcMatchesFun fun_name inf matches exp_ty ; checkArgs fun_name matches ; (wrap_gen, (wrap_fun, group)) - <- tcGen (SigSkol (FunSigCtxt fun_name)) exp_ty $ \ _ exp_rho -> + <- tcGen (FunSigCtxt fun_name) exp_ty $ \ _ exp_rho -> -- Note [Polymorphic expected type for tcMatchesFun] matchFunTys herald arity exp_rho $ \ pat_tys rhs_ty -> tcMatches match_ctxt pat_tys rhs_ty matches diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index a82584cc069c4849a0588d66df257afb7c12ca65..d28e901325e6c3de4f85802248260e02bb137f16 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -669,10 +669,7 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys ; checkExistentials ex_tvs penv - ; let skol_info = case pe_ctxt penv of - LamPat mc -> PatSkol data_con mc - LetPat {} -> UnkSkol -- Doesn't matter - ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs + ; ex_tvs' <- tcInstSuperSkolTyVars ex_tvs -- Get location from monad, not from ex_tvs ; let pat_ty' = mkTyConApp tycon ctxt_res_tys @@ -704,14 +701,17 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside -- order is *important* as we generate the list of -- dictionary binders from theta' no_equalities = not (any isEqPred theta') - + skol_info = case pe_ctxt penv of + LamPat mc -> PatSkol data_con mc + LetPat {} -> UnkSkol -- Doesn't matter + ; gadts_on <- xoptM Opt_GADTs ; checkTc (no_equalities || gadts_on) (ptext (sLit "A pattern match on a GADT requires -XGADTs")) -- Trac #2905 decided that a *pattern-match* of a GADT -- should require the GADT language flag - ; given <- newEvVars theta' + ; given <- newEvVars theta' ; (ev_binds, (arg_pats', res)) <- checkConstraints skol_info ex_tvs' given $ tcConArgs data_con arg_tys' arg_pats penv thing_inside diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index 773f307053344ef19f2aa8a070867c3f1c72b02f..ae3e2faf54b3f1f454c207ce78213cc7022b85da 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -505,6 +505,7 @@ tcRnHsBootDecls decls ; traceTc "Tc3" empty ; (tcg_env, inst_infos, _deriv_binds) <- tcInstDecls1 (concat tycl_decls) inst_decls deriv_decls + ; setGblEnv tcg_env $ do { -- Typecheck value declarations @@ -639,7 +640,11 @@ checkHiBootIface = case [dfun | inst <- local_insts, let dfun = instanceDFunId inst, idType dfun `tcEqType` boot_inst_ty ] of - [] -> do { addErrTc (instMisMatch boot_inst); return Nothing } + [] -> do { traceTc "check_inst" (vcat [ text "local_insts" <+> vcat (map (ppr . idType . instanceDFunId) local_insts) + , text "boot_inst" <+> ppr boot_inst + , text "boot_inst_ty" <+> ppr boot_inst_ty + ]) + ; addErrTc (instMisMatch boot_inst); return Nothing } (dfun:_) -> return (Just (local_boot_dfun, dfun)) where boot_dfun = instanceDFunId boot_inst @@ -1308,9 +1313,16 @@ tcRnExpr hsc_env ictxt rdr_expr -- Now typecheck the expression; -- it might have a rank-2 type (e.g. :t runST) - ((_tc_expr, res_ty), lie) <- captureConstraints (tcInferRho rn_expr) ; - ((qtvs, dicts, _), lie_top) <- captureConstraints (simplifyInfer False {- No MR for now -} - (tyVarsOfType res_ty) lie) ; + + uniq <- newUnique ; + let { fresh_it = itName uniq } ; + ((_tc_expr, res_ty), lie) <- captureConstraints (tcInferRho rn_expr) ; + ((qtvs, dicts, _), lie_top) <- captureConstraints $ + simplifyInfer TopLevel + False {- No MR for now -} + [(fresh_it, res_ty)] + lie ; + _ <- simplifyInteractive lie_top ; -- Ignore the dicionary bindings let { all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty) } ; diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs index 6cfbc20fc9855f9bb4b3f8c22d7778b643044edf..37e11663885c4829e4dd6085859a24ca61b4865f 100644 --- a/compiler/typecheck/TcRnMonad.lhs +++ b/compiler/typecheck/TcRnMonad.lhs @@ -75,7 +75,7 @@ initTc hsc_env hsc_src keep_rn_syntax mod do_this keep_var <- newIORef emptyNameSet ; used_rdr_var <- newIORef Set.empty ; th_var <- newIORef False ; - lie_var <- newIORef emptyBag ; + lie_var <- newIORef emptyWC ; dfun_n_var <- newIORef emptyOccSet ; type_env_var <- case hsc_type_env_var hsc_env of { Just (_mod, te_var) -> return te_var ; @@ -147,7 +147,7 @@ initTc hsc_env hsc_src keep_rn_syntax mod do_this -- Check for unsolved constraints lie <- readIORef lie_var ; - if isEmptyBag lie + if isEmptyWC lie then return () else pprPanic "initTc: unsolved constraints" (pprWantedsWithLocs lie) ; @@ -965,17 +965,32 @@ setConstraintVar lie_var = updLclEnv (\ env -> env { tcl_lie = lie_var }) emitConstraints :: WantedConstraints -> TcM () emitConstraints ct = do { lie_var <- getConstraintVar ; - updTcRef lie_var (`andWanteds` ct) } + updTcRef lie_var (`andWC` ct) } -emitConstraint :: WantedConstraint -> TcM () -emitConstraint ct +emitFlat :: WantedEvVar -> TcM () +emitFlat ct = do { lie_var <- getConstraintVar ; - updTcRef lie_var (`extendWanteds` ct) } + updTcRef lie_var (`addFlats` unitBag ct) } + +emitFlats :: Bag WantedEvVar -> TcM () +emitFlats ct + = do { lie_var <- getConstraintVar ; + updTcRef lie_var (`addFlats` ct) } + +emitImplication :: Implication -> TcM () +emitImplication ct + = do { lie_var <- getConstraintVar ; + updTcRef lie_var (`addImplics` unitBag ct) } + +emitImplications :: Bag Implication -> TcM () +emitImplications ct + = do { lie_var <- getConstraintVar ; + updTcRef lie_var (`addImplics` ct) } captureConstraints :: TcM a -> TcM (a, WantedConstraints) -- (captureConstraints m) runs m, and returns the type constraints it generates captureConstraints thing_inside - = do { lie_var <- newTcRef emptyWanteds ; + = do { lie_var <- newTcRef emptyWC ; res <- updLclEnv (\ env -> env { tcl_lie = lie_var }) thing_inside ; lie <- readTcRef lie_var ; diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 721f0782812ef604d358937db4051d848d8a90c8..fc781df6159b812546167e0d08cc97660ea9c41b 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -29,22 +29,28 @@ module TcRnTypes( -- Constraints Untouchables(..), inTouchableRange, isNoUntouchables, - WantedConstraints, emptyWanteds, andWanteds, extendWanteds, - WantedConstraint(..), WantedEvVar(..), wantedEvVarLoc, - wantedEvVarToVar, wantedEvVarPred, splitWanteds, - evVarsToWanteds, - Implication(..), + WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, + andWC, addFlats, addImplics, mkFlatWC, + + EvVarX(..), mkEvVarX, evVarOf, evVarX, evVarOfPred, + WantedEvVar, wantedToFlavored, + keepWanted, + + Implication(..), CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin, CtOrigin(..), EqOrigin(..), WantedLoc, GivenLoc, pushErrCtxt, - SkolemInfo(..), + SkolemInfo(..), + + CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived, + FlavoredEvVar, -- Pretty printing - pprEvVarTheta, pprWantedsWithLocs, pprWantedWithLoc, + pprEvVarTheta, pprWantedEvVar, pprWantedsWithLocs, pprEvVars, pprEvVarWithType, - pprArising, pprArisingAt, + pprArising, pprArisingAt, -- Misc other types TcId, TcIdSet, TcTyVarBind(..), TcTyVarBinds @@ -56,6 +62,8 @@ module TcRnTypes( import HsSyn import HscTypes import Type +import Class ( Class ) +import DataCon ( DataCon, dataConUserType ) import TcType import Annotations import InstEnv @@ -79,7 +87,6 @@ import Bag import Outputable import ListSetOps import FastString -import StaticFlags( opt_ErrorSpans ) import Data.Set (Set) \end{code} @@ -675,6 +682,58 @@ instance Outputable WhereFrom where %* * v%************************************************************************ +\begin{code} +data WantedConstraints + = WC { wc_flat :: Bag WantedEvVar -- Unsolved constraints, all wanted + , wc_impl :: Bag Implication + , wc_insol :: Bag FlavoredEvVar -- Insoluble constraints, can be + -- wanted, given, or derived + -- See Note [Insoluble constraints] + } + +emptyWC :: WantedConstraints +emptyWC = WC { wc_flat = emptyBag, wc_impl = emptyBag, wc_insol = emptyBag } + +mkFlatWC :: Bag WantedEvVar -> WantedConstraints +mkFlatWC wevs = WC { wc_flat = wevs, wc_impl = emptyBag, wc_insol = emptyBag } + +isEmptyWC :: WantedConstraints -> Bool +isEmptyWC (WC { wc_flat = f, wc_impl = i, wc_insol = n }) + = isEmptyBag f && isEmptyBag i && isEmptyBag n + +insolubleWC :: WantedConstraints -> Bool +-- True if there are any insoluble constraints in the wanted bag +insolubleWC wc = not (isEmptyBag (wc_insol wc)) + || anyBag ic_insol (wc_impl wc) + +andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints +andWC (WC { wc_flat = f1, wc_impl = i1, wc_insol = n1 }) + (WC { wc_flat = f2, wc_impl = i2, wc_insol = n2 }) + = WC { wc_flat = f1 `unionBags` f2 + , wc_impl = i1 `unionBags` i2 + , wc_insol = n1 `unionBags` n2 } + +addFlats :: WantedConstraints -> Bag WantedEvVar -> WantedConstraints +addFlats wc wevs = wc { wc_flat = wevs `unionBags` wc_flat wc } + +addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints +addImplics wc implic = wc { wc_impl = implic `unionBags` wc_impl wc } + +instance Outputable WantedConstraints where + ppr (WC {wc_flat = f, wc_impl = i, wc_insol = n}) + = ptext (sLit "WC") <+> braces (vcat + [ if isEmptyBag f then empty else + ptext (sLit "wc_flat =") <+> pprBag pprWantedEvVar f + , if isEmptyBag i then empty else + ptext (sLit "wc_impl =") <+> pprBag ppr i + , if isEmptyBag n then empty else + ptext (sLit "wc_insol =") <+> pprBag ppr n ]) + +pprBag :: (a -> SDoc) -> Bag a -> SDoc +pprBag pp b = foldrBag (($$) . pp) empty b +\end{code} + + \begin{code} data Untouchables = NoUntouchables | TouchableRange @@ -700,34 +759,26 @@ inTouchableRange (TouchableRange low high) tv where uniq = varUnique tv -type WantedConstraints = Bag WantedConstraint - -data WantedConstraint - = WcEvVar WantedEvVar - | WcImplic Implication - -- ToDo: add literals, methods - --- EvVar defined in module Var.lhs: +-- EvVar defined in module Var.lhs: -- Evidence variables include all *quantifiable* constraints -- dictionaries -- implicit parameters -- coercion variables +\end{code} -data WantedEvVar -- The sort of constraint over which one can lambda-abstract - = WantedEvVar - EvVar -- The variable itself; make a binding for it please - WantedLoc -- How the constraint arose in the first place - -- (used for error messages only) - -type WantedLoc = CtLoc CtOrigin -type GivenLoc = CtLoc SkolemInfo +%************************************************************************ +%* * + Implication constraints +%* * +%************************************************************************ +\begin{code} data Implication = Implic { ic_untch :: Untouchables, -- Untouchables: unification variables - -- free in the environment + -- free in the environment ic_env :: TcTypeEnv, -- The type environment - -- Used only when generating error messages + -- Used only when generating error messages -- Generally, ic_untch is a superset of tvsof(ic_env) -- However, we don't zonk ic_env when zonking the Implication -- Instead we do that when generating a skolem-escape error message @@ -735,37 +786,31 @@ data Implication ic_skols :: TcTyVarSet, -- Introduced skolems -- See Note [Skolems in an implication] - ic_scoped :: [TcTyVar], -- List of scoped variables to be unified - -- bijectively to a subset of ic_tyvars - -- Note [Scoped pattern variable] - ic_given :: [EvVar], -- Given evidence variables -- (order does not matter) + ic_loc :: GivenLoc, -- Binding location of the implication, + -- which is also the location of all the + -- given evidence variables - ic_wanted :: WantedConstraints, -- Wanted constraints - - ic_binds :: EvBindsVar, -- Points to the place to fill in the - -- abstraction and bindings - - ic_loc :: GivenLoc } - -evVarsToWanteds :: WantedLoc -> [EvVar] -> WantedConstraints -evVarsToWanteds loc evs = listToBag [WcEvVar (WantedEvVar ev loc) | ev <- evs] + ic_wanted :: WantedConstraints, -- The wanted + ic_insol :: Bool, -- True iff insolubleWC ic_wantted is true -wantedEvVarLoc :: WantedEvVar -> WantedLoc -wantedEvVarLoc (WantedEvVar _ loc) = loc - -wantedEvVarToVar :: WantedEvVar -> EvVar -wantedEvVarToVar (WantedEvVar ev _) = ev - -wantedEvVarPred :: WantedEvVar -> PredType -wantedEvVarPred (WantedEvVar ev _) = evVarPred ev + ic_binds :: EvBindsVar -- Points to the place to fill in the + -- abstraction and bindings + } -splitWanteds :: WantedConstraints -> (Bag WantedEvVar, Bag Implication) -splitWanteds wanted = partitionBagWith pick wanted - where - pick (WcEvVar v) = Left v - pick (WcImplic i) = Right i +instance Outputable Implication where + ppr (Implic { ic_untch = untch, ic_skols = skols, ic_given = given + , ic_wanted = wanted + , ic_binds = binds, ic_loc = loc }) + = ptext (sLit "Implic") <+> braces + (sep [ ptext (sLit "Untouchables = ") <+> ppr untch + , ptext (sLit "Skolems = ") <+> ppr skols + , ptext (sLit "Given = ") <+> pprEvVars given + , ptext (sLit "Wanted = ") <+> ppr wanted + , ptext (sLit "Binds = ") <+> ppr binds + , pprSkolInfo (ctLocOrigin loc) + , ppr (ctLocSpan loc) ]) \end{code} Note [Skolems in an implication] @@ -779,29 +824,73 @@ Instead, ic_skols is used only when considering floating a constraint outside the implication in TcSimplify.floatEqualities or TcSimplify.approximateImplications -Note [Scoped pattern variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - data T where K :: forall a,b. a -> b -> T - - ...(case x of K (p::c) (q::d) -> ...)... +Note [Insoluble constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Some of the errors that we get during canonicalization are best +reported when all constraints have been simplified as much as +possible. For instance, assume that during simplification the +following constraints arise: + + [Wanted] F alpha ~ uf1 + [Wanted] beta ~ uf1 beta + +When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail +we will simply see a message: + 'Can't construct the infinite type beta ~ uf1 beta' +and the user has no idea what the uf1 variable is. + +Instead our plan is that we will NOT fail immediately, but: + (1) Record the "frozen" error in the ic_insols field + (2) Isolate the offending constraint from the rest of the inerts + (3) Keep on simplifying/canonicalizing + +At the end, we will hopefully have substituted uf1 := F alpha, and we +will be able to report a more informative error: + 'Can't construct the infinite type beta ~ F alpha beta' -We create fresh MetaTvs for c,d, and later check that they are -bound bijectively to the skolems we created for a,b. So the -implication constraint looks like - ic_skols = {a',b'} -- Skolem tvs created from a,b - ic_scoped = {c',d'} -- Meta tvs created from c,d +%************************************************************************ +%* * + EvVarX, WantedEvVar, FlavoredEvVar +%* * +%************************************************************************ \begin{code} -emptyWanteds :: WantedConstraints -emptyWanteds = emptyBag +data EvVarX a = EvVarX EvVar a + -- An evidence variable with accompanying info + +type WantedEvVar = EvVarX WantedLoc -- The location where it arose +type FlavoredEvVar = EvVarX CtFlavor + +instance Outputable (EvVarX a) where + ppr (EvVarX ev _) = pprEvVarWithType ev + -- If you want to see the associated info, + -- use a more specific printing function + +mkEvVarX :: EvVar -> a -> EvVarX a +mkEvVarX = EvVarX -andWanteds :: WantedConstraints -> WantedConstraints -> WantedConstraints -andWanteds = unionBags +evVarOf :: EvVarX a -> EvVar +evVarOf (EvVarX ev _) = ev -extendWanteds :: WantedConstraints -> WantedConstraint -> WantedConstraints -extendWanteds = snocBag +evVarX :: EvVarX a -> a +evVarX (EvVarX _ a) = a + +evVarOfPred :: EvVarX a -> PredType +evVarOfPred wev = evVarPred (evVarOf wev) + +wantedToFlavored :: WantedEvVar -> FlavoredEvVar +wantedToFlavored (EvVarX v wl) = EvVarX v (Wanted wl) + +keepWanted :: Bag FlavoredEvVar -> Bag WantedEvVar +keepWanted flevs + = foldlBag keep_wanted emptyBag flevs + where + keep_wanted :: Bag WantedEvVar -> FlavoredEvVar -> Bag WantedEvVar + keep_wanted r (EvVarX ev (Wanted wloc)) = consBag (EvVarX ev wloc) r + keep_wanted r _ = r \end{code} - + + \begin{code} pprEvVars :: [EvVar] -> SDoc -- Print with their types pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars) @@ -812,55 +901,79 @@ pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars) pprEvVarWithType :: EvVar -> SDoc pprEvVarWithType v = ppr v <+> dcolon <+> pprPred (evVarPred v) -pprWantedsWithLocs :: Bag WantedConstraint -> SDoc -pprWantedsWithLocs = foldrBag (($$) . pprWantedWithLoc) empty - -pprWantedWithLoc :: WantedConstraint -> SDoc -pprWantedWithLoc (WcImplic i) = ppr i -pprWantedWithLoc (WcEvVar v) = pprWantedEvVarWithLoc v - -instance Outputable WantedConstraint where - ppr (WcEvVar v) = ppr v - ppr (WcImplic i) = ppr i - --- Adding -ferror-spans makes the output more voluminous -instance Outputable WantedEvVar where - ppr wev | opt_ErrorSpans = pprWantedEvVarWithLoc wev - | otherwise = pprWantedEvVar wev +pprWantedsWithLocs :: WantedConstraints -> SDoc +pprWantedsWithLocs wcs + = vcat [ pprBag pprWantedEvVarWithLoc (wc_flat wcs) + , pprBag ppr (wc_impl wcs) + , pprBag ppr (wc_insol wcs) ] pprWantedEvVarWithLoc, pprWantedEvVar :: WantedEvVar -> SDoc -pprWantedEvVarWithLoc (WantedEvVar v loc) = hang (pprEvVarWithType v) - 2 (pprArisingAt loc) -pprWantedEvVar (WantedEvVar v _) = pprEvVarWithType v +pprWantedEvVarWithLoc (EvVarX v loc) = hang (pprEvVarWithType v) + 2 (pprArisingAt loc) +pprWantedEvVar (EvVarX v _) = pprEvVarWithType v +\end{code} -instance Outputable Implication where - ppr (Implic { ic_untch = untch, ic_skols = skols, ic_given = given - , ic_wanted = wanted, ic_binds = binds, ic_loc = loc }) - = ptext (sLit "Implic") <+> braces - (sep [ ptext (sLit "Untouchables = ") <+> ppr untch - , ptext (sLit "Skolems = ") <+> ppr skols - , ptext (sLit "Given = ") <+> pprEvVars given - , ptext (sLit "Wanted = ") <+> ppr wanted - , ptext (sLit "Binds = ") <+> ppr binds - , pprSkolInfo (ctLocOrigin loc) - , ppr (ctLocSpan loc) ]) +%************************************************************************ +%* * + CtLoc +%* * +%************************************************************************ + +\begin{code} +data CtFlavor + = Given GivenLoc -- We have evidence for this constraint in TcEvBinds + | Derived WantedLoc + -- We have evidence for this constraint in TcEvBinds; + -- *however* this evidence can contain wanteds, so + -- it's valid only provisionally to the solution of + -- these wanteds + | Wanted WantedLoc -- We have no evidence bindings for this constraint. + +-- data DerivedOrig = DerSC | DerInst | DerSelf +-- Deriveds are either superclasses of other wanteds or deriveds, or partially +-- solved wanteds from instances, or 'self' dictionaries containing yet wanted +-- superclasses. + +instance Outputable CtFlavor where + ppr (Given _) = ptext (sLit "[Given]") + ppr (Wanted _) = ptext (sLit "[Wanted]") + ppr (Derived {}) = ptext (sLit "[Derived]") + +pprFlavorArising :: CtFlavor -> SDoc +pprFlavorArising (Derived wl ) = pprArisingAt wl +pprFlavorArising (Wanted wl) = pprArisingAt wl +pprFlavorArising (Given gl) = pprArisingAt gl + +isWanted :: CtFlavor -> Bool +isWanted (Wanted {}) = True +isWanted _ = False + +isGiven :: CtFlavor -> Bool +isGiven (Given {}) = True +isGiven _ = False + +isDerived :: CtFlavor -> Bool +isDerived (Derived {}) = True +isDerived _ = False \end{code} %************************************************************************ %* * - CtLoc, CtOrigin + CtLoc %* * %************************************************************************ -The 'CtLoc' and 'CtOrigin' types gives information about where a -*wanted constraint* came from. This is important for decent error -message reporting because dictionaries don't appear in the original -source code. Doubtless this type will evolve... +The 'CtLoc' gives information about where a constraint came from. +This is important for decent error message reporting because +dictionaries don't appear in the original source code. +type will evolve... \begin{code} -------------------------------------------- data CtLoc orig = CtLoc orig SrcSpan [ErrCtxt] +type WantedLoc = CtLoc CtOrigin -- Instantiation for wanted constraints +type GivenLoc = CtLoc SkolemInfo -- Instantiation for given constraints + ctLocSpan :: CtLoc o -> SrcSpan ctLocSpan (CtLoc _ s _) = s @@ -883,8 +996,96 @@ pprArising orig = text "arising from" <+> ppr orig pprArisingAt :: Outputable o => CtLoc o -> SDoc pprArisingAt (CtLoc o s _) = sep [ text "arising from" <+> ppr o , text "at" <+> ppr s] +\end{code} -------------------------------------------- +%************************************************************************ +%* * + SkolemInfo +%* * +%************************************************************************ + +\begin{code} +-- SkolemInfo gives the origin of *given* constraints +-- a) type variables are skolemised +-- b) an implication constraint is generated +data SkolemInfo + = SigSkol UserTypeCtxt -- A skolem that is created by instantiating + Type -- a programmer-supplied type signature + -- Location of the binding site is on the TyVar + + -- The rest are for non-scoped skolems + | ClsSkol Class -- Bound at a class decl + | InstSkol -- Bound at an instance decl + | DataSkol -- Bound at a data type declaration + | FamInstSkol -- Bound at a family instance decl + | PatSkol -- An existential type variable bound by a pattern for + DataCon -- a data constructor with an existential type. + (HsMatchContext Name) + -- e.g. data T = forall a. Eq a => MkT a + -- f (MkT x) = ... + -- The pattern MkT x will allocate an existential type + -- variable for 'a'. + + | ArrowSkol -- An arrow form (see TcArrows) + + | IPSkol [IPName Name] -- Binding site of an implicit parameter + + | RuleSkol RuleName -- The LHS of a RULE + + | InferSkol [(Name,TcType)] + -- We have inferred a type for these (mutually-recursivive) + -- polymorphic Ids, and are now checking that their RHS + -- constraints are satisfied. + + | RuntimeUnkSkol -- a type variable used to represent an unknown + -- runtime type (used in the GHCi debugger) + + | BracketSkol -- Template Haskell bracket + + | UnkSkol -- Unhelpful info (until I improve it) + +instance Outputable SkolemInfo where + ppr = pprSkolInfo + +pprSkolInfo :: SkolemInfo -> SDoc +-- Complete the sentence "is a rigid type variable bound by..." +pprSkolInfo (SigSkol (FunSigCtxt f) ty) + = hang (ptext (sLit "the type signature for")) + 2 (ppr f <+> dcolon <+> ppr ty) +pprSkolInfo (SigSkol cx ty) = hang (pprUserTypeCtxt cx <> colon) + 2 (ppr ty) +pprSkolInfo (IPSkol ips) = ptext (sLit "the implicit-parameter bindings for") + <+> pprWithCommas ppr ips +pprSkolInfo (ClsSkol cls) = ptext (sLit "the class declaration for") <+> quotes (ppr cls) +pprSkolInfo InstSkol = ptext (sLit "the instance declaration") +pprSkolInfo DataSkol = ptext (sLit "the data type declaration") +pprSkolInfo FamInstSkol = ptext (sLit "the family instance declaration") +pprSkolInfo BracketSkol = ptext (sLit "a Template Haskell bracket") +pprSkolInfo (RuleSkol name) = ptext (sLit "the RULE") <+> doubleQuotes (ftext name) +pprSkolInfo ArrowSkol = ptext (sLit "the arrow form") +pprSkolInfo (PatSkol dc mc) = sep [ ptext (sLit "a pattern with constructor") + , nest 2 $ ppr dc <+> dcolon + <+> ppr (dataConUserType dc) <> comma + , ptext (sLit "in") <+> pprMatchContext mc ] +pprSkolInfo (InferSkol ids) = sep [ ptext (sLit "the inferred type of") + , vcat [ ppr name <+> dcolon <+> ppr ty + | (name,ty) <- ids ]] + +-- UnkSkol +-- For type variables the others are dealt with by pprSkolTvBinding. +-- For Insts, these cases should not happen +pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol") +pprSkolInfo RuntimeUnkSkol = WARN( True, text "pprSkolInfo: RuntimeUnkSkol" ) ptext (sLit "RuntimeUnkSkol") +\end{code} + + +%************************************************************************ +%* * + CtOrigin +%* * +%************************************************************************ + +\begin{code} -- CtOrigin gives the origin of *wanted* constraints data CtOrigin = OccurrenceOf Name -- Occurrence of an overloaded identifier @@ -957,3 +1158,4 @@ pprO FunDepOrigin = ptext (sLit "a functional dependency") instance Outputable EqOrigin where ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2 \end{code} + diff --git a/compiler/typecheck/TcRules.lhs b/compiler/typecheck/TcRules.lhs index 81c018a1183a3e21ff7af8f2521004f0fbaa94b0..b2c1dac62088a88cd7eaa1d42857b4a95a883821 100644 --- a/compiler/typecheck/TcRules.lhs +++ b/compiler/typecheck/TcRules.lhs @@ -91,7 +91,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs) -- c.f. TcSimplify.simplifyInfer ; zonked_forall_tvs <- zonkTcTyVarsAndFV forall_tvs ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked - ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)) + ; qtvs <- zonkQuantifiedTyVars $ + varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs) ; return (HsRule name act (map (RuleBndr . noLoc) (qtvs ++ tpl_ids)) -- yuk @@ -111,7 +112,7 @@ tcRuleBndrs (RuleBndrSig var rn_ty : rule_bndrs) -- a::*, x :: a->a = do { let ctxt = FunSigCtxt (unLoc var) ; (tyvars, ty) <- tcHsPatSigType ctxt rn_ty - ; let skol_tvs = tcSkolSigTyVars (SigSkol ctxt) tyvars + ; let skol_tvs = tcSuperSkolTyVars tyvars id_ty = substTyWith tyvars (mkTyVarTys skol_tvs) ty id = mkLocalId (unLoc var) id_ty diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 36c46b3eff1967150941b88897e5b3290a10b9ad..36befd9cd6240697fcdafa48f70d842bd5dfca67 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -5,18 +5,18 @@ module TcSMonad ( -- Canonical constraints CanonicalCts, emptyCCan, andCCan, andCCans, singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, - isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, + isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, + isCFrozenErr, CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, - mkWantedConstraints, deCanonicaliseWanted, - makeGivens, makeSolvedByInst, + deCanonicalise, mkFrozenError, + makeSolvedByInst, - CtFlavor (..), isWanted, isGiven, isDerived, - isGivenCt, isWantedCt, pprFlavorArising, + isWanted, isGiven, isDerived, + isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising, isFlexiTcsTv, - DerivedOrig (..), canRewrite, canSolve, combineCtLoc, mkGivenFlavor, mkWantedFlavor, getWantedLoc, @@ -24,26 +24,21 @@ module TcSMonad ( TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, SimplContext(..), isInteractive, simplEqsOnly, performDefaulting, - - -- Creation of evidence variables - newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar, + -- Creation of evidence variables + newEvVar, newCoVar, newWantedCoVar, newGivenCoVar, + newDerivedId, newIPVar, newDictVar, newKindConstraint, -- Setting evidence variables - setWantedCoBind, setDerivedCoBind, + setWantedCoBind, setIPBind, setDictBind, setEvBind, setWantedTyBind, - newTcEvBindsTcS, - - getInstEnvs, getFamInstEnvs, -- Getting the environments + getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, - getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors, - getTcSErrorsBag, FrozenError (..), - addErrorTcS, - ErrorKind(..), + getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, newFlattenSkolemTy, -- Flatten skolems @@ -52,11 +47,8 @@ module TcSMonad ( instDFunConstraints, newFlexiTcSTy, - isGoodRecEv, - compatKind, - TcsUntouchables, isTouchableMetaTyVar, isTouchableMetaTyVar_InRange, @@ -73,7 +65,7 @@ module TcSMonad ( -- here - mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps + mkDerivedFunDepEqns -- Instantiation of 'Equations' from FunDeps ) where @@ -156,8 +148,8 @@ data CanonicalCt | CTyEqCan { -- tv ~ xi (recall xi means function free) -- Invariant: -- * tv not in tvs(xi) (occurs check) - -- * If constraint is given then typeKind xi `compatKind` typeKind tv - -- See Note [Spontaneous solving and kind compatibility] + -- * typeKind xi `compatKind` typeKind tv + -- See Note [Spontaneous solving and kind compatibility] -- * We prefer unification variables on the left *JUST* for efficiency cc_id :: EvVar, cc_flavor :: CtFlavor, @@ -167,8 +159,7 @@ data CanonicalCt | CFunEqCan { -- F xis ~ xi -- Invariant: * isSynFamilyTyCon cc_fun - -- * If constraint is given then - -- typeKind (F xis) `compatKind` typeKind xi + -- * typeKind (F xis) `compatKind` typeKind xi cc_id :: EvVar, cc_flavor :: CtFlavor, cc_fun :: TyCon, -- A type function @@ -178,38 +169,35 @@ data CanonicalCt } -compatKind :: Kind -> Kind -> Bool -compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 + | CFrozenErr { -- A "frozen error" does not interact with anything + -- See Note [Frozen Errors] + cc_id :: EvVar, + cc_flavor :: CtFlavor + } -makeGivens :: Bag WantedEvVar -> Bag (CtFlavor,EvVar) -makeGivens = mapBag (\(WantedEvVar ev wloc) -> (mkGivenFlavor (Wanted wloc) UnkSkol, ev)) --- ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol }) - -- The UnkSkol doesn't matter because these givens are - -- not contradictory (else we'd have rejected them already) +mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt +mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl } + +compatKind :: Kind -> Kind -> Bool +compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 makeSolvedByInst :: CanonicalCt -> CanonicalCt -- Record that a constraint is now solved --- Wanted -> Derived +-- Wanted -> Given -- Given, Derived -> no-op makeSolvedByInst ct - | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst } + | Wanted loc <- cc_flavor ct = ct { cc_flavor = mkGivenFlavor (Wanted loc) UnkSkol } | otherwise = ct -mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints -mkWantedConstraints flats implics - = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics - -deCanonicaliseWanted :: CanonicalCt -> WantedEvVar -deCanonicaliseWanted ct - = WARN( not (isWanted $ cc_flavor ct), ppr ct ) - let Wanted loc = cc_flavor ct - in WantedEvVar (cc_id ct) loc +deCanonicalise :: CanonicalCt -> FlavoredEvVar +deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct) tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys) tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys -tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty +tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty +tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev tyVarsOfCDict :: CanonicalCt -> TcTyVarSet tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys @@ -230,6 +218,8 @@ instance Outputable CanonicalCt where = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty) ppr (CFunEqCan co fl tc tys ty) = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty) + ppr (CFrozenErr co fl) + = ppr fl <+> pprEvVarWithType co \end{code} Note [Canonical implicit parameter constraints] @@ -279,6 +269,9 @@ isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc isCFunEqCan_Maybe _ = Nothing +isCFrozenErr :: CanonicalCt -> Bool +isCFrozenErr (CFrozenErr {}) = True +isCFrozenErr _ = False \end{code} %************************************************************************ @@ -289,42 +282,6 @@ isCFunEqCan_Maybe _ = Nothing %************************************************************************ \begin{code} -data CtFlavor - = Given GivenLoc -- We have evidence for this constraint in TcEvBinds - | Derived WantedLoc DerivedOrig - -- We have evidence for this constraint in TcEvBinds; - -- *however* this evidence can contain wanteds, so - -- it's valid only provisionally to the solution of - -- these wanteds - | Wanted WantedLoc -- We have no evidence bindings for this constraint. - -data DerivedOrig = DerSC | DerInst | DerSelf --- Deriveds are either superclasses of other wanteds or deriveds, or partially --- solved wanteds from instances, or 'self' dictionaries containing yet wanted --- superclasses. - -instance Outputable CtFlavor where - ppr (Given _) = ptext (sLit "[Given]") - ppr (Wanted _) = ptext (sLit "[Wanted]") - ppr (Derived {}) = ptext (sLit "[Derived]") - -isWanted :: CtFlavor -> Bool -isWanted (Wanted {}) = True -isWanted _ = False - -isGiven :: CtFlavor -> Bool -isGiven (Given {}) = True -isGiven _ = False - -isDerived :: CtFlavor -> Bool -isDerived (Derived {}) = True -isDerived _ = False - -pprFlavorArising :: CtFlavor -> SDoc -pprFlavorArising (Derived wl _) = pprArisingAt wl -pprFlavorArising (Wanted wl) = pprArisingAt wl -pprFlavorArising (Given gl) = pprArisingAt gl - getWantedLoc :: CanonicalCt -> WantedLoc getWantedLoc ct = ASSERT (isWanted (cc_flavor ct)) @@ -332,11 +289,12 @@ getWantedLoc ct Wanted wl -> wl _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty - -isWantedCt :: CanonicalCt -> Bool +isWantedCt :: CanonicalCt -> Bool isWantedCt ct = isWanted (cc_flavor ct) -isGivenCt :: CanonicalCt -> Bool -isGivenCt ct = isGiven (cc_flavor ct) +isGivenCt :: CanonicalCt -> Bool +isGivenCt ct = isGiven (cc_flavor ct) +isDerivedCt :: CanonicalCt -> Bool +isDerivedCt ct = isDerived (cc_flavor ct) canSolve :: CtFlavor -> CtFlavor -> Bool -- canSolve ctid1 ctid2 @@ -348,8 +306,8 @@ canSolve :: CtFlavor -> CtFlavor -> Bool -- active(IP nm ty) = nm ----------------------------------------- canSolve (Given {}) _ = True -canSolve (Derived {}) (Wanted {}) = True -canSolve (Derived {}) (Derived {}) = True +canSolve (Derived {}) (Wanted {}) = False -- DV: changing the semantics +canSolve (Derived {}) (Derived {}) = True -- DV: changing the semantics of derived canSolve (Wanted {}) (Wanted {}) = True canSolve _ _ = False @@ -362,22 +320,21 @@ combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc -- Precondition: At least one of them should be wanted combineCtLoc (Wanted loc) _ = loc combineCtLoc _ (Wanted loc) = loc -combineCtLoc (Derived loc _) _ = loc -combineCtLoc _ (Derived loc _) = loc +combineCtLoc (Derived loc ) _ = loc +combineCtLoc _ (Derived loc ) = loc combineCtLoc _ _ = panic "combineCtLoc: both given" mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor -mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) mkWantedFlavor :: CtFlavor -> CtFlavor -mkWantedFlavor (Wanted loc) = Wanted loc -mkWantedFlavor (Derived loc _) = Wanted loc -mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl) +mkWantedFlavor (Wanted loc) = Wanted loc +mkWantedFlavor (Derived loc) = Wanted loc +mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl) \end{code} - %************************************************************************ %* * %* The TcS solver monad * @@ -408,53 +365,16 @@ data TcSEnv tcs_context :: SimplContext, - tcs_errors :: IORef (Bag FrozenError), - -- Frozen errors that we defer reporting as much as possible, in order to - -- make them as informative as possible. See Note [Frozen Errors] - - tcs_untch :: TcsUntouchables + tcs_untch :: TcsUntouchables } type TcsUntouchables = (Untouchables,TcTyVarSet) -- Like the TcM Untouchables, -- but records extra TcsTv variables generated during simplification -- See Note [Extra TcsTv untouchables] in TcSimplify - -data FrozenError - = FrozenError ErrorKind CtFlavor TcType TcType - -data ErrorKind - = MisMatchError | OccCheckError | KindError - -instance Outputable FrozenError where - ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)" - \end{code} -Note [Frozen Errors] -~~~~~~~~~~~~~~~~~~~~ -Some of the errors that we get during canonicalization are best reported when all constraints -have been simplified as much as possible. For instance, assume that during simplification -the following constraints arise: - - [Wanted] F alpha ~ uf1 - [Wanted] beta ~ uf1 beta - -When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply -see a message: - 'Can't construct the infinite type beta ~ uf1 beta' -and the user has no idea what the uf1 variable is. - -Instead our plan is that we will NOT fail immediately, but: - (1) Record the "frozen" error in the tcs_errors field - (2) Isolate the offending constraint from the rest of the inerts - (3) Keep on simplifying/canonicalizing - -At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to -report a more informative error: - 'Can't construct the infinite type beta ~ F alpha beta' \begin{code} - data SimplContext = SimplInfer -- Inferring type of a let-bound thing | SimplRuleLhs -- Inferring type of a RULE lhs @@ -527,16 +447,14 @@ traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc runTcS :: SimplContext -> Untouchables -- Untouchables -> TcS a -- What to run - -> TcM (a, Bag FrozenError, Bag EvBind) + -> TcM (a, Bag EvBind) runTcS context untouch tcs = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds - ; err_ref <- TcM.newTcRef emptyBag ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var , tcs_context = context , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet - , tcs_errors = err_ref } -- Run the computation @@ -546,23 +464,20 @@ runTcS context untouch tcs ; mapM_ do_unification (varEnvElts ty_binds) -- And return - ; frozen_errors <- TcM.readTcRef err_ref ; ev_binds <- TcM.readTcRef evb_ref - ; return (res, frozen_errors, evBindMapBinds ev_binds) } + ; return (res, evBindMapBinds ev_binds) } where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a nestImplicTcS ref untch (TcS thing_inside) = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, - tcs_context = ctxt, - tcs_errors = err_ref } -> + tcs_context = ctxt } -> let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds , tcs_untch = untch - , tcs_context = ctxtUnderImplic ctxt - , tcs_errors = err_ref } + , tcs_context = ctxtUnderImplic ctxt } in thing_inside nest_env @@ -582,10 +497,8 @@ tryTcS :: TcS a -> TcS a tryTcS tcs = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var <- TcM.newTcEvBinds - ; err_ref <- TcM.newTcRef emptyBag ; let env1 = env { tcs_ev_binds = ev_binds_var - , tcs_ty_binds = ty_binds_var - , tcs_errors = err_ref } + , tcs_ty_binds = ty_binds_var } ; unTcS tcs env1 }) -- Update TcEvBinds @@ -606,14 +519,7 @@ getUntouchables = TcS (return . tcs_untch) getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) -getTcSErrors :: TcS (IORef (Bag FrozenError)) -getTcSErrors = TcS (return . tcs_errors) - -getTcSErrorsBag :: TcS (Bag FrozenError) -getTcSErrorsBag = do { err_ref <- getTcSErrors - ; wrapTcS $ TcM.readTcRef err_ref } - -getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) +getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) @@ -627,10 +533,6 @@ setWantedCoBind cv co = setEvBind cv (EvCoercion co) -- Was: wrapTcS $ TcM.writeWantedCoVar cv co -setDerivedCoBind :: CoVar -> Coercion -> TcS () -setDerivedCoBind cv co - = setEvBind cv (EvCoercion co) - setWantedTyBind :: TcTyVar -> TcType -> TcS () -- Add a type binding -- We never do this twice! @@ -655,12 +557,9 @@ setDictBind = setEvBind setEvBind :: EvVar -> EvTerm -> TcS () -- Internal setEvBind ev rhs - = do { tc_evbinds <- getTcEvBinds + = do { tc_evbinds <- getTcEvBinds ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) } -newTcEvBindsTcS :: TcS EvBindsVar -newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds) - warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS () warnTcS loc warn_if doc | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc @@ -672,25 +571,6 @@ getDefaultInfo ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt)) ; return (ctxt, tys, flags) } - - --- Recording errors in the TcS monad --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS () -addErrorTcS frknd fl ty1 ty2 - = do { err_ref <- getTcSErrors - ; wrapTcS $ do - { TcM.updTcRef err_ref $ \ errs -> - consBag (FrozenError frknd fl ty1 ty2) errs - - -- If there's an error in the *given* constraints, - -- stop right now, to avoid a cascade of errors - -- in the wanteds - ; when (isGiven fl) TcM.failM - - ; return () } } - -- Just get some environments needed for instance looking up and matching -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -760,7 +640,7 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty newFlattenSkolemTyVar :: TcType -> TcS TcTyVar newFlattenSkolemTyVar ty = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique - ; let name = mkSysTvName uniq (fsLit "f") + ; let name = TcM.mkTcTyVarName uniq (fsLit "f") ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } ; traceTcS "New Flatten Skolem Born" $ (ppr tv <+> text "[:= " <+> ppr ty <+> text "]") @@ -792,7 +672,7 @@ newFlexiTcSTy knd = wrapTcS $ do { uniq <- TcM.newUnique ; ref <- TcM.newMutVar Flexi - ; let name = mkSysTvName uniq (fsLit "uf") + ; let name = TcM.mkTcTyVarName uniq (fsLit "uf") ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) } isFlexiTcsTv :: TyVar -> Bool @@ -821,18 +701,18 @@ instFlexiTcSHelper tvname tvkind -- Superclasses and recursive dictionaries -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar -newGivOrDerEvVar pty evtrm - = do { ev <- wrapTcS $ TcM.newEvVar pty - ; setEvBind ev evtrm - ; return ev } +newEvVar :: TcPredType -> TcS EvVar +newEvVar pty = wrapTcS $ TcM.newEvVar pty -newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar +newDerivedId :: TcPredType -> TcS EvVar +newDerivedId pty = wrapTcS $ TcM.newEvVar pty + +newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar -- Note we create immutable variables for given or derived, since we -- must bind them to TcEvBinds (because their evidence may involve -- superclasses). However we should be able to override existing -- 'derived' evidence, even in TcEvBinds -newGivOrDerCoVar ty1 ty2 co +newGivenCoVar ty1 ty2 co = do { cv <- newCoVar ty1 ty2 ; setEvBind cv (EvCoercion co) ; return cv } @@ -840,8 +720,7 @@ newGivOrDerCoVar ty1 ty2 co newWantedCoVar :: TcType -> TcType -> TcS EvVar newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2 - -newCoVar :: TcType -> TcType -> TcS EvVar +newCoVar :: TcType -> TcType -> TcS EvVar newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 newIPVar :: IPName Name -> TcType -> TcS EvVar @@ -853,74 +732,6 @@ newDictVar cl tys = wrapTcS $ TcM.newDict cl tys \begin{code} -isGoodRecEv :: EvVar -> EvVar -> TcS Bool --- In a call (isGoodRecEv ev wv), we are considering solving wv --- using some term that involves ev, such as: --- by setting wv = ev --- or wv = EvCast x |> ev --- etc. --- But that would be Very Bad if the evidence for 'ev' mentions 'wv', --- in an "unguarded" way. So isGoodRecEv looks at the evidence ev --- recursively through the evidence binds, to see if uses of 'wv' are guarded. --- --- Guarded means: more instance calls than superclass selections. We --- compute this by chasing the evidence, adding +1 for every instance --- call (constructor) and -1 for every superclass selection (destructor). --- --- See Note [Superclasses and recursive dictionaries] in TcInteract -isGoodRecEv ev_var wv - = do { tc_evbinds <- getTcEvBindsBag - ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var - ; return $ case mb of - Nothing -> True - Just min_guardedness -> min_guardedness > 0 - } - - where chase_ev_var :: EvBindMap -- Evidence binds - -> EvVar -- Target variable whose gravity we want to return - -> Int -- Current gravity - -> [EvVar] -- Visited nodes - -> EvVar -- Current node - -> TcS (Maybe Int) - chase_ev_var assocs trg curr_grav visited orig - | trg == orig = return $ Just curr_grav - | orig `elem` visited = return $ Nothing - | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig - = chase_ev assocs trg curr_grav (orig:visited) ev_trm - - | otherwise = return Nothing - - chase_ev assocs trg curr_grav visited (EvId v) - = chase_ev_var assocs trg curr_grav visited v - chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) - = chase_ev_var assocs trg (curr_grav-1) visited d_id - chase_ev assocs trg curr_grav visited (EvCast v co) - = do { m1 <- chase_ev_var assocs trg curr_grav visited v - ; m2 <- chase_co assocs trg curr_grav visited co - ; return (comb_chase_res Nothing [m1,m2]) } - - chase_ev assocs trg curr_grav visited (EvCoercion co) - = chase_co assocs trg curr_grav visited co - chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_deps) - = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps - ; return (comb_chase_res Nothing chase_results) } - - chase_co assocs trg curr_grav visited co - = -- Look for all the coercion variables in the coercion - -- chase them, and combine the results. This is OK since the - -- coercion will not contain any superclass terms -- anything - -- that involves dictionaries will be bound in assocs. - let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) [] - (tyVarsOfType co) - in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars - ; return (comb_chase_res Nothing chase_results) } - - comb_chase_res f [] = f - comb_chase_res f (Nothing:rest) = comb_chase_res f rest - comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest - comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest - - -- Matching and looking up classes and family instances -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -977,28 +788,29 @@ matchFam tycon args -- Functional dependencies, instantiation of equations ------------------------------------------------------- -mkWantedFunDepEqns :: WantedLoc +mkDerivedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))] - -> TcS [WantedEvVar] -mkWantedFunDepEqns _ [] = return [] -mkWantedFunDepEqns loc eqns + -> TcS [FlavoredEvVar] -- All Derived +mkDerivedFunDepEqns _ [] = return [] +mkDerivedFunDepEqns loc eqns = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns)) - ; wevvars <- mapM to_work_item eqns - ; return $ concat wevvars } + ; evvars <- mapM to_work_item eqns + ; return $ concat evvars } where - to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar] + to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar] to_work_item ((qtvs, pairs), d1, d2) = do { let tvs = varSetElems qtvs ; tvs' <- mapM instFlexiTcS tvs ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc - ; mapM (do_one subst loc') pairs } + flav = Derived loc' + ; mapM (do_one subst flav) pairs } - do_one subst loc' (ty1, ty2) + do_one subst flav (ty1, ty2) = do { let sty1 = substTy subst ty1 sty2 = substTy subst ty2 - ; ev <- newWantedCoVar sty1 sty2 - ; return (WantedEvVar ev loc') } + ; ev <- newCoVar sty1 sty2 + ; return (mkEvVarX ev flav) } pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc pprEquationDoc (eqn, (p1, _), (p2, _)) diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 90048b789dbfc330b0d035e9a798996cfaa17c76..197d6820b091ebe933aa9446385addf73d700ecd 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -1,7 +1,7 @@ \begin{code} module TcSimplify( simplifyInfer, - simplifyDefault, simplifyDeriv, simplifyBracket, + simplifyDefault, simplifyDeriv, simplifyRule, simplifyTop, simplifyInteractive ) where @@ -15,6 +15,7 @@ import TcType import TcSMonad import TcInteract import Inst +import Unify( niFixTvSubst, niSubstTvSet ) import Var import VarSet import VarEnv @@ -28,8 +29,8 @@ import Util import PrelInfo import PrelNames import Class ( classKey ) -import BasicTypes ( RuleName ) -import Data.List ( partition ) +import BasicTypes ( RuleName, TopLevelFlag, isTopLevel ) +import Control.Monad ( when ) import Outputable import FastString \end{code} @@ -59,27 +60,11 @@ simplifyInteractive wanteds simplifyDefault :: ThetaType -- Wanted; has no type variables in it -> TcM () -- Succeeds iff the constraint is soluble simplifyDefault theta - = do { loc <- getCtLoc DefaultOrigin - ; wanted <- newWantedEvVars theta - ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted] - ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag + = do { wanted <- newFlatWanteds DefaultOrigin theta + ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted) ; return () } \end{code} -simplifyBracket is used when simplifying the constraints arising from -a Template Haskell bracket [| ... |]. We want to check that there aren't -any constraints that can't be satisfied (e.g. Show Foo, where Foo has no -Show instance), but we aren't otherwise interested in the results. -Nor do we care about ambiguous dictionaries etc. We will type check -this bracket again at its usage site. - -\begin{code} -simplifyBracket :: WantedConstraints -> TcM () -simplifyBracket wanteds - = do { zonked_wanteds <- mapBagM zonkWanted wanteds - ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds - ; return () } -\end{code} ********************************************************************************* @@ -95,29 +80,35 @@ simplifyDeriv :: CtOrigin -> TcM ThetaType -- Needed -- Given instance (wanted) => C inst_ty -- Simplify 'wanted' as much as possibles +-- Fail if not possible simplifyDeriv orig tvs theta - = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize + = do { tvs_skols <- tcInstSuperSkolTyVars tvs -- Skolemize -- One reason is that the constraint solving machinery -- expects *TcTyVars* not TyVars. Another is that -- when looking up instances we don't want overlap -- of type variables ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols - - ; loc <- getCtLoc orig - ; wanted <- newWantedEvVars (substTheta skol_subst theta) - ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted] + subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs + + ; wanted <- newFlatWanteds orig (substTheta skol_subst theta) + + ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted) + ; (residual_wanted, _binds) + <- runTcS SimplInfer NoUntouchables $ + solveWanteds emptyInert (mkFlatWC wanted) - ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted) - ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag + ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted) + -- See Note [Exotic derived instance contexts] + get_good :: WantedEvVar -> Either PredType WantedEvVar + get_good wev | validDerivPred p = Left p + | otherwise = Right wev + where p = evVarOfPred wev - ; let (good, bad) = partition validDerivPred $ - foldrBag ((:) . wantedEvVarPred) [] unsolved - -- See Note [Exotic derived instance contexts] - subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs + ; reportUnsolved (residual_wanted { wc_flat = bad }) - ; reportUnsolvedDeriv bad loc - ; return $ substTheta subst_skol good } + ; let min_theta = mkMinimalBySCs (bagToList good) + ; return (substTheta subst_skol min_theta) } \end{code} Note [Exotic derived instance contexts] @@ -178,193 +169,225 @@ Allow constraints which consist only of type variables, with no repeats. *********************************************************************************** \begin{code} -simplifyInfer :: Bool -- Apply monomorphism restriction - -> TcTyVarSet -- These type variables are free in the - -- types to be generalised +simplifyInfer :: TopLevelFlag + -> Bool -- Apply monomorphism restriction + -> [(Name, TcTauType)] -- Variables to be generalised, + -- and their tau-types -> WantedConstraints -> TcM ([TcTyVar], -- Quantify over these type variables [EvVar], -- ... and these constraints TcEvBinds) -- ... binding these evidence variables -simplifyInfer apply_mr tau_tvs wanted - | isEmptyBag wanted -- Trivial case is quite common - = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs - ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked - ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs)) +simplifyInfer top_lvl apply_mr name_taus wanteds + | isEmptyWC wanteds + = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked + ; zonked_taus <- zonkTcTypes (map snd name_taus) + ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs + ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify) ; return (qtvs, [], emptyTcEvBinds) } | otherwise - = do { zonked_wanted <- mapBagM zonkWanted wanted + = do { zonked_wanteds <- zonkWC wanteds + ; zonked_taus <- zonkTcTypes (map snd name_taus) + ; gbl_tvs <- tcGetGlobalTyVars + ; traceTc "simplifyInfer {" $ vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr - , ptext (sLit "wanted =") <+> ppr zonked_wanted - , ptext (sLit "tau_tvs =") <+> ppr tau_tvs + , ptext (sLit "zonked_taus =") <+> ppr zonked_taus + , ptext (sLit "wanted =") <+> ppr zonked_wanteds ] - -- Make a guess at the quantified type variables + -- Step 1 + -- Make a guess at the quantified type variables -- Then split the constraints on the baisis of those tyvars -- to avoid unnecessarily simplifying a class constraint -- See Note [Avoid unecessary constraint simplification] - ; gbl_tvs <- tcGetGlobalTyVars - ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs - ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $ + ; let zonked_tau_tvs = get_tau_tvs zonked_taus + proto_qtvs = growWanteds gbl_tvs zonked_wanteds $ zonked_tau_tvs `minusVarSet` gbl_tvs - (perhaps_bound, surely_free) - = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted - - ; emitConstraints surely_free + (perhaps_bound, surely_free) + = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds) + + ; traceTc "simplifyInfer proto" $ vcat + [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs + , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs + , ptext (sLit "surely_fref =") <+> ppr surely_free + ] + + ; emitFlats surely_free ; traceTc "sinf" $ vcat [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound , ptext (sLit "surely_free =") <+> ppr surely_free ] - -- Now simplify the possibly-bound constraints - ; (simplified_perhaps_bound, tc_binds) - <- simplifyAsMuchAsPossible SimplInfer perhaps_bound - - -- Sigh: must re-zonk because because simplifyAsMuchAsPossible - -- may have done some unification - ; gbl_tvs <- tcGetGlobalTyVars - ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs - ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound + -- Step 2 + -- Now simplify the possibly-bound constraints + ; (simpl_results, tc_binds0) + <- runTcS SimplInfer NoUntouchables $ + simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound }) + + ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint + (do { reportUnsolved simpl_results; failM }) + + -- Step 3 + -- Split again simplified_perhaps_bound, because some unifications + -- may have happened, and emit the free constraints. + ; gbl_tvs <- tcGetGlobalTyVars + ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs + ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results) ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs mr_qtvs = init_tvs `minusVarSet` constrained_tvs - constrained_tvs = tyVarsOfWantedEvVars zonked_simples + constrained_tvs = tyVarsOfEvVarXs zonked_simples qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs (final_qtvs, (bound, free)) | apply_mr = (mr_qtvs, (emptyBag, zonked_simples)) | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples) + ; emitFlats free + + ; if isEmptyVarSet final_qtvs && isEmptyBag bound + then ASSERT( isEmptyBag (wc_insol simpl_results) ) + do { traceTc "} simplifyInfer/no quantification" empty + ; emitImplications (wc_impl simpl_results) + ; return ([], [], EvBinds tc_binds0) } + else do + + -- Step 4, zonk quantified variables + { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound + ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty) + | (name, ty) <- name_taus ] + -- Don't add the quantified variables here, because + -- they are also bound in ic_skols and we want them to be + -- tidied uniformly + skol_info = InferSkol poly_ids + + ; gloc <- getCtLoc skol_info + ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) + + -- Step 5 + -- Minimize `bound' and emit an implication + ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds + ; ev_binds_var <- newTcEvBinds + ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0 + ; lcl_env <- getLclTypeEnv + ; let implic = Implic { ic_untch = NoUntouchables + , ic_env = lcl_env + , ic_skols = mkVarSet qtvs_to_return + , ic_given = minimal_bound_ev_vars + , ic_wanted = simpl_results { wc_flat = bound } + , ic_insol = False + , ic_binds = ev_binds_var + , ic_loc = gloc } + ; emitImplication implic + ; traceTc "} simplifyInfer/produced residual implication for quantification" $ + vcat [ ptext (sLit "implic =") <+> ppr implic + -- ic_skols, ic_given give rest of result + , ptext (sLit "qtvs =") <+> ppr final_qtvs + , ptext (sLit "spb =") <+> ppr zonked_simples + , ptext (sLit "bound =") <+> ppr bound ] + + + + ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } } + where + get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes + | otherwise = exactTyVarsOfTypes + -- See Note [Silly type synonym] in TcType +\end{code} - ; traceTc "end simplifyInfer }" $ - vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr - , text "wanted = " <+> ppr zonked_wanted - , text "qtvs = " <+> ppr final_qtvs - , text "free = " <+> ppr free - , text "bound = " <+> ppr bound ] - - -- Turn the quantified meta-type variables into real type variables - ; emitConstraints (mapBag WcEvVar free) - ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) - ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound - ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) } - ------------------------- -simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints - -> TcM (Bag WantedEvVar, Bag EvBind) --- We use this function when inferring the type of a function --- The wanted constraints are already zonked -simplifyAsMuchAsPossible ctxt wanteds - = do { let untch = NoUntouchables - -- We allow ourselves to unify environment - -- variables; hence *no untouchables* - ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds) - <- runTcS ctxt untch $ - simplifyApproxLoop 0 wanteds +Note [Minimize by Superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -- Report any errors - ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors +When we quantify over a constraint, in simplifyInfer we need to +quantify over a constraint that is minimal in some sense: For +instance, if the final wanted constraint is (Eq alpha, Ord alpha), +we'd like to quantify over Ord alpha, because we can just get Eq alpha +from superclass selection from Ord alpha. This minimization is what +mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint +to check the original wanted. - ; return (unsolved_flats, ev_binds) } +\begin{code} +simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints +simplifyWithApprox wanted + = do { traceTcS "simplifyApproxLoop" (ppr wanted) + ; results <- solveWanteds emptyInert wanted + + ; let (residual_implics, floats) = approximateImplications (wc_impl results) + + -- If no new work was produced then we are done with simplifyApproxLoop + ; if insolubleWC results || isEmptyBag floats + then return results + + else solveWanteds emptyInert + (WC { wc_flat = floats `unionBags` wc_flat results + , wc_impl = residual_implics + , wc_insol = emptyBag }) } + +approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar) +-- Extracts any nested constraints that don't mention the skolems +approximateImplications impls + = do_bag (float_implic emptyVarSet) impls where - simplifyApproxLoop :: Int -> WantedConstraints - -> TcS (Bag WantedEvVar, Bag Implication) - simplifyApproxLoop n wanteds - | n > 10 - = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations") - | otherwise - = do { traceTcS "simplifyApproxLoop" (vcat - [ ptext (sLit "Wanted = ") <+> ppr wanteds ]) - ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds - - ; let (extra_flats, thiner_unsolved_implics) - = approximateImplications unsolved_implics - unsolved - = Bag.mapBag WcEvVar unsolved_flats `unionBags` - Bag.mapBag WcImplic thiner_unsolved_implics - - ; -- If no new work was produced then we are done with simplifyApproxLoop - if isEmptyBag extra_flats - then do { traceTcS "simplifyApproxLoopRes" (vcat - [ ptext (sLit "Wanted = ") <+> ppr wanteds - , ptext (sLit "Result = ") <+> ppr unsolved_flats ]) - ; return (unsolved_flats, unsolved_implics) } - - else -- Produced new flat work wanteds, go round the loop - simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved) - } - -approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication) --- (wc1, impls2) <- approximateImplications impls --- splits 'impls' into two parts --- wc1: a bag of constraints that do not mention any skolems --- impls2: a bag of *thiner* implication constraints -approximateImplications impls - = splitBag (do_implic emptyVarSet) impls - where - ------------------ - do_wanted :: TcTyVarSet -> WantedConstraint - -> (WantedConstraints, WantedConstraints) - do_wanted skols (WcImplic impl) - = let (fl_w, mb_impl) = do_implic skols impl - in (fl_w, mapBag WcImplic mb_impl) - do_wanted skols wc@(WcEvVar wev) - | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag) - | otherwise = (emptyBag, unitBag wc) - - ------------------ - do_implic :: TcTyVarSet -> Implication - -> (WantedConstraints, Bag Implication) - do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted }) - = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag - else unitBag impl{ ic_wanted = rest_wanted } ) - where - (floatable_wanted, rest_wanted) - = splitBag (do_wanted (skols `unionVarSet` skols')) wanted - - ------------------ - splitBag :: (a -> (WantedConstraints, Bag a)) - -> Bag a -> (WantedConstraints, Bag a) - splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag - where - do_one x (b1,b2) - = (wcs `unionBags` b1, imps `unionBags` b2) - where - (wcs, imps) = f x + do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c) + do_bag f = foldrBag (plus . f) (emptyBag, emptyBag) + plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c) + plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2) + + float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar) + float_implic skols imp + = (unitBag (imp { ic_wanted = wanted' }), floats) + where + (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp) + + float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic }) + = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2) + where + (flat', floats1) = do_bag (float_flat skols) flat + (implic', floats2) = do_bag (float_implic skols) implic + + float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar) + float_flat skols wev + | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev) + | otherwise = (unitBag wev, emptyBag) \end{code} \begin{code} -growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet -growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet -growWanteds gbl_tvs ws tvs - | isEmptyBag ws = tvs - | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs -growWantedEVs gbl_tvs ws tvs - | isEmptyBag ws = tvs - | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs - -growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet -growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet -growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet -- (growX gbls wanted tvs) grows a seed 'tvs' against the -- X-constraint 'wanted', nuking the 'gbls' at each stage +-- It's conservative in that if the seed could *possibly* +-- grow to include a type variable, then it does -growEvVar gbl_tvs ev tvs - = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs) - where - ev_tvs = growPredTyVars (evVarPred ev) tvs +growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet +growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc) + +growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet +growWantedEVs gbl_tvs ws tvs + | isEmptyBag ws = tvs + | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs -growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs +-------- Helper functions, do not do fixpoint ------------------------ +growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet +growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) . + growPreds gbl_tvs evVarOfPred (wc_flat wc) . + growPreds gbl_tvs evVarOfPred (wc_insol wc) -growWanted gbl_tvs (WcEvVar wev) tvs - = growWantedEV gbl_tvs wev tvs -growWanted gbl_tvs (WcImplic implic) tvs - = foldrBag (growWanted inner_gbl_tvs) - (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic)) - -- Must grow over inner givens too - (ic_wanted implic) +growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet +growImplics gbl_tvs implics tvs + = foldrBag grow_implic tvs implics + where + grow_implic implic tvs + = grow tvs `minusVarSet` ic_skols implic + where + grow = growWC gbl_tvs (ic_wanted implic) . + growPreds gbl_tvs evVarPred (listToBag (ic_given implic)) + -- We must grow from givens too; see test IPRun + +growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet +growPreds gbl_tvs get_pred items tvs + = foldrBag extend tvs items where - inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic + extend item tvs = tvs `unionVarSet` + (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs) -------------------- quantifyMe :: TyVarSet -- Quantifying over these @@ -374,18 +397,7 @@ quantifyMe qtvs wev | isIPPred pred = True -- Note [Inheriting implicit parameters] | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs where - pred = wantedEvVarPred wev - -quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool --- False => we can *definitely* float the WantedConstraint out -quantifyMeWC qtvs (WcImplic implic) - = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs) - || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic) - where - inner_qtvs = qtvs `minusVarSet` ic_skols implic - -quantifyMeWC qtvs (WcEvVar wev) - = quantifyMe qtvs wev + pred = evVarOfPred wev \end{code} Note [Avoid unecessary constraint simplification] @@ -503,14 +515,39 @@ simplifyRule :: RuleName TcEvBinds) -- Evidence for RHS -- See Note [Simplifying RULE lhs constraints] simplifyRule name tv_bndrs lhs_wanted rhs_wanted - = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted - ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs + = do { loc <- getCtLoc (RuleSkol name) + ; zonked_lhs <- zonkWC lhs_wanted + ; let untch = NoUntouchables + -- We allow ourselves to unify environment + -- variables; hence *no untouchables* + + ; (lhs_results, lhs_binds) + <- runTcS SimplRuleLhs untch $ + solveWanteds emptyInert lhs_wanted + + ; traceTc "simplifyRule" $ + vcat [ text "zonked_lhs" <+> ppr zonked_lhs + , text "lhs_results" <+> ppr lhs_results + , text "lhs_binds" <+> ppr lhs_binds + , text "rhs_wanted" <+> ppr rhs_wanted ] + -- Don't quantify over equalities (judgement call here) - ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual - lhs_dicts = map wantedEvVarToVar (bagToList dicts) - -- Dicts and implicit parameters - ; reportUnsolvedWantedEvVars eqs + ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred) + (wc_flat lhs_results) + lhs_dicts = map evVarOf (bagToList dicts) + -- Dicts and implicit parameters + + -- Fail if we have not got down to unsolved flats + ; ev_binds_var <- newTcEvBinds + ; emitImplication $ Implic { ic_untch = untch + , ic_env = emptyNameEnv + , ic_skols = mkVarSet tv_bndrs + , ic_given = lhs_dicts + , ic_wanted = lhs_results { wc_flat = eqs } + , ic_insol = insolubleWC lhs_results + , ic_binds = ev_binds_var + , ic_loc = loc } -- Notice that we simplify the RHS with only the explicitly -- introduced skolems, allowing the RHS to constrain any @@ -527,16 +564,18 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted -- Hence the rather painful ad-hoc treatement here ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds - ; loc <- getCtLoc (RuleSkol name) - ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $ - Implic { ic_untch = NoUntouchables - , ic_env = emptyNameEnv - , ic_skols = mkVarSet tv_bndrs - , ic_scoped = panic "emitImplication" - , ic_given = lhs_dicts - , ic_wanted = rhs_wanted - , ic_binds = rhs_binds_var - , ic_loc = loc } + ; rhs_binds1 <- simplifyCheck SimplCheck $ + WC { wc_flat = emptyBag + , wc_insol = emptyBag + , wc_impl = unitBag $ + Implic { ic_untch = NoUntouchables + , ic_env = emptyNameEnv + , ic_skols = mkVarSet tv_bndrs + , ic_given = lhs_dicts + , ic_wanted = rhs_wanted + , ic_insol = insolubleWC rhs_wanted + , ic_binds = rhs_binds_var + , ic_loc = loc } } ; rhs_binds2 <- readTcRef evb_ref ; return ( lhs_dicts @@ -568,119 +607,128 @@ simplifyCheck :: SimplContext -- -- Fails if can't solve something in the input wanteds simplifyCheck ctxt wanteds - = do { wanteds <- mapBagM zonkWanted wanteds + = do { wanteds <- zonkWC wanteds ; traceTc "simplifyCheck {" (vcat [ ptext (sLit "wanted =") <+> ppr wanteds ]) - ; (unsolved, frozen_errors, ev_binds) - <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds + ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $ + solveWanteds emptyInert wanteds ; traceTc "simplifyCheck }" $ - ptext (sLit "unsolved =") <+> ppr unsolved + ptext (sLit "unsolved =") <+> ppr unsolved - ; reportUnsolved unsolved frozen_errors + ; reportUnsolved unsolved ; return ev_binds } ---------------- -solveWanteds :: InertSet -- Given - -> WantedConstraints -- Wanted - -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why - -- they are WantedConstraints and not CanonicalCts - Bag Implication) -- Unsolved implications --- solveWanteds iterates when it is able to float equalities --- out of one or more of the implications -solveWanteds inert wanteds - = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds - ; traceTcS "solveWanteds {" $ - vcat [ text "wanteds =" <+> ppr wanteds - , text "inert =" <+> ppr inert ] - ; (unsolved_flats, unsolved_implics) - <- simpl_loop 1 inert flat_wanteds implic_wanteds +solveWanteds :: InertSet -- Given + -> WantedConstraints + -> TcS WantedConstraints +solveWanteds inert wanted + = do { (unsolved_flats, unsolved_implics, insols) + <- solve_wanteds inert wanted + ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived + , wc_impl = unsolved_implics + , wc_insol = insols }) } + +solve_wanteds :: InertSet -- Given + -> WantedConstraints + -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar) +-- solve_wanteds iterates when it is able to float equalities +-- out of one or more of the implications +solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) + = do { traceTcS "solveWanteds {" (ppr wanted) + + -- Try the flat bit + ; let all_flats = flats `unionBags` keepWanted insols + ; inert1 <- solveInteractWanted inert (bagToList all_flats) + + ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics + ; bb <- getTcEvBindsBag ; tb <- getTcSTyBindsMap ; traceTcS "solveWanteds }" $ vcat [ text "unsolved_flats =" <+> ppr unsolved_flats - , text "unsolved_implics =" <+> ppr unsolved_implics + , text "unsolved_implics =" <+> ppr unsolved_implics , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb)) ] - ; solveCTyFunEqs unsolved_flats unsolved_implics + ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats -- See Note [Solving Family Equations] - } + -- NB: remaining_flats has already had subst applied + + ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats + + ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats + , mapBag (substImplication subst) unsolved_implics + , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) } + where - simpl_loop :: Int - -> InertSet - -> Bag WantedEvVar + simpl_loop :: Int + -> InertSet -> Bag Implication - -> TcS (CanonicalCts, Bag Implication) - simpl_loop n inert work_items implics + -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived + simpl_loop n inert implics | n>10 = trace "solveWanteds: loop" $ -- Always bleat do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively - - -- We don't want to call the canonicalizer on those wanted ev vars - -- so try one last time to solveInteract them - ; inert1 <- solveInteract inert $ - mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items - ; let (_, unsolved_cans) = extractUnsolved inert1 + ; let (_, unsolved_cans) = extractUnsolved inert ; return (unsolved_cans, implics) } | otherwise = do { traceTcS "solveWanteds: simpl_loop start {" $ vcat [ text "n =" <+> ppr n - , text "work_items =" <+> ppr work_items , text "implics =" <+> ppr implics - , text "inert =" <+> ppr inert ] - ; inert1 <- solveInteract inert $ - mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items - ; let (inert2, unsolved_cans) = extractUnsolved inert1 - unsolved_wevvars - = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans - - -- NB: Importantly, inerts2 may contain *more* givens than inert - -- because of having solved equalities from can_ws - ; traceTcS "solveWanteds: done flats" $ - vcat [ text "inerts =" <+> ppr inert2 - , text "unsolved =" <+> ppr unsolved_cans ] + , text "inert =" <+> ppr inert ] + + ; let (just_given_inert, unsolved_cans) = extractUnsolved inert + -- unsolved_ccans contains either Wanted or Derived! -- Go inside each implication ; (implic_eqs, unsolved_implics) - <- solveNestedImplications inert2 unsolved_wevvars implics + <- solveNestedImplications just_given_inert implics -- Apply defaulting rules if and only if there -- no floated equalities. If there are, they may -- solve the remaining wanteds, so don't do defaulting. - ; final_eqs <- if not (isEmptyBag implic_eqs) - then return implic_eqs - else applyDefaultingRules inert2 unsolved_cans + ; improve_eqs <- if not (isEmptyBag implic_eqs) + then return implic_eqs + else applyDefaultingRules just_given_inert unsolved_cans ; traceTcS "solveWanteds: simpl_loop end }" $ - vcat [ text "final_eqs =" <+> ppr final_eqs - , text "unsolved_flats =" <+> ppr unsolved_cans + vcat [ text "improve_eqs =" <+> ppr improve_eqs + , text "unsolved_flats =" <+> ppr unsolved_cans , text "unsolved_implics =" <+> ppr unsolved_implics ] - ; if isEmptyBag final_eqs then + ; (improve_eqs_already_in_inert, inert_with_improvement) + <- solveInteract inert improve_eqs + + ; if improve_eqs_already_in_inert then return (unsolved_cans, unsolved_implics) else - simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars - (final_eqs `unionBags` unsolved_wevvars) unsolved_implics - -- Important: reiterate with inert2, not plainly inert - -- because inert2 may contain more givens, as the result of solving - -- some wanteds in the incoming can_ws + simpl_loop (n+1) inert_with_improvement + -- Contain unsolved_cans and the improve_eqs + unsolved_implics } -solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication - -> TcS (Bag WantedEvVar, Bag Implication) -solveNestedImplications inerts unsolved implics +solveNestedImplications :: InertSet -> Bag Implication + -> TcS (Bag FlavoredEvVar, Bag Implication) +solveNestedImplications inerts implics | isEmptyBag implics = return (emptyBag, emptyBag) | otherwise = do { -- See Note [Preparing inert set for implications] traceTcS "solveWanteds: preparing inerts for implications {" empty - ; inert_for_implics <- solveInteract inerts (makeGivens unsolved) + ; let inert_for_implics = inerts + -- DV: Used to be: + -- inert_for_implics <- solveInteract inerts (makeGivens unsolved). + -- But now the top-level simplifyInfer effectively converts the + -- quantifiable wanteds to givens, and hence we don't need to add + -- those unsolved as givens here; they will already be in the inert set. + ; traceTcS "}" empty ; traceTcS "solveWanteds: doing nested implications {" $ @@ -690,6 +738,7 @@ solveNestedImplications inerts unsolved implics ; let tcs_untouchables = filterVarSet isFlexiTcsTv $ tyVarsOfInert inert_for_implics -- See Note [Extra TcsTv untouchables] + ; (implic_eqs, unsolved_implics) <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics @@ -699,11 +748,11 @@ solveNestedImplications inerts unsolved implics ; return (implic_eqs, unsolved_implics) } -solveImplication :: TcTyVarSet -- Untouchable TcS unification variables - -> InertSet -- Given - -> Implication -- Wanted - -> TcS (Bag WantedEvVar, -- Unsolved unification var = type - Bag Implication) -- Unsolved rest (always empty or singleton) +solveImplication :: TcTyVarSet -- Untouchable TcS unification variables + -> InertSet -- Given + -> Implication -- Wanted + -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type + Bag Implication) -- Unsolved rest (always empty or singleton) -- Returns: -- 1. A bag of floatable wanted constraints, not mentioning any skolems, -- that are of the form unification var = type @@ -726,41 +775,44 @@ solveImplication tcs_untouchables inert do { traceTcS "solveImplication {" (ppr imp) -- Solve flat givens --- ; can_givens <- canGivens loc givens --- ; let given_fl = Given loc - ; given_inert <- solveInteract inert $ - mapBag (\c -> (Given loc,c)) (listToBag givens) + ; given_inert <- solveInteractGiven inert loc givens -- Simplify the wanteds - ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds + ; (unsolved_flats, unsolved_implics, insols) + <- solve_wanteds given_inert wanteds + + ; let (res_flat_free, res_flat_bound) + = floatEqualities skols givens unsolved_flats + final_flat = keepWanted res_flat_bound - ; let (res_flat_free, res_flat_bound) - = floatEqualities skols givens unsolved_flats - unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags` - Bag.mapBag WcImplic unsolved_implics + ; let res_wanted = WC { wc_flat = final_flat + , wc_impl = unsolved_implics + , wc_insol = insols } + res_implic = unitImplication $ + imp { ic_wanted = res_wanted + , ic_insol = insolubleWC res_wanted } ; traceTcS "solveImplication end }" $ vcat [ text "res_flat_free =" <+> ppr res_flat_free - , text "res_flat_bound =" <+> ppr res_flat_bound - , text "unsolved_implics =" <+> ppr unsolved_implics ] + , text "res_implic =" <+> ppr res_implic ] - ; let res_bag | isEmptyBag unsolved = emptyBag - | otherwise = unitBag (imp { ic_wanted = unsolved }) + ; return (res_flat_free, res_implic) } - ; return (res_flat_free, res_bag) } -floatEqualities :: TcTyVarSet -> [EvVar] - -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar) - -- The CanonicalCts will be floated out to be used later, whereas - -- the remaining WantedEvVars will remain inside the implication. -floatEqualities skols can_given wanteds - | hasEqualities can_given = (emptyBag, wanteds) +floatEqualities :: TcTyVarSet -> [EvVar] + -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar) +-- Post: The returned FlavoredEvVar's are only Wanted or Derived +-- and come from the input wanted ev vars or deriveds +floatEqualities skols can_given wantders + | hasEqualities can_given = (emptyBag, wantders) -- Note [Float Equalities out of Implications] - | otherwise = partitionBag is_floatable wanteds - where is_floatable :: WantedEvVar -> Bool - is_floatable (WantedEvVar cv _) + | otherwise = partitionBag is_floatable wantders + + + where is_floatable :: FlavoredEvVar -> Bool + is_floatable (EvVarX cv _fl) | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv) - is_floatable _wv = False + is_floatable _flev = False tvs_under_fsks :: Type -> TyVarSet -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym @@ -784,10 +836,6 @@ floatEqualities skols can_given wanteds predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys) predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2 - - - - \end{code} Note [Float Equalities out of Implications] @@ -847,86 +895,70 @@ NB: A consequence is that every simplifier-generated TcsTv variable that gets fl \begin{code} -solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication) +solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts) -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible -- See Note [Solving Family Equations] -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications -- where the newly generated equalities (alpha := F xi) have been substituted through. -solveCTyFunEqs cts implics +solveCTyFunEqs cts = do { untch <- getUntouchables - ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts + ; let (unsolved_can_cts, (ni_subst, cv_binds)) + = getSolvableCTyFunEqs untch cts ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:" - , ppr funeq_bnds + , ppr ni_subst, ppr cv_binds ]) - ; mapM_ solve_one funeq_bnds - - -- Apply the substitution through to eliminate the flatten - -- unification variables we substituted both in the unsolved flats and implics - ; let final_unsolved - = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts - final_implics - = Bag.mapBag (subst_impl funeq_bnds) implics - - ; return (final_unsolved, final_implics) } - - where solve_one (tv,(ty,cv,fl)) - | not (typeKind ty `isSubKind` tyVarKind tv) - = addErrorTcS KindError fl (mkTyVarTy tv) ty - -- Must do a small kind check since TcCanonical invariants - -- on family equations only impose compatibility, not subkinding - | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty - - subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint - subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv) - subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl) - - subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar - subst_wevar funeq_bnds (WantedEvVar v loc) - = let orig_ty = varType v - new_ty = substFunEqBnds funeq_bnds orig_ty - in WantedEvVar (setVarType v new_ty) loc - - subst_impl :: FunEqBinds -> Implication -> Implication - subst_impl funeq_bnds impl@(Implic { ic_wanted = ws }) - = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws } - - -type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))] --- Invariant: if it contains: --- [... a -> (ta,...) ... b -> (tb,...) ... ] --- then 'ta' cannot mention 'b' + ; mapM_ solve_one cv_binds + + ; return (niFixTvSubst ni_subst, unsolved_can_cts) } + where + solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty +------------ +type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)]) + -- The TvSubstEnv is not idempotent, but is loop-free + -- See Note [Non-idempotent substitution] in Unify +emptyFunEqBinds :: FunEqBinds +emptyFunEqBinds = (emptyVarEnv, []) + +extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds +extendFunEqBinds (tv_subst, cv_binds) cv tv ty + = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds) + +------------ getSolvableCTyFunEqs :: TcsUntouchables - -> CanonicalCts -- Precondition: all wanteds + -> CanonicalCts -- Precondition: all Wanteds or Derived! -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables getSolvableCTyFunEqs untch cts - = Bag.foldlBag dflt_funeq (emptyCCan, []) cts - where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv - , cc_flavor = fl - , cc_fun = tc - , cc_tyargs = xis - , cc_rhs = xi }) - | Just tv <- tcGetTyVar_maybe xi - , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable - , Nothing <- lookup tv extra_binds -- or in extra_binds - -- See Note [Solving Family Equations], Point 1 - = ASSERT ( isWanted fl ) - let ty_orig = mkTyConApp tc xis - ty_bind = substFunEqBnds extra_binds ty_orig - in if tv `elemVarSet` tyVarsOfType ty_bind - then (cts_in `extendCCans` ct, extra_binds) - -- See Note [Solving Family Equations], Point 2 - else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds) - -- Postcondition met because extra_binds is already applied to ty_bind - - dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds) - -substFunEqBnds :: FunEqBinds -> TcType -> TcType -substFunEqBnds bnds ty - = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds - -- foldr works because of the FunEqBinds invariant - - + = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts + where + dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt + -> (CanonicalCts, FunEqBinds) + dflt_funeq (cts_in, feb@(tv_subst, _)) + (CFunEqCan { cc_id = cv + , cc_flavor = fl + , cc_fun = tc + , cc_tyargs = xis + , cc_rhs = xi }) + | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable + + , isTouchableMetaTyVar_InRange untch tv + -- And it's a *touchable* unification variable + + , typeKind xi `isSubKind` tyVarKind tv + -- Must do a small kind check since TcCanonical invariants + -- on family equations only impose compatibility, not subkinding + + , not (tv `elemVarEnv` tv_subst) + -- Check not in extra_binds + -- See Note [Solving Family Equations], Point 1 + + , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis)) + -- Occurs check: see Note [Solving Family Equations], Point 2 + = ASSERT ( not (isGiven fl) ) + (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis)) + + dflt_funeq (cts_in, fun_eq_binds) ct + = (cts_in `extendCCans` ct, fun_eq_binds) \end{code} Note [Solving Family Equations] @@ -988,8 +1020,8 @@ Basic plan behind applyDefaulting rules: \begin{code} applyDefaultingRules :: InertSet - -> CanonicalCts -- All wanteds - -> TcS (Bag WantedEvVar) -- All wanteds again! + -> CanonicalCts -- All wanteds + -> TcS (Bag FlavoredEvVar) -- All wanteds again! -- Return some *extra* givens, which express the -- type-class-default choice @@ -1011,7 +1043,7 @@ applyDefaultingRules inert wanteds ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) } ------------------ -defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar) +defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar) -- defaultTyVar is used 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 @@ -1031,7 +1063,7 @@ defaultTyVar untch the_tv , not (k `eqKind` default_k) = do { ev <- TcSMonad.newKindConstraint the_tv default_k ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk - ; return (unitBag (WantedEvVar ev loc)) } + ; return (unitBag (mkEvVarX ev (Wanted loc))) } | otherwise = return emptyBag -- The common case where @@ -1096,39 +1128,41 @@ disambigGroup :: [Type] -- The default types -> InertSet -- Given inert -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) -- sharing same type variable - -> TcS (Bag WantedEvVar) + -> TcS (Bag FlavoredEvVar) disambigGroup [] _inert _grp = return emptyBag disambigGroup (default_ty:default_tys) inert group = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty) - ; let ct_loc = get_ct_loc (cc_flavor the_ct) - ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty - ; success <- tryTcS $ - do { final_inert <- solveInteract inert $ - consBag (Wanted ct_loc, ev) wanted_to_solve + ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty + ; let der_flav = mk_derived_flavor (cc_flavor the_ct) + derived_eq = mkEvVarX ev der_flav + + ; success <- tryTcS $ + do { (_,final_inert) <- solveInteract inert $ listToBag $ + derived_eq : wanted_ev_vars ; let (_, unsolved) = extractUnsolved final_inert - ; errs <- getTcSErrorsBag - ; return (isEmptyBag unsolved && isEmptyBag errs) } + ; let wanted_unsolved = filterBag isWantedCt unsolved + -- Don't care about Derived's + ; return (isEmptyBag wanted_unsolved) } ; case success of True -> -- Success: record the type variable binding, and return do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty ; traceTcS "disambigGroup succeeded" (ppr default_ty) - ; return (unitBag $ WantedEvVar ev ct_loc) } + ; return (unitBag derived_eq) } False -> -- Failure: try with the next type - do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty) + do { traceTcS "disambigGroup failed, will try other default types" + (ppr default_ty) ; disambigGroup default_tys inert group } } where ((the_ct,the_tv):_) = group wanteds = map fst group - wanted_ev_vars = map deCanonicaliseWanted wanteds - wanted_to_solve = listToBag $ - map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars - - get_ct_loc (Wanted l) = l - get_ct_loc _ = panic "Asked to disambiguate given or derived!" - + wanted_ev_vars :: [FlavoredEvVar] + wanted_ev_vars = map deCanonicalise wanteds + mk_derived_flavor :: CtFlavor -> CtFlavor + mk_derived_flavor (Wanted loc) = Derived loc + mk_derived_flavor _ = panic "Asked to disambiguate given or derived!" \end{code} Note [Avoiding spurious errors] @@ -1143,3 +1177,19 @@ that g isn't polymorphic enough; but then we get another one when dealing with the (Num a) context arising from f's definition; we try to unify a with Int (to default it), but find that it's already been unified with the rigid variable from g's type sig + + + +********************************************************************************* +* * +* Utility functions +* * +********************************************************************************* + +\begin{code} +newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar) +newFlatWanteds orig theta + = do { loc <- getCtLoc orig + ; evs <- newWantedEvVars theta + ; return (listToBag [EvVarX w loc | w <- evs]) } +\end{code} \ No newline at end of file diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs index cb4043e239e4da96a259c99fdbba8925730d8aa6..cc18707ac266bde5aca7355a3cbe6f070c6024c5 100644 --- a/compiler/typecheck/TcSplice.lhs +++ b/compiler/typecheck/TcSplice.lhs @@ -343,16 +343,17 @@ tcBracket brack res_ty ; lie_var <- getConstraintVar ; let brack_stage = Brack cur_stage pending_splices lie_var - ; (meta_ty, lie) <- setStage brack_stage $ - captureConstraints $ - tc_bracket cur_stage brack - - ; simplifyBracket lie - - -- Make the expected type have the right shape - ; _ <- unifyType meta_ty res_ty - - -- Return the original expression, not the type-decorated one + -- We want to check that there aren't any constraints that + -- can't be satisfied (e.g. Show Foo, where Foo has no Show + -- instance), but we aren't otherwise interested in the + -- results. Nor do we care about ambiguous dictionaries etc. + -- We will type check this bracket again at its usage site. + ; _ <- newImplication BracketSkol [] [] $ + setStage brack_stage $ + do { meta_ty <- tc_bracket cur_stage brack + ; unifyType meta_ty res_ty } + + -- Return the original expression, not the type-decorated one ; pendings <- readMutVar pending_splices ; return (noLoc (HsBracketOut brack pendings)) } diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index c68c10ffa6ed0b980f8979df32549255296a814c..3ea53e81fde31f7fdce90d462bc6f3d12555e6bc 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -24,13 +24,12 @@ module TcType ( -------------------------------- -- MetaDetails UserTypeCtxt(..), pprUserTypeCtxt, - TcTyVarDetails(..), pprTcTyVarDetails, + TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv, MetaDetails(Flexi, Indirect), MetaInfo(..), - SkolemInfo(..), pprSkolTvBinding, pprSkolInfo, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isSigTyVar, isOverlappableTyVar, isTyConableTyVar, metaTvRef, - isFlexi, isIndirect, isUnkSkol, isRuntimeUnkSkol, + isFlexi, isIndirect, isRuntimeUnkSkol, -------------------------------- -- Builders @@ -53,7 +52,7 @@ module TcType ( -- Again, newtypes are opaque tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX, eqKind, - isSigmaTy, isOverloadedTy, isRigidTy, + isSigmaTy, isOverloadedTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isIntegerTy, isBoolTy, isUnitTy, isCharTy, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, @@ -74,7 +73,7 @@ module TcType ( isPredTy, isDictTy, isDictLikeTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, isIPPred, - isRefineableTy, isRefineablePred, + mkMinimalBySCs, transSuperClasses, immSuperClasses, -- * Tidying type related things up for printing tidyType, tidyTypes, @@ -82,7 +81,7 @@ module TcType ( tidyTyVarBndr, tidyFreeTyVars, tidyOpenTyVar, tidyOpenTyVars, tidyTopType, tidyPred, - tidyKind, tidySkolemTyVar, + tidyKind, --------------------------------- -- Foreign import and export @@ -147,7 +146,6 @@ module TcType ( -- friends: import TypeRep -import DataCon import Class import Var import ForeignCall @@ -155,7 +153,6 @@ import VarSet import Type import Coercion import TyCon -import HsExpr( HsMatchContext ) -- others: import DynFlags @@ -273,9 +270,15 @@ TcBinds.tcInstSig, and its use_skols parameter. \begin{code} -- A TyVarDetails is inside a TyVar data TcTyVarDetails - = SkolemTv SkolemInfo -- A skolem constant + = SkolemTv -- A skolem + Bool -- True <=> this skolem type variable can be overlapped + -- when looking up instances + -- See Note [Binding when looking up instances] in InstEnv - | FlatSkol TcType + | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi + -- interactive context + + | FlatSkol TcType -- The "skolem" obtained by flattening during -- constraint simplification @@ -285,11 +288,20 @@ data TcTyVarDetails | MetaTv MetaInfo (IORef MetaDetails) +vanillaSkolemTv, superSkolemTv :: TcTyVarDetails +-- See Note [Binding when looking up instances] in InstEnv +vanillaSkolemTv = SkolemTv False -- Might be instantiated +superSkolemTv = SkolemTv True -- Treat this as a completely distinct type + data MetaDetails = Flexi -- Flexi type variables unify to become Indirects | Indirect TcType -data MetaInfo +instance Outputable MetaDetails where + ppr Flexi = ptext (sLit "Flexi") + ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty + +data MetaInfo = TauTv -- This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which -- never contains any ForAlls @@ -308,44 +320,11 @@ data MetaInfo -- Nevertheless, the constraint solver has to try to guess -- what type to instantiate it to ----------------------------------- --- SkolemInfo describes a site where --- a) type variables are skolemised --- b) an implication constraint is generated -data SkolemInfo - = SigSkol UserTypeCtxt -- A skolem that is created by instantiating - -- a programmer-supplied type signature - -- Location of the binding site is on the TyVar - - -- The rest are for non-scoped skolems - | ClsSkol Class -- Bound at a class decl - | InstSkol -- Bound at an instance decl - | FamInstSkol -- Bound at a family instance decl - | PatSkol -- An existential type variable bound by a pattern for - DataCon -- a data constructor with an existential type. - (HsMatchContext Name) - -- e.g. data T = forall a. Eq a => MkT a - -- f (MkT x) = ... - -- The pattern MkT x will allocate an existential type - -- variable for 'a'. - - | ArrowSkol -- An arrow form (see TcArrows) - - | IPSkol [IPName Name] -- Binding site of an implicit parameter - - | RuleSkol RuleName -- The LHS of a RULE - | GenSkol TcType -- Bound when doing a subsumption check for ty - - | RuntimeUnkSkol -- a type variable used to represent an unknown - -- runtime type (used in the GHCi debugger) - - | UnkSkol -- Unhelpful info (until I improve it) - ------------------------------------- --- UserTypeCtxt describes the places where a --- programmer-written type signature can occur --- Like SkolemInfo, no location info -data UserTypeCtxt +-- UserTypeCtxt describes the origin of the polymorphic type +-- in the places where we need to an expression has that type + +data UserTypeCtxt = FunSigCtxt Name -- Function type signature -- Also used for types in SPECIALISE pragmas | ExprSigCtxt -- Expression type signature @@ -364,6 +343,10 @@ data UserTypeCtxt | SpecInstCtxt -- SPECIALISE instance pragma | ThBrackCtxt -- Template Haskell type brackets [t| ... |] + | GenSigCtxt -- Higher-rank or impredicative situations + -- e.g. (f e) where f has a higher-rank type + -- We might want to elaborate this + -- Notes re TySynCtxt -- We allow type synonyms that aren't types; e.g. type List = [] -- @@ -409,7 +392,8 @@ kind_var_occ = mkOccName tvName "k" \begin{code} pprTcTyVarDetails :: TcTyVarDetails -> SDoc -- For debugging -pprTcTyVarDetails (SkolemTv _) = ptext (sLit "sk") +pprTcTyVarDetails (SkolemTv {}) = ptext (sLit "sk") +pprTcTyVarDetails (RuntimeUnk {}) = ptext (sLit "rt") pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk") pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau") pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs") @@ -428,53 +412,7 @@ pprUserTypeCtxt ResSigCtxt = ptext (sLit "a result type signature") pprUserTypeCtxt (ForSigCtxt n) = ptext (sLit "the foreign declaration for") <+> quotes (ppr n) pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration") pprUserTypeCtxt SpecInstCtxt = ptext (sLit "a SPECIALISE instance pragma") - -pprSkolTvBinding :: TcTyVar -> SDoc --- Print info about the binding of a skolem tyvar, --- or nothing if we don't have anything useful to say -pprSkolTvBinding tv - = ASSERT ( isTcTyVar tv ) - quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv) - where - ppr_details (SkolemTv info) = ppr_skol info - ppr_details (FlatSkol {}) = ptext (sLit "is a flattening type variable") - ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") - <+> quotes (ppr n) - ppr_details (MetaTv _ _) = ptext (sLit "is a meta type variable") - - ppr_skol UnkSkol = ptext (sLit "is an unknown type variable") -- Unhelpful - ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type") - ppr_skol info = sep [ptext (sLit "is a rigid type variable bound by"), - sep [pprSkolInfo info, - nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]] - -instance Outputable SkolemInfo where - ppr = pprSkolInfo - -pprSkolInfo :: SkolemInfo -> SDoc --- Complete the sentence "is a rigid type variable bound by..." -pprSkolInfo (SigSkol ctxt) = pprUserTypeCtxt ctxt -pprSkolInfo (IPSkol ips) = ptext (sLit "the implicit-parameter bindings for") - <+> pprWithCommas ppr ips -pprSkolInfo (ClsSkol cls) = ptext (sLit "the class declaration for") <+> quotes (ppr cls) -pprSkolInfo InstSkol = ptext (sLit "the instance declaration") -pprSkolInfo FamInstSkol = ptext (sLit "the family instance declaration") -pprSkolInfo (RuleSkol name) = ptext (sLit "the RULE") <+> doubleQuotes (ftext name) -pprSkolInfo ArrowSkol = ptext (sLit "the arrow form") -pprSkolInfo (PatSkol dc _) = sep [ ptext (sLit "a pattern with constructor") - , ppr dc <+> dcolon <+> ppr (dataConUserType dc) ] -pprSkolInfo (GenSkol ty) = sep [ ptext (sLit "the polymorphic type") - , quotes (ppr ty) ] - --- UnkSkol --- For type variables the others are dealt with by pprSkolTvBinding. --- For Insts, these cases should not happen -pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol") -pprSkolInfo RuntimeUnkSkol = WARN( True, text "pprSkolInfo: RuntimeUnkSkol" ) ptext (sLit "RuntimeUnkSkol") - -instance Outputable MetaDetails where - ppr Flexi = ptext (sLit "Flexi") - ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty +pprUserTypeCtxt GenSigCtxt = ptext (sLit "a type expected by the context") \end{code} @@ -491,18 +429,27 @@ instance Outputable MetaDetails where -- It doesn't change the uniques at all, just the print names. tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar) tidyTyVarBndr env@(tidy_env, subst) tyvar - = case tidyOccName tidy_env (getOccName name) of + = case tidyOccName tidy_env occ1 of (tidy', occ') -> ((tidy', subst'), tyvar'') where - subst' = extendVarEnv subst tyvar tyvar'' - tyvar' = setTyVarName tyvar name' - name' = tidyNameOcc name occ' - -- Don't forget to tidy the kind for coercions! + subst' = extendVarEnv subst tyvar tyvar'' + tyvar' = setTyVarName tyvar name' + + name' = tidyNameOcc name occ' + + -- Don't forget to tidy the kind for coercions! tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind' | otherwise = tyvar' kind' = tidyType env (tyVarKind tyvar) where name = tyVarName tyvar + occ = getOccName name + -- System Names are for unification variables; + -- when we tidy them we give them a trailing "0" (or 1 etc) + -- so that they don't take precedence for the un-modified name + occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0") + | otherwise = occ + --------------- tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv @@ -577,24 +524,6 @@ tidyOpenTypes env tys = mapAccumL tidyOpenType env tys tidyTopType :: Type -> Type tidyTopType ty = tidyType emptyTidyEnv ty ---------------- -tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) --- Tidy the type inside a GenSkol, preparatory to printing it -tidySkolemTyVar env tv - = ASSERT( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) ) - (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1) - where - (env1, info1) = case tcTyVarDetails tv of - SkolemTv info -> (env1, SkolemTv info') - where - (env1, info') = tidy_skol_info env info - info -> (env, info) - - tidy_skol_info env (GenSkol ty) = (env1, GenSkol ty1) - where - (env1, ty1) = tidyOpenType env ty - tidy_skol_info env info = (env, info) - --------------- tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind) tidyKind env k = tidyOpenType env k @@ -629,18 +558,16 @@ isTyConableTyVar tv isSkolemTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - SkolemTv {} -> True - FlatSkol {} -> True - MetaTv {} -> False + SkolemTv {} -> True + FlatSkol {} -> True + RuntimeUnk {} -> True + MetaTv {} -> False --- isOverlappableTyVar has a unique purpose. --- See Note [Binding when looking up instances] in InstEnv. isOverlappableTyVar tv = ASSERT( isTcTyVar tv ) case tcTyVarDetails tv of - SkolemTv (PatSkol {}) -> True - SkolemTv (InstSkol {}) -> True - _ -> False + SkolemTv overlappable -> overlappable + _ -> False isMetaTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) @@ -675,15 +602,9 @@ isIndirect _ = False isRuntimeUnkSkol :: TyVar -> Bool -- Called only in TcErrors; see Note [Runtime skolems] there -isRuntimeUnkSkol x | isTcTyVar x - , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x - = True - | otherwise = False - -isUnkSkol :: TyVar -> Bool -isUnkSkol x | isTcTyVar x - , SkolemTv UnkSkol <- tcTyVarDetails x = True - | otherwise = False +isRuntimeUnkSkol x + | isTcTyVar x, RuntimeUnk <- tcTyVarDetails x = True + | otherwise = False \end{code} @@ -713,7 +634,6 @@ isTauTy (FunTy a b) = isTauTy a && isTauTy b isTauTy (PredTy _) = True -- Don't look through source types isTauTy _ = False - isTauTyCon :: TyCon -> Bool -- Returns False for type synonyms whose expansion is a polytype isTauTyCon tc @@ -721,24 +641,7 @@ isTauTyCon tc | otherwise = True --------------- -isRigidTy :: TcType -> Bool --- A type is rigid if it has no meta type variables in it -isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty)) - -isRefineableTy :: TcType -> (Bool,Bool) --- A type should have type refinements applied to it if it has --- free type variables, and they are all rigid -isRefineableTy ty = (null tc_tvs, all isImmutableTyVar tc_tvs) - where - tc_tvs = varSetElems (tcTyVarsOfType ty) - -isRefineablePred :: TcPredType -> Bool -isRefineablePred pred = not (null tc_tvs) && all isImmutableTyVar tc_tvs - where - tc_tvs = varSetElems (tcTyVarsOfPred pred) - ---------------- -getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to +getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to -- construct a dictionary function name getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty' getDFunTyKey (TyVarTy tv) = getOccName tv @@ -1037,6 +940,35 @@ isDictLikeTy (TyConApp tc tys) isDictLikeTy _ = False \end{code} +Superclasses + +\begin{code} +mkMinimalBySCs :: [PredType] -> [PredType] +-- Remove predicates that can be deduced from others by superclasses +mkMinimalBySCs ptys = [ ploc | ploc <- ptys + , ploc `not_in_preds` rec_scs ] + where + rec_scs = concatMap trans_super_classes ptys + not_in_preds p ps = null (filter (tcEqPred p) ps) + trans_super_classes (ClassP cls tys) = transSuperClasses cls tys + trans_super_classes _other_pty = [] + +transSuperClasses :: Class -> [Type] -> [PredType] +transSuperClasses cls tys + = foldl (\pts p -> trans_sc p ++ pts) [] $ + immSuperClasses cls tys + where trans_sc :: PredType -> [PredType] + trans_sc this_pty@(ClassP cls tys) + = foldl (\pts p -> trans_sc p ++ pts) [this_pty] $ + immSuperClasses cls tys + trans_sc pty = [pty] + +immSuperClasses :: Class -> [Type] -> [PredType] +immSuperClasses cls tys + = substTheta (zipTopTvSubst tyvars tys) sc_theta + where (tyvars,sc_theta,_,_) = classBigSig cls +\end{code} + Note [Dictionary-like types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Being "dictionary-like" means either a dictionary type or a tuple thereof. diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index f74f1af07fc8ccac1621e705804a3ead87371d5f..985d9bc69a5aac668c29858eec0092a8df6cfc49 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -27,8 +27,8 @@ module TcUnify ( import HsSyn import TypeRep - -import TcErrors ( typeExtraInfoMsg, unifyCtxt ) +import CoreUtils( mkPiTypes ) +import TcErrors ( unifyCtxt ) import TcMType import TcIface import TcRnMonad @@ -44,7 +44,6 @@ import VarEnv import Name import ErrUtils import BasicTypes -import Bag import Maybes ( allMaybes ) import Util @@ -298,14 +297,14 @@ which takes an HsExpr of type actual_ty into one of type expected_ty. \begin{code} -tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -- Check that ty_actual is more polymorphic than ty_expected -- Both arguments might be polytypes, so we must instantiate and skolemise -- Returns a wrapper of shape ty_actual ~ ty_expected -tcSubType origin skol_info ty_actual ty_expected +tcSubType origin ctxt ty_actual ty_expected | isSigmaTy ty_actual = do { (sk_wrap, inst_wrap) - <- tcGen skol_info ty_expected $ \ _ sk_rho -> do + <- tcGen ctxt ty_expected $ \ _ sk_rho -> do { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual ; coi <- unifyType in_rho sk_rho ; return (coiToHsWrapper coi <.> in_wrap) } @@ -353,16 +352,16 @@ wrapFunResCoercion arg_tys co_fn_res %************************************************************************ \begin{code} -tcGen :: SkolemInfo -> TcType +tcGen :: UserTypeCtxt -> TcType -> ([TcTyVar] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty -tcGen skol_info expected_ty thing_inside +tcGen ctxt expected_ty thing_inside -- We expect expected_ty to be a forall-type -- If not, the call is a no-op = do { traceTc "tcGen" empty - ; (wrap, tvs', given, rho') <- deeplySkolemise skol_info expected_ty + ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty ; when debugIsOn $ traceTc "tcGen" $ vcat [ @@ -379,9 +378,13 @@ tcGen skol_info expected_ty thing_inside -- So now s' isn't unconstrained because it's linked to a. -- -- However [Oct 10] now that the untouchables are a range of - -- TcTyVars, all tihs is handled automatically with no need for + -- TcTyVars, all this is handled automatically with no need for -- extra faffing around + -- Use the *instantiated* type in the SkolemInfo + -- so that the names of displayed type variables line up + ; let skol_info = SigSkol ctxt (mkPiTypes given rho') + ; (ev_binds, result) <- checkConstraints skol_info tvs' given $ thing_inside tvs' rho' @@ -414,7 +417,7 @@ newImplication skol_info skol_tvs given thing_inside captureUntouchables $ thing_inside - ; if isEmptyBag wanted && not (hasEqualities given) + ; if isEmptyWC wanted && not (hasEqualities given) -- Optimisation : if there are no wanteds, and the givens -- are sufficiently simple, don't generate an implication -- at all. Reason for the hasEqualities test: @@ -426,16 +429,15 @@ newImplication skol_info skol_tvs given thing_inside { ev_binds_var <- newTcEvBinds ; lcl_env <- getLclTypeEnv ; loc <- getCtLoc skol_info - ; let implic = Implic { ic_untch = untch - , ic_env = lcl_env - , ic_skols = mkVarSet skol_tvs - , ic_scoped = panic "emitImplication" - , ic_given = given - , ic_wanted = wanted - , ic_binds = ev_binds_var - , ic_loc = loc } - - ; emitConstraint (WcImplic implic) + ; emitImplication $ Implic { ic_untch = untch + , ic_env = lcl_env + , ic_skols = mkVarSet skol_tvs + , ic_given = given + , ic_wanted = wanted + , ic_insol = insolubleWC wanted + , ic_binds = ev_binds_var + , ic_loc = loc } + ; return (TcEvBinds ev_binds_var, result) } } \end{code} @@ -518,11 +520,16 @@ uType, uType_np, uType_defer -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] uType_defer (item : origin) ty1 ty2 - = do { co_var <- newWantedCoVar ty1 ty2 - ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin]) + = wrapEqCtxt origin $ + do { co_var <- newWantedCoVar ty1 ty2 ; loc <- getCtLoc (TypeEqOrigin item) - ; wrapEqCtxt origin $ - emitConstraint (WcEvVar (WantedEvVar co_var loc)) + ; emitFlat (mkEvVarX co_var loc) + + -- Error trace only + ; ctxt <- getErrCtxt + ; doc <- mkErrInfo emptyTidyEnv ctxt + ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin, doc]) + ; return $ ACo $ mkTyVarTy co_var } uType_defer [] _ _ = panic "uType_defer" @@ -629,7 +636,7 @@ unifySigmaTy origin ty1 ty2 = do { let (tvs1, body1) = tcSplitForAllTys ty1 (tvs2, body2) = tcSplitForAllTys ty2 ; unless (equalLength tvs1 tvs2) (failWithMisMatch origin) - ; skol_tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo + ; skol_tvs <- tcInstSkolTyVars tvs1 -- Get location from monad, not from tvs1 ; let tys = mkTyVarTys skol_tvs in_scope = mkInScopeSet (mkVarSet skol_tvs) @@ -641,9 +648,7 @@ unifySigmaTy origin ty1 ty2 captureUntouchables $ uType origin phi1 phi2 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a) - ; let bad_lie = filterBag is_bad lie - is_bad w = any (`elemVarSet` tyVarsOfWanted w) skol_tvs - ; when (not (isEmptyBag bad_lie)) + ; when (any (`elemVarSet` tyVarsOfWC lie) skol_tvs) (failWithMisMatch origin) -- ToDo: give details from bad_lie ; emitConstraints lie @@ -1019,7 +1024,7 @@ lookupTcTyVar tyvar Indirect ty -> return (Filled ty) Flexi -> do { is_untch <- isUntouchable tyvar ; let -- Note [Unifying untouchables] - ret_details | is_untch = SkolemTv UnkSkol + ret_details | is_untch = vanillaSkolemTv | otherwise = details ; return (Unfilled ret_details) } } | otherwise @@ -1075,18 +1080,14 @@ failWithMisMatch (item:origin) ; env0 <- tcInitTidyEnv ; let (env1, pp_exp) = tidyOpenType env0 ty_exp (env2, pp_act) = tidyOpenType env1 ty_act - ; failWithTcM (misMatchMsg env2 pp_act pp_exp) } + ; failWithTcM (env2, misMatchMsg pp_act pp_exp) } failWithMisMatch [] = panic "failWithMisMatch" -misMatchMsg :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc) -misMatchMsg env ty_act ty_exp - = (env2, sep [sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp) - , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)] - , nest 2 (extra1 $$ extra2) ]) - where - (env1, extra1) = typeExtraInfoMsg env ty_exp - (env2, extra2) = typeExtraInfoMsg env1 ty_act +misMatchMsg :: TcType -> TcType -> SDoc +misMatchMsg ty_act ty_exp + = sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp) + , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)] \end{code} diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index eed3bf57cb5b254c4c724dec7d16bf83769f123d..93a67a7eddc17417e9ed7fb1fed3c0c8039d5cc5 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -187,6 +187,9 @@ data FamilyInstEnv -- If *not* then the common case of looking up -- (T a b c) can fail immediately +instance Outputable FamilyInstEnv where + ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs) + -- INVARIANTS: -- * The fs_tvs are distinct in each FamInst -- of a range value of the map (so we can safely unify them) diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 2f2cfb892734c4c31b990705989bd2916492f72f..2acf71efa6e75ab6534d7e5845f9368161d81b11 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -13,7 +13,8 @@ module Unify ( dataConCannotMatch, -- Side-effect free unification - tcUnifyTys, BindFlag(..) + tcUnifyTys, BindFlag(..), + niFixTvSubst, niSubstTvSet ) where @@ -31,7 +32,6 @@ import Outputable import ErrUtils import Util import Maybes -import UniqFM import FastString \end{code} @@ -373,8 +373,8 @@ dataConCannotMatch tys con %************************************************************************ %* * - Unification -%* * + Unification +%* * %************************************************************************ \begin{code} @@ -389,28 +389,48 @@ tcUnifyTys bind_fn tys1 tys2 do { subst <- unifyList emptyTvSubstEnv tys1 tys2 -- Find the fixed point of the resulting non-idempotent substitution - ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2) - tv_env = fixTvSubstEnv in_scope subst + ; return (niFixTvSubst subst) } +\end{code} + + +%************************************************************************ +%* * + Non-idempotent substitution +%* * +%************************************************************************ + +Note [Non-idempotent substitution] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +During unification we use a TvSubstEnv that is + (a) non-idempotent + (b) loop-free; ie repeatedly applying it yields a fixed point - ; return (mkTvSubst in_scope tv_env) } +\begin{code} +niFixTvSubst :: TvSubstEnv -> TvSubst +-- Find the idempotent fixed point of the non-idempotent substitution +-- ToDo: use laziness instead of iteration? +niFixTvSubst env = f env where - tvs1 = tyVarsOfTypes tys1 - tvs2 = tyVarsOfTypes tys2 - ----------------------------- --- XXX Can we do this more nicely, by exploiting laziness? --- Or avoid needing it in the first place? -fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv -fixTvSubstEnv in_scope env = f env + f e | not_fixpoint = f (mapVarEnv (substTy subst) e) + | otherwise = subst + where + range_tvs = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e + subst = mkTvSubst (mkInScopeSet range_tvs) e + not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs + in_domain tv = tv `elemVarEnv` e + +niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet +-- Apply the non-idempotent substitution to a set of type variables, +-- remembering that the substitution isn't necessarily idempotent +-- This is used in the occurs check, before extending the substitution +niSubstTvSet subst tvs + = foldVarSet (unionVarSet . get) emptyVarSet tvs where - f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e - in if and $ eltsUFM $ intersectUFM_C tcEqType e e' - then e - else f e' - + get tv = case lookupVarEnv subst tv of + Nothing -> unitVarSet tv + Just ty -> niSubstTvSet subst (tyVarsOfType ty) \end{code} - %************************************************************************ %* * The workhorse @@ -543,7 +563,7 @@ uUnrefined subst tv1 ty2 (TyVarTy tv2) bind tv ty = return $ extendVarEnv subst tv ty uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable - | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2') + | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2') = failWith (occursCheck tv1 ty2) -- Occurs check | not (k2 `isSubKind` k1) = failWith (kindMisMatch tv1 ty2) -- Kind check @@ -553,16 +573,6 @@ uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable k1 = tyVarKind tv1 k2 = typeKind ty2' -substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet --- Apply the non-idempotent substitution to a set of type variables, --- remembering that the substitution isn't necessarily idempotent -substTvSet subst tvs - = foldVarSet (unionVarSet . get) emptyVarSet tvs - where - get tv = case lookupVarEnv subst tv of - Nothing -> unitVarSet tv - Just ty -> substTvSet subst (tyVarsOfType ty) - bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv bindTv subst tv ty -- ty is not a type variable = do { b <- tvBindFlag tv diff --git a/compiler/utils/Bag.lhs b/compiler/utils/Bag.lhs index fa18219cb8d4b3194232f9e8e6d05bed3242eff0..bb0f10481a6c6c1bc083f8b15d4883966b3236f2 100644 --- a/compiler/utils/Bag.lhs +++ b/compiler/utils/Bag.lhs @@ -18,7 +18,7 @@ module Bag ( listToBag, bagToList, foldlBagM, mapBagM, mapBagM_, flatMapBagM, flatMapBagPairM, - mapAndUnzipBagM + mapAndUnzipBagM, mapAccumBagLM ) where #include "Typeable.h" @@ -231,6 +231,19 @@ mapAndUnzipBagM f (ListBag xs) = do ts <- mapM f xs let (rs,ss) = unzip ts return (ListBag rs, ListBag ss) +mapAccumBagLM :: Monad m + => (acc -> x -> m (acc, y)) -- ^ combining funcction + -> acc -- ^ initial state + -> Bag x -- ^ inputs + -> m (acc, Bag y) -- ^ final state, outputs +mapAccumBagLM _ s EmptyBag = return (s, EmptyBag) +mapAccumBagLM f s (UnitBag x) = do { (s1, x1) <- f s x; return (s1, UnitBag x1) } +mapAccumBagLM f s (TwoBags b1 b2) = do { (s1, b1') <- mapAccumBagLM f s b1 + ; (s2, b2') <- mapAccumBagLM f s1 b2 + ; return (s2, TwoBags b1' b2') } +mapAccumBagLM f s (ListBag xs) = do { (s', xs') <- mapAccumLM f s xs + ; return (s', ListBag xs') } + listToBag :: [a] -> Bag a listToBag [] = EmptyBag listToBag vs = ListBag vs