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