X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FInst.lhs;h=17dce300f00ad2276d200cea6a1faa0cbab1d9dd;hp=77ca56a10e7c57dde8880f884c051c1df9401311;hb=c4ec8f2a77894af1c6160c4e8ad5625ab62f0bea;hpb=61d2625ae2e6a4cdae2ffc92df828905e81c24cc diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 77ca56a..17dce30 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -1,116 +1,154 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section[Inst]{The @Inst@ type: dictionaries or method instances} + +The @Inst@ type: dictionaries or method instances \begin{code} module Inst ( - Inst, + Inst, pprInstances, pprDictsTheta, pprDictsInFull, -- User error messages showLIE, pprInst, pprInsts, pprInstInFull, -- Debugging messages tidyInsts, tidyMoreInsts, - newDicts, newDictAtLoc, newDictsAtLoc, cloneDict, - shortCutFracLit, shortCutIntLit, newIPDict, - newMethod, newMethodFromName, newMethodWithGivenTy, - tcInstClassOp, tcInstStupidTheta, + newDictBndr, newDictBndrs, newDictBndrsO, + instCall, instStupidTheta, + cloneDict, mkOverLit, + newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy, + tcInstClassOp, tcSyntaxName, isHsVar, tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts, - instLoc, getDictClassTys, dictPred, + getDictClassTys, dictPred, - lookupInst, LookupInstResult(..), lookupPred, + lookupSimpleInst, LookupInstResult(..), tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag, - isDict, isClassDict, isMethod, - isLinearInst, linearInstType, isIPDict, isInheritableInst, + isAbstractableInst, isEqInst, + isDict, isClassDict, isMethod, isImplicInst, + isIPDict, isInheritableInst, isMethodOrLit, isTyVarDict, isMethodFor, zonkInst, zonkInsts, - instToId, instName, - - InstOrigin(..), InstLoc(..), pprInstLoc + instToId, instToVar, instType, instName, instToDictBind, + addInstToDictBind, + + InstOrigin(..), InstLoc, pprInstLoc, + + mkWantedCo, mkGivenCo, + isWantedCo, fromWantedCo, fromGivenCo, eqInstCoType, + mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo, + mkRightTransEqInstCo, mkAppEqInstCo, + eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, finalizeEqInst, + eqInstType, updateEqInstCoercion, + eqInstCoercion, eqInstTys ) where #include "HsVersions.h" import {-# SOURCE #-} TcExpr( tcPolyExpr ) +import {-# SOURCE #-} TcUnify( boxyUnify {- , unifyType -} ) -import HsSyn ( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp, - nlHsLit, nlHsVar ) -import TcHsSyn ( mkHsTyApp, mkHsDictApp, zonkId ) +import FastString +import HsSyn +import TcHsSyn import TcRnMonad -import TcEnv ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy ) -import InstEnv ( DFunId, InstEnv, Instance(..), OverlapFlag(..), - lookupInstEnv, extendInstEnv, pprInstances, - instanceHead, instanceDFunId, setInstanceDFunId ) -import FunDeps ( checkFunDeps ) -import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, zonkTcThetaType, - tcInstTyVar, tcInstSkolType - ) -import TcType ( Type, TcType, TcThetaType, TcTyVarSet, TcPredType, - BoxyRhoType, - PredType(..), SkolemInfo(..), typeKind, mkSigmaTy, - tcSplitForAllTys, applyTys, - tcSplitPhiTy, tcSplitDFunHead, - isIntTy,isFloatTy, isIntegerTy, isDoubleTy, - mkPredTy, mkTyVarTys, - tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred, - isClassPred, isTyVarClassPred, isLinearPred, - getClassPredTys, mkPredName, - isInheritablePred, isIPPred, - tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy, - pprPred, pprParendType, pprTheta - ) -import Type ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSubst, - notElemTvSubst, extendTvSubstList ) -import Unify ( tcMatchTys ) -import Module ( modulePackageId ) -import Kind ( isSubKind ) -import HscTypes ( ExternalPackageState(..), HscEnv(..) ) -import CoreFVs ( idFreeTyVars ) -import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName, dataConWrapId ) -import Id ( Id, idName, idType, mkUserLocal, mkLocalId ) -import Name ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule, - isInternalName, setNameUnique ) -import NameSet ( addOneToNameSet ) -import Literal ( inIntRange ) -import Var ( TyVar, tyVarKind, setIdType ) -import VarEnv ( TidyEnv, emptyTidyEnv ) -import VarSet ( elemVarSet, emptyVarSet, unionVarSet, mkVarSet ) -import TysWiredIn ( floatDataCon, doubleDataCon ) -import PrelNames ( integerTyConName, fromIntegerName, fromRationalName, rationalTyConName ) -import BasicTypes( IPName(..), mapIPName, ipNameName ) -import UniqSupply( uniqsFromSupply ) -import SrcLoc ( mkSrcSpan, noLoc, unLoc, Located(..) ) -import DynFlags ( DynFlag(..), DynFlags(..), dopt ) -import Maybes ( isJust ) +import TcEnv +import InstEnv +import FunDeps +import TcMType +import TcType +import MkCore +import Type +import TypeRep +import Class +import Unify +import Module +import Coercion +import HscTypes +import CoreFVs +import Id +import Name +import NameSet +import Var ( Var, TyVar ) +import qualified Var +import VarEnv +import VarSet +import PrelNames +import BasicTypes +import SrcLoc +import DynFlags +import Bag +import Maybes +import Util +import Unique import Outputable +import Data.List + +import Control.Monad \end{code} + Selection ~~~~~~~~~ \begin{code} instName :: Inst -> Name -instName inst = idName (instToId inst) +instName (EqInst {tci_name = name}) = name +instName inst = Var.varName (instToVar inst) instToId :: Inst -> TcId -instToId (LitInst nm _ ty _) = mkLocalId nm ty -instToId (Dict nm pred _) = mkLocalId nm (mkPredTy pred) -instToId (Method id _ _ _ _) = id - -instLoc (Dict _ _ loc) = loc -instLoc (Method _ _ _ _ loc) = loc -instLoc (LitInst _ _ _ loc) = loc - -dictPred (Dict _ pred _ ) = pred -dictPred inst = pprPanic "dictPred" (ppr inst) - -getDictClassTys (Dict _ pred _) = getClassPredTys pred +instToId inst = WARN( not (isId id), ppr inst ) + id + where + id = instToVar inst + +instToVar :: Inst -> Var +instToVar (LitInst {tci_name = nm, tci_ty = ty}) + = mkLocalId nm ty +instToVar (Method {tci_id = id}) + = id +instToVar (Dict {tci_name = nm, tci_pred = pred}) + | isEqPred pred = Var.mkCoVar nm (mkPredTy pred) + | otherwise = mkLocalId nm (mkPredTy pred) +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) + +instType :: Inst -> Type +instType (LitInst {tci_ty = ty}) = ty +instType (Method {tci_id = id}) = idType id +instType (Dict {tci_pred = pred}) = mkPredTy pred +instType imp@(ImplicInst {}) = mkImplicTy (tci_tyvars imp) (tci_given imp) + (tci_wanted imp) +-- instType i@(EqInst {tci_co = co}) = eitherEqInst i TyVarTy id +instType (EqInst {tci_left = ty1, tci_right = ty2}) = mkPredTy (EqPred ty1 ty2) + +mkImplicTy :: [TyVar] -> [Inst] -> [Inst] -> Type +mkImplicTy tvs givens wanteds -- The type of an implication constraint + = ASSERT( all isAbstractableInst givens ) + -- pprTrace "mkImplicTy" (ppr givens) $ + -- See [Equational Constraints in Implication Constraints] + let dict_wanteds = filter (not . isEqInst) wanteds + in + mkForAllTys tvs $ + mkPhiTy (map dictPred givens) $ + mkBigCoreTupTy (map instType dict_wanteds) + +dictPred :: Inst -> TcPredType +dictPred (Dict {tci_pred = pred}) = pred +dictPred (EqInst {tci_left=ty1,tci_right=ty2}) = EqPred ty1 ty2 +dictPred inst = pprPanic "dictPred" (ppr inst) + +getDictClassTys :: Inst -> (Class, [Type]) +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 @@ -118,79 +156,108 @@ getDictClassTys (Dict _ pred _) = getClassPredTys pred -- Leaving these in is really important for the call to fdPredsOfInsts -- in TcSimplify.inferLoop, because the result is fed to 'grow', -- which is supposed to be conservative -fdPredsOfInst (Dict _ pred _) = [pred] -fdPredsOfInst (Method _ _ _ theta _) = theta -fdPredsOfInst other = [] -- LitInsts etc +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 (LitInst {}) = [] +fdPredsOfInst (EqInst {}) = [] fdPredsOfInsts :: [Inst] -> [PredType] fdPredsOfInsts insts = concatMap fdPredsOfInst insts -isInheritableInst (Dict _ pred _) = isInheritablePred pred -isInheritableInst (Method _ _ _ theta _) = all isInheritablePred theta -isInheritableInst other = True +isInheritableInst :: Inst -> Bool +isInheritableInst (Dict {tci_pred = pred}) = isInheritablePred pred +isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta +isInheritableInst _ = True +--------------------------------- +-- Get the implicit parameters mentioned by these Insts +-- NB: the results of these functions are insensitive to zonking + ipNamesOfInsts :: [Inst] -> [Name] ipNamesOfInst :: Inst -> [Name] --- Get the implicit parameters mentioned by these Insts --- NB: ?x and %x get different Names ipNamesOfInsts insts = [n | inst <- insts, n <- ipNamesOfInst inst] -ipNamesOfInst (Dict _ (IParam n _) _) = [ipNameName n] -ipNamesOfInst (Method _ _ _ theta _) = [ipNameName n | IParam n _ <- theta] -ipNamesOfInst other = [] +ipNamesOfInst (Dict {tci_pred = IParam n _}) = [ipNameName n] +ipNamesOfInst (Method {tci_theta = theta}) = [ipNameName n | IParam n _ <- theta] +ipNamesOfInst _ = [] +--------------------------------- 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 {tci_ty = ty}) = tyVarsOfType ty +tyVarsOfInst (Dict {tci_pred = pred}) = tyVarsOfPred pred +tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id + -- The id might have free type variables; in the case of + -- locally-overloaded class methods, for example +tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds}) + = (tyVarsOfInsts givens `unionVarSet` tyVarsOfInsts wanteds) + `minusVarSet` mkVarSet tvs + `unionVarSet` unionVarSets (map varTypeTyVars tvs) + -- Remember the free tyvars of a coercion +tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 + +tyVarsOfInsts :: [Inst] -> VarSet tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts +tyVarsOfLIE :: Bag Inst -> VarSet tyVarsOfLIE lie = tyVarsOfInsts (lieToList lie) + + +-------------------------- +instToDictBind :: Inst -> LHsExpr TcId -> TcDictBinds +instToDictBind inst rhs + = unitBag (L (instSpan inst) (VarBind (instToId inst) rhs)) + +addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds +addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs \end{code} Predicates ~~~~~~~~~~ \begin{code} + +isAbstractableInst :: Inst -> Bool +isAbstractableInst inst = isDict inst || isEqInst inst + +isEqInst :: Inst -> Bool +isEqInst (EqInst {}) = True +isEqInst _ = False + isDict :: Inst -> Bool -isDict (Dict _ _ _) = True -isDict other = False +isDict (Dict {}) = True +isDict _ = False isClassDict :: Inst -> Bool -isClassDict (Dict _ pred _) = isClassPred pred -isClassDict other = False +isClassDict (Dict {tci_pred = pred}) = isClassPred pred +isClassDict _ = False isTyVarDict :: Inst -> Bool -isTyVarDict (Dict _ pred _) = isTyVarClassPred pred -isTyVarDict other = False +isTyVarDict (Dict {tci_pred = pred}) = isTyVarClassPred pred +isTyVarDict _ = False isIPDict :: Inst -> Bool -isIPDict (Dict _ pred _) = isIPPred pred -isIPDict other = False +isIPDict (Dict {tci_pred = pred}) = isIPPred pred +isIPDict _ = False + +isImplicInst :: Inst -> Bool +isImplicInst (ImplicInst {}) = True +isImplicInst _ = False isMethod :: Inst -> Bool isMethod (Method {}) = True -isMethod other = False +isMethod _ = False isMethodFor :: TcIdSet -> Inst -> Bool -isMethodFor ids (Method uniq id tys _ loc) = id `elemVarSet` ids -isMethodFor ids inst = False - -isLinearInst :: Inst -> Bool -isLinearInst (Dict _ pred _) = isLinearPred pred -isLinearInst other = False - -- We never build Method Insts that have - -- linear implicit paramters in them. - -- Hence no need to look for Methods - -- See TcExpr.tcId - -linearInstType :: Inst -> TcType -- %x::t --> t -linearInstType (Dict _ (IParam _ ty) _) = ty -\end{code} +isMethodFor ids (Method {tci_oid = id}) = id `elemVarSet` ids +isMethodFor _ _ = False +isMethodOrLit :: Inst -> Bool +isMethodOrLit (Method {}) = True +isMethodOrLit (LitInst {}) = True +isMethodOrLit _ = False +\end{code} %************************************************************************ @@ -199,51 +266,130 @@ linearInstType (Dict _ (IParam _ ty) _) = ty %* * %************************************************************************ -\begin{code} -newDicts :: InstOrigin - -> TcThetaType - -> TcM [Inst] -newDicts orig theta - = getInstLoc orig `thenM` \ loc -> - newDictsAtLoc loc theta +-- newDictBndrs makes a dictionary at a binding site +-- instCall makes a dictionary at an occurrence site +-- and throws it into the LIE -cloneDict :: Inst -> TcM Inst -cloneDict (Dict nm ty loc) = newUnique `thenM` \ uniq -> - returnM (Dict (setNameUnique nm uniq) ty loc) - -newDictAtLoc :: InstLoc -> TcPredType -> TcM Inst -newDictAtLoc inst_loc pred +\begin{code} +---------------- +newDictBndrsO :: InstOrigin -> TcThetaType -> TcM [Inst] +newDictBndrsO orig theta = do { loc <- getInstLoc orig + ; newDictBndrs loc theta } + +newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst] +newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta + +newDictBndr :: InstLoc -> TcPredType -> TcM Inst +newDictBndr inst_loc pred@(EqPred ty1 ty2) + = do { uniq <- newUnique + ; let name = mkPredName uniq inst_loc 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 + = do { uniq <- newUnique + ; let name = mkPredName uniq inst_loc pred + ; return (Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}) } + +---------------- +instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper +-- Instantiate the constraints of a call +-- (instCall o tys theta) +-- (a) Makes fresh dictionaries as necessary for the constraints (theta) +-- (b) Throws these dictionaries into the LIE +-- (c) Returns an HsWrapper ([.] tys dicts) + +instCall orig tys theta + = do { loc <- getInstLoc orig + ; dict_app <- instCallDicts loc theta + ; return (dict_app <.> mkWpTyApps tys) } + +---------------- +instStupidTheta :: InstOrigin -> TcThetaType -> TcM () +-- Similar to instCall, but only emit the constraints in the LIE +-- Used exclusively for the 'stupid theta' of a data constructor +instStupidTheta orig theta + = do { loc <- getInstLoc orig + ; _co <- instCallDicts loc theta -- Discard the coercion + ; return () } + +---------------- +instCallDicts :: InstLoc -> TcThetaType -> TcM HsWrapper +-- Instantiates the TcTheta, puts all constraints thereby generated +-- into the LIE, and returns a HsWrapper to enclose the call site. +-- This is the key place where equality predicates +-- are unleashed into the world +instCallDicts _ [] = return idHsWrapper + +-- instCallDicts loc (EqPred ty1 ty2 : preds) +-- = do { unifyType ty1 ty2 -- For now, we insist that they unify right away +-- -- Later on, when we do associated types, +-- -- unifyType :: Type -> Type -> TcM ([Inst], Coercion) +-- ; (dicts, co_fn) <- instCallDicts loc preds +-- ; return (dicts, co_fn <.> WpTyApp ty1) } +-- -- We use type application to apply the function to the +-- -- coercion; here ty1 *is* the appropriate identity coercion + +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 - ; return (mkDict inst_loc uniq pred) } + ; let name = mkPredName uniq loc pred + dict = Dict {tci_name = name, tci_pred = pred, tci_loc = loc} + ; extendLIE dict + ; co_fn <- instCallDicts loc preds + ; return (co_fn <.> WpApp (instToId dict)) } -newDictsAtLoc :: InstLoc -> TcThetaType -> TcM [Inst] -newDictsAtLoc inst_loc theta - = newUniqueSupply `thenM` \ us -> - returnM (zipWith (mkDict inst_loc) (uniqsFromSupply us) theta) - -mkDict inst_loc uniq pred - = Dict name pred inst_loc - where - name = mkPredName uniq (instLocSrcLoc inst_loc) pred +------------- +cloneDict :: Inst -> TcM Inst +cloneDict dict@(Dict nm _ _) = do { uniq <- newUnique + ; 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 -- at any time, so we used to use the name of the implicit parameter itself -- But with splittable implicit parameters there may be many in --- scope, so we make up a new name. +-- scope, so we make up a new namea. newIPDict :: InstOrigin -> IPName Name -> Type -> TcM (IPName Id, Inst) -newIPDict orig ip_name ty - = getInstLoc orig `thenM` \ inst_loc -> - newUnique `thenM` \ uniq -> +newIPDict orig ip_name ty = do + inst_loc <- getInstLoc orig + uniq <- newUnique let pred = IParam ip_name ty - name = mkPredName uniq (instLocSrcLoc inst_loc) pred - dict = Dict name pred inst_loc - in - returnM (mapIPName (\n -> instToId dict) ip_name, dict) + 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) \end{code} +\begin{code} +mkPredName :: Unique -> InstLoc -> PredType -> Name +mkPredName uniq loc pred_ty + = mkInternalName uniq occ (instLocSpan loc) + where + occ = case pred_ty of + ClassP cls _ -> mkDictOcc (getOccName cls) + IParam ip _ -> getOccName (ipNameName ip) + EqPred ty _ -> mkEqPredCoOcc baseOcc + where + -- 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 -> mkTcOcc "$" + Just (tc, _) -> getOccName tc +\end{code} %************************************************************************ %* * @@ -253,37 +399,24 @@ newIPDict orig ip_name ty \begin{code} -tcInstStupidTheta :: DataCon -> [TcType] -> TcM () --- Instantiate the "stupid theta" of the data con, and throw --- the constraints into the constraint set -tcInstStupidTheta data_con inst_tys - | null stupid_theta - = return () - | otherwise - = do { stupid_dicts <- newDicts (OccurrenceOf (dataConName data_con)) - (substTheta tenv stupid_theta) - ; extendLIEs stupid_dicts } - where - stupid_theta = dataConStupidTheta data_con - tenv = zipTopTvSubst (dataConTyVars data_con) inst_tys - newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId -newMethodFromName origin ty name - = tcLookupId name `thenM` \ id -> +newMethodFromName origin ty name = do + id <- tcLookupId name -- Use tcLookupId not tcLookupGlobalId; the method is almost - -- always a class op, but with -fno-implicit-prelude GHC is + -- always a class op, but with -XNoImplicitPrelude GHC is -- meant to find whatever thing is in scope, and that may -- be an ordinary function. - getInstLoc origin `thenM` \ loc -> - tcInstClassOp loc id [ty] `thenM` \ inst -> - extendLIE inst `thenM_` - returnM (instToId inst) - -newMethodWithGivenTy orig id tys - = getInstLoc orig `thenM` \ loc -> - newMethod loc id tys `thenM` \ inst -> - extendLIE inst `thenM_` - returnM (instToId inst) + loc <- getInstLoc origin + inst <- tcInstClassOp loc id [ty] + extendLIE inst + return (instToId inst) + +newMethodWithGivenTy :: InstOrigin -> Id -> [Type] -> TcRn TcId +newMethodWithGivenTy orig id tys = do + loc <- getInstLoc orig + inst <- newMethod loc id tys + extendLIE inst + return (instToId inst) -------------------------------------------- -- tcInstClassOp, and newMethod do *not* drop the @@ -297,11 +430,10 @@ newMethodWithGivenTy orig id tys -- Hence the call to checkKind -- A worry: is this needed anywhere else? tcInstClassOp :: InstLoc -> Id -> [TcType] -> TcM Inst -tcInstClassOp inst_loc sel_id tys - = let +tcInstClassOp inst_loc sel_id tys = do + let (tyvars, _rho) = tcSplitForAllTys (idType sel_id) - in - zipWithM_ checkKind tyvars tys `thenM_` + zipWithM_ checkKind tyvars tys newMethod inst_loc sel_id tys checkKind :: TyVar -> TcType -> TcM () @@ -309,12 +441,12 @@ checkKind :: TyVar -> TcType -> TcM () checkKind tv ty = do { let ty1 = ty -- ty1 <- zonkTcType ty - ; if typeKind ty1 `isSubKind` tyVarKind tv + ; if typeKind ty1 `isSubKind` Var.tyVarKind tv then return () else pprPanic "checkKind: adding kind constraint" - (vcat [ppr tv <+> ppr (tyVarKind tv), + (vcat [ppr tv <+> ppr (Var.tyVarKind tv), ppr ty <+> ppr ty1 <+> ppr (typeKind ty1)]) } -- do { tv1 <- tcInstTyVar tv @@ -322,51 +454,34 @@ checkKind tv ty --------------------------- -newMethod inst_loc id tys - = newUnique `thenM` \ new_uniq -> +newMethod :: InstLoc -> Id -> [Type] -> TcRn Inst +newMethod inst_loc id tys = do + new_uniq <- newUnique let (theta,tau) = tcSplitPhiTy (applyTys (idType id) tys) meth_id = mkUserLocal (mkMethodOcc (getOccName id)) new_uniq tau loc - inst = Method meth_id id tys theta inst_loc - loc = instLocSrcLoc inst_loc - in - returnM inst + inst = Method {tci_id = meth_id, tci_oid = id, tci_tys = tys, + tci_theta = theta, tci_loc = inst_loc} + loc = instLocSpan inst_loc + + return inst \end{code} \begin{code} -shortCutIntLit :: Integer -> TcType -> Maybe (HsExpr TcId) -shortCutIntLit i ty - | isIntTy ty && inIntRange i -- Short cut for Int - = Just (HsLit (HsInt i)) - | isIntegerTy ty -- Short cut for Integer - = Just (HsLit (HsInteger i ty)) - | otherwise = Nothing - -shortCutFracLit :: Rational -> TcType -> Maybe (HsExpr TcId) -shortCutFracLit f ty - | isFloatTy ty - = Just (mk_lit floatDataCon (HsFloatPrim f)) - | isDoubleTy ty - = Just (mk_lit doubleDataCon (HsDoublePrim f)) - | otherwise = Nothing - where - mk_lit con lit = HsApp (nlHsVar (dataConWrapId con)) (nlHsLit lit) +mkOverLit :: OverLitVal -> TcM HsLit +mkOverLit (HsIntegral i) + = do { integer_ty <- tcMetaTy integerTyConName + ; return (HsInteger i integer_ty) } -mkIntegerLit :: Integer -> TcM (LHsExpr TcId) -mkIntegerLit i - = tcMetaTy integerTyConName `thenM` \ integer_ty -> - getSrcSpanM `thenM` \ span -> - returnM (L span $ HsLit (HsInteger i integer_ty)) +mkOverLit (HsFractional r) + = do { rat_ty <- tcMetaTy rationalTyConName + ; return (HsRat r rat_ty) } -mkRatLit :: Rational -> TcM (LHsExpr TcId) -mkRatLit r - = tcMetaTy rationalTyConName `thenM` \ rat_ty -> - getSrcSpanM `thenM` \ span -> - returnM (L span $ HsLit (HsRat r rat_ty)) +mkOverLit (HsIsString s) = return (HsString s) isHsVar :: HsExpr Name -> Name -> Bool -isHsVar (HsVar f) g = f==g -isHsVar other g = False +isHsVar (HsVar f) g = f == g +isHsVar _ _ = False \end{code} @@ -380,25 +495,42 @@ Zonking makes sure that the instance types are fully zonked. \begin{code} zonkInst :: Inst -> TcM Inst -zonkInst (Dict name pred loc) - = zonkTcPredType pred `thenM` \ new_pred -> - returnM (Dict name new_pred loc) +zonkInst dict@(Dict { tci_pred = pred}) = do + new_pred <- zonkTcPredType pred + return (dict {tci_pred = new_pred}) -zonkInst (Method m id tys theta loc) - = zonkId id `thenM` \ new_id -> +zonkInst meth@(Method {tci_oid = id, tci_tys = tys, tci_theta = theta}) = do + new_id <- zonkId id -- Essential to zonk the id in case it's a local variable -- Can't use zonkIdOcc because the id might itself be -- an InstId, in which case it won't be in scope - zonkTcTypes tys `thenM` \ new_tys -> - zonkTcThetaType theta `thenM` \ new_theta -> - returnM (Method m new_id new_tys new_theta loc) - -zonkInst (LitInst nm lit ty loc) - = zonkTcType ty `thenM` \ new_ty -> - returnM (LitInst nm lit new_ty loc) - -zonkInsts insts = mappM zonkInst insts + new_tys <- zonkTcTypes tys + new_theta <- zonkTcThetaType theta + return (meth { tci_oid = new_id, tci_tys = new_tys, tci_theta = new_theta }) + -- No need to zonk the tci_id + +zonkInst lit@(LitInst {tci_ty = ty}) = do + new_ty <- zonkTcType ty + return (lit {tci_ty = new_ty}) + +zonkInst implic@(ImplicInst {}) + = ASSERT( all isImmutableTyVar (tci_tyvars implic) ) + do { givens' <- zonkInsts (tci_given implic) + ; wanteds' <- zonkInsts (tci_wanted implic) + ; return (implic {tci_given = givens',tci_wanted = wanteds'}) } + +zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2}) + = do { co' <- eitherEqInst eqinst + (\covar -> return (mkWantedCo covar)) + (\co -> liftM mkGivenCo $ zonkTcType co) + ; ty1' <- zonkTcType ty1 + ; ty2' <- zonkTcType ty2 + ; return (eqinst {tci_co = co', tci_left= ty1', tci_right = ty2' }) + } + +zonkInsts :: [Inst] -> TcRn [Inst] +zonkInsts insts = mapM zonkInst insts \end{code} @@ -417,36 +549,53 @@ instance Outputable Inst where pprDictsTheta :: [Inst] -> SDoc -- Print in type-like fashion (Eq a, Show b) -pprDictsTheta dicts = pprTheta (map dictPred dicts) +-- The Inst can be an implication constraint, but not a Method or LitInst +pprDictsTheta insts = parens (sep (punctuate comma (map (ppr . instType) insts))) pprDictsInFull :: [Inst] -> SDoc -- Print in type-like fashion, but with source location pprDictsInFull dicts = vcat (map go dicts) where - go dict = sep [quotes (ppr (dictPred dict)), nest 2 (pprInstLoc (instLoc dict))] + go dict = sep [quotes (ppr (instType dict)), nest 2 (pprInstArising dict)] pprInsts :: [Inst] -> SDoc -- Debugging: print the evidence :: type -pprInsts insts = brackets (interpp'SP insts) +pprInsts insts = brackets (interpp'SP insts) pprInst, pprInstInFull :: Inst -> SDoc -- Debugging: print the evidence :: type -pprInst (LitInst nm lit ty loc) = ppr nm <+> dcolon <+> ppr ty -pprInst (Dict nm pred loc) = ppr nm <+> dcolon <+> pprPred pred - -pprInst m@(Method inst_id id tys theta loc) - = ppr inst_id <+> dcolon <+> - braces (sep [ppr id <+> ptext SLIT("at"), - brackets (sep (map pprParendType tys))]) +pprInst i@(EqInst {tci_left = ty1, tci_right = ty2}) + = eitherEqInst i + (\covar -> text "Wanted" <+> ppr (TyVarTy covar) <+> dcolon <+> ppr (EqPred ty1 ty2)) + (\co -> text "Given" <+> ppr co <+> dcolon <+> ppr (EqPred ty1 ty2)) +pprInst inst = ppr name <> braces (pprUnique (getUnique name)) <+> dcolon + <+> braces (ppr (instType inst) <> implicWantedEqs) + where + name = instName inst + implicWantedEqs + | isImplicInst inst = text " &" <+> + ppr (filter isEqInst (tci_wanted inst)) + | otherwise = empty -pprInstInFull inst - = sep [quotes (pprInst inst), nest 2 (pprInstLoc (instLoc inst))] +pprInstInFull inst@(EqInst {}) = pprInst inst +pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)] tidyInst :: TidyEnv -> Inst -> Inst -tidyInst env (LitInst nm lit ty loc) = LitInst nm lit (tidyType env ty) loc -tidyInst env (Dict nm pred loc) = Dict nm (tidyPred env pred) loc -tidyInst env (Method u id tys theta loc) = Method u id (tidyTypes env tys) theta loc +tidyInst env eq@(EqInst {tci_left = lty, tci_right = rty, tci_co = co}) = + eq { tci_left = tidyType env lty + , tci_right = tidyType env rty + , tci_co = either Left (Right . tidyType env) co + } +tidyInst env lit@(LitInst {tci_ty = ty}) = lit {tci_ty = tidyType env ty} +tidyInst env dict@(Dict {tci_pred = pred}) = dict {tci_pred = tidyPred env pred} +tidyInst env meth@(Method {tci_tys = tys}) = meth {tci_tys = tidyTypes env tys} +tidyInst env implic@(ImplicInst {}) + = implic { tci_tyvars = tvs' + , tci_given = map (tidyInst env') (tci_given implic) + , tci_wanted = map (tidyInst env') (tci_wanted implic) } + where + (env', tvs') = mapAccumL tidyTyVarBndr env (tci_tyvars implic) tidyMoreInsts :: TidyEnv -> [Inst] -> (TidyEnv, [Inst]) -- This function doesn't assume that the tyvars are in scope @@ -496,7 +645,7 @@ addLocalInst home_ie ispec -- We use tcInstSkolType because we don't want to allocate fresh -- *meta* type variables. let dfun = instanceDFunId ispec - ; (tvs', theta', tau') <- tcInstSkolType (InstSkol dfun) (idType dfun) + ; (tvs', theta', tau') <- tcInstSkolType InstSkol (idType dfun) ; let (cls, tys') = tcSplitDFunHead tau' dfun' = setIdType dfun (mkSigmaTy tvs' theta' tau') ispec' = setInstanceDFunId ispec dfun' @@ -514,7 +663,7 @@ addLocalInst home_ie ispec -- Check for duplicate instance decls ; let { (matches, _) = lookupInstEnv inst_envs cls tys' ; dup_ispecs = [ dup_ispec - | (_, dup_ispec) <- matches + | (dup_ispec, _) <- matches , let (_,_,_,dup_tys) = instanceHead dup_ispec , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] } -- Find memebers of the match list which ispec itself matches. @@ -529,29 +678,33 @@ addLocalInst home_ie ispec getOverlapFlag :: TcM OverlapFlag getOverlapFlag = do { dflags <- getDOpts - ; let overlap_ok = dopt Opt_AllowOverlappingInstances dflags - incoherent_ok = dopt Opt_AllowIncoherentInstances dflags + ; let overlap_ok = dopt Opt_OverlappingInstances dflags + incoherent_ok = dopt Opt_IncoherentInstances dflags overlap_flag | incoherent_ok = Incoherent | overlap_ok = OverlapOk | otherwise = NoOverlap ; return overlap_flag } +traceDFuns :: [Instance] -> TcRn () traceDFuns ispecs = traceTc (hang (text "Adding instances:") 2 (vcat (map pp ispecs))) where pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec -- Print the dfun name itself too +funDepErr :: Instance -> [Instance] -> TcRn () funDepErr ispec ispecs = addDictLoc ispec $ - addErr (hang (ptext SLIT("Functional dependencies conflict between instance declarations:")) + addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:")) 2 (pprInstances (ispec:ispecs))) +dupInstErr :: Instance -> Instance -> TcRn () dupInstErr ispec dup_ispec = addDictLoc ispec $ - addErr (hang (ptext SLIT("Duplicate instance declarations:")) + addErr (hang (ptext (sLit "Duplicate instance declarations:")) 2 (pprInstances [ispec, dup_ispec])) +addDictLoc :: Instance -> TcRn a -> TcRn a addDictLoc ispec thing_inside = setSrcSpan (mkSrcSpan loc loc) thing_inside where @@ -568,111 +721,96 @@ addDictLoc ispec thing_inside \begin{code} data LookupInstResult = NoInstance - | SimpleInst (LHsExpr TcId) -- Just a variable, type application, or literal - | GenInst [Inst] (LHsExpr TcId) -- The expression and its needed insts + | GenInst [Inst] (LHsExpr TcId) -- The expression and its needed insts + +lookupSimpleInst :: Inst -> TcM LookupInstResult +-- This is "simple" in that it returns NoInstance for implication constraints -lookupInst :: Inst -> TcM LookupInstResult -- It's important that lookupInst does not put any new stuff into -- the LIE. Instead, any Insts needed by the lookup are returned in -- the LookupInstResult, where they can be further processed by tcSimplify +lookupSimpleInst (EqInst {}) = return NoInstance --- Methods +--------------------- Implications ------------------------ +lookupSimpleInst (ImplicInst {}) = return NoInstance -lookupInst inst@(Method _ id tys theta loc) - = newDictsAtLoc loc theta `thenM` \ dicts -> - returnM (GenInst dicts (mkHsDictApp (mkHsTyApp (L span (HsVar id)) tys) (map instToId dicts))) +--------------------- Methods ------------------------ +lookupSimpleInst (Method {tci_oid = id, tci_tys = tys, tci_theta = theta, tci_loc = loc}) + = do { (dict_app, dicts) <- getLIE $ instCallDicts loc theta + ; let co_fn = dict_app <.> mkWpTyApps tys + ; return (GenInst dicts (L span $ HsWrap co_fn (HsVar id))) } where - span = instLocSrcSpan loc - --- Literals + span = instLocSpan loc +--------------------- Literals ------------------------ -- Look for short cuts first: if the literal is *definitely* a -- int, integer, float or a double, generate the real thing here. -- This is essential (see nofib/spectral/nucleic). -- [Same shortcut as in newOverloadedLit, but we -- may have done some unification by now] -lookupInst inst@(LitInst _nm (HsIntegral i from_integer_name) ty loc) - | Just expr <- shortCutIntLit i ty - = returnM (GenInst [] (noLoc expr)) -- GenInst, not SimpleInst, because - -- expr may be a constructor application - | otherwise - = ASSERT( from_integer_name `isHsVar` fromIntegerName ) -- A LitInst invariant - tcLookupId fromIntegerName `thenM` \ from_integer -> - tcInstClassOp loc from_integer [ty] `thenM` \ method_inst -> - mkIntegerLit i `thenM` \ integer_lit -> - returnM (GenInst [method_inst] - (mkHsApp (L (instLocSrcSpan loc) - (HsVar (instToId method_inst))) integer_lit)) - -lookupInst inst@(LitInst _nm (HsFractional f from_rat_name) ty loc) - | Just expr <- shortCutFracLit f ty - = returnM (GenInst [] (noLoc expr)) +lookupSimpleInst (LitInst { tci_lit = lit@OverLit { ol_val = lit_val + , ol_rebindable = rebindable } + , tci_ty = ty, tci_loc = iloc}) + | debugIsOn && rebindable = panic "lookupSimpleInst" -- A LitInst invariant + | Just witness <- shortCutLit lit_val ty + = do { let lit' = lit { ol_witness = witness, ol_type = ty } + ; return (GenInst [] (L loc (HsOverLit lit'))) } | otherwise - = ASSERT( from_rat_name `isHsVar` fromRationalName ) -- A LitInst invariant - tcLookupId fromRationalName `thenM` \ from_rational -> - tcInstClassOp loc from_rational [ty] `thenM` \ method_inst -> - mkRatLit f `thenM` \ rat_lit -> - returnM (GenInst [method_inst] (mkHsApp (L (instLocSrcSpan loc) - (HsVar (instToId method_inst))) rat_lit)) - --- Dictionaries -lookupInst (Dict _ pred loc) + = do { hs_lit <- mkOverLit lit_val + ; from_thing <- tcLookupId (hsOverLitName lit_val) + -- Not rebindable, so hsOverLitName is the right thing + ; method_inst <- tcInstClassOp iloc from_thing [ty] + ; let witness = HsApp (L loc (HsVar (instToId method_inst))) + (L loc (HsLit hs_lit)) + lit' = lit { ol_witness = witness, ol_type = ty } + ; return (GenInst [method_inst] (L loc (HsOverLit lit'))) } + where + loc = instLocSpan iloc + +--------------------- Dictionaries ------------------------ +lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc}) = do { mb_result <- lookupPred pred ; case mb_result of { Nothing -> return NoInstance ; - Just (tenv, dfun_id) -> do - - -- tenv is a substitution that instantiates the dfun_id - -- to match the requested result type. - -- - -- We ASSUME that the dfun is quantified over the very same tyvars - -- that are bound by the tenv. - -- - -- However, the dfun - -- might have some tyvars that *only* appear in arguments - -- dfun :: forall a b. C a b, Ord b => D [a] - -- We instantiate b to a flexi type variable -- it'll presumably - -- become fixed later via functional dependencies + Just (dfun_id, mb_inst_tys) -> do + { use_stage <- getStage - ; checkWellStaged (ptext SLIT("instance for") <+> quotes (ppr pred)) + ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred)) (topIdLvl dfun_id) use_stage -- It's possible that not all the tyvars are in -- the substitution, tenv. For example: -- instance C X a => D X where ... -- (presumably there's a functional dependency in class C) - -- Hence the open_tvs to instantiate any un-substituted tyvars. - ; let (tyvars, rho) = tcSplitForAllTys (idType dfun_id) - open_tvs = filter (`notElemTvSubst` tenv) tyvars - ; open_tvs' <- mappM tcInstTyVar open_tvs + -- Hence mb_inst_tys :: Either TyVar TcType + + ; let inst_tv (Left tv) = do { tv' <- tcInstTyVar tv; return (mkTyVarTy tv') } + inst_tv (Right ty) = return ty + ; tys <- mapM inst_tv mb_inst_tys ; let - tenv' = extendTvSubstList tenv open_tvs (mkTyVarTys open_tvs') - -- Since the open_tvs' are freshly made, they cannot possibly be captured by - -- any nested for-alls in rho. So the in-scope set is unchanged - dfun_rho = substTy tenv' rho - (theta, _) = tcSplitPhiTy dfun_rho - ty_app = mkHsTyApp (L (instLocSrcSpan loc) (HsVar dfun_id)) - (map (substTyVar tenv') tyvars) + (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys) + src_loc = instLocSpan loc + dfun = HsVar dfun_id ; if null theta then - returnM (SimpleInst ty_app) + return (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun)) else do - { dicts <- newDictsAtLoc loc theta - ; let rhs = mkHsDictApp ty_app (map instToId dicts) - ; returnM (GenInst dicts rhs) + { (dict_app, dicts) <- getLIE $ instCallDicts loc theta -- !!! + ; let co_fn = dict_app <.> mkWpTyApps tys + ; return (GenInst dicts (L src_loc $ HsWrap co_fn dfun)) }}}} --------------- -lookupPred :: TcPredType -> TcM (Maybe (TvSubst, DFunId)) +lookupPred :: TcPredType -> TcM (Maybe (DFunId, [Either TyVar TcType])) -- Look up a class constraint in the instance environment lookupPred pred@(ClassP clas tys) = do { eps <- getEps ; tcg_env <- getGblEnv ; let inst_envs = (eps_inst_env eps, tcg_inst_env tcg_env) ; case lookupInstEnv inst_envs clas tys of { - ([(tenv, ispec)], []) + ([(ispec, inst_tys)], []) -> do { let dfun_id = is_dfun ispec ; traceTc (text "lookupInst success" <+> vcat [text "dict" <+> ppr pred, @@ -680,7 +818,7 @@ lookupPred pred@(ClassP clas tys) <+> ppr (idType dfun_id) ]) -- Record that this dfun is needed ; record_dfun_usage dfun_id - ; return (Just (tenv, dfun_id)) } ; + ; return (Just (dfun_id, inst_tys)) } ; (matches, unifs) -> do { traceTc (text "lookupInst fail" <+> @@ -695,8 +833,10 @@ lookupPred pred@(ClassP clas tys) ; return Nothing } }} -lookupPred ip_pred = return Nothing +lookupPred (IParam {}) = return Nothing -- Implicit parameters +lookupPred (EqPred {}) = panic "lookupPred EqPred" +record_dfun_usage :: Id -> TcRn () record_dfun_usage dfun_id = do { hsc_env <- getTopEnv ; let dfun_name = idName dfun_id @@ -724,7 +864,7 @@ tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv; %* * %************************************************************************ -Suppose we are doing the -fno-implicit-prelude thing, and we encounter +Suppose we are doing the -XNoImplicitPrelude thing, and we encounter a do-expression. We have to find (>>) in the current environment, which is done by the rename. Then we have to check that it has the same type as Control.Monad.(>>). Or, more precisely, a compatible type. One 'customer' had @@ -757,34 +897,208 @@ tcSyntaxName :: InstOrigin tcSyntaxName orig ty (std_nm, HsVar user_nm) | std_nm == user_nm - = newMethodFromName orig ty std_nm `thenM` \ id -> - returnM (std_nm, HsVar id) + = do id <- newMethodFromName orig ty std_nm + return (std_nm, HsVar id) -tcSyntaxName orig ty (std_nm, user_nm_expr) - = tcLookupId std_nm `thenM` \ std_id -> +tcSyntaxName orig ty (std_nm, user_nm_expr) = do + std_id <- tcLookupId std_nm let -- C.f. newMethodAtLoc ([tv], _, tau) = tcSplitSigmaTy (idType std_id) sigma1 = substTyWith [tv] [ty] tau -- Actually, the "tau-type" might be a sigma-type in the -- case of locally-polymorphic methods. - in - addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ + + addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do -- Check that the user-supplied thing has the -- same type as the standard one. -- Tiresome jiggling because tcCheckSigma takes a located expression - getSrcSpanM `thenM` \ span -> - tcPolyExpr (L span user_nm_expr) sigma1 `thenM` \ expr -> - returnM (std_nm, unLoc expr) - -syntaxNameCtxt name orig ty tidy_env - = getInstLoc orig `thenM` \ inst_loc -> + span <- getSrcSpanM + expr <- tcPolyExpr (L span user_nm_expr) sigma1 + return (std_nm, unLoc expr) + +syntaxNameCtxt :: HsExpr Name -> InstOrigin -> Type -> TidyEnv + -> TcRn (TidyEnv, SDoc) +syntaxNameCtxt name orig ty tidy_env = do + inst_loc <- getInstLoc orig let - msg = vcat [ptext SLIT("When checking that") <+> quotes (ppr name) <+> - ptext SLIT("(needed by a syntactic construct)"), - nest 2 (ptext SLIT("has the required type:") <+> ppr (tidyType tidy_env ty)), - nest 2 (pprInstLoc inst_loc)] - in - returnM (tidy_env, msg) + msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+> + ptext (sLit "(needed by a syntactic construct)"), + nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)), + nest 2 (ptext (sLit "arising from") <+> pprInstLoc inst_loc)] + + return (tidy_env, msg) +\end{code} + +%************************************************************************ +%* * + EqInsts +%* * +%************************************************************************ + +Operations on EqInstCo. + +\begin{code} +mkGivenCo :: Coercion -> EqInstCo +mkGivenCo = Right + +mkWantedCo :: TcTyVar -> EqInstCo +mkWantedCo = Left + +isWantedCo :: EqInstCo -> Bool +isWantedCo (Left _) = True +isWantedCo _ = False + +fromGivenCo :: EqInstCo -> Coercion +fromGivenCo (Right co) = co +fromGivenCo _ = panic "fromGivenCo: not a wanted coercion" + +fromWantedCo :: String -> EqInstCo -> TcTyVar +fromWantedCo _ (Left covar) = covar +fromWantedCo msg _ = + panic ("fromWantedCo: not a wanted coercion: " ++ msg) + +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: + + 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) +\end{code} + +Operations on entire EqInst. + +\begin{code} +eitherEqInst :: Inst -- given or wanted EqInst + -> (TcTyVar -> a) -- result if wanted + -> (Coercion -> a) -- result if given + -> a +eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven + = case either_co of + Left covar -> withWanted covar + Right co -> withGiven co +eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i) + +mkEqInsts :: [PredType] -> [EqInstCo] -> TcM [Inst] +mkEqInsts preds cos = zipWithM mkEqInst preds cos + +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 + } + ; return inst + } + where + mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span +mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred) + +mkWantedEqInst :: PredType -> TcM Inst +mkWantedEqInst pred@(EqPred ty1 ty2) + = do { cotv <- newMetaCoVar ty1 ty2 + ; mkEqInst pred (Left cotv) + } +mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred) + +-- 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}) + = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2) + + -- fill the coercion hole + ; let cotv = fromWantedCo "writeWantedCoercion" $ tci_co wanted + ; writeMetaTyVar cotv (TyVarTy var) + + -- set the new coercion + ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var } + ; return given + } + +finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i) + +eqInstType :: Inst -> TcType +eqInstType inst = eitherEqInst inst mkTyVarTy id + +eqInstCoercion :: Inst -> EqInstCo +eqInstCoercion = tci_co + +eqInstTys :: Inst -> (TcType, TcType) +eqInstTys inst = (tci_left inst, tci_right inst) + +updateEqInstCoercion :: (EqInstCo -> EqInstCo) -> Inst -> Inst +updateEqInstCoercion f inst = inst {tci_co = f $ tci_co inst} \end{code}