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
  10     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
  11     mkWantedConstraints, deCanonicaliseWanted,
  12     makeGivens, makeSolvedByInst,
  13
  14     CtFlavor (..), isWanted, isGiven, isDerived,
  15     isGivenCt, isWantedCt, pprFlavorArising,
  16
  17     isFlexiTcsTv,
  18
  19     DerivedOrig (..),
  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
  30     newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar,
  31     newIPVar, newDictVar, newKindConstraint,
  32
  33        -- Setting evidence variables
  34     setWantedCoBind, setDerivedCoBind,
  35     setIPBind, setDictBind, setEvBind,
  36
  37     setWantedTyBind,
  38
  39     newTcEvBindsTcS,
  40
  41     getInstEnvs, getFamInstEnvs,                -- Getting the environments
  42     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
  43     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
  44     getTcSErrorsBag, FrozenError (..),
  45     addErrorTcS,
  46     ErrorKind(..),
  47
  48     newFlattenSkolemTy,                         -- Flatten skolems
  49
  50
  51     instDFunTypes,                              -- Instantiation
  52     instDFunConstraints,
  53     newFlexiTcSTy,
  54
  55     isGoodRecEv,
  56
  57     compatKind,
  58
  59
  60     TcsUntouchables,
  61     isTouchableMetaTyVar,
  62     isTouchableMetaTyVar_InRange,
  63
  64     getDefaultInfo, getDynFlags,
  65
  66     matchClass, matchFam, MatchInstResult (..),
  67     checkWellStagedDFun,
  68     warnTcS,
  69     pprEq,                                   -- Smaller utils, re-exported from TcM
  70                                              -- TODO (DV): these are only really used in the
  71                                              -- instance matcher in TcSimplify. I am wondering
  72                                              -- if the whole instance matcher simply belongs
  73                                              -- here
  74
  75
  76     mkWantedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
  77
  78 ) where
  79
  80 #include "HsVersions.h"
  81
  82 import HscTypes
  83 import BasicTypes
  84
  85 import Inst
  86 import InstEnv
  87 import FamInst
  88 import FamInstEnv
  89
  90 import qualified TcRnMonad as TcM
  91 import qualified TcMType as TcM
  92 import qualified TcEnv as TcM
  93        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
  94 import TcType
  95 import DynFlags
  96
  97 import Coercion
  98 import Class
  99 import TyCon
 100 import TypeRep
 101
 102 import Name
 103 import Var
 104 import VarEnv
 105 import Outputable
 106 import Bag
 107 import MonadUtils
 108 import VarSet
 109 import FastString
 110
 111 import HsBinds               -- for TcEvBinds stuff
 112 import Id
 113 import FunDeps
 114
 115 import TcRnTypes
 116
 117 import Control.Monad
 118 import Data.IORef
 119 \end{code}
 120
 121
 122 %************************************************************************
 123 %*                                                                      *
 124 %*                       Canonical constraints                          *
 125 %*                                                                      *
 126 %*   These are the constraints the low-level simplifier works with      *
 127 %*                                                                      *
 128 %************************************************************************
 129
 130 \begin{code}
 131 -- Types without any type functions inside.  However, note that xi
 132 -- types CAN contain unexpanded type synonyms; however, the
 133 -- (transitive) expansions of those type synonyms will not contain any
 134 -- type functions.
 135 type Xi = Type       -- In many comments, "xi" ranges over Xi
 136
 137 type CanonicalCts = Bag CanonicalCt
 138
 139 data CanonicalCt
 140   -- Atomic canonical constraints
 141   = CDictCan {  -- e.g.  Num xi
 142       cc_id     :: EvVar,
 143       cc_flavor :: CtFlavor,
 144       cc_class  :: Class,
 145       cc_tyargs :: [Xi]
 146     }
 147
 148   | CIPCan {    -- ?x::tau
 149       -- See note [Canonical implicit parameter constraints].
 150       cc_id     :: EvVar,
 151       cc_flavor :: CtFlavor,
 152       cc_ip_nm  :: IPName Name,
 153       cc_ip_ty  :: TcTauType
 154     }
 155
 156   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
 157        -- Invariant:
 158        --   * tv not in tvs(xi)   (occurs check)
 159        --   * If constraint is given then typeKind xi `compatKind` typeKind tv
 160        --                See Note [Spontaneous solving and kind compatibility]
 161        --   * We prefer unification variables on the left *JUST* for efficiency
 162       cc_id     :: EvVar,
 163       cc_flavor :: CtFlavor,
 164       cc_tyvar  :: TcTyVar,
 165       cc_rhs    :: Xi
 166     }
 167
 168   | CFunEqCan {  -- F xis ~ xi
 169                  -- Invariant: * isSynFamilyTyCon cc_fun
 170                  --            * If constraint is given then
 171                  --                 typeKind (F xis) `compatKind` typeKind xi
 172       cc_id     :: EvVar,
 173       cc_flavor :: CtFlavor,
 174       cc_fun    :: TyCon,       -- A type function
 175       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
 176       cc_rhs    :: Xi           --    *never* over-saturated (because if so
 177                                 --    we should have decomposed)
 178
 179     }
 180
 181 compatKind :: Kind -> Kind -> Bool
 182 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
 183
 184 makeGivens :: Bag WantedEvVar -> Bag (CtFlavor,EvVar)
 185 makeGivens = mapBag (\(WantedEvVar ev wloc) -> (mkGivenFlavor (Wanted wloc) UnkSkol, ev))
 186 -- ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
 187            -- The UnkSkol doesn't matter because these givens are
 188            -- not contradictory (else we'd have rejected them already)
 189
 190 makeSolvedByInst :: CanonicalCt -> CanonicalCt
 191 -- Record that a constraint is now solved
 192 --        Wanted         -> Derived
 193 --        Given, Derived -> no-op
 194 makeSolvedByInst ct
 195   | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
 196   | otherwise                  = ct
 197
 198 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
 199 mkWantedConstraints flats implics
 200   = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
 201
 202 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
 203 deCanonicaliseWanted ct
 204   = WARN( not (isWanted $ cc_flavor ct), ppr ct )
 205     let Wanted loc = cc_flavor ct
 206     in WantedEvVar (cc_id ct) loc
 207
 208 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
 209 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
 210 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
 211 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
 212 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
 213
 214 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
 215 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
 216 tyVarsOfCDict _ct                            = emptyVarSet
 217
 218 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
 219 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
 220
 221 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
 222 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
 223
 224 instance Outputable CanonicalCt where
 225   ppr (CDictCan d fl cls tys)
 226       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
 227   ppr (CIPCan ip fl ip_nm ty)
 228       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
 229   ppr (CTyEqCan co fl tv ty)
 230       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
 231   ppr (CFunEqCan co fl tc tys ty)
 232       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
 233 \end{code}
 234
 235 Note [Canonical implicit parameter constraints]
 236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 237 The type in a canonical implicit parameter constraint doesn't need to
 238 be a xi (type-function-free type) since we can defer the flattening
 239 until checking this type for equality with another type.  If we
 240 encounter two IP constraints with the same name, they MUST have the
 241 same type, and at that point we can generate a flattened equality
 242 constraint between the types.  (On the other hand, the types in two
 243 class constraints for the same class MAY be equal, so they need to be
 244 flattened in the first place to facilitate comparing them.)
 245
 246 \begin{code}
 247 singleCCan :: CanonicalCt -> CanonicalCts
 248 singleCCan = unitBag
 249
 250 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts
 251 andCCan = unionBags
 252
 253 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts
 254 extendCCans = snocBag
 255
 256 andCCans :: [CanonicalCts] -> CanonicalCts
 257 andCCans = unionManyBags
 258
 259 emptyCCan :: CanonicalCts
 260 emptyCCan = emptyBag
 261
 262 isEmptyCCan :: CanonicalCts -> Bool
 263 isEmptyCCan = isEmptyBag
 264
 265 isCTyEqCan :: CanonicalCt -> Bool
 266 isCTyEqCan (CTyEqCan {})  = True
 267 isCTyEqCan (CFunEqCan {}) = False
 268 isCTyEqCan _              = False
 269
 270 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
 271 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
 272 isCDictCan_Maybe _              = Nothing
 273
 274 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
 275 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
 276 isCIPCan_Maybe _                = Nothing
 277
 278 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
 279 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
 280 isCFunEqCan_Maybe _ = Nothing
 281
 282 \end{code}
 283
 284 %************************************************************************
 285 %*                                                                      *
 286                     CtFlavor
 287          The "flavor" of a canonical constraint
 288 %*                                                                      *
 289 %************************************************************************
 290
 291 \begin{code}
 292 data CtFlavor
 293   = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
 294   | Derived WantedLoc DerivedOrig
 295                       -- We have evidence for this constraint in TcEvBinds;
 296                       --   *however* this evidence can contain wanteds, so
 297                       --   it's valid only provisionally to the solution of
 298                       --   these wanteds
 299   | Wanted WantedLoc  -- We have no evidence bindings for this constraint.
 300
 301 data DerivedOrig = DerSC | DerInst | DerSelf
 302 -- Deriveds are either superclasses of other wanteds or deriveds, or partially
 303 -- solved wanteds from instances, or 'self' dictionaries containing yet wanted
 304 -- superclasses.
 305
 306 instance Outputable CtFlavor where
 307   ppr (Given _)    = ptext (sLit "[Given]")
 308   ppr (Wanted _)   = ptext (sLit "[Wanted]")
 309   ppr (Derived {}) = ptext (sLit "[Derived]")
 310
 311 isWanted :: CtFlavor -> Bool
 312 isWanted (Wanted {}) = True
 313 isWanted _           = False
 314
 315 isGiven :: CtFlavor -> Bool
 316 isGiven (Given {}) = True
 317 isGiven _          = False
 318
 319 isDerived :: CtFlavor -> Bool
 320 isDerived (Derived {}) = True
 321 isDerived _            = False
 322
 323 pprFlavorArising :: CtFlavor -> SDoc
 324 pprFlavorArising (Derived wl _) = pprArisingAt wl
 325 pprFlavorArising (Wanted  wl)   = pprArisingAt wl
 326 pprFlavorArising (Given gl)     = pprArisingAt gl
 327
 328 getWantedLoc :: CanonicalCt -> WantedLoc
 329 getWantedLoc ct
 330   = ASSERT (isWanted (cc_flavor ct))
 331     case cc_flavor ct of
 332       Wanted wl -> wl
 333       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
 334
 335
 336 isWantedCt :: CanonicalCt -> Bool
 337 isWantedCt ct = isWanted (cc_flavor ct)
 338 isGivenCt :: CanonicalCt -> Bool
 339 isGivenCt ct = isGiven (cc_flavor ct)
 340
 341 canSolve :: CtFlavor -> CtFlavor -> Bool
 342 -- canSolve ctid1 ctid2
 343 -- The constraint ctid1 can be used to solve ctid2
 344 -- "to solve" means a reaction where the active parts of the two constraints match.
 345 --  active(F xis ~ xi) = F xis
 346 --  active(tv ~ xi)    = tv
 347 --  active(D xis)      = D xis
 348 --  active(IP nm ty)   = nm
 349 -----------------------------------------
 350 canSolve (Given {})   _            = True
 351 canSolve (Derived {}) (Wanted {})  = True
 352 canSolve (Derived {}) (Derived {}) = True
 353 canSolve (Wanted {})  (Wanted {})  = True
 354 canSolve _ _ = False
 355
 356 canRewrite :: CtFlavor -> CtFlavor -> Bool
 357 -- canRewrite ctid1 ctid2
 358 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
 359 canRewrite = canSolve
 360
 361 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
 362 -- Precondition: At least one of them should be wanted
 363 combineCtLoc (Wanted loc) _    = loc
 364 combineCtLoc _ (Wanted loc)    = loc
 365 combineCtLoc (Derived loc _) _ = loc
 366 combineCtLoc _ (Derived loc _) = loc
 367 combineCtLoc _ _ = panic "combineCtLoc: both given"
 368
 369 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
 370 mkGivenFlavor (Wanted  loc)   sk = Given (setCtLocOrigin loc sk)
 371 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
 372 mkGivenFlavor (Given   loc)   sk = Given (setCtLocOrigin loc sk)
 373
 374 mkWantedFlavor :: CtFlavor -> CtFlavor
 375 mkWantedFlavor (Wanted  loc)   = Wanted loc
 376 mkWantedFlavor (Derived loc _) = Wanted loc
 377 mkWantedFlavor fl@(Given {})   = pprPanic "mkWantedFlavour" (ppr fl)
 378 \end{code}
 379
 380
 381 %************************************************************************
 382 %*                                                                      *
 383 %*              The TcS solver monad                                    *
 384 %*                                                                      *
 385 %************************************************************************
 386
 387 Note [The TcS monad]
 388 ~~~~~~~~~~~~~~~~~~~~
 389 The TcS monad is a weak form of the main Tc monad
 390
 391 All you can do is
 392     * fail
 393     * allocate new variables
 394     * fill in evidence variables
 395
 396 Filling in a dictionary evidence variable means to create a binding
 397 for it, so TcS carries a mutable location where the binding can be
 398 added.  This is initialised from the innermost implication constraint.
 399
 400 \begin{code}
 401 data TcSEnv
 402   = TcSEnv {
 403       tcs_ev_binds :: EvBindsVar,
 404           -- Evidence bindings
 405
 406       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
 407           -- Global type bindings
 408
 409       tcs_context :: SimplContext,
 410
 411       tcs_errors :: IORef (Bag FrozenError),
 412           -- Frozen errors that we defer reporting as much as possible, in order to
 413           -- make them as informative as possible. See Note [Frozen Errors]
 414
 415       tcs_untch :: TcsUntouchables
 416     }
 417
 418 type TcsUntouchables = (Untouchables,TcTyVarSet)
 419 -- Like the TcM Untouchables,
 420 -- but records extra TcsTv variables generated during simplification
 421 -- See Note [Extra TcsTv untouchables] in TcSimplify
 422
 423 data FrozenError
 424   = FrozenError ErrorKind CtFlavor TcType TcType
 425
 426 data ErrorKind
 427   = MisMatchError | OccCheckError | KindError
 428
 429 instance Outputable FrozenError where
 430   ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
 431
 432 \end{code}
 433
 434 Note [Frozen Errors]
 435 ~~~~~~~~~~~~~~~~~~~~
 436 Some of the errors that we get during canonicalization are best reported when all constraints
 437 have been simplified as much as possible. For instance, assume that during simplification
 438 the following constraints arise:
 439
 440  [Wanted]   F alpha ~  uf1
 441  [Wanted]   beta ~ uf1 beta
 442
 443 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply
 444 see a message:
 445     'Can't construct the infinite type  beta ~ uf1 beta'
 446 and the user has no idea what the uf1 variable is.
 447
 448 Instead our plan is that we will NOT fail immediately, but:
 449     (1) Record the "frozen" error in the tcs_errors field
 450     (2) Isolate the offending constraint from the rest of the inerts
 451     (3) Keep on simplifying/canonicalizing
 452
 453 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to
 454 report a more informative error:
 455     'Can't construct the infinite type beta ~ F alpha beta'
 456 \begin{code}
 457
 458 data SimplContext
 459   = SimplInfer          -- Inferring type of a let-bound thing
 460   | SimplRuleLhs        -- Inferring type of a RULE lhs
 461   | SimplInteractive    -- Inferring type at GHCi prompt
 462   | SimplCheck          -- Checking a type signature or RULE rhs
 463   deriving Eq
 464
 465 instance Outputable SimplContext where
 466   ppr SimplInfer       = ptext (sLit "SimplInfer")
 467   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
 468   ppr SimplInteractive = ptext (sLit "SimplInteractive")
 469   ppr SimplCheck       = ptext (sLit "SimplCheck")
 470
 471 isInteractive :: SimplContext -> Bool
 472 isInteractive SimplInteractive = True
 473 isInteractive _                = False
 474
 475 simplEqsOnly :: SimplContext -> Bool
 476 -- Simplify equalities only, not dictionaries
 477 -- This is used for the LHS of rules; ee
 478 -- Note [Simplifying RULE lhs constraints] in TcSimplify
 479 simplEqsOnly SimplRuleLhs = True
 480 simplEqsOnly _            = False
 481
 482 performDefaulting :: SimplContext -> Bool
 483 performDefaulting SimplInfer       = False
 484 performDefaulting SimplRuleLhs     = False
 485 performDefaulting SimplInteractive = True
 486 performDefaulting SimplCheck       = True
 487
 488 ---------------
 489 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
 490
 491 instance Functor TcS where
 492   fmap f m = TcS $ fmap f . unTcS m
 493
 494 instance Monad TcS where
 495   return x  = TcS (\_ -> return x)
 496   fail err  = TcS (\_ -> fail err)
 497   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 498
 499 -- Basic functionality
 500 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 501 wrapTcS :: TcM a -> TcS a
 502 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
 503 -- and TcS is supposed to have limited functionality
 504 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
 505
 506 wrapErrTcS :: TcM a -> TcS a
 507 -- The thing wrapped should just fail
 508 -- There's no static check; it's up to the user
 509 -- Having a variant for each error message is too painful
 510 wrapErrTcS = wrapTcS
 511
 512 wrapWarnTcS :: TcM a -> TcS a
 513 -- The thing wrapped should just add a warning, or no-op
 514 -- There's no static check; it's up to the user
 515 wrapWarnTcS = wrapTcS
 516
 517 failTcS, panicTcS :: SDoc -> TcS a
 518 failTcS      = wrapTcS . TcM.failWith
 519 panicTcS doc = pprPanic "TcCanonical" doc
 520
 521 traceTcS :: String -> SDoc -> TcS ()
 522 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
 523
 524 traceTcS0 :: String -> SDoc -> TcS ()
 525 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
 526
 527 runTcS :: SimplContext
 528        -> Untouchables         -- Untouchables
 529        -> TcS a                -- What to run
 530        -> TcM (a, Bag FrozenError, Bag EvBind)
 531 runTcS context untouch tcs
 532   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 533        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
 534        ; err_ref <- TcM.newTcRef emptyBag
 535        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
 536                           , tcs_ty_binds = ty_binds_var
 537                           , tcs_context  = context
 538                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
 539                           , tcs_errors   = err_ref
 540                           }
 541
 542              -- Run the computation
 543        ; res <- unTcS tcs env
 544              -- Perform the type unifications required
 545        ; ty_binds <- TcM.readTcRef ty_binds_var
 546        ; mapM_ do_unification (varEnvElts ty_binds)
 547
 548              -- And return
 549        ; frozen_errors <- TcM.readTcRef err_ref
 550        ; ev_binds      <- TcM.readTcRef evb_ref
 551        ; return (res, frozen_errors, evBindMapBinds ev_binds) }
 552   where
 553     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
 554
 555 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
 556 nestImplicTcS ref untch (TcS thing_inside)
 557   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
 558                      tcs_context = ctxt,
 559                      tcs_errors = err_ref } ->
 560     let
 561        nest_env = TcSEnv { tcs_ev_binds = ref
 562                          , tcs_ty_binds = ty_binds
 563                          , tcs_untch    = untch
 564                          , tcs_context  = ctxtUnderImplic ctxt
 565                          , tcs_errors   = err_ref }
 566     in
 567     thing_inside nest_env
 568
 569 recoverTcS :: TcS a -> TcS a -> TcS a
 570 recoverTcS (TcS recovery_code) (TcS thing_inside)
 571   = TcS $ \ env ->
 572     TcM.recoverM (recovery_code env) (thing_inside env)
 573
 574 ctxtUnderImplic :: SimplContext -> SimplContext
 575 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
 576 ctxtUnderImplic SimplRuleLhs = SimplCheck
 577 ctxtUnderImplic ctxt         = ctxt
 578
 579 tryTcS :: TcS a -> TcS a
 580 -- Like runTcS, but from within the TcS monad
 581 -- Ignore all the evidence generated, and do not affect caller's evidence!
 582 tryTcS tcs
 583   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
 584                     ; ev_binds_var <- TcM.newTcEvBinds
 585                     ; err_ref      <- TcM.newTcRef emptyBag
 586                     ; let env1 = env { tcs_ev_binds = ev_binds_var
 587                                      , tcs_ty_binds = ty_binds_var
 588                                      , tcs_errors   = err_ref }
 589                     ; unTcS tcs env1 })
 590
 591 -- Update TcEvBinds
 592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 593
 594 getDynFlags :: TcS DynFlags
 595 getDynFlags = wrapTcS TcM.getDOpts
 596
 597 getTcSContext :: TcS SimplContext
 598 getTcSContext = TcS (return . tcs_context)
 599
 600 getTcEvBinds :: TcS EvBindsVar
 601 getTcEvBinds = TcS (return . tcs_ev_binds)
 602
 603 getUntouchables :: TcS TcsUntouchables
 604 getUntouchables = TcS (return . tcs_untch)
 605
 606 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
 607 getTcSTyBinds = TcS (return . tcs_ty_binds)
 608
 609 getTcSErrors :: TcS (IORef (Bag FrozenError))
 610 getTcSErrors = TcS (return . tcs_errors)
 611
 612 getTcSErrorsBag :: TcS (Bag FrozenError)
 613 getTcSErrorsBag = do { err_ref <- getTcSErrors
 614                      ; wrapTcS $ TcM.readTcRef err_ref }
 615
 616 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
 617 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
 618
 619
 620 getTcEvBindsBag :: TcS EvBindMap
 621 getTcEvBindsBag
 622   = do { EvBindsVar ev_ref _ <- getTcEvBinds
 623        ; wrapTcS $ TcM.readTcRef ev_ref }
 624
 625 setWantedCoBind :: CoVar -> Coercion -> TcS ()
 626 setWantedCoBind cv co
 627   = setEvBind cv (EvCoercion co)
 628      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co
 629
 630 setDerivedCoBind :: CoVar -> Coercion -> TcS ()
 631 setDerivedCoBind cv co
 632   = setEvBind cv (EvCoercion co)
 633
 634 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
 635 -- Add a type binding
 636 -- We never do this twice!
 637 setWantedTyBind tv ty
 638   = do { ref <- getTcSTyBinds
 639        ; wrapTcS $
 640          do { ty_binds <- TcM.readTcRef ref
 641 #ifdef DEBUG
 642             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
 643               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
 644                    , ppr tv <+> text ":=" <+> ppr ty
 645                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
 646 #endif
 647             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
 648
 649 setIPBind :: EvVar -> EvTerm -> TcS ()
 650 setIPBind = setEvBind
 651
 652 setDictBind :: EvVar -> EvTerm -> TcS ()
 653 setDictBind = setEvBind
 654
 655 setEvBind :: EvVar -> EvTerm -> TcS ()
 656 -- Internal
 657 setEvBind ev rhs
 658   = do { tc_evbinds <- getTcEvBinds
 659        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
 660
 661 newTcEvBindsTcS :: TcS EvBindsVar
 662 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
 663
 664 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 665 warnTcS loc warn_if doc
 666   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
 667   | otherwise = return ()
 668
 669 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
 670 getDefaultInfo
 671   = do { ctxt <- getTcSContext
 672        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
 673        ; return (ctxt, tys, flags) }
 674
 675
 676
 677 -- Recording errors in the TcS monad
 678 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 679
 680 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
 681 addErrorTcS frknd fl ty1 ty2
 682   = do { err_ref <- getTcSErrors
 683        ; wrapTcS $ do
 684        { TcM.updTcRef err_ref $ \ errs ->
 685            consBag (FrozenError frknd fl ty1 ty2) errs
 686
 687            -- If there's an error in the *given* constraints,
 688            -- stop right now, to avoid a cascade of errors
 689            -- in the wanteds
 690        ; when (isGiven fl) TcM.failM
 691
 692        ; return () } }
 693
 694 -- Just get some environments needed for instance looking up and matching
 695 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 696
 697 getInstEnvs :: TcS (InstEnv, InstEnv)
 698 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
 699
 700 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 701 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
 702
 703 getTopEnv :: TcS HscEnv
 704 getTopEnv = wrapTcS $ TcM.getTopEnv
 705
 706 getGblEnv :: TcS TcGblEnv
 707 getGblEnv = wrapTcS $ TcM.getGblEnv
 708
 709 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 710 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 711
 712 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS ()
 713 checkWellStagedDFun pred dfun_id loc
 714   = wrapTcS $ TcM.setCtLoc loc $
 715     do { use_stage <- TcM.getStage
 716        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
 717   where
 718     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
 719     bind_lvl = TcM.topIdLvl dfun_id
 720
 721 pprEq :: TcType -> TcType -> SDoc
 722 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 723
 724 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
 725 isTouchableMetaTyVar tv
 726   = do { untch <- getUntouchables
 727        ; return $ isTouchableMetaTyVar_InRange untch tv }
 728
 729 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
 730 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 731   = case tcTyVarDetails tv of
 732       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
 733                         -- See Note [Touchable meta type variables]
 734       MetaTv {}      -> inTouchableRange untch tv
 735       _              -> False
 736
 737
 738 \end{code}
 739
 740
 741 Note [Touchable meta type variables]
 742 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 743 Meta type variables allocated *by the constraint solver itself* are always
 744 touchable.  Example:
 745    instance C a b => D [a] where...
 746 if we use this instance declaration we "make up" a fresh meta type
 747 variable for 'b', which we must later guess.  (Perhaps C has a
 748 functional dependency.)  But since we aren't in the constraint *generator*
 749 we can't allocate a Unique in the touchable range for this implication
 750 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 751
 752
 753 \begin{code}
 754 -- Flatten skolems
 755 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 756
 757 newFlattenSkolemTy :: TcType -> TcS TcType
 758 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
 759
 760 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
 761 newFlattenSkolemTyVar ty
 762   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
 763                             ; let name = mkSysTvName uniq (fsLit "f")
 764                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 765        ; traceTcS "New Flatten Skolem Born" $
 766            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
 767        ; return tv }
 768
 769 -- Instantiations
 770 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 771
 772 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
 773 instDFunTypes mb_inst_tys
 774   = mapM inst_tv mb_inst_tys
 775   where
 776     inst_tv :: Either TyVar TcType -> TcS Type
 777     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
 778     inst_tv (Right ty) = return ty
 779
 780 instDFunConstraints :: TcThetaType -> TcS [EvVar]
 781 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
 782
 783
 784 instFlexiTcS :: TyVar -> TcS TcTyVar
 785 -- Like TcM.instMetaTyVar but the variable that is created is always
 786 -- touchable; we are supposed to guess its instantiation.
 787 -- See Note [Touchable meta type variables]
 788 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
 789
 790 newFlexiTcSTy :: Kind -> TcS TcType
 791 newFlexiTcSTy knd
 792   = wrapTcS $
 793     do { uniq <- TcM.newUnique
 794        ; ref  <- TcM.newMutVar  Flexi
 795        ; let name = mkSysTvName uniq (fsLit "uf")
 796        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
 797
 798 isFlexiTcsTv :: TyVar -> Bool
 799 isFlexiTcsTv tv
 800   | not (isTcTyVar tv)                  = False
 801   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
 802   | otherwise                           = False
 803
 804 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
 805 -- Create new wanted CoVar that constrains the type to have the specified kind.
 806 newKindConstraint tv knd
 807   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
 808        ; let ty_k = mkTyVarTy tv_k
 809        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
 810        ; return co_var }
 811
 812 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
 813 instFlexiTcSHelper tvname tvkind
 814   = wrapTcS $
 815     do { uniq <- TcM.newUnique
 816        ; ref  <- TcM.newMutVar  Flexi
 817        ; let name = setNameUnique tvname uniq
 818              kind = tvkind
 819        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
 820
 821 -- Superclasses and recursive dictionaries
 822 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 823
 824 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar
 825 newGivOrDerEvVar pty evtrm
 826   = do { ev <- wrapTcS $ TcM.newEvVar pty
 827        ; setEvBind ev evtrm
 828        ; return ev }
 829
 830 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar
 831 -- Note we create immutable variables for given or derived, since we
 832 -- must bind them to TcEvBinds (because their evidence may involve
 833 -- superclasses). However we should be able to override existing
 834 -- 'derived' evidence, even in TcEvBinds
 835 newGivOrDerCoVar ty1 ty2 co
 836   = do { cv <- newCoVar ty1 ty2
 837        ; setEvBind cv (EvCoercion co)
 838        ; return cv }
 839
 840 newWantedCoVar :: TcType -> TcType -> TcS EvVar
 841 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2
 842
 843
 844 newCoVar :: TcType -> TcType -> TcS EvVar
 845 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
 846
 847 newIPVar :: IPName Name -> TcType -> TcS EvVar
 848 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty
 849
 850 newDictVar :: Class -> [TcType] -> TcS EvVar
 851 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys
 852 \end{code}
 853
 854
 855 \begin{code}
 856 isGoodRecEv :: EvVar -> EvVar -> TcS Bool
 857 -- In a call (isGoodRecEv ev wv), we are considering solving wv
 858 -- using some term that involves ev, such as:
 859 -- by setting           wv = ev
 860 -- or                   wv = EvCast x |> ev
 861 -- etc.
 862 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
 863 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev
 864 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
 865 --
 866 -- Guarded means: more instance calls than superclass selections. We
 867 -- compute this by chasing the evidence, adding +1 for every instance
 868 -- call (constructor) and -1 for every superclass selection (destructor).
 869 --
 870 -- See Note [Superclasses and recursive dictionaries] in TcInteract
 871 isGoodRecEv ev_var wv
 872   = do { tc_evbinds <- getTcEvBindsBag
 873        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
 874        ; return $ case mb of
 875                     Nothing -> True
 876                     Just min_guardedness -> min_guardedness > 0
 877        }
 878
 879   where chase_ev_var :: EvBindMap   -- Evidence binds
 880                  -> EvVar           -- Target variable whose gravity we want to return
 881                  -> Int             -- Current gravity
 882                  -> [EvVar]         -- Visited nodes
 883                  -> EvVar           -- Current node
 884                  -> TcS (Maybe Int)
 885         chase_ev_var assocs trg curr_grav visited orig
 886             | trg == orig         = return $ Just curr_grav
 887             | orig `elem` visited = return $ Nothing
 888             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
 889             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
 890
 891             | otherwise = return Nothing
 892
 893         chase_ev assocs trg curr_grav visited (EvId v)
 894             = chase_ev_var assocs trg curr_grav visited v
 895         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _)
 896             = chase_ev_var assocs trg (curr_grav-1) visited d_id
 897         chase_ev assocs trg curr_grav visited (EvCast v co)
 898             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
 899                  ; m2 <- chase_co assocs trg curr_grav visited co
 900                  ; return (comb_chase_res Nothing [m1,m2]) }
 901
 902         chase_ev assocs trg curr_grav visited (EvCoercion co)
 903             = chase_co assocs trg curr_grav visited co
 904         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_deps)
 905             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
 906                  ; return (comb_chase_res Nothing chase_results) }
 907
 908         chase_co assocs trg curr_grav visited co
 909             = -- Look for all the coercion variables in the coercion
 910               -- chase them, and combine the results. This is OK since the
 911               -- coercion will not contain any superclass terms -- anything
 912               -- that involves dictionaries will be bound in assocs.
 913               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
 914                                              (tyVarsOfType co)
 915               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
 916                     ; return (comb_chase_res Nothing chase_results) }
 917
 918         comb_chase_res f []                   = f
 919         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest
 920         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
 921         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest
 922
 923
 924 -- Matching and looking up classes and family instances
 925 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 926
 927 data MatchInstResult mi
 928   = MatchInstNo         -- No matching instance
 929   | MatchInstSingle mi  -- Single matching instance
 930   | MatchInstMany       -- Multiple matching instances
 931
 932
 933 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
 934 -- Look up a class constraint in the instance environment
 935 matchClass clas tys
 936   = do  { let pred = mkClassPred clas tys
 937         ; instEnvs <- getInstEnvs
 938         ; case lookupInstEnv instEnvs clas tys of {
 939             ([], unifs)               -- Nothing matches
 940                 -> do { traceTcS "matchClass not matching"
 941                                  (vcat [ text "dict" <+> ppr pred,
 942                                          text "unifs" <+> ppr unifs ])
 943                       ; return MatchInstNo
 944                       } ;
 945             ([(ispec, inst_tys)], []) -- A single match
 946                 -> do   { let dfun_id = is_dfun ispec
 947                         ; traceTcS "matchClass success"
 948                                    (vcat [text "dict" <+> ppr pred,
 949                                           text "witness" <+> ppr dfun_id
 950                                            <+> ppr (idType dfun_id), ppr instEnvs ])
 951                                   -- Record that this dfun is needed
 952                         ; return $ MatchInstSingle (dfun_id, inst_tys)
 953                         } ;
 954             (matches, unifs)          -- More than one matches
 955                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
 956                                    (vcat [text "dict" <+> ppr pred,
 957                                           text "matches" <+> ppr matches,
 958                                           text "unifs" <+> ppr unifs])
 959                         ; return MatchInstMany
 960                         }
 961         }
 962         }
 963
 964 matchFam :: TyCon
 965          -> [Type]
 966          -> TcS (MatchInstResult (TyCon, [Type]))
 967 matchFam tycon args
 968   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
 969        ; case mb of
 970            Nothing  -> return MatchInstNo
 971            Just res -> return $ MatchInstSingle res
 972        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns
 973        -- multiple matches. Check.
 974        }
 975
 976
 977 -- Functional dependencies, instantiation of equations
 978 -------------------------------------------------------
 979
 980 mkWantedFunDepEqns :: WantedLoc
 981                    -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
 982                    -> TcS [WantedEvVar]
 983 mkWantedFunDepEqns _   [] = return []
 984 mkWantedFunDepEqns loc eqns
 985   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
 986        ; wevvars <- mapM to_work_item eqns
 987        ; return $ concat wevvars }
 988   where
 989     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
 990     to_work_item ((qtvs, pairs), d1, d2)
 991       = do { let tvs = varSetElems qtvs
 992            ; tvs' <- mapM instFlexiTcS tvs
 993            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
 994                  loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
 995            ; mapM (do_one subst loc') pairs }
 996
 997     do_one subst loc' (ty1, ty2)
 998        = do { let sty1 = substTy subst ty1
 999                   sty2 = substTy subst ty2
1000             ; ev <- newWantedCoVar sty1 sty2
1001             ; return (WantedEvVar ev loc') }
1002
1003 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
1004 pprEquationDoc (eqn, (p1, _), (p2, _))
1005   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1006
1007 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1008          -> TcM (TidyEnv, SDoc)
1009 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1010   = do  { pred1' <- TcM.zonkTcPredType pred1
1011         ; pred2' <- TcM.zonkTcPredType pred2
1012         ; let { pred1'' = tidyPred tidy_env pred1'
1013               ; pred2'' = tidyPred tidy_env pred2' }
1014         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1015                           nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1016                           nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1017         ; return (tidy_env, msg) }
1018 \end{code}