TcSimplify.hs 109 KB
Newer Older
1 2
{-# LANGUAGE CPP #-}

3
module TcSimplify(
4
       simplifyInfer, InferMode(..),
5
       growThetaTyVars,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
6
       simplifyAmbiguityCheck,
7
       simplifyDefault,
8
       simplifyTop, simplifyTopImplic, captureTopConstraints,
Richard Eisenberg's avatar
Richard Eisenberg committed
9
       simplifyInteractive, solveEqualities,
10
       simplifyWantedsTcM,
11
       tcCheckSatisfiability,
12
       tcSubsumes,
13
       tcCheckHoleFit,
14

15
       -- For Rules we need these
16 17
       solveWanteds, solveWantedsAndDrop,
       approximateWC, runTcSDeriveds
18
  ) where
19

20
#include "HsVersions.h"
21

22 23
import GhcPrelude

24
import Bag
25
import Class         ( Class, classKey, classTyCon )
26
import DynFlags      ( WarningFlag ( Opt_WarnMonomorphism )
27
                     , WarnReason ( Reason )
28
                     , DynFlags( solverIterations ) )
29
import Id            ( idType )
30
import Inst
31
import ListSetOps
32 33
import Name
import Outputable
34 35
import PrelInfo
import PrelNames
36 37 38
import TcErrors
import TcEvidence
import TcInteract
39
import TcCanonical   ( makeSuperClasses, solveCallStack )
40
import TcMType   as TcM
41
import TcRnMonad as TcM
42 43 44
import TcSMonad  as TcS
import TcType
import TrieMap       () -- DV: for now
45
import Type
Richard Eisenberg's avatar
Richard Eisenberg committed
46
import TysWiredIn    ( liftedRepTy )
Richard Eisenberg's avatar
Richard Eisenberg committed
47
import Unify         ( tcMatchTyKi )
48
import TcUnify       ( tcSubType_NC )
49 50 51
import Util
import Var
import VarSet
David Feuer's avatar
David Feuer committed
52
import UniqSet
53 54
import BasicTypes    ( IntWithInf, intGtLimit )
import ErrUtils      ( emptyMessages )
55
import qualified GHC.LanguageExtensions as LangExt
56

57
import Control.Monad
58 59 60
import Data.Foldable      ( toList )
import Data.List          ( partition )
import Data.List.NonEmpty ( NonEmpty(..) )
61

Austin Seipp's avatar
Austin Seipp committed
62
{-
63
*********************************************************************************
64
*                                                                               *
65 66 67
*                           External interface                                  *
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
68
-}
69

70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
-- (captureTopConstraints m) runs m, and returns the type constraints it
-- generates plus the constraints produced by static forms inside.
-- If it fails with an exception, it reports any insolubles
-- (out of scope variables) before doing so
captureTopConstraints thing_inside
  = do { static_wc_var <- TcM.newTcRef emptyWC ;
       ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
                          TcM.tryCaptureConstraints thing_inside
       ; stWC <- TcM.readTcRef static_wc_var

       -- See TcRnMonad Note [Constraints and errors]
       -- If the thing_inside threw an exception, but generated some insoluble
       -- constraints, report the latter before propagating the exception
       -- Otherwise they will be lost altogether
       ; case mb_res of
           Right res -> return (res, lie `andWC` stWC)
           Left {}   -> do { _ <- reportUnsolved lie; failM } }
                -- This call to reportUnsolved is the reason
                -- this function is here instead of TcRnMonad

91 92 93 94 95 96 97 98 99
simplifyTopImplic :: Bag Implication -> TcM ()
simplifyTopImplic implics
  = do { empty_binds <- simplifyTop (mkImplicWC implics)

       -- Since all the inputs are implications the returned bindings will be empty
       ; MASSERT2( isEmptyBag empty_binds, ppr empty_binds )

       ; return () }

100 101
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
102 103 104
-- Usually these will be implications,
-- but when there is nothing to quantify we don't wrap
-- in a degenerate implication, so we do that here instead
105
simplifyTop wanteds
106
  = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
107 108 109 110
       ; ((final_wc, unsafe_ol), binds1) <- runTcS $
            do { final_wc <- simpl_top wanteds
               ; unsafe_ol <- getSafeOverlapFailures
               ; return (final_wc, unsafe_ol) }
111 112 113
       ; traceTc "End simplifyTop }" empty

       ; traceTc "reportUnsolved {" empty
114
       ; binds2 <- reportUnsolved final_wc
115
       ; traceTc "reportUnsolved }" empty
116

117 118 119 120
       ; traceTc "reportUnsolved (unsafe overlapping) {" empty
       ; unless (isEmptyCts unsafe_ol) $ do {
           -- grab current error messages and clear, warnAllUnsolved will
           -- update error messages which we'll grab and then restore saved
121
           -- messages.
122
           ; errs_var  <- getErrsVar
123 124
           ; saved_msg <- TcM.readTcRef errs_var
           ; TcM.writeTcRef errs_var emptyMessages
125 126 127 128

           ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
                                  , wc_impl = emptyBag }

129 130
           ; whyUnsafe <- fst <$> TcM.readTcRef errs_var
           ; TcM.writeTcRef errs_var saved_msg
131 132 133 134
           ; recordUnsafeInfer whyUnsafe
           }
       ; traceTc "reportUnsolved (unsafe overlapping) }" empty

135 136 137
       ; return (evBindMapBinds binds1 `unionBags` binds2) }

