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

3
module TcSimplify(
Austin Seipp's avatar
Austin Seipp committed
4
       simplifyInfer,
5
       pickQuantifiablePreds, growThetaTyVars,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
6
       simplifyAmbiguityCheck,
7
       simplifyDefault,
8 9 10 11 12
       simplifyTop, simplifyInteractive,
       solveWantedsTcM,

       -- For Rules we need these twoo
       solveWanteds, runTcS
13
  ) where
14

15
#include "HsVersions.h"
16

17
import Bag
18 19 20
import Class         ( classKey )
import Class         ( Class )
import DynFlags      ( ExtensionFlag( Opt_AllowAmbiguousTypes
21 22
                                    , Opt_FlexibleContexts )
                     , DynFlags( solverIterations ) )
23
import Inst
24 25
import Id            ( idType )
import Kind          ( isKind, isSubKind, defaultKind_maybe )
26
import ListSetOps
27 28 29
import Maybes        ( isNothing )
import Name
import Outputable
30 31
import PrelInfo
import PrelNames
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
import TcErrors
import TcEvidence
import TcInteract
import TcMType   as TcM
import TcRnMonad as TcRn
import TcSMonad  as TcS
import TcType
import TrieMap       () -- DV: for now
import TyCon         ( isTypeFamilyTyCon )
import Type          ( classifyPredType, isIPClass, PredTree(..)
                     , getClassPredTys_maybe, EqRel(..) )
import Unify         ( tcMatchTy )
import Util
import Var
import VarSet
47 48 49
import BasicTypes    ( IntWithInf, intGtLimit )
import ErrUtils      ( emptyMessages )
import FastString
50 51 52

import Control.Monad ( unless )
import Data.List     ( partition )
53

Austin Seipp's avatar
Austin Seipp committed
54
{-
55
*********************************************************************************
56
*                                                                               *
57 58 59
*                           External interface                                  *
*                                                                               *
*********************************************************************************
Austin Seipp's avatar
Austin Seipp committed
60
-}
61

62 63
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
64 65 66
-- 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
67
simplifyTop wanteds
68
  = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
69
       ; ((final_wc, unsafe_ol), binds1) <- runTcS $ simpl_top wanteds
70 71 72
       ; traceTc "End simplifyTop }" empty

       ; traceTc "reportUnsolved {" empty
73
       ; binds2 <- reportUnsolved final_wc
74
       ; traceTc "reportUnsolved }" empty
75

76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
       ; 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
           -- messges.
           ; errs_var  <- getErrsVar
           ; saved_msg <- TcRn.readTcRef errs_var
           ; TcRn.writeTcRef errs_var emptyMessages

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

           ; whyUnsafe <- fst <$> TcRn.readTcRef errs_var
           ; TcRn.writeTcRef errs_var saved_msg
           ; recordUnsafeInfer whyUnsafe
           }
       ; traceTc "reportUnsolved (unsafe overlapping) }" empty

95
       ; return (binds1 `unionBags` binds2) }
96

97 98 99 100 101 102
type SafeOverlapFailures = Cts
-- ^ See Note [Safe Haskell Overlapping Instances Implementation]

type FinalConstraints = (WantedConstraints, SafeOverlapFailures)

simpl_top :: WantedConstraints -> TcS FinalConstraints
103
    -- See Note [Top-level Defaulting Plan]
104
simpl_top wanteds
105
  = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
106
                            -- This is where the main work happens
107 108 109
       ; wc_final <- try_tyvar_defaulting wc_first_go
       ; unsafe_ol <- getSafeOverlapFailures
       ; return (wc_final, unsafe_ol) }
110
  where
111 112
    try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints
    try_tyvar_defaulting wc
113
      | isEmptyWC wc
114 115
      = return wc
      | otherwise
116
      = do { free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc)
117
           ; let meta_tvs = varSetElems (filterVarSet isMetaTyVar free_tvs)
118
                   -- zonkTyVarsAndFV: the wc_first_go is not yet zonked
119
                   -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
120 121
                   -- and we definitely don't want to try to assign to those!

