compiler/typecheck/Inst.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 The @Inst@ type: dictionaries or method instances
   7
   8 \begin{code}
   9 module Inst (
  10         Inst,
  11
  12         pprInstances, pprDictsTheta, pprDictsInFull,    -- User error messages
  13         showLIE, pprInst, pprInsts, pprInstInFull,      -- Debugging messages
  14
  15         tidyInsts, tidyMoreInsts,
  16
  17         newDictBndr, newDictBndrs, newDictBndrsO,
  18         newDictOccs, newDictOcc,
  19         instCall, instStupidTheta,
  20         cloneDict, mkOverLit,
  21         newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy,
  22         tcInstClassOp,
  23         tcSyntaxName, isHsVar,
  24
  25         tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE,
  26         ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
  27         growInstsTyVars, getDictClassTys, dictPred,
  28
  29         lookupSimpleInst, LookupInstResult(..),
  30         tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
  31
  32         isAbstractableInst, isEqInst,
  33         isDict, isClassDict, isMethod, isImplicInst,
  34         isIPDict, isInheritableInst, isMethodOrLit,
  35         isTyVarDict, isMethodFor,
  36
  37         zonkInst, zonkInsts,
  38         instToId, instToVar, instType, instName, instToDictBind,
  39         addInstToDictBind,
  40
  41         InstOrigin(..), InstLoc, pprInstLoc,
  42
  43         mkWantedCo, mkGivenCo, isWantedCo, eqInstCoType, mkIdEqInstCo,
  44         mkSymEqInstCo, mkLeftTransEqInstCo, mkRightTransEqInstCo, mkAppEqInstCo,
  45         mkTyConEqInstCo, mkFunEqInstCo,
  46         wantedEqInstIsUnsolved, eitherEqInst, mkEqInst, mkWantedEqInst,
  47         wantedToLocalEqInst, finalizeEqInst, eqInstType, eqInstCoercion,
  48         eqInstTys
  49     ) where
  50
  51 #include "HsVersions.h"
  52
  53 import {-# SOURCE #-}   TcExpr( tcPolyExpr )
  54 import {-# SOURCE #-}   TcUnify( boxyUnify {- , unifyType -} )
  55
  56 import FastString
  57 import HsSyn
  58 import TcHsSyn
  59 import TcRnMonad
  60 import TcEnv
  61 import InstEnv
  62 import FunDeps
  63 import TcMType
  64 import TcType
  65 import MkCore
  66 import TyCon
  67 import Type
  68 import TypeRep
  69 import Class
  70 import Unify
  71 import Module
  72 import Coercion
  73 import HscTypes
  74 import CoreFVs
  75 import Id
  76 import Name
  77 import NameSet
  78 import Var      ( Var, TyVar )
  79 import qualified Var
  80 import VarEnv
  81 import VarSet
  82 import PrelNames
  83 import BasicTypes
  84 import SrcLoc
  85 import DynFlags
  86 import Bag
  87 import Maybes
  88 import Util
  89 import Unique
  90 import Outputable
  91 import Data.List
  92
  93 import Control.Monad
  94 \end{code}
  95
  96
  97
  98 Selection
  99 ~~~~~~~~~
 100 \begin{code}
 101 instName :: Inst -> Name
 102 instName (EqInst {tci_name = name}) = name
 103 instName inst = Var.varName (instToVar inst)
 104
 105 instToId :: Inst -> TcId
 106 instToId inst = WARN( not (isId id), ppr inst )
 107               id
 108               where
 109                 id = instToVar inst
 110
 111 instToVar :: Inst -> Var
 112 instToVar (LitInst {tci_name = nm, tci_ty = ty})
 113   = mkLocalId nm ty
 114 instToVar (Method {tci_id = id})
 115   = id
 116 instToVar (Dict {tci_name = nm, tci_pred = pred})
 117   | isEqPred pred = Var.mkCoVar nm (mkPredTy pred)
 118   | otherwise     = mkLocalId nm (mkPredTy pred)
 119 instToVar (ImplicInst {tci_name = nm, tci_tyvars = tvs, tci_given = givens,
 120                        tci_wanted = wanteds})
 121   = mkLocalId nm (mkImplicTy tvs givens wanteds)
 122 instToVar inst@(EqInst {})
 123   = eitherEqInst inst id assertCoVar
 124   where
 125     assertCoVar (TyVarTy cotv) = cotv
 126     assertCoVar coty           = pprPanic "Inst.instToVar" (ppr coty)
 127
 128 instType :: Inst -> Type
 129 instType (LitInst {tci_ty = ty})  = ty
 130 instType (Method {tci_id = id})   = idType id
 131 instType (Dict {tci_pred = pred}) = mkPredTy pred
 132 instType imp@(ImplicInst {})      = mkImplicTy (tci_tyvars imp) (tci_given imp)
 133                                                (tci_wanted imp)
 134 -- instType i@(EqInst {tci_co = co}) = eitherEqInst i TyVarTy id
 135 instType (EqInst {tci_left = ty1, tci_right = ty2}) = mkPredTy (EqPred ty1 ty2)
 136
 137 mkImplicTy :: [TyVar] -> [Inst] -> [Inst] -> Type
 138 mkImplicTy tvs givens wanteds   -- The type of an implication constraint
 139   = ASSERT( all isAbstractableInst givens )
 140     -- pprTrace "mkImplicTy" (ppr givens) $
 141     -- See [Equational Constraints in Implication Constraints]
 142     let dict_wanteds = filter (not . isEqInst) wanteds
 143     in
 144       mkForAllTys tvs $
 145       mkPhiTy (map dictPred givens) $
 146       mkBigCoreTupTy (map instType dict_wanteds)
 147
 148 dictPred :: Inst -> TcPredType
 149 dictPred (Dict {tci_pred = pred}) = pred
 150 dictPred (EqInst {tci_left=ty1,tci_right=ty2}) = EqPred ty1 ty2
 151 dictPred inst                     = pprPanic "dictPred" (ppr inst)
 152
 153 getDictClassTys :: Inst -> (Class, [Type])
 154 getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred
 155 getDictClassTys inst                     = pprPanic "getDictClassTys" (ppr inst)
 156
 157 --------------------------------
 158 -- fdPredsOfInst is used to get predicates that contain functional
 159 -- dependencies *or* might do so.  The "might do" part is because
 160 -- a constraint (C a b) might have a superclass with FDs
 161 -- Leaving these in is really important for the call to fdPredsOfInsts
 162 -- in TcSimplify.inferLoop, because the result is fed to 'grow',
 163 -- which is supposed to be conservative
 164 fdPredsOfInst :: Inst -> [TcPredType]
 165 fdPredsOfInst (Dict {tci_pred = pred})       = [pred]
 166 fdPredsOfInst (Method {tci_theta = theta})   = theta
 167 fdPredsOfInst (ImplicInst {tci_wanted = ws}) = fdPredsOfInsts ws
 168    -- The ImplicInst case doesn't look right;
 169    -- what if ws mentions skolem variables?
 170 fdPredsOfInst (LitInst {})                   = []
 171 fdPredsOfInst (EqInst {})                    = []
 172
 173 fdPredsOfInsts :: [Inst] -> [PredType]
 174 fdPredsOfInsts insts = concatMap fdPredsOfInst insts
 175
 176 ---------------------------------
 177 isInheritableInst :: Inst -> Bool
 178 isInheritableInst (Dict {tci_pred = pred})     = isInheritablePred pred
 179 isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta
 180 isInheritableInst _                            = True
 181
 182
 183 ---------------------------------
 184 -- Get the implicit parameters mentioned by these Insts
 185 -- NB: the results of these functions are insensitive to zonking
 186
 187 ipNamesOfInsts :: [Inst] -> [Name]
 188 ipNamesOfInst  :: Inst   -> [Name]
 189 ipNamesOfInsts insts = [n | inst <- insts, n <- ipNamesOfInst inst]
 190
 191 ipNamesOfInst (Dict {tci_pred = IParam n _}) = [ipNameName n]
 192 ipNamesOfInst (Method {tci_theta = theta})   = [ipNameName n | IParam n _ <- theta]
 193 ipNamesOfInst _                              = []
 194
 195 ---------------------------------
 196 tyVarsOfInst :: Inst -> TcTyVarSet
 197 tyVarsOfInst (LitInst {tci_ty = ty})  = tyVarsOfType  ty
 198 tyVarsOfInst (Dict {tci_pred = pred}) = tyVarsOfPred pred
 199 tyVarsOfInst (Method {tci_oid = id, tci_tys = tys}) = tyVarsOfTypes tys `unionVarSet` varTypeTyVars id
 200                                  -- The id might have free type variables; in the case of
 201                                  -- locally-overloaded class methods, for example
 202 tyVarsOfInst (ImplicInst {tci_tyvars = tvs, tci_given = givens, tci_wanted = wanteds})
 203   = (tyVarsOfInsts givens `unionVarSet` tyVarsOfInsts wanteds)
 204     `minusVarSet` mkVarSet tvs
 205     `unionVarSet` unionVarSets (map varTypeTyVars tvs)
 206                 -- Remember the free tyvars of a coercion
 207 tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 208
 209 tyVarsOfInsts :: [Inst] -> VarSet
 210 tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
 211 tyVarsOfLIE :: Bag Inst -> VarSet
 212 tyVarsOfLIE   lie   = tyVarsOfInsts (lieToList lie)
 213
 214
 215 --------------------------
 216 instToDictBind :: Inst -> LHsExpr TcId -> TcDictBinds
 217 instToDictBind inst rhs
 218   = unitBag (L (instSpan inst) (VarBind (instToId inst) rhs))
 219
 220 addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds
 221 addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs
 222 \end{code}
 223
 224 Note [Growing the tau-tvs using constraints]
 225 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 226 (growInstsTyVars insts tvs) is the result of extending the set
 227     of tyvars tvs using all conceivable links from pred
 228
 229 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
 230 Then grow precs tvs = {a,b,c}
 231
 232 All the type variables from an implicit parameter are added, whether or
 233 not they are mentioned in tvs; see Note [Implicit parameters and ambiguity]
 234 in TcSimplify.
 235
 236 See also Note [Ambiguity] in TcSimplify
 237
 238 \begin{code}
 239 growInstsTyVars :: [Inst] -> TyVarSet -> TyVarSet
 240 growInstsTyVars insts tvs
 241   | null insts = tvs
 242   | otherwise  = fixVarSet mk_next tvs
 243   where
 244     mk_next tvs = foldr grow_inst_tvs tvs insts
 245
 246 grow_inst_tvs :: Inst -> TyVarSet -> TyVarSet
 247 grow_inst_tvs (Dict {tci_pred = pred})     tvs = growPredTyVars pred tvs
 248 grow_inst_tvs (Method {tci_theta = theta}) tvs = foldr growPredTyVars tvs theta
 249 grow_inst_tvs (ImplicInst {tci_tyvars = tvs1, tci_wanted = ws}) tvs
 250   = tvs `unionVarSet` (foldr grow_inst_tvs (tvs `delVarSetList` tvs1) ws
 251                           `delVarSetList` tvs1)
 252 grow_inst_tvs inst tvs   -- EqInst, LitInst
 253   = growTyVars (tyVarsOfInst inst) tvs
 254 \end{code}
 255
 256
 257 %************************************************************************
 258 %*                                                                      *
 259                 Predicates
 260 %*                                                                      *
 261 %************************************************************************
 262
 263 \begin{code}
 264
 265 isAbstractableInst :: Inst -> Bool
 266 isAbstractableInst inst = isDict inst || isEqInst inst
 267
 268 isEqInst :: Inst -> Bool
 269 isEqInst (EqInst {}) = True
 270 isEqInst _           = False
 271
 272 isDict :: Inst -> Bool
 273 isDict (Dict {}) = True
 274 isDict _         = False
 275
 276 isClassDict :: Inst -> Bool
 277 isClassDict (Dict {tci_pred = pred}) = isClassPred pred
 278 isClassDict _                        = False
 279
 280 isTyVarDict :: Inst -> Bool
 281 isTyVarDict (Dict {tci_pred = pred}) = isTyVarClassPred pred
 282 isTyVarDict _                        = False
 283
 284 isIPDict :: Inst -> Bool
 285 isIPDict (Dict {tci_pred = pred}) = isIPPred pred
 286 isIPDict _                        = False
 287
 288 isImplicInst :: Inst -> Bool
 289 isImplicInst (ImplicInst {}) = True
 290 isImplicInst _               = False
 291
 292 isMethod :: Inst -> Bool
 293 isMethod (Method {}) = True
 294 isMethod _           = False
 295
 296 isMethodFor :: TcIdSet -> Inst -> Bool
 297 isMethodFor ids (Method {tci_oid = id}) = id `elemVarSet` ids
 298 isMethodFor _   _                       = False
 299
 300 isMethodOrLit :: Inst -> Bool
 301 isMethodOrLit (Method {})  = True
 302 isMethodOrLit (LitInst {}) = True
 303 isMethodOrLit _            = False
 304 \end{code}
 305
 306
 307 %************************************************************************
 308 %*                                                                      *
 309 \subsection{Building dictionaries}
 310 %*                                                                      *
 311 %************************************************************************
 312
 313 -- newDictBndrs makes a dictionary at a binding site
 314 -- instCall makes a dictionary at an occurrence site
 315 --      and throws it into the LIE
 316
 317 \begin{code}
 318 ----------------
 319 newDictBndrsO :: InstOrigin -> TcThetaType -> TcM [Inst]
 320 newDictBndrsO orig theta = do { loc <- getInstLoc orig
 321                               ; newDictBndrs loc theta }
 322
 323 newDictBndrs :: InstLoc -> TcThetaType -> TcM [Inst]
 324 newDictBndrs inst_loc theta = mapM (newDictBndr inst_loc) theta
 325
 326 newDictBndr :: InstLoc -> TcPredType -> TcM Inst
 327 -- Makes a "given"
 328 newDictBndr inst_loc pred@(EqPred ty1 ty2)
 329   = do { uniq <- newUnique
 330         ; let name = mkPredName uniq inst_loc pred
 331               co   = mkGivenCo $ TyVarTy (Var.mkCoVar name (PredTy pred))
 332         ; return (EqInst {tci_name  = name,
 333                           tci_loc   = inst_loc,
 334                           tci_left  = ty1,
 335                           tci_right = ty2,
 336                           tci_co    = co }) }
 337
 338 newDictBndr inst_loc pred = newDict inst_loc pred
 339
 340 -------------------
 341 newDictOccs :: InstLoc -> TcThetaType -> TcM [Inst]
 342 newDictOccs inst_loc theta = mapM (newDictOcc inst_loc) theta
 343
 344 newDictOcc :: InstLoc -> TcPredType -> TcM Inst
 345 -- Makes a "wanted"
 346 newDictOcc inst_loc pred@(EqPred ty1 ty2)
 347   = do  { uniq <- newUnique
 348         ; cotv <- newMetaCoVar ty1 ty2
 349         ; let name = mkPredName uniq inst_loc pred
 350         ; return (EqInst {tci_name  = name,
 351                           tci_loc   = inst_loc,
 352                           tci_left  = ty1,
 353                           tci_right = ty2,
 354                           tci_co    = Left cotv }) }
 355
 356 newDictOcc inst_loc pred = newDict inst_loc pred
 357
 358 ----------------
 359 newDict :: InstLoc -> TcPredType -> TcM Inst
 360 -- Always makes a Dict, not an EqInst
 361 newDict inst_loc pred
 362   = do  { uniq <- newUnique
 363         ; let name = mkPredName uniq inst_loc pred
 364         ; return (Dict {tci_name = name, tci_pred = pred, tci_loc = inst_loc}) }
 365
 366 ----------------
 367 instCall :: InstOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
 368 -- Instantiate the constraints of a call
 369 --      (instCall o tys theta)
 370 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
 371 -- (b) Throws these dictionaries into the LIE
 372 -- (c) Returns an HsWrapper ([.] tys dicts)
 373
 374 instCall orig tys theta
 375   = do  { loc <- getInstLoc orig
 376         ; dict_app <- instCallDicts loc theta
 377         ; return (dict_app <.> mkWpTyApps tys) }
 378
 379 ----------------
 380 instStupidTheta :: InstOrigin -> TcThetaType -> TcM ()
 381 -- Similar to instCall, but only emit the constraints in the LIE
 382 -- Used exclusively for the 'stupid theta' of a data constructor
 383 instStupidTheta orig theta
 384   = do  { loc <- getInstLoc orig
 385         ; _co <- instCallDicts loc theta        -- Discard the coercion
 386         ; return () }
 387
 388 ----------------
 389 instCallDicts :: InstLoc -> TcThetaType -> TcM HsWrapper
 390 -- Instantiates the TcTheta, puts all constraints thereby generated
 391 -- into the LIE, and returns a HsWrapper to enclose the call site.
 392 -- This is the key place where equality predicates
 393 -- are unleashed into the world
 394 instCallDicts _ [] = return idHsWrapper
 395
 396 -- instCallDicts loc (EqPred ty1 ty2 : preds)
 397 --   = do  { unifyType ty1 ty2  -- For now, we insist that they unify right away
 398 --                              -- Later on, when we do associated types,
 399 --                              -- unifyType :: Type -> Type -> TcM ([Inst], Coercion)
 400 --      ; (dicts, co_fn) <- instCallDicts loc preds
 401 --      ; return (dicts, co_fn <.> WpTyApp ty1) }
 402 --      -- We use type application to apply the function to the
 403 --      -- coercion; here ty1 *is* the appropriate identity coercion
 404
 405 instCallDicts loc (EqPred ty1 ty2 : preds)
 406   = do  { traceTc (text "instCallDicts" <+> ppr (EqPred ty1 ty2))
 407         ; coi <- boxyUnify ty1 ty2
 408         ; let co = fromCoI coi ty1
 409         ; co_fn <- instCallDicts loc preds
 410         ; return (co_fn <.> WpTyApp co) }
 411
 412 instCallDicts loc (pred : preds)
 413   = do  { dict <- newDict loc pred
 414         ; extendLIE dict
 415         ; co_fn <- instCallDicts loc preds
 416         ; return (co_fn <.> WpApp (instToId dict)) }
 417
 418 -------------
 419 cloneDict :: Inst -> TcM Inst
 420 cloneDict dict@(Dict nm _ _) = do { uniq <- newUnique
 421                                   ; return (dict {tci_name = setNameUnique nm uniq}) }
 422 cloneDict eq@(EqInst {})     = return eq
 423 cloneDict other = pprPanic "cloneDict" (ppr other)
 424
 425 -- For vanilla implicit parameters, there is only one in scope
 426 -- at any time, so we used to use the name of the implicit parameter itself
 427 -- But with splittable implicit parameters there may be many in
 428 -- scope, so we make up a new namea.
 429 newIPDict :: InstOrigin -> IPName Name -> Type
 430           -> TcM (IPName Id, Inst)
 431 newIPDict orig ip_name ty
 432   = do  { inst_loc <- getInstLoc orig
 433         ; dict <- newDict inst_loc (IParam ip_name ty)
 434         ; return (mapIPName (\_ -> instToId dict) ip_name, dict) }
 435 \end{code}
 436
 437
 438 \begin{code}
 439 mkPredName :: Unique -> InstLoc -> PredType -> Name
 440 mkPredName uniq loc pred_ty
 441   = mkInternalName uniq occ (instLocSpan loc)
 442   where
 443     occ = case pred_ty of
 444             ClassP cls _ -> mkDictOcc (getOccName cls)
 445             IParam ip  _ -> getOccName (ipNameName ip)
 446             EqPred ty  _ -> mkEqPredCoOcc baseOcc
 447               where
 448                 -- we use the outermost tycon of the lhs, if there is one, to
 449                 -- improve readability of Core code
 450                 baseOcc = case splitTyConApp_maybe ty of
 451                             Nothing      -> mkTcOcc "$"
 452                             Just (tc, _) -> getOccName tc
 453 \end{code}
 454
 455 %************************************************************************
 456 %*                                                                      *
 457 \subsection{Building methods (calls of overloaded functions)}
 458 %*                                                                      *
 459 %************************************************************************
 460
 461
 462 \begin{code}
 463 newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
 464 newMethodFromName origin ty name = do
 465     id <- tcLookupId name
 466         -- Use tcLookupId not tcLookupGlobalId; the method is almost
 467         -- always a class op, but with -XNoImplicitPrelude GHC is
 468         -- meant to find whatever thing is in scope, and that may
 469         -- be an ordinary function.
 470     loc <- getInstLoc origin
 471     inst <- tcInstClassOp loc id [ty]
 472     extendLIE inst
 473     return (instToId inst)
 474
 475 newMethodWithGivenTy :: InstOrigin -> Id -> [Type] -> TcRn TcId
 476 newMethodWithGivenTy orig id tys = do
 477     loc <- getInstLoc orig
 478     inst <- newMethod loc id tys
 479     extendLIE inst
 480     return (instToId inst)
 481
 482 --------------------------------------------
 483 -- tcInstClassOp, and newMethod do *not* drop the
 484 -- Inst into the LIE; they just returns the Inst
 485 -- This is important because they are used by TcSimplify
 486 -- to simplify Insts
 487
 488 -- NB: the kind of the type variable to be instantiated
 489 --     might be a sub-kind of the type to which it is applied,
 490 --     notably when the latter is a type variable of kind ??
 491 --     Hence the call to checkKind
 492 -- A worry: is this needed anywhere else?
 493 tcInstClassOp :: InstLoc -> Id -> [TcType] -> TcM Inst
 494 tcInstClassOp inst_loc sel_id tys = do
 495     let
 496         (tyvars, _rho) = tcSplitForAllTys (idType sel_id)
 497     zipWithM_ checkKind tyvars tys
 498     newMethod inst_loc sel_id tys
 499
 500 checkKind :: TyVar -> TcType -> TcM ()
 501 -- Ensure that the type has a sub-kind of the tyvar
 502 checkKind tv ty
 503   = do  { let ty1 = ty
 504                 -- ty1 <- zonkTcType ty
 505         ; if typeKind ty1 `isSubKind` Var.tyVarKind tv
 506           then return ()
 507           else
 508
 509     pprPanic "checkKind: adding kind constraint"
 510              (vcat [ppr tv <+> ppr (Var.tyVarKind tv),
 511                     ppr ty <+> ppr ty1 <+> ppr (typeKind ty1)])
 512         }
 513 --    do        { tv1 <- tcInstTyVar tv
 514 --      ; unifyType ty1 (mkTyVarTy tv1) } }
 515
 516
 517 ---------------------------
 518 newMethod :: InstLoc -> Id -> [Type] -> TcRn Inst
 519 newMethod inst_loc id tys = do
 520     new_uniq <- newUnique
 521     let
 522         (theta,tau) = tcSplitPhiTy (applyTys (idType id) tys)
 523         meth_id     = mkUserLocal (mkMethodOcc (getOccName id)) new_uniq tau loc
 524         inst        = Method {tci_id = meth_id, tci_oid = id, tci_tys = tys,
 525                               tci_theta = theta, tci_loc = inst_loc}
 526         loc         = instLocSpan inst_loc
 527
 528     return inst
 529 \end{code}
 530
 531 \begin{code}
 532 mkOverLit :: OverLitVal -> TcM HsLit
 533 mkOverLit (HsIntegral i)
 534   = do  { integer_ty <- tcMetaTy integerTyConName
 535         ; return (HsInteger i integer_ty) }
 536
 537 mkOverLit (HsFractional r)
 538   = do  { rat_ty <- tcMetaTy rationalTyConName
 539         ; return (HsRat r rat_ty) }
 540
 541 mkOverLit (HsIsString s) = return (HsString s)
 542
 543 isHsVar :: HsExpr Name -> Name -> Bool
 544 isHsVar (HsVar f) g = f == g
 545 isHsVar _         _ = False
 546 \end{code}
 547
 548
 549 %************************************************************************
 550 %*                                                                      *
 551 \subsection{Zonking}
 552 %*                                                                      *
 553 %************************************************************************
 554
 555 Zonking makes sure that the instance types are fully zonked.
 556
 557 \begin{code}
 558 zonkInst :: Inst -> TcM Inst
 559 zonkInst dict@(Dict {tci_pred = pred}) = do
 560     new_pred <- zonkTcPredType pred
 561     return (dict {tci_pred = new_pred})
 562
 563 zonkInst meth@(Method {tci_oid = id, tci_tys = tys, tci_theta = theta}) = do
 564     new_id <- zonkId id
 565         -- Essential to zonk the id in case it's a local variable
 566         -- Can't use zonkIdOcc because the id might itself be
 567         -- an InstId, in which case it won't be in scope
 568
 569     new_tys <- zonkTcTypes tys
 570     new_theta <- zonkTcThetaType theta
 571     return (meth { tci_oid = new_id, tci_tys = new_tys, tci_theta = new_theta })
 572         -- No need to zonk the tci_id
 573
 574 zonkInst lit@(LitInst {tci_ty = ty}) = do
 575     new_ty <- zonkTcType ty
 576     return (lit {tci_ty = new_ty})
 577
 578 zonkInst implic@(ImplicInst {})
 579   = ASSERT( all isImmutableTyVar (tci_tyvars implic) )
 580     do  { givens'  <- zonkInsts (tci_given  implic)
 581         ; wanteds' <- zonkInsts (tci_wanted implic)
 582         ; return (implic {tci_given = givens',tci_wanted = wanteds'}) }
 583
 584 zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2})
 585   = do { co' <- eitherEqInst eqinst
 586                   (\covar -> return (mkWantedCo covar))
 587                   (\co    -> liftM mkGivenCo $ zonkTcType co)
 588        ; ty1' <- zonkTcType ty1
 589        ; ty2' <- zonkTcType ty2
 590        ; return (eqinst {tci_co = co', tci_left = ty1', tci_right = ty2' })
 591        }
 592
 593 zonkInsts :: [Inst] -> TcRn [Inst]
 594 zonkInsts insts = mapM zonkInst insts
 595 \end{code}
 596
 597
 598 %************************************************************************
 599 %*                                                                      *
 600 \subsection{Printing}
 601 %*                                                                      *
 602 %************************************************************************
 603
 604 ToDo: improve these pretty-printing things.  The ``origin'' is really only
 605 relevant in error messages.
 606
 607 \begin{code}
 608 instance Outputable Inst where
 609     ppr inst = pprInst inst
 610
 611 pprDictsTheta :: [Inst] -> SDoc
 612 -- Print in type-like fashion (Eq a, Show b)
 613 -- The Inst can be an implication constraint, but not a Method or LitInst
 614 pprDictsTheta insts = parens (sep (punctuate comma (map (ppr . instType) insts)))
 615
 616 pprDictsInFull :: [Inst] -> SDoc
 617 -- Print in type-like fashion, but with source location
 618 pprDictsInFull dicts
 619   = vcat (map go dicts)
 620   where
 621     go dict = sep [quotes (ppr (instType dict)), nest 2 (pprInstArising dict)]
 622
 623 pprInsts :: [Inst] -> SDoc
 624 -- Debugging: print the evidence :: type
 625 pprInsts insts = brackets (interpp'SP insts)
 626
 627 pprInst, pprInstInFull :: Inst -> SDoc
 628 -- Debugging: print the evidence :: type
 629 pprInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 630         = eitherEqInst i
 631                 (\covar -> text "Wanted" <+> ppr (TyVarTy covar) <+> dcolon <+> ppr (EqPred ty1 ty2))
 632                 (\co    -> text "Given"  <+> ppr co              <+> dcolon <+> ppr (EqPred ty1 ty2))
 633 pprInst inst = ppr name <> braces (pprUnique (getUnique name)) <+> dcolon
 634                 <+> braces (ppr (instType inst) <> implicWantedEqs)
 635   where
 636     name = instName inst
 637     implicWantedEqs
 638       | isImplicInst inst = text " &" <+>
 639                             ppr (filter isEqInst (tci_wanted inst))
 640       | otherwise         = empty
 641
 642 pprInstInFull inst@(EqInst {}) = pprInst inst
 643 pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]
 644
 645 tidyInst :: TidyEnv -> Inst -> Inst
 646 tidyInst env eq@(EqInst {tci_left = lty, tci_right = rty, tci_co = co}) =
 647   eq { tci_left  = tidyType env lty
 648      , tci_right = tidyType env rty
 649      , tci_co    = either Left (Right . tidyType env) co
 650      }
 651 tidyInst env lit@(LitInst {tci_ty = ty})   = lit {tci_ty = tidyType env ty}
 652 tidyInst env dict@(Dict {tci_pred = pred}) = dict {tci_pred = tidyPred env pred}
 653 tidyInst env meth@(Method {tci_tys = tys}) = meth {tci_tys = tidyTypes env tys}
 654 tidyInst env implic@(ImplicInst {})
 655   = implic { tci_tyvars = tvs'
 656            , tci_given  = map (tidyInst env') (tci_given  implic)
 657            , tci_wanted = map (tidyInst env') (tci_wanted implic) }
 658   where
 659     (env', tvs') = mapAccumL tidyTyVarBndr env (tci_tyvars implic)
 660
 661 tidyMoreInsts :: TidyEnv -> [Inst] -> (TidyEnv, [Inst])
 662 -- This function doesn't assume that the tyvars are in scope
 663 -- so it works like tidyOpenType, returning a TidyEnv
 664 tidyMoreInsts env insts
 665   = (env', map (tidyInst env') insts)
 666   where
 667     env' = tidyFreeTyVars env (tyVarsOfInsts insts)
 668
 669 tidyInsts :: [Inst] -> (TidyEnv, [Inst])
 670 tidyInsts insts = tidyMoreInsts emptyTidyEnv insts
 671
 672 showLIE :: SDoc -> TcM ()       -- Debugging
 673 showLIE str
 674   = do { lie_var <- getLIEVar ;
 675          lie <- readMutVar lie_var ;
 676          traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) }
 677 \end{code}
 678
 679
 680 %************************************************************************
 681 %*                                                                      *
 682         Extending the instance environment
 683 %*                                                                      *
 684 %************************************************************************
 685
 686 \begin{code}
 687 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
 688   -- Add new locally-defined instances
 689 tcExtendLocalInstEnv dfuns thing_inside
 690  = do { traceDFuns dfuns
 691       ; env <- getGblEnv
 692       ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
 693       ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
 694                          tcg_inst_env = inst_env' }
 695       ; setGblEnv env' thing_inside }
 696
 697 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
 698 -- Check that the proposed new instance is OK,
 699 -- and then add it to the home inst env
 700 addLocalInst home_ie ispec
 701   = do  {       -- Instantiate the dfun type so that we extend the instance
 702                 -- envt with completely fresh template variables
 703                 -- This is important because the template variables must
 704                 -- not overlap with anything in the things being looked up
 705                 -- (since we do unification).
 706                 -- We use tcInstSkolType because we don't want to allocate fresh
 707                 --  *meta* type variables.
 708           let dfun = instanceDFunId ispec
 709         ; (tvs', theta', tau') <- tcInstSkolType InstSkol (idType dfun)
 710         ; let   (cls, tys') = tcSplitDFunHead tau'
 711                 dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')
 712                 ispec'      = setInstanceDFunId ispec dfun'
 713
 714                 -- Load imported instances, so that we report
 715                 -- duplicates correctly
 716         ; eps <- getEps
 717         ; let inst_envs = (eps_inst_env eps, home_ie)
 718
 719                 -- Check functional dependencies
 720         ; case checkFunDeps inst_envs ispec' of
 721                 Just specs -> funDepErr ispec' specs
 722                 Nothing    -> return ()
 723
 724                 -- Check for duplicate instance decls
 725         ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
 726               ; dup_ispecs = [ dup_ispec
 727                              | (dup_ispec, _) <- matches
 728                              , let (_,_,_,dup_tys) = instanceHead dup_ispec
 729                              , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
 730                 -- Find memebers of the match list which ispec itself matches.
 731                 -- If the match is 2-way, it's a duplicate
 732         ; case dup_ispecs of
 733             dup_ispec : _ -> dupInstErr ispec' dup_ispec
 734             []            -> return ()
 735
 736                 -- OK, now extend the envt
 737         ; return (extendInstEnv home_ie ispec') }
 738
 739 getOverlapFlag :: TcM OverlapFlag
 740 getOverlapFlag
 741   = do  { dflags <- getDOpts
 742         ; let overlap_ok    = dopt Opt_OverlappingInstances dflags
 743               incoherent_ok = dopt Opt_IncoherentInstances  dflags
 744               overlap_flag | incoherent_ok = Incoherent
 745                            | overlap_ok    = OverlapOk
 746                            | otherwise     = NoOverlap
 747
 748         ; return overlap_flag }
 749
 750 traceDFuns :: [Instance] -> TcRn ()
 751 traceDFuns ispecs
 752   = traceTc (hang (text "Adding instances:") 2 (vcat (map pp ispecs)))
 753   where
 754     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
 755         -- Print the dfun name itself too
 756
 757 funDepErr :: Instance -> [Instance] -> TcRn ()
 758 funDepErr ispec ispecs
 759   = addDictLoc ispec $
 760     addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
 761                2 (pprInstances (ispec:ispecs)))
 762 dupInstErr :: Instance -> Instance -> TcRn ()
 763 dupInstErr ispec dup_ispec
 764   = addDictLoc ispec $
 765     addErr (hang (ptext (sLit "Duplicate instance declarations:"))
 766                2 (pprInstances [ispec, dup_ispec]))
 767
 768 addDictLoc :: Instance -> TcRn a -> TcRn a
 769 addDictLoc ispec thing_inside
 770   = setSrcSpan (mkSrcSpan loc loc) thing_inside
 771   where
 772    loc = getSrcLoc ispec
 773 \end{code}
 774
 775
 776 %************************************************************************
 777 %*                                                                      *
 778 \subsection{Looking up Insts}
 779 %*                                                                      *
 780 %************************************************************************
 781
 782 \begin{code}
 783 data LookupInstResult
 784   = NoInstance
 785   | GenInst [Inst] (LHsExpr TcId)       -- The expression and its needed insts
 786
 787 lookupSimpleInst :: Inst -> TcM LookupInstResult
 788 -- This is "simple" in that it returns NoInstance for implication constraints
 789
 790 -- It's important that lookupInst does not put any new stuff into
 791 -- the LIE.  Instead, any Insts needed by the lookup are returned in
 792 -- the LookupInstResult, where they can be further processed by tcSimplify
 793
 794 lookupSimpleInst (EqInst {}) = return NoInstance
 795
 796 --------------------- Implications ------------------------
 797 lookupSimpleInst (ImplicInst {}) = return NoInstance
 798
 799 --------------------- Methods ------------------------
 800 lookupSimpleInst (Method {tci_oid = id, tci_tys = tys, tci_theta = theta, tci_loc = loc})
 801   = do  { (dict_app, dicts) <- getLIE $ instCallDicts loc theta
 802         ; let co_fn = dict_app <.> mkWpTyApps tys
 803         ; return (GenInst dicts (L span $ HsWrap co_fn (HsVar id))) }
 804   where
 805     span = instLocSpan loc
 806
 807 --------------------- Literals ------------------------
 808 -- Look for short cuts first: if the literal is *definitely* a
 809 -- int, integer, float or a double, generate the real thing here.
 810 -- This is essential (see nofib/spectral/nucleic).
 811 -- [Same shortcut as in newOverloadedLit, but we
 812 --  may have done some unification by now]
 813
 814 lookupSimpleInst (LitInst { tci_lit = lit@OverLit { ol_val = lit_val
 815                                                   , ol_rebindable = rebindable }
 816                           , tci_ty = ty, tci_loc = iloc})
 817   | debugIsOn && rebindable = panic "lookupSimpleInst" -- A LitInst invariant
 818   | Just witness <- shortCutLit lit_val ty
 819   = do  { let lit' = lit { ol_witness = witness, ol_type = ty }
 820         ; return (GenInst [] (L loc (HsOverLit lit'))) }
 821
 822   | otherwise
 823   = do  { hs_lit <- mkOverLit lit_val
 824         ; from_thing <- tcLookupId (hsOverLitName lit_val)
 825                   -- Not rebindable, so hsOverLitName is the right thing
 826         ; method_inst <- tcInstClassOp iloc from_thing [ty]
 827         ; let witness = HsApp (L loc (HsVar (instToId method_inst)))
 828                               (L loc (HsLit hs_lit))
 829               lit' = lit { ol_witness = witness, ol_type = ty }
 830         ; return (GenInst [method_inst] (L loc (HsOverLit lit'))) }
 831   where
 832     loc = instLocSpan iloc
 833
 834 --------------------- Dictionaries ------------------------
 835 lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
 836   = do  { mb_result <- lookupPred pred
 837         ; case mb_result of {
 838             Nothing -> return NoInstance ;
 839             Just (dfun_id, mb_inst_tys) -> do
 840
 841     { use_stage <- getStage
 842     ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
 843                       (topIdLvl dfun_id) use_stage
 844
 845         -- It's possible that not all the tyvars are in
 846         -- the substitution, tenv. For example:
 847         --      instance C X a => D X where ...
 848         -- (presumably there's a functional dependency in class C)
 849         -- Hence mb_inst_tys :: Either TyVar TcType
 850
 851     ; let inst_tv (Left tv)  = do { tv' <- tcInstTyVar tv; return (mkTyVarTy tv') }
 852           inst_tv (Right ty) = return ty
 853     ; tys <- mapM inst_tv mb_inst_tys
 854     ; let
 855         (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
 856         src_loc    = instLocSpan loc
 857         dfun       = HsVar dfun_id
 858     ; if null theta then
 859         return (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
 860       else do
 861     { (dict_app, dicts) <- getLIE $ instCallDicts loc theta -- !!!
 862     ; let co_fn = dict_app <.> mkWpTyApps tys
 863     ; return (GenInst dicts (L src_loc $ HsWrap co_fn dfun))
 864     }}}}
 865
 866 ---------------
 867 lookupPred :: TcPredType -> TcM (Maybe (DFunId, [Either TyVar TcType]))
 868 -- Look up a class constraint in the instance environment
 869 lookupPred pred@(ClassP clas tys)
 870   = do  { eps     <- getEps
 871         ; tcg_env <- getGblEnv
 872         ; let inst_envs = (eps_inst_env eps, tcg_inst_env tcg_env)
 873         ; case lookupInstEnv inst_envs clas tys of {
 874             ([(ispec, inst_tys)], [])
 875                 -> do   { let dfun_id = is_dfun ispec
 876                         ; traceTc (text "lookupInst success" <+>
 877                                    vcat [text "dict" <+> ppr pred,
 878                                          text "witness" <+> ppr dfun_id
 879                                          <+> ppr (idType dfun_id) ])
 880                                 -- Record that this dfun is needed
 881                         ; record_dfun_usage dfun_id
 882                         ; return (Just (dfun_id, inst_tys)) } ;
 883
 884             (matches, unifs)
 885                 -> do   { traceTc (text "lookupInst fail" <+>
 886                                    vcat [text "dict" <+> ppr pred,
 887                                          text "matches" <+> ppr matches,
 888                                          text "unifs" <+> ppr unifs])
 889                 -- In the case of overlap (multiple matches) we report
 890                 -- NoInstance here.  That has the effect of making the
 891                 -- context-simplifier return the dict as an irreducible one.
 892                 -- Then it'll be given to addNoInstanceErrs, which will do another
 893                 -- lookupInstEnv to get the detailed info about what went wrong.
 894                         ; return Nothing }
 895         }}
 896
 897 lookupPred (IParam {}) = return Nothing -- Implicit parameters
 898 lookupPred (EqPred {}) = panic "lookupPred EqPred"
 899
 900 record_dfun_usage :: Id -> TcRn ()
 901 record_dfun_usage dfun_id
 902   = do  { hsc_env <- getTopEnv
 903         ; let  dfun_name = idName dfun_id
 904                dfun_mod  = ASSERT( isExternalName dfun_name )
 905                            nameModule dfun_name
 906         ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 907              modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 908           then return () -- internal, or in another package
 909            else do { tcg_env <- getGblEnv
 910                    ; updMutVar (tcg_inst_uses tcg_env)
 911                                (`addOneToNameSet` idName dfun_id) }}
 912
 913
 914 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
 915 -- Gets both the external-package inst-env
 916 -- and the home-pkg inst env (includes module being compiled)
 917 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
 918                      return (eps_inst_env eps, tcg_inst_env env) }
 919 \end{code}
 920
 921
 922
 923 %************************************************************************
 924 %*                                                                      *
 925                 Re-mappable syntax
 926 %*                                                                      *
 927 %************************************************************************
 928
 929 Suppose we are doing the -XNoImplicitPrelude thing, and we encounter
 930 a do-expression.  We have to find (>>) in the current environment, which is
 931 done by the rename. Then we have to check that it has the same type as
 932 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
 933 this:
 934
 935   (>>) :: HB m n mn => m a -> n b -> mn b
 936
 937 So the idea is to generate a local binding for (>>), thus:
 938
 939         let then72 :: forall a b. m a -> m b -> m b
 940             then72 = ...something involving the user's (>>)...
 941         in
 942         ...the do-expression...
 943
 944 Now the do-expression can proceed using then72, which has exactly
 945 the expected type.
 946
 947 In fact tcSyntaxName just generates the RHS for then72, because we only
 948 want an actual binding in the do-expression case. For literals, we can
 949 just use the expression inline.
 950
 951 \begin{code}
 952 tcSyntaxName :: InstOrigin
 953              -> TcType                  -- Type to instantiate it at
 954              -> (Name, HsExpr Name)     -- (Standard name, user name)
 955              -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
 956 --      *** NOW USED ONLY FOR CmdTop (sigh) ***
 957 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
 958 -- So we do not call it from lookupInst, which is called from tcSimplify
 959
 960 tcSyntaxName orig ty (std_nm, HsVar user_nm)
 961   | std_nm == user_nm
 962   = do id <- newMethodFromName orig ty std_nm
 963        return (std_nm, HsVar id)
 964
 965 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
 966     std_id <- tcLookupId std_nm
 967     let
 968         -- C.f. newMethodAtLoc
 969         ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
 970         sigma1          = substTyWith [tv] [ty] tau
 971         -- Actually, the "tau-type" might be a sigma-type in the
 972         -- case of locally-polymorphic methods.
 973
 974     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
 975
 976         -- Check that the user-supplied thing has the
 977         -- same type as the standard one.
 978         -- Tiresome jiggling because tcCheckSigma takes a located expression
 979      span <- getSrcSpanM
 980      expr <- tcPolyExpr (L span user_nm_expr) sigma1
 981      return (std_nm, unLoc expr)
 982
 983 syntaxNameCtxt :: HsExpr Name -> InstOrigin -> Type -> TidyEnv
 984                -> TcRn (TidyEnv, SDoc)
 985 syntaxNameCtxt name orig ty tidy_env = do
 986     inst_loc <- getInstLoc orig
 987     let
 988         msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
 989                                 ptext (sLit "(needed by a syntactic construct)"),
 990                     nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
 991                     nest 2 (ptext (sLit "arising from") <+> pprInstLoc inst_loc)]
 992
 993     return (tidy_env, msg)
 994 \end{code}
 995
 996 %************************************************************************
 997 %*                                                                      *
 998                 EqInsts
 999 %*                                                                      *
1000 %************************************************************************
1001
1002 Operations on EqInstCo.
1003
1004 \begin{code}
1005 mkGivenCo   :: Coercion -> EqInstCo
1006 mkGivenCo   =  Right
1007
1008 mkWantedCo  :: TcTyVar  -> EqInstCo
1009 mkWantedCo  =  Left
1010
1011 isWantedCo :: EqInstCo -> Bool
1012 isWantedCo (Left _) = True
1013 isWantedCo _        = False
1014
1015 eqInstCoType :: EqInstCo -> TcType
1016 eqInstCoType (Left cotv) = mkTyVarTy cotv
1017 eqInstCoType (Right co)  = co
1018 \end{code}
1019
1020 Coercion transformations on EqInstCo.  These transformations work differently
1021 depending on whether a EqInstCo is for a wanted or local equality:
1022
1023   Local : apply the inverse of the specified coercion
1024   Wanted: obtain a fresh coercion hole (meta tyvar) and update the old hole
1025           to be the specified coercion applied to the new coercion hole
1026
1027 \begin{code}
1028 -- Coercion transformation: co = id
1029 --
1030 mkIdEqInstCo :: EqInstCo -> Type -> TcM ()
1031 mkIdEqInstCo (Left cotv) t
1032   = writeMetaTyVar cotv t
1033 mkIdEqInstCo (Right _) _
1034   = return ()
1035
1036 -- Coercion transformation: co = sym co'
1037 --
1038 mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo
1039 mkSymEqInstCo (Left cotv) (ty1, ty2)
1040   = do { cotv' <- newMetaCoVar ty1 ty2
1041        ; writeMetaTyVar cotv (mkSymCoercion (TyVarTy cotv'))
1042        ; return $ Left cotv'
1043        }
1044 mkSymEqInstCo (Right co) _
1045   = return $ Right (mkSymCoercion co)
1046
1047 -- Coercion transformation: co = co' |> given_co
1048 --
1049 mkLeftTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
1050 mkLeftTransEqInstCo (Left cotv) given_co (ty1, ty2)
1051   = do { cotv' <- newMetaCoVar ty1 ty2
1052        ; writeMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co)
1053        ; return $ Left cotv'
1054        }
1055 mkLeftTransEqInstCo (Right co) given_co _
1056   = return $ Right (co `mkTransCoercion` mkSymCoercion given_co)
1057
1058 -- Coercion transformation: co = given_co |> co'
1059 --
1060 mkRightTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
1061 mkRightTransEqInstCo (Left cotv) given_co (ty1, ty2)
1062   = do { cotv' <- newMetaCoVar ty1 ty2
1063        ; writeMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv')
1064        ; return $ Left cotv'
1065        }
1066 mkRightTransEqInstCo (Right co) given_co _
1067   = return $ Right (mkSymCoercion given_co `mkTransCoercion` co)
1068
1069 -- Coercion transformation: co = col cor
1070 --
1071 mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
1072               -> TcM (EqInstCo, EqInstCo)
1073 mkAppEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
1074   = do { cotv_l <- newMetaCoVar ty1_l ty2_l
1075        ; cotv_r <- newMetaCoVar ty1_r ty2_r
1076        ; writeMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
1077        ; return (Left cotv_l, Left cotv_r)
1078        }
1079 mkAppEqInstCo (Right co) _ _
1080   = return (Right $ mkLeftCoercion co, Right $ mkRightCoercion co)
1081
1082 -- Coercion transformation: co = con col -> cor
1083 --
1084 mkTyConEqInstCo :: EqInstCo -> TyCon -> [(Type, Type)] -> TcM ([EqInstCo])
1085 mkTyConEqInstCo (Left cotv) con ty12s
1086   = do { cotvs <- mapM (uncurry newMetaCoVar) ty12s
1087        ; writeMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs))
1088        ; return (map Left cotvs)
1089        }
1090 mkTyConEqInstCo (Right co) _ args
1091   = return $ map (\mkCoes -> Right $ foldl (.) id mkCoes co) mkCoes
1092     -- make cascades of the form
1093     --   mkRightCoercion (mkLeftCoercion .. (mkLeftCoercion co)..)
1094   where
1095     n      = length args
1096     mkCoes = [mkRightCoercion : replicate i mkLeftCoercion | i <- [n-1, n-2..0]]
1097
1098 -- Coercion transformation: co = col -> cor
1099 --
1100 mkFunEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
1101               -> TcM (EqInstCo, EqInstCo)
1102 mkFunEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
1103   = do { cotv_l <- newMetaCoVar ty1_l ty2_l
1104        ; cotv_r <- newMetaCoVar ty1_r ty2_r
1105        ; writeMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
1106        ; return (Left cotv_l, Left cotv_r)
1107        }
1108 mkFunEqInstCo (Right co) _ _
1109   = return (Right $ mkRightCoercion (mkLeftCoercion co),
1110             Right $ mkRightCoercion co)
1111 \end{code}
1112
1113 Operations on entire EqInst.
1114
1115 \begin{code}
1116 -- |A wanted equality is unsolved as long as its cotv is unfilled.
1117 --
1118 wantedEqInstIsUnsolved :: Inst -> TcM Bool
1119 wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv})
1120   = liftM not $ isFilledMetaTyVar cotv
1121 wantedEqInstIsUnsolved _ = return True
1122
1123 eitherEqInst :: Inst                -- given or wanted EqInst
1124              -> (TcTyVar  -> a)     --  result if wanted
1125              -> (Coercion -> a)     --  result if given
1126              -> a
1127 eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
1128         = case either_co of
1129                 Left  covar -> withWanted covar
1130                 Right co    -> withGiven  co
1131 eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
1132
1133 mkEqInst :: PredType -> EqInstCo -> TcM Inst
1134 mkEqInst (EqPred ty1 ty2) co
1135         = do { uniq <- newUnique
1136              ; src_span <- getSrcSpanM
1137              ; err_ctxt <- getErrCtxt
1138              ; let loc  = InstLoc EqOrigin src_span err_ctxt
1139                    name = mkName uniq src_span
1140                    inst = EqInst { tci_left = ty1
1141                                  , tci_right = ty2
1142                                  , tci_co = co
1143                                  , tci_loc = loc
1144                                  , tci_name = name
1145                                  }
1146              ; return inst
1147              }
1148         where
1149           mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
1150 mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred)
1151
1152 mkWantedEqInst :: PredType -> TcM Inst
1153 mkWantedEqInst pred@(EqPred ty1 ty2)
1154   = do { cotv <- newMetaCoVar ty1 ty2
1155        ; mkEqInst pred (Left cotv)
1156        }
1157 mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred)
1158
1159 -- Turn a wanted equality into a local that propagates the uninstantiated
1160 -- coercion variable as witness.  We need this to propagate wanted irreds into
1161 -- attempts to solve implication constraints.
1162 --
1163 wantedToLocalEqInst :: Inst -> Inst
1164 wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv})
1165   = eq {tci_co = Right (mkTyVarTy cotv)}
1166 wantedToLocalEqInst eq = eq
1167
1168 -- Turn a wanted into a local EqInst (needed during type inference for
1169 -- signatures)
1170 --
1171 -- * Give it a name and change the coercion around.
1172 --
1173 finalizeEqInst :: Inst                  -- wanted
1174                -> TcM Inst              -- given
1175 finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2,
1176                               tci_name = name, tci_co = Left cotv})
1177   = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
1178
1179          -- fill the coercion hole
1180        ; writeMetaTyVar cotv (TyVarTy var)
1181
1182          -- set the new coercion
1183        ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
1184        ; return given
1185        }
1186
1187 finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i)
1188
1189 eqInstType :: Inst -> TcType
1190 eqInstType inst = eitherEqInst inst mkTyVarTy id
1191
1192 eqInstCoercion :: Inst -> EqInstCo
1193 eqInstCoercion = tci_co
1194
1195 eqInstTys :: Inst -> (TcType, TcType)
1196 eqInstTys inst = (tci_left inst, tci_right inst)
1197 \end{code}