-- | Type-check a thing that emits only equality constraints, then
138
-- solve those constraints. Fails outright if there is trouble.
139 140
solveEqualities :: TcM a -> TcM a
solveEqualities thing_inside
141 142
  = checkNoErrs $  -- See Note [Fail fast on kind errors]
    do { (result, wanted) <- captureConstraints thing_inside
143
       ; traceTc "solveEqualities {" $ text "wanted = " <+> ppr wanted
Simon Peyton Jones's avatar
Simon Peyton Jones committed
144
       ; final_wc <- runTcSEqualities $ simpl_top wanted
145 146 147 148 149 150
       ; traceTc "End solveEqualities }" empty

       ; traceTc "reportAllUnsolved {" empty
       ; reportAllUnsolved final_wc
       ; traceTc "reportAllUnsolved }" empty
       ; return result }
151

Simon Peyton Jones's avatar
Simon Peyton Jones committed
152
simpl_top :: WantedConstraints -> TcS WantedConstraints
153
    -- See Note [Top-level Defaulting Plan]
154
simpl_top wanteds
155
  = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
156
                            -- This is where the main work happens
Simon Peyton Jones's avatar
Simon Peyton Jones committed
157
       ; try_tyvar_defaulting wc_first_go }
158
  where
159 160
    try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
    try_tyvar_defaulting wc
161
      | isEmptyWC wc
162 163
      = return wc
      | otherwise
164 165
      = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
           ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
166
                   -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
167
                   -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
168
                   -- and we definitely don't want to try to assign to those!
169
                   -- The isTyVar is needed to weed out coercion variables
170

171 172 173
           ; defaulted <- mapM defaultTyVarTcS meta_tvs   -- Has unification side effects
           ; if or defaulted
             then do { wc_residual <- nestTcS (solveWanteds wc)
174
                            -- See Note [Must simplify after defaulting]
175 176
                     ; try_class_defaulting wc_residual }
             else try_class_defaulting wc }     -- No defaulting took place
177

178 179
    try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
    try_class_defaulting wc
Austin Seipp's avatar
Austin Seipp committed
180
      | isEmptyWC wc
181 182
      = return wc
      | otherwise  -- See Note [When to do type-class defaulting]
183
      = do { something_happened <- applyDefaultingRules wc
184
                                   -- See Note [Top-level Defaulting Plan]
185
           ; if something_happened
186
             then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
187
                     ; try_class_defaulting wc_residual }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
188
                  -- See Note [Overview of implicit CallStacks] in TcEvidence
189 190 191 192 193 194 195 196 197 198 199 200 201 202
             else try_callstack_defaulting wc }

    try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
    try_callstack_defaulting wc
      | isEmptyWC wc
      = return wc
      | otherwise
      = defaultCallStacks wc

-- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
-- See Note [Overview of implicit CallStacks] in TcEvidence
defaultCallStacks wanteds
  = do simples <- handle_simples (wc_simple wanteds)
203 204 205
       mb_implics <- mapBagM handle_implic (wc_impl wanteds)
       return (wanteds { wc_simple = simples
                       , wc_impl = catBagMaybes mb_implics })
206 207 208 209 210 211

  where

  handle_simples simples
    = catBagMaybes <$> mapBagM defaultCallStack simples

212 213 214
  handle_implic :: Implication -> TcS (Maybe Implication)
  -- The Maybe is because solving the CallStack constraint
  -- may well allow us to discard the implication entirely
215
  handle_implic implic
216 217 218
    | isSolvedStatus (ic_status implic)
    = return (Just implic)
    | otherwise
219 220 221 222
    = do { wanteds <- setEvBindsTcS (ic_binds implic) $
                      -- defaultCallStack sets a binding, so
                      -- we must set the correct binding group
                      defaultCallStacks (ic_wanted implic)
223
         ; setImplicationStatus (implic { ic_wanted = wanteds }) }
224 225

  defaultCallStack ct
226 227
    | ClassPred cls tys <- classifyPredType (ctPred ct)
    , Just {} <- isCallStackPred cls tys
228 229 230 231 232
    = do { solveCallStack (cc_ev ct) EvCsEmpty
         ; return Nothing }

  defaultCallStack ct
    = return (Just ct)
233

234