122 123 124 125
           ; meta_tvs' <- mapM defaultTyVar meta_tvs   -- Has unification side effects
           ; if meta_tvs' == meta_tvs   -- No defaulting took place;
                                        -- (defaulting returns fresh vars)
             then try_class_defaulting wc
126
             else do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
127 128
                            -- See Note [Must simplify after defaulting]
                     ; try_class_defaulting wc_residual } }
129

130 131
    try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
    try_class_defaulting wc
Austin Seipp's avatar
Austin Seipp committed
132
      | isEmptyWC wc
133 134
      = return wc
      | otherwise  -- See Note [When to do type-class defaulting]
135
      = do { something_happened <- applyDefaultingRules wc
136
                                   -- See Note [Top-level Defaulting Plan]
137
           ; if something_happened
138
             then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
139 140
                     ; try_class_defaulting wc_residual }
             else return wc }
141

Austin Seipp's avatar
Austin Seipp committed
142
{-
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
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
158
   run = fromInteger 0
159 160 161
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
162 163
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
164 165 166 167 168 169
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.

170 171 172 173 174 175 176 177 178
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.

179 180
Note [Top-level Defaulting Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
181 182
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
183
       simple constraints, maybe deep inside the context of implications.
184
       This used to be the case in GHC 7.4.1.
185
   (ii) Do it in a tight loop at simplifyTop, once all other constraint has
186 187
        finished. This is the current story.

188 189 190 191 192
Option (i) had many disadvantages:
   a) First it was deep inside the actual solver,
   b) Second it was dependent on the context (Infer a type signature,
      or Check a type signature, or Interactive) since we did not want
      to always start defaulting when inferring (though there is an exception to
193 194 195 196 197 198 199 200 201 202 203 204 205 206
      this see Note [Default while Inferring])
   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
go with option (i), implemented at SimplifyTop. Namely:
     - First have a go at solving the residual constraint of the whole program
207 208
     - Try to approximate it with a simple constraint
     - Figure out derived defaulting equations for that simple constraint
209 210 211 212
     - 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:
213
     - At the top-level, once you had a go at solving the constraint, do
Gabor Greif's avatar
Gabor Greif committed
214
       figure out /all/ the touchable unification variables of the wanted constraints.
215 216 217
     - Apply defaulting to their kinds

More details in Note [DefaultTyVar].
218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318

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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

How is this implemented? It's compilcated! So we'll step through it all:

 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
 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.

 2) `TcInteract.matchClassInst` -- This module drives the instance resolution /
 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.

 3) `TcInteract.doTopReactDict` -- Takes a dictionary / class constraint and
 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 `-fwarn-unsafe`) 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.simpl_top` -- Top-level function for driving the simplifier for
 constraint resolution. Once finished, we call `getSafeOverlapFailures` to
 retrieve the list of overlapping instances that were successfully resolved,
 but unsafe. Remember, this is only applicable for generating warnings
 (`-fwarn-unsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
 cause compilation failure by not resolving the unsafe constraint at all.
 `simpl_top` returns a list of unresolved constraints (all types), and resolved
 (but unsafe) resolved dictionary constraints.

 5) `TcSimplify.simplifyTop` -- Is the caller of `simpl_top`. For unresolved
 constraints, it calls `TcErrors.reportUnsolved`, while for unsafe overlapping
 instance constraints, it calls `TcErrors.warnAllUnsolved`. Both functions
 convert constraints into a warning message for the user.

 6) `TcErrors.*Unsolved` -- Generates error messages for conastraints by
 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
 know is the constraint that is unresolved or unsafe. For dictionary, this is
 know 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.

 7) `TcSimplify.simplifyTop` -- 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.

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

 9) `HscMain.tcRnModule'` -- Reads `tcg_safeInfer` after type-checking, calling
 `HscMain.markUnsafeInfer` (passing the reason along) when safe-inferrence
 failed.
Austin Seipp's avatar
Austin Seipp committed
319
-}
320

321
------------------
322 323 324
simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
simplifyAmbiguityCheck ty wanteds
  = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
325
       ; ((final_wc, _), _binds) <- runTcS $ simpl_top wanteds
