+----------------
+instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM ExprCoFn
+-- 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) Eeturns an ExprCoFn ([.] tys dicts)
+
+instCall orig tys theta
+ = do { loc <- getInstLoc orig
+ ; (dicts, dict_app) <- instCallDicts loc theta
+ ; extendLIEs dicts
+ ; return (dict_app <.> mkCoTyApps 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
+ ; (dicts, _) <- instCallDicts loc theta
+ ; extendLIEs dicts }
+
+----------------
+instCallDicts :: InstLoc -> TcThetaType -> TcM ([Inst], ExprCoFn)
+-- This is the key place where equality predicates
+-- are unleashed into the world
+instCallDicts loc [] = return ([], idCoercion)
+
+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 <.> CoTyApp ty1) }
+ -- We use type application to apply the function to the
+ -- coercion; here ty1 *is* the appropriate identity coercion
+
+instCallDicts loc (pred : preds)
+ = do { uniq <- newUnique
+ ; let name = mkPredName uniq (instLocSrcLoc loc) pred
+ dict = Dict name pred loc
+ ; (dicts, co_fn) <- instCallDicts loc preds
+ ; return (dict:dicts, co_fn <.> CoApp (instToId dict)) }
+
+-------------
+cloneDict :: Inst -> TcM Inst -- Only used for linear implicit params
+cloneDict (Dict nm ty loc) = newUnique `thenM` \ uniq ->
+ returnM (Dict (setNameUnique nm uniq) ty loc)
+