235 236 237 238 239
{- Note [Fail fast on kind errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solveEqualities is used to solve kind equalities when kind-checking
user-written types. If solving fails we should fail outright, rather
than just accumulate an error message, for two reasons:
Simon Peyton Jones's avatar
Simon Peyton Jones committed
240

241 242 243
  * A kind-bogus type signature may cause a cascade of knock-on
    errors if we let it pass

Simon Peyton Jones's avatar
Simon Peyton Jones committed
244 245 246 247 248
  * More seriously, we don't have a convenient term-level place to add
    deferred bindings for unsolved kind-equality constraints, so we
    don't build evidence bindings (by usine reportAllUnsolved). That
    means that we'll be left with with a type that has coercion holes
    in it, something like
249 250 251 252 253 254 255
           <type> |> co-hole
    where co-hole is not filled in.  Eeek!  That un-filled-in
    hole actually causes GHC to crash with "fvProv falls into a hole"
    See Trac #11563, #11520, #11516, #11399

So it's important to use 'checkNoErrs' here!

256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
Note [When to do type-class defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
was false, on the grounds that defaulting can't help solve insoluble
constraints.  But if we *don't* do defaulting we may report a whole
lot of errors that would be solved by defaulting; these errors are
quite spurious because fixing the single insoluble error means that
defaulting happens again, which makes all the other errors go away.
This is jolly confusing: Trac #9033.

So it seems better to always do type-class defaulting.

However, always doing defaulting does mean that we'll do it in
situations like this (Trac #5934):
   run :: (forall s. GenST s) -> Int
Austin Seipp's avatar
Austin Seipp committed
271
   run = fromInteger 0
272 273 274
We don't unify the return type of fromInteger with the given function
type, because the latter involves foralls.  So we're left with
    (Num alpha, alpha ~ (forall s. GenST s) -> Int)
Austin Seipp's avatar
Austin Seipp committed
275 276
Now we do defaulting, get alpha := Integer, and report that we can't
match Integer with (forall s. GenST s) -> Int.  That's not totally
277 278 279 280 281 282
stupid, but perhaps a little strange.

Another potential alternative would be to suppress *all* non-insoluble
errors if there are *any* insoluble errors, anywhere, but that seems
too drastic.

283 284 285 286 287 288 289 290 291
Note [Must simplify after defaulting]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We may have a deeply buried constraint
    (t:*) ~ (a:Open)
which we couldn't solve because of the kind incompatibility, and 'a' is free.
Then when we default 'a' we can solve the constraint.  And we want to do
that before starting in on type classes.  We MUST do it before reporting
errors, because it isn't an error!  Trac #7967 was due to this.

292 293
Note [Top-level Defaulting Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
294 295
We have considered two design choices for where/when to apply defaulting.
   (i) Do it in SimplCheck mode only /whenever/ you try to solve some
296
       simple constraints, maybe deep inside the context of implications.
297
       This used to be the case in GHC 7.4.1.
298
   (ii) Do it in a tight loop at simplifyTop, once all other constraints have
299 300
        finished. This is the current story.

301
Option (i) had many disadvantages:
302 303
   a) Firstly, it was deep inside the actual solver.
   b) Secondly, it was dependent on the context (Infer a type signature,
304 305
      or Check a type signature, or Interactive) since we did not want
      to always start defaulting when inferring (though there is an exception to
306
      this, see Note [Default while Inferring]).
307 308 309 310 311 312 313 314 315 316 317
   c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
          f :: Int -> Bool
          f x = const True (\y -> let w :: a -> a
                                      w a = const a (y+1)
                                  in w y)
      We will get an implication constraint (for beta the type of y):
               [untch=beta] forall a. 0 => Num beta
      which we really cannot default /while solving/ the implication, since beta is
      untouchable.

Instead our new defaulting story is to pull defaulting out of the solver loop and
318
go with option (ii), implemented at SimplifyTop. Namely:
319 320
     - First, have a go at solving the residual constraint of the whole
       program
321 322
     - Try to approximate it with a simple constraint
     - Figure out derived defaulting equations for that simple constraint
323 324 325 326
     - Go round the loop again if you did manage to get some equations

Now, that has to do with class defaulting. However there exists type variable /kind/
defaulting. Again this is done at the top-level and the plan is:
327
     - At the top-level, once you had a go at solving the constraint, do
Gabor Greif's avatar
Gabor Greif committed
328
       figure out /all/ the touchable unification variables of the wanted constraints.
329 330 331
     - Apply defaulting to their kinds

More details in Note [DefaultTyVar].
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374

Note [Safe Haskell Overlapping Instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Safe Haskell, we apply an extra restriction to overlapping instances. The
motive is to prevent untrusted code provided by a third-party, changing the
behavior of trusted code through type-classes. This is due to the global and
implicit nature of type-classes that can hide the source of the dictionary.

Another way to state this is: if a module M compiles without importing another
module N, changing M to import N shouldn't change the behavior of M.

Overlapping instances with type-classes can violate this principle. However,
overlapping instances aren't always unsafe. They are just unsafe when the most
selected dictionary comes from untrusted code (code compiled with -XSafe) and
overlaps instances provided by other modules.

In particular, in Safe Haskell at a call site with overlapping instances, we
apply the following rule to determine if it is a 'unsafe' overlap:

 1) Most specific instance, I1, defined in an `-XSafe` compiled module.
 2) I1 is an orphan instance or a MPTC.
 3) At least one overlapped instance, Ix, is both:
    A) from a different module than I1
    B) Ix is not marked `OVERLAPPABLE`

This is a slightly involved heuristic, but captures the situation of an
imported module N changing the behavior of existing code. For example, if
condition (2) isn't violated, then the module author M must depend either on a
type-class or type defined in N.

Secondly, when should these heuristics be enforced? We enforced them when the
type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.
This allows `-XUnsafe` modules to operate without restriction, and for Safe
Haskell inferrence to infer modules with unsafe overlaps as unsafe.

One alternative design would be to also consider if an instance was imported as
a `safe` import or not and only apply the restriction to instances imported
safely. However, since instances are global and can be imported through more
than one path, this alternative doesn't work.

Note [Safe Haskell Overlapping Instances Implementation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

375
How is this implemented? It's complicated! So we'll step through it all:
376 377

 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
378 379 380 381
    we check if a particular type-class method call is safe or unsafe. We do this
    through the return type, `ClsInstLookupResult`, where the last parameter is a
    list of instances that are unsafe to overlap. When the method call is safe,
    the list is null.
382

383
 2) `TcInteract.matchClassInst` -- This module drives the instance resolution
