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