* Do we want to record a package name in a .hi file?
Does pi_mod have a ModuleName or a Module?
-* Does teh finder
+ ------------------------------------
+ Mainly FunDeps (23 Jan 01)
+ ------------------------------------
+
+This commit re-engineers the handling of functional dependencies.
+A functional dependency is no longer an Inst; instead, the necessary
+dependencies are snaffled out of their Class when necessary.
+
+As part of this exercise I found that I had to re-work how to do generalisation
+in a binding group. There is rather exhaustive documentation on the new Plan
+at the top of TcSimplify.
+
+ ******************
+ WARNING: I have compiled all the libraries with this new compiler
+ and all looks well, but I have not run many programs.
+ Things may break. Let me know if so.
+ ******************
+
+The main changes are these:
+
+1. typecheck/TcBinds and TcSimplify have a lot of changes due to the
+ new generalisation and context reduction story. There are extensive
+ comments at the start of TcSimplify
+
+2. typecheck/TcImprove is removed altogether. Instead, improvement is
+ interleaved with context reduction (until a fixpoint is reached).
+ All this is done in TcSimplify.
+
+3. types/FunDeps has new exports
+ * 'improve' does improvement, returning a list of equations
+ * 'grow' and 'oclose' close a list of type variables wrt a set of
+ PredTypes, but in slightly different ways. Comments in file.
+
+4. I improved the way in which we check that main::IO t. It's tidier now.
+
+In addition
+
+* typecheck/TcMatches:
+ a) Tidy up, introducing a common function tcCheckExistentialPat
+
+ b) Improve the typechecking of parallel list comprehensions,
+ which wasn't quite right before. (see comments with tcStmts)
+
+ WARNING: (b) is untested! Jeff, you might want to check.
+
+* Numerous other incidental changes in the typechecker
+
+* Manuel found that rules don't fire well when you have partial applications
+ from overloading. For example, we may get
+
+ f a (d::Ord a) = let m_g = g a d
+ in
+ \y :: a -> ...(m_g (h y))...
+
+ The 'method' m_g doesn't get inlined because (g a d) might be a redex.
+ Yet a rule that looks like
+ g a d (h y) = ...
+ won't fire because that doesn't show up. One way out would be to make
+ the rule matcher a bit less paranoid about duplicating work, but instead
+ I've added a flag
+ -fno-method-sharing
+ which controls whether we generate things like m_g in the first place.
+ It's not clear that they are a win in the first place.
+
+ The flag is actually consulted in Inst.tcInstId
+
+
------------------------------------
Mainly PredTypes (28 Sept 00)
opt_NoMonomorphismRestriction,
-- optimisation opts
+ opt_NoMethodSharing,
opt_DoSemiTagging,
opt_FoldrBuildOn,
opt_LiberateCaseThreshold,
opt_SMP = lookUp SLIT("-fsmp")
-- optimisation opts
+opt_NoMethodSharing = lookUp SLIT("-fno-method-sharing")
opt_DoSemiTagging = lookUp SLIT("-fsemi-tagging")
opt_FoldrBuildOn = lookUp SLIT("-ffoldr-build-on")
opt_LiberateCaseThreshold = lookup_def_int "-fliberate-case-threshold" (10::Int)
Inst,
pprInst, pprInsts, pprInstsInFull, tidyInst, tidyInsts,
- newDictFromOld, newDicts, newClassDicts, newDictsAtLoc,
+ newDictsFromOld, newDicts, newClassDicts,
newMethod, newMethodWithGivenTy, newOverloadedLit,
- newIPDict, instOverloadedFun,
- instantiateFdClassTys, instFunDeps, instFunDepsOfTheta,
- newFunDepFromDict,
+ newIPDict, tcInstId,
tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, instLoc, getDictClassTys,
- getDictPred_maybe, getMethodTheta_maybe,
- getFunDeps, getFunDepsOfLIE,
- getIPs, getIPsOfLIE,
- getAllFunDeps, getAllFunDepsOfLIE,
+ getIPs,
+ predsOfInsts,
lookupInst, lookupSimpleInst, LookupInstResult(..),
- isDict, isClassDict, isMethod,
- isTyVarDict, isStdClassTyVarDict, isMethodFor, notFunDep,
+ isDict, isClassDict, isMethod, instMentionsIPs,
+ isTyVarDict, isStdClassTyVarDict, isMethodFor,
instBindingRequired, instCanBeGeneralised,
- zonkInst, zonkInsts, zonkFunDeps, zonkTvFunDeps,
- instToId, instToIdBndr, ipToId,
+ zonkInst, zonkInsts,
+ instToId,
InstOrigin(..), InstLoc, pprInstLoc
) where
#include "HsVersions.h"
+import CmdLineOpts ( opt_NoMethodSharing )
import HsSyn ( HsLit(..), HsOverLit(..), HsExpr(..) )
import RnHsSyn ( RenamedHsOverLit )
import TcHsSyn ( TcExpr, TcId,
)
import TcMonad
import TcEnv ( TcIdSet, tcGetInstEnv, tcLookupGlobalId )
-import InstEnv ( InstLookupResult(..), lookupInstEnv )
-import TcType ( TcThetaType,
+import InstEnv ( InstLookupResult(..), lookupInstEnv )
+import TcType ( TcThetaType, TcClassContext,
TcType, TcTauType, TcTyVarSet,
- zonkTcTyVars, zonkTcType, zonkTcTypes,
- zonkTcThetaType
+ zonkTcType, zonkTcTypes,
+ zonkTcThetaType, tcInstTyVar, tcInstType
)
import CoreFVs ( idFreeTyVars )
-import Class ( Class, FunDep )
-import FunDeps ( instantiateFdClassTys )
-import Id ( Id, idType, mkUserLocal, mkSysLocal )
+import Class ( Class )
+import Id ( Id, idType, mkUserLocal, mkSysLocal, mkVanillaId )
import PrelInfo ( isStandardClass, isCcallishClass, isNoDictClass )
-import Name ( mkDictOcc, mkMethodOcc, mkIPOcc, getOccName, nameUnique )
+import Name ( mkDictOcc, mkMethodOcc, getOccName, mkLocalName )
+import NameSet ( NameSet )
import PprType ( pprPred )
import Type ( Type, PredType(..),
- isTyVarTy, mkDictTy, mkPredTy,
+ isTyVarTy, mkPredTy, mkTyVarTy, mkTyVarTys,
splitForAllTys, splitSigmaTy, funArgTy,
splitMethodTy, splitRhoTy, classesOfPreds,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
- tidyOpenType, tidyOpenTypes
+ tidyOpenType, tidyOpenTypes, predMentionsIPs
)
-import Subst ( emptyInScopeSet, mkSubst, mkInScopeSet,
+import Subst ( emptyInScopeSet, mkSubst,
substTy, substClasses, mkTyVarSubst, mkTopTyVarSubst
)
import Literal ( inIntRange )
import TysWiredIn ( isIntTy,
floatDataCon, isFloatTy,
doubleDataCon, isDoubleTy,
- isIntegerTy, voidTy
+ isIntegerTy
)
-import PrelNames( Unique, hasKey, fromIntName, fromIntegerClassOpKey )
-import Maybe ( catMaybes )
+import PrelNames( hasKey, fromIntName, fromIntegerClassOpKey )
import Util ( thenCmp, zipWithEqual, mapAccumL )
import Bag
import Outputable
\begin{code}
data Inst
= Dict
- Unique
+ Id
TcPredType
InstLoc
| Method
- Unique
+ Id
TcId -- The overloaded function
-- This function will be a global, local, or ClassOpId;
-- type of (f tys dicts(from theta)) = tau
| LitInst
- Unique
+ Id
RenamedHsOverLit -- The literal from the occurrence site
TcType -- The type at which the literal is used
InstLoc
-
- | FunDep
- Unique
- Class -- the class from which this arises
- [FunDep TcType]
- InstLoc
\end{code}
Ordering
cmpInst (Method _ _ _ _ _ _) other = LT
cmpInst (LitInst _ lit1 ty1 _) (LitInst _ lit2 ty2 _) = (lit1 `compare` lit2) `thenCmp` (ty1 `compare` ty2)
-cmpInst (LitInst _ _ _ _) (FunDep _ _ _ _) = LT
cmpInst (LitInst _ _ _ _) other = GT
-cmpInst (FunDep _ clas1 fds1 _) (FunDep _ clas2 fds2 _) = (clas1 `compare` clas2) `thenCmp` (fds1 `compare` fds2)
-cmpInst (FunDep _ _ _ _) other = GT
-
-- and they can only have HsInt or HsFracs in them.
\end{code}
Selection
~~~~~~~~~
\begin{code}
-instLoc (Dict u pred loc) = loc
-instLoc (Method u _ _ _ _ loc) = loc
-instLoc (LitInst u lit ty loc) = loc
-instLoc (FunDep _ _ _ loc) = loc
-
-getDictPred_maybe (Dict _ p _) = Just p
-getDictPred_maybe _ = Nothing
-
-getMethodTheta_maybe (Method _ _ _ theta _ _) = Just theta
-getMethodTheta_maybe _ = Nothing
-
-getDictClassTys (Dict u (Class clas tys) _) = (clas, tys)
-
-getFunDeps (FunDep _ clas fds _) = Just (clas, fds)
-getFunDeps _ = Nothing
+instToId :: Inst -> TcId
+instToId (Dict id _ _) = id
+instToId (Method id _ _ _ _ _) = id
+instToId (LitInst id _ _ _) = id
-getFunDepsOfLIE lie = catMaybes (map getFunDeps (lieToList lie))
+instLoc (Dict _ _ loc) = loc
+instLoc (Method _ _ _ _ _ loc) = loc
+instLoc (LitInst _ _ _ loc) = loc
-getIPsOfPred (IParam n ty) = [(n, ty)]
-getIPsOfPred _ = []
-getIPsOfTheta theta = concatMap getIPsOfPred theta
+getDictClassTys (Dict _ (Class clas tys) _) = (clas, tys)
-getIPs (Dict u (IParam n ty) loc) = [(n, ty)]
-getIPs (Method u id _ theta t loc) = getIPsOfTheta theta
-getIPs _ = []
+predsOfInsts :: [Inst] -> [PredType]
+predsOfInsts insts = concatMap predsOfInst insts
-getIPsOfLIE lie = concatMap getIPs (lieToList lie)
+predsOfInst (Dict _ pred _) = [pred]
+predsOfInst (Method _ _ _ theta _ _) = theta
+predsOfInst (LitInst _ _ _ _) = []
+ -- The last case is is really a big cheat
+ -- LitInsts to give rise to a (Num a) or (Fractional a) predicate
+ -- But Num and Fractional have only one parameter and no functional
+ -- dependencies, so I think no caller of predsOfInst will care.
-getAllFunDeps (FunDep _ clas fds _) = fds
-getAllFunDeps inst = map (\(n,ty) -> ([], [ty])) (getIPs inst)
+ipsOfPreds theta = [(n,ty) | IParam n ty <- theta]
-getAllFunDepsOfLIE lie = concat (map getAllFunDeps (lieToList lie))
+getIPs inst = ipsOfPreds (predsOfInst inst)
tyVarsOfInst :: Inst -> TcTyVarSet
+tyVarsOfInst (LitInst _ _ ty _) = tyVarsOfType ty
tyVarsOfInst (Dict _ pred _) = tyVarsOfPred pred
tyVarsOfInst (Method _ id tys _ _ _) = tyVarsOfTypes tys `unionVarSet` idFreeTyVars id
-- The id might have free type variables; in the case of
-- locally-overloaded class methods, for example
-tyVarsOfInst (LitInst _ _ ty _) = tyVarsOfType ty
-tyVarsOfInst (FunDep _ _ fds _)
- = foldr unionVarSet emptyVarSet (map tyVarsOfFd fds)
- where tyVarsOfFd (ts1, ts2) =
- tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2
-
-tyVarsOfInsts insts
- = foldr unionVarSet emptyVarSet (map tyVarsOfInst insts)
-tyVarsOfLIE lie
- = foldr unionVarSet emptyVarSet (map tyVarsOfInst insts)
- where insts = lieToList lie
+tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
+tyVarsOfLIE lie = tyVarsOfInsts (lieToList lie)
\end{code}
Predicates
isMethodFor ids (Method uniq id tys _ _ loc) = id `elemVarSet` ids
isMethodFor ids inst = False
+instMentionsIPs :: Inst -> NameSet -> Bool
+ -- True if the Inst mentions any of the implicit
+ -- parameters in the supplied set of names
+instMentionsIPs (Dict _ pred _) ip_names = pred `predMentionsIPs` ip_names
+instMentionsIPs (Method _ _ _ theta _ _) ip_names = any (`predMentionsIPs` ip_names) theta
+instMentionsIPs other ip_names = False
+
isTyVarDict :: Inst -> Bool
isTyVarDict (Dict _ (Class _ tys) _) = all isTyVarTy tys
isTyVarDict other = False
= isStandardClass clas && isTyVarTy ty
isStdClassTyVarDict other
= False
-
-notFunDep :: Inst -> Bool
-notFunDep (FunDep _ _ _ _) = False
-notFunDep other = True
\end{code}
Two predicates which deal with the case where class constraints don't
\end{code}
-Construction
-~~~~~~~~~~~~
+%************************************************************************
+%* *
+\subsection{Building dictionaries}
+%* *
+%************************************************************************
\begin{code}
newDicts :: InstOrigin
-> TcThetaType
- -> NF_TcM (LIE, [TcId])
+ -> NF_TcM [Inst]
newDicts orig theta
= tcGetInstLoc orig `thenNF_Tc` \ loc ->
- newDictsAtLoc loc theta `thenNF_Tc` \ (dicts, ids) ->
- returnNF_Tc (listToBag dicts, ids)
+ newDictsAtLoc loc theta
newClassDicts :: InstOrigin
- -> [(Class,[TcType])]
- -> NF_TcM (LIE, [TcId])
-newClassDicts orig theta
- = newDicts orig (map (uncurry Class) theta)
+ -> TcClassContext
+ -> NF_TcM [Inst]
+newClassDicts orig theta = newDicts orig (map (uncurry Class) theta)
+
+newDictsFromOld :: Inst -> TcClassContext -> NF_TcM [Inst]
+newDictsFromOld (Dict _ _ loc) theta = newDictsAtLoc loc (map (uncurry Class) theta)
-- Local function, similar to newDicts,
-- but with slightly different interface
newDictsAtLoc :: InstLoc
-> TcThetaType
- -> NF_TcM ([Inst], [TcId])
-newDictsAtLoc loc theta =
- tcGetUniques (length theta) `thenNF_Tc` \ new_uniqs ->
- let
- mk_dict u pred = Dict u pred loc
- dicts = zipWithEqual "newDictsAtLoc" mk_dict new_uniqs theta
- in
- returnNF_Tc (dicts, map instToId dicts)
+ -> NF_TcM [Inst]
+newDictsAtLoc inst_loc@(_,loc,_) theta
+ = tcGetUniques (length theta) `thenNF_Tc` \ new_uniqs ->
+ returnNF_Tc (zipWithEqual "newDictsAtLoc" mk_dict new_uniqs theta)
+ where
+ mk_dict uniq pred = Dict (mkVanillaId (mk_dict_name uniq pred) (mkPredTy pred)) pred inst_loc
+
+ mk_dict_name uniq (Class cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
+ mk_dict_name uniq (IParam name ty) = name
+
+newIPDict orig name ty
+ = tcGetInstLoc orig `thenNF_Tc` \ inst_loc ->
+ returnNF_Tc (Dict (mkVanillaId name ty) (IParam name ty) inst_loc)
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Building methods (calls of overloaded functions)}
+%* *
+%************************************************************************
+
+tcInstId instantiates an occurrence of an Id.
+The instantiate_it loop runs round instantiating the Id.
+It has to be a loop because we are now prepared to entertain
+types like
+ f:: forall a. Eq a => forall b. Baz b => tau
+We want to instantiate this to
+ f2::tau {f2 = f1 b (Baz b), f1 = f a (Eq a)}
+
+The -fno-method-sharing flag controls what happens so far as the LIE
+is concerned. The default case is that for an overloaded function we
+generate a "method" Id, and add the Method Inst to the LIE. So you get
+something like
+ f :: Num a => a -> a
+ f = /\a (d:Num a) -> let m = (+) a d in \ (x:a) -> m x x
+If you specify -fno-method-sharing, the dictionary application
+isn't shared, so we get
+ f :: Num a => a -> a
+ f = /\a (d:Num a) (x:a) -> (+) a d x x
+This gets a bit less sharing, but
+ a) it's better for RULEs involving overloaded functions
+ b) perhaps fewer separated lambdas
+
-newDictFromOld :: Inst -> Class -> [TcType] -> NF_TcM Inst
-newDictFromOld (Dict _ _ loc) clas tys
- = tcGetUnique `thenNF_Tc` \ uniq ->
- returnNF_Tc (Dict uniq (Class clas tys) loc)
+\begin{code}
+tcInstId :: Id -> NF_TcM (TcExpr, LIE, TcType)
+tcInstId fun
+ | opt_NoMethodSharing = loop_noshare (HsVar fun) (idType fun)
+ | otherwise = loop_share fun
+ where
+ orig = OccurrenceOf fun
+ loop_noshare fun fun_ty
+ = tcInstType fun_ty `thenNF_Tc` \ (tyvars, theta, tau) ->
+ let
+ ty_app = mkHsTyApp fun (mkTyVarTys tyvars)
+ in
+ if null theta then -- Is it overloaded?
+ returnNF_Tc (ty_app, emptyLIE, tau)
+ else
+ newDicts orig theta `thenNF_Tc` \ dicts ->
+ loop_noshare (mkHsDictApp ty_app (map instToId dicts)) tau `thenNF_Tc` \ (expr, lie, final_tau) ->
+ returnNF_Tc (expr, mkLIE dicts `plusLIE` lie, final_tau)
+
+ loop_share fun
+ = tcInstType (idType fun) `thenNF_Tc` \ (tyvars, theta, tau) ->
+ let
+ arg_tys = mkTyVarTys tyvars
+ in
+ if null theta then -- Is it overloaded?
+ returnNF_Tc (mkHsTyApp (HsVar fun) arg_tys, emptyLIE, tau)
+ else
+ -- Yes, it's overloaded
+ newMethodWithGivenTy orig fun arg_tys theta tau `thenNF_Tc` \ meth ->
+ loop_share (instToId meth) `thenNF_Tc` \ (expr, lie, final_tau) ->
+ returnNF_Tc (expr, unitLIE meth `plusLIE` lie, final_tau)
newMethod :: InstOrigin
-> TcId
-> [TcType]
- -> NF_TcM (LIE, TcId)
+ -> NF_TcM Inst
newMethod orig id tys
= -- Get the Id type and instantiate it at the specified types
let
(tyvars, rho) = splitForAllTys (idType id)
rho_ty = substTy (mkTyVarSubst tyvars tys) rho
- (pred, tau) = splitMethodTy rho_ty
+ (pred, tau) = splitMethodTy rho_ty
in
- newMethodWithGivenTy orig id tys [pred] tau `thenNF_Tc` \ meth_inst ->
- returnNF_Tc (unitLIE meth_inst, instToId meth_inst)
-
-instOverloadedFun orig v arg_tys theta tau
--- This is where we introduce new functional dependencies into the LIE
- = newMethodWithGivenTy orig v arg_tys theta tau `thenNF_Tc` \ inst ->
- instFunDeps orig theta `thenNF_Tc` \ fds ->
- returnNF_Tc (instToId inst, mkLIE (inst : fds))
-
-instFunDeps orig theta
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcGetInstLoc orig `thenNF_Tc` \ loc ->
- let ifd (Class clas tys) =
- let fds = instantiateFdClassTys clas tys in
- if null fds then Nothing else Just (FunDep uniq clas fds loc)
- ifd _ = Nothing
- in returnNF_Tc (catMaybes (map ifd theta))
-
-instFunDepsOfTheta theta
- = let ifd (Class clas tys) = instantiateFdClassTys clas tys
- ifd (IParam n ty) = [([], [ty])]
- in concat (map ifd theta)
+ newMethodWithGivenTy orig id tys [pred] tau
newMethodWithGivenTy orig id tys theta tau
= tcGetInstLoc orig `thenNF_Tc` \ loc ->
- newMethodWith id tys theta tau loc
+ newMethodWith loc id tys theta tau
-newMethodWith id tys theta tau loc
+newMethodWith inst_loc@(_,loc,_) id tys theta tau
= tcGetUnique `thenNF_Tc` \ new_uniq ->
- returnNF_Tc (Method new_uniq id tys theta tau loc)
+ let
+ meth_id = mkUserLocal (mkMethodOcc (getOccName id)) new_uniq tau loc
+ in
+ returnNF_Tc (Method meth_id id tys theta tau inst_loc)
newMethodAtLoc :: InstLoc
-> Id -> [TcType]
-> NF_TcM (Inst, TcId)
-newMethodAtLoc loc real_id tys -- Local function, similar to newMethod but with
- -- slightly different interface
+newMethodAtLoc inst_loc real_id tys
+ -- This actually builds the Inst
= -- Get the Id type and instantiate it at the specified types
- tcGetUnique `thenNF_Tc` \ new_uniq ->
let
(tyvars,rho) = splitForAllTys (idType real_id)
rho_ty = ASSERT( length tyvars == length tys )
substTy (mkTopTyVarSubst tyvars tys) rho
(theta, tau) = splitRhoTy rho_ty
- meth_inst = Method new_uniq real_id tys theta tau loc
in
+ newMethodWith inst_loc real_id tys theta tau `thenNF_Tc` \ meth_inst ->
returnNF_Tc (meth_inst, instToId meth_inst)
\end{code}
= tcGetInstLoc orig `thenNF_Tc` \ loc ->
tcGetUnique `thenNF_Tc` \ new_uniq ->
let
- lit_inst = LitInst new_uniq lit ty loc
+ lit_inst = LitInst lit_id lit ty loc
+ lit_id = mkSysLocal SLIT("lit") new_uniq ty
in
returnNF_Tc (HsVar (instToId lit_inst), unitLIE lit_inst)
\end{code}
-\begin{code}
-newFunDepFromDict dict
- | isClassDict dict
- = tcGetUnique `thenNF_Tc` \ uniq ->
- let (clas, tys) = getDictClassTys dict
- fds = instantiateFdClassTys clas tys
- inst = FunDep uniq clas fds (instLoc dict)
- in
- if null fds then returnNF_Tc Nothing else returnNF_Tc (Just inst)
- | otherwise
- = returnNF_Tc Nothing
-\end{code}
-
-\begin{code}
-newIPDict name ty loc
- = tcGetUnique `thenNF_Tc` \ new_uniq ->
- let d = Dict new_uniq (IParam name ty) loc in
- returnNF_Tc d
-\end{code}
-
-\begin{code}
-instToId :: Inst -> TcId
-instToId inst = instToIdBndr inst
-
-instToIdBndr :: Inst -> TcId
-instToIdBndr (Dict u (Class clas tys) (_,loc,_))
- = mkUserLocal (mkDictOcc (getOccName clas)) u (mkDictTy clas tys) loc
-instToIdBndr (Dict u (IParam n ty) (_,loc,_))
- = ipToId n ty loc
-
-instToIdBndr (Method u id tys theta tau (_,loc,_))
- = mkUserLocal (mkMethodOcc (getOccName id)) u tau loc
-
-instToIdBndr (LitInst u list ty loc)
- = mkSysLocal SLIT("lit") u ty
-
-instToIdBndr (FunDep u clas fds _)
- = mkSysLocal SLIT("FunDep") u voidTy
-
-ipToId n ty loc
- = mkUserLocal (mkIPOcc (getOccName n)) (nameUnique n) (mkPredTy (IParam n ty)) loc
-\end{code}
+%************************************************************************
+%* *
+\subsection{Zonking}
+%* *
+%************************************************************************
-Zonking
-~~~~~~~
Zonking makes sure that the instance types are fully zonked,
-but doesn't do the same for the Id in a Method. There's no
+but doesn't do the same for any of the Ids in an Inst. There's no
need, and it's a lot of extra work.
\begin{code}
returnNF_Tc (IParam n new_ty)
zonkInst :: Inst -> NF_TcM Inst
-zonkInst (Dict u pred loc)
+zonkInst (Dict id pred loc)
= zonkPred pred `thenNF_Tc` \ new_pred ->
- returnNF_Tc (Dict u new_pred loc)
+ returnNF_Tc (Dict id new_pred loc)
-zonkInst (Method u id tys theta tau loc)
+zonkInst (Method m id tys theta tau loc)
= zonkId id `thenNF_Tc` \ new_id ->
-- Essential to zonk the id in case it's a local variable
-- Can't use zonkIdOcc because the id might itself be
zonkTcTypes tys `thenNF_Tc` \ new_tys ->
zonkTcThetaType theta `thenNF_Tc` \ new_theta ->
zonkTcType tau `thenNF_Tc` \ new_tau ->
- returnNF_Tc (Method u new_id new_tys new_theta new_tau loc)
+ returnNF_Tc (Method m new_id new_tys new_theta new_tau loc)
-zonkInst (LitInst u lit ty loc)
+zonkInst (LitInst id lit ty loc)
= zonkTcType ty `thenNF_Tc` \ new_ty ->
- returnNF_Tc (LitInst u lit new_ty loc)
-
-zonkInst (FunDep u clas fds loc)
- = zonkFunDeps fds `thenNF_Tc` \ fds' ->
- returnNF_Tc (FunDep u clas fds' loc)
+ returnNF_Tc (LitInst id lit new_ty loc)
zonkInsts insts = mapNF_Tc zonkInst insts
-
-zonkFunDeps fds = mapNF_Tc zonkFd fds
- where
- zonkFd (ts1, ts2)
- = zonkTcTypes ts1 `thenNF_Tc` \ ts1' ->
- zonkTcTypes ts2 `thenNF_Tc` \ ts2' ->
- returnNF_Tc (ts1', ts2')
-
-zonkTvFunDeps fds = mapNF_Tc zonkFd fds
- where
- zonkFd (tvs1, tvs2)
- = zonkTcTyVars tvs1 `thenNF_Tc` \ tvs1' ->
- zonkTcTyVars tvs2 `thenNF_Tc` \ tvs2' ->
- returnNF_Tc (tvs1', tvs2')
\end{code}
-Printing
-~~~~~~~~
+%************************************************************************
+%* *
+\subsection{Printing}
+%* *
+%************************************************************************
+
ToDo: improve these pretty-printing things. The ``origin'' is really only
relevant in error messages.
show_uniq u,
ppr (instToId m) -}]
-pprInst (FunDep _ clas fds loc)
- = hsep [ppr clas, ppr fds]
-
tidyPred :: TidyEnv -> TcPredType -> (TidyEnv, TcPredType)
tidyPred env (Class clas tys)
= (env', Class clas tys')
where
(env', tys') = tidyOpenTypes env tys
--- this case shouldn't arise... (we never print fundeps)
-tidyInst env fd@(FunDep _ clas fds loc)
- = (env, fd)
-
tidyInsts env insts = mapAccumL tidyInst env insts
show_uniq u = ifPprDebug (text "{-" <> ppr u <> text "-}")
%************************************************************************
%* *
-\subsection[InstEnv-types]{Type declarations}
+\subsection{Looking up Insts}
%* *
%************************************************************************
FoundInst tenv dfun_id
-> let
- subst = mkSubst (mkInScopeSet (tyVarsOfTypes tys)) tenv
(tyvars, rho) = splitForAllTys (idType dfun_id)
- ty_args = map subst_tv tyvars
+ mk_ty_arg tv = case lookupSubstEnv tenv tv of
+ Just (DoneTy ty) -> returnNF_Tc ty
+ Nothing -> tcInstTyVar tv `thenNF_Tc` \ tc_tv ->
+ returnTc (mkTyVarTy tc_tv)
+ in
+ mapNF_Tc mk_ty_arg tyvars `thenNF_Tc` \ ty_args ->
+ let
+ subst = mkTyVarSubst tyvars ty_args
dfun_rho = substTy subst rho
(theta, _) = splitRhoTy dfun_rho
ty_app = mkHsTyApp (HsVar dfun_id) ty_args
- subst_tv tv = case lookupSubstEnv tenv tv of
- Just (DoneTy ty) -> ty
- -- tenv should bind all the tyvars
in
if null theta then
returnNF_Tc (SimpleInst ty_app)
else
- newDictsAtLoc loc theta `thenNF_Tc` \ (dicts, dict_ids) ->
+ newDictsAtLoc loc theta `thenNF_Tc` \ dicts ->
let
- rhs = mkHsDictApp ty_app dict_ids
+ rhs = mkHsDictApp ty_app (map instToId dicts)
in
returnNF_Tc (GenInst dicts rhs)
other -> returnNF_Tc NoInstance
+
lookupInst dict@(Dict _ _ loc) = returnNF_Tc NoInstance
-- Methods
lookupInst inst@(Method _ id tys theta _ loc)
- = newDictsAtLoc loc theta `thenNF_Tc` \ (dicts, dict_ids) ->
- returnNF_Tc (GenInst dicts (mkHsDictApp (mkHsTyApp (HsVar id) tys) dict_ids))
+ = newDictsAtLoc loc theta `thenNF_Tc` \ dicts ->
+ returnNF_Tc (GenInst dicts (mkHsDictApp (mkHsTyApp (HsVar id) tys) (map instToId dicts)))
-- Literals
float_lit = mkHsConApp floatDataCon [] [floatprim_lit]
doubleprim_lit = HsLit (HsDoublePrim f)
double_lit = mkHsConApp doubleDataCon [] [doubleprim_lit]
-
--- there are no `instances' of functional dependencies or implicit params
-
-lookupInst _ = returnNF_Tc NoInstance
-
\end{code}
There is a second, simpler interface, when you want an instance of a
import TcHsSyn ( TcMonoBinds, TcId, zonkId, mkHsLet )
import TcMonad
-import Inst ( LIE, emptyLIE, mkLIE, plusLIE, InstOrigin(..),
- newDicts, tyVarsOfInst, instToId,
- getAllFunDepsOfLIE, getIPsOfLIE, zonkFunDeps
+import Inst ( LIE, emptyLIE, mkLIE, plusLIE, lieToList, InstOrigin(..),
+ newDicts, tyVarsOfInsts, instToId
)
import TcEnv ( tcExtendLocalValEnv,
newSpecPragmaId, newLocalId,
- tcLookupTyCon,
- tcGetGlobalTyVars, tcExtendGlobalTyVars
+ tcGetGlobalTyVars
)
-import TcSimplify ( tcSimplify, tcSimplifyAndCheck, tcSimplifyToDicts )
-import TcImprove ( tcImprove )
+import TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyToDicts )
import TcMonoType ( tcHsSigType, checkSigTyVars,
TcSigInfo(..), tcTySig, maybeSig, sigCtxt
)
import TcPat ( tcPat )
import TcSimplify ( bindInstsOfLocalFuns )
-import TcType ( TcThetaType, newTyVarTy, newTyVar,
- zonkTcTypes, zonkTcThetaType, zonkTcTyVarToTyVar
+import TcType ( newTyVarTy, newTyVar, zonkTcTyVarsAndFV,
+ zonkTcTyVarToTyVar
)
import TcUnify ( unifyTauTy, unifyTauTyLists )
import IdInfo ( InlinePragInfo(..) )
import Name ( Name, getOccName, getSrcLoc )
import NameSet
-import Type ( mkTyVarTy, tyVarsOfTypes, mkTyConApp,
- mkForAllTys, mkFunTys,
+import Type ( mkTyVarTy,
+ mkForAllTys, mkFunTys, tyVarsOfType,
mkPredTy, mkForAllTy, isUnLiftedType,
unliftedTypeKind, liftedTypeKind, openTypeKind
)
-import FunDeps ( oclose )
import Var ( tyVarKind )
import VarSet
import Bag
import Util ( isIn )
import Maybes ( maybeToBool )
-import BasicTypes ( TopLevelFlag(..), RecFlag(..), isNotTopLevel )
+import BasicTypes ( TopLevelFlag(..), RecFlag(..), isNonRec, isNotTopLevel )
import FiniteMap ( listToFM, lookupFM )
-import PrelNames ( ioTyConName, mainKey, hasKey )
import Outputable
\end{code}
)
\end{code}
-An aside. The original version of @tcBindsAndThen@ which lacks a
-combiner function, appears below. Though it is perfectly well
-behaved, it cannot be typed by Haskell, because the recursive call is
-at a different type to the definition itself. There aren't too many
-examples of this, which is why I thought it worth preserving! [SLPJ]
-
-\begin{pseudocode}
-% tcBindsAndThen
-% :: RenamedHsBinds
-% -> TcM (thing, LIE, thing_ty))
-% -> TcM ((TcHsBinds, thing), LIE, thing_ty)
-%
-% tcBindsAndThen EmptyBinds do_next
-% = do_next `thenTc` \ (thing, lie, thing_ty) ->
-% returnTc ((EmptyBinds, thing), lie, thing_ty)
-%
-% tcBindsAndThen (ThenBinds binds1 binds2) do_next
-% = tcBindsAndThen binds1 (tcBindsAndThen binds2 do_next)
-% `thenTc` \ ((binds1', (binds2', thing')), lie1, thing_ty) ->
-%
-% returnTc ((binds1' `ThenBinds` binds2', thing'), lie1, thing_ty)
-%
-% tcBindsAndThen (MonoBind bind sigs is_rec) do_next
-% = tcBindAndThen bind sigs do_next
-\end{pseudocode}
-
%************************************************************************
%* *
Nothing -> mkVanillaId name forall_a_a -- No signature
in
returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
- ) $
+ ) $
-- TYPECHECK THE BINDINGS
tcMonoBinds mbind tc_ty_sigs is_rec `thenTc` \ (mbind', lie_req, binder_names, mono_ids) ->
-
- -- CHECK THAT THE SIGNATURES MATCH
- -- (must do this before getTyVarsToGen)
- checkSigMatch top_lvl binder_names mono_ids tc_ty_sigs `thenTc` \ maybe_sig_theta ->
-
- -- IMPROVE the LIE
- -- Force any unifications dictated by functional dependencies.
- -- Because unification may happen, it's important that this step
- -- come before:
- -- - computing vars over which to quantify
- -- - zonking the generalized type vars
- let lie_avail = case maybe_sig_theta of
- Nothing -> emptyLIE
- Just (_, la) -> la
- lie_avail_req = lie_avail `plusLIE` lie_req in
- tcImprove lie_avail_req `thenTc_`
-
- -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
- -- The tyvars_not_to_gen are free in the environment, and hence
- -- candidates for generalisation, but sometimes the monomorphism
- -- restriction means we can't generalise them nevertheless
- let
- mono_id_tys = map idType mono_ids
- in
- getTyVarsToGen is_unrestricted mono_id_tys lie_req `thenNF_Tc` \ (tyvars_not_to_gen, tyvars_to_gen) ->
-
- -- Finally, zonk the generalised type variables to real TyVars
- -- This commits any unbound kind variables to lifted kind
- -- I'm a little worried that such a kind variable might be
- -- free in the environment, but I don't think it's possible for
- -- this to happen when the type variable is not free in the envt
- -- (which it isn't). SLPJ Nov 98
- mapTc zonkTcTyVarToTyVar (varSetElems tyvars_to_gen) `thenTc` \ real_tyvars_to_gen_list ->
let
- real_tyvars_to_gen = mkVarSet real_tyvars_to_gen_list
- -- It's important that the final list
- -- (real_tyvars_to_gen and real_tyvars_to_gen_list) is fully
- -- zonked, *including boxity*, because they'll be included in the forall types of
- -- the polymorphic Ids, and instances of these Ids will be generated from them.
- --
- -- Also NB that tcSimplify takes zonked tyvars as its arg, hence we pass
- -- real_tyvars_to_gen
+ tau_tvs = varSetElems (foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids)
in
- -- SIMPLIFY THE LIE
- tcExtendGlobalTyVars tyvars_not_to_gen (
- let ips = getIPsOfLIE lie_avail_req in
- if null real_tyvars_to_gen_list && (null ips || not is_unrestricted) then
- -- No polymorphism, and no IPs, so no need to simplify context
- returnTc (lie_req, EmptyMonoBinds, [])
- else
- case maybe_sig_theta of
- Nothing ->
- -- No signatures, so just simplify the lie
- -- NB: no signatures => no polymorphic recursion, so no
- -- need to use lie_avail (which will be empty anyway)
- tcSimplify (text "tcBinds1" <+> ppr binder_names)
- real_tyvars_to_gen lie_req `thenTc` \ (lie_free, dict_binds, lie_bound) ->
- returnTc (lie_free, dict_binds, map instToId (bagToList lie_bound))
-
- Just (sig_theta, lie_avail) ->
- -- There are signatures, and their context is sig_theta
- -- Furthermore, lie_avail is an LIE containing the 'method insts'
- -- for the things bound here
-
- zonkTcThetaType sig_theta `thenNF_Tc` \ sig_theta' ->
- newDicts SignatureOrigin sig_theta' `thenNF_Tc` \ (dicts_sig, dict_ids) ->
- -- It's important that sig_theta is zonked, because
- -- dict_id is later used to form the type of the polymorphic thing,
- -- and forall-types must be zonked so far as their bound variables
- -- are concerned
-
- let
- -- The "givens" is the stuff available. We get that from
- -- the context of the type signature, BUT ALSO the lie_avail
- -- so that polymorphic recursion works right (see comments at end of fn)
- givens = dicts_sig `plusLIE` lie_avail
- in
-
- -- Check that the needed dicts can be expressed in
- -- terms of the signature ones
- tcAddErrCtxt (bindSigsCtxt tysig_names) $
- tcSimplifyAndCheck
- (ptext SLIT("type signature for") <+> pprQuotedList binder_names)
- real_tyvars_to_gen givens lie_req `thenTc` \ (lie_free, dict_binds) ->
-
- returnTc (lie_free, dict_binds, dict_ids)
-
- ) `thenTc` \ (lie_free, dict_binds, dicts_bound) ->
-
- -- GET THE FINAL MONO_ID_TYS
- zonkTcTypes mono_id_tys `thenNF_Tc` \ zonked_mono_id_types ->
-
-
- -- CHECK FOR BOGUS UNPOINTED BINDINGS
- (if any isUnLiftedType zonked_mono_id_types then
- -- Unlifted bindings must be non-recursive,
- -- not top level, and non-polymorphic
- checkTc (isNotTopLevel top_lvl)
- (unliftedBindErr "Top-level" mbind) `thenTc_`
- checkTc (case is_rec of {Recursive -> False; NonRecursive -> True})
- (unliftedBindErr "Recursive" mbind) `thenTc_`
- checkTc (null real_tyvars_to_gen_list)
- (unliftedBindErr "Polymorphic" mbind)
- else
- returnTc ()
- ) `thenTc_`
+ -- GENERALISE
+ generalise binder_names mbind tau_tvs lie_req tc_ty_sigs
+ `thenTc` \ (tc_tyvars_to_gen, lie_free, dict_binds, dict_ids) ->
- ASSERT( not (any ((== unliftedTypeKind) . tyVarKind) real_tyvars_to_gen_list) )
- -- The instCantBeGeneralised stuff in tcSimplify should have
- -- already raised an error if we're trying to generalise an
- -- unlifted tyvar (NB: unlifted tyvars are always introduced
- -- along with a class constraint) and it's better done there
- -- because we have more precise origin information.
- -- That's why we just use an ASSERT here.
+ -- ZONK THE GENERALISED TYPE VARIABLES TO REAL TyVars
+ -- This commits any unbound kind variables to boxed kind, by unification
+ -- It's important that the final quanfified type variables
+ -- are fully zonked, *including boxity*, because they'll be
+ -- included in the forall types of the polymorphic Ids.
+ -- At calls of these Ids we'll instantiate fresh type variables from
+ -- them, and we use their boxity then.
+ mapNF_Tc zonkTcTyVarToTyVar tc_tyvars_to_gen `thenNF_Tc` \ real_tyvars_to_gen ->
- -- BUILD THE POLYMORPHIC RESULT IDs
- mapNF_Tc zonkId mono_ids `thenNF_Tc` \ zonked_mono_ids ->
+ -- ZONK THE Ids
+ -- It's important that the dict Ids are zonked, including the boxity set
+ -- in the previous step, because they are later used to form the type of
+ -- the polymorphic thing, and forall-types must be zonked so far as
+ -- their bound variables are concerned
+ mapNF_Tc zonkId dict_ids `thenNF_Tc` \ zonked_dict_ids ->
+ mapNF_Tc zonkId mono_ids `thenNF_Tc` \ zonked_mono_ids ->
+
+ -- CHECK FOR BOGUS UNLIFTED BINDINGS
+ checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids `thenTc_`
+
+ -- BUILD THE POLYMORPHIC RESULT IDs
let
exports = zipWith mk_export binder_names zonked_mono_ids
- dict_tys = map idType dicts_bound
+ dict_tys = map idType zonked_dict_ids
inlines = mkNameSet [name | InlineSig name _ loc <- inline_sigs]
no_inlines = listToFM ([(name, IMustNotBeINLINEd False phase) | NoInlineSig name phase loc <- inline_sigs] ++
case maybeSig tc_ty_sigs binder_name of
Just (TySigInfo _ sig_poly_id sig_tyvars _ _ _ _ _) ->
(sig_tyvars, sig_poly_id)
- Nothing -> (real_tyvars_to_gen_list, new_poly_id)
+ Nothing -> (real_tyvars_to_gen, new_poly_id)
new_poly_id = mkVanillaId binder_name poly_ty
- poly_ty = mkForAllTys real_tyvars_to_gen_list
+ poly_ty = mkForAllTys real_tyvars_to_gen
$ mkFunTys dict_tys
- $ idType (zonked_mono_id)
+ $ idType zonked_mono_id
-- It's important to build a fully-zonked poly_ty, because
-- we'll slurp out its free type variables when extending the
-- local environment (tcExtendLocalValEnv); if it's not zonked
-- it appears to have free tyvars that aren't actually free
-- at all.
-
- pat_binders :: [Name]
- pat_binders = collectMonoBinders (justPatBindings mbind EmptyMonoBinds)
in
- -- CHECK FOR UNLIFTED BINDERS IN PATTERN BINDINGS
- mapTc (\id -> checkTc (not (idName id `elem` pat_binders
- && isUnLiftedType (idType id)))
- (unliftedPatBindErr id)) zonked_mono_ids
- `thenTc_`
-- BUILD RESULTS
returnTc (
- -- pprTrace "binding.." (ppr ((dicts_bound, dict_binds), exports, [idType poly_id | (_, poly_id, _) <- exports])) $
- AbsBinds real_tyvars_to_gen_list
- dicts_bound
- exports
- inlines
- (dict_binds `andMonoBinds` mbind'),
- lie_free,
- [poly_id | (_, poly_id, _) <- exports]
+ -- pprTrace "binding.." (ppr ((zonked_dict_ids, dict_binds),
+ -- exports, [idType poly_id | (_, poly_id, _) <- exports])) $
+ AbsBinds real_tyvars_to_gen
+ zonked_dict_ids
+ exports
+ inlines
+ (dict_binds `andMonoBinds` mbind'),
+ lie_free,
+ [poly_id | (_, poly_id, _) <- exports]
)
- where
- tysig_names = [name | (TySigInfo name _ _ _ _ _ _ _) <- tc_ty_sigs]
- is_unrestricted | opt_NoMonomorphismRestriction = True
- | otherwise = isUnRestrictedGroup tysig_names mbind
-
-justPatBindings bind@(PatMonoBind _ _ _) binds = bind `andMonoBinds` binds
-justPatBindings (AndMonoBinds b1 b2) binds =
- justPatBindings b1 (justPatBindings b2 binds)
-justPatBindings other_bind binds = binds
attachNoInlinePrag no_inlines bndr
= case lookupFM no_inlines (idName bndr) of
Just prag -> bndr `setInlinePragma` prag
Nothing -> bndr
+
+checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids
+ = ASSERT( not (any ((== unliftedTypeKind) . tyVarKind) real_tyvars_to_gen) )
+ -- The instCantBeGeneralised stuff in tcSimplify should have
+ -- already raised an error if we're trying to generalise an
+ -- unboxed tyvar (NB: unboxed tyvars are always introduced
+ -- along with a class constraint) and it's better done there
+ -- because we have more precise origin information.
+ -- That's why we just use an ASSERT here.
+
+ -- Check that pattern-bound variables are not unlifted
+ (if or [ (idName id `elem` pat_binders) && isUnLiftedType (idType id)
+ | id <- zonked_mono_ids ] then
+ addErrTc (unliftedBindErr "Pattern" mbind)
+ else
+ returnTc ()
+ ) `thenTc_`
+
+ -- Unlifted bindings must be non-recursive,
+ -- not top level, non-polymorphic, and not pattern bound
+ if any (isUnLiftedType . idType) zonked_mono_ids then
+ checkTc (isNotTopLevel top_lvl)
+ (unliftedBindErr "Top-level" mbind) `thenTc_`
+ checkTc (isNonRec is_rec)
+ (unliftedBindErr "Recursive" mbind) `thenTc_`
+ checkTc (null real_tyvars_to_gen)
+ (unliftedBindErr "Polymorphic" mbind)
+ else
+ returnTc ()
+
+ where
+ pat_binders :: [Name]
+ pat_binders = collectMonoBinders (justPatBindings mbind EmptyMonoBinds)
+
+ justPatBindings bind@(PatMonoBind _ _ _) binds = bind `andMonoBinds` binds
+ justPatBindings (AndMonoBinds b1 b2) binds =
+ justPatBindings b1 (justPatBindings b2 binds)
+ justPatBindings other_bind binds = binds
\end{code}
+
Polymorphic recursion
~~~~~~~~~~~~~~~~~~~~~
The game plan for polymorphic recursion in the code above is
%* *
%************************************************************************
+\begin{code}
+generalise binder_names mbind tau_tvs lie_req sigs
+
+-----------------------
+ | is_unrestricted && null sigs
+ = -- INFERENCE CASE: Unrestricted group, no type signatures
+ tcSimplifyInfer (ptext SLIT("bindings for") <+> pprBinders binder_names)
+ tau_tvs lie_req
+
+-----------------------
+ | is_unrestricted
+ = -- CHECKING CASE: Unrestricted group, there are type signatures
+ -- Check signature contexts are empty
+ checkSigsCtxts sigs `thenTc` \ (sig_avails, sig_dicts) ->
+
+ -- Check that the needed dicts can be
+ -- expressed in terms of the signature ones
+ tcSimplifyInferCheck check_doc tau_tvs sig_avails lie_req `thenTc` \ (forall_tvs, lie_free, dict_binds) ->
+
+ -- Check that signature type variables are OK
+ checkSigsTyVars sigs `thenTc_`
+
+ returnTc (forall_tvs, lie_free, dict_binds, sig_dicts)
+
+-----------------------
+ | otherwise -- RESTRICTED CASE: Restricted group
+ = -- Check signature contexts are empty
+ (if null sigs then
+ returnTc ()
+ else
+ checkSigsCtxts sigs `thenTc` \ (_, sig_dicts) ->
+ checkTc (null sig_dicts)
+ (restrictedBindCtxtErr binder_names)
+ ) `thenTc_`
+
+ -- Identify constrained tyvars
+ tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
+ zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
+ zonkTcTyVarsAndFV lie_tvs `thenNF_Tc` \ lie_tvs' ->
+ let
+ forall_tvs = tau_tvs' `minusVarSet` (lie_tvs' `unionVarSet` gbl_tvs)
+ -- Don't bother to oclose the gbl_tvs; this is a rare case
+ in
+ returnTc (varSetElems forall_tvs, lie_req, EmptyMonoBinds, [])
+
+ where
+ tysig_names = [name | (TySigInfo name _ _ _ _ _ _ _) <- sigs]
+ is_unrestricted | opt_NoMonomorphismRestriction = True
+ | otherwise = isUnRestrictedGroup tysig_names mbind
+ lie_tvs = varSetElems (tyVarsOfInsts (lieToList lie_req))
+ check_doc = case tysig_names of
+ [n] -> ptext SLIT("type signature for") <+> quotes (ppr n)
+ other -> ptext SLIT("type signature(s) for") <+> pprBinders tysig_names
+
+
+ -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
+ -- The type signatures on a mutually-recursive group of definitions
+ -- must all have the same context (or none).
+ --
+ -- We unify them because, with polymorphic recursion, their types
+ -- might not otherwise be related. This is a rather subtle issue.
+ -- ToDo: amplify
+ --
+ -- We return a representative
+checkSigsCtxts sigs@(TySigInfo _ id1 sig_tvs theta1 _ _ _ _ : other_sigs)
+ = mapTc_ check_one other_sigs `thenTc_`
+ if null theta1 then
+ returnTc ([], []) -- Non-overloaded type signatures
+ else
+ newDicts SignatureOrigin theta1 `thenNF_Tc` \ sig_dicts ->
+ let
+ -- The "sig_avails" is the stuff available. We get that from
+ -- the context of the type signature, BUT ALSO the lie_avail
+ -- so that polymorphic recursion works right (see comments at end of fn)
+ sig_avails = sig_dicts ++ sig_meths
+ in
+ returnTc (sig_avails, map instToId sig_dicts)
+ where
+ sig1_dict_tys = map mkPredTy theta1
+ n_sig1_theta = length theta1
+ sig_meths = concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs]
+
+ check_one sig@(TySigInfo _ id _ theta _ _ _ src_loc)
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxt (sigContextsCtxt id1 id) $
+ checkTc (length theta == n_sig1_theta) sigContextsErr `thenTc_`
+ unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
+
+checkSigsTyVars sigs = mapTc_ check_one sigs
+ where
+ check_one (TySigInfo _ id sig_tyvars sig_theta sig_tau _ _ src_loc)
+ = tcAddSrcLoc src_loc $
+ tcAddErrCtxtM (sigCtxt (sig_msg id) sig_tyvars sig_theta sig_tau) $
+ checkSigTyVars sig_tyvars (idFreeTyVars id)
+
+ sig_msg id = ptext SLIT("When checking the type signature for") <+> quotes (ppr id)
+\end{code}
+
@getTyVarsToGen@ decides what type variables to generalise over.
For a "restricted group" -- see the monomorphism restriction
Another, more common, example is when there's a Method inst in
the LIE, whose type might very well involve non-overloaded
type variables.
+ [NOTE: Jan 2001: I don't understand the problem here so I'm doing
+ the simple thing instead]
(b) On the other hand, we mustn't generalise tyvars which are constrained,
because we are going to pass on out the unmodified LIE, with those
find which tyvars are constrained.
\begin{code}
-getTyVarsToGen is_unrestricted mono_id_tys lie
- = tcGetGlobalTyVars `thenNF_Tc` \ free_tyvars ->
- zonkTcTypes mono_id_tys `thenNF_Tc` \ zonked_mono_id_tys ->
- let
- body_tyvars = tyVarsOfTypes zonked_mono_id_tys `minusVarSet` free_tyvars
- fds = getAllFunDepsOfLIE lie
- in
- if is_unrestricted
- then
- -- We need to augment the type variables that appear explicitly in
- -- the type by those that are determined by the functional dependencies.
- -- e.g. suppose our type is C a b => a -> a
- -- with the fun-dep a->b
- -- Then we should generalise over b too; otherwise it will be
- -- reported as ambiguous.
- zonkFunDeps fds `thenNF_Tc` \ fds' ->
- let
- extended_tyvars = oclose fds' body_tyvars
- in
- returnNF_Tc (emptyVarSet, extended_tyvars)
- else
- -- This recover and discard-errs is to avoid duplicate error
- -- messages; this, after all, is an "extra" call to tcSimplify
- recoverNF_Tc (returnNF_Tc (emptyVarSet, body_tyvars)) $
- discardErrsTc $
-
- tcSimplify (text "getTVG") body_tyvars lie `thenTc` \ (_, _, constrained_dicts) ->
- let
- -- ASSERT: dicts_sig is already zonked!
- constrained_tyvars = foldrBag (unionVarSet . tyVarsOfInst) emptyVarSet constrained_dicts
- reduced_tyvars_to_gen = body_tyvars `minusVarSet` constrained_tyvars
- in
- returnTc (constrained_tyvars, reduced_tyvars_to_gen)
-\end{code}
-
-
-\begin{code}
isUnRestrictedGroup :: [Name] -- Signatures given for these
-> RenamedMonoBinds
-> Bool
-> TcM (TcMonoBinds,
LIE, -- LIE required
[Name], -- Bound names
- [TcId]) -- Corresponding monomorphic bound things
+ [TcId]) -- Corresponding monomorphic bound things
tcMonoBinds mbinds tc_ty_sigs is_rec
= tc_mb_pats mbinds `thenTc` \ (complete_it, lie_req_pat, tvs, ids, lie_avail) ->
returnTc (mbinds', lie_req_pat `plusLIE` lie_req_rhss, names, mono_ids)
where
- -- This function is used when dealing with a LHS binder; we make a monomorphic
- -- version of the Id. We check for type signatures
+ -- This function is used when dealing with a LHS binder;
+ -- we make a monomorphic version of the Id.
+ -- We check for a type signature; if there is one, we use the mono_id
+ -- from the signature. This is how we make sure the tau part of the
+ -- signature actually maatches the type of the LHS; then tc_mb_pats
+ -- ensures the LHS and RHS have the same type
+
tc_pat_bndr name pat_ty
= case maybeSig tc_ty_sigs name of
Nothing
-> newLocalId (getOccName name) pat_ty (getSrcLoc name)
Just (TySigInfo _ _ _ _ _ mono_id _ _)
- -> tcAddSrcLoc (getSrcLoc name) $
+ -> tcAddSrcLoc (getSrcLoc name) $
unifyTauTy (idType mono_id) pat_ty `thenTc_`
returnTc mono_id
NonRecursive -> openTypeKind -- Non-recursive, so we permit unlifted types
\end{code}
-%************************************************************************
-%* *
-\subsection{Signatures}
-%* *
-%************************************************************************
-
-@checkSigMatch@ does the next step in checking signature matching.
-The tau-type part has already been unified. What we do here is to
-check that this unification has not over-constrained the (polymorphic)
-type variables of the original signature type.
-
-The error message here is somewhat unsatisfactory, but it'll do for
-now (ToDo).
-
-\begin{code}
-checkSigMatch :: TopLevelFlag -> [Name] -> [TcId] -> [TcSigInfo] -> TcM (Maybe (TcThetaType, LIE))
-checkSigMatch top_lvl binder_names mono_ids sigs
- | main_bound_here
- = -- First unify the main_id with IO t, for any old t
- tcSetErrCtxt mainTyCheckCtxt (
- tcLookupTyCon ioTyConName `thenTc` \ ioTyCon ->
- newTyVarTy liftedTypeKind `thenNF_Tc` \ t_tv ->
- unifyTauTy ((mkTyConApp ioTyCon [t_tv]))
- (idType main_mono_id)
- ) `thenTc_`
-
- -- Now check the signatures
- -- Must do this after the unification with IO t,
- -- in case of a silly signature like
- -- main :: forall a. a
- -- The unification to IO t will bind the type variable 'a',
- -- which is just waht check_one_sig looks for
- mapTc check_one_sig sigs `thenTc_`
- mapTc check_main_ctxt sigs `thenTc_`
- returnTc (Just ([], emptyLIE))
-
- | not (null sigs)
- = mapTc check_one_sig sigs `thenTc_`
- mapTc check_one_ctxt all_sigs_but_first `thenTc_`
- returnTc (Just (theta1, sig_lie))
-
- | otherwise
- = returnTc Nothing -- No constraints from type sigs
-
- where
- (TySigInfo _ id1 _ theta1 _ _ _ _ : all_sigs_but_first) = sigs
-
- sig1_dict_tys = mk_dict_tys theta1
- n_sig1_dict_tys = length sig1_dict_tys
- sig_lie = mkLIE (concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs])
-
- maybe_main = find_main top_lvl binder_names mono_ids
- main_bound_here = maybeToBool maybe_main
- Just main_mono_id = maybe_main
-
- -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
- -- Doesn't affect substitution
- check_one_sig (TySigInfo _ id sig_tyvars sig_theta sig_tau _ _ src_loc)
- = tcAddSrcLoc src_loc $
- tcAddErrCtxtM (sigCtxt (sig_msg id) sig_tyvars sig_theta sig_tau) $
- checkSigTyVars sig_tyvars (idFreeTyVars id)
-
-
- -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
- -- The type signatures on a mutually-recursive group of definitions
- -- must all have the same context (or none).
- --
- -- We unify them because, with polymorphic recursion, their types
- -- might not otherwise be related. This is a rather subtle issue.
- -- ToDo: amplify
- check_one_ctxt sig@(TySigInfo _ id _ theta _ _ _ src_loc)
- = tcAddSrcLoc src_loc $
- tcAddErrCtxt (sigContextsCtxt id1 id) $
- checkTc (length this_sig_dict_tys == n_sig1_dict_tys)
- sigContextsErr `thenTc_`
- unifyTauTyLists sig1_dict_tys this_sig_dict_tys
- where
- this_sig_dict_tys = mk_dict_tys theta
-
- -- CHECK THAT FOR A GROUP INVOLVING Main.main, all
- -- the signature contexts are empty (what a bore)
- check_main_ctxt sig@(TySigInfo _ id _ theta _ _ _ src_loc)
- = tcAddSrcLoc src_loc $
- checkTc (null theta) (mainContextsErr id)
-
- mk_dict_tys theta = map mkPredTy theta
-
- sig_msg id = ptext SLIT("When checking the type signature for") <+> quotes (ppr id)
-
- -- Search for Main.main in the binder_names, return corresponding mono_id
- find_main NotTopLevel binder_names mono_ids = Nothing
- find_main TopLevel binder_names mono_ids = go binder_names mono_ids
- go [] [] = Nothing
- go (n:ns) (m:ms) | n `hasKey` mainKey = Just m
- | otherwise = go ns ms
-\end{code}
-
%************************************************************************
%* *
tcExpr (HsVar name) sig_ty `thenTc` \ (spec_expr, spec_lie) ->
-- Squeeze out any Methods (see comments with tcSimplifyToDicts)
- tcSimplifyToDicts spec_lie `thenTc` \ (spec_lie1, spec_binds) ->
+ tcSimplifyToDicts spec_lie `thenTc` \ (spec_dicts, spec_binds) ->
-- Just specialise "f" by building a SpecPragmaId binding
-- It is the thing that makes sure we don't prematurely
-- Do the rest and combine
tcSpecSigs sigs `thenTc` \ (binds_rest, lie_rest) ->
returnTc (binds_rest `andMonoBinds` VarMonoBind spec_id (mkHsLet spec_binds spec_expr),
- lie_rest `plusLIE` spec_lie1)
+ lie_rest `plusLIE` mkLIE spec_dicts)
tcSpecSigs (other_sig : sigs) = tcSpecSigs sigs
tcSpecSigs [] = returnTc (EmptyMonoBinds, emptyLIE)
nest 4 (ppr v <+> dcolon <+> ppr ty)]
-----------------------------------------------
-unliftedPatBindErr id
- = ptext SLIT("variable in a lazy pattern binding has unlifted type: ")
- <+> quotes (ppr id)
-
------------------------------------------------
-bindSigsCtxt ids
- = ptext SLIT("When checking the type signature(s) for") <+> pprQuotedList ids
-
------------------------------------------------
-sigContextsErr
- = ptext SLIT("Mismatched contexts")
+sigContextsErr = ptext SLIT("Mismatched contexts")
sigContextsCtxt s1 s2
= hang (hsep [ptext SLIT("When matching the contexts of the signatures for"),
quotes (ppr s1), ptext SLIT("and"), quotes (ppr s2)])
4 (ptext SLIT("(the signature contexts in a mutually recursive group should all be identical)"))
-mainContextsErr id
- | id `hasKey` mainKey = ptext SLIT("Main.main cannot be overloaded")
- | otherwise
- = quotes (ppr id) <+> ptext SLIT("cannot be overloaded") <> char ',' <> -- sigh; workaround for cpp's inability to deal
- ptext SLIT("because it is mutually recursive with Main.main") -- with commas inside SLIT strings.
-
-mainTyCheckCtxt
- = hsep [ptext SLIT("When checking that"), quotes (ptext SLIT("main")),
- ptext SLIT("has the required type")]
-
-----------------------------------------------
unliftedBindErr flavour mbind
= hang (text flavour <+> ptext SLIT("bindings for unlifted types aren't allowed:"))
4 (ppr mbind)
+-----------------------------------------------
existentialExplode mbinds
= hang (vcat [text "My brain just exploded.",
text "I can't handle pattern bindings for existentially-quantified constructors.",
text "In the binding group"])
4 (ppr mbinds)
+
+-----------------------------------------------
+restrictedBindCtxtErr binder_names
+ = hang (ptext SLIT("Illegal overloaded type signature(s)"))
+ 4 (vcat [ptext SLIT("in a binding group for") <+> pprBinders binder_names,
+ ptext SLIT("that falls under the monomorphism restriction")])
+
+-- Used in error messages
+pprBinders bndrs = braces (pprWithCommas ppr bndrs)
\end{code}
)
import TcHsSyn ( TcMonoBinds )
-import Inst ( InstOrigin(..), LIE, emptyLIE, plusLIE, plusLIEs,
- newDicts, newMethod )
+import Inst ( Inst, InstOrigin(..), LIE, emptyLIE, plusLIE, plusLIEs,
+ instToId, newDicts, newMethod )
import TcEnv ( TcId, TcEnv, RecTcEnv, TyThingDetails(..), tcAddImportedIdInfo,
tcLookupClass, tcExtendTyVarEnvForMeths, tcExtendGlobalTyVars,
tcExtendLocalValEnv, tcExtendTyVarEnv
)
import TcBinds ( tcBindWithSigs, tcSpecSigs )
import TcMonoType ( tcHsRecType, tcRecClassContext, checkSigTyVars, checkAmbiguity, sigCtxt, mkTcSig )
-import TcSimplify ( tcSimplifyAndCheck, bindInstsOfLocalFuns )
-import TcType ( TcType, TcTyVar, tcInstTyVars, zonkTcSigTyVars )
+import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
+import TcType ( TcType, TcTyVar, tcInstTyVars )
import TcMonad
import Generics ( mkGenericRhs, validGenericMethodType )
import PrelInfo ( nO_METHOD_BINDING_ERROR_ID )
let
theta = [(mkClassPred clas inst_tys)]
in
- newDicts origin theta `thenNF_Tc` \ (this_dict, [this_dict_id]) ->
+ newDicts origin theta `thenNF_Tc` \ [this_dict] ->
tcExtendTyVarEnvForMeths tyvars clas_tyvars (
tcMethodBind clas origin clas_tyvars inst_tys theta
binds_in prags False op_item
- ) `thenTc` \ (defm_bind, insts_needed, (_, local_dm_id)) ->
+ ) `thenTc` \ (defm_bind, insts_needed, local_dm_inst) ->
tcAddErrCtxt (defltMethCtxt clas) $
- -- tcMethodBind has checked that the class_tyvars havn't
- -- been unified with each other or another type, but we must
- -- still zonk them before passing them to tcSimplifyAndCheck
- zonkTcSigTyVars clas_tyvars `thenNF_Tc` \ clas_tyvars' ->
-
-- Check the context
- tcSimplifyAndCheck
+ tcSimplifyCheck
(ptext SLIT("class") <+> ppr clas)
- (mkVarSet clas_tyvars')
- this_dict
- insts_needed `thenTc` \ (const_lie, dict_binds) ->
+ clas_tyvars
+ [this_dict]
+ insts_needed `thenTc` \ (const_lie, dict_binds) ->
+
+ -- Simplification can do unification
+ checkSigTyVars clas_tyvars emptyVarSet `thenTc` \ clas_tyvars' ->
let
full_bind = AbsBinds
clas_tyvars'
- [this_dict_id]
- [(clas_tyvars', dm_id, local_dm_id)]
+ [instToId this_dict]
+ [(clas_tyvars', dm_id, instToId local_dm_inst)]
emptyNameSet -- No inlines (yet)
(dict_binds `andMonoBinds` defm_bind)
in
-> [RenamedSig] -- Pramgas (just for this one)
-> Bool -- True <=> This method is from an instance declaration
-> ClassOpItem -- The method selector and default-method Id
- -> TcM (TcMonoBinds, LIE, (LIE, TcId))
+ -> TcM (TcMonoBinds, LIE, Inst)
tcMethodBind clas origin inst_tyvars inst_tys inst_theta
meth_binds prags is_inst_decl (sel_id, dm_info)
= tcGetSrcLoc `thenNF_Tc` \ loc ->
- newMethod origin sel_id inst_tys `thenNF_Tc` \ meth@(_, meth_id) ->
- mkTcSig meth_id loc `thenNF_Tc` \ sig_info ->
+ newMethod origin sel_id inst_tys `thenNF_Tc` \ meth ->
let
+ meth_id = instToId meth
meth_name = idName meth_id
sig_msg = ptext SLIT("When checking the expected type for class method") <+> ppr sel_id
meth_prags = find_prags (idName sel_id) meth_name prags
in
+ mkTcSig meth_id loc `thenNF_Tc` \ sig_info ->
+
-- Figure out what method binding to use
-- If the user suppplied one, use it, else construct a default one
(case find_bind (idName sel_id) meth_name meth_binds of
tcLookupGlobal_maybe, tcLookupGlobal,
-- Local environment
- tcExtendKindEnv,
+ tcExtendKindEnv, tcLookupLocalIds,
tcExtendTyVarEnv, tcExtendTyVarEnvForMeths,
- tcExtendLocalValEnv, tcLookup,
+ tcExtendLocalValEnv, tcLookup, tcLookup_maybe,
-- Global type variables
tcGetGlobalTyVars, tcExtendGlobalTyVars,
-- Random useful things
- RecTcEnv, tcAddImportedIdInfo, tcLookupRecId, tcLookupRecId_maybe, tcInstId,
+ RecTcEnv, tcAddImportedIdInfo, tcLookupRecId, tcLookupRecId_maybe,
-- New Ids
newLocalId, newSpecPragmaId,
import RnHsSyn ( RenamedMonoBinds, RenamedSig )
import TcMonad
-import TcType ( TcKind, TcType, TcTyVar, TcTyVarSet, TcThetaType,
- tcInstTyVars, zonkTcTyVars,
+import TcType ( TcKind, TcType, TcTyVar, TcTyVarSet,
+ zonkTcTyVarsAndFV
)
import Id ( idName, mkUserLocal, isDataConWrapId_maybe )
import IdInfo ( constantIdInfo )
import VarSet
import Type ( Type,
tyVarsOfTypes, splitDFunTy,
- splitForAllTys, splitRhoTy,
getDFunTyKey, tyConAppTyCon
)
import DataCon ( DataCon )
import TyCon ( TyCon )
import Class ( Class, ClassOpItem, ClassContext )
-import Subst ( substTy )
import Name ( Name, OccName, NamedThing(..),
nameOccName, getSrcLoc, mkLocalName,
isLocalName, nameModule_maybe
%************************************************************************
%* *
-\subsection{Random useful functions}
-%* *
-%************************************************************************
-
-
-\begin{code}
--- A useful function that takes an occurrence of a global thing
--- and instantiates its type with fresh type variables
-tcInstId :: Id
- -> NF_TcM ([TcTyVar], -- It's instantiated type
- TcThetaType, --
- TcType) --
-tcInstId id
- = let
- (tyvars, rho) = splitForAllTys (idType id)
- in
- tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
- let
- rho' = substTy tenv rho
- (theta', tau') = splitRhoTy rho'
- in
- returnNF_Tc (tyvars', theta', tau')
-\end{code}
-
-
-%************************************************************************
-%* *
\subsection{Making new Ids}
%* *
%************************************************************************
tcLookupGlobalId name
= tcLookupGlobal_maybe name `thenNF_Tc` \ maybe_id ->
case maybe_id of
- Just (AnId clas) -> returnNF_Tc clas
- other -> notFound "tcLookupGlobalId" name
+ Just (AnId id) -> returnNF_Tc id
+ other -> notFound "tcLookupGlobalId" name
tcLookupDataCon :: Name -> TcM DataCon
tcLookupDataCon con_name
case maybe_tc of
Just (ATyCon tc) -> returnNF_Tc tc
other -> notFound "tcLookupTyCon" name
+
+tcLookupLocalIds :: [Name] -> NF_TcM [TcId]
+tcLookupLocalIds ns
+ = tcGetEnv `thenNF_Tc` \ env ->
+ returnNF_Tc (map (lookup (tcLEnv env)) ns)
+ where
+ lookup lenv name = case lookupNameEnv lenv name of
+ Just (ATcId id) -> id
+ other -> pprPanic "tcLookupLocalIds" (ppr name)
\end{code}
tcGetGlobalTyVars :: NF_TcM TcTyVarSet
tcGetGlobalTyVars
= tcGetEnv `thenNF_Tc` \ (TcEnv {tcTyVars = gtv_var}) ->
- tcReadMutVar gtv_var `thenNF_Tc` \ global_tvs ->
- zonkTcTyVars (varSetElems global_tvs) `thenNF_Tc` \ global_tys' ->
- let
- global_tvs' = (tyVarsOfTypes global_tys')
- in
- tcWriteMutVar gtv_var global_tvs' `thenNF_Tc_`
- returnNF_Tc global_tvs'
+ tcReadMutVar gtv_var `thenNF_Tc` \ gbl_tvs ->
+ zonkTcTyVarsAndFV (varSetElems gbl_tvs) `thenNF_Tc` \ gbl_tvs' ->
+ tcWriteMutVar gtv_var gbl_tvs' `thenNF_Tc_`
+ returnNF_Tc gbl_tvs'
\end{code}
#include "HsVersions.h"
import HsSyn ( HsExpr(..), HsLit(..), ArithSeqInfo(..),
- MonoBinds(..), StmtCtxt(..),
- mkMonoBind, nullMonoBinds
+ StmtCtxt(..), mkMonoBind
)
import RnHsSyn ( RenamedHsExpr, RenamedRecordBinds )
-import TcHsSyn ( TcExpr, TcRecordBinds, mkHsTyApp, mkHsLet )
+import TcHsSyn ( TcExpr, TcRecordBinds, mkHsLet )
import TcMonad
import BasicTypes ( RecFlag(..) )
import Inst ( InstOrigin(..),
- LIE, emptyLIE, unitLIE, plusLIE, plusLIEs,
+ LIE, mkLIE, emptyLIE, unitLIE, plusLIE, plusLIEs,
newOverloadedLit, newMethod, newIPDict,
- instOverloadedFun, newDicts, newClassDicts,
- getIPsOfLIE, instToId, ipToId
+ newDicts, newClassDicts,
+ instToId, tcInstId
)
import TcBinds ( tcBindsAndThen )
-import TcEnv ( TcTyThing(..), tcInstId,
+import TcEnv ( TcTyThing(..),
tcLookupClass, tcLookupGlobalId, tcLookupGlobal_maybe,
tcLookupTyCon, tcLookupDataCon, tcLookup,
tcExtendGlobalTyVars
import TcMatches ( tcMatchesCase, tcMatchLambda, tcStmts )
import TcMonoType ( tcHsSigType, checkSigTyVars, sigCtxt )
import TcPat ( badFieldCon, simpleHsLitTy )
-import TcSimplify ( tcSimplifyAndCheck, partitionPredsOfLIE )
-import TcImprove ( tcImprove )
+import TcSimplify ( tcSimplifyCheck, tcSimplifyIPs )
import TcType ( TcType, TcTauType,
- tcInstTyVars,
- tcInstTcType, tcSplitRhoTy,
+ tcInstTyVars, tcInstType,
newTyVarTy, newTyVarTys, zonkTcType )
import FieldLabel ( fieldLabelName, fieldLabelType, fieldLabelTyCon )
-import Id ( idType, recordSelectorFieldLabel, isRecordSelector, mkVanillaId )
+import Id ( idType, recordSelectorFieldLabel, isRecordSelector )
import DataCon ( dataConFieldLabels, dataConSig,
dataConStrictMarks, StrictnessMark(..)
)
-import Name ( Name, getName )
-import Type ( mkFunTy, mkAppTy, mkTyVarTys, ipName_maybe,
+import Name ( Name )
+import Type ( mkFunTy, mkAppTy, mkTyConTy,
splitFunTy_maybe, splitFunTys,
mkTyConApp, splitSigmaTy,
- splitRhoTy,
isTauTy, tyVarsOfType, tyVarsOfTypes,
isSigmaTy, splitAlgTyConApp, splitAlgTyConApp_maybe,
liftedTypeKind, openTypeKind, mkArrowKind,
)
import TyCon ( TyCon, tyConTyVars )
import Subst ( mkTopTyVarSubst, substClasses, substTy )
-import VarSet ( elemVarSet, mkVarSet )
-import TysWiredIn ( boolTy )
+import VarSet ( elemVarSet )
+import TysWiredIn ( boolTy, mkListTy, listTyCon )
import TcUnify ( unifyTauTy, unifyFunTy, unifyListTy, unifyTupleTy )
import PrelNames ( cCallableClassName,
cReturnableClassName,
-- To ensure that the forall'd type variables don't get unified with each
-- other or any other types, we make fresh copy of the alleged type
- tcInstTcType expected_arg_ty `thenNF_Tc` \ (sig_tyvars, sig_rho) ->
+ tcInstType expected_arg_ty `thenNF_Tc` \ (sig_tyvars, sig_theta, sig_tau) ->
let
- (sig_theta, sig_tau) = splitRhoTy sig_rho
- free_tyvars = tyVarsOfType expected_arg_ty
+ free_tvs = tyVarsOfType expected_arg_ty
in
-- Type-check the arg and unify with expected type
tcMonoExpr arg sig_tau `thenTc` \ (arg', lie_arg) ->
-- Conclusion: include the free vars of the expected arg type in the
-- list of "free vars" for the signature check.
- tcExtendGlobalTyVars free_tyvars $
+ tcExtendGlobalTyVars free_tvs $
tcAddErrCtxtM (sigCtxt sig_msg sig_tyvars sig_theta sig_tau) $
- checkSigTyVars sig_tyvars free_tyvars `thenTc` \ zonked_sig_tyvars ->
-
- newDicts SignatureOrigin sig_theta `thenNF_Tc` \ (sig_dicts, dict_ids) ->
- tcImprove (sig_dicts `plusLIE` lie_arg) `thenTc_`
- -- ToDo: better origin
- tcSimplifyAndCheck
+ newDicts SignatureOrigin sig_theta `thenNF_Tc` \ sig_dicts ->
+ tcSimplifyCheck
(text "the type signature of an expression")
- (mkVarSet zonked_sig_tyvars)
+ sig_tyvars
sig_dicts lie_arg `thenTc` \ (free_insts, inst_binds) ->
+ checkSigTyVars sig_tyvars free_tvs `thenTc` \ zonked_sig_tyvars ->
+
let
-- This HsLet binds any Insts which came out of the simplification.
-- It's a bit out of place here, but using AbsBind involves inventing
-- a couple of new names which seems worse.
generalised_arg = TyLam zonked_sig_tyvars $
- DictLam dict_ids $
+ DictLam (map instToId sig_dicts) $
mkHsLet inst_binds $
arg'
in
\begin{code}
tcMonoExpr (HsIPVar name) res_ty
- -- ZZ What's the `id' used for here...
- = let id = mkVanillaId name res_ty in
- tcGetInstLoc (OccurrenceOf id) `thenNF_Tc` \ loc ->
- newIPDict name res_ty loc `thenNF_Tc` \ ip ->
+ = newIPDict (IPOcc name) name res_ty `thenNF_Tc` \ ip ->
returnNF_Tc (HsIPVar (instToId ip), unitLIE ip)
\end{code}
let
new_arg_dict (arg, arg_ty)
= newClassDicts (CCallOrigin (_UNPK_ lbl) (Just arg))
- [(cCallableClass, [arg_ty])] `thenNF_Tc` \ (arg_dicts, _) ->
+ [(cCallableClass, [arg_ty])] `thenNF_Tc` \ arg_dicts ->
returnNF_Tc arg_dicts -- Actually a singleton bag
result_origin = CCallOrigin (_UNPK_ lbl) Nothing {- Not an arg -}
-- Construct the extra insts, which encode the
-- constraints on the argument and result types.
mapNF_Tc new_arg_dict (zipEqual "tcMonoExpr:CCall" args arg_tys) `thenNF_Tc` \ ccarg_dicts_s ->
- newClassDicts result_origin [(cReturnableClass, [result_ty])] `thenNF_Tc` \ (ccres_dict, _) ->
+ newClassDicts result_origin [(cReturnableClass, [result_ty])] `thenNF_Tc` \ ccres_dict ->
returnTc (HsCCall lbl args' may_gc is_asm io_result_ty,
- foldr plusLIE ccres_dict ccarg_dicts_s `plusLIE` args_lie)
+ mkLIE (ccres_dict ++ concat ccarg_dicts_s) `plusLIE` args_lie)
\end{code}
\begin{code}
inst_env = mkTopTyVarSubst tyvars result_inst_tys
theta' = substClasses inst_env theta
in
- newClassDicts RecordUpdOrigin theta' `thenNF_Tc` \ (con_lie, dicts) ->
+ newClassDicts RecordUpdOrigin theta' `thenNF_Tc` \ dicts ->
-- Phew!
- returnTc (RecordUpdOut record_expr' result_record_ty dicts rbinds',
- con_lie `plusLIE` record_lie `plusLIE` rbinds_lie)
+ returnTc (RecordUpdOut record_expr' result_record_ty (map instToId dicts) rbinds',
+ mkLIE dicts `plusLIE` record_lie `plusLIE` rbinds_lie)
tcMonoExpr (ArithSeqIn seq@(From expr)) res_ty
= unifyListTy res_ty `thenTc` \ elt_ty ->
tcLookupGlobalId enumFromName `thenNF_Tc` \ sel_id ->
newMethod (ArithSeqOrigin seq)
- sel_id [elt_ty] `thenNF_Tc` \ (lie2, enum_from_id) ->
+ sel_id [elt_ty] `thenNF_Tc` \ enum_from ->
- returnTc (ArithSeqOut (HsVar enum_from_id) (From expr'),
- lie1 `plusLIE` lie2)
+ returnTc (ArithSeqOut (HsVar (instToId enum_from)) (From expr'),
+ lie1 `plusLIE` unitLIE enum_from)
tcMonoExpr in_expr@(ArithSeqIn seq@(FromThen expr1 expr2)) res_ty
= tcAddErrCtxt (arithSeqCtxt in_expr) $
tcMonoExpr expr1 elt_ty `thenTc` \ (expr1',lie1) ->
tcMonoExpr expr2 elt_ty `thenTc` \ (expr2',lie2) ->
tcLookupGlobalId enumFromThenName `thenNF_Tc` \ sel_id ->
- newMethod (ArithSeqOrigin seq) sel_id [elt_ty] `thenNF_Tc` \ (lie3, enum_from_then_id) ->
+ newMethod (ArithSeqOrigin seq) sel_id [elt_ty] `thenNF_Tc` \ enum_from_then ->
- returnTc (ArithSeqOut (HsVar enum_from_then_id)
- (FromThen expr1' expr2'),
- lie1 `plusLIE` lie2 `plusLIE` lie3)
+ returnTc (ArithSeqOut (HsVar (instToId enum_from_then))
+ (FromThen expr1' expr2'),
+ lie1 `plusLIE` lie2 `plusLIE` unitLIE enum_from_then)
tcMonoExpr in_expr@(ArithSeqIn seq@(FromTo expr1 expr2)) res_ty
= tcAddErrCtxt (arithSeqCtxt in_expr) $
tcMonoExpr expr1 elt_ty `thenTc` \ (expr1',lie1) ->
tcMonoExpr expr2 elt_ty `thenTc` \ (expr2',lie2) ->
tcLookupGlobalId enumFromToName `thenNF_Tc` \ sel_id ->
- newMethod (ArithSeqOrigin seq) sel_id [elt_ty] `thenNF_Tc` \ (lie3, enum_from_to_id) ->
+ newMethod (ArithSeqOrigin seq) sel_id [elt_ty] `thenNF_Tc` \ enum_from_to ->
- returnTc (ArithSeqOut (HsVar enum_from_to_id)
+ returnTc (ArithSeqOut (HsVar (instToId enum_from_to))
(FromTo expr1' expr2'),
- lie1 `plusLIE` lie2 `plusLIE` lie3)
+ lie1 `plusLIE` lie2 `plusLIE` unitLIE enum_from_to)
tcMonoExpr in_expr@(ArithSeqIn seq@(FromThenTo expr1 expr2 expr3)) res_ty
= tcAddErrCtxt (arithSeqCtxt in_expr) $
tcMonoExpr expr2 elt_ty `thenTc` \ (expr2',lie2) ->
tcMonoExpr expr3 elt_ty `thenTc` \ (expr3',lie3) ->
tcLookupGlobalId enumFromThenToName `thenNF_Tc` \ sel_id ->
- newMethod (ArithSeqOrigin seq) sel_id [elt_ty] `thenNF_Tc` \ (lie4, eft_id) ->
+ newMethod (ArithSeqOrigin seq) sel_id [elt_ty] `thenNF_Tc` \ eft ->
- returnTc (ArithSeqOut (HsVar eft_id)
- (FromThenTo expr1' expr2' expr3'),
- lie1 `plusLIE` lie2 `plusLIE` lie3 `plusLIE` lie4)
+ returnTc (ArithSeqOut (HsVar (instToId eft))
+ (FromThenTo expr1' expr2' expr3'),
+ lie1 `plusLIE` lie2 `plusLIE` lie3 `plusLIE` unitLIE eft)
\end{code}
%************************************************************************
-- If everything is ok, return the stuff unchanged, except for
-- the effect of any substutions etc. We simply discard the
- -- result of the tcSimplifyAndCheck (inside tcPolyExpr), except for any default
+ -- result of the tcSimplifyCheck (inside tcPolyExpr), except for any default
-- resolution it may have done, which is recorded in the
-- substitution.
returnTc (expr, lie)
\begin{code}
tcMonoExpr (HsWith expr binds) res_ty
- = tcMonoExpr expr res_ty `thenTc` \ (expr', lie) ->
- tcIPBinds binds `thenTc` \ (binds', types, lie2) ->
- partitionPredsOfLIE isBound lie `thenTc` \ (ips, lie', dict_binds) ->
- let expr'' = if nullMonoBinds dict_binds
- then expr'
- else HsLet (mkMonoBind (revBinds dict_binds) [] NonRecursive)
- expr'
+ = tcMonoExpr expr res_ty `thenTc` \ (expr', expr_lie) ->
+ mapAndUnzipTc tcIPBind binds `thenTc` \ (pairs, bind_lies) ->
+ tcSimplifyIPs (map fst binds) expr_lie `thenTc` \ (expr_lie', dict_binds) ->
+ let
+ binds' = [(instToId ip, rhs) | (ip,rhs) <- pairs]
+ expr'' = HsLet (mkMonoBind dict_binds [] Recursive) expr'
in
- tcCheckIPBinds binds' types ips `thenTc_`
- returnTc (HsWith expr'' binds', lie' `plusLIE` lie2)
- where isBound p
- = case ipName_maybe p of
- Just n -> n `elem` names
- Nothing -> False
- names = map fst binds
- -- revBinds is used because tcSimplify outputs the bindings
- -- out-of-order. it's not a problem elsewhere because these
- -- bindings are normally used in a recursive let
- -- ZZ probably need to find a better solution
- revBinds (b1 `AndMonoBinds` b2) =
- (revBinds b2) `AndMonoBinds` (revBinds b1)
- revBinds b = b
-
-tcIPBinds ((name, expr) : binds)
- = newTyVarTy openTypeKind `thenTc` \ ty ->
- tcGetSrcLoc `thenTc` \ loc ->
- let id = ipToId name ty loc in
- tcMonoExpr expr ty `thenTc` \ (expr', lie) ->
- zonkTcType ty `thenTc` \ ty' ->
- tcIPBinds binds `thenTc` \ (binds', types, lie2) ->
- returnTc ((id, expr') : binds', ty : types, lie `plusLIE` lie2)
-tcIPBinds [] = returnTc ([], [], emptyLIE)
-
-tcCheckIPBinds binds types ips
- = foldrTc tcCheckIPBind (getIPsOfLIE ips) (zip binds types)
-
--- ZZ how do we use the loc?
-tcCheckIPBind bt@((v, _), t1) ((n, t2) : ips) | getName v == n
- = unifyTauTy t1 t2 `thenTc_`
- tcCheckIPBind bt ips `thenTc` \ ips' ->
- returnTc ips'
-tcCheckIPBind bt (ip : ips)
- = tcCheckIPBind bt ips `thenTc` \ ips' ->
- returnTc (ip : ips')
-tcCheckIPBind bt []
- = returnTc []
+ returnTc (HsWith expr'' binds', expr_lie' `plusLIE` plusLIEs bind_lies)
+
+tcIPBind (name, expr)
+ = newTyVarTy openTypeKind `thenTc` \ ty ->
+ tcGetSrcLoc `thenTc` \ loc ->
+ newIPDict (IPBind name) name ty `thenNF_Tc` \ ip ->
+ tcMonoExpr expr ty `thenTc` \ (expr', lie) ->
+ returnTc ((ip, expr'), lie)
\end{code}
Typecheck expression which in most cases will be an Id.
= -- Look up the Id and instantiate its type
tcLookup name `thenNF_Tc` \ thing ->
case thing of
- ATcId tc_id -> instantiate_it (OccurrenceOf tc_id) tc_id (idType tc_id)
- AGlobal (AnId id) -> tcInstId id `thenNF_Tc` \ (tyvars, theta, tau) ->
- instantiate_it2 (OccurrenceOf id) id tyvars theta tau
- where
- -- The instantiate_it loop runs round instantiating the Id.
- -- It has to be a loop because we are now prepared to entertain
- -- types like
- -- f:: forall a. Eq a => forall b. Baz b => tau
- -- We want to instantiate this to
- -- f2::tau {f2 = f1 b (Baz b), f1 = f a (Eq a)}
- instantiate_it orig fun ty
- = tcInstTcType ty `thenNF_Tc` \ (tyvars, rho) ->
- tcSplitRhoTy rho `thenNF_Tc` \ (theta, tau) ->
- instantiate_it2 orig fun tyvars theta tau
-
- instantiate_it2 orig fun tyvars theta tau
- = if null theta then -- Is it overloaded?
- returnNF_Tc (mkHsTyApp (HsVar fun) arg_tys, emptyLIE, tau)
- else
- -- Yes, it's overloaded
- instOverloadedFun orig fun arg_tys theta tau `thenNF_Tc` \ (fun', lie1) ->
- instantiate_it orig fun' tau `thenNF_Tc` \ (expr, lie2, final_tau) ->
- returnNF_Tc (expr, lie1 `plusLIE` lie2, final_tau)
-
- where
- arg_tys = mkTyVarTys tyvars
+ ATcId tc_id -> tcInstId tc_id
+ AGlobal (AnId id) -> tcInstId id
\end{code}
%************************************************************************
ASSERT( not (null stmts) )
tcAddSrcLoc src_loc $
- newTyVarTy (mkArrowKind liftedTypeKind liftedTypeKind) `thenNF_Tc` \ m ->
- newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
- unifyTauTy res_ty (mkAppTy m elt_ty) `thenTc_`
-
-- If it's a comprehension we're dealing with,
-- force it to be a list comprehension.
-- (as of Haskell 98, monad comprehensions are no more.)
(case do_or_lc of
- ListComp -> unifyListTy res_ty `thenTc_` returnTc ()
- _ -> returnTc ()) `thenTc_`
+ ListComp -> unifyListTy res_ty `thenTc` \ elt_ty ->
+ returnNF_Tc (mkTyConTy listTyCon, (mkListTy, elt_ty))
+
+ _ -> newTyVarTy (mkArrowKind liftedTypeKind liftedTypeKind) `thenNF_Tc` \ m_ty ->
+ newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
+ unifyTauTy res_ty (mkAppTy m_ty elt_ty) `thenTc_`
+ returnNF_Tc (m_ty, (mkAppTy m_ty, elt_ty))
+ ) `thenNF_Tc` \ (tc_ty, m_ty) ->
- tcStmts do_or_lc (mkAppTy m) elt_ty src_loc stmts `thenTc` \ ((stmts', _), stmts_lie) ->
+ tcStmts do_or_lc m_ty stmts `thenTc` \ (stmts', stmts_lie) ->
-- Build the then and zero methods in case we need them
-- It's important that "then" and "return" appear just once in the final LIE,
tcLookupGlobalId returnMName `thenNF_Tc` \ return_sel_id ->
tcLookupGlobalId thenMName `thenNF_Tc` \ then_sel_id ->
tcLookupGlobalId failMName `thenNF_Tc` \ fail_sel_id ->
- newMethod DoOrigin return_sel_id [m] `thenNF_Tc` \ (return_lie, return_id) ->
- newMethod DoOrigin then_sel_id [m] `thenNF_Tc` \ (then_lie, then_id) ->
- newMethod DoOrigin fail_sel_id [m] `thenNF_Tc` \ (fail_lie, fail_id) ->
+ newMethod DoOrigin return_sel_id [tc_ty] `thenNF_Tc` \ return_inst ->
+ newMethod DoOrigin then_sel_id [tc_ty] `thenNF_Tc` \ then_inst ->
+ newMethod DoOrigin fail_sel_id [tc_ty] `thenNF_Tc` \ fail_inst ->
let
- monad_lie = then_lie `plusLIE` return_lie `plusLIE` fail_lie
+ monad_lie = mkLIE [return_inst, then_inst, fail_inst]
in
- returnTc (HsDoOut do_or_lc stmts' return_id then_id fail_id res_ty src_loc,
+ returnTc (HsDoOut do_or_lc stmts'
+ (instToId return_inst) (instToId then_inst) (instToId fail_inst)
+ res_ty src_loc,
stmts_lie `plusLIE` monad_lie)
\end{code}
tcLit (HsLitLit s _) res_ty
= tcLookupClass cCallableClassName `thenNF_Tc` \ cCallableClass ->
newClassDicts (LitLitOrigin (_UNPK_ s))
- [(cCallableClass,[res_ty])] `thenNF_Tc` \ (dicts, _) ->
- returnTc (HsLit (HsLitLit s res_ty), dicts)
+ [(cCallableClass,[res_ty])] `thenNF_Tc` \ dicts ->
+ returnTc (HsLit (HsLitLit s res_ty), mkLIE dicts)
tcLit lit res_ty
= unifyTauTy res_ty (simpleHsLitTy lit) `thenTc_`
mkHsTyLam, mkHsDictLam, mkHsLet,
-- re-exported from TcEnv
- TcId, tcInstId,
+ TcId,
zonkTopBinds, zonkId, zonkIdOcc, zonkExpr,
zonkForeignExports, zonkRules
import Id ( idName, idType, isLocalId, setIdType, isIP, Id )
import DataCon ( dataConWrapId )
import TcEnv ( tcLookupGlobal_maybe, tcExtendGlobalValEnv,
- TcEnv, TcId, tcInstId
+ TcEnv, TcId
)
import TcMonad
+++ /dev/null
-\begin{code}
-module TcImprove ( tcImprove ) where
-
-#include "HsVersions.h"
-
-import Name ( Name )
-import Class ( Class, FunDep, className )
-import Unify ( unifyTyListsX )
-import Subst ( mkSubst, emptyInScopeSet, substTy )
-import TcEnv ( tcGetInstEnv )
-import InstEnv ( classInstEnv )
-import TcMonad
-import TcType ( TcType, TcTyVarSet, zonkTcType )
-import TcUnify ( unifyTauTyLists )
-import Inst ( LIE, getFunDepsOfLIE, getIPsOfLIE )
-import VarSet ( VarSet, emptyVarSet, unionVarSet )
-import FunDeps ( instantiateFdClassTys )
-import List ( nub )
-\end{code}
-
-\begin{code}
-tcImprove :: LIE -> TcM ()
--- Do unifications based on functional dependencies in the LIE
-tcImprove lie
- = tcGetInstEnv `thenNF_Tc` \ inst_env ->
- let
- nfdss, clas_nfdss, inst_nfdss, ip_nfdss :: [(TcTyVarSet, Name, [FunDep TcType])]
- nfdss = ip_nfdss ++ clas_nfdss ++ inst_nfdss
-
- cfdss :: [(Class, [FunDep TcType])]
- cfdss = getFunDepsOfLIE lie
- clas_nfdss = [(emptyVarSet, className c, fds) | (c,fds) <- cfdss]
-
- classes = nub (map fst cfdss)
- inst_nfdss = [ (free, className c, instantiateFdClassTys c ts)
- | c <- classes,
- (free, ts, i) <- classInstEnv inst_env c
- ]
-
- ip_nfdss = [(emptyVarSet, n, [([], [ty])]) | (n,ty) <- getIPsOfLIE lie]
-
- {- Example: we have
- class C a b c | a->b where ...
- instance C Int Bool c
-
- Given the LIE FD C (Int->t)
- we get clas_nfdss = [({}, C, [Int->t, t->Int])
- inst_nfdss = [({c}, C, [Int->Bool, Bool->Int])]
-
- Another way would be to flatten a bit
- we get clas_nfdss = [({}, C, Int->t), ({}, C, t->Int)]
- inst_nfdss = [({c}, C, Int->Bool), ({c}, C, Bool->Int)]
-
- iterImprove then matches up the C and Int, and unifies t <-> Bool
- -}
-
- in
- iterImprove nfdss
-
-
-iterImprove :: [(VarSet, Name, [FunDep TcType])] -> TcM ()
-iterImprove [] = returnTc ()
-iterImprove cfdss
- = selfImprove pairImprove cfdss `thenTc` \ change2 ->
- if {- change1 || -} change2 then
- iterImprove cfdss
- else
- returnTc ()
-
--- ZZ this will do a lot of redundant checking wrt instances
--- it would do to make this operate over two lists, the first
--- with only clas_nfds and ip_nfds, and the second with everything
--- control would otherwise mimic the current loop, so that the
--- caller could control whether the redundant inst improvements
--- were avoided
--- you could then also use this to check for consistency of new instances
-
--- selfImprove is really just doing a cartesian product of all the fds
-selfImprove f [] = returnTc False
-selfImprove f (nfds : nfdss)
- = mapTc (f nfds) nfdss `thenTc` \ changes ->
- selfImprove f nfdss `thenTc` \ rest_changed ->
- returnTc (or changes || rest_changed)
-
-pairImprove (free1, n1, fds1) (free2, n2, fds2)
- = if n1 == n2 then
- checkFds (free1 `unionVarSet` free2) fds1 fds2
- else
- returnTc False
-
-checkFds free [] [] = returnTc False
-checkFds free (fd1 : fd1s) (fd2 : fd2s) =
- checkFd free fd1 fd2 `thenTc` \ change ->
- checkFds free fd1s fd2s `thenTc` \ changes ->
- returnTc (change || changes)
---checkFds _ _ = returnTc False
-
-checkFd free (t_x, t_y) (s_x, s_y)
- -- we need to zonk each time because unification
- -- may happen at any time
- = zonkUnifyTys free t_x s_x `thenTc` \ msubst ->
- case msubst of
- Just subst ->
- let full_subst = mkSubst emptyInScopeSet subst
- t_y' = map (substTy full_subst) t_y
- s_y' = map (substTy full_subst) s_y
- in
- zonkEqTys t_y' s_y' `thenTc` \ eq ->
- if eq then
- -- they're the same, nothing changes...
- returnTc False
- else
- -- ZZ what happens if two instance vars unify?
- unifyTauTyLists t_y' s_y' `thenTc_`
- -- if we get here, something must have unified
- returnTc True
- Nothing ->
- returnTc False
-
-zonkEqTys ts1 ts2
- = mapTc zonkTcType ts1 `thenTc` \ ts1' ->
- mapTc zonkTcType ts2 `thenTc` \ ts2' ->
- returnTc (ts1' == ts2')
-
-zonkUnifyTys free ts1 ts2
- = mapTc zonkTcType ts1 `thenTc` \ ts1' ->
- mapTc zonkTcType ts2 `thenTc` \ ts2' ->
- -- pprTrace "zMT" (ppr (ts1', free, ts2')) $
- returnTc (unifyTyListsX free ts2' ts1')
-\end{code}
import CmdLineOpts ( DynFlag(..), dopt )
-import HsSyn ( HsDecl(..), InstDecl(..), TyClDecl(..),
+import HsSyn ( HsDecl(..), InstDecl(..), TyClDecl(..), HsType(..),
MonoBinds(..), HsExpr(..), HsLit(..), Sig(..),
andMonoBindList, collectMonoBinders, isClassDecl
)
import TcBinds ( tcSpecSigs )
import TcClassDcl ( tcMethodBind, badMethodErr )
import TcMonad
+import TcType ( tcInstType )
import Inst ( InstOrigin(..),
- newDicts, newClassDicts,
- LIE, emptyLIE, plusLIE, plusLIEs )
+ newDicts, newClassDicts, instToId,
+ LIE, mkLIE, emptyLIE, plusLIE, plusLIEs )
import TcDeriv ( tcDeriving )
import TcEnv ( TcEnv, tcExtendGlobalValEnv,
tcExtendTyVarEnvForMeths,
- tcAddImportedIdInfo, tcInstId, tcLookupClass,
+ tcAddImportedIdInfo, tcLookupClass,
InstInfo(..), pprInstInfo, simpleInstInfoTyCon, simpleInstInfoTy,
newDFunName, tcExtendTyVarEnv
)
import InstEnv ( InstEnv, extendInstEnv )
-import TcMonoType ( tcTyVars, tcHsSigType, kcHsSigType )
-import TcSimplify ( tcSimplifyAndCheck )
-import TcType ( zonkTcSigTyVars )
+import TcMonoType ( tcTyVars, tcHsSigType, kcHsSigType, checkSigTyVars )
+import TcSimplify ( tcSimplifyCheck )
import HscTypes ( HomeSymbolTable, DFunId,
ModDetails(..), PackageInstEnv, PersistentRenamerState
)
-import Bag ( unionManyBags )
import DataCon ( classDataCon )
import Class ( Class, DefMeth(..), classBigSig )
import Var ( idName, idType )
+import VarSet ( emptyVarSet )
import Maybes ( maybeToBool )
import MkId ( mkDictFunId )
+import FunDeps ( checkInstFDs )
import Generics ( validGenericInstanceType )
import Module ( Module, foldModuleEnv )
import Name ( getSrcLoc )
import NameSet ( emptyNameSet, nameSetToList )
import PrelInfo ( eRROR_ID )
-import PprType ( pprConstraint, pprPred )
+import PprType ( pprClassPred, pprPred )
import TyCon ( TyCon, isSynTyCon )
import Type ( splitDFunTy, isTyVarTy,
splitTyConApp_maybe, splitDictTy,
getClassTys_maybe
)
import Subst ( mkTopTyVarSubst, substClasses )
-import VarSet ( mkVarSet, varSetElems )
+import VarSet ( varSetElems )
import TysWiredIn ( genericTyCons, isFFIArgumentTy, isFFIImportResultTy )
import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
import Name ( Name )
\begin{code}
tcInstDecl1 :: TcEnv -> RenamedInstDecl -> NF_TcM [InstInfo]
-- Deal with a single instance declaration
-tcInstDecl1 unf_env (InstDecl poly_ty binds uprags maybe_dfun_name src_loc)
+tcInstDecl1 unf_env decl@(InstDecl poly_ty binds uprags maybe_dfun_name src_loc)
= -- Prime error recovery, set source location
recoverNF_Tc (returnNF_Tc []) $
tcAddSrcLoc src_loc $
-- Type-check all the stuff before the "where"
- tcHsSigType poly_ty `thenTc` \ poly_ty' ->
+ tcAddErrCtxt (instDeclCtxt poly_ty) (
+ tcHsSigType poly_ty
+ ) `thenTc` \ poly_ty' ->
let
(tyvars, theta, clas, inst_tys) = splitDFunTy poly_ty'
in
-- Imported ones should have been checked already, and may indeed
-- contain something illegal in normal Haskell, notably
-- instance CCallable [Char]
-
- getDOptsTc `thenTc` \ dflags ->
- scrutiniseInstanceHead dflags clas inst_tys `thenNF_Tc_`
- mapNF_Tc (scrutiniseInstanceConstraint dflags) theta `thenNF_Tc_`
+ getDOptsTc `thenTc` \ dflags ->
+ checkInstValidity dflags theta clas inst_tys `thenTc_`
-- Make the dfun id and return it
newDFunName clas inst_tys src_loc `thenNF_Tc` \ dfun_name ->
tcAddSrcLoc (getSrcLoc dfun_id) $
-- Instantiate the instance decl with tc-style type variables
- tcInstId dfun_id `thenNF_Tc` \ (inst_tyvars', dfun_theta', dict_ty') ->
+ tcInstType (idType dfun_id) `thenNF_Tc` \ (inst_tyvars', dfun_theta', dict_ty') ->
let
(clas, inst_tys') = splitDictTy dict_ty'
origin = InstanceDeclOrigin
mapTc (addErrTc . badMethodErr clas) bad_bndrs `thenNF_Tc_`
-- Create dictionary Ids from the specified instance contexts.
- newClassDicts origin sc_theta' `thenNF_Tc` \ (sc_dicts, sc_dict_ids) ->
- newDicts origin dfun_theta' `thenNF_Tc` \ (dfun_arg_dicts, dfun_arg_dicts_ids) ->
- newClassDicts origin [(clas,inst_tys')] `thenNF_Tc` \ (this_dict, [this_dict_id]) ->
+ newClassDicts origin sc_theta' `thenNF_Tc` \ sc_dicts ->
+ newDicts origin dfun_theta' `thenNF_Tc` \ dfun_arg_dicts ->
+ newClassDicts origin [(clas,inst_tys')] `thenNF_Tc` \ [this_dict] ->
tcExtendTyVarEnvForMeths inst_tyvars inst_tyvars' (
tcExtendGlobalValEnv dm_ids (
dfun_theta'
monobinds uprags True)
op_items
- )) `thenTc` \ (method_binds_s, insts_needed_s, meth_lies_w_ids) ->
+ )) `thenTc` \ (method_binds_s, insts_needed_s, meth_insts) ->
-- Deal with SPECIALISE instance pragmas by making them
-- look like SPECIALISE pragmas for the dfun
) `thenTc` \ (prag_binds, prag_lie) ->
-- Check the overloading constraints of the methods and superclasses
-
- -- tcMethodBind has checked that the class_tyvars havn't
- -- been unified with each other or another type, but we must
- -- still zonk them before passing them to tcSimplifyAndCheck
- zonkTcSigTyVars inst_tyvars' `thenNF_Tc` \ zonked_inst_tyvars ->
let
- inst_tyvars_set = mkVarSet zonked_inst_tyvars
-
- (meth_lies, meth_ids) = unzip meth_lies_w_ids
-
-- These insts are in scope; quite a few, eh?
- avail_insts = this_dict `plusLIE`
- dfun_arg_dicts `plusLIE`
- sc_dicts `plusLIE`
- unionManyBags meth_lies
+ avail_insts = [this_dict] ++
+ dfun_arg_dicts ++
+ sc_dicts ++
+ meth_insts
- methods_lie = plusLIEs insts_needed_s
+ methods_lie = plusLIEs insts_needed_s
in
-- Simplify the constraints from methods
tcAddErrCtxt methodCtxt (
- tcSimplifyAndCheck
+ tcSimplifyCheck
(ptext SLIT("instance declaration context"))
- inst_tyvars_set -- Local tyvars
+ inst_tyvars'
avail_insts
methods_lie
) `thenTc` \ (const_lie1, lie_binds1) ->
-- Figure out bindings for the superclass context
tcAddErrCtxt superClassCtxt (
- tcSimplifyAndCheck
+ tcSimplifyCheck
(ptext SLIT("instance declaration context"))
- inst_tyvars_set
+ inst_tyvars'
dfun_arg_dicts -- NB! Don't include this_dict here, else the sc_dicts
-- get bound by just selecting from this_dict!!
- sc_dicts
- ) `thenTc` \ (const_lie2, lie_binds2) ->
-
+ (mkLIE sc_dicts)
+ ) `thenTc` \ (const_lie2, lie_binds2) ->
+
+ checkSigTyVars inst_tyvars' emptyVarSet `thenNF_Tc` \ zonked_inst_tyvars ->
-- Create the result bindings
let
dict_constr = classDataCon clas
- scs_and_meths = sc_dict_ids ++ meth_ids
+ scs_and_meths = map instToId (sc_dicts ++ meth_insts)
+ this_dict_id = instToId this_dict
dict_rhs
| null scs_and_meths
(HsLit (HsString msg))
| otherwise -- The common case
- = mkHsConApp dict_constr inst_tys' (map HsVar (sc_dict_ids ++ meth_ids))
+ = mkHsConApp dict_constr inst_tys' (map HsVar scs_and_meths)
-- We don't produce a binding for the dict_constr; instead we
-- rely on the simplifier to unfold this saturated application
-- We do this rather than generate an HsCon directly, because
main_bind
= AbsBinds
zonked_inst_tyvars
- dfun_arg_dicts_ids
+ (map instToId dfun_arg_dicts)
[(inst_tyvars', dfun_id, this_dict_id)]
emptyNameSet -- No inlines (yet)
(lie_binds1 `AndMonoBinds`
We can also have instances for functions: @instance Foo (a -> b) ...@.
\begin{code}
-scrutiniseInstanceConstraint dflags pred
+checkInstValidity dflags theta clas inst_tys
+ | null errs = returnTc ()
+ | otherwise = addErrsTc errs `thenNF_Tc_` failTc
+ where
+ errs = checkInstHead dflags clas inst_tys ++
+ [err | pred <- theta, err <- checkInstConstraint dflags pred]
+
+checkInstConstraint dflags pred
| dopt Opt_AllowUndecidableInstances dflags
- = returnNF_Tc ()
+ = []
| Just (clas,tys) <- getClassTys_maybe pred,
all isTyVarTy tys
- = returnNF_Tc ()
+ = []
| otherwise
- = addErrTc (instConstraintErr pred)
+ = [instConstraintErr pred]
-scrutiniseInstanceHead dflags clas inst_taus
+checkInstHead dflags clas inst_taus
| -- CCALL CHECK
-- A user declaration of a CCallable/CReturnable instance
-- must be for a "boxed primitive" type.
||
(clas `hasKey` cReturnableClassKey
&& not (creturnable_type first_inst_tau))
- = addErrTc (nonBoxedPrimCCallErr clas first_inst_tau)
-
- -- Allow anything for AllowUndecidableInstances
- | dopt Opt_AllowUndecidableInstances dflags
- = returnNF_Tc ()
+ = [nonBoxedPrimCCallErr clas first_inst_tau]
-- If GlasgowExts then check at least one isn't a type variable
- | dopt Opt_GlasgowExts dflags
- = if all isTyVarTy inst_taus
- then addErrTc (instTypeErr clas inst_taus
- (text "There must be at least one non-type-variable in the instance head"))
- else returnNF_Tc ()
+ | dopt Opt_GlasgowExts dflags
+ = -- GlasgowExts case
+ check_tyvars dflags clas inst_taus ++ check_fundeps dflags clas inst_taus
-- WITH HASKELL 1.4, MUST HAVE C (T a b c)
- | not (length inst_taus == 1 &&
- maybeToBool maybe_tycon_app && -- Yes, there's a type constuctor
- not (isSynTyCon tycon) && -- ...but not a synonym
- all isTyVarTy arg_tys && -- Applied to type variables
- length (varSetElems (tyVarsOfTypes arg_tys)) == length arg_tys
+ | not (length inst_taus == 1 &&
+ maybeToBool maybe_tycon_app && -- Yes, there's a type constuctor
+ not (isSynTyCon tycon) && -- ...but not a synonym
+ all isTyVarTy arg_tys && -- Applied to type variables
+ length (varSetElems (tyVarsOfTypes arg_tys)) == length arg_tys
-- This last condition checks that all the type variables are distinct
- )
- = addErrTc (instTypeErr clas inst_taus
- (text "the instance type must be of form (T a b c)" $$
- text "where T is not a synonym, and a,b,c are distinct type variables")
- )
+ )
+ = [instTypeErr clas inst_taus
+ (text "the instance type must be of form (T a b c)" $$
+ text "where T is not a synonym, and a,b,c are distinct type variables")]
| otherwise
- = returnNF_Tc ()
+ = []
where
(first_inst_tau : _) = inst_taus
ccallable_type dflags ty = isFFIArgumentTy dflags False {- Not safe call -} ty
creturnable_type ty = isFFIImportResultTy dflags ty
+
+check_tyvars dflags clas inst_taus
+ -- Check that at least one isn't a type variable
+ -- unless -fallow-undecideable-instances
+ | dopt Opt_AllowUndecidableInstances dflags = []
+ | not (all isTyVarTy inst_taus) = []
+ | otherwise = [the_err]
+ where
+ the_err = instTypeErr clas inst_taus msg
+ msg = ptext SLIT("There must be at least one non-type-variable in the instance head")
+
+check_fundeps dflags clas inst_taus
+ | checkInstFDs clas inst_taus = []
+ | otherwise = [the_err]
+ where
+ the_err = instTypeErr clas inst_taus msg
+ msg = ptext SLIT("the instance types do not agree with the functional dependencies of the class")
\end{code}
ctxt = hsep [ptext SLIT("In the"), text thing,
ptext SLIT("declaration for"), quotes (ppr (tcdName decl))]
+
+instDeclCtxt inst_ty = ptext SLIT("In the instance declaration for") <+> quotes doc
+ where
+ doc = case inst_ty of
+ HsForAllTy _ _ (HsPredTy pred) -> ppr pred
+ HsPredTy pred -> ppr pred
+ other -> ppr inst_ty -- Don't expect this
\end{code}
\begin{code}
ppr_inst_ty (tc,inst) = ppr (simpleInstInfoTy inst)
instTypeErr clas tys msg
- = sep [ptext SLIT("Illegal instance declaration for") <+> quotes (pprConstraint clas tys),
+ = sep [ptext SLIT("Illegal instance declaration for") <+>
+ quotes (pprClassPred clas tys),
nest 4 (parens msg)
]
nonBoxedPrimCCallErr clas inst_ty
= hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
- 4 (hsep [ ptext SLIT("class"), ppr clas, ptext SLIT("type"),
- ppr inst_ty])
+ 4 (pprClassPred clas [inst_ty])
methodCtxt = ptext SLIT("When checking the methods of an instance declaration")
superClassCtxt = ptext SLIT("When checking the super-classes of an instance declaration")
import HsSyn ( HsBinds(..), Match(..), GRHSs(..), GRHS(..),
MonoBinds(..), StmtCtxt(..), Stmt(..),
- pprMatch, getMatchLoc, consLetStmt,
- mkMonoBind, collectSigTysFromPats
+ pprMatch, getMatchLoc,
+ mkMonoBind, nullMonoBinds, collectSigTysFromPats
)
import RnHsSyn ( RenamedMatch, RenamedGRHSs, RenamedStmt )
-import TcHsSyn ( TcMatch, TcGRHSs, TcStmt )
+import TcHsSyn ( TcMatch, TcGRHSs, TcStmt, TcDictBinds )
import TcMonad
import TcMonoType ( kcHsSigType, tcTyVars, checkSigTyVars, tcHsSigType, sigPatCtxt )
-import Inst ( LIE, plusLIE, emptyLIE, plusLIEs )
-import TcEnv ( TcId, tcExtendTyVarEnv, tcExtendLocalValEnv, tcExtendGlobalTyVars )
-import TcPat ( tcPat, tcPatBndr_NoSigs, polyPatSig )
+import Inst ( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList )
+import TcEnv ( TcId, tcLookupLocalIds, tcExtendTyVarEnv, tcExtendLocalValEnv, tcExtendGlobalTyVars )
+import TcPat ( tcPat, tcMonoPatBndr, polyPatSig )
import TcType ( TcType, newTyVarTy )
import TcBinds ( tcBindsAndThen )
-import TcSimplify ( tcSimplifyAndCheck, bindInstsOfLocalFuns )
-import TcUnify ( unifyFunTy, unifyTauTy, unifyListTy )
+import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
+import TcUnify ( unifyFunTy, unifyTauTy )
import Name ( Name )
-import TysWiredIn ( boolTy )
-
+import TysWiredIn ( boolTy, mkListTy )
+import Id ( idType )
import BasicTypes ( RecFlag(..) )
-import Type ( tyVarsOfType, isTauTy, mkArrowKind, mkAppTy, mkFunTy,
- liftedTypeKind, openTypeKind )
-import SrcLoc ( SrcLoc )
+import Type ( tyVarsOfType, isTauTy, mkFunTy,
+ liftedTypeKind, openTypeKind, splitSigmaTy )
import VarSet
import Var ( Id )
import Bag
let
xve2 = bagToList pat_bndrs
pat_ids = map snd xve2
- ex_tv_list = bagToList ex_tvs
in
-- STEP 2: Check that the remaining "expected type" is not a rank-2 type
)) `thenTc` \ (grhss', lie_req2) ->
-- STEP 5: Check for existentially bound type variables
- tcExtendGlobalTyVars (tyVarsOfType rhs_ty) (
- tcAddErrCtxtM (sigPatCtxt ex_tv_list pat_ids) $
- checkSigTyVars ex_tv_list emptyVarSet `thenTc` \ zonked_ex_tvs ->
- tcSimplifyAndCheck
- (text ("the existential context of a data constructor"))
- (mkVarSet zonked_ex_tvs)
- lie_avail (lie_req1 `plusLIE` lie_req2)
- ) `thenTc` \ (lie_req', ex_binds) ->
-
- -- STEP 6 In case there are any polymorpic, overloaded binders in the pattern
- -- (which can happen in the case of rank-2 type signatures, or data constructors
- -- with polymorphic arguments), we must do a bindInstsOfLocalFns here
- bindInstsOfLocalFuns lie_req' pat_ids `thenTc` \ (lie_req'', inst_binds) ->
+ tcCheckExistentialPat pat_ids ex_tvs lie_avail
+ (lie_req1 `plusLIE` lie_req2)
+ rhs_ty `thenTc` \ (lie_req', ex_binds) ->
-- Phew! All done.
let
- grhss'' = glue_on Recursive ex_binds $
- glue_on Recursive inst_binds grhss'
+ match' = Match [] pats' Nothing (glue_on Recursive ex_binds grhss')
in
- returnTc (pat_ids, (Match [] pats' Nothing grhss'', lie_req''))
+ returnTc (pat_ids, (match', lie_req'))
-- glue_on just avoids stupid dross
glue_on _ EmptyMonoBinds grhss = grhss -- The common case
returnTc (GRHSs grhss' EmptyBinds (Just expected_ty), plusLIEs lies)
tc_grhs (GRHS guarded locn)
- = tcAddSrcLoc locn $
- tcStmts ctxt (\ty -> ty) expected_ty locn guarded
- `thenTc` \ ((guarded', _), lie) ->
+ = tcAddSrcLoc locn $
+ tcStmts ctxt (\ty -> ty, expected_ty) guarded `thenTc` \ (guarded', lie) ->
returnTc (GRHS guarded' locn, lie)
+
+
+tcCheckExistentialPat :: [TcId] -- Ids bound by this pattern
+ -> Bag TcTyVar -- Existentially quantified tyvars bound by pattern
+ -> LIE -- and context
+ -> LIE -- Required context
+ -> TcType -- and result type; vars in here must not escape
+ -> TcM (LIE, TcDictBinds) -- LIE to float out and dict bindings
+tcCheckExistentialPat ids ex_tvs lie_avail lie_req result_ty
+ | isEmptyBag ex_tvs && all not_overloaded ids
+ -- Short cut for case when there are no existentials
+ -- and no polymorphic overloaded variables
+ -- e.g. f :: (forall a. Ord a => a -> a) -> Int -> Int
+ -- f op x = ....
+ -- Here we must discharge op Methods
+ = ASSERT( isEmptyLIE lie_avail )
+ returnTc (lie_req, EmptyMonoBinds)
+
+ | otherwise
+ = tcExtendGlobalTyVars (tyVarsOfType result_ty) $
+ tcAddErrCtxtM (sigPatCtxt tv_list ids) $
+
+ -- In case there are any polymorpic, overloaded binders in the pattern
+ -- (which can happen in the case of rank-2 type signatures, or data constructors
+ -- with polymorphic arguments), we must do a bindInstsOfLocalFns here
+ bindInstsOfLocalFuns lie_req ids `thenTc` \ (lie1, inst_binds) ->
+
+ -- Deal with overloaded functions bound by the pattern
+ tcSimplifyCheck doc tv_list
+ (lieToList lie_avail) lie1 `thenTc` \ (lie2, dict_binds) ->
+ checkSigTyVars tv_list emptyVarSet `thenTc_`
+
+ returnTc (lie2, dict_binds `AndMonoBinds` inst_binds)
+ where
+ doc = text ("the existential context of a data constructor")
+ tv_list = bagToList ex_tvs
+ not_overloaded id = case splitSigmaTy (idType id) of
+ (_, theta, _) -> null theta
\end{code}
tcMatchPats (pat:pats) expected_ty
= unifyFunTy expected_ty `thenTc` \ (arg_ty, rest_ty) ->
- tcPat tcPatBndr_NoSigs pat arg_ty `thenTc` \ (pat', lie_req, pat_tvs, pat_ids, lie_avail) ->
+ tcPat tcMonoPatBndr pat arg_ty `thenTc` \ (pat', lie_req, pat_tvs, pat_ids, lie_avail) ->
tcMatchPats pats rest_ty `thenTc` \ (rhs_ty, pats', lie_reqs, pats_tvs, pats_ids, lie_avails) ->
returnTc ( rhs_ty,
pat':pats',
%* *
%************************************************************************
+Typechecking statements is rendered a bit tricky by parallel list comprehensions:
+
+ [ (g x, h x) | ... ; let g v = ...
+ | ... ; let h v = ... ]
+
+It's possible that g,h are overloaded, so we need to feed the LIE from the
+(g x, h x) up through both lots of bindings (so we get the bindInstsOfLocalFuns).
+Similarly if we had an existential pattern match:
+
+ data T = forall a. Show a => C a
+
+ [ (show x, show y) | ... ; C x <- ...
+ | ... ; C y <- ... ]
+
+Then we need the LIE from (show x, show y) to be simplified against
+the bindings for x and y.
+
+It's difficult to do this in parallel, so we rely on the renamer to
+ensure that g,h and x,y don't duplicate, and simply grow the environment.
+So the binders of the first parallel group will be in scope in the second
+group. But that's fine; there's no shadowing to worry about.
\begin{code}
-tcParStep src_loc stmts
- = newTyVarTy (mkArrowKind liftedTypeKind liftedTypeKind) `thenTc` \ m ->
- newTyVarTy liftedTypeKind `thenTc` \ elt_ty ->
- unifyListTy (mkAppTy m elt_ty) `thenTc_`
-
- tcStmts ListComp (mkAppTy m) elt_ty src_loc stmts `thenTc` \ ((stmts', val_env), stmts_lie) ->
- returnTc (stmts', val_env, stmts_lie)
-
-tcStmts :: StmtCtxt
- -> (TcType -> TcType) -- m, the relationship type of pat and rhs in pat <- rhs
- -> TcType -- elt_ty, where type of the comprehension is (m elt_ty)
- -> SrcLoc
+tcStmts do_or_lc m_ty stmts
+ = tcStmtsAndThen (:) do_or_lc m_ty stmts (returnTc ([], emptyLIE))
+
+tcStmtsAndThen
+ :: (TcStmt -> thing -> thing) -- Combiner
+ -> StmtCtxt
+ -> (TcType -> TcType, TcType) -- m, the relationship type of pat and rhs in pat <- rhs
+ -- elt_ty, where type of the comprehension is (m elt_ty)
-> [RenamedStmt]
- -> TcM (([TcStmt], [(Name, TcId)]), LIE)
-
-tcStmts do_or_lc m elt_ty loc (ParStmtOut bndrstmtss : stmts)
- = let stmtss = map snd bndrstmtss in
- mapAndUnzip3Tc (tcParStep loc) stmtss `thenTc` \ (stmtss', val_envs, lies) ->
- let outstmts = zip (map (map snd) val_envs) stmtss'
- lie = plusLIEs lies
- new_val_env = concat val_envs
- in
- tcExtendLocalValEnv new_val_env (
- tcStmts do_or_lc m elt_ty loc stmts) `thenTc` \ ((stmts', rest_val_env), stmts_lie) ->
- returnTc ((ParStmtOut outstmts : stmts', rest_val_env ++ new_val_env), lie `plusLIE` stmts_lie)
+ -> TcM (thing, LIE)
+ -> TcM (thing, LIE)
-tcStmts do_or_lc m elt_ty loc (stmt@(ReturnStmt exp) : stmts)
- = ASSERT( null stmts )
- tcSetErrCtxt (stmtCtxt do_or_lc stmt) $
- tcExpr exp elt_ty `thenTc` \ (exp', exp_lie) ->
- returnTc (([ReturnStmt exp'], []), exp_lie)
-
- -- ExprStmt at the end
-tcStmts do_or_lc m elt_ty loc [stmt@(ExprStmt exp src_loc)]
- = tcSetErrCtxt (stmtCtxt do_or_lc stmt) $
- tcExpr exp (m elt_ty) `thenTc` \ (exp', exp_lie) ->
- returnTc (([ExprStmt exp' src_loc], []), exp_lie)
-
- -- ExprStmt not at the end
-tcStmts do_or_lc m elt_ty loc (stmt@(ExprStmt exp src_loc) : stmts)
- = ASSERT( isDoStmt do_or_lc )
- tcAddSrcLoc src_loc (
- tcSetErrCtxt (stmtCtxt do_or_lc stmt) $
- -- exp has type (m tau) for some tau (doesn't matter what)
- newTyVarTy openTypeKind `thenNF_Tc` \ any_ty ->
- tcExpr exp (m any_ty)
- ) `thenTc` \ (exp', exp_lie) ->
- tcStmts do_or_lc m elt_ty loc stmts `thenTc` \ ((stmts', rest_val_env), stmts_lie) ->
- returnTc ((ExprStmt exp' src_loc : stmts', rest_val_env),
- exp_lie `plusLIE` stmts_lie)
-
-tcStmts do_or_lc m elt_ty loc (stmt@(GuardStmt exp src_loc) : stmts)
- = ASSERT( not (isDoStmt do_or_lc) )
- tcSetErrCtxt (stmtCtxt do_or_lc stmt) (
- tcAddSrcLoc src_loc $
- tcExpr exp boolTy
- ) `thenTc` \ (exp', exp_lie) ->
- tcStmts do_or_lc m elt_ty loc stmts `thenTc` \ ((stmts', rest_val_env), stmts_lie) ->
- -- ZZ is this right?
- returnTc ((GuardStmt exp' src_loc : stmts', rest_val_env),
- exp_lie `plusLIE` stmts_lie)
-
-tcStmts do_or_lc m elt_ty loc (stmt@(BindStmt pat exp src_loc) : stmts)
+ -- Base case
+tcStmtsAndThen combine do_or_lc m_ty [] do_next
+ = do_next
+
+ -- LetStmt
+tcStmtsAndThen combine do_or_lc m_ty (LetStmt binds : stmts) do_next
+ = tcBindsAndThen -- No error context, but a binding group is
+ (glue_binds combine) -- rather a large thing for an error context anyway
+ binds
+ (tcStmtsAndThen combine do_or_lc m_ty stmts do_next)
+
+ -- BindStmt
+tcStmtsAndThen combine do_or_lc m_ty@(m,elt_ty) (stmt@(BindStmt pat exp src_loc) : stmts) do_next
= tcAddSrcLoc src_loc (
tcSetErrCtxt (stmtCtxt do_or_lc stmt) $
- newTyVarTy liftedTypeKind `thenNF_Tc` \ pat_ty ->
- tcPat tcPatBndr_NoSigs pat pat_ty `thenTc` \ (pat', pat_lie, pat_tvs, pat_ids, avail) ->
- tcExpr exp (m pat_ty) `thenTc` \ (exp', exp_lie) ->
+ newTyVarTy liftedTypeKind `thenNF_Tc` \ pat_ty ->
+ tcPat tcMonoPatBndr pat pat_ty `thenTc` \ (pat', pat_lie, pat_tvs, pat_ids, avail) ->
+ tcExpr exp (m pat_ty) `thenTc` \ (exp', exp_lie) ->
returnTc (pat', exp',
pat_lie `plusLIE` exp_lie,
pat_tvs, pat_ids, avail)
let
new_val_env = bagToList pat_bndrs
pat_ids = map snd new_val_env
- pat_tv_list = bagToList pat_tvs
in
-- Do the rest; we don't need to add the pat_tvs to the envt
-- because they all appear in the pat_ids's types
tcExtendLocalValEnv new_val_env (
- tcStmts do_or_lc m elt_ty loc stmts
- ) `thenTc` \ ((stmts', rest_val_env), stmts_lie) ->
-
+ tcStmtsAndThen combine do_or_lc m_ty stmts do_next
+ ) `thenTc` \ (thing, stmts_lie) ->
-- Reinstate context for existential checks
- tcSetErrCtxt (stmtCtxt do_or_lc stmt) $
- tcExtendGlobalTyVars (tyVarsOfType (m elt_ty)) $
- tcAddErrCtxtM (sigPatCtxt pat_tv_list pat_ids) $
-
- checkSigTyVars pat_tv_list emptyVarSet `thenTc` \ zonked_pat_tvs ->
-
- tcSimplifyAndCheck
- (text ("the existential context of a data constructor"))
- (mkVarSet zonked_pat_tvs)
- lie_avail stmts_lie `thenTc` \ (final_lie, dict_binds) ->
-
- -- ZZ we have to be sure that concating the val_env lists preserves
- -- shadowing properly...
- returnTc ((BindStmt pat' exp' src_loc :
- consLetStmt (mkMonoBind dict_binds [] Recursive) stmts',
- rest_val_env ++ new_val_env),
+ tcSetErrCtxt (stmtCtxt do_or_lc stmt) $
+ tcCheckExistentialPat pat_ids pat_tvs lie_avail
+ stmts_lie (m elt_ty) `thenTc` \ (final_lie, dict_binds) ->
+
+ returnTc (combine (BindStmt pat' exp' src_loc)
+ (glue_binds combine Recursive dict_binds thing),
lie_req `plusLIE` final_lie)
-tcStmts do_or_lc m elt_ty loc (LetStmt binds : stmts)
- = tcBindsAndThen -- No error context, but a binding group is
- combine -- rather a large thing for an error context anyway
- binds
- (tcStmts do_or_lc m elt_ty loc stmts) `thenTc` \ ((stmts', rest_val_env), lie) ->
- -- ZZ fix val_env
- returnTc ((stmts', rest_val_env), lie)
- where
- combine is_rec binds' (stmts', val_env) = (consLetStmt (mkMonoBind binds' [] is_rec) stmts', undefined)
-tcStmts do_or_lc m elt_ty loc [] = returnTc (([], []), emptyLIE)
+ -- ParStmt
+tcStmtsAndThen combine do_or_lc m_ty (ParStmtOut bndr_stmts_s : stmts) do_next
+ = loop bndr_stmts_s `thenTc` \ ((pairs', thing), lie) ->
+ returnTc (combine (ParStmtOut pairs') thing, lie)
+ where
+ loop []
+ = tcStmtsAndThen combine do_or_lc m_ty stmts do_next `thenTc` \ (thing, stmts_lie) ->
+ returnTc (([], thing), stmts_lie)
+
+ loop ((bndrs,stmts) : pairs)
+ = tcStmtsAndThen
+ combine_par ListComp (mkListTy, not_required) stmts
+ (tcLookupLocalIds bndrs `thenNF_Tc` \ bndrs' ->
+ loop pairs `thenTc` \ ((pairs', thing), lie) ->
+ returnTc (([], (bndrs', pairs', thing)), lie)) `thenTc` \ ((stmts', (bndrs', pairs', thing)), lie) ->
+
+ returnTc ( ((bndrs',stmts') : pairs', thing), lie)
+
+ combine_par stmt (stmts, thing) = (stmt:stmts, thing)
+ not_required = panic "tcStmtsAndThen: elt_ty"
+
+ -- The simple-statment case
+tcStmtsAndThen combine do_or_lc m_ty (stmt:stmts) do_next
+ = tcSetErrCtxt (stmtCtxt do_or_lc stmt) (
+ tcSimpleStmt do_or_lc m_ty stmt (null stmts)
+ ) `thenTc` \ (stmt', stmt_lie) ->
+
+ tcStmtsAndThen combine do_or_lc m_ty stmts do_next `thenTc` \ (thing, stmts_lie) ->
+
+ returnTc (combine stmt' thing,
+ stmt_lie `plusLIE` stmts_lie)
+
+
+------------------------------
+ -- ReturnStmt
+tcSimpleStmt do_or_lc (_,elt_ty) (ReturnStmt exp) is_last_stmt
+ = ASSERT( is_last_stmt )
+ tcExpr exp elt_ty `thenTc` \ (exp', exp_lie) ->
+ returnTc (ReturnStmt exp', exp_lie)
+
+ -- ExprStmt
+tcSimpleStmt do_or_lc (m, elt_ty) (ExprStmt exp src_loc) is_last_stmt
+ = tcAddSrcLoc src_loc $
+ (if is_last_stmt then -- do { ... ; wuggle } wuggle : m elt_ty
+ returnNF_Tc elt_ty
+ else -- do { ... ; wuggle ; .... } wuggle : m any_ty
+ ASSERT( isDoStmt do_or_lc )
+ newTyVarTy openTypeKind
+ ) `thenNF_Tc` \ arg_ty ->
+ tcExpr exp (m arg_ty) `thenTc` \ (exp', exp_lie) ->
+ returnTc (ExprStmt exp' src_loc, exp_lie)
+
+ -- GuardStmt
+tcSimpleStmt do_or_lc m_ty (GuardStmt exp src_loc) is_last_stmt
+ = ASSERT( not (isDoStmt do_or_lc) )
+ tcAddSrcLoc src_loc $
+ tcExpr exp boolTy `thenTc` \ (exp', exp_lie) ->
+ returnTc (GuardStmt exp' src_loc, exp_lie)
+
+------------------------------
+glue_binds combine is_rec binds thing
+ | nullMonoBinds binds = thing
+ | otherwise = combine (LetStmt (mkMonoBind binds [] is_rec)) thing
isDoStmt DoStmt = True
isDoStmt other = False
module TcMonad(
TcType,
TcTauType, TcPredType, TcThetaType, TcRhoType,
- TcTyVar, TcTyVarSet,
+ TcTyVar, TcTyVarSet, TcClassContext,
TcKind,
TcM, NF_TcM, TcDown, TcEnv,
import Bag ( Bag, emptyBag, isEmptyBag,
foldBag, unitBag, unionBags, snocBag )
-import Class ( Class )
+import Class ( Class, ClassContext )
import Name ( Name )
import Var ( Id, TyVar, newMutTyVar, newSigTyVar, readMutTyVar, writeMutTyVar )
import VarEnv ( TidyEnv, emptyTidyEnv )
-- a cannot occur inside a MutTyVar in T; that is,
-- T is "flattened" before quantifying over a
-type TcPredType = PredType
-type TcThetaType = ThetaType
-type TcRhoType = RhoType
-type TcTauType = TauType
-type TcKind = TcType
+type TcClassContext = ClassContext
+type TcPredType = PredType
+type TcThetaType = ThetaType
+type TcRhoType = RhoType
+type TcTauType = TauType
+type TcKind = TcType
\end{code}
data InstOrigin
= OccurrenceOf Id -- Occurrence of an overloaded identifier
+ | IPOcc Name -- Occurrence of an implicit parameter
+ | IPBind Name -- Binding site of an implicit parameter
+
| RecordUpdOrigin
| DataDeclOrigin -- Typechecking a data declaration
where
pp_orig (OccurrenceOf id)
= hsep [ptext SLIT("use of"), quotes (ppr id)]
+ pp_orig (IPOcc name)
+ = hsep [ptext SLIT("use of implicit parameter"), quotes (char '?' <> ppr name)]
+ pp_orig (IPBind name)
+ = hsep [ptext SLIT("binding for implicit parameter"), quotes (char '?' <> ppr name)]
pp_orig (LiteralOrigin lit)
= hsep [ptext SLIT("the literal"), quotes (ppr lit)]
pp_orig (PatOrigin pat)
newKindVar, tcInstSigVar,
zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
)
-import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
- instFunDeps, instFunDepsOfTheta )
-import FunDeps ( oclose )
+import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
+import FunDeps ( grow )
import TcUnify ( unifyKind, unifyOpenTypeKind )
+import Unify ( allDistinctTyVars )
import Type ( Type, Kind, PredType(..), ThetaType, SigmaType, TauType,
mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
zipFunTys, hoistForAllTys,
import Class ( ClassContext, classArity, classTyCon )
import Name ( Name )
import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
-import UniqFM ( elemUFM )
import BasicTypes ( Boxity(..), RecFlag(..), isRec )
import SrcLoc ( SrcLoc )
import Util ( mapAccumL, isSingleton )
where
sigma_ty = mkSigmaTy forall_tyvars theta tau
tau_vars = tyVarsOfType tau
- fds = instFunDepsOfTheta theta
- extended_tau_vars = oclose fds tau_vars
+ extended_tau_vars = grow theta tau_vars
is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
- not (ct_var `elemUFM` extended_tau_vars)
+ not (ct_var `elemVarSet` extended_tau_vars)
is_free ct_var = not (ct_var `elem` forall_tyvars)
check_pred pred = checkTc (not any_ambig) (ambigErr pred sigma_ty) `thenTc_`
tyvar_tys'
theta' tau' `thenNF_Tc` \ inst ->
-- We make a Method even if it's not overloaded; no harm
- instFunDeps SignatureOrigin theta' `thenNF_Tc` \ fds ->
- returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
+ returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
where
name = idName poly_id
\end{code}
\begin{code}
checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
-> TcTyVarSet -- Tyvars that are free in the type signature
- -- These should *already* be in the global-var set, and are
- -- used here only to improve the error message
- -> TcM [TcTyVar] -- Zonked signature type variables
+ -- Not necessarily zonked
+ -- These should *already* be in the free-in-env set,
+ -- and are used here only to improve the error message
+ -> TcM [TcTyVar] -- Zonked signature type variables
checkSigTyVars [] free = returnTc []
-
checkSigTyVars sig_tyvars free_tyvars
= zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
tcGetGlobalTyVars `thenNF_Tc` \ globals ->
- checkTcM (all_ok sig_tys globals)
+ checkTcM (allDistinctTyVars sig_tys globals)
(complain sig_tys globals) `thenTc_`
returnTc (map (getTyVar "checkSigTyVars") sig_tys)
where
- all_ok [] acc = True
- all_ok (ty:tys) acc = case getTyVar_maybe ty of
- Nothing -> False -- Point (a)
- Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
- | otherwise -> all_ok tys (acc `extendVarSet` tv)
-
-
complain sig_tys globals
= -- For the in-scope ones, zonk them and construct a map
-- from the zonked tyvar to the in-scope one
ambigErr pred ty
= sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
nest 4 (ptext SLIT("for the type:") <+> ppr ty),
- nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
+ nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
+ ptext SLIT("must be reachable from the type after the =>"))]
freeErr pred ty
= sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
\section[TcPat]{Typechecking patterns}
\begin{code}
-module TcPat ( tcPat, tcPatBndr_NoSigs, simpleHsLitTy, badFieldCon, polyPatSig ) where
+module TcPat ( tcPat, tcMonoPatBndr, simpleHsLitTy, badFieldCon, polyPatSig ) where
#include "HsVersions.h"
import TcMonad
import Inst ( InstOrigin(..),
- emptyLIE, plusLIE, LIE,
+ emptyLIE, plusLIE, LIE, mkLIE, unitLIE, instToId,
newMethod, newOverloadedLit, newDicts, newClassDicts
)
-import Name ( Name, getOccName, getSrcLoc )
+import Id ( mkVanillaId )
+import Name ( Name )
import FieldLabel ( fieldLabelName )
-import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupGlobalId, newLocalId )
+import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupGlobalId )
import TcType ( TcType, TcTyVar, tcInstTyVars, newTyVarTy )
import TcMonoType ( tcHsSigType )
import TcUnify ( unifyTauTy, unifyListTy, unifyTupleTy )
%************************************************************************
\begin{code}
--- This is the right function to pass to tcPat when there are no signatures
-tcPatBndr_NoSigs binder_name pat_ty
- = -- Need to make a new, monomorphic, Id
- -- The binder_name is already being used for the polymorphic Id
- newLocalId (getOccName binder_name) pat_ty loc `thenNF_Tc` \ bndr_id ->
- returnTc bndr_id
- where
- loc = getSrcLoc binder_name
+-- This is the right function to pass to tcPat when
+-- we're looking at a lambda-bound pattern,
+-- so there's no polymorphic guy to worry about
+tcMonoPatBndr binder_name pat_ty = returnTc (mkVanillaId binder_name pat_ty)
\end{code}
-- cf tcExpr on LitLits
= tcLookupClass cCallableClassName `thenNF_Tc` \ cCallableClass ->
newDicts (LitLitOrigin (_UNPK_ s))
- [mkClassPred cCallableClass [pat_ty]] `thenNF_Tc` \ (dicts, _) ->
- returnTc (LitPat (HsLitLit s pat_ty) pat_ty, dicts, emptyBag, emptyBag, emptyLIE)
+ [mkClassPred cCallableClass [pat_ty]] `thenNF_Tc` \ dicts ->
+ returnTc (LitPat (HsLitLit s pat_ty) pat_ty, mkLIE dicts, emptyBag, emptyBag, emptyLIE)
tcPat tc_bndr pat@(LitPatIn lit@(HsString _)) pat_ty
= unifyTauTy pat_ty stringTy `thenTc_`
tcPat tc_bndr pat@(NPatIn over_lit) pat_ty
= newOverloadedLit (PatOrigin pat) over_lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie1) ->
tcLookupGlobalId eqName `thenNF_Tc` \ eq_sel_id ->
- newMethod origin eq_sel_id [pat_ty] `thenNF_Tc` \ (lie2, eq_id) ->
+ newMethod origin eq_sel_id [pat_ty] `thenNF_Tc` \ eq ->
- returnTc (NPat lit' pat_ty (HsApp (HsVar eq_id) over_lit_expr),
- lie1 `plusLIE` lie2,
+ returnTc (NPat lit' pat_ty (HsApp (HsVar (instToId eq)) over_lit_expr),
+ lie1 `plusLIE` unitLIE eq,
emptyBag, emptyBag, emptyLIE)
where
origin = PatOrigin pat
tcLookupGlobalId minus `thenNF_Tc` \ minus_sel_id ->
tcLookupGlobalId geName `thenNF_Tc` \ ge_sel_id ->
newOverloadedLit origin lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie1) ->
- newMethod origin ge_sel_id [pat_ty] `thenNF_Tc` \ (lie2, ge_id) ->
- newMethod origin minus_sel_id [pat_ty] `thenNF_Tc` \ (lie3, minus_id) ->
+ newMethod origin ge_sel_id [pat_ty] `thenNF_Tc` \ ge ->
+ newMethod origin minus_sel_id [pat_ty] `thenNF_Tc` \ minus ->
returnTc (NPlusKPat bndr_id i pat_ty
- (SectionR (HsVar ge_id) over_lit_expr)
- (SectionR (HsVar minus_id) over_lit_expr),
- lie1 `plusLIE` lie2 `plusLIE` lie3,
+ (SectionR (HsVar (instToId ge)) over_lit_expr)
+ (SectionR (HsVar (instToId minus)) over_lit_expr),
+ lie1 `plusLIE` mkLIE [ge,minus],
emptyBag, unitBag (name, bndr_id), emptyLIE)
where
origin = PatOrigin pat
ex_tvs' = take n_ex_tvs all_tvs'
result_ty = mkTyConApp tycon (drop n_ex_tvs ty_args')
in
- newClassDicts (PatOrigin pat) ex_theta' `thenNF_Tc` \ (lie_avail, dicts) ->
+ newClassDicts (PatOrigin pat) ex_theta' `thenNF_Tc` \ dicts ->
-- Check overall type matches
unifyTauTy pat_ty result_ty `thenTc_`
- returnTc (data_con, ex_tvs', dicts, lie_avail, arg_tys')
+ returnTc (data_con, ex_tvs', map instToId dicts, mkLIE dicts, arg_tys')
\end{code}
------------------------------------------------------
import HscTypes ( PackageRuleBase )
import TcHsSyn ( TypecheckedRuleDecl, mkHsLet )
import TcMonad
-import TcSimplify ( tcSimplifyToDicts, tcSimplifyAndCheck )
-import TcType ( zonkTcTypes, zonkTcTyVarToTyVar, newTyVarTy )
+import TcSimplify ( tcSimplifyToDicts, tcSimplifyInferCheck )
+import TcType ( zonkTcTyVarToTyVar, newTyVarTy )
import TcIfaceSig ( tcCoreExpr, tcCoreLamBndrs, tcVar )
import TcMonoType ( kcHsSigType, tcHsSigType, tcTyVars, checkSigTyVars )
import TcExpr ( tcExpr )
-import TcEnv ( tcExtendLocalValEnv, tcExtendTyVarEnv, tcGetGlobalTyVars, isLocalThing )
+import TcEnv ( tcExtendLocalValEnv, tcExtendTyVarEnv, isLocalThing )
import Rules ( extendRuleBase )
import Inst ( LIE, plusLIEs, instToId )
-import Id ( idType, idName, mkVanillaId )
+import Id ( idName, mkVanillaId )
import Module ( Module )
import VarSet
-import Type ( tyVarsOfTypes, openTypeKind )
-import Bag ( bagToList )
+import Type ( tyVarsOfType, openTypeKind )
import List ( partition )
import Outputable
\end{code}
) `thenTc` \ (sig_tyvars, ids, lhs', rhs', lhs_lie, rhs_lie) ->
-- Check that LHS has no overloading at all
- tcSimplifyToDicts lhs_lie `thenTc` \ (lhs_dicts, lhs_binds) ->
- checkSigTyVars sig_tyvars emptyVarSet `thenTc_`
+ tcSimplifyToDicts lhs_lie `thenTc` \ (lhs_dicts, lhs_binds) ->
+ checkSigTyVars sig_tyvars emptyVarSet `thenTc_`
-- Gather the template variables and tyvars
let
- tpl_ids = map instToId (bagToList lhs_dicts) ++ ids
+ tpl_ids = map instToId lhs_dicts ++ ids
-- IMPORTANT! We *quantify* over any dicts that appear in the LHS
-- Reason:
-- See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
in
- -- Gather type variables to quantify over
- -- and turn them into real TyVars (just as in TcBinds.tcBindWithSigs)
- zonkTcTypes (rule_ty : map idType tpl_ids) `thenNF_Tc` \ zonked_tys ->
- tcGetGlobalTyVars `thenNF_Tc` \ free_tyvars ->
- let
- poly_tyvars = tyVarsOfTypes zonked_tys `minusVarSet` free_tyvars
- -- There can be tyvars free in the environment, if there are
- -- monomorphic overloaded top-level bindings. Sigh.
- in
- mapTc zonkTcTyVarToTyVar (varSetElems poly_tyvars) `thenTc` \ tvs ->
-
-- RHS can be a bit more lenient. In particular,
-- we let constant dictionaries etc float outwards
- tcSimplifyAndCheck (text "tcRule") (mkVarSet tvs)
- lhs_dicts rhs_lie `thenTc` \ (lie', rhs_binds) ->
+ tcSimplifyInferCheck (text "tcRule")
+ (varSetElems (tyVarsOfType rule_ty))
+ lhs_dicts rhs_lie `thenTc` \ (forall_tvs', lie', rhs_binds) ->
+ mapTc zonkTcTyVarToTyVar forall_tvs' `thenTc` \ tvs ->
returnTc (lie', HsRule name tvs
(map RuleBndr tpl_ids) -- yuk
(mkHsLet lhs_binds lhs')
%
\section[TcSimplify]{TcSimplify}
-Notes:
-
-Inference (local definitions)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the inst constrains a local type variable, then
- [ReduceMe] if it's a literal or method inst, reduce it
-
- [DontReduce] otherwise see whether the inst is just a constant
- if succeed, use it
- if not, add original to context
- This check gets rid of constant dictionaries without
- losing sharing.
-
-If the inst does not constrain a local type variable then
- [Free] then throw it out as free.
-
-Inference (top level definitions)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the inst does not constrain a local type variable, then
- [FreeIfTautological] try for tautology;
- if so, throw it out as free
- (discarding result of tautology check)
- if not, make original inst part of the context
- (eliminating superclasses as usual)
-
-If the inst constrains a local type variable, then
- as for inference (local defns)
-
-
-Checking (local defns)
-~~~~~~~~
-If the inst constrains a local type variable then
- [ReduceMe] reduce (signal error on failure)
-
-If the inst does not constrain a local type variable then
- [Free] throw it out as free.
-
-Checking (top level)
-~~~~~~~~~~~~~~~~~~~~
-If the inst constrains a local type variable then
- as for checking (local defns)
-
-If the inst does not constrain a local type variable then
- as for checking (local defns)
-
-
-
-Checking once per module
-~~~~~~~~~~~~~~~~~~~~~~~~~
-For dicts of the form (C a), where C is a std class
- and "a" is a type variable,
- [DontReduce] add to context
-
-otherwise [ReduceMe] always reduce
-
-[NB: we may generate one Tree [Int] dict per module, so
- sharing is not complete.]
-
-Sort out ambiguity at the end.
-
-Principal types
-~~~~~~~~~~~~~~~
-class C a where
- op :: a -> a
-
-f x = let g y = op (y::Int) in True
-
-Here the principal type of f is (forall a. a->a)
-but we'll produce the non-principal type
- f :: forall a. C Int => a -> a
-
-
-Ambiguity
-~~~~~~~~~
-Consider this:
-
- instance C (T a) Int where ...
- instance C (T a) Bool where ...
-
-and suppose we infer a context
-
- C (T x) y
-
-from some expression, where x and y are type varibles,
-and x is ambiguous, and y is being quantified over.
-Should we complain, or should we generate the type
-
- forall x y. C (T x) y => <type not involving x>
-
-The idea is that at the call of the function we might
-know that y is Int (say), so the "x" isn't really ambiguous.
-Notice that we have to add "x" to the type variables over
-which we generalise.
-
-Something similar can happen even if C constrains only ambiguous
-variables. Suppose we infer the context
-
- C [x]
-
-where x is ambiguous. Then we could infer the type
-
- forall x. C [x] => <type not involving x>
-
-in the hope that at the call site there was an instance
-decl such as
-
- instance Num a => C [a] where ...
-
-and hence the default mechanism would resolve the "a".
\begin{code}
module TcSimplify (
- tcSimplify, tcSimplifyAndCheck, tcSimplifyToDicts,
- tcSimplifyTop, tcSimplifyThetas, tcSimplifyCheckThetas,
- bindInstsOfLocalFuns, partitionPredsOfLIE
+ tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck,
+ tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
+ tcSimplifyThetas, tcSimplifyCheckThetas,
+ bindInstsOfLocalFuns
) where
#include "HsVersions.h"
import TcMonad
import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
- tyVarsOfInst,
- isDict, isClassDict, isMethod, notFunDep,
+ tyVarsOfInst, predsOfInsts,
+ isDict, isClassDict,
isStdClassTyVarDict, isMethodFor,
- instToId, instBindingRequired, instCanBeGeneralised,
- newDictFromOld, newFunDepFromDict,
+ instToId, tyVarsOfInsts,
+ instBindingRequired, instCanBeGeneralised,
+ newDictsFromOld, instMentionsIPs,
getDictClassTys, getIPs, isTyVarDict,
- getDictPred_maybe, getMethodTheta_maybe,
instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
Inst, LIE, pprInsts, pprInstsInFull,
- mkLIE, emptyLIE, unitLIE, consLIE, plusLIE,
+ mkLIE,
lieToList
)
import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
-import InstEnv ( lookupInstEnv, InstLookupResult(..) )
+import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-import TcType ( TcTyVarSet )
+import TcType ( zonkTcTyVarsAndFV )
import TcUnify ( unifyTauTy )
import Id ( idType )
+import Name ( Name )
+import NameSet ( mkNameSet )
import Class ( Class, classBigSig )
+import FunDeps ( oclose, grow, improve )
import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
import Type ( Type, ClassContext,
- mkTyVarTy, getTyVar,
+ mkTyVarTy, getTyVar,
isTyVarTy, splitSigmaTy, tyVarsOfTypes
)
import Subst ( mkTopTyVarSubst, substClasses )
-import PprType ( pprConstraint )
+import PprType ( pprClassPred )
import TysWiredIn ( unitTy )
import VarSet
import FiniteMap
import ListSetOps ( equivClasses )
import Util ( zipEqual, mapAccumL )
import List ( partition )
-import Maybe ( fromJust )
-import Maybes ( maybeToBool )
import CmdLineOpts
\end{code}
%************************************************************************
%* *
-\subsection[tcSimplify-main]{Main entry function}
+\subsection{NOTES}
%* *
%************************************************************************
-The main wrapper is @tcSimplify@. It just calls @tcSimpl@, but with
-the ``don't-squash-consts'' flag set depending on top-level ness. For
-top level defns we *do* squash constants, so that they stay local to a
-single defn. This makes things which are inlined more likely to be
-exportable, because their constants are "inside". Later passes will
-float them out if poss, after inlinings are sorted out.
+ --------------------------------------
+ Notes on quantification
+ --------------------------------------
+
+Suppose we are about to do a generalisation step.
+We have in our hand
+
+ G the environment
+ T the type of the RHS
+ C the constraints fromm that RHS
+
+The game is to figure out
+
+ Q the set of type variables over which to quantify
+ Ct the constraints we will *not* quantify over
+ Cq the constraints we will quantify over
+
+So we're going to infer the type
+
+ forall Q. Cq => T
+
+and float the constraints Ct further outwards.
+
+Here are the things that *must* be true:
+
+ (A) Q intersect fv(G) = EMPTY limits how big Q can be
+ (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
+
+(A) says we can't quantify over a variable that's free in the
+environment. (B) says we must quantify over all the truly free
+variables in T, else we won't get a sufficiently general type. We do
+not *need* to quantify over any variable that is fixed by the free
+vars of the environment G.
+
+ BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
+
+Example: class H x y | x->y where ...
+
+ fv(G) = {a} C = {H a b, H c d}
+ T = c -> b
+
+ (A) Q intersect {a} is empty
+ (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
+
+ So Q can be {c,d}, {b,c,d}
+
+Other things being equal, however, we'd like to quantify over as few
+variables as possible: smaller types, fewer type applications, more
+constraints can get into Ct instead of Cq.
+
+
+-----------------------------------------
+We will make use of
+
+ fv(T) the free type vars of T
+
+ oclose(vs,C) The result of extending the set of tyvars vs
+ using the functional dependencies from C
+
+ grow(vs,C) The result of extend the set of tyvars vs
+ using all conceivable links from C.
+
+ E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
+ Then grow(vs,C) = {a,b,c}
+
+ Note that grow(vs,C) `superset` grow(vs,simplify(C))
+ That is, simplfication can only shrink the result of grow.
+
+Notice that
+ oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
+ grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
+
+
+-----------------------------------------
+
+Choosing Q
+~~~~~~~~~~
+Here's a good way to choose Q:
+
+ Q = grow( fv(T), C ) \ oclose( fv(G), C )
+
+That is, quantify over all variable that that MIGHT be fixed by the
+call site (which influences T), but which aren't DEFINITELY fixed by
+G. This choice definitely quantifies over enough type variables,
+albeit perhaps too many.
+
+Why grow( fv(T), C ) rather than fv(T)? Consider
+
+ class H x y | x->y where ...
+
+ T = c->c
+ C = (H c d)
+
+ If we used fv(T) = {c} we'd get the type
+
+ forall c. H c d => c -> b
+
+ And then if the fn was called at several different c's, each of
+ which fixed d differently, we'd get a unification error, because
+ d isn't quantified. Solution: quantify d. So we must quantify
+ everything that might be influenced by c.
+
+Why not oclose( fv(T), C )? Because we might not be able to see
+all the functional dependencies yet:
+
+ class H x y | x->y where ...
+ instance H x y => Eq (T x y) where ...
+
+ T = c->c
+ C = (Eq (T c d))
+
+ Now oclose(fv(T),C) = {c}, because the functional dependency isn't
+ apparent yet, and that's wrong. We must really quantify over d too.
+
+
+There really isn't any point in quantifying over any more than
+grow( fv(T), C ), because the call sites can't possibly influence
+any other type variables.
+
+
+
+ --------------------------------------
+ Notes on ambiguity
+ --------------------------------------
+
+It's very hard to be certain when a type is ambiguous. Consider
+
+ class K x
+ class H x y | x -> y
+ instance H x y => K (x,y)
+
+Is this type ambiguous?
+ forall a b. (K (a,b), Eq b) => a -> a
+
+Looks like it! But if we simplify (K (a,b)) we get (H a b) and
+now we see that a fixes b. So we can't tell about ambiguity for sure
+without doing a full simplification. And even that isn't possible if
+the context has some free vars that may get unified. Urgle!
+
+Here's another example: is this ambiguous?
+ forall a b. Eq (T b) => a -> a
+Not if there's an insance decl (with no context)
+ instance Eq (T b) where ...
+
+You may say of this example that we should use the instance decl right
+away, but you can't always do that:
+
+ class J a b where ...
+ instance J Int b where ...
+
+ f :: forall a b. J a b => a -> a
+
+(Notice: no functional dependency in J's class decl.)
+Here f's type is perfectly fine, provided f is only called at Int.
+It's premature to complain when meeting f's signature, or even
+when inferring a type for f.
+
+
+
+However, we don't *need* to report ambiguity right away. It'll always
+show up at the call site.... and eventually at main, which needs special
+treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
+
+So heres the plan. We WARN about probable ambiguity if
+
+ fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
+
+(all tested before quantification).
+That is, all the type variables in Cq must be fixed by the the variables
+in the environment, or by the variables in the type.
+
+Notice that we union before calling oclose. Here's an example:
+
+ class J a b c | a,b -> c
+ fv(G) = {a}
+
+Is this ambiguous?
+ forall b,c. (J a b c) => b -> b
+
+Only if we union {a} from G with {b} from T before using oclose,
+do we see that c is fixed.
+
+It's a bit vague exactly which C we should use for this oclose call. If we
+don't fix enough variables we might complain when we shouldn't (see
+the above nasty example). Nothing will be perfect. That's why we can
+only issue a warning.
+
+
+Can we ever be *certain* about ambiguity? Yes: if there's a constraint
+
+ c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
+
+then c is a "bubble"; there's no way it can ever improve, and it's
+certainly ambiguous. UNLESS it is a constant (sigh). And what about
+the nasty example?
+
+ class K x
+ class H x y | x -> y
+ instance H x y => K (x,y)
+
+Is this type ambiguous?
+ forall a b. (K (a,b), Eq b) => a -> a
+
+Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
+is a "bubble" that's a set of constraints
+
+ Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
+
+Hence another idea. To decide Q start with fv(T) and grow it
+by transitive closure in Cq (no functional dependencies involved).
+Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
+The definitely-ambigous can then float out, and get smashed at top level
+(which squashes out the constants, like Eq (T a) above)
+
+
+ --------------------------------------
+ Notes on implicit parameters
+ --------------------------------------
+
+Consider
+
+ f x = ...?y...
+
+Then we get an LIE like (?y::Int). Doesn't constrain a type variable,
+but we must nevertheless infer a type like
+
+ f :: (?y::Int) => Int -> Int
+
+so that f is passed the value of y at the call site. Is this legal?
+
+ f :: Int -> Int
+ f x = x + ?y
+
+Should f be overloaded on "?y" ? Or does the type signature say that it
+shouldn't be? Our position is that it should be illegal. Otherwise
+you can change the *dynamic* semantics by adding a type signature:
+
+ (let f x = x + ?y -- f :: (?y::Int) => Int -> Int
+ in (f 3, f 3 with ?y=5)) with ?y = 6
+
+ returns (3+6, 3+5)
+vs
+ (let f :: Int -> Int
+ f x = x + ?y
+ in (f 3, f 3 with ?y=5)) with ?y = 6
+
+ returns (3+6, 3+6)
+
+URK! Let's not do this. So this is illegal:
+
+ f :: Int -> Int
+ f x = x + ?y
+
+BOTTOM LINE: you *must* quantify over implicit parameters.
+
+
+ --------------------------------------
+ Notes on principal types
+ --------------------------------------
+
+ class C a where
+ op :: a -> a
+
+ f x = let g y = op (y::Int) in True
+
+Here the principal type of f is (forall a. a->a)
+but we'll produce the non-principal type
+ f :: forall a. C Int => a -> a
+
+
+%************************************************************************
+%* *
+\subsection{tcSimplifyInfer}
+%* *
+%************************************************************************
+
+tcSimplify is called when we *inferring* a type. Here's the overall game plan:
+
+ 1. Compute Q = grow( fvs(T), C )
+
+ 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
+ predicates will end up in Ct; we deal with them at the top level
+
+ 3. Try improvement, using functional dependencies
+
+ 4. If Step 3 did any unification, repeat from step 1
+ (Unification can change the result of 'grow'.)
+
+Note: we don't reduce dictionaries in step 2. For example, if we have
+Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
+after step 2. However note that we may therefore quantify over more
+type variables than we absolutely have to.
+
+For the guts, we need a loop, that alternates context reduction and
+improvement with unification. E.g. Suppose we have
+
+ class C x y | x->y where ...
+
+and tcSimplify is called with:
+ (C Int a, C Int b)
+Then improvement unifies a with b, giving
+ (C Int a, C Int a)
+
+If we need to unify anything, we rattle round the whole thing all over
+again.
+
\begin{code}
-tcSimplify
+tcSimplifyInfer
:: SDoc
- -> TcTyVarSet -- ``Local'' type variables
- -- ASSERT: this tyvar set is already zonked
- -> LIE -- Wanted
- -> TcM (LIE, -- Free
- TcDictBinds, -- Bindings
- LIE) -- Remaining wanteds; no dups
-
-tcSimplify str local_tvs wanted_lie
-{- this is just an optimization, and interferes with implicit params,
- disable it for now. same goes for tcSimplifyAndCheck
- | isEmptyVarSet local_tvs
- = returnTc (wanted_lie, EmptyMonoBinds, emptyLIE)
+ -> [TcTyVar] -- fv(T); type vars
+ -> LIE -- Wanted
+ -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
+ LIE, -- Free
+ TcDictBinds, -- Bindings
+ [TcId]) -- Dict Ids that must be bound here (zonked)
+\end{code}
- | otherwise
--}
- = reduceContext str try_me [] wanteds `thenTc` \ (binds, frees, irreds) ->
+
+\begin{code}
+tcSimplifyInfer doc tau_tvs wanted_lie
+ = inferLoop doc tau_tvs (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
-- Check for non-generalisable insts
+ mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
+
+ returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
+
+inferLoop doc tau_tvs wanteds
+ = -- Step 1
+ zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
+ mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
let
- cant_generalise = filter (not . instCanBeGeneralised) irreds
- in
- checkTc (null cant_generalise)
- (genCantGenErr cant_generalise) `thenTc_`
-
- -- Check for ambiguous insts.
- -- You might think these can't happen (I did) because an ambiguous
- -- inst like (Eq a) will get tossed out with "frees", and eventually
- -- dealt with by tcSimplifyTop.
- -- But we can get stuck with
- -- C a b
- -- where "a" is one of the local_tvs, but "b" is unconstrained.
- -- Then we must yell about the ambiguous b
- -- But we must only do so if "b" really is unconstrained; so
- -- we must grab the global tyvars to answer that question
- tcGetGlobalTyVars `thenNF_Tc` \ global_tvs ->
- let
- avail_tvs = local_tvs `unionVarSet` global_tvs
- (irreds', bad_guys) = partition (isEmptyVarSet . ambig_tv_fn) irreds
- ambig_tv_fn dict = tyVarsOfInst dict `minusVarSet` avail_tvs
+ preds = predsOfInsts wanteds'
+ qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+
+ try_me inst
+ | isFree qtvs inst = Free
+ | isClassDict inst = DontReduceUnlessConstant -- Dicts
+ | otherwise = ReduceMe AddToIrreds -- Lits and Methods
in
- addAmbigErrs ambig_tv_fn bad_guys `thenNF_Tc_`
+ -- Step 2
+ reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+ -- Step 3
+ if no_improvement then
+ returnTc (varSetElems qtvs, frees, binds, irreds)
+ else
+ inferLoop doc tau_tvs wanteds
+\end{code}
+\begin{code}
+isFree qtvs inst
+ = not (tyVarsOfInst inst `intersectsVarSet` qtvs) -- Constrains no quantified vars
+ && null (getIPs inst) -- And no implicit parameter involved
+ -- (see "Notes on implicit parameters")
+\end{code}
- -- Finished
- returnTc (mkLIE frees, binds, mkLIE irreds')
- where
- wanteds = lieToList wanted_lie
- try_me inst
- -- Does not constrain a local tyvar
- | isEmptyVarSet (tyVarsOfInst inst `intersectVarSet` local_tvs)
- && null (getIPs inst)
- = -- if is_top_level then
- -- FreeIfTautological -- Special case for inference on
- -- -- top-level defns
- -- else
- Free
-
- -- We're infering (not checking) the type, and
- -- the inst constrains a local type variable
- | isClassDict inst = DontReduceUnlessConstant -- Dicts
- | otherwise = ReduceMe AddToIrreds -- Lits and Methods
-\end{code}
+%************************************************************************
+%* *
+\subsection{tcSimplifyCheck}
+%* *
+%************************************************************************
-@tcSimplifyAndCheck@ is similar to the above, except that it checks
-that there is an empty wanted-set at the end. It may still return
-some of constant insts, which have to be resolved finally at the end.
+@tcSimplifyCheck@ is used when we know exactly the set of variables
+we are going to quantify over.
\begin{code}
-tcSimplifyAndCheck
+tcSimplifyCheck
:: SDoc
- -> TcTyVarSet -- ``Local'' type variables
- -- ASSERT: this tyvar set is already zonked
- -> LIE -- Given; constrain only local tyvars
+ -> [TcTyVar] -- Quantify over these
+ -> [Inst] -- Given
-> LIE -- Wanted
-> TcM (LIE, -- Free
- TcDictBinds) -- Bindings
+ TcDictBinds) -- Bindings
-tcSimplifyAndCheck str local_tvs given_lie wanted_lie
-{-
- | isEmptyVarSet local_tvs
- -- This can happen quite legitimately; for example in
- -- instance Num Int where ...
- = returnTc (wanted_lie, EmptyMonoBinds)
-
- | otherwise
--}
- = reduceContext str try_me givens wanteds `thenTc` \ (binds, frees, irreds) ->
+tcSimplifyCheck doc qtvs givens wanted_lie
+ = checkLoop doc qtvs givens (lieToList wanted_lie) `thenTc` \ (frees, binds, irreds) ->
-- Complain about any irreducible ones
- mapNF_Tc complain irreds `thenNF_Tc_`
+ complainCheck doc givens irreds `thenNF_Tc_`
-- Done
returnTc (mkLIE frees, binds)
+
+checkLoop doc qtvs givens wanteds
+ = -- Step 1
+ zonkTcTyVarsAndFV qtvs `thenNF_Tc` \ qtvs' ->
+ mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
+ mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ let
+ -- When checking against a given signature we always reduce
+ -- until we find a match against something given, or can't reduce
+ try_me inst | isFree qtvs' inst = Free
+ | otherwise = ReduceMe AddToIrreds
+ in
+ -- Step 2
+ reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+ -- Step 3
+ if no_improvement then
+ returnTc (frees, binds, irreds)
+ else
+ checkLoop doc qtvs givens wanteds
+
+complainCheck doc givens irreds
+ = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
+ mapNF_Tc (addNoInstanceErr doc given_dicts) irreds `thenNF_Tc_`
+ returnTc ()
where
- givens = lieToList given_lie
- wanteds = lieToList wanted_lie
- given_dicts = filter isClassDict givens
+ given_dicts = filter isDict givens
+ -- Filter out methods, which are only added to
+ -- the given set as an optimisation
+\end{code}
+
+
+
+%************************************************************************
+%* *
+\subsection{tcSimplifyAndCheck}
+%* *
+%************************************************************************
+
+@tcSimplifyInferCheck@ is used when we know the consraints we are to simplify
+against, but we don't know the type variables over which we are going to quantify.
+
+\begin{code}
+tcSimplifyInferCheck
+ :: SDoc
+ -> [TcTyVar] -- fv(T)
+ -> [Inst] -- Given
+ -> LIE -- Wanted
+ -> TcM ([TcTyVar], -- Variables over which to quantify
+ LIE, -- Free
+ TcDictBinds) -- Bindings
+
+tcSimplifyInferCheck doc tau_tvs givens wanted
+ = inferCheckLoop doc tau_tvs givens (lieToList wanted) `thenTc` \ (qtvs, frees, binds, irreds) ->
- try_me inst
- -- Does not constrain a local tyvar
- | isEmptyVarSet (tyVarsOfInst inst `intersectVarSet` local_tvs)
- && (not (isMethod inst) || null (getIPs inst))
- = Free
+ -- Complain about any irreducible ones
+ complainCheck doc givens irreds `thenNF_Tc_`
+
+ -- Done
+ returnTc (qtvs, mkLIE frees, binds)
- -- When checking against a given signature we always reduce
- -- until we find a match against something given, or can't reduce
- | otherwise
- = ReduceMe AddToIrreds
+inferCheckLoop doc tau_tvs givens wanteds
+ = -- Step 1
+ zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
+ mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
+ mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
- complain dict = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens ->
- addNoInstanceErr str given_dicts dict
+ let
+ -- Figure out what we are going to generalise over
+ -- You might think it should just be the signature tyvars,
+ -- but in bizarre cases you can get extra ones
+ -- f :: forall a. Num a => a -> a
+ -- f x = fst (g (x, head [])) + 1
+ -- g a b = (b,a)
+ -- Here we infer g :: forall a b. a -> b -> (b,a)
+ -- We don't want g to be monomorphic in b just because
+ -- f isn't quantified over b.
+ qtvs = (tau_tvs' `unionVarSet` tyVarsOfInsts givens') `minusVarSet` gbl_tvs
+ -- We could close gbl_tvs, but its not necessary for
+ -- soundness, and it'll only affect which tyvars, not which
+ -- dictionaries, we quantify over
+
+ -- When checking against a given signature we always reduce
+ -- until we find a match against something given, or can't reduce
+ try_me inst | isFree qtvs inst = Free
+ | otherwise = ReduceMe AddToIrreds
+ in
+ -- Step 2
+ reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+ -- Step 3
+ if no_improvement then
+ returnTc (varSetElems qtvs, frees, binds, irreds)
+ else
+ inferCheckLoop doc tau_tvs givens wanteds
\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{tcSimplifyToDicts}
+%* *
+%************************************************************************
+
On the LHS of transformation rules we only simplify methods and constants,
getting dictionaries. We want to keep all of them unsimplified, to serve
as the available stuff for the RHS of the rule.
So tcSimplifyToDicts squeezes out all Methods.
\begin{code}
-tcSimplifyToDicts :: LIE -> TcM (LIE, TcDictBinds)
+tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
tcSimplifyToDicts wanted_lie
- = reduceContext (text "tcSimplifyToDicts") try_me [] wanteds `thenTc` \ (binds, frees, irreds) ->
+ = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ -- Since try_me doesn't look at types, we don't need to
+ -- do any zonking, so it's safe to call reduceContext directly
ASSERT( null frees )
- returnTc (mkLIE irreds, binds)
+ returnTc (irreds, binds)
+
where
+ doc = text "tcSimplifyToDicts"
wanteds = lieToList wanted_lie
-- Reduce methods and lits only; stop as soon as we get a dictionary
| otherwise = ReduceMe AddToIrreds
\end{code}
-The following function partitions a LIE by a predicate defined
-over `Pred'icates (an unfortunate overloading of terminology!).
-This means it sometimes has to split up `Methods', in which case
-a binding is generated.
-It is used in `with' bindings to extract from the LIE the implicit
-parameters being bound.
+%************************************************************************
+%* *
+\subsection{Filtering at a dynamic binding}
+%* *
+%************************************************************************
+
+When we have
+ let ?x = R in B
+
+we must discharge all the ?x constraints from B. We also do an improvement
+step; if we have ?x::t1 and ?x::t2 we must unify t1, t2. No need to iterate, though.
\begin{code}
-partitionPredsOfLIE pred lie
- = foldlTc (partPreds pred) (emptyLIE, emptyLIE, EmptyMonoBinds) insts
- where insts = lieToList lie
-
--- warning: the term `pred' is overloaded here!
-partPreds pred (lie1, lie2, binds) inst
- | maybeToBool maybe_pred
- = if pred p then
- returnTc (consLIE inst lie1, lie2, binds)
- else
- returnTc (lie1, consLIE inst lie2, binds)
- where maybe_pred = getDictPred_maybe inst
- Just p = maybe_pred
-
--- the assumption is that those satisfying `pred' are being extracted,
--- so we leave the method untouched when nothing satisfies `pred'
-partPreds pred (lie1, lie2, binds1) inst
- | maybeToBool maybe_theta
- = if any pred theta then
- zonkInst inst `thenTc` \ inst' ->
- tcSimplifyToDicts (unitLIE inst') `thenTc` \ (lie3, binds2) ->
- partitionPredsOfLIE pred lie3 `thenTc` \ (lie1', lie2', EmptyMonoBinds) ->
- returnTc (lie1 `plusLIE` lie1',
- lie2 `plusLIE` lie2',
- binds1 `AndMonoBinds` binds2)
- else
- returnTc (lie1, consLIE inst lie2, binds1)
- where maybe_theta = getMethodTheta_maybe inst
- Just theta = maybe_theta
+tcSimplifyIPs :: [Name] -- The implicit parameters bound here
+ -> LIE
+ -> TcM (LIE, TcDictBinds)
+tcSimplifyIPs ip_names wanted_lie
+ = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ -- The irreducible ones should be a subset of the implicit
+ -- parameters we provided
+ ASSERT( all here_ip irreds )
+ returnTc (mkLIE frees, binds)
+
+ where
+ doc = text "tcSimplifyIPs" <+> ppr ip_names
+ wanteds = lieToList wanted_lie
+ ip_set = mkNameSet ip_names
+ here_ip ip = isDict ip && ip `instMentionsIPs` ip_set
-partPreds pred (lie1, lie2, binds) inst
- = returnTc (lie1, consLIE inst lie2, binds)
+ -- Simplify any methods that mention the implicit parameter
+ try_me inst | inst `instMentionsIPs` ip_set = ReduceMe AddToIrreds
+ | otherwise = Free
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
+%* *
+%************************************************************************
+
+When doing a binding group, we may have @Insts@ of local functions.
+For example, we might have...
+\begin{verbatim}
+let f x = x + 1 -- orig local function (overloaded)
+ f.1 = f Int -- two instances of f
+ f.2 = f Float
+ in
+ (f.1 5, f.2 6.7)
+\end{verbatim}
+The point is: we must drop the bindings for @f.1@ and @f.2@ here,
+where @f@ is in scope; those @Insts@ must certainly not be passed
+upwards towards the top-level. If the @Insts@ were binding-ified up
+there, they would have unresolvable references to @f@.
+
+We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
+For each method @Inst@ in the @init_lie@ that mentions one of the
+@Ids@, we create a binding. We return the remaining @Insts@ (in an
+@LIE@), as well as the @HsBinds@ generated.
+
+\begin{code}
+bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
+
+bindInstsOfLocalFuns init_lie local_ids
+ | null overloaded_ids
+ -- Common case
+ = returnTc (init_lie, EmptyMonoBinds)
+
+ | otherwise
+ = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ ASSERT( null irreds )
+ returnTc (mkLIE frees, binds)
+ where
+ doc = text "bindInsts" <+> ppr local_ids
+ wanteds = lieToList init_lie
+ overloaded_ids = filter is_overloaded local_ids
+ is_overloaded id = case splitSigmaTy (idType id) of
+ (_, theta, _) -> not (null theta)
+
+ overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
+ -- so it's worth building a set, so that
+ -- lookup (in isMethodFor) is faster
+
+ try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
+ | otherwise = Free
\end{code}
| Free -- Return as free
- | FreeIfTautological -- Return as free iff it's tautological;
- -- if not, return as irreducible
- -- The FreeIfTautological case is to allow the possibility
- -- of generating functions with types like
- -- f :: C Int => Int -> Int
- -- Here, the C Int isn't a tautology presumably because Int
- -- isn't an instance of C in this module; but perhaps it will
- -- be at f's call site(s). Haskell doesn't allow this at
- -- present.
-
data NoInstanceAction
= Stop -- Fail; no error message
-- (Only used when tautology checking.)
\begin{code}
-type RedState s
- = (Avails s, -- What's available
- [Inst], -- Insts for which try_me returned Free
- [Inst] -- Insts for which try_me returned DontReduce
- )
+type RedState = (Avails, -- What's available
+ [Inst]) -- Insts for which try_me returned Free
-type Avails s = FiniteMap Inst Avail
+type Avails = FiniteMap Inst Avail
data Avail
- = Avail
- TcId -- The "main Id"; that is, the Id for the Inst that
- -- caused this avail to be put into the finite map in the first place
- -- It is this Id that is bound to the RHS.
-
- RHS -- The RHS: an expression whose value is that Inst.
- -- The main Id should be bound to this RHS
-
- [TcId] -- Extra Ids that must all be bound to the main Id.
- -- At the end we generate a list of bindings
- -- { i1 = main_id; i2 = main_id; i3 = main_id; ... }
-
-data RHS
- = NoRhs -- Used for irreducible dictionaries,
- -- which are going to be lambda bound, or for those that are
- -- suppplied as "given" when checking againgst a signature.
- --
- -- NoRhs is also used for Insts like (CCallable f)
+ = Irred -- Used for irreducible dictionaries,
+ -- which are going to be lambda bound
+
+ | BoundTo TcId -- Used for dictionaries for which we have a binding
+ -- e.g. those "given" in a signature
+
+ | NoRhs -- Used for Insts like (CCallable f)
-- where no witness is required.
| Rhs -- Used when there is a RHS
- TcExpr
- Bool -- True => the RHS simply selects a superclass dictionary
- -- from a subclass dictionary.
- -- False => not so.
- -- This is useful info, because superclass selection
- -- is cheaper than building the dictionary using its dfun,
- -- and we can sometimes replace the latter with the former
-
- | PassiveScSel -- Used for as-yet-unactivated RHSs. For example suppose we have
- -- an (Ord t) dictionary; then we put an (Eq t) entry in
- -- the finite map, with an PassiveScSel. Then if the
- -- the (Eq t) binding is ever *needed* we make it an Rhs
- TcExpr
- [Inst] -- List of Insts that are free in the RHS.
- -- If the main Id is subsequently needed, we toss this list into
- -- the needed-inst pool so that we make sure their bindings
- -- will actually be produced.
- --
- -- Invariant: these Insts are already in the finite mapping
-
+ TcExpr -- The RHS
+ [Inst] -- Insts free in the RHS; we need these too
pprAvails avails = vcat (map pprAvail (eltsFM avails))
-pprAvail (Avail main_id rhs ids)
- = ppr main_id <> colon <+> brackets (ppr ids) <+> pprRhs rhs
-
instance Outputable Avail where
ppr = pprAvail
-pprRhs NoRhs = text "<no rhs>"
-pprRhs (Rhs rhs b) = ppr rhs
-pprRhs (PassiveScSel rhs is) = text "passive" <+> ppr rhs
+pprAvail NoRhs = text "<no rhs>"
+pprAvail Irred = text "Irred"
+pprAvail (BoundTo x) = text "Bound to" <+> ppr x
+pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
+\end{code}
+
+Extracting the bindings from a bunch of Avails.
+The bindings do *not* come back sorted in dependency order.
+We assume that they'll be wrapped in a big Rec, so that the
+dependency analyser can sort them out later
+
+The loop startes
+\begin{code}
+bindsAndIrreds :: Avails
+ -> [Inst] -- Wanted
+ -> (TcDictBinds, -- Bindings
+ [Inst]) -- Irreducible ones
+
+bindsAndIrreds avails wanteds
+ = go avails EmptyMonoBinds [] wanteds
+ where
+ go avails binds irreds [] = (binds, irreds)
+
+ go avails binds irreds (w:ws)
+ = case lookupFM avails w of
+ Nothing -> -- Free guys come out here
+ -- (If we didn't do addFree we could use this as the
+ -- criterion for free-ness, and pick up the free ones here too)
+ go avails binds irreds ws
+
+ Just NoRhs -> go avails binds irreds ws
+
+ Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
+
+ Just (BoundTo id) -> go avails new_binds irreds ws
+ where
+ -- For implicit parameters, all occurrences share the same
+ -- Id, so there is no need for synonym bindings
+ new_binds | new_id == id = binds
+ | otherwise = binds `AndMonoBinds` new_bind
+ new_bind = VarMonoBind new_id (HsVar id)
+ new_id = instToId w
+
+ Just (Rhs rhs ws') -> go avails' (binds `AndMonoBinds` new_bind) irreds (ws' ++ ws)
+ where
+ id = instToId w
+ avails' = addToFM avails w (BoundTo id)
+ new_bind = VarMonoBind id rhs
\end{code}
%* *
%************************************************************************
-The main entry point for context reduction is @reduceContext@:
+When the "what to do" predicate doesn't depend on the quantified type variables,
+matters are easier. We don't need to do any zonking, unless the improvement step
+does something, in which case we zonk before iterating.
+
+The "given" set is always empty.
\begin{code}
-reduceContext :: SDoc -> (Inst -> WhatToDo)
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst], -- Free
- [Inst]) -- Irreducible
-
-reduceContext str try_me givens wanteds
- = -- Zonking first
- mapNF_Tc zonkInst givens `thenNF_Tc` \ givens ->
- mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds ->
- -- JRL - process fundeps last. We eliminate fundeps by seeing
- -- what available classes generate them, so we need to process the
- -- classes first. (would it be useful to make LIEs ordered in the first place?)
- let (wantedOther, wantedFds) = partition notFunDep wanteds
- wanteds' = wantedOther ++ wantedFds in
+simpleReduceLoop :: SDoc
+ -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
+ -> [Inst] -- Wanted
+ -> TcM ([Inst], -- Free
+ TcDictBinds,
+ [Inst]) -- Irreducible
+
+simpleReduceLoop doc try_me wanteds
+ = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ if no_improvement then
+ returnTc (frees, binds, irreds)
+ else
+ simpleReduceLoop doc try_me wanteds
+\end{code}
-{-
- pprTrace "reduceContext" (vcat [
+
+
+\begin{code}
+reduceContext :: SDoc
+ -> (Inst -> WhatToDo)
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> NF_TcM (Bool, -- True <=> improve step did no unification
+ [Inst], -- Free
+ TcDictBinds, -- Dictionary bindings
+ [Inst]) -- Irreducible
+
+reduceContext doc try_me givens wanteds
+ =
+{- traceTc (text "reduceContext" <+> (vcat [
text "----------------------",
- str,
+ doc,
text "given" <+> ppr givens,
text "wanted" <+> ppr wanteds,
text "----------------------"
- ]) $
+ ])) `thenNF_Tc_`
+
-}
-- Build the Avail mapping from "givens"
- foldlNF_Tc addGiven emptyFM givens `thenNF_Tc` \ avails ->
+ foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
-- Do the real work
- reduceList (0,[]) try_me wanteds' (avails, [], []) `thenNF_Tc` \ (avails, frees, irreds) ->
+ reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
+
+ -- Do improvement, using everything in avails
+ -- In particular, avails includes all superclasses of everything
+ tcImprove avails `thenTc` \ no_improvement ->
- -- Extract the bindings from avails
- let
- binds = foldFM add_bind EmptyMonoBinds avails
-
- add_bind _ (Avail main_id rhs ids) binds
- = foldr add_synonym (add_rhs_bind rhs binds) ids
- where
- add_rhs_bind (Rhs rhs _) binds = binds `AndMonoBinds` VarMonoBind main_id rhs
- add_rhs_bind other binds = binds
-
- -- Add the trivial {x = y} bindings
- -- The main Id can end up in the list when it's first added passively
- -- and then activated, so we have to filter it out. A bit of a hack.
- add_synonym id binds
- | id /= main_id = binds `AndMonoBinds` VarMonoBind id (HsVar main_id)
- | otherwise = binds
- in
{-
- pprTrace ("reduceContext end") (vcat [
+ traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
- str,
+ doc,
text "given" <+> ppr givens,
text "wanted" <+> ppr wanteds,
text "----",
text "avails" <+> pprAvails avails,
text "frees" <+> ppr frees,
- text "irreds" <+> ppr irreds,
+ text "no_improvement =" <+> ppr no_improvement,
text "----------------------"
- ]) $
+ ])) `thenNF_Tc_`
-}
- returnNF_Tc (binds, frees, irreds)
+ let
+ (binds, irreds) = bindsAndIrreds avails wanteds
+ in
+ returnTc (no_improvement, frees, binds, irreds)
+
+tcImprove avails
+ = tcGetInstEnv `thenTc` \ inst_env ->
+ let
+ preds = predsOfInsts (keysFM avails)
+ -- Avails has all the superclasses etc (good)
+ -- It also has all the intermediates of the deduction (good)
+ -- It does not have duplicates (good)
+ -- NB that (?x::t1) and (?x::t2) will be held separately in avails
+ -- so that improve will see them separate
+ eqns = improve (classInstEnv inst_env) preds
+ in
+ if null eqns then
+ returnTc True
+ else
+ mapTc_ (\ (t1,t2) -> unifyTauTy t1 t2) eqns `thenTc_`
+ returnTc False
\end{code}
The main context-reduction function is @reduce@. Here's its game plan.
-- along with its depth
-> (Inst -> WhatToDo)
-> [Inst]
- -> RedState s
- -> TcM (RedState s)
+ -> RedState
+ -> TcM RedState
\end{code}
@reduce@ is passed
go ws state'
-- Base case: we're done!
-reduce stack try_me wanted state@(avails, frees, irreds)
+reduce stack try_me wanted state
-- It's the same as an existing inst, or a superclass thereof
- | wanted `elemFM` avails
- = returnTc (activate avails wanted, frees, irreds)
+ | isAvailable state wanted
+ = returnTc state
| otherwise
= case try_me wanted of {
- ReduceMe no_instance_action -> -- It should be reduced
- lookupInst wanted `thenNF_Tc` \ lookup_result ->
- case lookup_result of
- GenInst wanteds' rhs -> use_instance wanteds' rhs
- SimpleInst rhs -> use_instance [] rhs
-
- NoInstance -> -- No such instance!
- case no_instance_action of
- Stop -> failTc
- AddToIrreds -> add_to_irreds
- ;
- Free -> -- It's free and this isn't a top-level binding, so just chuck it upstairs
- -- First, see if the inst can be reduced to a constant in one step
- lookupInst wanted `thenNF_Tc` \ lookup_result ->
- case lookup_result of
- SimpleInst rhs -> use_instance [] rhs
- other -> add_to_frees
-
-
-
- ;
- FreeIfTautological -> -- It's free and this is a top level binding, so
- -- check whether it's a tautology or not
- tryTc_
- add_to_irreds -- If tautology trial fails, add to irreds
-
- -- If tautology succeeds, just add to frees
- (reduce stack try_me_taut wanted (avails, [], []) `thenTc_`
- returnTc (avails, wanted:frees, irreds))
-
-
- ;
-
- DontReduce -> add_to_irreds
- ;
-
- DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
- -- See if the inst can be reduced to a constant in one step
- lookupInst wanted `thenNF_Tc` \ lookup_result ->
- case lookup_result of
- SimpleInst rhs -> use_instance [] rhs
- other -> add_to_irreds
- }
- where
- -- The three main actions
- add_to_frees = let
- avails' = addFree avails wanted
- -- Add the thing to the avails set so any identical Insts
- -- will be commoned up with it right here
- in
- returnTc (avails', wanted:frees, irreds)
-
- add_to_irreds = addGiven avails wanted `thenNF_Tc` \ avails' ->
- returnTc (avails', frees, wanted:irreds)
-
- use_instance wanteds' rhs = addWanted avails wanted rhs `thenNF_Tc` \ avails' ->
- reduceList stack try_me wanteds' (avails', frees, irreds)
-
-
- -- The try-me to use when trying to identify tautologies
- -- It blunders on reducing as much as possible
- try_me_taut inst = ReduceMe Stop -- No error recovery
-\end{code}
-
-
-\begin{code}
-activate :: Avails s -> Inst -> Avails s
- -- Activate the binding for Inst, ensuring that a binding for the
- -- wanted Inst will be generated.
- -- (Activate its parent if necessary, recursively).
- -- Precondition: the Inst is in Avails already
-
-activate avails wanted
- | not (instBindingRequired wanted)
- = avails
-
- | otherwise
- = case lookupFM avails wanted of
-
- Just (Avail main_id (PassiveScSel rhs insts) ids) ->
- foldl activate avails' insts -- Activate anything it needs
- where
- avails' = addToFM avails wanted avail'
- avail' = Avail main_id (Rhs rhs True) (wanted_id : ids) -- Activate it
-
- Just (Avail main_id other_rhs ids) -> -- Just add to the synonyms list
- addToFM avails wanted (Avail main_id other_rhs (wanted_id : ids))
-
- Nothing -> panic "activate"
- where
- wanted_id = instToId wanted
-
-addWanted avails wanted rhs_expr
- = ASSERT( not (wanted `elemFM` avails) )
- addFunDeps (addToFM avails wanted avail) wanted
- -- NB: we don't add the thing's superclasses too!
- -- Why not? Because addWanted is used when we've successfully used an
- -- instance decl to reduce something; e.g.
- -- d:Ord [a] = dfunOrd (d1:Eq [a]) (d2:Ord a)
- -- Note that we pass the superclasses to the dfun, so they will be "wanted".
- -- If we put the superclasses of "d" in avails, then we might end up
- -- expressing "d1" in terms of "d", which would be a disaster.
- where
- avail = Avail (instToId wanted) rhs []
-
- rhs | instBindingRequired wanted = Rhs rhs_expr False -- Not superclass selection
- | otherwise = NoRhs
-
-addFree :: Avails s -> Inst -> (Avails s)
- -- When an Inst is tossed upstairs as 'free' we nevertheless add it
- -- to avails, so that any other equal Insts will be commoned up right
- -- here rather than also being tossed upstairs. This is really just
- -- an optimisation, and perhaps it is more trouble that it is worth,
- -- as the following comments show!
- --
- -- NB1: do *not* add superclasses. If we have
- -- df::Floating a
- -- dn::Num a
- -- but a is not bound here, then we *don't* want to derive
- -- dn from df here lest we lose sharing.
- --
- -- NB2: do *not* add the Inst to avails at all if it's a method.
- -- The following situation shows why this is bad:
- -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
- -- From an application (truncate f i) we get
- -- t1 = truncate at f
- -- t2 = t1 at i
- -- If we have also have a secon occurrence of truncate, we get
- -- t3 = truncate at f
- -- t4 = t3 at i
- -- When simplifying with i,f free, we might still notice that
- -- t1=t3; but alas, the binding for t2 (which mentions t1)
- -- will continue to float out!
- -- Solution: never put methods in avail till they are captured
- -- in which case addFree isn't used
-addFree avails free
- | isDict free = addToFM avails free (Avail (instToId free) NoRhs [])
- | otherwise = avails
-
-addGiven :: Avails s -> Inst -> NF_TcM (Avails s)
-addGiven avails given
- = -- ASSERT( not (given `elemFM` avails) )
- -- This assertion isn't necessarily true. It's permitted
- -- to given a redundant context in a type signature (eg (Ord a, Eq a) => ...)
- -- and when typechecking instance decls we generate redundant "givens" too.
- addAvail avails given avail
- where
- avail = Avail (instToId given) NoRhs []
-
-addAvail avails wanted avail
- = addSuperClasses (addToFM avails wanted avail) wanted
-
-addSuperClasses :: Avails s -> Inst -> NF_TcM (Avails s)
- -- Add all the superclasses of the Inst to Avails
- -- Invariant: the Inst is already in Avails.
-
-addSuperClasses avails dict
- | not (isClassDict dict)
- = returnNF_Tc avails
-
- | otherwise -- It is a dictionary
- = foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_theta' sc_sels) `thenNF_Tc` \ avails' ->
- addFunDeps avails' dict
- where
- (clas, tys) = getDictClassTys dict
- (tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
-
- add_sc avails ((super_clas, super_tys), sc_sel)
- = newDictFromOld dict super_clas super_tys `thenNF_Tc` \ super_dict ->
- let
- sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys)
- [instToId dict]
- in
- case lookupFM avails super_dict of
-
- Just (Avail main_id (Rhs rhs False {- not sc selection -}) ids) ->
- -- Already there, but not as a superclass selector
- -- No need to look at its superclasses; since it's there
- -- already they must be already in avails
- -- However, we must remember to activate the dictionary
- -- from which it is (now) generated
- returnNF_Tc (activate avails' dict)
- where
- avails' = addToFM avails super_dict avail
- avail = Avail main_id (Rhs sc_sel_rhs True) ids -- Superclass selection
-
- Just (Avail _ _ _) -> returnNF_Tc avails
- -- Already there; no need to do anything
-
- Nothing ->
- -- Not there at all, so add it, and its superclasses
- addAvail avails super_dict avail
- where
- avail = Avail (instToId super_dict)
- (PassiveScSel sc_sel_rhs [dict])
- []
-
-addFunDeps :: Avails s -> Inst -> NF_TcM (Avails s)
- -- Add in the functional dependencies generated by the inst
-addFunDeps avails inst
- = newFunDepFromDict inst `thenNF_Tc` \ fdInst_maybe ->
- case fdInst_maybe of
- Nothing -> returnNF_Tc avails
- Just fdInst ->
- let fdAvail = Avail (instToId (fromJust fdInst_maybe)) NoRhs [] in
- addAvail avails fdInst fdAvail
-\end{code}
-
-%************************************************************************
-%* *
-\subsection[simple]{@Simple@ versions}
-%* *
-%************************************************************************
-
-Much simpler versions when there are no bindings to make!
-
-@tcSimplifyThetas@ simplifies class-type constraints formed by
-@deriving@ declarations and when specialising instances. We are
-only interested in the simplified bunch of class/type constraints.
-
-It simplifies to constraints of the form (C a b c) where
-a,b,c are type variables. This is required for the context of
-instance declarations.
-
-\begin{code}
-tcSimplifyThetas :: ClassContext -- Wanted
- -> TcM ClassContext -- Needed
-
-tcSimplifyThetas wanteds
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
- reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
- let
- -- For multi-param Haskell, check that the returned dictionaries
- -- don't have any of the form (C Int Bool) for which
- -- we expect an instance here
- -- For Haskell 98, check that all the constraints are of the form C a,
- -- where a is a type variable
- bad_guys | glaExts = [ct | ct@(clas,tys) <- irreds,
- isEmptyVarSet (tyVarsOfTypes tys)]
- | otherwise = [ct | ct@(clas,tys) <- irreds,
- not (all isTyVarTy tys)]
- in
- if null bad_guys then
- returnTc irreds
- else
- mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
- failTc
-\end{code}
-
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
-used with \tr{default} declarations. We are only interested in
-whether it worked or not.
-
-\begin{code}
-tcSimplifyCheckThetas :: ClassContext -- Given
- -> ClassContext -- Wanted
- -> TcM ()
-
-tcSimplifyCheckThetas givens wanteds
- = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
- if null irreds then
- returnTc ()
- else
- mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
- failTc
-\end{code}
-
-
-\begin{code}
-type AvailsSimple = FiniteMap (Class,[Type]) Bool
- -- True => irreducible
- -- False => given, or can be derived from a given or from an irreducible
-
-reduceSimple :: ClassContext -- Given
- -> ClassContext -- Wanted
- -> NF_TcM ClassContext -- Irreducible
-
-reduceSimple givens wanteds
- = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
- returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
- where
- givens_fm = foldl addNonIrred emptyFM givens
-
-reduce_simple :: (Int,ClassContext) -- Stack
- -> AvailsSimple
- -> ClassContext
- -> NF_TcM AvailsSimple
-
-reduce_simple (n,stack) avails wanteds
- = go avails wanteds
- where
- go avails [] = returnNF_Tc avails
- go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
- go avails' ws
-
-reduce_simple_help stack givens wanted@(clas,tys)
- | wanted `elemFM` givens
- = returnNF_Tc givens
-
- | otherwise
- = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
-
- case maybe_theta of
- Nothing -> returnNF_Tc (addIrred givens wanted)
- Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
-
-addIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
-addIrred givens ct@(clas,tys)
- = addSCs (addToFM givens ct True) ct
-
-addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
-addNonIrred givens ct@(clas,tys)
- = addSCs (addToFM givens ct False) ct
-
-addSCs givens ct@(clas,tys)
- = foldl add givens sc_theta
- where
- (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
- sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
+ DontReduce -> addIrred state wanted
- add givens ct@(clas, tys)
- = case lookupFM givens ct of
- Nothing -> -- Add it and its superclasses
- addSCs (addToFM givens ct False) ct
+ ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
+ -- First, see if the inst can be reduced to a constant in one step
+ try_simple addIrred
- Just True -> -- Set its flag to False; superclasses already done
- addToFM givens ct False
+ ; Free -> -- It's free so just chuck it upstairs
+ -- First, see if the inst can be reduced to a constant in one step
+ try_simple addFree
- Just False -> -- Already done
- givens
-
-\end{code}
+ ; ReduceMe no_instance_action -> -- It should be reduced
+ lookupInst wanted `thenNF_Tc` \ lookup_result ->
+ case lookup_result of
+ GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
+ addWanted state' wanted rhs wanteds'
+ SimpleInst rhs -> addWanted state wanted rhs []
-%************************************************************************
-%* *
-\subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
-%* *
-%************************************************************************
+ NoInstance -> -- No such instance!
+ case no_instance_action of
+ Stop -> failTc
+ AddToIrreds -> addIrred state wanted
-When doing a binding group, we may have @Insts@ of local functions.
-For example, we might have...
-\begin{verbatim}
-let f x = x + 1 -- orig local function (overloaded)
- f.1 = f Int -- two instances of f
- f.2 = f Float
- in
- (f.1 5, f.2 6.7)
-\end{verbatim}
-The point is: we must drop the bindings for @f.1@ and @f.2@ here,
-where @f@ is in scope; those @Insts@ must certainly not be passed
-upwards towards the top-level. If the @Insts@ were binding-ified up
-there, they would have unresolvable references to @f@.
+ }
+ where
+ try_simple do_this_otherwise
+ = lookupInst wanted `thenNF_Tc` \ lookup_result ->
+ case lookup_result of
+ SimpleInst rhs -> addWanted state wanted rhs []
+ other -> do_this_otherwise state wanted
+\end{code}
-We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
-For each method @Inst@ in the @init_lie@ that mentions one of the
-@Ids@, we create a binding. We return the remaining @Insts@ (in an
-@LIE@), as well as the @HsBinds@ generated.
\begin{code}
-bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
+isAvailable :: RedState -> Inst -> Bool
+isAvailable (avails, _) wanted = wanted `elemFM` avails
+ -- NB: the Ord instance of Inst compares by the class/type info
+ -- *not* by unique. So
+ -- d1::C Int == d2::C Int
+
+-------------------------
+addFree :: RedState -> Inst -> NF_TcM RedState
+ -- When an Inst is tossed upstairs as 'free' we nevertheless add it
+ -- to avails, so that any other equal Insts will be commoned up right
+ -- here rather than also being tossed upstairs. This is really just
+ -- an optimisation, and perhaps it is more trouble that it is worth,
+ -- as the following comments show!
+ --
+ -- NB1: do *not* add superclasses. If we have
+ -- df::Floating a
+ -- dn::Num a
+ -- but a is not bound here, then we *don't* want to derive
+ -- dn from df here lest we lose sharing.
+ --
+ -- NB2: do *not* add the Inst to avails at all if it's a method.
+ -- The following situation shows why this is bad:
+ -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
+ -- From an application (truncate f i) we get
+ -- t1 = truncate at f
+ -- t2 = t1 at i
+ -- If we have also have a second occurrence of truncate, we get
+ -- t3 = truncate at f
+ -- t4 = t3 at i
+ -- When simplifying with i,f free, we might still notice that
+ -- t1=t3; but alas, the binding for t2 (which mentions t1)
+ -- will continue to float out!
+ -- Solution: never put methods in avail till they are captured
+ -- in which case addFree isn't used
+ --
+ -- NB3: make sure that CCallable/CReturnable use NoRhs rather
+ -- than BoundTo, else we end up with bogus bindings.
+ -- c.f. instBindingRequired in addWanted
+addFree (avails, frees) free
+ | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
+ | otherwise = returnNF_Tc (avails, free:frees)
+ where
+ avail | instBindingRequired free = BoundTo (instToId free)
+ | otherwise = NoRhs
+
+addGiven :: RedState -> Inst -> NF_TcM RedState
+addGiven state given = add_avail state given (BoundTo (instToId given))
+
+addIrred :: RedState -> Inst -> NF_TcM RedState
+addIrred state irred = add_avail state irred Irred
+
+addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
+addWanted state wanted rhs_expr wanteds
+ = ASSERT( not (isAvailable state wanted) )
+ add_avail state wanted avail
+ where
+ avail | instBindingRequired wanted = Rhs rhs_expr wanteds
+ | otherwise = ASSERT( null wanteds ) NoRhs
+
+add_avail :: RedState -> Inst -> Avail -> NF_TcM RedState
+add_avail (avails, frees) wanted avail
+ = addAvail avails wanted avail `thenNF_Tc` \ avails' ->
+ returnNF_Tc (avails', frees)
+
+---------------------
+addAvail :: Avails -> Inst -> Avail -> NF_TcM Avails
+addAvail avails wanted avail
+ = addSuperClasses (addToFM avails wanted avail) wanted
-bindInstsOfLocalFuns init_lie local_ids
- | null overloaded_ids || null lie_for_here
- -- Common case
- = returnTc (init_lie, EmptyMonoBinds)
+addSuperClasses :: Avails -> Inst -> NF_TcM Avails
+ -- Add all the superclasses of the Inst to Avails
+ -- Invariant: the Inst is already in Avails.
- | otherwise
- = reduceContext (text "bindInsts" <+> ppr local_ids)
- try_me [] lie_for_here `thenTc` \ (binds, frees, irreds) ->
- ASSERT( null irreds )
- returnTc (mkLIE frees `plusLIE` mkLIE lie_not_for_here, binds)
- where
- overloaded_ids = filter is_overloaded local_ids
- is_overloaded id = case splitSigmaTy (idType id) of
- (_, theta, _) -> not (null theta)
+addSuperClasses avails dict
+ | not (isClassDict dict)
+ = returnNF_Tc avails
- overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
- -- so it's worth building a set, so that
- -- lookup (in isMethodFor) is faster
+ | otherwise -- It is a dictionary
+ = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
+ foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_dicts sc_sels)
+ where
+ (clas, tys) = getDictClassTys dict
+ (tyvars, sc_theta, sc_sels, _) = classBigSig clas
+ sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
- -- No sense in repeatedly zonking lots of
- -- constant constraints so filter them out here
- (lie_for_here, lie_not_for_here) = partition (isMethodFor overloaded_set)
- (lieToList init_lie)
- try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
- | otherwise = Free
+ add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
+ = case lookupFM avails sc_dict of
+ Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
+ other -> addAvail avails sc_dict avail
+ where
+ sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
+ avail = Rhs sc_sel_rhs [dict]
\end{code}
+Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
+and want to deduce (d2:C [a]) where
+
+ class Ord a => C a where
+ instance Ord a => C [a] where ...
+
+Then we'll use the instance decl to deduce C [a] and then add the
+superclasses of C [a] to avails. But we must not overwrite the binding
+for d1:Ord a (which is given) with a superclass selection or we'll just
+build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
+than a selection.
+
%************************************************************************
%* *
-\section[Disambig]{Disambiguation of overloading}
+\section{tcSimplifyTop: defaulting}
%* *
%************************************************************************
If a dictionary constrains a type variable which is
-\begin{itemize}
-\item
-not mentioned in the environment
-\item
-and not mentioned in the type of the expression
-\end{itemize}
+ * not mentioned in the environment
+ * and not mentioned in the type of the expression
then it is ambiguous. No further information will arise to instantiate
the type variable; nor will it be generalised and turned into an extra
parameter to a function.
It is an error for this to occur, except that Haskell provided for
certain rules to be applied in the special case of numeric types.
-
Specifically, if
-\begin{itemize}
-\item
-at least one of its classes is a numeric class, and
-\item
-all of its classes are numeric or standard
-\end{itemize}
+ * at least one of its classes is a numeric class, and
+ * all of its classes are numeric or standard
then the type variable can be defaulted to the first type in the
default-type list which is an instance of all the offending classes.
complains. It works by splitting the dictionary list by type
variable, and using @disambigOne@ to do the real business.
+@tcSimplifyTop@ is called once per module to simplify all the constant
+and ambiguous Insts.
+
+We need to be careful of one case. Suppose we have
+
+ instance Num a => Num (Foo a b) where ...
+
+and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
+to (Num x), and default x to Int. But what about y??
+
+It's OK: the final zonking stage should zap y to (), which is fine.
-@tcSimplifyTop@ is called once per module to simplify
-all the constant and ambiguous Insts.
\begin{code}
tcSimplifyTop :: LIE -> TcM TcDictBinds
tcSimplifyTop wanted_lie
- = reduceContext (text "tcSimplTop") try_me [] wanteds `thenTc` \ (binds1, frees, irreds) ->
+ = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
ASSERT( null frees )
let
-- All the non-std ones are definite errors
(stds, non_stds) = partition isStdClassTyVarDict irreds
-
-- Group by type variable
std_groups = equivClasses cmp_by_tyvar stds
-- Pick the ones which its worth trying to disambiguate
(std_oks, std_bads) = partition worth_a_try std_groups
+
-- Have a try at disambiguation
-- if the type variable isn't bound
-- up with one of the non-standard classes
- worth_a_try group@(d:_) = isEmptyVarSet (tyVarsOfInst d `intersectVarSet` non_std_tyvars)
+ worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
-- Collect together all the bad guys
mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
-- And complain about the ones that don't
- mapNF_Tc complain bad_guys `thenNF_Tc_`
+ addTopAmbigErrs bad_guys `thenNF_Tc_`
- returnTc (binds1 `andMonoBinds` andMonoBindList binds_ambig)
+ returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
where
wanteds = lieToList wanted_lie
try_me inst = ReduceMe AddToIrreds
d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
- complain d | not (null (getIPs d)) = addTopIPErr d
- | isEmptyVarSet (tyVarsOfInst d) = addTopInstanceErr d
- | otherwise = addAmbigErr tyVarsOfInst d
-
get_tv d = case getDictClassTys d of
(clas, [ty]) -> getTyVar "tcSimplifyTop" ty
get_clas d = case getDictClassTys d of
in
-- See if any default works, and if so bind the type variable to it
-- If not, add an AmbigErr
- recoverTc (complain dicts `thenNF_Tc_` returnTc EmptyMonoBinds) $
+ recoverTc (addAmbigErrs dicts `thenNF_Tc_` returnTc EmptyMonoBinds) $
try_default default_tys `thenTc` \ chosen_default_ty ->
-- Bind the type variable and reduce the context, for real this time
unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
- reduceContext (text "disambig" <+> ppr dicts)
- try_me [] dicts `thenTc` \ (binds, frees, ambigs) ->
+ simpleReduceLoop (text "disambig" <+> ppr dicts)
+ try_me dicts `thenTc` \ (frees, binds, ambigs) ->
WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
warnDefault dicts chosen_default_ty `thenTc_`
returnTc binds
returnTc EmptyMonoBinds
| otherwise -- No defaults
- = complain dicts `thenNF_Tc_`
+ = addAmbigErrs dicts `thenNF_Tc_`
returnTc EmptyMonoBinds
where
- complain = addAmbigErrs tyVarsOfInst
try_me inst = ReduceMe AddToIrreds -- This reduce should not fail
tyvar = get_tv (head dicts) -- Should be non-empty
classes = map get_clas dicts
]
-Errors and contexts
-~~~~~~~~~~~~~~~~~~~
+
+%************************************************************************
+%* *
+\subsection[simple]{@Simple@ versions}
+%* *
+%************************************************************************
+
+Much simpler versions when there are no bindings to make!
+
+@tcSimplifyThetas@ simplifies class-type constraints formed by
+@deriving@ declarations and when specialising instances. We are
+only interested in the simplified bunch of class/type constraints.
+
+It simplifies to constraints of the form (C a b c) where
+a,b,c are type variables. This is required for the context of
+instance declarations.
+
+\begin{code}
+tcSimplifyThetas :: ClassContext -- Wanted
+ -> TcM ClassContext -- Needed
+
+tcSimplifyThetas wanteds
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
+ reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
+ let
+ -- For multi-param Haskell, check that the returned dictionaries
+ -- don't have any of the form (C Int Bool) for which
+ -- we expect an instance here
+ -- For Haskell 98, check that all the constraints are of the form C a,
+ -- where a is a type variable
+ bad_guys | glaExts = [ct | ct@(clas,tys) <- irreds,
+ isEmptyVarSet (tyVarsOfTypes tys)]
+ | otherwise = [ct | ct@(clas,tys) <- irreds,
+ not (all isTyVarTy tys)]
+ in
+ if null bad_guys then
+ returnTc irreds
+ else
+ mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
+ failTc
+\end{code}
+
+@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+used with \tr{default} declarations. We are only interested in
+whether it worked or not.
+
+\begin{code}
+tcSimplifyCheckThetas :: ClassContext -- Given
+ -> ClassContext -- Wanted
+ -> TcM ()
+
+tcSimplifyCheckThetas givens wanteds
+ = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
+ if null irreds then
+ returnTc ()
+ else
+ mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
+ failTc
+\end{code}
+
+
+\begin{code}
+type AvailsSimple = FiniteMap (Class,[Type]) Bool
+ -- True => irreducible
+ -- False => given, or can be derived from a given or from an irreducible
+
+reduceSimple :: ClassContext -- Given
+ -> ClassContext -- Wanted
+ -> NF_TcM ClassContext -- Irreducible
+
+reduceSimple givens wanteds
+ = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
+ returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
+ where
+ givens_fm = foldl addNonIrred emptyFM givens
+
+reduce_simple :: (Int,ClassContext) -- Stack
+ -> AvailsSimple
+ -> ClassContext
+ -> NF_TcM AvailsSimple
+
+reduce_simple (n,stack) avails wanteds
+ = go avails wanteds
+ where
+ go avails [] = returnNF_Tc avails
+ go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
+ go avails' ws
+
+reduce_simple_help stack givens wanted@(clas,tys)
+ | wanted `elemFM` givens
+ = returnNF_Tc givens
+
+ | otherwise
+ = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
+
+ case maybe_theta of
+ Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
+ Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
+
+addSimpleIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
+addSimpleIrred givens ct@(clas,tys)
+ = addSCs (addToFM givens ct True) ct
+
+addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
+addNonIrred givens ct@(clas,tys)
+ = addSCs (addToFM givens ct False) ct
+
+addSCs givens ct@(clas,tys)
+ = foldl add givens sc_theta
+ where
+ (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
+ sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
+
+ add givens ct@(clas, tys)
+ = case lookupFM givens ct of
+ Nothing -> -- Add it and its superclasses
+ addSCs (addToFM givens ct False) ct
+
+ Just True -> -- Set its flag to False; superclasses already done
+ addToFM givens ct False
+
+ Just False -> -- Already done
+ givens
+
+\end{code}
+
+
+%************************************************************************
+%* *
+\section{Errors and contexts}
+%* *
+%************************************************************************
+
ToDo: for these error messages, should we note the location as coming
from the insts, or just whatever seems to be around in the monad just
now?
\begin{code}
-genCantGenErr insts -- Can't generalise these Insts
- = sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
- nest 4 (pprInstsInFull insts)
- ]
+addTopAmbigErrs dicts
+ = mapNF_Tc complain tidy_dicts
+ where
+ fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
+ (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
+ complain d | not (null (getIPs d)) = addTopIPErr tidy_env d
+ | tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
+ | otherwise = addAmbigErr tidy_env d
+
+addTopIPErr tidy_env tidy_dict
+ = addInstErrTcM (instLoc tidy_dict)
+ (tidy_env,
+ ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
+
+-- Used for top-level irreducibles
+addTopInstanceErr tidy_env tidy_dict
+ = addInstErrTcM (instLoc tidy_dict)
+ (tidy_env,
+ ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
-addAmbigErrs ambig_tv_fn dicts = mapNF_Tc (addAmbigErr ambig_tv_fn) dicts
+addAmbigErrs dicts
+ = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
+ where
+ (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
-addAmbigErr ambig_tv_fn dict
- = addInstErrTcM (instLoc dict)
+addAmbigErr tidy_env tidy_dict
+ = addInstErrTcM (instLoc tidy_dict)
(tidy_env,
sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
where
- ambig_tvs = varSetElems (ambig_tv_fn tidy_dict)
- (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
+ ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
warnDefault dicts default_ty
= doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
warnTc True (vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty),
pprInstsInFull dicts])
-addTopIPErr dict
- = addInstErrTcM (instLoc dict)
- (tidy_env,
- ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
- where
- (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
-
--- Used for top-level irreducibles
-addTopInstanceErr dict
- = addInstErrTcM (instLoc dict)
- (tidy_env,
- ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
- where
- (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
-
-- The error message when we don't find a suitable instance
-- is complicated by the fact that sometimes this is because
-- there is no instance, and sometimes it's because there are
-- too many instances (overlap). See the comments in TcEnv.lhs
-- with the InstEnv stuff.
-addNoInstanceErr str givens dict
+addNoInstanceErr what_doc givens dict
= tcGetInstEnv `thenNF_Tc` \ inst_env ->
let
doc = vcat [sep [herald <+> quotes (pprInst tidy_dict),
quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
- ptext SLIT("to the") <+> str]
+ ptext SLIT("to the") <+> what_doc]
fix2 | isTyVarDict dict || ambig_overlap
= empty
-- Used for the ...Thetas variants; all top level
addNoInstErr (c,ts)
- = addErrTc (ptext SLIT("No instance for") <+> quotes (pprConstraint c ts))
+ = addErrTc (ptext SLIT("No instance for") <+> quotes (pprClassPred c ts))
reduceDepthErr n stack
= vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
nest 4 (pprInstsInFull stack)]
reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+
+-----------------------------------------------
+addCantGenErr inst
+ = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
+ nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
\end{code}
newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
-----------------------------------------
- TcType, TcTauType, TcThetaType, TcRhoType,
+ TcType, TcTauType, TcThetaType, TcRhoType, TcClassContext,
-- Find the type to which a type variable is bound
tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType
tcSplitRhoTy,
- tcInstTyVars,
+ tcInstTyVar, tcInstTyVars,
tcInstSigVar,
- tcInstTcType,
+ tcInstType,
--------------------------------
TcKind,
newKindVar, newKindVars, newBoxityVar,
--------------------------------
- zonkTcTyVar, zonkTcTyVars, zonkTcSigTyVars,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
splitPredTy_maybe, splitForAllTys,
isTyVarTy, mkTyVarTy, mkTyVarTys,
openTypeKind, liftedTypeKind,
- superKind, superBoxity,
+ superKind, superBoxity, tyVarsOfTypes,
defaultKind, liftedBoxity
)
import Subst ( Subst, mkTopTyVarSubst, substTy )
tcNewSigTyVar name kind
\end{code}
-@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, returning them and the instantiated body of the for-all.
+@tcInstType@ instantiates the outer-level for-alls of a TcType with
+fresh type variables, splits off the dictionary part, and returns the results.
\begin{code}
-tcInstTcType :: TcType -> NF_TcM ([TcTyVar], TcType)
-tcInstTcType ty
+tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+tcInstType ty
= case splitForAllTys ty of
- ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
- (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
- returnNF_Tc (tyvars', substTy tenv rho)
+ ([], _) -> returnNF_Tc ([], [], ty) -- Nothing to do
+ (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
+ tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) ->
+ returnNF_Tc (tyvars', theta, tau)
\end{code}
Putting is easy:
\begin{code}
-tcPutTyVar tyvar ty = UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
- tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
- returnNF_Tc ty
+tcPutTyVar tyvar ty
+ | not (isMutTyVar tyvar)
+ = pprTrace "tcPutTyVar" (ppr tyvar) $
+ returnNF_Tc ty
+
+ | otherwise
+ = ASSERT( isMutTyVar tyvar )
+ UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
+ tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
+ returnNF_Tc ty
\end{code}
Getting is more interesting. The easy thing to do is just to read, thus:
\begin{code}
tcGetTyVar tyvar
+ | not (isMutTyVar tyvar)
+ = pprTrace "tcGetTyVar" (ppr tyvar) $
+ returnNF_Tc (Just (mkTyVarTy tyvar))
+
+ | otherwise
= ASSERT2( isMutTyVar tyvar, ppr tyvar )
tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
case maybe_ty of
zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
+zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
+ returnNF_Tc (tyVarsOfTypes tys)
+
zonkTcTyVar :: TcTyVar -> NF_TcM TcType
zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
mkClass, classTyVars, classArity,
classKey, className, classSelIds, classTyCon,
- classBigSig, classExtraBigSig, classTvsFds
+ classBigSig, classExtraBigSig, classTvsFds, classSCTheta
) where
#include "HsVersions.h"
\begin{code}
module FunDeps (
- oclose,
- instantiateFdClassTys,
- pprFundeps
+ oclose, grow, improve, checkInstFDs, checkClsFD, pprFundeps
) where
#include "HsVersions.h"
import Var ( TyVar )
import Class ( Class, FunDep, classTvsFds )
-import Type ( Type, tyVarsOfTypes )
+import Type ( Type, PredType(..), predTyUnique, tyVarsOfTypes, tyVarsOfPred )
+import Subst ( mkSubst, emptyInScopeSet, substTy )
+import Unify ( unifyTyListsX )
import Outputable ( Outputable, SDoc, interppSP, ptext, empty, hsep, punctuate, comma )
-import UniqSet
import VarSet
import VarEnv
-import Util ( zipEqual )
+import List ( tails )
+import ListSetOps ( equivClassesByUniq )
\end{code}
+%************************************************************************
+%* *
+\subsection{Close type variables}
+%* *
+%************************************************************************
+
+(oclose preds tvs) closes the set of type variables tvs,
+wrt functional dependencies in preds. The result is a superset
+of the argument set. For example, if we have
+ class C a b | a->b where ...
+then
+ oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
+because if we know x and y then that fixes z.
+
+Using oclose
+~~~~~~~~~~~~
+oclose is used
+
+a) When determining ambiguity. The type
+ forall a,b. C a b => a
+is not ambiguous (given the above class decl for C) because
+a determines b.
+
+b) When generalising a type T. Usually we take FV(T) \ FV(Env),
+but in fact we need
+ FV(T) \ (FV(Env)+)
+where the '+' is the oclosure operation. Notice that we do not
+take FV(T)+. This puzzled me for a bit. Consider
+
+ f = E
+
+and suppose e have that E :: C a b => a, and suppose that b is
+free in the environment. Then we quantify over 'a' only, giving
+the type forall a. C a b => a. Since a->b but we don't have b->a,
+we might have instance decls like
+ instance C Bool Int where ...
+ instance C Char Int where ...
+so knowing that b=Int doesn't fix 'a'; so we quantify over it.
+
+ ---------------
+ A WORRY: ToDo!
+ ---------------
+If we have class C a b => D a b where ....
+ class D a b | a -> b where ...
+and the preds are [C (x,y) z], then we want to see the fd in D,
+even though it is not explicit in C, giving [({x,y},{z})]
+
+Similarly for instance decls? E.g. Suppose we have
+ instance C a b => Eq (T a b) where ...
+and we infer a type t with constraints Eq (T a b) for a particular
+expression, and suppose that 'a' is free in the environment.
+We could generalise to
+ forall b. Eq (T a b) => t
+but if we reduced the constraint, to C a b, we'd see that 'a' determines
+b, so that a better type might be
+ t (with free constraint C a b)
+Perhaps it doesn't matter, because we'll still force b to be a
+particular type at the call sites. Generalising over too many
+variables (provided we don't shadow anything by quantifying over a
+variable that is actually free in the envt) may postpone errors; it
+won't hide them altogether.
+
+
+\begin{code}
+oclose :: [PredType] -> TyVarSet -> TyVarSet
+oclose preds fixed_tvs
+ | null tv_fds = fixed_tvs -- Fast escape hatch for common case
+ | otherwise = loop fixed_tvs
+ where
+ loop fixed_tvs
+ | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
+ | otherwise = loop new_fixed_tvs
+ where
+ new_fixed_tvs = foldl extend fixed_tvs tv_fds
+
+ extend fixed_tvs (ls,rs) | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
+ | otherwise = fixed_tvs
+
+ tv_fds :: [(TyVarSet,TyVarSet)]
+ -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
+ -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
+ tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
+ | Class cls tys <- preds, -- Ignore implicit params
+ let (cls_tvs, cls_fds) = classTvsFds cls,
+ fd <- cls_fds,
+ let (xs,ys) = instFD fd cls_tvs tys
+ ]
+\end{code}
+
+\begin{code}
+grow :: [PredType] -> TyVarSet -> TyVarSet
+grow preds fixed_tvs
+ | null pred_sets = fixed_tvs
+ | otherwise = loop fixed_tvs
+ where
+ loop fixed_tvs
+ | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
+ | otherwise = loop new_fixed_tvs
+ where
+ new_fixed_tvs = foldl extend fixed_tvs pred_sets
+
+ extend fixed_tvs pred_tvs
+ | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs
+ | otherwise = fixed_tvs
+
+ pred_sets = [tyVarsOfPred pred | pred <- preds]
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Generate equations from functional dependencies}
+%* *
+%************************************************************************
+
+
+\begin{code}
+----------
+type Equation = (Type,Type) -- These two types should be equal
+ -- INVARIANT: they aren't already equal
+
+----------
+improve :: InstEnv a -- Gives instances for given class
+ -> [PredType] -- Current constraints
+ -> [Equation] -- Derived equalities that must also hold
+ -- (NB the above INVARIANT for type Equation)
+
+type InstEnv a = Class -> [(TyVarSet, [Type], a)]
+-- This is a bit clumsy, because InstEnv is really
+-- defined in module InstEnv. However, we don't want
+-- to define it (and ClsInstEnv) here because InstEnv
+-- is their home. Nor do we want to make a recursive
+-- module group (InstEnv imports stuff from FunDeps).
+\end{code}
+
+Given a bunch of predicates that must hold, such as
+
+ C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
+
+improve figures out what extra equations must hold.
+For example, if we have
+
+ class C a b | a->b where ...
+
+then improve will return
+
+ [(t1,t2), (t4,t5)]
+
+NOTA BENE:
+
+ * improve does not iterate. It's possible that when we make
+ t1=t2, for example, that will in turn trigger a new equation.
+ This would happen if we also had
+ C t1 t7, C t2 t8
+ If t1=t2, we also get t7=t8.
+
+ improve does *not* do this extra step. It relies on the caller
+ doing so.
+
+ * The equations unify types that are not already equal. So there
+ is no effect iff the result of improve is empty
+
+
+
\begin{code}
-oclose :: [FunDep Type] -> TyVarSet -> TyVarSet
--- (oclose fds tvs) closes the set of type variables tvs,
--- wrt the functional dependencies fds. The result is a superset
--- of the argument set.
---
--- In fact the functional dependencies are *instantiated*, so we
--- first have to extract the free vars.
---
--- For example,
--- oclose [a -> b] {a} = {a,b}
--- oclose [a b -> c] {a} = {a}
--- oclose [a b -> c] {a,b} = {a,b,c}
--- If all of the things on the left of an arrow are in the set, add
--- the things on the right of that arrow.
-
-oclose fds vs
- = go vs
+improve inst_env preds
+ = [ eqn | group <- equivClassesByUniq predTyUnique preds,
+ eqn <- checkGroup inst_env group ]
+
+----------
+checkGroup :: InstEnv a -> [PredType] -> [Equation]
+ -- The preds are all for the same class or implicit param
+
+checkGroup inst_env (IParam _ ty : ips)
+ = -- For implicit parameters, all the types must match
+ [(ty, ty') | IParam _ ty' <- ips, ty /= ty']
+
+checkGroup inst_env clss@(Class cls tys : _)
+ = -- For classes life is more complicated
+ -- Suppose the class is like
+ -- classs C as | (l1 -> r1), (l2 -> r2), ... where ...
+ -- Then FOR EACH PAIR (Class c tys1, Class c tys2) in the list clss
+ -- we check whether
+ -- U l1[tys1/as] = U l2[tys2/as]
+ -- (where U is a unifier)
+ --
+ -- If so, we return the pair
+ -- U r1[tys1/as] = U l2[tys2/as]
+ --
+ -- We need to do something very similar comparing each predicate
+ -- with relevant instance decls
+ pairwise_eqns ++ instance_eqns
+
where
- go vs = case oclose1 tv_fds vs of
- (vs', False) -> vs'
- (vs', True) -> go vs'
-
- tv_fds :: [FunDep TyVar]
- tv_fds = [(get_tvs xs, get_tvs ys) | (xs, ys) <- fds]
- get_tvs = varSetElems . tyVarsOfTypes
-
-oclose1 [] vs = (vs, False)
-oclose1 (fd@(ls, rs):fds) vs =
- if osubset ls vs then
- (vs'', b1 || b2)
- else
- vs'b1
- where
- vs'b1@(vs', b1) = oclose1 fds vs
- (vs'', b2) = ounion rs vs'
-
-osubset [] vs = True
-osubset (u:us) vs = if u `elementOfUniqSet` vs then osubset us vs else False
-
-ounion [] ys = (ys, False)
-ounion (x:xs) ys
- | x `elementOfUniqSet` ys = (ys', b)
- | otherwise = (addOneToUniqSet ys' x, True)
- where
- (ys', b) = ounion xs ys
-
-instantiateFdClassTys :: Class -> [Type] -> [FunDep Type]
--- Get the FDs of the class, and instantiate them
-instantiateFdClassTys clas tys
- = [(map lookup us, map lookup vs) | (us,vs) <- fundeps]
+ (cls_tvs, cls_fds) = classTvsFds cls
+ cls_inst_env = inst_env cls
+
+ -- NOTE that we iterate over the fds first; they are typically
+ -- empty, which aborts the rest of the loop.
+ pairwise_eqns :: [(Type,Type)]
+ pairwise_eqns -- This group comes from pairwise comparison
+ = [ eqn | fd <- cls_fds,
+ Class _ tys1 : rest <- tails clss,
+ Class _ tys2 <- rest,
+ eqn <- checkClsFD emptyVarSet fd cls_tvs tys1 tys2
+ ]
+
+ instance_eqns :: [(Type,Type)]
+ instance_eqns -- This group comes from comparing with instance decls
+ = [ eqn | fd <- cls_fds,
+ (qtvs, tys1, _) <- cls_inst_env,
+ Class _ tys2 <- clss,
+ eqn <- checkClsFD qtvs fd cls_tvs tys1 tys2
+ ]
+
+
+----------
+checkClsFD :: TyVarSet
+ -> FunDep TyVar -> [TyVar] -- One functional dependency from the class
+ -> [Type] -> [Type]
+ -> [Equation]
+
+checkClsFD qtvs fd clas_tvs tys1 tys2
+-- We use 'unify' even though we are often only matching
+-- unifyTyListsX will only bind variables in qtvs, so it's OK!
+ = case unifyTyListsX qtvs ls1 ls2 of
+ Nothing -> []
+ Just unif -> [(sr1, sr2) | (r1,r2) <- rs1 `zip` rs2,
+ let sr1 = substTy full_unif r1,
+ let sr2 = substTy full_unif r2,
+ sr1 /= sr2]
+ where
+ full_unif = mkSubst emptyInScopeSet unif
+ -- No for-alls in sight; hmm
+ where
+ (ls1, rs1) = instFD fd clas_tvs tys1
+ (ls2, rs2) = instFD fd clas_tvs tys2
+
+instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
+instFD (ls,rs) tvs tys
+ = (map lookup ls, map lookup rs)
where
- (tyvars, fundeps) = classTvsFds clas
- env = mkVarEnv (zipEqual "instantiateFdClassTys" tyvars tys)
+ env = zipVarEnv tvs tys
lookup tv = lookupVarEnv_NF env tv
+\end{code}
+\begin{code}
+checkInstFDs :: Class -> [Type] -> Bool
+-- Check that functional dependencies are obeyed in an instance decl
+-- For example, if we have
+-- class C a b | a -> b
+-- instance C t1 t2
+-- Then we require fv(t2) `subset` fv(t1)
+checkInstFDs clas inst_taus
+ = all fundep_ok fds
+ where
+ (tyvars, fds) = classTvsFds clas
+ fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
+ where
+ (ls,rs) = instFD fd tyvars inst_taus
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Miscellaneous}
+%* *
+%************************************************************************
+
+\begin{code}
pprFundeps :: Outputable a => [FunDep a] -> SDoc
pprFundeps [] = empty
pprFundeps fds = hsep (ptext SLIT("|") : punctuate comma (map ppr_fd fds))
#include "HsVersions.h"
-import Class ( Class )
-import Var ( Id )
-import VarSet ( TyVarSet, unionVarSet, mkVarSet, varSetElems )
-import VarEnv ( TyVarSubstEnv )
+import Class ( Class, classTvsFds )
+import Var ( TyVar, Id )
+import VarSet
+import VarEnv
import Maybes ( MaybeErr(..), returnMaB, failMaB, thenMaB, maybeToBool )
import Name ( getSrcLoc )
-import Type ( Type, tyConAppTyCon,
- splitSigmaTy, splitDFunTy, tyVarsOfTypes
+import Type ( Type, tyConAppTyCon, mkTyVarTy,
+ splitDFunTy, tyVarsOfTypes
)
-import PprType ( )
+import PprType ( pprClassPred )
+import FunDeps ( checkClsFD )
import TyCon ( TyCon )
import Outputable
-import Unify ( matchTys, unifyTyListsX )
+import Unify ( matchTys, unifyTyListsX, allDistinctTyVars )
import UniqFM ( UniqFM, lookupWithDefaultUFM, addToUFM, emptyUFM, eltsUFM )
import Id ( idType )
import ErrUtils ( Message )
type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
-type ClsInstEnv = [(TyVarSet, [Type], DFunId)] -- The instances for a particular class
-
simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
simpleDFunClassTyCon dfun
= (clas, tycon)
%* *
%************************************************************************
-The actual type declarations are in HscTypes.
-
\begin{code}
+type ClsInstEnv = [(TyVarSet, [Type], DFunId)] -- The instances for a particular class
+ -- INVARIANTs: see notes below
+
emptyInstEnv :: InstEnv
emptyInstEnv = emptyUFM
classInstEnv env cls = lookupWithDefaultUFM env [] cls
\end{code}
-A @ClsInstEnv@ lives inside a class, and identifies all the instances
-of that class. The @Id@ inside a ClsInstEnv mapping is the dfun for
-that instance.
+A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
+ClsInstEnv mapping is the dfun for that instance.
If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
* [a,b] must be a superset of the free vars of [t1,t2,t3]
* The dfun must itself be quantified over [a,b]
+
+ * More specific instances come before less specific ones,
+ where they overlap
Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
[a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
--Jeff
+%************************************************************************
+%* *
+\subsection{Looking up an instance}
+%* *
+%************************************************************************
+
@lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
the env is kept ordered, the first match must be the only one. The
thing we are looking up can have an arbitrary "flexi" part.
key_vars = tyVarsOfTypes key_tys
find [] = NoMatch False
- find ((tpl_tyvars, tpl, val) : rest)
+ find ((tpl_tyvars, tpl, dfun_id) : rest)
= case matchTys tpl_tyvars tpl key_tys of
Nothing ->
+ -- Check for reverse match, so that
+ -- we bale out if a later instantiation of this
+ -- predicate might match this instance
+ -- [see notes about overlapping instances above]
case matchTys key_vars key_tys tpl of
Nothing -> find rest
Just (_, _) -> NoMatch (any_match rest)
Just (subst, leftovers) -> ASSERT( null leftovers )
- FoundInst subst val
+ FoundInst subst dfun_id
any_match rest = or [ maybeToBool (matchTys tvs tpl key_tys)
| (tvs,tpl,_) <- rest
]
\end{code}
-@addToClsInstEnv@ extends a @ClsInstEnv@, checking for overlaps.
+
+%************************************************************************
+%* *
+\subsection{Extending an instance environment}
+%* *
+%************************************************************************
+
+@extendInstEnv@ extends a @ClsInstEnv@, checking for overlaps.
A boolean flag controls overlap reporting.
\begin{code}
extendInstEnv :: DynFlags -> InstEnv -> [DFunId] -> (InstEnv, [Message])
-- Similar, but all we have is the DFuns
-extendInstEnv dflags env infos
- = go env [] infos
- where
- go env msgs [] = (env, msgs)
- go env msgs (dfun:dfuns) = case addToInstEnv dflags env dfun of
- Succeeded new_env -> go new_env msgs dfuns
- Failed dfun' -> go env (msg:msgs) dfuns
- where
- msg = dupInstErr dfun dfun'
-
-
-dupInstErr dfun1 dfun2
- -- Overlapping/duplicate instances for given class; msg could be more glamourous
- = hang (ptext SLIT("Duplicate or overlapping instance declarations:"))
- 2 (ppr_dfun dfun1 $$ ppr_dfun dfun2)
- where
- ppr_dfun dfun = ppr (getSrcLoc dfun) <> colon <+> ppr tau
- where
- (_,_,tau) = splitSigmaTy (idType dfun)
+extendInstEnv dflags env dfun_ids = foldl (addToInstEnv dflags) (env, []) dfun_ids
+
addToInstEnv :: DynFlags
- -> InstEnv -> DFunId
- -> MaybeErr InstEnv -- Success...
- DFunId -- Failure: Offending overlap
-
-addToInstEnv dflags inst_env dfun_id
- = case insert_into (classInstEnv inst_env clas) of
- Failed stuff -> Failed stuff
- Succeeded new_env -> Succeeded (addToUFM inst_env clas new_env)
-
+ -> (InstEnv, [Message])
+ -> DFunId
+ -> (InstEnv, [Message]) -- Resulting InstEnv and augmented error messages
+
+addToInstEnv dflags (inst_env, errs) dfun_id
+ -- Check first that the new instance doesn't
+ -- conflict with another. See notes below about fundeps.
+ | not (null bad_fundeps)
+ = (inst_env, fundep_err : errs) -- Bad fundeps; report the first only
+
+ | otherwise
+ = case insert_into cls_inst_env of
+ Failed err -> (inst_env, err : errs)
+ Succeeded new_env -> (addToUFM inst_env clas new_env, errs)
+
where
+ cls_inst_env = classInstEnv inst_env clas
(ins_tvs, _, clas, ins_tys) = splitDFunTy (idType dfun_id)
+ bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
+ fundep_err = fundepErr dfun_id (head bad_fundeps)
ins_tv_set = mkVarSet ins_tvs
- ins_item = (ins_tv_set, ins_tys, dfun_id)
+ ins_item = (ins_tv_set, ins_tys, dfun_id)
insert_into [] = returnMaB [ins_item]
- insert_into env@(cur_item@(tpl_tvs, tpl_tys, val) : rest)
-
- -- FAIL if:
- -- (a) they are the same, or
- -- (b) they unify, and any sort of overlap is prohibited,
- -- (c) they unify but neither is more specific than t'other
- | identical
- || (unifiable && not (dopt Opt_AllowOverlappingInstances dflags))
- || (unifiable && not (ins_item_more_specific || cur_item_more_specific))
- = failMaB val
-
- -- New item is an instance of current item, so drop it here
- | ins_item_more_specific = returnMaB (ins_item : env)
-
- -- Otherwise carry on
- | otherwise = insert_into rest `thenMaB` \ rest' ->
- returnMaB (cur_item : rest')
+ insert_into env@(cur_item@(tpl_tvs, tpl_tys, tpl_dfun_id) : rest)
+ = case unifyTyListsX (ins_tv_set `unionVarSet` tpl_tvs) tpl_tys ins_tys of
+ Just subst -> insert_unifiable env subst
+ Nothing -> carry_on cur_item rest
+
+ carry_on cur_item rest = insert_into rest `thenMaB` \ rest' ->
+ returnMaB (cur_item : rest')
+
+ -- The two templates unify. This is acceptable iff
+ -- (a) -fallow-overlapping-instances is on
+ -- (b) one is strictly more specific than the other
+ -- [It's bad if they are identical or incomparable]
+ insert_unifiable env@(cur_item@(tpl_tvs, tpl_tys, tpl_dfun_id) : rest) subst
+ | ins_item_more_specific && cur_item_more_specific
+ = -- Duplicates
+ failMaB (dupInstErr dfun_id tpl_dfun_id)
+
+ | not (dopt Opt_AllowOverlappingInstances dflags)
+ || not (ins_item_more_specific || cur_item_more_specific)
+ = -- Overlap illegal, or the two are incomparable
+ failMaB (overlapErr dfun_id tpl_dfun_id)
+
+ | otherwise
+ = -- OK, it's acceptable. Remaining question is whether
+ -- we drop it here or compare it with others
+ if ins_item_more_specific then
+ -- New item is an instance of current item, so drop it here
+ returnMaB (ins_item : env)
+ else
+ carry_on cur_item rest
+
where
- unifiable = maybeToBool (unifyTyListsX (ins_tv_set `unionVarSet` tpl_tvs) tpl_tys ins_tys)
- ins_item_more_specific = maybeToBool (matchTys tpl_tvs tpl_tys ins_tys)
- cur_item_more_specific = maybeToBool (matchTys ins_tv_set ins_tys tpl_tys)
- identical = ins_item_more_specific && cur_item_more_specific
+ ins_item_more_specific = allVars subst ins_tvs
+ cur_item_more_specific = allVars subst (varSetElems tpl_tvs)
+
+allVars :: TyVarSubstEnv -> [TyVar] -> Bool
+-- True iff all the type vars are mapped to distinct type vars
+allVars subst tvs
+ = allDistinctTyVars (map lookup tvs) emptyVarSet
+ where
+ lookup tv = case lookupSubstEnv subst tv of
+ Just (DoneTy ty) -> ty
+ Nothing -> mkTyVarTy tv
\end{code}
+Functional dependencies
+~~~~~~~~~~~~~~~~~~~~~~~
+Here is the bad case:
+ class C a b | a->b where ...
+ instance C Int Bool where ...
+ instance C Int Char where ...
+
+The point is that a->b, so Int in the first parameter must uniquely
+determine the second. In general, given the same class decl, and given
+
+ instance C s1 s2 where ...
+ instance C t1 t2 where ...
+Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
+
+\begin{code}
+badFunDeps :: ClsInstEnv -> Class
+ -> TyVarSet -> [Type] -- Proposed new instance type
+ -> [DFunId]
+badFunDeps cls_inst_env clas ins_tv_set ins_tys
+ = [ dfun_id | fd <- fds,
+ (tvs, tys, dfun_id) <- cls_inst_env,
+ not (null (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys))
+ ]
+ where
+ (clas_tvs, fds) = classTvsFds clas
+\end{code}
+
+
+\begin{code}
+dupInstErr dfun1 dfun2 = addInstErr (ptext SLIT("Duplicate instance declarations:")) dfun1 dfun2
+overlapErr dfun1 dfun2 = addInstErr (ptext SLIT("Overlapping instance declarations:")) dfun1 dfun2
+fundepErr dfun1 dfun2 = addInstErr (ptext SLIT("Functional dependencies conflict between instance declarations:"))
+ dfun1 dfun2
+
+addInstErr what dfun1 dfun2
+ = hang what 2 (ppr_dfun dfun1 $$ ppr_dfun dfun2)
+ where
+ ppr_dfun dfun = ppr (getSrcLoc dfun) <> colon <+> pprClassPred clas tys
+ where
+ (_,_,clas,tys) = splitDFunTy (idType dfun)
+\end{code}
module PprType(
pprKind, pprParendKind,
pprType, pprParendType,
- pprConstraint, pprPred, pprTheta,
+ pprPred, pprTheta, pprClassPred,
pprTyVarBndr, pprTyVarBndrs,
-- Junk
predRepTy, isUTyVar
)
import Var ( TyVar, tyVarKind )
+import Class ( Class )
import TyCon ( TyCon, isPrimTyCon, isTupleTyCon, tupleTyConBoxity,
maybeTyConSingleCon, isEnumerationTyCon,
tyConArity, tyConName
)
-import Class ( Class )
-- others:
import CmdLineOpts ( opt_PprStyle_RawTypes )
import Maybes ( maybeToBool )
import Name ( getOccString, getOccName )
import Outputable
-import PprEnv
import Unique ( Uniquable(..) )
import BasicTypes ( tupleParens )
import PrelNames -- quite a few *Keys
\begin{code}
pprType, pprParendType :: Type -> SDoc
-pprType ty = ppr_ty pprTyEnv tOP_PREC ty
-pprParendType ty = ppr_ty pprTyEnv tYCON_PREC ty
+pprType ty = ppr_ty tOP_PREC ty
+pprParendType ty = ppr_ty tYCON_PREC ty
pprKind, pprParendKind :: Kind -> SDoc
pprKind = pprType
pprParendKind = pprParendType
pprPred :: PredType -> SDoc
-pprPred (Class clas tys) = pprConstraint clas tys
+pprPred (Class clas tys) = pprClassPred clas tys
pprPred (IParam n ty) = hsep [ptext SLIT("?") <> ppr n,
ptext SLIT("::"), ppr ty]
-pprConstraint :: Class -> [Type] -> SDoc
-pprConstraint clas tys = ppr clas <+> hsep (map pprParendType tys)
+pprClassPred :: Class -> [Type] -> SDoc
+pprClassPred clas tys = ppr clas <+> hsep (map pprParendType tys)
pprTheta :: ThetaType -> SDoc
pprTheta theta = parens (hsep (punctuate comma (map pprPred theta)))
\end{code}
\begin{code}
-ppr_ty :: PprEnv TyVar -> Int -> Type -> SDoc
-ppr_ty env ctxt_prec (TyVarTy tyvar)
- = pTyVarO env tyvar
+ppr_ty :: Int -> Type -> SDoc
+ppr_ty ctxt_prec (TyVarTy tyvar)
+ = ppr tyvar
-ppr_ty env ctxt_prec ty@(TyConApp tycon tys)
+ppr_ty ctxt_prec ty@(TyConApp tycon tys)
-- KIND CASE; it's of the form (Type x)
| tycon `hasKey` typeConKey && n_tys == 1
= -- For kinds, print (Type x) as just x if x is a
-- LIST CASE
| tycon `hasKey` listTyConKey && n_tys == 1
- = brackets (ppr_ty env tOP_PREC ty1)
+ = brackets (ppr_ty tOP_PREC ty1)
-- DICTIONARY CASE, prints {C a}
-- This means that instance decls come out looking right in interfaces
-- and that in turn means they get "gated" correctly when being slurped in
| maybeToBool maybe_pred
- = braces (ppr_pred env pred)
+ = braces (pprPred pred)
-- NO-ARGUMENT CASE (=> no parens)
| null tys
(ty1:_) = tys
Just pred = maybe_pred
maybe_pred = splitPredTy_maybe ty -- Checks class and arity
- tys_w_commas = sep (punctuate comma (map (ppr_ty env tOP_PREC) tys))
- tys_w_spaces = sep (map (ppr_ty env tYCON_PREC) tys)
+ tys_w_commas = sep (punctuate comma (map (ppr_ty tOP_PREC) tys))
+ tys_w_spaces = sep (map (ppr_ty tYCON_PREC) tys)
-ppr_ty env ctxt_prec ty@(ForAllTy _ _)
+ppr_ty ctxt_prec ty@(ForAllTy _ _)
= getPprStyle $ \ sty ->
maybeParen ctxt_prec fUN_PREC $
sep [ ptext SLIT("forall") <+> pp_tyvars sty <> ptext SLIT("."),
ppr_theta theta,
- ppr_ty env tOP_PREC tau
+ ppr_ty tOP_PREC tau
]
where
(tyvars, rho) = splitForAllTys ty
(theta, tau) = splitRhoTy rho
- pp_tyvars sty = hsep (map (pBndr env LambdaBind) some_tyvars)
+ pp_tyvars sty = hsep (map pprTyVarBndr some_tyvars)
where
some_tyvars | userStyle sty && not opt_PprStyle_RawTypes
= filter (not . isUTyVar) tyvars -- hide uvars from user
| otherwise
= tyvars
- ppr_theta [] = empty
- ppr_theta theta = parens (hsep (punctuate comma (map (ppr_pred env) theta)))
- <+> ptext SLIT("=>")
+ ppr_theta [] = empty
+ ppr_theta theta = pprTheta theta <+> ptext SLIT("=>")
-ppr_ty env ctxt_prec (FunTy ty1 ty2)
+ppr_ty ctxt_prec (FunTy ty1 ty2)
-- we don't want to lose usage annotations or synonyms,
-- so we mustn't use splitFunTys here.
= maybeParen ctxt_prec fUN_PREC $
- sep [ ppr_ty env fUN_PREC ty1
- , ptext SLIT("->") <+> ppr_ty env tOP_PREC ty2
+ sep [ ppr_ty fUN_PREC ty1
+ , ptext SLIT("->") <+> ppr_ty tOP_PREC ty2
]
-ppr_ty env ctxt_prec (AppTy ty1 ty2)
+ppr_ty ctxt_prec (AppTy ty1 ty2)
= maybeParen ctxt_prec tYCON_PREC $
- ppr_ty env fUN_PREC ty1 <+> ppr_ty env tYCON_PREC ty2
+ ppr_ty fUN_PREC ty1 <+> ppr_ty tYCON_PREC ty2
-ppr_ty env ctxt_prec (UsageTy u ty)
+ppr_ty ctxt_prec (UsageTy u ty)
= maybeParen ctxt_prec tYCON_PREC $
- ptext SLIT("__u") <+> ppr_ty env tYCON_PREC u
- <+> ppr_ty env tYCON_PREC ty
+ ptext SLIT("__u") <+> ppr_ty tYCON_PREC u
+ <+> ppr_ty tYCON_PREC ty
-- fUN_PREC would be logical for u, but it yields a reduce/reduce conflict with AppTy
-ppr_ty env ctxt_prec (NoteTy (SynNote ty) expansion)
- = ppr_ty env ctxt_prec ty
--- = ppr_ty env ctxt_prec expansion -- if we don't want to see syntys
+ppr_ty ctxt_prec (NoteTy (SynNote ty) expansion)
+ = ppr_ty ctxt_prec ty
+-- = ppr_ty ctxt_prec expansion -- if we don't want to see syntys
-ppr_ty env ctxt_prec (NoteTy (FTVNote _) ty) = ppr_ty env ctxt_prec ty
+ppr_ty ctxt_prec (NoteTy (FTVNote _) ty) = ppr_ty ctxt_prec ty
-ppr_ty env ctxt_prec (PredTy p) = braces (ppr_pred env p)
-
-ppr_pred env (Class clas tys) = ppr clas <+>
- hsep (map (ppr_ty env tYCON_PREC) tys)
-ppr_pred env (IParam n ty) = hsep [char '?' <> ppr n, text "::",
- ppr_ty env tYCON_PREC ty]
-\end{code}
-
-\begin{code}
-pprTyEnv = initPprEnv b (Just ppr) b (Just (\site -> pprTyVarBndr)) b
- where
- b = panic "PprType:init_ppr_env"
+ppr_ty ctxt_prec (PredTy p) = braces (pprPred p)
\end{code}
and when in debug mode.
\begin{code}
+pprTyVarBndr :: TyVar -> SDoc
pprTyVarBndr tyvar
= getPprStyle $ \ sty ->
if (ifaceStyle sty && kind /= liftedTypeKind) || debugStyle sty then
isUsageKind, isUsage, isUTyVar,
-- Predicates and the like
- mkDictTy, mkDictTys, mkPredTy, splitPredTy_maybe,
+ mkDictTy, mkDictTys, mkPredTy, splitPredTy_maybe, predTyUnique,
splitDictTy, splitDictTy_maybe, isDictTy, predRepTy, splitDFunTy,
mkSynTy, deNoteType,
TauType, RhoType, SigmaType, PredType(..), ThetaType,
ClassPred, ClassContext, mkClassPred,
- getClassTys_maybe, ipName_maybe, classesOfPreds,
+ getClassTys_maybe, predMentionsIPs, classesOfPreds,
isTauTy, mkRhoTy, splitRhoTy, splitMethodTy,
mkSigmaTy, isSigmaTy, splitSigmaTy,
getDFunTyKey,
import VarEnv
import VarSet
-import Name ( Name, NamedThing(..), OccName, mkLocalName, tidyOccName )
+import Name ( NamedThing(..), OccName, mkLocalName, tidyOccName )
import NameSet
import Class ( classTyCon, Class, ClassPred, ClassContext )
import TyCon ( TyCon,
import Maybes ( maybeToBool )
import SrcLoc ( noSrcLoc )
import PrimRep ( PrimRep(..) )
-import Unique ( Uniquable(..) )
+import Unique ( Unique, Uniquable(..) )
import Util ( mapAccumL, seqList, thenCmp )
import Outputable
import UniqSet ( sizeUniqSet ) -- Should come via VarSet
mkPredTy :: PredType -> Type
mkPredTy pred = PredTy pred
+predTyUnique :: PredType -> Unique
+predTyUnique (IParam n _) = getUnique n
+predTyUnique (Class clas tys) = getUnique clas
+
predRepTy :: PredType -> Type
-- Convert a predicate to its "representation type";
-- the type of evidence for that predicate, which is actually passed at runtime
getClassTys_maybe (Class clas tys) = Just (clas, tys)
getClassTys_maybe _ = Nothing
-ipName_maybe :: PredType -> Maybe Name
-ipName_maybe (IParam n _) = Just n
-ipName_maybe _ = Nothing
+predMentionsIPs :: PredType -> NameSet -> Bool
+predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
+predMentionsIPs other ns = False
classesOfPreds :: ThetaType -> ClassContext
classesOfPreds theta = [(clas,tys) | Class clas tys <- theta]
compare p1 p2 = cmpPred emptyVarEnv p1 p2
cmpPred :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
-cmpPred env (IParam n1 t) (IParam n2 t2) = n1 `compare` n2
- -- Just compare the names!
+cmpPred env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+ -- Compare types as well as names for implicit parameters
+ -- This comparison is used exclusively (I think) for the
+ -- finite map built in TcSimplify
cmpPred env (Class c1 tys1) (Class c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
cmpPred env (IParam _ _) (Class _ _) = LT
cmpPred env (Class _ _) (IParam _ _) = GT
use an explicit substitution
\begin{code}
-module Unify ( unifyTysX, unifyTyListsX,
- match, matchTy, matchTys
+module Unify ( unifyTysX, unifyTyListsX, allDistinctTyVars,
+ match, matchTy, matchTys,
) where
#include "HsVersions.h"
import TypeRep ( Type(..) ) -- friend
-import Type ( typeKind, tyVarsOfType, splitAppTy_maybe,
+import Type ( typeKind, tyVarsOfType, splitAppTy_maybe, getTyVar_maybe,
splitUTy, isUTy, deNoteType
)
%* *
%************************************************************************
+(allDistinctTyVars tys tvs) = True
+ iff
+all the types tys are type variables,
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables. For example, if the type sig is
+ f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't
+ (a) been unified with a non-tyvar type
+ (b) been unified with each other (all distinct)
+ (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars [] acc
+ = True
+allDistinctTyVars (ty:tys) acc
+ = case getTyVar_maybe ty of
+ Nothing -> False -- (a)
+ Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
+ | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Unification with an explicit substitution}
+%* *
+%************************************************************************
+
Unify types with an explicit substitution and no monad.
Ignore usage annotations.
projects / ghc-hetmet.git / commitdiff