326 327 328 329 330 331 332
       ; traceTc "End simplifyAmbiguityCheck }" empty

       -- Normally report all errors; but with -XAllowAmbiguousTypes
       -- report only insoluble ones, since they represent genuinely
       -- inaccessible code
       ; allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
       ; traceTc "reportUnsolved(ambig) {" empty
333 334
       ; unless (allow_ambiguous && not (insolubleWC final_wc))
                (discardResult (reportUnsolved final_wc))
335 336 337 338
       ; traceTc "reportUnsolved(ambig) }" empty

       ; return () }

339 340
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
341
simplifyInteractive wanteds
342
  = traceTc "simplifyInteractive" empty >>
343
    simplifyTop wanteds
344 345

------------------
346 347
simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
                -> TcM ()       -- Succeeds iff the constraint is soluble
348
simplifyDefault theta
349
  = do { traceTc "simplifyInteractive" empty
350
       ; wanted <- newWanteds DefaultOrigin theta
351
       ; unsolved <- solveWantedsTcM wanted
352 353 354

       ; traceTc "reportUnsolved {" empty
       -- See Note [Deferring coercion errors to runtime]
355
       ; reportAllUnsolved unsolved
356 357
       ; traceTc "reportUnsolved }" empty

358
       ; return () }
359

Austin Seipp's avatar
Austin Seipp committed
360
{-
361
*********************************************************************************
362
*                                                                                 *
363 364 365
*                            Inference
*                                                                                 *
***********************************************************************************
366

367 368 369 370 371 372 373 374
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
375
        pushLevelAndCaptureConstraints (tcMonoBinds...)
376 377 378 379
   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,
380
   here called rhs_tclvl.
381 382 383 384

This ensures that the implication constraint we generate, if any,
has a strictly-increased level compared to the ambient level outside
the let binding.
Austin Seipp's avatar
Austin Seipp committed
385
-}
386

387
simplifyInfer :: TcLevel          -- Used when generating the constraints
388 389 390
              -> Bool                  -- Apply monomorphism restriction
              -> [(Name, TcTauType)]   -- Variables to be generalised,
                                       -- and their tau-types
391
              -> WantedConstraints
392
              -> TcM ([TcTyVar],    -- Quantify over these type variables
393
                      [EvVar],      -- ... and these constraints (fully zonked)
394 395 396
                      Bool,         -- The monomorphism restriction did something
                                    --   so the results type is not as general as
                                    --   it could be
397
                      TcEvBinds)    -- ... binding these evidence variables
398
simplifyInfer rhs_tclvl apply_mr name_taus wanteds
399
  | isEmptyWC wanteds
400 401
  = do { gbl_tvs <- tcGetGlobalTyVars
       ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
402
       ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
403
       ; return (qtkvs, [], False, emptyTcEvBinds) }
404

405
  | otherwise
406 407
  = do { traceTc "simplifyInfer {"  $ vcat
             [ ptext (sLit "binds =") <+> ppr name_taus
408
             , ptext (sLit "rhs_tclvl =") <+> ppr rhs_tclvl
409
             , ptext (sLit "apply_mr =") <+> ppr apply_mr
410
             , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
411 412
             ]

413 414 415 416 417
              -- Historical note: Before step 2 we used to have a
              -- HORRIBLE HACK described in Note [Avoid unecessary
              -- constraint simplification] but, as described in Trac
              -- #4361, we have taken in out now.  That's why we start
              -- with step 2!
418

419
              -- Step 2) First try full-blown solving
420 421 422 423 424 425 426

              -- 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.
427

428
       ; ev_binds_var <- TcM.newTcEvBinds
429
       ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $
430
                                           runTcSWithEvBinds ev_binds_var (solveWanteds wanteds)
431
       ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
432 433

              -- Step 4) Candidates for quantification are an approximation of wanted_transformed
434
              -- NB: Already the fixpoint of any unifications that may have happened
435 436
              -- NB: We do not do any defaulting when inferring a type, this can lead
              -- to less polymorphic types, see Note [Default while Inferring]
437

438
       ; tc_lcl_env <- TcRn.getLclEnv
439 440
       ; null_ev_binds_var <- TcM.newTcEvBinds
       ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
441
       ; quant_pred_candidates   -- Fully zonked
