%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%

The @Inst@ type: dictionaries or method instances

\begin{code}
module 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, 

	tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, tcTyVarsOfInst,
	tcTyVarsOfInsts, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst,
	fdPredsOfInsts, growInstsTyVars, getDictClassTys, dictPred,

	lookupSimpleInst, LookupInstResult(..), 
	tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,

	isAbstractableInst, isEqInst,
	isDict, isClassDict, isMethod, isImplicInst,
	isIPDict, isInheritableInst, isMethodOrLit,
	isTyVarDict, isMethodFor, 

	zonkInst, zonkInsts,
	instToId, instToVar, instType, instName, instToDictBind,
	addInstToDictBind,

	InstOrigin(..), InstLoc, pprInstLoc,

	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 {-# SOURCE #-}	TcExpr( tcPolyExpr )
import {-# SOURCE #-}	TcUnify( boxyUnify {- , unifyType -} )

import FastString
import HsSyn
import TcHsSyn
import TcRnMonad
import TcEnv
import InstEnv
import FunDeps
import TcMType
import TcType
import MkCore ( mkBigCoreTupTy )
import TyCon
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 (EqInst {tci_name = name}) = name
instName inst = Var.varName (instToVar inst)

instToId :: Inst -> TcId
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 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
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
-- a constraint (C a b) might have a superclass with FDs
-- 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 :: Inst -> [TcPredType]
fdPredsOfInst (Dict {tci_pred = pred}) 	     = [pred]
fdPredsOfInst (Method {tci_theta = theta})   = theta
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
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]
ipNamesOfInsts insts = [n | inst <- insts, n <- ipNamesOfInst inst]

ipNamesOfInst (Dict {tci_pred = IParam n _}) = [ipNameName n]
ipNamesOfInst (Method {tci_theta = theta})   = [ipNameName n | IParam n _ <- theta]
ipNamesOfInst _                              = []

---------------------------------

-- |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})
  = (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

-- |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] -> TyVarSet
tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts

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))

addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds
addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs
\end{code}

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
isAbstractableInst inst = isDict inst || isEqInst inst

isEqInst :: Inst -> Bool
isEqInst (EqInst {}) = True
isEqInst _           = False

isDict :: Inst -> Bool
isDict (Dict {}) = True
isDict _         = False

isClassDict :: Inst -> Bool
isClassDict (Dict {tci_pred = pred}) = isClassPred pred
isClassDict _                        = False

isTyVarDict :: Inst -> Bool
isTyVarDict (Dict {tci_pred = pred}) = isTyVarClassPred pred
isTyVarDict _                        = False

isIPDict :: Inst -> Bool
isIPDict (Dict {tci_pred = pred}) = isIPPred pred
isIPDict _                        = False

isImplicInst :: Inst -> Bool
isImplicInst (ImplicInst {}) = True
isImplicInst _               = False

isMethod :: Inst -> Bool
isMethod (Method {}) = True
isMethod _           = False

isMethodFor :: TcIdSet -> Inst -> Bool
isMethodFor ids (Method {tci_oid = id}) = id `elemVarSet` ids
isMethodFor _   _                       = False

isMethodOrLit :: Inst -> Bool
isMethodOrLit (Method {})  = True
isMethodOrLit (LitInst {}) = True
isMethodOrLit _            = False
\end{code}


%************************************************************************
%*									*
\subsection{Building dictionaries}
%*									*
%************************************************************************

-- newDictBndrs makes a dictionary at a binding site
-- instCall makes a dictionary at an occurrence site
--	and throws it into the LIE

\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
-- 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    = 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}) }

----------------
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
	; let co = fromCoI coi ty1
	; co_fn <- instCallDicts loc preds
	; return (co_fn <.> WpTyApp co) }

instCallDicts loc (pred : preds)
  = 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
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 namea.
newIPDict :: InstOrigin -> IPName Name -> Type 
	  -> TcM (IPName Id, Inst)
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}


\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}

%************************************************************************
%*									*
\subsection{Building methods (calls of overloaded functions)}
%*									*
%************************************************************************


\begin{code}
newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
newMethodFromName origin ty name = do
    id <- tcLookupId name
	-- Use tcLookupId not tcLookupGlobalId; the method is almost
	-- 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
    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 
-- Inst into the LIE; they just returns the Inst
-- This is important because they are used by TcSimplify
-- to simplify Insts

