+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}
+-- For debugging, make sure the cotv of a wanted is not filled.
+--
+isValidWantedEqInst :: Inst -> TcM Bool
+isValidWantedEqInst (EqInst {tci_co = Left cotv})
+ = liftM not $ isFilledMetaTyVar cotv
+isValidWantedEqInst _ = return True