442
           <- if insolubleWC wanted_transformed_incl_derivs
443
              then return []   -- See Note [Quantification with errors]
444
                               -- NB: must include derived errors in this test,
445 446 447
                               --     hence "incl_derivs"

              else do { let quant_cand = approximateWC wanted_transformed
448
                            meta_tvs   = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
449 450 451 452
                      ; gbl_tvs <- tcGetGlobalTyVars
                            -- Miminise quant_cand.  We are not interested in any evidence
                            -- produced, because we are going to simplify wanted_transformed
                            -- again later. All we want here is the predicates over which to
453
                            -- quantify.
454 455 456 457
                            --
                            -- If any meta-tyvar unifications take place (unlikely), we'll
                            -- pick that up later.

458
                      ; WC { wc_simple = simples }
459
                           <- setTcLevel rhs_tclvl                $
460
                              runTcSWithEvBinds null_ev_binds_var $
461
                              do { mapM_ (promoteAndDefaultTyVar rhs_tclvl gbl_tvs) meta_tvs
462
                                     -- See Note [Promote _and_ default when inferring]
463
                                 ; solveSimpleWanteds quant_cand }
464

465
                      ; return [ ctEvPred ev | ct <- bagToList simples
466 467
                                             , let ev = ctEvidence ct
                                             , isWanted ev ] }
468

469
       -- NB: quant_pred_candidates is already fully zonked
470

471
         -- Decide what type variables and constraints to quantify
472 473
       ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
       ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus
474
       ; (qtvs, bound_theta, mr_bites)
475
             <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
476

477
         -- Emit an implication constraint for the
478
         -- remaining constraints from the RHS
479 480
       ; bound_ev_vars <- mapM TcM.newEvVar bound_theta
       ; let skol_info = InferSkol [ (name, mkSigmaTy [] bound_theta ty)
481
                                   | (name, ty) <- name_taus ]
482
                        -- Don't add the quantified variables here, because
483 484
                        -- they are also bound in ic_skols and we want them
                        -- to be tidied uniformly
485

486
             implic = Implic { ic_tclvl    = rhs_tclvl
487
                             , ic_skols    = qtvs
488
                             , ic_no_eqs   = False
489
                             , ic_given    = bound_ev_vars
490
                             , ic_wanted   = wanted_transformed
491
                             , ic_status   = IC_Unsolved
492
                             , ic_binds    = ev_binds_var
493
                             , ic_info     = skol_info
494
                             , ic_env      = tc_lcl_env }
495
       ; emitImplication implic
496

497 498 499
         -- Promote any type variables that are free in the inferred type
         -- of the function:
         --    f :: forall qtvs. bound_theta => zonked_tau
500
         -- These variables now become free in the envt, and hence will show
501 502 503 504 505 506 507 508
         -- up whenever 'f' is called.  They may currently at rhs_tclvl, but
         -- they had better be unifiable at the outer_tclvl!
         -- Example:   envt mentions alpha[1]
         --            tau_ty = beta[2] -> beta[2]
         --            consraints = alpha ~ [beta]
         -- we don't quantify over beta (since it is fixed by envt)
         -- so we must promote it!  The inferred type is just
         --   f :: beta -> beta
509
       ; outer_tclvl    <- TcRn.getTcLevel
510 511 512 513 514 515 516 517 518
       ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV zonked_tau_tvs
              -- decideQuantification turned some meta tyvars into
              -- quantified skolems, so we have to zonk again
       ; let phi_tvs     = tyVarsOfTypes bound_theta `unionVarSet` zonked_tau_tvs
             promote_tvs = varSetElems (closeOverKinds phi_tvs `delVarSetList` qtvs)
       ; runTcSWithEvBinds null_ev_binds_var $  -- runTcS just to get the types right :-(
         mapM_ (promoteTyVar outer_tclvl) promote_tvs

         -- All done!
519
       ; traceTc "} simplifyInfer/produced residual implication for quantification" $
520
         vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
521
              , ptext (sLit "zonked_taus") <+> ppr zonked_taus
522
              , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
523
              , ptext (sLit "promote_tvs=") <+> ppr promote_tvs
524 525
              , ptext (sLit "bound_theta =") <+> vcat [ ppr v <+> dcolon <+> ppr (idType v)
                                                        | v <- bound_ev_vars]
526 527 528
              , ptext (sLit "mr_bites =") <+> ppr mr_bites
              , ptext (sLit "qtvs =") <+> ppr qtvs
              , ptext (sLit "implic =") <+> ppr implic ]
