+ 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
+%* *
+%************************************************************************
+
+\begin{code}
+mkGivenCo :: Coercion -> Either TcTyVar Coercion
+mkGivenCo = Right
+
+mkWantedCo :: TcTyVar -> Either TcTyVar Coercion
+mkWantedCo = Left
+
+fromGivenCo :: Either TcTyVar Coercion -> Coercion
+fromGivenCo (Right co) = co
+fromGivenCo _ = panic "fromGivenCo: not a wanted coercion"
+
+fromWantedCo :: String -> Either TcTyVar Coercion -> TcTyVar
+fromWantedCo _ (Left covar) = covar
+fromWantedCo msg _ = panic ("fromWantedCo: not a wanted coercion: " ++ msg)
+
+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
+
+mkEqInsts :: [PredType] -> [Either TcTyVar Coercion] -> TcM [Inst]
+mkEqInsts preds cos = zipWithM mkEqInst preds cos
+
+mkEqInst :: PredType -> Either TcTyVar Coercion -> 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
+
+mkWantedEqInst :: PredType -> TcM Inst
+mkWantedEqInst pred@(EqPred ty1 ty2)
+ = do { cotv <- newMetaCoVar ty1 ty2
+ ; mkEqInst pred (Left cotv)
+ }
+
+-- 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
+ }
+
+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
+ }
+
+eqInstType :: Inst -> TcType
+eqInstType inst = eitherEqInst inst mkTyVarTy id
+
+eqInstCoercion :: Inst -> Either TcTyVar Coercion
+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}