compiler/typecheck/TcSMonad.lhs

   1 \begin{code}
   2 -- Type definitions for the constraint solver
   3 module TcSMonad (
   4
   5        -- Canonical constraints
   6     CanonicalCts, emptyCCan, andCCan, andCCans,
   7     singleCCan, extendCCans, isEmptyCCan, isCTyEqCan,
   8     isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
   9     isCFrozenErr,
  10
  11     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
  12     deCanonicalise, mkFrozenError,
  13     makeSolvedByInst,
  14
  15     isWanted, isGiven, isDerived,
  16     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
  17
  18     isFlexiTcsTv,
  19
  20     canRewrite, canSolve,
  21     combineCtLoc, mkGivenFlavor, mkWantedFlavor,
  22     getWantedLoc,
  23
  24     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality
  25     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
  26     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
  27
  28        -- Creation of evidence variables
  29     newEvVar, newCoVar, newWantedCoVar, newGivenCoVar,
  30     newDerivedId,
  31     newIPVar, newDictVar, newKindConstraint,
  32
  33        -- Setting evidence variables
  34     setWantedCoBind,
  35     setIPBind, setDictBind, setEvBind,
  36
  37     setWantedTyBind,
  38
  39     getInstEnvs, getFamInstEnvs,                -- Getting the environments
  40     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
  41     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
  42
  43     newFlattenSkolemTy,                         -- Flatten skolems
  44
  45
  46     instDFunTypes,                              -- Instantiation
  47     instDFunConstraints,
  48     newFlexiTcSTy,
  49
  50     compatKind,
  51
  52     TcsUntouchables,
  53     isTouchableMetaTyVar,
  54     isTouchableMetaTyVar_InRange,
  55
  56     getDefaultInfo, getDynFlags,
  57
  58     matchClass, matchFam, MatchInstResult (..),
  59     checkWellStagedDFun,
  60     warnTcS,
  61     pprEq,                                   -- Smaller utils, re-exported from TcM
  62                                              -- TODO (DV): these are only really used in the
  63                                              -- instance matcher in TcSimplify. I am wondering
  64                                              -- if the whole instance matcher simply belongs
  65                                              -- here
  66
  67
  68     mkDerivedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
  69
  70 ) where
  71
  72 #include "HsVersions.h"
  73
  74 import HscTypes
  75 import BasicTypes
  76
  77 import Inst
  78 import InstEnv
  79 import FamInst
  80 import FamInstEnv
  81
  82 import qualified TcRnMonad as TcM
  83 import qualified TcMType as TcM
  84 import qualified TcEnv as TcM
  85        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
  86 import TcType
  87 import DynFlags
  88
  89 import Coercion
  90 import Class
  91 import TyCon
  92 import TypeRep
  93
  94 import Name
  95 import Var
  96 import VarEnv
  97 import Outputable
  98 import Bag
  99 import MonadUtils
 100 import VarSet
 101 import FastString
 102
 103 import HsBinds               -- for TcEvBinds stuff
 104 import Id
 105 import FunDeps
 106
 107 import TcRnTypes
 108
 109 import Control.Monad
 110 import Data.IORef
 111 \end{code}
 112
 113
 114 %************************************************************************
 115 %*                                                                      *
 116 %*                       Canonical constraints                          *
 117 %*                                                                      *
 118 %*   These are the constraints the low-level simplifier works with      *
 119 %*                                                                      *
 120 %************************************************************************
 121
 122 \begin{code}
 123 -- Types without any type functions inside.  However, note that xi
 124 -- types CAN contain unexpanded type synonyms; however, the
 125 -- (transitive) expansions of those type synonyms will not contain any
 126 -- type functions.
 127 type Xi = Type       -- In many comments, "xi" ranges over Xi
 128
 129 type CanonicalCts = Bag CanonicalCt
 130
 131 data CanonicalCt
 132   -- Atomic canonical constraints
 133   = CDictCan {  -- e.g.  Num xi
 134       cc_id     :: EvVar,
 135       cc_flavor :: CtFlavor,
 136       cc_class  :: Class,
 137       cc_tyargs :: [Xi]
 138     }
 139
 140   | CIPCan {    -- ?x::tau
 141       -- See note [Canonical implicit parameter constraints].
 142       cc_id     :: EvVar,
 143       cc_flavor :: CtFlavor,
 144       cc_ip_nm  :: IPName Name,
 145       cc_ip_ty  :: TcTauType
 146     }
 147
 148   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
 149        -- Invariant:
 150        --   * tv not in tvs(xi)   (occurs check)
 151        --   * typeKind xi `compatKind` typeKind tv
 152        --       See Note [Spontaneous solving and kind compatibility]
 153        --   * We prefer unification variables on the left *JUST* for efficiency
 154       cc_id     :: EvVar,
 155       cc_flavor :: CtFlavor,
 156       cc_tyvar  :: TcTyVar,
 157       cc_rhs    :: Xi
 158     }
 159
 160   | CFunEqCan {  -- F xis ~ xi
 161                  -- Invariant: * isSynFamilyTyCon cc_fun
 162                  --            * typeKind (F xis) `compatKind` typeKind xi
 163       cc_id     :: EvVar,
 164       cc_flavor :: CtFlavor,
 165       cc_fun    :: TyCon,       -- A type function
 166       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
 167       cc_rhs    :: Xi           --    *never* over-saturated (because if so
 168                                 --    we should have decomposed)
 169
 170     }
 171
 172   | CFrozenErr {      -- A "frozen error" does not interact with anything
 173                       -- See Note [Frozen Errors]
 174       cc_id     :: EvVar,
 175       cc_flavor :: CtFlavor
 176     }
 177
 178 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
 179 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
 180
 181 compatKind :: Kind -> Kind -> Bool
 182 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
 183
 184 makeSolvedByInst :: CanonicalCt -> CanonicalCt
 185 -- Record that a constraint is now solved
 186 --        Wanted         -> Given
 187 --        Given, Derived -> no-op
 188 makeSolvedByInst ct
 189   | Wanted loc <- cc_flavor ct
 190   = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
 191   | otherwise      -- Only called on wanteds
 192   = pprPanic "makeSolvedByInst" (ppr ct)
 193
 194 deCanonicalise :: CanonicalCt -> FlavoredEvVar
 195 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
 196
 197 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
 198 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
 199 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
 200 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
 201 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
 202 tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
 203
 204 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
 205 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
 206 tyVarsOfCDict _ct                            = emptyVarSet
 207
 208 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
 209 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
 210
 211 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
 212 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
 213
 214 instance Outputable CanonicalCt where
 215   ppr (CDictCan d fl cls tys)
 216       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
 217   ppr (CIPCan ip fl ip_nm ty)
 218       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
 219   ppr (CTyEqCan co fl tv ty)
 220       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
 221   ppr (CFunEqCan co fl tc tys ty)
 222       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
 223   ppr (CFrozenErr co fl)
 224       = ppr fl <+> pprEvVarWithType co
 225 \end{code}
 226
 227 Note [Canonical implicit parameter constraints]
 228 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 229 The type in a canonical implicit parameter constraint doesn't need to
 230 be a xi (type-function-free type) since we can defer the flattening
 231 until checking this type for equality with another type.  If we
 232 encounter two IP constraints with the same name, they MUST have the
 233 same type, and at that point we can generate a flattened equality
 234 constraint between the types.  (On the other hand, the types in two
 235 class constraints for the same class MAY be equal, so they need to be
 236 flattened in the first place to facilitate comparing them.)
 237
 238 \begin{code}
 239 singleCCan :: CanonicalCt -> CanonicalCts
 240 singleCCan = unitBag
 241
 242 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
 243 andCCan = unionBags
 244
 245 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
 246 extendCCans = snocBag
 247
 248 andCCans :: [CanonicalCts] -> CanonicalCts
 249 andCCans = unionManyBags
 250
 251 emptyCCan :: CanonicalCts
 252 emptyCCan = emptyBag
 253
 254 isEmptyCCan :: CanonicalCts -> Bool
 255 isEmptyCCan = isEmptyBag
 256
 257 isCTyEqCan :: CanonicalCt -> Bool
 258 isCTyEqCan (CTyEqCan {})  = True
 259 isCTyEqCan (CFunEqCan {}) = False
 260 isCTyEqCan _              = False
 261
 262 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
 263 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
 264 isCDictCan_Maybe _              = Nothing
 265
 266 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
 267 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
 268 isCIPCan_Maybe _                = Nothing
 269
 270 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
 271 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
 272 isCFunEqCan_Maybe _ = Nothing
 273
 274 isCFrozenErr :: CanonicalCt -> Bool
 275 isCFrozenErr (CFrozenErr {}) = True
 276 isCFrozenErr _               = False
 277 \end{code}
 278
 279 %************************************************************************
 280 %*                                                                      *
 281                     CtFlavor
 282          The "flavor" of a canonical constraint
 283 %*                                                                      *
 284 %************************************************************************
 285
 286 \begin{code}
 287 getWantedLoc :: CanonicalCt -> WantedLoc
 288 getWantedLoc ct
 289   = ASSERT (isWanted (cc_flavor ct))
 290     case cc_flavor ct of
 291       Wanted wl -> wl
 292       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
 293
 294 isWantedCt :: CanonicalCt -> Bool
 295 isWantedCt ct = isWanted (cc_flavor ct)
 296 isGivenCt :: CanonicalCt -> Bool
 297 isGivenCt ct = isGiven (cc_flavor ct)
 298 isDerivedCt :: CanonicalCt -> Bool
 299 isDerivedCt ct = isDerived (cc_flavor ct)
 300
 301 canSolve :: CtFlavor -> CtFlavor -> Bool
 302 -- canSolve ctid1 ctid2
 303 -- The constraint ctid1 can be used to solve ctid2
 304 -- "to solve" means a reaction where the active parts of the two constraints match.
 305 --  active(F xis ~ xi) = F xis
 306 --  active(tv ~ xi)    = tv
 307 --  active(D xis)      = D xis
 308 --  active(IP nm ty)   = nm
 309 -----------------------------------------
 310 canSolve (Given {})   _            = True
 311 canSolve (Derived {}) (Wanted {})  = False -- DV: changing the semantics
 312 canSolve (Derived {}) (Derived {}) = True  -- DV: changing the semantics of derived
 313 canSolve (Wanted {})  (Wanted {})  = True
 314 canSolve _ _ = False
 315
 316 canRewrite :: CtFlavor -> CtFlavor -> Bool
 317 -- canRewrite ctid1 ctid2
 318 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
 319 canRewrite = canSolve
 320
 321 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
 322 -- Precondition: At least one of them should be wanted
 323 combineCtLoc (Wanted loc) _    = loc
 324 combineCtLoc _ (Wanted loc)    = loc
 325 combineCtLoc (Derived loc ) _  = loc
 326 combineCtLoc _ (Derived loc )  = loc
 327 combineCtLoc _ _ = panic "combineCtLoc: both given"
 328
 329 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 330 mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
 331 mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
 332 mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
 333
 334 mkWantedFlavor :: CtFlavor -> CtFlavor
 335 mkWantedFlavor (Wanted  loc) = Wanted loc
 336 mkWantedFlavor (Derived loc) = Wanted loc
 337 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
 338 \end{code}
 339
 340 %************************************************************************
 341 %*                                                                      *
 342 %*              The TcS solver monad                                    *
 343 %*                                                                      *
 344 %************************************************************************
 345
 346 Note [The TcS monad]
 347 ~~~~~~~~~~~~~~~~~~~~
 348 The TcS monad is a weak form of the main Tc monad
 349
 350 All you can do is
 351     * fail
 352     * allocate new variables
 353     * fill in evidence variables
 354
 355 Filling in a dictionary evidence variable means to create a binding
 356 for it, so TcS carries a mutable location where the binding can be
 357 added.  This is initialised from the innermost implication constraint.
 358
 359 \begin{code}
 360 data TcSEnv
 361   = TcSEnv {
 362       tcs_ev_binds :: EvBindsVar,
 363           -- Evidence bindings
 364
 365       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
 366           -- Global type bindings
 367
 368       tcs_context :: SimplContext,
 369
 370       tcs_untch :: TcsUntouchables
 371     }
 372
 373 type TcsUntouchables = (Untouchables,TcTyVarSet)
 374 -- Like the TcM Untouchables,
 375 -- but records extra TcsTv variables generated during simplification
 376 -- See Note [Extra TcsTv untouchables] in TcSimplify
 377 \end{code}
 378
 379 \begin{code}
 380 data SimplContext
 381   = SimplInfer          -- Inferring type of a let-bound thing
 382   | SimplRuleLhs        -- Inferring type of a RULE lhs
 383   | SimplInteractive    -- Inferring type at GHCi prompt
 384   | SimplCheck          -- Checking a type signature or RULE rhs
 385   deriving Eq
 386
 387 instance Outputable SimplContext where
 388   ppr SimplInfer       = ptext (sLit "SimplInfer")
 389   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
 390   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 391   ppr SimplCheck       = ptext (sLit "SimplCheck")
 392
 393 isInteractive :: SimplContext -> Bool
 394 isInteractive SimplInteractive = True
 395 isInteractive _                = False
 396
 397 simplEqsOnly :: SimplContext -> Bool
 398 -- Simplify equalities only, not dictionaries
 399 -- This is used for the LHS of rules; ee
 400 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 401 simplEqsOnly SimplRuleLhs = True
 402 simplEqsOnly _            = False
 403
 404 performDefaulting :: SimplContext -> Bool
 405 performDefaulting SimplInfer       = False
 406 performDefaulting SimplRuleLhs     = False
 407 performDefaulting SimplInteractive = True
 408 performDefaulting SimplCheck       = True
 409
 410 ---------------
 411 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 412
 413 instance Functor TcS where
 414   fmap f m = TcS $ fmap f . unTcS m
 415
 416 instance Monad TcS where
 417   return x  = TcS (\_ -> return x)
 418   fail err  = TcS (\_ -> fail err)
 419   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 420
 421 -- Basic functionality
 422 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 423 wrapTcS :: TcM a -> TcS a
 424 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 425 -- and TcS is supposed to have limited functionality
 426 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 427
 428 wrapErrTcS :: TcM a -> TcS a
 429 -- The thing wrapped should just fail
 430 -- There's no static check; it's up to the user
 431 -- Having a variant for each error message is too painful
 432 wrapErrTcS = wrapTcS
 433
 434 wrapWarnTcS :: TcM a -> TcS a
 435 -- The thing wrapped should just add a warning, or no-op
 436 -- There's no static check; it's up to the user
 437 wrapWarnTcS = wrapTcS
 438
 439 failTcS, panicTcS :: SDoc -> TcS a
 440 failTcS      = wrapTcS . TcM.failWith
 441 panicTcS doc = pprPanic "TcCanonical" doc
 442
 443 traceTcS :: String -> SDoc -> TcS ()
 444 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 445
 446 traceTcS0 :: String -> SDoc -> TcS ()
 447 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
 448
 449 runTcS :: SimplContext
 450        -> Untouchables         -- Untouchables
 451        -> TcS a                -- What to run
 452        -> TcM (a, Bag EvBind)
 453 runTcS context untouch tcs
 454   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 455        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 456        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 457                           , tcs_ty_binds = ty_binds_var
 458                           , tcs_context  = context
 459                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
 460                           }
 461
 462              -- Run the computation
 463        ; res <- unTcS tcs env
 464              -- Perform the type unifications required
 465        ; ty_binds <- TcM.readTcRef ty_binds_var
 466        ; mapM_ do_unification (varEnvElts ty_binds)
 467
 468              -- And return
 469        ; ev_binds      <- TcM.readTcRef evb_ref
 470        ; return (res, evBindMapBinds ev_binds) }
 471   where
 472     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 473
 474 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
 475 nestImplicTcS ref untch (TcS thing_inside)
 476   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
 477                      tcs_context = ctxt } ->
 478     let
 479        nest_env = TcSEnv { tcs_ev_binds = ref
 480                          , tcs_ty_binds = ty_binds
 481                          , tcs_untch    = untch
 482                          , tcs_context  = ctxtUnderImplic ctxt }
 483     in
 484     thing_inside nest_env
 485
 486 recoverTcS :: TcS a -> TcS a -> TcS a
 487 recoverTcS (TcS recovery_code) (TcS thing_inside)
 488   = TcS $ \ env ->
 489     TcM.recoverM (recovery_code env) (thing_inside env)
 490
 491 ctxtUnderImplic :: SimplContext -> SimplContext
 492 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 493 ctxtUnderImplic SimplRuleLhs = SimplCheck
 494 ctxtUnderImplic ctxt         = ctxt
 495
 496 tryTcS :: TcS a -> TcS a
 497 -- Like runTcS, but from within the TcS monad
 498 -- Ignore all the evidence generated, and do not affect caller's evidence!
 499 tryTcS tcs
 500   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 501                     ; ev_binds_var <- TcM.newTcEvBinds
 502                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 503                                      , tcs_ty_binds = ty_binds_var }
 504                     ; unTcS tcs env1 })
 505
 506 -- Update TcEvBinds
 507 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 508
 509 getDynFlags :: TcS DynFlags
 510 getDynFlags = wrapTcS TcM.getDOpts
 511
 512 getTcSContext :: TcS SimplContext
 513 getTcSContext = TcS (return . tcs_context)
 514
 515 getTcEvBinds :: TcS EvBindsVar
 516 getTcEvBinds = TcS (return . tcs_ev_binds)
 517
 518 getUntouchables :: TcS TcsUntouchables
 519 getUntouchables = TcS (return . tcs_untch)
 520
 521 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
 522 getTcSTyBinds = TcS (return . tcs_ty_binds)
 523
 524 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
 525 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 526
 527
 528 getTcEvBindsBag :: TcS EvBindMap
 529 getTcEvBindsBag
 530   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 531        ; wrapTcS $ TcM.readTcRef ev_ref }
 532
 533 setWantedCoBind :: CoVar -> Coercion -> TcS ()
 534 setWantedCoBind cv co
 535   = setEvBind cv (EvCoercion co)
 536      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
 537
 538 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 539 -- Add a type binding
 540 -- We never do this twice!
 541 setWantedTyBind tv ty
 542   = do { ref <- getTcSTyBinds
 543        ; wrapTcS $
 544          do { ty_binds <- TcM.readTcRef ref
 545 #ifdef DEBUG
 546             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
 547               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
 548                    , ppr tv <+> text ":=" <+> ppr ty
 549                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
 550 #endif
 551             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 552
 553 setIPBind :: EvVar -> EvTerm -> TcS ()
 554 setIPBind = setEvBind
 555
 556 setDictBind :: EvVar -> EvTerm -> TcS ()
 557 setDictBind = setEvBind
 558
 559 setEvBind :: EvVar -> EvTerm -> TcS ()
 560 -- Internal
 561 setEvBind ev rhs
 562   = do { tc_evbinds <- getTcEvBinds
 563        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 564
 565 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 566 warnTcS loc warn_if doc
 567   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 568   | otherwise = return ()
 569
 570 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 571 getDefaultInfo
 572   = do { ctxt <- getTcSContext
 573        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 574        ; return (ctxt, tys, flags) }
 575
 576 -- Just get some environments needed for instance looking up and matching
 577 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 578
 579 getInstEnvs :: TcS (InstEnv, InstEnv)
 580 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 581
 582 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 583 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 584
 585 getTopEnv :: TcS HscEnv
 586 getTopEnv = wrapTcS $ TcM.getTopEnv
 587
 588 getGblEnv :: TcS TcGblEnv
 589 getGblEnv = wrapTcS $ TcM.getGblEnv
 590
 591 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 593
 594 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 595 checkWellStagedDFun pred dfun_id loc
 596   = wrapTcS $ TcM.setCtLoc loc $
 597     do { use_stage <- TcM.getStage
 598        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 599   where
 600     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 601     bind_lvl = TcM.topIdLvl dfun_id
 602
 603 pprEq :: TcType -> TcType -> SDoc
 604 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 605
 606 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 607 isTouchableMetaTyVar tv
 608   = do { untch <- getUntouchables
 609        ; return $ isTouchableMetaTyVar_InRange untch tv }
 610
 611 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
 612 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 613   = case tcTyVarDetails tv of
 614       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
 615                         -- See Note [Touchable meta type variables]
 616       MetaTv {}      -> inTouchableRange untch tv
 617       _              -> False
 618
 619
 620 \end{code}
 621
 622
 623 Note [Touchable meta type variables]
 624 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 625 Meta type variables allocated *by the constraint solver itself* are always
 626 touchable.  Example:
 627    instance C a b => D [a] where...
 628 if we use this instance declaration we "make up" a fresh meta type
 629 variable for 'b', which we must later guess.  (Perhaps C has a
 630 functional dependency.)  But since we aren't in the constraint *generator*
 631 we can't allocate a Unique in the touchable range for this implication
 632 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 633
 634
 635 \begin{code}
 636 -- Flatten skolems
 637 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 638
 639 newFlattenSkolemTy :: TcType -> TcS TcType
 640 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 641
 642 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 643 newFlattenSkolemTyVar ty
 644   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
 645                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
 646                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 647        ; traceTcS "New Flatten Skolem Born" $
 648            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
 649        ; return tv }
 650
 651 -- Instantiations
 652 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 653
 654 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 655 instDFunTypes mb_inst_tys
 656   = mapM inst_tv mb_inst_tys
 657   where
 658     inst_tv :: Either TyVar TcType -> TcS Type
 659     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
 660     inst_tv (Right ty) = return ty
 661
 662 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 663 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 664
 665
 666 instFlexiTcS :: TyVar -> TcS TcTyVar
 667 -- Like TcM.instMetaTyVar but the variable that is created is always
 668 -- touchable; we are supposed to guess its instantiation.
 669 -- See Note [Touchable meta type variables]
 670 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
 671
 672 newFlexiTcSTy :: Kind -> TcS TcType
 673 newFlexiTcSTy knd
 674   = wrapTcS $
 675     do { uniq <- TcM.newUnique
 676        ; ref  <- TcM.newMutVar  Flexi
 677        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
 678        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
 679
 680 isFlexiTcsTv :: TyVar -> Bool
 681 isFlexiTcsTv tv
 682   | not (isTcTyVar tv)                  = False
 683   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
 684   | otherwise                           = False
 685
 686 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
 687 -- Create new wanted CoVar that constrains the type to have the specified kind.
 688 newKindConstraint tv knd
 689   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
 690        ; let ty_k = mkTyVarTy tv_k
 691        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
 692        ; return co_var }
 693
 694 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
 695 instFlexiTcSHelper tvname tvkind
 696   = wrapTcS $
 697     do { uniq <- TcM.newUnique
 698        ; ref  <- TcM.newMutVar  Flexi
 699        ; let name = setNameUnique tvname uniq
 700              kind = tvkind
 701        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
 702
 703 -- Superclasses and recursive dictionaries
 704 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 705
 706 newEvVar :: TcPredType -> TcS EvVar
 707 newEvVar pty = wrapTcS $ TcM.newEvVar pty
 708
 709 newDerivedId :: TcPredType -> TcS EvVar
 710 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
 711
 712 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 713 -- Note we create immutable variables for given or derived, since we
 714 -- must bind them to TcEvBinds (because their evidence may involve
 715 -- superclasses). However we should be able to override existing
 716 -- 'derived' evidence, even in TcEvBinds
 717 newGivenCoVar ty1 ty2 co
 718   = do { cv <- newCoVar ty1 ty2
 719        ; setEvBind cv (EvCoercion co)
 720        ; return cv }
 721
 722 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 723 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 724
 725 newCoVar :: TcType -> TcType -> TcS EvVar
 726 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 727
 728 newIPVar :: IPName Name -> TcType -> TcS EvVar
 729 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 730
 731 newDictVar :: Class -> [TcType] -> TcS EvVar
 732 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 733 \end{code}
 734
 735
 736 \begin{code}
 737 -- Matching and looking up classes and family instances
 738 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 739
 740 data MatchInstResult mi
 741   = MatchInstNo         -- No matching instance
 742   | MatchInstSingle mi  -- Single matching instance
 743   | MatchInstMany       -- Multiple matching instances
 744
 745
 746 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 747 -- Look up a class constraint in the instance environment
 748 matchClass clas tys
 749   = do  { let pred = mkClassPred clas tys
 750         ; instEnvs <- getInstEnvs
 751         ; case lookupInstEnv instEnvs clas tys of {
 752             ([], unifs)               -- Nothing matches
 753                 -> do { traceTcS "matchClass not matching"
 754                                  (vcat [ text "dict" <+> ppr pred,
 755                                          text "unifs" <+> ppr unifs ])
 756                       ; return MatchInstNo
 757                       } ;
 758             ([(ispec, inst_tys)], []) -- A single match
 759                 -> do   { let dfun_id = is_dfun ispec
 760                         ; traceTcS "matchClass success"
 761                                    (vcat [text "dict" <+> ppr pred,
 762                                           text "witness" <+> ppr dfun_id
 763                                            <+> ppr (idType dfun_id) ])
 764                                   -- Record that this dfun is needed
 765                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 766                         } ;
 767             (matches, unifs)          -- More than one matches
 768                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 769                                    (vcat [text "dict" <+> ppr pred,
 770                                           text "matches" <+> ppr matches,
 771                                           text "unifs" <+> ppr unifs])
 772                         ; return MatchInstMany
 773                         }
 774         }
 775         }
 776
 777 matchFam :: TyCon
 778          -> [Type]
 779          -> TcS (MatchInstResult (TyCon, [Type]))
 780 matchFam tycon args
 781   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 782        ; case mb of
 783            Nothing  -> return MatchInstNo
 784            Just res -> return $ MatchInstSingle res
 785        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 786        -- multiple matches. Check.
 787        }
 788
 789
 790 -- Functional dependencies, instantiation of equations
 791 -------------------------------------------------------
 792
 793 mkDerivedFunDepEqns :: WantedLoc
 794                    -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 795                    -> TcS [FlavoredEvVar]    -- All Derived
 796 mkDerivedFunDepEqns _   [] = return []
 797 mkDerivedFunDepEqns loc eqns
 798   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 799        ; evvars <- mapM to_work_item eqns
 800        ; return $ concat evvars }
 801   where
 802     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
 803     to_work_item ((qtvs, pairs), d1, d2)
 804       = do { let tvs = varSetElems qtvs
 805            ; tvs' <- mapM instFlexiTcS tvs
 806            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
 807                  loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
 808                  flav  = Derived loc'
 809            ; mapM (do_one subst flav) pairs }
 810
 811     do_one subst flav (ty1, ty2)
 812        = do { let sty1 = substTy subst ty1
 813                   sty2 = substTy subst ty2
 814             ; ev <- newCoVar sty1 sty2
 815             ; return (mkEvVarX ev flav) }
 816
 817 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
 818 pprEquationDoc (eqn, (p1, _), (p2, _))
 819   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 820
 821 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
 822          -> TcM (TidyEnv, SDoc)
 823 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
 824   = do  { pred1' <- TcM.zonkTcPredType pred1
 825         ; pred2' <- TcM.zonkTcPredType pred2
 826         ; let { pred1'' = tidyPred tidy_env pred1'
 827               ; pred2'' = tidyPred tidy_env pred2' }
 828         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
 829                           nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
 830                           nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
 831         ; return (tidy_env, msg) }
 832 \end{code}