529

530
       ; return ( qtvs, bound_ev_vars, mr_bites, TcEvBinds ev_binds_var) }
531

Austin Seipp's avatar
Austin Seipp committed
532 533 534
{-
************************************************************************
*                                                                      *
535
                Quantification
Austin Seipp's avatar
Austin Seipp committed
536 537
*                                                                      *
************************************************************************
538 539 540 541 542 543 544

Note [Deciding quantification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the monomorphism restriction does not apply, then we quantify as follows:
  * 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
          happen because alpha is untouchable here) then do not quantify over
545 546
          beta, because alpha fixes beta, and beta is effectively free in
          the environment too
547 548 549
    These are the mono_tvs

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

552 553 554 555
  * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
    careful to close over kinds, and to skolemise the quantified tyvars.
    (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
    Result is qtvs.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
556

557 558 559
  * Filter the constraints using pickQuantifyablePreds and the qtvs.
    We have to zonk the constraints first, so they "see" the freshly
    created skolems.
560 561 562

If the MR does apply, mono_tvs includes all the constrained tyvars,
and the quantified constraints are empty.
Austin Seipp's avatar
Austin Seipp committed
563
-}
564

565
decideQuantification
566 567 568 569 570
    :: Bool                       -- Apply monomorphism restriction
    -> [PredType] -> TcTyVarSet   -- Constraints and type variables from RHS
    -> TcM ( [TcTyVar]       -- Quantify over these tyvars (skolems)
           , [PredType]      -- and this context (fully zonked)
           , Bool )          -- Did the MR bite?
571 572 573 574
-- See Note [Deciding quantification]
decideQuantification apply_mr constraints zonked_tau_tvs
  | apply_mr     -- Apply the Monomorphism restriction
  = do { gbl_tvs <- tcGetGlobalTyVars
575 576
       ; let constrained_tvs = tyVarsOfTypes constraints
             mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
577 578
             mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
       ; qtvs <- quantifyTyVars mono_tvs zonked_tau_tvs
579
       ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr qtvs])
580
       ; return (qtvs, [], mr_bites) }
581 582 583

  | otherwise
  = do { gbl_tvs <- tcGetGlobalTyVars
584 585 586 587 588 589 590
       ; let mono_tvs     = growThetaTyVars (filter isEqPred constraints) gbl_tvs
             tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
       ; qtvs        <- quantifyTyVars mono_tvs tau_tvs_plus
       ; constraints <- zonkTcThetaType constraints
              -- quantifyTyVars turned some meta tyvars into
              -- quantified skolems, so we have to zonk again

591 592 593
       ; theta <- pickQuantifiablePreds (mkVarSet qtvs) constraints
       ; let min_theta = mkMinimalBySCs theta  -- See Note [Minimize by Superclasses]

594 595 596
       ; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
                                                , ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
       ; return (qtvs, min_theta, False) }
597 598

------------------
599 600 601
pickQuantifiablePreds :: TyVarSet         -- Quantifying over these
                      -> TcThetaType      -- Proposed constraints to quantify
                      -> TcM TcThetaType  -- A subset that we can actually quantify
602 603
-- This function decides whether a particular constraint shoudl be
-- quantified over, given the type variables that are being quantified
604 605 606
pickQuantifiablePreds qtvs theta
  = do { flex_ctxt <- xoptM Opt_FlexibleContexts
       ; return (filter (pick_me flex_ctxt) theta) }
607
  where
608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626
    pick_me flex_ctxt pred
      = case classifyPredType pred of
          ClassPred cls tys
             | isIPClass cls -> True -- See note [Inheriting implicit parameters]
             | otherwise     -> pick_cls_pred flex_ctxt tys

          EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt [ty1, ty2]
                -- Representational equality is like a class constraint

          EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
          IrredPred ty          -> tyVarsOfType ty `intersectsVarSet` qtvs

    pick_cls_pred flex_ctxt tys
      = tyVarsOfTypes tys `intersectsVarSet` qtvs
        && (checkValidClsArgs flex_ctxt tys)
           -- Only quantify over predicates that checkValidType
           -- will pass!  See Trac #10351.

        -- See Note [Quantifying over equality constraints]
