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