-- NB: the kind of the type variable to be instantiated
--     might be a sub-kind of the type to which it is applied,
--     notably when the latter is a type variable of kind ??
--     Hence the call to checkKind
-- A worry: is this needed anywhere else?
tcInstClassOp :: InstLoc -> Id -> [TcType] -> TcM Inst
tcInstClassOp inst_loc sel_id tys = do
    let
	(tyvars, _rho) = tcSplitForAllTys (idType sel_id)
    zipWithM_ checkKind tyvars tys
    newMethod inst_loc sel_id tys

checkKind :: TyVar -> TcType -> TcM ()
-- Ensure that the type has a sub-kind of the tyvar
checkKind tv ty
  = do	{ let ty1 = ty 
		-- ty1 <- zonkTcType ty
	; if typeKind ty1 `isSubKind` Var.tyVarKind tv
	  then return ()
	  else 

    pprPanic "checkKind: adding kind constraint" 
	     (vcat [ppr tv <+> ppr (Var.tyVarKind tv), 
	            ppr ty <+> ppr ty1 <+> ppr (typeKind ty1)])
	}
--    do	{ tv1 <- tcInstTyVar tv
--	; unifyType ty1 (mkTyVarTy tv1) } }


---------------------------
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 {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}
mkOverLit :: OverLitVal -> TcM HsLit
mkOverLit (HsIntegral i) 
  = do	{ integer_ty <- tcMetaTy integerTyConName
	; return (HsInteger i integer_ty) }

mkOverLit (HsFractional r)
  = do	{ rat_ty <- tcMetaTy rationalTyConName
	; return (HsRat r rat_ty) }

mkOverLit (HsIsString s) = return (HsString s)
\end{code}


%************************************************************************
%*									*
\subsection{Zonking}
%*									*
%************************************************************************

Zonking makes sure that the instance types are fully zonked.

\begin{code}
zonkInst :: Inst -> TcM Inst
zonkInst dict@(Dict {tci_pred = pred}) = do
    new_pred <- zonkTcPredType pred
    return (dict {tci_pred = new_pred})

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

    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}


%************************************************************************
%*									*
\subsection{Printing}
%*									*
%************************************************************************

ToDo: improve these pretty-printing things.  The ``origin'' is really only
relevant in error messages.

\begin{code}
instance Outputable Inst where
    ppr inst = pprInst inst

pprDictsTheta :: [Inst] -> SDoc
-- Print in type-like fashion (Eq a, Show b)
-- 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 (instType dict)), nest 2 (pprInstArising dict)]

pprInsts :: [Inst] -> SDoc
-- Debugging: print the evidence :: type
pprInsts insts = brackets (interpp'SP insts)

pprInst, pprInstInFull :: Inst -> SDoc
-- Debugging: print the evidence :: type
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@(EqInst {}) = pprInst inst
pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]

tidyInst :: TidyEnv -> Inst -> Inst
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
-- so it works like tidyOpenType, returning a TidyEnv
tidyMoreInsts env insts
  = (env', map (tidyInst env') insts)
  where
    env' = tidyFreeTyVars env (tyVarsOfInsts insts)

tidyInsts :: [Inst] -> (TidyEnv, [Inst])
tidyInsts insts = tidyMoreInsts emptyTidyEnv insts

showLIE :: SDoc -> TcM ()	-- Debugging
showLIE str
  = do { lie_var <- getLIEVar ;
	 lie <- readMutVar lie_var ;
	 traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) }
\end{code}


%************************************************************************
%*									*
	Extending the instance environment
%*									*
%************************************************************************

\begin{code}
tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
  -- Add new locally-defined instances