627 628
    quant_fun ty
      = case tcSplitTyConApp_maybe ty of
629
          Just (tc, tys) | isTypeFamilyTyCon tc
630 631 632 633 634 635 636
                         -> tyVarsOfTypes tys `intersectsVarSet` qtvs
          _ -> False

------------------
growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
-- See Note [Growing the tau-tvs using constraints]
growThetaTyVars theta tvs
637 638
  | null theta = tvs
  | otherwise  = transCloVarSet mk_next seed_tvs
639 640 641 642
  where
    seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips
    (ips, non_ips) = partition isIPPred theta
                         -- See note [Inheriting implicit parameters]
643 644 645 646 647 648

    mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
    mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
    grow_one so_far pred tvs
       | pred_tvs `intersectsVarSet` so_far = tvs `unionVarSet` pred_tvs
       | otherwise                          = tvs
649 650
       where
         pred_tvs = tyVarsOfType pred
651

Austin Seipp's avatar
Austin Seipp committed
652
{-
653 654 655 656 657 658 659 660 661 662 663 664 665
Note [Quantifying over equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Should we quantify over an equality constraint (s ~ t)?  In general, we don't.
Doing so may simply postpone a type error from the function definition site to
its call site.  (At worst, imagine (Int ~ Bool)).

However, consider this
         forall a. (F [a] ~ Int) => blah
Should we quantify over the (F [a] ~ Int).  Perhaps yes, because at the call
site we will know 'a', and perhaps we have instance  F [Bool] = Int.
So we *do* quantify over a type-family equality where the arguments mention
the quantified variables.

666 667 668 669 670 671 672 673 674 675 676 677
Note [Growing the tau-tvs using constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(growThetaTyVars insts tvs) is the result of extending the set
    of tyvars tvs using all conceivable links from pred

E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
Then growThetaTyVars preds tvs = {a,b,c}

Notice that
   growThetaTyVars is conservative       if v might be fixed by vs
                                         => v `elem` grow(vs,C)

Simon Peyton Jones's avatar
Simon Peyton Jones committed
678 679 680 681
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:

682
        f x = (x::Int) + ?y
Simon Peyton Jones's avatar
Simon Peyton Jones committed
683 684 685 686 687

where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:

688
        f :: Int -> Int
Simon Peyton Jones's avatar
Simon Peyton Jones committed
689 690 691

(so we get ?y from the context of f's definition), or

692
        f :: (?y::Int) => Int -> Int
Simon Peyton Jones's avatar
Simon Peyton Jones committed
693

Gabor Greif's avatar
typos  
Gabor Greif committed
694
At first you might think the first was better, because then
Simon Peyton Jones's avatar
Simon Peyton Jones committed
695 696 697 698 699
?y behaves like a free variable of the definition, rather than
having to be passed at each call site.  But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
700 701 702
BOTTOM LINE: when *inferring types* you must quantify over implicit
parameters, *even if* they don't mention the bound type variables.
Reason: because implicit parameters, uniquely, have local instance
703
declarations. See the pickQuantifiablePreds.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
704

705 706 707 708 709 710 711 712
Note [Quantification with errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we find that the RHS of the definition has some absolutely-insoluble
constraints, we abandon all attempts to find a context to quantify
over, and instead make the function fully-polymorphic in whatever
type we have found.  For two reasons
  a) Minimise downstream errors
  b) Avoid spurious errors from this function
713

714
But NB that we must include *derived* errors in the check. Example:
715 716 717
    (a::*) ~ Int#
We get an insoluble derived error *~#, and we don't want to discard
it before doing the isInsolubleWC test!  (Trac #8262)
718

719 720
Note [Default while Inferring]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
721 722 723 724
Our current plan is that defaulting only happens at simplifyTop and
not simplifyInfer.  This may lead to some insoluble deferred constraints
Example:

725
instance D g => C g Int b
726 727

constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
728
type inferred       = gamma -> gamma
729

730 731 732
Now, if we try to default (alpha := Int) we will be able to refine the implication to
  (forall b. 0 => C gamma Int b)
which can then be simplified further to
733 734 735 736
  (forall b. 0 => D gamma)
Finally we /can/ approximate this implication with (D gamma) and infer the quantified
type:  forall g. D g => g -> g

737
Instead what will currently happen is that we will get a quantified type
738 739 740
(forall g. g -> g) and an implication:
       forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha

741
which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
742 743 744
unsolvable implication:
       forall g. 0 => (forall b. 0 => D g)

745
The concrete example would be:
746 747 748 749
       h :: C g a s => g -> a -> ST s a
       f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)

But it is quite tedious to do defaulting and resolve the implication constraints and
750
we have not observed code breaking because of the lack of defaulting in inference so
751 752 753 754
we don't do it for now.



755
Note [Minimize by Superclasses]
756
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
757 758 759 760 761 762 763
When we quantify over a constraint, in simplifyInfer we need to
quantify over a constraint that is minimal in some sense: For
instance, if the final wanted constraint is (Eq alpha, Ord alpha),
we'd like to quantify over Ord alpha, because we can just get Eq alpha
from superclass selection from Ord alpha. This minimization is what
mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
to check the original wanted.
764

765

766 767
Note [Avoid unecessary constraint simplification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
768
    -------- NB NB NB (Jun 12) -------------
769 770 771
    This note not longer applies; see the notes with Trac #4361.
    But I'm leaving it in here so we remember the issue.)
    ----------------------------------------
772
When inferring the type of a let-binding, with simplifyInfer,
773
try to avoid unnecessarily simplifying class constraints.
774
Doing so aids sharing, but it also helps with delicate
775
situations like
776

777
   instance C t => C [t] where ..
778

779
   f :: C [t] => ....
780
   f x = let g y = ...(constraint C [t])...
781 782 783 784
         in ...
When inferring a type for 'g', we don't want to apply the
instance decl, because then we can't satisfy (C t).  So we
just notice that g isn't quantified over 't' and partition
Gabor Greif's avatar
Gabor Greif committed
785
the constraints before simplifying.
786 787 788 789

This only half-works, but then let-generalisation only half-works.


790
*********************************************************************************
791
*                                                                                 *
792 793 794
*                                 Main Simplifier                                 *
*                                                                                 *
***********************************************************************************
795

796 797 798 799 800 801
Note [Deferring coercion errors to runtime]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
While developing, sometimes it is desirable to allow compilation to succeed even
if there are type errors in the code. Consider the following case:

  module Main where
802

803 804
  a :: Int
  a = 'a'
805

806
  main = print "b"
807

808 809
Even though `a` is ill-typed, it is not used in the end, so if all that we're
interested in is `main` it is handy to be able to ignore the problems in `a`.
810

811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829
Since we treat type equalities as evidence, this is relatively simple. Whenever
we run into a type mismatch in TcUnify, we normally just emit an error. But it
is always safe to defer the mismatch to the main constraint solver. If we do
that, `a` will get transformed into

  co :: Int ~ Char
  co = ...

  a :: Int
  a = 'a' `cast` co

The constraint solver would realize that `co` is an insoluble constraint, and
emit an error with `reportUnsolved`. But we can also replace the right-hand side
of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
to compile, and it will run fine unless we evaluate `a`. This is what
`deferErrorsToRuntime` does.

It does this by keeping track of which errors correspond to which coercion
in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
830
and does not fail if -fdefer-type-errors is on, so that we can continue
831
compilation. The errors are turned into warnings in `reportUnsolved`.
Austin Seipp's avatar
Austin Seipp committed
832
-}
833

834 835 836
solveWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
-- Simplify the input constraints
-- Discard the evidence binds
837
-- Discards all Derived stuff in result
838
-- Result is /not/ guaranteed zonked
839
solveWantedsTcM wanted
840 841
  = do { (wanted1, _binds) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
       ; return wanted1 }
842

843
solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
844
-- Since solveWanteds returns the residual WantedConstraints,
845
-- it should always be called within a runTcS or something similar,
846 847 848 849
-- Result is not zonked
solveWantedsAndDrop wanted
  = do { wc <- solveWanteds wanted
       ; return (dropDerivedWC wc) }
850

851
solveWanteds :: WantedConstraints -> TcS WantedConstraints
852
-- so that the inert set doesn't mindlessly propagate.
853
-- NB: wc_simples may be wanted /or/ derived now
854 855
solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
  = do { traceTcS "solveWanteds {" (ppr wc)
856

857
         -- Try the simple bit, including insolubles. Solving insolubles a
858 859 860 861
         -- second time round is a bit of a waste; but the code is simple
         -- and the program is wrong anyway, and we don't run the danger
         -- of adding Derived insolubles twice; see
         -- TcSMonad Note [Do not add duplicate derived insolubles]
862 863
       ; wc1 <- solveSimpleWanteds simples
       ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
864

865 866
       ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)

867 868
       ; dflags <- getDynFlags
       ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
869 870
                                (WC { wc_simple = simples1, wc_impl = implics2
                                    , wc_insol  = insols `unionBags` insols1 })
871

872
       ; bb <- getTcEvBindsMap
873
       ; traceTcS "solveWanteds }" $
874
                 vcat [ text "final wc =" <+> ppr final_wc
875 876
                      , text "current evbinds  =" <+> ppr (evBindMapBinds bb) ]

877
       ; return final_wc }
878

879
simpl_loop :: Int -> IntWithInf -> Cts
880 881
           -> WantedConstraints
           -> TcS WantedConstraints
882
simpl_loop n limit floated_eqs
883
           wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
884 885 886 887 888
  | n `intGtLimit` limit
  = failTcS (hang (ptext (sLit "solveWanteds: too many iterations")
                   <+> parens (ptext (sLit "limit =") <+> ppr limit))
                2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
                        , ppr wc ] ))
