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, 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
  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
 574 isHsVar :: HsExpr Name -> Name -> Bool
 575 isHsVar (HsVar f) g = f == g
 576 isHsVar _         _ = False
 577 \end{code}
 578
 579
 580 %************************************************************************
 581 %*                                                                      *
 582 \subsection{Zonking}
 583 %*                                                                      *
 584 %************************************************************************
 585
 586 Zonking makes sure that the instance types are fully zonked.
 587
 588 \begin{code}
 589 zonkInst :: Inst -> TcM Inst
 590 zonkInst dict@(Dict {tci_pred = pred}) = do
 591     new_pred <- zonkTcPredType pred
 592     return (dict {tci_pred = new_pred})
 593
 594 zonkInst meth@(Method {tci_oid = id, tci_tys = tys, tci_theta = theta}) = do
 595     new_id <- zonkId id
 596         -- Essential to zonk the id in case it's a local variable
 597         -- Can't use zonkIdOcc because the id might itself be
 598         -- an InstId, in which case it won't be in scope
 599
 600     new_tys <- zonkTcTypes tys
 601     new_theta <- zonkTcThetaType theta
 602     return (meth { tci_oid = new_id, tci_tys = new_tys, tci_theta = new_theta })
 603         -- No need to zonk the tci_id
 604
 605 zonkInst lit@(LitInst {tci_ty = ty}) = do
 606     new_ty <- zonkTcType ty
 607     return (lit {tci_ty = new_ty})
 608
 609 zonkInst implic@(ImplicInst {})
 610   = ASSERT( all isImmutableTyVar (tci_tyvars implic) )
 611     do  { givens'  <- zonkInsts (tci_given  implic)
 612         ; wanteds' <- zonkInsts (tci_wanted implic)
 613         ; return (implic {tci_given = givens',tci_wanted = wanteds'}) }
 614
 615 zonkInst eqinst@(EqInst {tci_left = ty1, tci_right = ty2})
 616   = do { co' <- eitherEqInst eqinst
 617                   (\covar -> return (mkWantedCo covar))
 618                   (\co    -> liftM mkGivenCo $ zonkTcType co)
 619        ; ty1' <- zonkTcType ty1
 620        ; ty2' <- zonkTcType ty2
 621        ; return (eqinst {tci_co = co', tci_left = ty1', tci_right = ty2' })
 622        }
 623
 624 zonkInsts :: [Inst] -> TcRn [Inst]
 625 zonkInsts insts = mapM zonkInst insts
 626 \end{code}
 627
 628
 629 %************************************************************************
 630 %*                                                                      *
 631 \subsection{Printing}
 632 %*                                                                      *
 633 %************************************************************************
 634
 635 ToDo: improve these pretty-printing things.  The ``origin'' is really only
 636 relevant in error messages.
 637
 638 \begin{code}
 639 instance Outputable Inst where
 640     ppr inst = pprInst inst
 641
 642 pprDictsTheta :: [Inst] -> SDoc
 643 -- Print in type-like fashion (Eq a, Show b)
 644 -- The Inst can be an implication constraint, but not a Method or LitInst
 645 pprDictsTheta insts = parens (sep (punctuate comma (map (ppr . instType) insts)))
 646
 647 pprDictsInFull :: [Inst] -> SDoc
 648 -- Print in type-like fashion, but with source location
 649 pprDictsInFull dicts
 650   = vcat (map go dicts)
 651   where
 652     go dict = sep [quotes (ppr (instType dict)), nest 2 (pprInstArising dict)]
 653
 654 pprInsts :: [Inst] -> SDoc
 655 -- Debugging: print the evidence :: type
 656 pprInsts insts = brackets (interpp'SP insts)
 657
 658 pprInst, pprInstInFull :: Inst -> SDoc
 659 -- Debugging: print the evidence :: type
 660 pprInst i@(EqInst {tci_left = ty1, tci_right = ty2})
 661         = eitherEqInst i
 662                 (\covar -> text "Wanted" <+> ppr (TyVarTy covar) <+> dcolon <+> ppr (EqPred ty1 ty2))
 663                 (\co    -> text "Given"  <+> ppr co              <+> dcolon <+> ppr (EqPred ty1 ty2))
 664 pprInst inst = ppr name <> braces (pprUnique (getUnique name)) <+> dcolon
 665                 <+> braces (ppr (instType inst) <> implicWantedEqs)
 666   where
 667     name = instName inst
 668     implicWantedEqs
 669       | isImplicInst inst = text " &" <+>
 670                             ppr (filter isEqInst (tci_wanted inst))
 671       | otherwise         = empty
 672
 673 pprInstInFull inst@(EqInst {}) = pprInst inst
 674 pprInstInFull inst = sep [quotes (pprInst inst), nest 2 (pprInstArising inst)]
 675
 676 tidyInst :: TidyEnv -> Inst -> Inst
 677 tidyInst env eq@(EqInst {tci_left = lty, tci_right = rty, tci_co = co}) =
 678   eq { tci_left  = tidyType env lty
 679      , tci_right = tidyType env rty
 680      , tci_co    = either Left (Right . tidyType env) co
 681      }
 682 tidyInst env lit@(LitInst {tci_ty = ty})   = lit {tci_ty = tidyType env ty}
 683 tidyInst env dict@(Dict {tci_pred = pred}) = dict {tci_pred = tidyPred env pred}
 684 tidyInst env meth@(Method {tci_tys = tys}) = meth {tci_tys = tidyTypes env tys}
 685 tidyInst env implic@(ImplicInst {})
 686   = implic { tci_tyvars = tvs'
 687            , tci_given  = map (tidyInst env') (tci_given  implic)
 688            , tci_wanted = map (tidyInst env') (tci_wanted implic) }
 689   where
 690     (env', tvs') = mapAccumL tidyTyVarBndr env (tci_tyvars implic)
 691
 692 tidyMoreInsts :: TidyEnv -> [Inst] -> (TidyEnv, [Inst])
 693 -- This function doesn't assume that the tyvars are in scope
 694 -- so it works like tidyOpenType, returning a TidyEnv
 695 tidyMoreInsts env insts
 696   = (env', map (tidyInst env') insts)
 697   where
 698     env' = tidyFreeTyVars env (tyVarsOfInsts insts)
 699
 700 tidyInsts :: [Inst] -> (TidyEnv, [Inst])
 701 tidyInsts insts = tidyMoreInsts emptyTidyEnv insts
 702
 703 showLIE :: SDoc -> TcM ()       -- Debugging
 704 showLIE str
 705   = do { lie_var <- getLIEVar ;
 706          lie <- readMutVar lie_var ;
 707          traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) }
 708 \end{code}
 709
 710
 711 %************************************************************************
 712 %*                                                                      *
 713         Extending the instance environment
 714 %*                                                                      *
 715 %************************************************************************
 716
 717 \begin{code}
 718 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
 719   -- Add new locally-defined instances
 720 tcExtendLocalInstEnv dfuns thing_inside
 721  = do { traceDFuns dfuns
 722       ; env <- getGblEnv
 723       ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
 724       ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
 725                          tcg_inst_env = inst_env' }
 726       ; setGblEnv env' thing_inside }
 727
 728 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
 729 -- Check that the proposed new instance is OK,
 730 -- and then add it to the home inst env
 731 addLocalInst home_ie ispec
 732   = do  {       -- Instantiate the dfun type so that we extend the instance
 733                 -- envt with completely fresh template variables
 734                 -- This is important because the template variables must
 735                 -- not overlap with anything in the things being looked up
 736                 -- (since we do unification).
 737                 -- We use tcInstSkolType because we don't want to allocate fresh
 738                 --  *meta* type variables.
 739           let dfun = instanceDFunId ispec
 740         ; (tvs', theta', tau') <- tcInstSkolType InstSkol (idType dfun)
 741         ; let   (cls, tys') = tcSplitDFunHead tau'
 742                 dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')
 743                 ispec'      = setInstanceDFunId ispec dfun'
 744
 745                 -- Load imported instances, so that we report
 746                 -- duplicates correctly
 747         ; eps <- getEps
 748         ; let inst_envs = (eps_inst_env eps, home_ie)
 749
 750                 -- Check functional dependencies
 751         ; case checkFunDeps inst_envs ispec' of
 752                 Just specs -> funDepErr ispec' specs
 753                 Nothing    -> return ()
 754
 755                 -- Check for duplicate instance decls
 756         ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
 757               ; dup_ispecs = [ dup_ispec
 758                              | (dup_ispec, _) <- matches
 759                              , let (_,_,_,dup_tys) = instanceHead dup_ispec
 760                              , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
 761                 -- Find memebers of the match list which ispec itself matches.
 762                 -- If the match is 2-way, it's a duplicate
 763         ; case dup_ispecs of
 764             dup_ispec : _ -> dupInstErr ispec' dup_ispec
 765             []            -> return ()
 766
 767                 -- OK, now extend the envt
 768         ; return (extendInstEnv home_ie ispec') }
 769
 770 getOverlapFlag :: TcM OverlapFlag
 771 getOverlapFlag
 772   = do  { dflags <- getDOpts
 773         ; let overlap_ok    = dopt Opt_OverlappingInstances dflags
 774               incoherent_ok = dopt Opt_IncoherentInstances  dflags
 775               overlap_flag | incoherent_ok = Incoherent
 776                            | overlap_ok    = OverlapOk
 777                            | otherwise     = NoOverlap
 778
 779         ; return overlap_flag }
 780
 781 traceDFuns :: [Instance] -> TcRn ()
 782 traceDFuns ispecs
 783   = traceTc (hang (text "Adding instances:") 2 (vcat (map pp ispecs)))
 784   where
 785     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
 786         -- Print the dfun name itself too
 787
 788 funDepErr :: Instance -> [Instance] -> TcRn ()
 789 funDepErr ispec ispecs
 790   = addDictLoc ispec $
 791     addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
 792                2 (pprInstances (ispec:ispecs)))
 793 dupInstErr :: Instance -> Instance -> TcRn ()
 794 dupInstErr ispec dup_ispec
 795   = addDictLoc ispec $
 796     addErr (hang (ptext (sLit "Duplicate instance declarations:"))
 797                2 (pprInstances [ispec, dup_ispec]))
 798
 799 addDictLoc :: Instance -> TcRn a -> TcRn a
 800 addDictLoc ispec thing_inside
 801   = setSrcSpan (mkSrcSpan loc loc) thing_inside
 802   where
 803    loc = getSrcLoc ispec
 804 \end{code}
 805
 806
 807 %************************************************************************
 808 %*                                                                      *
 809 \subsection{Looking up Insts}
 810 %*                                                                      *
 811 %************************************************************************
 812
 813 \begin{code}
 814 data LookupInstResult
 815   = NoInstance
 816   | GenInst [Inst] (LHsExpr TcId)       -- The expression and its needed insts
 817
 818 lookupSimpleInst :: Inst -> TcM LookupInstResult
 819 -- This is "simple" in that it returns NoInstance for implication constraints
 820
 821 -- It's important that lookupInst does not put any new stuff into
 822 -- the LIE.  Instead, any Insts needed by the lookup are returned in
 823 -- the LookupInstResult, where they can be further processed by tcSimplify
 824
 825 lookupSimpleInst (EqInst {}) = return NoInstance
 826
 827 --------------------- Implications ------------------------
 828 lookupSimpleInst (ImplicInst {}) = return NoInstance
 829
 830 --------------------- Methods ------------------------
 831 lookupSimpleInst (Method {tci_oid = id, tci_tys = tys, tci_theta = theta, tci_loc = loc})
 832   = do  { (dict_app, dicts) <- getLIE $ instCallDicts loc theta
 833         ; let co_fn = dict_app <.> mkWpTyApps tys
 834         ; return (GenInst dicts (L span $ HsWrap co_fn (HsVar id))) }
 835   where
 836     span = instLocSpan loc
 837
 838 --------------------- Literals ------------------------
 839 -- Look for short cuts first: if the literal is *definitely* a
 840 -- int, integer, float or a double, generate the real thing here.
 841 -- This is essential (see nofib/spectral/nucleic).
 842 -- [Same shortcut as in newOverloadedLit, but we
 843 --  may have done some unification by now]
 844
 845 lookupSimpleInst (LitInst { tci_lit = lit@OverLit { ol_val = lit_val
 846                                                   , ol_rebindable = rebindable }
 847                           , tci_ty = ty, tci_loc = iloc})
 848   | debugIsOn && rebindable = panic "lookupSimpleInst" -- A LitInst invariant
 849   | Just witness <- shortCutLit lit_val ty
 850   = do  { let lit' = lit { ol_witness = witness, ol_type = ty }
 851         ; return (GenInst [] (L loc (HsOverLit lit'))) }
 852
 853   | otherwise
 854   = do  { hs_lit <- mkOverLit lit_val
 855         ; from_thing <- tcLookupId (hsOverLitName lit_val)
 856                   -- Not rebindable, so hsOverLitName is the right thing
 857         ; method_inst <- tcInstClassOp iloc from_thing [ty]
 858         ; let witness = HsApp (L loc (HsVar (instToId method_inst)))
 859                               (L loc (HsLit hs_lit))
 860               lit' = lit { ol_witness = witness, ol_type = ty }
 861         ; return (GenInst [method_inst] (L loc (HsOverLit lit'))) }
 862   where
 863     loc = instLocSpan iloc
 864
 865 --------------------- Dictionaries ------------------------
 866 lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
 867   = do  { mb_result <- lookupPred pred
 868         ; case mb_result of {
 869             Nothing -> return NoInstance ;
 870             Just (dfun_id, mb_inst_tys) -> do
 871
 872     { use_stage <- getStage
 873     ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
 874                       (topIdLvl dfun_id) use_stage
 875
 876         -- It's possible that not all the tyvars are in
 877         -- the substitution, tenv. For example:
 878         --      instance C X a => D X where ...
 879         -- (presumably there's a functional dependency in class C)
 880         -- Hence mb_inst_tys :: Either TyVar TcType
 881
 882     ; let inst_tv (Left tv)  = do { tv' <- tcInstTyVar tv; return (mkTyVarTy tv') }
 883           inst_tv (Right ty) = return ty
 884     ; tys <- mapM inst_tv mb_inst_tys
 885     ; let
 886         (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
 887         src_loc    = instLocSpan loc
 888         dfun       = HsVar dfun_id
 889     ; if null theta then
 890         return (GenInst [] (L src_loc $ HsWrap (mkWpTyApps tys) dfun))
 891       else do
 892     { (dict_app, dicts) <- getLIE $ instCallDicts loc theta -- !!!
 893     ; let co_fn = dict_app <.> mkWpTyApps tys
 894     ; return (GenInst dicts (L src_loc $ HsWrap co_fn dfun))
 895     }}}}
 896
 897 ---------------
 898 lookupPred :: TcPredType -> TcM (Maybe (DFunId, [Either TyVar TcType]))
 899 -- Look up a class constraint in the instance environment
 900 lookupPred pred@(ClassP clas tys)
 901   = do  { eps     <- getEps
 902         ; tcg_env <- getGblEnv
 903         ; let inst_envs = (eps_inst_env eps, tcg_inst_env tcg_env)
 904         ; case lookupInstEnv inst_envs clas tys of {
 905             ([(ispec, inst_tys)], [])
 906                 -> do   { let dfun_id = is_dfun ispec
 907                         ; traceTc (text "lookupInst success" <+>
 908                                    vcat [text "dict" <+> ppr pred,
 909                                          text "witness" <+> ppr dfun_id
 910                                          <+> ppr (idType dfun_id) ])
 911                                 -- Record that this dfun is needed
 912                         ; record_dfun_usage dfun_id
 913                         ; return (Just (dfun_id, inst_tys)) } ;
 914
 915             (matches, unifs)
 916                 -> do   { traceTc (text "lookupInst fail" <+>
 917                                    vcat [text "dict" <+> ppr pred,
 918                                          text "matches" <+> ppr matches,
 919                                          text "unifs" <+> ppr unifs])
 920                 -- In the case of overlap (multiple matches) we report
 921                 -- NoInstance here.  That has the effect of making the
 922                 -- context-simplifier return the dict as an irreducible one.
 923                 -- Then it'll be given to addNoInstanceErrs, which will do another
 924                 -- lookupInstEnv to get the detailed info about what went wrong.
 925                         ; return Nothing }
 926         }}
 927
 928 lookupPred (IParam {}) = return Nothing -- Implicit parameters
 929 lookupPred (EqPred {}) = panic "lookupPred EqPred"
 930
 931 record_dfun_usage :: Id -> TcRn ()
 932 record_dfun_usage dfun_id
 933   = do  { hsc_env <- getTopEnv
 934         ; let  dfun_name = idName dfun_id
 935                dfun_mod  = ASSERT( isExternalName dfun_name )
 936                            nameModule dfun_name
 937         ; if isInternalName dfun_name ||    -- Internal name => defined in this module
 938              modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
 939           then return () -- internal, or in another package
 940            else do { tcg_env <- getGblEnv
 941                    ; updMutVar (tcg_inst_uses tcg_env)
 942                                (`addOneToNameSet` idName dfun_id) }}
 943
 944
 945 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
 946 -- Gets both the external-package inst-env
 947 -- and the home-pkg inst env (includes module being compiled)
 948 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
 949                      return (eps_inst_env eps, tcg_inst_env env) }
 950 \end{code}
 951
 952
 953
 954 %************************************************************************
 955 %*                                                                      *
 956                 Re-mappable syntax
 957 %*                                                                      *
 958 %************************************************************************
 959
 960 Suppose we are doing the -XNoImplicitPrelude thing, and we encounter
 961 a do-expression.  We have to find (>>) in the current environment, which is
 962 done by the rename. Then we have to check that it has the same type as
 963 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
 964 this:
 965
 966   (>>) :: HB m n mn => m a -> n b -> mn b
 967
 968 So the idea is to generate a local binding for (>>), thus:
 969
 970         let then72 :: forall a b. m a -> m b -> m b
 971             then72 = ...something involving the user's (>>)...
 972         in
 973         ...the do-expression...
 974
 975 Now the do-expression can proceed using then72, which has exactly
 976 the expected type.
 977
 978 In fact tcSyntaxName just generates the RHS for then72, because we only
 979 want an actual binding in the do-expression case. For literals, we can
 980 just use the expression inline.
 981
 982 \begin{code}
 983 tcSyntaxName :: InstOrigin
 984              -> TcType                  -- Type to instantiate it at
 985              -> (Name, HsExpr Name)     -- (Standard name, user name)
 986              -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
 987 --      *** NOW USED ONLY FOR CmdTop (sigh) ***
 988 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
 989 -- So we do not call it from lookupInst, which is called from tcSimplify
 990
 991 tcSyntaxName orig ty (std_nm, HsVar user_nm)
 992   | std_nm == user_nm
 993   = do id <- newMethodFromName orig ty std_nm
 994        return (std_nm, HsVar id)
 995
 996 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
 997     std_id <- tcLookupId std_nm
 998     let
 999         -- C.f. newMethodAtLoc
1000         ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
1001         sigma1          = substTyWith [tv] [ty] tau
1002         -- Actually, the "tau-type" might be a sigma-type in the
1003         -- case of locally-polymorphic methods.
1004
1005     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
1006
1007         -- Check that the user-supplied thing has the
1008         -- same type as the standard one.
1009         -- Tiresome jiggling because tcCheckSigma takes a located expression
1010      span <- getSrcSpanM
1011      expr <- tcPolyExpr (L span user_nm_expr) sigma1
1012      return (std_nm, unLoc expr)
1013
1014 syntaxNameCtxt :: HsExpr Name -> InstOrigin -> Type -> TidyEnv
1015                -> TcRn (TidyEnv, SDoc)
1016 syntaxNameCtxt name orig ty tidy_env = do
1017     inst_loc <- getInstLoc orig
1018     let
1019         msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
1020                                 ptext (sLit "(needed by a syntactic construct)"),
1021                     nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
1022                     nest 2 (ptext (sLit "arising from") <+> pprInstLoc inst_loc)]
1023
1024     return (tidy_env, msg)
1025 \end{code}
1026
1027 %************************************************************************
1028 %*                                                                      *
1029                 EqInsts
1030 %*                                                                      *
1031 %************************************************************************
1032
1033 Operations on EqInstCo.
1034
1035 \begin{code}
1036 mkGivenCo   :: Coercion -> EqInstCo
1037 mkGivenCo   =  Right
1038
1039 mkWantedCo  :: TcTyVar  -> EqInstCo
1040 mkWantedCo  =  Left
1041
1042 isWantedCo :: EqInstCo -> Bool
1043 isWantedCo (Left _) = True
1044 isWantedCo _        = False
1045
1046 eqInstCoType :: EqInstCo -> TcType
1047 eqInstCoType (Left cotv) = mkTyVarTy cotv
1048 eqInstCoType (Right co)  = co
1049 \end{code}
1050
1051 Coercion transformations on EqInstCo.  These transformations work differently
1052 depending on whether a EqInstCo is for a wanted or local equality:
1053
1054   Local : apply the inverse of the specified coercion
1055   Wanted: obtain a fresh coercion hole (meta tyvar) and update the old hole
1056           to be the specified coercion applied to the new coercion hole
1057
1058 \begin{code}
1059 -- Coercion transformation: co = id
1060 --
1061 mkIdEqInstCo :: EqInstCo -> Type -> TcM ()
1062 mkIdEqInstCo (Left cotv) t
1063   = bindMetaTyVar cotv t
1064 mkIdEqInstCo (Right _) _
1065   = return ()
1066
1067 -- Coercion transformation: co = sym co'
1068 --
1069 mkSymEqInstCo :: EqInstCo -> (Type, Type) -> TcM EqInstCo
1070 mkSymEqInstCo (Left cotv) (ty1, ty2)
1071   = do { cotv' <- newMetaCoVar ty1 ty2
1072        ; bindMetaTyVar cotv (mkSymCoercion (TyVarTy cotv'))
1073        ; return $ Left cotv'
1074        }
1075 mkSymEqInstCo (Right co) _
1076   = return $ Right (mkSymCoercion co)
1077
1078 -- Coercion transformation: co = co' |> given_co
1079 --
1080 mkLeftTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
1081 mkLeftTransEqInstCo (Left cotv) given_co (ty1, ty2)
1082   = do { cotv' <- newMetaCoVar ty1 ty2
1083        ; bindMetaTyVar cotv (TyVarTy cotv' `mkTransCoercion` given_co)
1084        ; return $ Left cotv'
1085        }
1086 mkLeftTransEqInstCo (Right co) given_co _
1087   = return $ Right (co `mkTransCoercion` mkSymCoercion given_co)
1088
1089 -- Coercion transformation: co = given_co |> co'
1090 --
1091 mkRightTransEqInstCo :: EqInstCo -> Coercion -> (Type, Type) -> TcM EqInstCo
1092 mkRightTransEqInstCo (Left cotv) given_co (ty1, ty2)
1093   = do { cotv' <- newMetaCoVar ty1 ty2
1094        ; bindMetaTyVar cotv (given_co `mkTransCoercion` TyVarTy cotv')
1095        ; return $ Left cotv'
1096        }
1097 mkRightTransEqInstCo (Right co) given_co _
1098   = return $ Right (mkSymCoercion given_co `mkTransCoercion` co)
1099
1100 -- Coercion transformation: co = col cor
1101 --
1102 mkAppEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
1103               -> TcM (EqInstCo, EqInstCo)
1104 mkAppEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
1105   = do { cotv_l <- newMetaCoVar ty1_l ty2_l
1106        ; cotv_r <- newMetaCoVar ty1_r ty2_r
1107        ; bindMetaTyVar cotv (mkAppCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
1108        ; return (Left cotv_l, Left cotv_r)
1109        }
1110 mkAppEqInstCo (Right co) _ _
1111   = return (Right $ mkLeftCoercion co, Right $ mkRightCoercion co)
1112
1113 -- Coercion transformation: co = con col -> cor
1114 --
1115 mkTyConEqInstCo :: EqInstCo -> TyCon -> [(Type, Type)] -> TcM ([EqInstCo])
1116 mkTyConEqInstCo (Left cotv) con ty12s
1117   = do { cotvs <- mapM (uncurry newMetaCoVar) ty12s
1118        ; bindMetaTyVar cotv (mkTyConCoercion con (mkTyVarTys cotvs))
1119        ; return (map Left cotvs)
1120        }
1121 mkTyConEqInstCo (Right co) _ args
1122   = return $ map (\mkCoes -> Right $ foldl (.) id mkCoes co) mkCoes
1123     -- make cascades of the form
1124     --   mkRightCoercion (mkLeftCoercion .. (mkLeftCoercion co)..)
1125   where
1126     n      = length args
1127     mkCoes = [mkRightCoercion : replicate i mkLeftCoercion | i <- [n-1, n-2..0]]
1128
1129 -- Coercion transformation: co = col -> cor
1130 --
1131 mkFunEqInstCo :: EqInstCo -> (Type, Type) -> (Type, Type)
1132               -> TcM (EqInstCo, EqInstCo)
1133 mkFunEqInstCo (Left cotv) (ty1_l, ty2_l) (ty1_r, ty2_r)
1134   = do { cotv_l <- newMetaCoVar ty1_l ty2_l
1135        ; cotv_r <- newMetaCoVar ty1_r ty2_r
1136        ; bindMetaTyVar cotv (mkFunCoercion (TyVarTy cotv_l) (TyVarTy cotv_r))
1137        ; return (Left cotv_l, Left cotv_r)
1138        }
1139 mkFunEqInstCo (Right co) _ _
1140   = return (Right $ mkRightCoercion (mkLeftCoercion co),
1141             Right $ mkRightCoercion co)
1142 \end{code}
1143
1144 Operations on entire EqInst.
1145
1146 \begin{code}
1147 -- |A wanted equality is unsolved as long as its cotv is unfilled.
1148 --
1149 wantedEqInstIsUnsolved :: Inst -> TcM Bool
1150 wantedEqInstIsUnsolved (EqInst {tci_co = Left cotv})
1151   = liftM not $ isFilledMetaTyVar cotv
1152 wantedEqInstIsUnsolved _ = return True
1153
1154 eitherEqInst :: Inst                -- given or wanted EqInst
1155              -> (TcTyVar  -> a)     --  result if wanted
1156              -> (Coercion -> a)     --  result if given
1157              -> a
1158 eitherEqInst (EqInst {tci_co = either_co}) withWanted withGiven
1159         = case either_co of
1160                 Left  covar -> withWanted covar
1161                 Right co    -> withGiven  co
1162 eitherEqInst i _ _ = pprPanic "eitherEqInst" (ppr i)
1163
1164 mkEqInst :: PredType -> EqInstCo -> TcM Inst
1165 mkEqInst (EqPred ty1 ty2) co
1166         = do { uniq <- newUnique
1167              ; src_span <- getSrcSpanM
1168              ; err_ctxt <- getErrCtxt
1169              ; let loc  = InstLoc EqOrigin src_span err_ctxt
1170                    name = mkName uniq src_span
1171                    inst = EqInst { tci_left = ty1
1172                                  , tci_right = ty2
1173                                  , tci_co = co
1174                                  , tci_loc = loc
1175                                  , tci_name = name
1176                                  }
1177              ; return inst
1178              }
1179         where
1180           mkName uniq src_span = mkInternalName uniq (mkVarOcc "co") src_span
1181 mkEqInst pred _ = pprPanic "mkEqInst" (ppr pred)
1182
1183 mkWantedEqInst :: PredType -> TcM Inst
1184 mkWantedEqInst pred@(EqPred ty1 ty2)
1185   = do { cotv <- newMetaCoVar ty1 ty2
1186        ; mkEqInst pred (Left cotv)
1187        }
1188 mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred)
1189
1190 -- Turn a wanted equality into a local that propagates the uninstantiated
1191 -- coercion variable as witness.  We need this to propagate wanted irreds into
1192 -- attempts to solve implication constraints.
1193 --
1194 wantedToLocalEqInst :: Inst -> Inst
1195 wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv})
1196   = eq {tci_co = Right (mkTyVarTy cotv)}
1197 wantedToLocalEqInst eq = eq
1198
1199 -- Turn a wanted into a local EqInst (needed during type inference for
1200 -- signatures)
1201 --
1202 -- * Give it a name and change the coercion around.
1203 --
1204 finalizeEqInst :: Inst                  -- wanted
1205                -> TcM Inst              -- given
1206 finalizeEqInst wanted@(EqInst{tci_left = ty1, tci_right = ty2,
1207                               tci_name = name, tci_co = Left cotv})
1208   = do { let var = Var.mkCoVar name (PredTy $ EqPred ty1 ty2)
1209
1210          -- fill the coercion hole
1211        ; writeMetaTyVar cotv (TyVarTy var)
1212
1213          -- set the new coercion
1214        ; let given = wanted { tci_co = mkGivenCo $ TyVarTy var }
1215        ; return given
1216        }
1217
1218 finalizeEqInst i = pprPanic "finalizeEqInst" (ppr i)
1219
1220 eqInstType :: Inst -> TcType
1221 eqInstType inst = eitherEqInst inst mkTyVarTy id
1222
1223 eqInstCoercion :: Inst -> EqInstCo
1224 eqInstCoercion = tci_co
1225
1226 eqInstTys :: Inst -> (TcType, TcType)
1227 eqInstTys inst = (tci_left inst, tci_right inst)
1228 \end{code}