Simon Peyton Jones's avatar
Simon Peyton Jones committed
384 385 386
    / dictionary generation. The return type is `LookupInstResult`, which either
    says no instance matched, or one found, and if it was a safe or unsafe
    overlap.
387 388

 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and
Simon Peyton Jones's avatar
Simon Peyton Jones committed
389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
     tries to resolve it by calling (in part) `matchClassInst`. The resolving
     mechanism has a work list (of constraints) that it process one at a time. If
     the constraint can't be resolved, it's added to an inert set. When compiling
     an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know
     compilation should fail. These are handled as normal constraint resolution
     failures from here-on (see step 6).

     Otherwise, we may be inferring safety (or using `-Wunsafe`), and
     compilation should succeed, but print warnings and/or mark the compiled module
     as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
     the unsafe (but resolved!) constraint to the `inert_safehask` field of
     `InertCans`.

 4) `TcSimplify.simplifyTop`:
       * Call simpl_top, the top-level function for driving the simplifier for
         constraint resolution.

       * Once finished, call `getSafeOverlapFailures` to retrieve the
         list of overlapping instances that were successfully resolved,
         but unsafe. Remember, this is only applicable for generating warnings
         (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
         cause compilation failure by not resolving the unsafe constraint at all.

       * For unresolved constraints (all types), call `TcErrors.reportUnsolved`,
         while for resolved but unsafe overlapping dictionary constraints, call
         `TcErrors.warnAllUnsolved`. Both functions convert constraints into a
         warning message for the user.

       * In the case of `warnAllUnsolved` for resolved, but unsafe
         dictionary constraints, we collect the generated warning
         message (pop it) and call `TcRnMonad.recordUnsafeInfer` to
         mark the module we are compiling as unsafe, passing the
         warning message along as the reason.

 5) `TcErrors.*Unsolved` -- Generates error messages for constraints by
    actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
    know is the constraint that is unresolved or unsafe. For dictionary, all we
    know is that we need a dictionary of type C, but not what instances are
    available and how they overlap. So we once again call `lookupInstEnv` to
    figure that out so we can generate a helpful error message.

 6) `TcRnMonad.recordUnsafeInfer` -- Save the unsafe result and reason in an
      IORef called `tcg_safeInfer`.

 7) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling
    `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence
    failed.
436 437 438 439 440 441 442 443 444 445

Note [No defaulting in the ambiguity check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When simplifying constraints for the ambiguity check, we use
solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
Trac #11947 was an example:
   f :: Num a => Int -> Int
This is ambiguous of course, but we don't want to default the
(Num alpha) constraint to (Num Int)!  Doing so gives a defaulting
warning, but no error.
Austin Seipp's avatar
Austin Seipp committed
446
-}
447

448
------------------
449 450 451
simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
simplifyAmbiguityCheck ty wanteds
  = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
452 453 454
       ; (final_wc, _) <- runTcS $ solveWantedsAndDrop wanteds
             -- NB: no defaulting!  See Note [No defaulting in the ambiguity check]

455 456 457 458 459
       ; traceTc "End simplifyAmbiguityCheck }" empty

       -- Normally report all errors; but with -XAllowAmbiguousTypes
       -- report only insoluble ones, since they represent genuinely
       -- inaccessible code
460
       ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
461
       ; traceTc "reportUnsolved(ambig) {" empty
462
       ; unless (allow_ambiguous && not (insolubleWC final_wc))
463
                (discardResult (reportUnsolved final_wc))
464 465 466 467
       ; traceTc "reportUnsolved(ambig) }" empty

       ; return () }

468 469
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
470
simplifyInteractive wanteds
471
  = traceTc "simplifyInteractive" empty >>
472
    simplifyTop wanteds
473 474

------------------
475
simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
476
                -> TcM ()       -- Succeeds if the constraint is soluble
477
simplifyDefault theta
478
  = do { traceTc "simplifyDefault" empty
479 480
       ; wanteds  <- newWanteds DefaultOrigin theta
       ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
481
       ; traceTc "reportUnsolved {" empty
482
       ; reportAllUnsolved unsolved
483
       ; traceTc "reportUnsolved }" empty
484
       ; return () }
485

486 487 488 489 490 491
-- | Reports whether first type (ty_a) subsumes the second type (ty_b),
-- discarding any errors. Subsumption here means that the ty_b can fit into the
-- ty_a, i.e. `tcSubsumes a b == True` if b is a subtype of a.
-- N.B.: Make sure that the types contain all the constraints
-- contained in any associated implications.
tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
492 493 494 495 496 497 498 499 500
tcSubsumes = tcCheckHoleFit emptyBag


-- | A tcSubsumes which takes into account relevant constraints, to fix trac
-- #14273. Make sure that the constraints are cloned, since the simplifier may
-- perform unification
tcCheckHoleFit :: Cts -> TcSigmaType -> TcSigmaType -> TcM Bool
tcCheckHoleFit _ hole_ty ty | hole_ty `eqType` ty = return True
tcCheckHoleFit relevantCts hole_ty ty = discardErrs $
501
 do {  (_, wanted, _) <- pushLevelAndCaptureConstraints $
502 503
                           tcSubType_NC ExprSigCtxt ty hole_ty
    ; (rem, _) <- runTcS (simpl_top $ addSimples wanted relevantCts)
504 505 506
    -- We don't want any insoluble or simple constraints left,
    -- but solved implications are ok (and neccessary for e.g. undefined)
    ; return (isEmptyBag (wc_simple rem)
507
              && allBag (isSolvedStatus . ic_status) (wc_impl rem))
508 509
    }

510 511 512
------------------
tcCheckSatisfiability :: Bag EvVar -> TcM Bool
-- Return True if satisfiable, False if definitely contradictory
513
tcCheckSatisfiability given_ids
514
  = do { lcl_env <- TcM.getLclEnv
515 516
       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
       ; (res, _ev_binds) <- runTcS $
517
             do { traceTcS "checkSatisfiability {" (ppr given_ids)
518
                ; let given_cts = mkGivens given_loc (bagToList given_ids)
519
                     -- See Note [Superclasses and satisfiability]
520 521
                ; solveSimpleGivens given_cts
                ; insols <- getInertInsols
522 523 524 525
                ; insols <- try_harder insols
                ; traceTcS "checkSatisfiability }" (ppr insols)
                ; return (isEmptyBag insols) }
       ; return res }
526
 where
527 528 529
    try_harder :: Cts -> TcS Cts
    -- Maybe we have to search up the superclass chain to find
    -- an unsatisfiable constraint.  Example: pmcheck/T3927b.
530
    -- At the moment we try just once
531 532 533 534 535 536
    try_harder insols
      | not (isEmptyBag insols)   -- We've found that it's definitely unsatisfiable
      = return insols             -- Hurrah -- stop now.
      | otherwise
      = do { pending_given <- getPendingScDicts
           ; new_given <- makeSuperClasses pending_given
537 538
           ; solveSimpleGivens new_given
           ; getInertInsols }
539

540
{- Note [Superclasses and satisfiability]
541 542 543 544 545 546 547 548 549 550 551 552 553
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand superclasses before starting, because (Int ~ Bool), has
(Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
as a superclass, and it's the latter that is insoluble.  See
Note [The equality types story] in TysPrim.

If we fail to prove unsatisfiability we (arbitrarily) try just once to
find superclasses, using try_harder.  Reason: we might have a type
signature
   f :: F op (Implements push) => ..
where F is a type function.  This happened in Trac #3972.

We could do more than once but we'd have to have /some/ limit: in the
554
the recursive case, we would go on forever in the common case where
555 556 557 558 559
the constraints /are/ satisfiable (Trac #10592 comment:12!).

For stratightforard situations without type functions the try_harder
step does nothing.

560

561
***********************************************************************************
562
*                                                                                 *
563 564 565
*                            Inference
*                                                                                 *
***********************************************************************************
566

567 568 569 570 571 572 573 574
Note [Inferring the type of a let-bound variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   f x = rhs

To infer f's type we do the following:
 * Gather the constraints for the RHS with ambient level *one more than*
   the current one.  This is done by the call
575
        pushLevelAndCaptureConstraints (tcMonoBinds...)
576 577 578 579
   in TcBinds.tcPolyInfer

 * Call simplifyInfer to simplify the constraints and decide what to
   quantify over. We pass in the level used for the RHS constraints,
580
   here called rhs_tclvl.
581 582 583 584

This ensures that the implication constraint we generate, if any,
has a strictly-increased level compared to the ambient level outside
the let binding.
585

Austin Seipp's avatar
Austin Seipp committed
586
-}
587

588 589 590 591 592 593 594 595 596 597 598 599 600 601
-- | How should we choose which constraints to quantify over?
data InferMode = ApplyMR          -- ^ Apply the monomorphism restriction,
                                  -- never quantifying over any constraints
               | EagerDefaulting  -- ^ See Note [TcRnExprMode] in TcRnDriver,
                                  -- the :type +d case; this mode refuses
                                  -- to quantify over any defaultable constraint
               | NoRestrictions   -- ^ Quantify over any constraint that
                                  -- satisfies TcType.pickQuantifiablePreds

instance Outputable InferMode where
  ppr ApplyMR         = text "ApplyMR"
  ppr EagerDefaulting = text "EagerDefaulting"
  ppr NoRestrictions  = text "NoRestrictions"

602
simplifyInfer :: TcLevel               -- Used when generating the constraints
603
              -> InferMode
604
              -> [TcIdSigInst]         -- Any signatures (possibly partial)
605 606
              -> [(Name, TcTauType)]   -- Variables to be generalised,
                                       -- and their tau-types
607
              -> WantedConstraints
608
              -> TcM ([TcTyVar],    -- Quantify over these type variables
609
                      [EvVar],      -- ... and these constraints (fully zonked)
610 611 612
                      TcEvBinds,    -- ... binding these evidence variables
                      Bool)         -- True <=> there was an insoluble type error
                                    --          in these bindings
613
simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
614
  | isEmptyWC wanteds
615
  = do { gbl_tvs <- tcGetGlobalTyCoVars
616
       ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
617
       ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
618
       ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
619
       ; return (qtkvs, [], emptyTcEvBinds, False) }
620

621
  | otherwise
622
  = do { traceTc "simplifyInfer {"  $ vcat
623 624 625
             [ text "sigs =" <+> ppr sigs
             , text "binds =" <+> ppr name_taus
             , text "rhs_tclvl =" <+> ppr rhs_tclvl
626
             , text "infer_mode =" <+> ppr infer_mode
627
             , text "(unzonked) wanted =" <+> ppr wanteds
628 629
             ]

630 631
       ; let partial_sigs = filter isPartialSig sigs
             psig_theta   = concatMap sig_inst_theta partial_sigs
632

633 634 635 636 637 638 639
       -- First do full-blown solving
       -- NB: we must gather up all the bindings from doing
       -- this solving; hence (runTcSWithEvBinds ev_binds_var).
       -- And note that since there are nested implications,
       -- calling solveWanteds will side-effect their evidence
       -- bindings, so we can't just revert to the input
       -- constraint.
640

641 642 643 644 645
       ; tc_lcl_env      <- TcM.getLclEnv
       ; ev_binds_var    <- TcM.newTcEvBinds
       ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
       ; wanted_transformed_incl_derivs
            <- setTcLevel rhs_tclvl $
646
               runTcSWithEvBinds ev_binds_var $
647
               do { let loc         = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env
648
                        psig_givens = mkGivens loc psig_theta_vars
649 650
                  ; _ <- solveSimpleGivens psig_givens
                         -- See Note [Add signature contexts as givens]
651 652
                  ; wanteds' <- solveWanteds wanteds
                  ; TcS.zonkWC wanteds' }
653

654

655 656
       -- Find quant_pred_candidates, the predicates that
       -- we'll consider quantifying over
657 658 659 660
       -- NB1: wanted_transformed does not include anything provable from
       --      the psig_theta; it's just the extra bit
       -- NB2: We do not do any defaulting when inferring a type, this can lead
       --      to less polymorphic types, see Note [Default while Inferring]
661 662 663 664 665 666 667 668
       ; let definite_error = insolubleWC wanted_transformed_incl_derivs
                              -- See Note [Quantification with errors]
                              -- NB: must include derived errors in this test,
                              --     hence "incl_derivs"
             wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
             quant_pred_candidates
               | definite_error = []
               | otherwise      = ctsPreds (approximateWC False wanted_transformed)
669

670
       -- Decide what type variables and constraints to quantify
671
       -- NB: quant_pred_candidates is already fully zonked
672
       -- NB: bound_theta are constraints we want to quantify over,
673 674
       --     including the psig_theta, which we always quantify over
       -- NB: bound_theta are fully zonked
675
       ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
676
                                                     name_taus partial_sigs
677
                                                     quant_pred_candidates
678
       ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
679

680 681 682 683 684 685 686 687 688 689 690
       -- We must produce bindings for the psig_theta_vars, because we may have
       -- used them in evidence bindings constructed by solveWanteds earlier
       -- Easiest way to do this is to emit them as new Wanteds (Trac #14643)
       ; ct_loc <- getCtLocM AnnOrigin Nothing
       ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
                                      , ctev_dest = EvVarDest psig_theta_var
                                      , ctev_nosh = WDeriv
                                      , ctev_loc  = ct_loc }
                           | psig_theta_var <- psig_theta_vars ]

       -- Now we can emil the residual constraints
691 692
       ; emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
                                 name_taus co_vars qtvs
693 694
                                 bound_theta_vars
                                 (wanted_transformed `andWC` mkSimpleWC psig_wanted)
695

696
         -- All done!
697
       ; traceTc "} simplifyInfer/produced residual implication for quantification" $
698
         vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
699
              , text "psig_theta =" <+> ppr psig_theta
700
              , text "bound_theta =" <+> ppr bound_theta
701
              , text "qtvs ="       <+> ppr qtvs
702
              , text "definite_error =" <+> ppr definite_error ]
703

704 705
       ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
         -- NB: bound_theta_vars must be fully zonked
706

707

708
--------------------
709 710 711
emitResidualConstraints :: TcLevel -> TcLclEnv -> EvBindsVar
                        -> [(Name, TcTauType)]
                        -> VarSet -> [TcTyVar] -> [EvVar]
712
                        -> WantedConstraints -> TcM ()
713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738
-- Emit the remaining constraints from the RHS.
-- See Note [Emitting the residual implication in simplifyInfer]
emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
                        name_taus co_vars qtvs full_theta_vars wanteds
  | isEmptyWC wanteds
  = return ()
  | otherwise
  = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
       ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
             is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars

        ; tc_lvl <- TcM.getTcLevel
        ; mapM_ (promoteTyVar tc_lvl) (tyCoVarsOfCtsList outer_simple)

        ; unless (isEmptyCts outer_simple) $
          do { traceTc "emitResidualConstrants:simple" (ppr outer_simple)
             ; emitSimples outer_simple }

        ; let inner_wanted = wanteds { wc_simple = inner_simple }
              implic       = mk_implic inner_wanted
        ; unless (isEmptyWC inner_wanted) $
          do { traceTc "emitResidualConstraints:implic" (ppr implic)
             ; emitImplication implic }
     }
  where
    mk_implic inner_wanted
739 740 741 742 743 744 745
       = newImplication { ic_tclvl    = rhs_tclvl
                        , ic_skols    = qtvs
                        , ic_given    = full_theta_vars
                        , ic_wanted   = inner_wanted
                        , ic_binds    = ev_binds_var
                        , ic_info     = skol_info
                        , ic_env      = tc_lcl_env }
746 747 748 749 750 751 752

    full_theta = map idType full_theta_vars
    skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
                           | (name, ty) <- name_taus ]
                 -- Don't add the quantified variables here, because
                 -- they are also bound in ic_skols and we want them
                 -- to be tidied uniformly
753 754

--------------------
755 756 757 758
ctsPreds :: Cts -> [PredType]
ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
                             , let ev = ctEvidence ct ]

759 760 761 762
{- Note [Emitting the residual implication in simplifyInfer]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   f = e
Richard Eisenberg's avatar
Richard Eisenberg committed
763
where f's type is inferred to be something like (a, Proxy k (Int |> co))
764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787
and we have an as-yet-unsolved, or perhaps insoluble, constraint
   [W] co :: Type ~ k
We can't form types like (forall co. blah), so we can't generalise over
the coercion variable, and hence we can't generalise over things free in
its kind, in the case 'k'.  But we can still generalise over 'a'.  So
we'll generalise to
   f :: forall a. (a, Proxy k (Int |> co))
Now we do NOT want to form the residual implication constraint
   forall a. [W] co :: Type ~ k
because then co's eventual binding (which will be a value binding if we
use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
type mentions 'co').  Instead, just as we don't generalise over 'co', we
should not bury its constraint inside the implication.  Instead, we must
put it outside.

That is the reason for the partitionBag in emitResidualConstraints,
which takes the CoVars free in the inferred type, and pulls their
constraints out.  (NB: this set of CoVars should be
closed-over-kinds.)

All rather subtle; see Trac #14584.

Note [Add signature contexts as givens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
788 789 790
Consider this (Trac #11016):
  f2 :: (?x :: Int) => _
  f2 = ?x
791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806
or this
  f3 :: a ~ Bool => (a, _)
  f3 = (True, False)
or theis
  f4 :: (Ord a, _) => a -> Bool
  f4 x = x==x

We'll use plan InferGen because there are holes in the type.  But:
 * For f2 we want to have the (?x :: Int) constraint floating around
   so that the functional dependencies kick in.  Otherwise the
   occurrence of ?x on the RHS produces constraint (?x :: alpha), and
   we won't unify alpha:=Int.
 * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool)
   in the RHS
 * For f4 we want to use the (Ord a) in the signature to solve the Eq a
   constraint.
807 808

Solution: in simplifyInfer, just before simplifying the constraints
809 810
gathered from the RHS, add Given constraints for the context of any
type signatures.
811

Austin Seipp's avatar
Austin Seipp committed
812 813
************************************************************************
*                                                                      *
814
                Quantification
Austin Seipp's avatar
Austin Seipp committed
815 816
*                                                                      *
************************************************************************
817 818 819 820

Note [Deciding quantification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the monomorphism restriction does not apply, then we quantify as follows:
821

822 823 824
* Step 1. Take the global tyvars, and "grow" them using the equality
  constraints
     E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
825
          happen because alpha is untouchable here) then do not quantify over
826 827
          beta, because alpha fixes beta, and beta is effectively free in
          the environment too
828

829 830 831 832 833 834 835 836 837 838 839 840
  We also account for the monomorphism restriction; if it applies,
  add the free vars of all the constraints.

  Result is mono_tvs; we will not quantify over these.

* Step 2. Default any non-mono tyvars (i.e ones that are definitely
  not going to become further constrained), and re-simplify the
  candidate constraints.

  Motivation for re-simplification (Trac #7857): imagine we have a
  constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
  not free in the envt, and instance forall (a::*) (b::*). (C a) => C
Gabor Greif's avatar
Gabor Greif committed
841
  (a -> b) The instance doesn't match while l1,l2 are polymorphic, but
842 843 844
  it will match when we default them to LiftedRep.

  This is all very tiresome.
845

846 847 848 849 850 851
* Step 3: decide which variables to quantify over, as follows:

  - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
    them using all the constraints.  These are tau_tvs_plus

  - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
852 853
    careful to close over kinds, and to skolemise the quantified tyvars.
    (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
854

855
  Result is qtvs.
856

857 858 859
* Step 4: Filter the constraints using pickQuantifiablePreds and the
  qtvs. We have to zonk the constraints first, so they "see" the
  freshly created skolems.
860

Austin Seipp's avatar
Austin Seipp committed
861
-}
862

863
decideQuantification
864
  :: InferMode
865
  -> TcLevel
866
  -> [(Name, TcTauType)]   -- Variables to be generalised
867
  -> [TcIdSigInst]         -- Partial type signatures (if any)
868
  -> [PredType]            -- Candidate theta; already zonked
869
  -> TcM ( [TcTyVar]       -- Quantify over these (skolems)
870 871
         , [PredType]      -- and this context (fully zonked)
         , VarSet)
872
-- See Note [Deciding quantification]
873
decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
874
  = do { -- Step 1: find the mono_tvs
875 876
       ; (mono_tvs, candidates) <- decideMonoTyVars infer_mode
                                        name_taus psigs candidates
877 878

       -- Step 2: default any non-mono tyvars, and re-simplify
879
       -- This step may do some unification, but result candidates is zonked
880 881 882
       ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates

       -- Step 3: decide which kind/type variables to quantify over
883
       ; (qtvs, co_vars) <- decideQuantifiedTyVars mono_tvs name_taus psigs candidates
884 885 886 887 888

       -- Step 4: choose which of the remaining candidate
       --         predicates to actually quantify over
       -- NB: decideQuantifiedTyVars turned some meta tyvars
       -- into quantified skolems, so we have to zonk again
Simon Peyton Jones's avatar
Simon Peyton Jones committed
889 890 891 892 893 894 895 896 897 898
       ; candidates <- TcM.zonkTcTypes candidates
       ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
       ; let quantifiable_candidates
               = pickQuantifiablePreds (mkVarSet qtvs) candidates
             -- NB: do /not/ run pickQuantifieablePreds over psig_theta,
             -- because we always want to quantify over psig_theta, and not
             -- drop any of them; e.g. CallStack constraints.  c.f Trac #14658

             theta = mkMinimalBySCs id $  -- See Note [Minimize by Superclasses]
                     (psig_theta ++ quantifiable_candidates)
899 900

       ; traceTc "decideQuantification"
Simon Peyton Jones's avatar
Simon Peyton Jones committed
901 902 903 904 905 906 907
           (vcat [ text "infer_mode:" <+> ppr infer_mode
                 , text "candidates:" <+> ppr candidates
                 , text "psig_theta:" <+> ppr psig_theta
                 , text "mono_tvs:"   <+> ppr mono_tvs
                 , text "co_vars:"    <+> ppr co_vars
                 , text "qtvs:"       <+> ppr qtvs
                 , text "theta:"      <+> ppr theta ])
908
       ; return (qtvs, theta, co_vars) }
909 910

------------------
911
decideMonoTyVars :: InferMode
912
                 -> [(Name,TcType)]
913 914
                 -> [TcIdSigInst]
                 -> [PredType]
915
                 -> TcM (TcTyCoVarSet, [PredType])
916
-- Decide which tyvars and covars cannot be generalised:
917 918 919 920
--   (a) Free in the environment
--   (b) Mentioned in a constraint we can't generalise
--   (c) Connected by an equality to (a) or (b)
-- Also return the reduced set of constraint we can generalise
921
decideMonoTyVars infer_mode name_taus psigs candidates
922 923 924 925 926 927
  = do { (no_quant, maybe_quant) <- pick infer_mode candidates

       -- If possible, we quantify over partial-sig qtvs, so they are
       -- not mono. Need to zonk them because they are meta-tyvar SigTvs
       ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
                      concatMap (map snd . sig_inst_skols) psigs
928

929 930 931
       ; mono_tvs0 <- tcGetGlobalTyCoVars
       ; let eq_constraints = filter isEqPred candidates
             mono_tvs1     = growThetaTyVars eq_constraints mono_tvs0
932 933

             constrained_tvs = (growThetaTyVars eq_constraints
934
                                               (tyCoVarsOfTypes no_quant)
935 936 937 938 939
                                `minusVarSet` mono_tvs1)
                               `delVarSetList` psig_qtvs
             -- constrained_tvs: the tyvars that we are not going to
             -- quantify solely because of the moonomorphism restriction
             --
940
             -- (`minusVarSet` mono_tvs1`): a type variable is only
