\begin{code}
module Inst (
- Inst,
+ Inst,
pprInstances, pprDictsTheta, pprDictsInFull, -- User error messages
showLIE, pprInst, pprInsts, pprInstInFull, -- Debugging messages
tidyInsts, tidyMoreInsts,
newDictBndr, newDictBndrs, newDictBndrsO,
+ newDictOccs, newDictOcc,
instCall, instStupidTheta,
cloneDict, mkOverLit,
newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy,
tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE,
ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
- getDictClassTys, dictPred,
+ growInstsTyVars, getDictClassTys, dictPred,
lookupSimpleInst, LookupInstResult(..),
tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
InstOrigin(..), InstLoc, pprInstLoc,
- mkWantedCo, mkGivenCo,
- fromWantedCo, fromGivenCo,
- eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
- finalizeEqInst, writeWantedCoercion,
- eqInstType, updateEqInstCoercion,
- eqInstCoercion, eqInstTys
+ mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo,
+ mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo,
+ mkTyConEqInstCo, mkFunEqInstCo,
+ wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst,
+ wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion,
+ eqInstTys
) where
#include "HsVersions.h"
import FunDeps
import TcMType
import TcType
-import DsUtils
+import MkCore
+import TyCon
import Type
import TypeRep
import Class
\end{code}
+
Selection
~~~~~~~~~
\begin{code}
instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
tci_wanted = wanteds})
= mkLocalId nm (mkImplicTy tvs givens wanteds)
-instToVar i@(EqInst {})
- = eitherEqInst i id (\(TyVarTy covar) -> covar)
+instToVar inst@(EqInst {})
+ = eitherEqInst inst id assertCoVar
+ where
+ assertCoVar (TyVarTy cotv) = cotv
+ assertCoVar coty = pprPanic "Inst.instToVar" (ppr coty)
instType :: Inst -> Type
instType (LitInst {tci_ty = ty}) = ty
getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred
getDictClassTys inst = pprPanic "getDictClassTys" (ppr inst)
+--------------------------------
-- fdPredsOfInst is used to get predicates that contain functional
-- dependencies *or* might do so. The "might do" part is because
-- a constraint (C a b) might have a superclass with FDs
fdPredsOfInst :: Inst -> [TcPredType]
fdPredsOfInst (Dict {tci_pred = pred}) = [pred]
fdPredsOfInst (Method {tci_theta = theta}) = theta
-fdPredsOfInst (ImplicInst {tci_given = gs,
- tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws)
+fdPredsOfInst (ImplicInst {tci_wanted = ws}) = fdPredsOfInsts ws
+ -- The ImplicInst case doesn't look right;
+ -- what if ws mentions skolem variables?
fdPredsOfInst (LitInst {}) = []
fdPredsOfInst (EqInst {}) = []
fdPredsOfInsts :: [Inst] -> [PredType]
fdPredsOfInsts insts = concatMap fdPredsOfInst insts
+---------------------------------
isInheritableInst :: Inst -> Bool
isInheritableInst (Dict {tci_pred = pred}) = isInheritablePred pred
isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta
addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs
\end{code}
-Predicates
-~~~~~~~~~~
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growInstsTyVars insts tvs) is the result of extending the set
+ of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then grow precs tvs = {a,b,c}
+
+All the type variables from an implicit parameter are added, whether or
+not they are mentioned in tvs; see Note [Implicit parameters and ambiguity]
+in TcSimplify.
+
+See also Note [Ambiguity] in TcSimplify
+
+\begin{code}
+growInstsTyVars :: [Inst] -> TyVarSet -> TyVarSet
+growInstsTyVars insts tvs
+ | null insts = tvs
+ | otherwise = fixVarSet mk_next tvs
+ where
+ mk_next tvs = foldr grow_inst_tvs tvs insts
+
+grow_inst_tvs :: Inst -> TyVarSet -> TyVarSet
+grow_inst_tvs (Dict {tci_pred = pred}) tvs = growPredTyVars pred tvs
+grow_inst_tvs (Method {tci_theta = theta}) tvs = foldr growPredTyVars tvs theta
+grow_inst_tvs (ImplicInst {tci_tyvars = tvs1, tci_wanted = ws}) tvs
+ = tvs `unionVarSet` (foldr grow_inst_tvs (tvs `delVarSetList` tvs1) ws
+ `delVarSetList` tvs1)
+grow_inst_tvs inst tvs -- EqInst, LitInst
+ = growTyVars (tyVarsOfInst inst) tvs
+\end{code}
+
+
+%************************************************************************
+%* *
+ Predicates
+%* *
+%************************************************************************
+
\begin{code}
isAbstractableInst :: Inst -> Bool
newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
newDictBndr :: InstLoc -> TcPredType -> TcM Inst
+-- Makes a "given"
newDictBndr inst_loc pred@(EqPred ty1 ty2)
= do { uniq <- newUnique
; let name = mkPredName uniq inst_loc pred
+ co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))
; return (EqInst {tci_name = name,
tci_loc = inst_loc,
tci_left = ty1,
tci_right = ty2,
- tci_co = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))})
- }
-newDictBndr inst_loc pred
+ tci_co = co }) }
+
+newDictBndr inst_loc pred = newDict inst_loc pred
+
+-------------------
+newDictOccs :: InstLoc -> TcThetaType -> TcM [Inst]
+newDictOccs inst_loc theta = mapM (newDictOcc inst_loc) theta
+
+newDictOcc :: InstLoc -> TcPredType -> TcM Inst
+-- Makes a "wanted"
+newDictOcc inst_loc pred@(EqPred ty1 ty2)
+ = do { uniq <- newUnique
+ ; cotv <- newMetaCoVar ty1 ty2
+ ; let name = mkPredName uniq inst_loc pred
+ ; return (EqInst {tci_name = name,
+ tci_loc = inst_loc,
+ tci_left = ty1,
+ tci_right = ty2,
+ tci_co = Left cotv }) }
+
+newDictOcc inst_loc pred = newDict inst_loc pred
+
+----------------
+newDict :: InstLoc -> TcPredType -> TcM Inst
+-- Always makes a Dict, not an EqInst
+newDict inst_loc pred
= do { uniq <- newUnique
; let name = mkPredName uniq inst_loc pred
; return (Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}) }
instCallDicts loc (EqPred ty1 ty2 : preds)
= do { traceTc (text "instCallDicts" <+> ppr (EqPred ty1 ty2))
; coi <- boxyUnify ty1 ty2
--- ; coi <- unifyType ty1 ty2
; let co = fromCoI coi ty1
; co_fn <- instCallDicts loc preds
; return (co_fn <.> WpTyApp co) }
instCallDicts loc (pred : preds)
- = do { uniq <- newUnique
- ; let name = mkPredName uniq loc pred
- dict = Dict {tci_name = name, tci_pred = pred, tci_loc = loc}
+ = do { dict <- newDict loc pred
; extendLIE dict
; co_fn <- instCallDicts loc preds
; return (co_fn <.> WpApp (instToId dict)) }
-------------
cloneDict :: Inst -> TcM Inst
cloneDict dict@(Dict nm _ _) = do { uniq <- newUnique
- ; return (dict {tci_name = setNameUnique nm uniq}) }
-cloneDict eq@(EqInst {}) = return eq
+ ; return (dict {tci_name = setNameUnique nm uniq}) }
+cloneDict eq@(EqInst {}) = return eq
cloneDict other = pprPanic "cloneDict" (ppr other)
-- For vanilla implicit parameters, there is only one in scope
-- scope, so we make up a new namea.
newIPDict :: InstOrigin -> IPName Name -> Type
-> TcM (IPName Id, Inst)
-newIPDict orig ip_name ty = do
- inst_loc <- getInstLoc orig
- uniq <- newUnique
- let
- pred = IParam ip_name ty
- name = mkPredName uniq inst_loc pred
- dict = Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}
-
- return (mapIPName (\_ -> instToId dict) ip_name, dict)
+newIPDict orig ip_name ty
+ = do { inst_loc <- getInstLoc orig
+ ; dict <- newDict inst_loc (IParam ip_name ty)
+ ; return (mapIPName (\_ -> instToId dict) ip_name, dict) }
\end{code}
-- we use the outermost tycon of the lhs, if there is one, to
-- improve readability of Core code
baseOcc = case splitTyConApp_maybe ty of
- Nothing -> mkOccName tcName "$"
+ Nothing -> mkTcOcc "$"
Just (tc, _) -> getOccName tc
\end{code}
\begin{code}
zonkInst :: Inst -> TcM Inst
-zonkInst dict@(Dict { tci_pred = pred}) = do
+zonkInst dict@(Dict {tci_pred = pred}) = do
new_pred <- zonkTcPredType pred
return (dict {tci_pred = new_pred})
(\co -> liftM mkGivenCo $ zonkTcType co)
; ty1' <- zonkTcType ty1
; ty2' <- zonkTcType ty2
- ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' })
+ ; return (eqinst {tci_co = co', tci_left = ty1', tci_right = ty2' })
}
zonkInsts :: [Inst] -> TcRn [Inst]
record_dfun_usage dfun_id
= do { hsc_env <- getTopEnv
; let dfun_name = idName dfun_id
- dfun_mod = nameModule dfun_name
+ dfun_mod = ASSERT( isExternalName dfun_name )
+ nameModule dfun_name
; if isInternalName dfun_name || -- Internal name => defined in this module
modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
then return () -- internal, or in another package
%* *
%************************************************************************
+Operations on EqInstCo.
+
\begin{code}
-mkGivenCo :: Coercion -> Either TcTyVar Coercion
+mkGivenCo :: Coercion -> EqInstCo
mkGivenCo = Right
-mkWantedCo :: TcTyVar -> Either TcTyVar Coercion
+mkWantedCo :: TcTyVar -> EqInstCo
mkWantedCo = Left
-fromGivenCo :: Either TcTyVar Coercion -> Coercion
-fromGivenCo (Right co) = co
-fromGivenCo _ = panic "fromGivenCo: not a wanted coercion"
+isWantedCo :: EqInstCo -> Bool
+isWantedCo (Left _) = True
+isWantedCo _ = False
+
+eqInstCoType :: EqInstCo -> TcType
+eqInstCoType (Left cotv) = mkTyVarTy cotv
+eqInstCoType (Right co) = co
+\end{code}
+
+Coercion transformations on EqInstCo. These transformations work differently
+depending on whether a EqInstCo is for a wanted or local equality:
-fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
-fromWantedCo _ (Left covar) = covar
-fromWantedCo msg _ = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+ Local : apply the inverse of the specified coercion
+ Wanted: obtain a fresh coercion hole (meta tyvar) and update the old hole
+ to be the specified coercion applied to the new coercion hole
+
+\begin{code}
+-- Coercion transformation: co = id
+--
+mkIdEqInstCo :: EqInstCo -> Type -> TcM ()
+mkIdEqInstCo (Left cotv) t
+ = writeMetaTyVar cotv t
+mkIdEqInstCo (Right _) _
+ = return ()
+
+-- Coercion transformation: co = sym co'
+--
+mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo
+mkSymEqInstCo (Left cotv) (ty1, ty2)
+ = do { cotv' <- newMetaCoVar ty1 ty2
+ ; writeMetaTyVar cotv (mkSymCoercion (TyVarTy cotv'))
+ ; return $ Left cotv'
+ }
+mkSymEqInstCo (Right co) _
+ = return $ Right (mkSymCoercion co)
+
+-- Coercion transformation: co = co' |> given_co
+--
+mkLeftTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
+mkLeftTransEqInstCo (Left cotv) given_co (ty1, ty2)
+ = do { cotv' <- newMetaCoVar ty1 ty2
+ ; writeMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co)
+ ; return $ Left cotv'
+ }
+mkLeftTransEqInstCo (Right co) given_co _
+ = return $ Right (co `mkTransCoercion` mkSymCoercion given_co)
+
+-- Coercion transformation: co = given_co |> co'
+--
+mkRightTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
+mkRightTransEqInstCo (Left cotv) given_co (ty1, ty2)
+ = do { cotv' <- newMetaCoVar ty1 ty2
+ ; writeMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv')
+ ; return $ Left cotv'
+ }
+mkRightTransEqInstCo (Right co) given_co _
+ = return $ Right (mkSymCoercion given_co `mkTransCoercion` co)
+
+-- Coercion transformation: co = col cor
+--
+mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
+ -> TcM (EqInstCo, EqInstCo)
+mkAppEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
+ = do { cotv_l <- newMetaCoVar ty1_l ty2_l
+ ; cotv_r <- newMetaCoVar ty1_r ty2_r
+ ; writeMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
+ ; return (Left cotv_l, Left cotv_r)
+ }
+mkAppEqInstCo (Right co) _ _
+ = return (Right $ mkLeftCoercion co, Right $ mkRightCoercion co)
+
+-- Coercion transformation: co = con col -> cor
+--
+mkTyConEqInstCo :: EqInstCo -> TyCon -> [(Type, Type)] -> TcM ([EqInstCo])
+mkTyConEqInstCo (Left cotv) con ty12s
+ = do { cotvs <- mapM (uncurry newMetaCoVar) ty12s
+ ; writeMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs))
+ ; return (map Left cotvs)
+ }
+mkTyConEqInstCo (Right co) _ args
+ = return $ map (\mkCoes -> Right $ foldl (.) id mkCoes co) mkCoes
+ -- make cascades of the form
+ -- mkRightCoercion (mkLeftCoercion .. (mkLeftCoercion co)..)
+ where
+ n = length args
+ mkCoes = [mkRightCoercion : replicate i mkLeftCoercion | i <- [n-1, n-2..0]]
+
+-- Coercion transformation: co = col -> cor
+--
+mkFunEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
+ -> TcM (EqInstCo, EqInstCo)
+mkFunEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
+ = do { cotv_l <- newMetaCoVar ty1_l ty2_l
+ ; cotv_r <- newMetaCoVar ty1_r ty2_r
+ ; writeMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
+ ; return (Left cotv_l, Left cotv_r)
+ }
+mkFunEqInstCo (Right co) _ _
+ = return (Right $ mkRightCoercion (mkLeftCoercion co),
+ Right $ mkRightCoercion co)
+\end{code}
+
+Operations on entire EqInst.
+
+\begin{code}
+-- |A wanted equality is unsolved as long as its cotv is unfilled.
+--
+wantedEqInstIsUnsolved :: Inst -> TcM Bool
+wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv})
+ = liftM not $ isFilledMetaTyVar cotv
+wantedEqInstIsUnsolved _ = return True
eitherEqInst :: Inst -- given or wanted EqInst
-> (TcTyVar -> a) -- result if wanted
Right co -> withGiven co
eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
-mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst]
-mkEqInsts preds cos = zipWithM mkEqInst preds cos
-
-mkEqInst :: PredType -> Either TcTyVar Coercion -> TcM Inst
+mkEqInst :: PredType -> EqInstCo -> TcM Inst
mkEqInst (EqPred ty1 ty2) co
= do { uniq <- newUnique
; src_span <- getSrcSpanM
; err_ctxt <- getErrCtxt
; let loc = InstLoc EqOrigin src_span err_ctxt
name = mkName uniq src_span
- inst = EqInst {tci_left = ty1, tci_right = ty2, tci_co = co, tci_loc = loc, tci_name = name}
+ inst = EqInst { tci_left = ty1
+ , tci_right = ty2
+ , tci_co = co
+ , tci_loc = loc
+ , tci_name = name
+ }
; return inst
}
- where mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
+ where
+ mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred)
mkWantedEqInst :: PredType -> TcM Inst
}
mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred)
--- type inference:
--- We want to promote the wanted EqInst to a given EqInst
--- in the signature context.
--- This means we have to give the coercion a name
--- and fill it in as its own name.
-finalizeEqInst
- :: Inst -- wanted
- -> TcM Inst -- given
-finalizeEqInst wanted@(EqInst {tci_left = ty1, tci_right = ty2, tci_name = name})
- = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
- ; writeWantedCoercion wanted (TyVarTy var)
- ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
- ; return given
- }
-finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i)
+-- Turn a wanted equality into a local that propagates the uninstantiated
+-- coercion variable as witness. We need this to propagate wanted irreds into
+-- attempts to solve implication constraints.
+--
+wantedToLocalEqInst :: Inst -> Inst
+wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv})
+ = eq {tci_co = Right (mkTyVarTy cotv)}
+wantedToLocalEqInst eq = eq
+
+-- Turn a wanted into a local EqInst (needed during type inference for
+-- signatures)
+--
+-- * Give it a name and change the coercion around.
+--
+finalizeEqInst :: Inst -- wanted
+ -> TcM Inst -- given
+finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2,
+ tci_name = name, tci_co = Left cotv})
+ = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
+
+ -- fill the coercion hole
+ ; writeMetaTyVar cotv (TyVarTy var)
+
+ -- set the new coercion
+ ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
+ ; return given
+ }
-writeWantedCoercion
- :: Inst -- wanted EqInst
- -> Coercion -- coercion to fill the hole with
- -> TcM ()
-writeWantedCoercion wanted co
- = do { let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted
- ; writeMetaTyVar cotv co
- }
+finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i)
eqInstType :: Inst -> TcType
eqInstType inst = eitherEqInst inst mkTyVarTy id
-eqInstCoercion :: Inst -> Either TcTyVar Coercion
+eqInstCoercion :: Inst -> EqInstCo
eqInstCoercion = tci_co
eqInstTys :: Inst -> (TcType, TcType)
eqInstTys inst = (tci_left inst, tci_right inst)
-
-updateEqInstCoercion :: (Either TcTyVar Coercion -> Either TcTyVar Coercion) -> Inst -> Inst
-updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst}
\end{code}