tcExtendLocalInstEnv dfuns thing_inside
 = do { traceDFuns dfuns
      ; env <- getGblEnv
      ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
      ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
			 tcg_inst_env = inst_env' }
      ; setGblEnv env' thing_inside }

addLocalInst :: InstEnv -> Instance -> TcM InstEnv
-- Check that the proposed new instance is OK, 
-- and then add it to the home inst env
addLocalInst home_ie ispec
  = do	{ 	-- Instantiate the dfun type so that we extend the instance
		-- envt with completely fresh template variables
		-- This is important because the template variables must
		-- not overlap with anything in the things being looked up
		-- (since we do unification).  
		-- We use tcInstSkolType because we don't want to allocate fresh
		--  *meta* type variables.  
	  let dfun = instanceDFunId ispec
	; (tvs', theta', tau') <- tcInstSkolType InstSkol (idType dfun)
	; let	(cls, tys') = tcSplitDFunHead tau'
		dfun' 	    = setIdType dfun (mkSigmaTy tvs' theta' tau')	    
	  	ispec'      = setInstanceDFunId ispec dfun'

		-- Load imported instances, so that we report
		-- duplicates correctly
	; eps <- getEps
	; let inst_envs = (eps_inst_env eps, home_ie)

		-- Check functional dependencies
	; case checkFunDeps inst_envs ispec' of
		Just specs -> funDepErr ispec' specs
		Nothing    -> return ()

		-- Check for duplicate instance decls
	; let { (matches, _) = lookupInstEnv inst_envs cls tys'
	      ;	dup_ispecs = [ dup_ispec 
			     | (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.
		-- If the match is 2-way, it's a duplicate
	; case dup_ispecs of
	    dup_ispec : _ -> dupInstErr ispec' dup_ispec
	    []            -> return ()

		-- OK, now extend the envt
	; return (extendInstEnv home_ie ispec') }

getOverlapFlag :: TcM OverlapFlag
getOverlapFlag 
  = do 	{ dflags <- getDOpts
	; 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:"))
	       2 (pprInstances (ispec:ispecs)))
dupInstErr :: Instance -> Instance -> TcRn ()
dupInstErr ispec dup_ispec
  = addDictLoc ispec $
    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
   loc = getSrcLoc ispec
\end{code}
    

%************************************************************************
%*									*
\subsection{Looking up Insts}
%*									*
%************************************************************************

\begin{code}
data LookupInstResult
  = NoInstance
  | 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

-- 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

--------------------- Implications ------------------------
lookupSimpleInst (ImplicInst {}) = return NoInstance

--------------------- 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 = 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] 		

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
  = 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 (dfun_id, mb_inst_tys) -> do

    { use_stage <- getStage
    ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
    		      (topIdLvl dfun_id) (thLevel 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 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
    	(theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
	src_loc	   = instLocSpan loc
	dfun	   = HsVar dfun_id
    ; if null theta then
        return (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
      else do
    { (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 (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 {
	    ([(ispec, inst_tys)], []) 
		-> do	{ let dfun_id = is_dfun ispec
			; traceTc (text "lookupInst success" <+> 
				   vcat [text "dict" <+> ppr pred, 
				         text "witness" <+> ppr dfun_id
					 <+> ppr (idType dfun_id) ])
				-- Record that this dfun is needed
			; record_dfun_usage dfun_id
			; return (Just (dfun_id, inst_tys)) } ;

     	    (matches, unifs)
		-> do	{ traceTc (text "lookupInst fail" <+> 
				   vcat [text "dict" <+> ppr pred,
				   	 text "matches" <+> ppr matches,
				   	 text "unifs" <+> ppr unifs])
		-- In the case of overlap (multiple matches) we report
		-- NoInstance here.  That has the effect of making the 
		-- context-simplifier return the dict as an irreducible one.
		-- Then it'll be given to addNoInstanceErrs, which will do another
		-- lookupInstEnv to get the detailed info about what went wrong.
			; 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
	       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
	   else do { tcg_env <- getGblEnv
	  	   ; updMutVar (tcg_inst_uses tcg_env)
			       (`addOneToNameSet` idName dfun_id) }}


tcGetInstEnvs :: TcM (InstEnv, InstEnv)
-- Gets both the external-package inst-env
-- and the home-pkg inst env (includes module being compiled)
tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
		     return (eps_inst_env eps, tcg_inst_env env) }
\end{code}



%************************************************************************
%*									*
		Re-mappable syntax
%*									*
%************************************************************************

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
this:

  (>>) :: HB m n mn => m a -> n b -> mn b

So the idea is to generate a local binding for (>>), thus:

	let then72 :: forall a b. m a -> m b -> m b
	    then72 = ...something involving the user's (>>)...
	in
	...the do-expression...

Now the do-expression can proceed using then72, which has exactly
the expected type.

In fact tcSyntaxName just generates the RHS for then72, because we only
want an actual binding in the do-expression case. For literals, we can 
just use the expression inline.

\begin{code}
tcSyntaxName :: InstOrigin
	     -> TcType			-- Type to instantiate it at
	     -> (Name, HsExpr Name)	-- (Standard name, user name)
	     -> TcM (Name, HsExpr TcId)	-- (Standard name, suitable expression)
--	*** NOW USED ONLY FOR CmdTop (sigh) ***
-- NB: tcSyntaxName calls tcExpr, and hence can do unification.
-- So we do not call it from lookupInst, which is called from tcSimplify

tcSyntaxName orig ty (std_nm, HsVar user_nm)
  | std_nm == user_nm
  = do id <- newMethodFromName orig ty std_nm
       return (std_nm, HsVar 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.

    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
     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 (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

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
  = 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
	     -> (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)

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_ei") 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 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
       }

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)
\end{code}