941 942 943 944 945 946 947 948 949 950 951
             --   "constrained" (so that the MR bites) if it is not
             --   free in the environment (Trac #13785)
             --
             -- (`delVarSetList` psig_qtvs): if the user has explicitly
             --   asked for quantification, then that request "wins"
             --   over the MR.  Note: do /not/ delete psig_qtvs from
             --   mono_tvs1, because mono_tvs1 cannot under any circumstances
             --   be quantified (Trac #14479); see
             --   Note [Quantification and partial signatures], Wrinkle 3, 4

             mono_tvs = mono_tvs1 `unionVarSet` constrained_tvs
952 953 954 955 956 957

           -- Warn about the monomorphism restriction
       ; warn_mono <- woptM Opt_WarnMonomorphism
       ; when (case infer_mode of { ApplyMR -> warn_mono; _ -> False}) $
         do { taus <- mapM (TcM.zonkTcType . snd) name_taus
            ; warnTc (Reason Opt_WarnMonomorphism)
958 959
                (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus)
                mr_msg }
960

961
       ; traceTc "decideMonoTyVars" $ vcat
962 963
           [ text "mono_tvs0 =" <+> ppr mono_tvs0
           , text "mono_tvs1 =" <+> ppr mono_tvs1
964
           , text "no_quant =" <+> ppr no_quant
965
           , text "maybe_quant =" <+> ppr maybe_quant
966 967 968
           , text "eq_constraints =" <+> ppr eq_constraints
           , text "mono_tvs =" <+> ppr mono_tvs ]

969
       ; return (mono_tvs, maybe_quant) }
970 971 972 973 974 975 976 977 978
  where
    pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
    -- Split the candidates into ones we definitely
    -- won't quantify, and ones that we might
    pick NoRestrictions  cand = return ([], cand)
    pick ApplyMR         cand = return (cand, [])
    pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
                                   ; return (partition (is_int_ct os) cand) }

979 980
    -- For EagerDefaulting, do not quantify over
    -- over any interactive class constraint
981 982 983 984 985 986 987
    is_int_ct ovl_strings pred
      | Just (cls, _) <- getClassPredTys_maybe pred
      = isInteractiveClass ovl_strings cls
      | otherwise
      = False

    pp_bndrs = pprWithCommas (quotes . ppr . fst) name_taus
988 989 990 991 992 993 994
    mr_msg =
         hang (sep [ text "The Monomorphism Restriction applies to the binding"
                     <> plural name_taus
                   , text "for" <+> pp_bndrs ])
            2 (hsep [ text "Consider giving"
                    , text (if isSingleton name_taus then "it" else "them")
                    , text "a type signature"])
995 996 997 998 999

-------------------
defaultTyVarsAndSimplify :: TcLevel
                         -> TyCoVarSet
                         -> [PredType]          -- Assumed zonked
1000
                         -> TcM [PredType]      -- Guaranteed zonked
1001
-- Default any tyvar free in the constraints,
Gabor Greif's avatar
Gabor Greif committed
1002
-- and re-simplify in case the defaulting allows further simplification
1003
defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
1004 1005 1006 1007 1008 1009 1010 1011 1012 1013