889 890 891

  | no_floated_eqs
  = return wc  -- Done!
892

893
  | otherwise
894
  = do { traceTcS "simpl_loop, iteration" (int n)
895

896
       -- solveSimples may make progress if either float_eqs hold
897 898 899 900 901
       ; (unifs1, wc1) <- reportUnifications $
                          solveSimpleWanteds (floated_eqs `unionBags` simples)
                               -- Put floated_eqs first so they get solved first
                               -- NB: the floated_eqs may include /derived/ equalities
                               --     arising from fundeps inside an implication
902

903
       ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
904

905
       -- solveImplications may make progress only if unifs2 holds
906
       ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
907 908
                                     then return (emptyBag, implics)
                                     else solveNestedImplications (implics `unionBags` implics1)
909

910
       ; simpl_loop (n+1) limit floated_eqs2
911 912 913 914 915
                    (WC { wc_simple = simples1, wc_impl = implics2
                        , wc_insol  = insols `unionBags` insols1 }) }

  where
    no_floated_eqs = isEmptyBag floated_eqs
916

917 918
solveNestedImplications :: Bag Implication
                        -> TcS (Cts, Bag Implication)
919
-- Precondition: the TcS inerts may contain unsolved simples which have
920 921 922 923
-- to be converted to givens before we go inside a nested implication.
solveNestedImplications implics
  | isEmptyBag implics
  = return (emptyBag, emptyBag)
924
  | otherwise
925 926 927
  = do { traceTcS "solveNestedImplications starting {" empty
       ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics
       ; let floated_eqs = concatBag floated_eqs_s
928

929
       -- ... and we are back in the original TcS inerts
930
       -- Notice that the original includes the _insoluble_simples so it was safe to ignore
931
       -- them in the beginning of this function.
932
       ; traceTcS "solveNestedImplications end }" $
933
                  vcat [ text "all floated_eqs ="  <+> ppr floated_eqs
934 935
                       , text "unsolved_implics =" <+> ppr unsolved_implics ]

936
       ; return (floated_eqs, catBagMaybes unsolved_implics) }
937

938
solveImplication :: Implication    -- Wanted
939
                 -> TcS (Cts,      -- All wanted or derived floated equalities: var = type