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
mkTyVarOcc, mkTyVarOccFS,
mkTcOcc, mkTcOccFS,
mkClsOcc, mkClsOccFS,
- mkDFunOcc,
+ mkDFunOcc,
mkTupleOcc,
setOccNameSpace,
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}
%************************************************************************
mkTyVar, mkTcTyVar, mkWildCoVar,
-- ** Taking 'TyVar's apart
- tyVarName, tyVarKind, tcTyVarDetails,
+ tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails,
-- ** Modifying 'TyVar's
setTyVarName, setTyVarUnique, setTyVarKind,
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}
%************************************************************************
-- | 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 ()
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
-- | 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
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
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.
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
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
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 */
-- 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))
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"
import HscTypes
import Id
import Name
-import Var ( Var, TyVar, EvVar, varType, setVarType )
+import Var
import VarEnv
import VarSet
import PrelNames
import Maybes
import Util
import Outputable
-import Data.List
+import Data.List( mapAccumL )
\end{code}
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)
\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
-- 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'
%************************************************************************
\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
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
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
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
import Name
import NameSet
import NameEnv
-import VarSet
import SrcLoc
import Bag
import ErrUtils
-- 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) $
; 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
; 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)
-- 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
| 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
\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
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]
; (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
\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
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
-- 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].
, cc_flavor = fl
, cc_class = cn
, cc_tyargs = xis }) }
-
\end{code}
Note [Adding superclasses]
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]
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
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
; 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) }
, 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]
; 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 }
-- 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]
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
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
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
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
-- 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
-- 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
= 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):_)
\begin{code}
module TcErrors(
- reportUnsolved, reportUnsolvedDeriv,
- reportUnsolvedWantedEvVars, warnDefaulting,
- unifyCtxt, typeExtraInfoMsg,
+ reportUnsolved,
+ warnDefaulting,
+ unifyCtxt,
flattenForAllErrorTcS,
solverDepthErrorTcS
import Name
import NameEnv
import Id ( idType )
-import HsExpr ( pprMatchContext )
import Var
import VarSet
import VarEnv
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
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
-- 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
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
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
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 ()
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}
\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}
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
= -- 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)
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
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
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)
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
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 ]
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:"),
-- 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
-- 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
-- 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
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
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]
%************************************************************************
\begin{code}
-
solverDepthErrorTcS :: Int -> [CanonicalCt] -> TcS a
solverDepthErrorTcS depth stack
| null stack -- Shouldn't happen unless you say -fcontext-stack=0
| 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
\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}
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') }
-- 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
-- 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
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")
= 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') }
; 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 {
; 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
import TcTyClsDecls
import TcClassDcl
import TcPat( addInlinePrags )
-import TcSimplify( simplifyTop )
import TcRnMonad
import TcMType
import TcType
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
; 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]
, abs_binds = unitBag dict_bind }
; return (unitBag (L loc main_bind) `unionBags`
- unionManyBags sc_binds `unionBags`
listToBag meth_binds)
}
where
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 = <blah> in sc_dict
- -- where <blah> 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)
; (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
\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"
import TcType
import HsBinds
+import Inst( tyVarsOfEvVar )
import InstEnv
import Class
import TyCon
import FunDeps
-import Control.Monad ( when )
-
import Coercion
import Outputable
import Bag
import qualified Data.Map as Map
-import Control.Monad( unless )
+import Control.Monad( when )
+
import FastString ( sLit )
import DynFlags
\end{code}
\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
| 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 *
-- 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
-- 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
| 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
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 = (->)
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}
, 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.
| 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
---------------------------------------------------
--- 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.
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)
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'
= 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
}
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)
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
-- 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
-- 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
-- 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]
-- 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
-- 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
-- { 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 })
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
= 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
; 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
; 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
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'
; 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'
}
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
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:
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:
\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)
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
= 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
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
; 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
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 }
_
= 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}
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:
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:
----------
that participate in recursive dictionary bindings.
\begin{code}
-
-
data LookupInstResult
= NoInstance
| GenInst [WantedEvVar] EvTerm
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) }
}
}
newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newKindVar, newKindVars,
+ mkTcTyVarName,
newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
isFilledMetaTyVar, isFlexiMetaTyVar,
--------------------------------
-- Instantiation
tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
- tcInstType, tcInstSigType, instMetaTyVar,
- tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars,
+ tcInstType, instMetaTyVar,
+ tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+ tcSkolDFunType, tcSuperSkolTyVars,
--------------------------------
-- Checking type validity
--------------------------------
-- 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
import SrcLoc
import Outputable
import FastString
+import Unique( Unique )
import Bag
import Control.Monad
-import Data.List ( (\\) )
+import Data.List ( (\\) )
\end{code}
; 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
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)) }
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
zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
----------------- Types
-
zonkTcTypeCarefully :: TcType -> TcM TcType
-- Do not zonk type variables free in the environment
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 }
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 }
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
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
(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}
\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:
= 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
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
; 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
; 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
-- 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
; traceTc "Tc3" empty
; (tcg_env, inst_infos, _deriv_binds)
<- tcInstDecls1 (concat tycl_decls) inst_decls deriv_decls
+
; setGblEnv tcg_env $ do {
-- Typecheck value declarations
= 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
-- 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) } ;
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 ;
-- Check for unsolved constraints
lie <- readIORef lie_var ;
- if isEmptyBag lie
+ if isEmptyWC lie
then return ()
else pprPanic "initTc: unsolved constraints"
(pprWantedsWithLocs lie) ;
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 ;
-- 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
import HsSyn
import HscTypes
import Type
+import Class ( Class )
+import DataCon ( DataCon, dataConUserType )
import TcType
import Annotations
import InstEnv
import Outputable
import ListSetOps
import FastString
-import StaticFlags( opt_ErrorSpans )
import Data.Set (Set)
\end{code}
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
Unique -- Low end
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
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]
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)
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
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
instance Outputable EqOrigin where
ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2
\end{code}
+
-- 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
-- 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
-- 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,
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
instDFunConstraints,
newFlexiTcSTy,
- isGoodRecEv,
-
compatKind,
-
TcsUntouchables,
isTouchableMetaTyVar,
isTouchableMetaTyVar_InRange,
-- here
- mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps
+ mkDerivedFunDepEqns -- Instantiation of 'Equations' from FunDeps
) where
| 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,
| 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
}
-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
= 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]
isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
isCFunEqCan_Maybe _ = Nothing
+isCFrozenErr :: CanonicalCt -> Bool
+isCFrozenErr (CFrozenErr {}) = True
+isCFrozenErr _ = False
\end{code}
%************************************************************************
%************************************************************************
\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))
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
-- 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
-- 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 *
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
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
; 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
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
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)
= 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!
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
; (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
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 "]")
= 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
-- 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 }
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
\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
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- 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, _))
\begin{code}
module TcSimplify(
simplifyInfer,
- simplifyDefault, simplifyDeriv, simplifyBracket,
+ simplifyDefault, simplifyDeriv,
simplifyRule, simplifyTop, simplifyInteractive
) where
import TcSMonad
import TcInteract
import Inst
+import Unify( niFixTvSubst, niSubstTvSet )
import Var
import VarSet
import VarEnv
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}
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}
*********************************************************************************
-> 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]
***********************************************************************************
\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
| 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]
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
-- 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
--
-- 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 {" $
; 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
; 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
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
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]
\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]
\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
; 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
, 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
-> 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]
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
; 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)) }
--------------------------------
-- 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
-- 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,
isPredTy, isDictTy, isDictLikeTy,
tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
isIPPred,
- isRefineableTy, isRefineablePred,
+ mkMinimalBySCs, transSuperClasses, immSuperClasses,
-- * Tidying type related things up for printing
tidyType, tidyTypes,
tidyTyVarBndr, tidyFreeTyVars,
tidyOpenTyVar, tidyOpenTyVars,
tidyTopType, tidyPred,
- tidyKind, tidySkolemTyVar,
+ tidyKind,
---------------------------------
-- Foreign import and export
-- friends:
import TypeRep
-import DataCon
import Class
import Var
import ForeignCall
import Type
import Coercion
import TyCon
-import HsExpr( HsMatchContext )
-- others:
import DynFlags
\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
| 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
-- 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
| 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 = []
--
\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")
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}
-- 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
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
\end{code}
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 )
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}
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
| 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
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.
import HsSyn
import TypeRep
-
-import TcErrors ( typeExtraInfoMsg, unifyCtxt )
+import CoreUtils( mkPiTypes )
+import TcErrors ( unifyCtxt )
import TcMType
import TcIface
import TcRnMonad
import Name
import ErrUtils
import BasicTypes
-import Bag
import Maybes ( allMaybes )
import Util
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) }
%************************************************************************
\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 [
-- 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'
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:
{ 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}
-- 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"
= 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)
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
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
; 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}
-- 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)
dataConCannotMatch,
-- Side-effect free unification
- tcUnifyTys, BindFlag(..)
+ tcUnifyTys, BindFlag(..),
+ niFixTvSubst, niSubstTvSet
) where
import ErrUtils
import Util
import Maybes
-import UniqFM
import FastString
\end{code}
%************************************************************************
%* *
- Unification
-%* *
+ Unification
+%* *
%************************************************************************
\begin{code}
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
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
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
listToBag, bagToList,
foldlBagM, mapBagM, mapBagM_,
flatMapBagM, flatMapBagPairM,
- mapAndUnzipBagM
+ mapAndUnzipBagM, mapAccumBagLM
) where
#include "Typeable.h"
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