\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,
tcInstClassOp,
- tcSyntaxName, isHsVar,
+ tcSyntaxName,
- tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE,
- ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
- getDictClassTys, dictPred,
+ tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, tcTyVarsOfInst,
+ tcTyVarsOfInsts, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst,
+ fdPredsOfInsts, 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 MkCore ( mkBigCoreTupTy )
+import TyCon
import Type
import TypeRep
import Class
import Coercion
import HscTypes
import CoreFVs
-import DataCon
import Id
import Name
import NameSet
-import Literal
import Var ( Var, TyVar )
import qualified Var
import VarEnv
import VarSet
-import TysWiredIn
import PrelNames
import BasicTypes
import SrcLoc
import Unique
import Outputable
import Data.List
-import TypeRep
-import Class
import Control.Monad
\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
in
mkForAllTys tvs $
mkPhiTy (map dictPred givens) $
- if isSingleton dict_wanteds then
- instType (head dict_wanteds)
- else
- mkTupleTy Boxed (length dict_wanteds) (map instType dict_wanteds)
+ mkBigCoreTupTy (map instType dict_wanteds)
dictPred :: Inst -> TcPredType
dictPred (Dict {tci_pred = pred}) = pred
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
ipNamesOfInst _ = []
---------------------------------
-tyVarsOfInst :: Inst -> TcTyVarSet
+
+-- |All free type variables (not including the coercion variables of
+-- equalities)
+--
+tyVarsOfInst :: Inst -> TyVarSet
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})
+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
+tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2})
+ = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+
+-- |All free meta type variables *including* the coercion variables of
+-- equalities
+--
+tcTyVarsOfInst :: Inst -> TyVarSet
+tcTyVarsOfInst (LitInst {tci_ty = ty}) = tcTyVarsOfType ty
+tcTyVarsOfInst (Dict {tci_pred = pred}) = tcTyVarsOfPred pred
+tcTyVarsOfInst (Method {tci_oid = id, tci_tys = tys})
+ = tcTyVarsOfTypes tys `unionVarSet` varTypeTcTyVars id
+ -- The id might have free type variables; in the case of
+ -- locally-overloaded class methods, for example
+tcTyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens,
+ tci_wanted = wanteds})
+ = (tcTyVarsOfInsts givens `unionVarSet` tcTyVarsOfInsts wanteds)
+ `minusVarSet` mkVarSet tvs
+ `unionVarSet` unionVarSets (map varTypeTcTyVars tvs)
+ -- Remember the free tyvars of a coercion
+tcTyVarsOfInst (EqInst {tci_co = co, tci_left = ty1, tci_right = ty2})
+ = either unitVarSet tcTyVarsOfType co `unionVarSet` -- include covars
+ tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
-tyVarsOfInsts :: [Inst] -> VarSet
+tyVarsOfInsts :: [Inst] -> TyVarSet
tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
-tyVarsOfLIE :: Bag Inst -> VarSet
+
+tcTyVarsOfInsts :: [Inst] -> TcTyVarSet
+tcTyVarsOfInsts insts = foldr (unionVarSet . tcTyVarsOfInst) emptyVarSet insts
+
+tyVarsOfLIE :: Bag Inst -> TyVarSet
tyVarsOfLIE lie = tyVarsOfInsts (lieToList lie)
--------------------------
instToDictBind :: Inst -> LHsExpr TcId -> TcDictBinds
instToDictBind inst rhs
- = unitBag (L (instSpan inst) (VarBind (instToId inst) rhs))
+ = unitBag (L (instSpan inst) (VarBind { var_id = instToId inst
+ , var_rhs = rhs
+ , var_inline = False }))
addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds
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}
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.
loc <- getInstLoc origin
; return (HsRat r rat_ty) }
mkOverLit (HsIsString s) = return (HsString s)
-
-isHsVar :: HsExpr Name -> Name -> Bool
-isHsVar (HsVar f) g = f == g
-isHsVar _ _ = False
\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]
{ use_stage <- getStage
; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
- (topIdLvl dfun_id) use_stage
+ (topIdLvl dfun_id) (thLevel use_stage)
-- It's possible that not all the tyvars are in
-- the substitution, tenv. For example:
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
%* *
%************************************************************************
-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
%* *
%************************************************************************
+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
+ = bindMetaTyVar 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
+ ; bindMetaTyVar 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
+ ; bindMetaTyVar 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
+ ; bindMetaTyVar 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
+ ; bindMetaTyVar 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
+ ; bindMetaTyVar 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
+ ; bindMetaTyVar 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_ei") 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}