TcInteract.lhs 76.3 KB
Newer Older
1
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
2
3
4
5
6
7
8
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

9
module TcInteract ( 
10
     solveInteractGiven,  -- Solves [EvVar],GivenLoc
11
     solveInteract,       -- Solves Cts
12
13
14
15
  ) where  

#include "HsVersions.h"

16

17
import BasicTypes ()
18
19
20
import TcCanonical
import VarSet
import Type
dimitris's avatar
dimitris committed
21
import Unify
22
23
import FamInstEnv
import Coercion( mkAxInstRHS )
24
25
26

import Var
import TcType
27
import PrelNames (singIClassName, ipClassNameKey )
28

29
30
import Class
import TyCon
31
32
33
34
import Name

import FunDeps

35
import TcEvidence
36
37
import Outputable

38
39
import TcMType ( zonkTcPredType )

40
import TcRnTypes
41
import TcErrors
42
import TcSMonad
43
import Maybes( orElse )
44
import Bag
45

46
47
import Control.Monad ( foldM )

dimitris's avatar
dimitris committed
48
49
import VarEnv

50
import Control.Monad( when, unless )
51
import Pair ()
52
import Unique( hasKey )
53
import UniqFM
54
55
import FastString ( sLit ) 
import DynFlags
56
import Util
57
\end{code}
58
59
**********************************************************************
*                                                                    * 
60
61
62
63
*                      Main Interaction Solver                       *
*                                                                    *
**********************************************************************

64
65
Note [Basic Simplifier Plan] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
66

67
68
1. Pick an element from the WorkList if there exists one with depth 
   less thanour context-stack depth. 
69

70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
2. Run it down the 'stage' pipeline. Stages are: 
      - canonicalization
      - inert reactions
      - spontaneous reactions
      - top-level intreactions
   Each stage returns a StopOrContinue and may have sideffected 
   the inerts or worklist.
  
   The threading of the stages is as follows: 
      - If (Stop) is returned by a stage then we start again from Step 1. 
      - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to 
        the next stage in the pipeline. 
4. If the element has survived (i.e. ContinueWith x) the last stage 
   then we add him in the inerts and jump back to Step 1.

If in Step 1 no such element exists, we have exceeded our context-stack 
depth and will simply fail.
87
\begin{code}
88
solveInteractGiven :: CtLoc -> [TcTyVar] -> [EvVar] -> TcS ()
89
90
91
92
-- In principle the givens can kick out some wanteds from the inert
-- resulting in solving some more wanted goals here which could emit
-- implications. That's why I return a bag of implications. Not sure
-- if this can happen in practice though.
93
solveInteractGiven loc fsks givens
94
95
96
97
98
99
100
  = do { implics <- solveInteract (fsk_bag `unionBags` given_bag)
       ; ASSERT( isEmptyBag implics )
         return () }  -- We do not decompose *given* polymorphic equalities
                      --    (forall a. t1 ~ forall a. t2)
                      -- What would the evidence look like?!
                      -- See Note [Do not decompose given polytype equalities]
                      -- in TcCanonical
101
  where 
102
103
    given_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvId ev_id
                                                         , ctev_pred = evVarPred ev_id }
104
105
                          | ev_id <- givens ]

106
107
    fsk_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
                                                       , ctev_pred = pred  }
108
109
110
111
112
                        | tv <- fsks
                        , let FlatSkol fam_ty = tcTyVarDetails tv
                              tv_ty = mkTyVarTy tv
                              pred  = mkTcEqPred fam_ty tv_ty
                        ]
113
114
115

-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
116
117
118
119
solveInteract :: Cts -> TcS (Bag Implication)
-- Returns the final InertSet in TcS
-- Has no effect on work-list or residual-iplications
solveInteract cts
120
  = {-# SCC "solveInteract" #-}
121
    withWorkList cts $
122
    do { dyn_flags <- getDynFlags
123
124
125
126
127
128
129
130
131
       ; solve_loop (ctxtStkDepth dyn_flags) }
  where
    solve_loop max_depth
      = {-# SCC "solve_loop" #-}
        do { sel <- selectNextWorkItem max_depth
           ; case sel of 
              NoWorkRemaining     -- Done, successfuly (modulo frozen)
                -> return ()
              MaxDepthExceeded ct -- Failure, depth exceeded
132
                -> wrapErrTcS $ solverDepthErrorTcS ct
133
134
              NextWorkItem ct     -- More work, loop around!
                -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

type WorkItem = Ct
type SimplifierStage = WorkItem -> TcS StopOrContinue

continueWith :: WorkItem -> TcS StopOrContinue
continueWith work_item = return (ContinueWith work_item) 

data SelectWorkItem 
       = NoWorkRemaining      -- No more work left (effectively we're done!)
       | MaxDepthExceeded Ct  -- More work left to do but this constraint has exceeded
                              -- the max subgoal depth and we must stop 
       | NextWorkItem Ct      -- More work left, here's the next item to look at 

selectNextWorkItem :: SubGoalDepth -- Max depth allowed
                   -> TcS SelectWorkItem
selectNextWorkItem max_depth
  = updWorkListTcS_return pick_next
152
  where 
153
    pick_next :: WorkList -> (SelectWorkItem, WorkList)
154
155
156
157
158
159
160
161
162
    pick_next wl 
      = case selectWorkItem wl of
          (Nothing,_) 
              -> (NoWorkRemaining,wl)           -- No more work
          (Just ct, new_wl) 
              | ctLocDepth (cc_loc ct) > max_depth  -- Depth exceeded
              -> (MaxDepthExceeded ct,new_wl)
          (Just ct, new_wl) 
              -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
163
164
165
166
167
168
169
170
171
172
173

runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline 
                  -> WorkItem                   -- The work item 
                  -> TcS () 
-- Run this item down the pipeline, leaving behind new work and inerts
runSolverPipeline pipeline workItem 
  = do { initial_is <- getTcSInerts 
       ; traceTcS "Start solver pipeline {" $ 
                  vcat [ ptext (sLit "work item = ") <+> ppr workItem 
                       , ptext (sLit "inerts    = ") <+> ppr initial_is]

174
       ; bumpStepCountTcS    -- One step for each constraint processed
175
176
177
178
179
180
181
       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)

       ; final_is <- getTcSInerts
       ; case final_res of 
           Stop            -> do { traceTcS "End solver pipeline (discharged) }" 
                                       (ptext (sLit "inerts    = ") <+> ppr final_is)
                                 ; return () }
182
183
           ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
                                 ; traceTcS "End solver pipeline (not discharged) }" $
184
                                       vcat [ ptext (sLit "final_item = ") <+> ppr ct
185
                                            , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
186
                                            , ptext (sLit "inerts     = ") <+> ppr final_is]
187
                                 ; insertInertItemTcS ct }
188
189
190
191
192
193
194
195
196
197
198
       }
  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
        run_pipeline [] res = return res 
        run_pipeline _ Stop = return Stop 
        run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
          = do { traceTcS ("runStage " ++ stg_name ++ " {")
                          (text "workitem   = " <+> ppr ct) 
               ; res <- stg ct 
               ; traceTcS ("end stage " ++ stg_name ++ " }") empty
               ; run_pipeline stgs res 
               }
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
\end{code}

Example 1:
  Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
  Reagent: a ~ [b] (given)

React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []

Example 2:
  Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
  Reagent: a ~w [b]

React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
etc.

Example 3:
  Inert:  {a ~ Int, F Int ~ b} (given)
  Reagent: F a ~ b (wanted)

React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing

\begin{code}
225
thePipeline :: [(String,SimplifierStage)]
226
thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
227
228
229
              , ("spontaneous solve",       spontaneousSolveStage)
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
230
231
232
\end{code}


233
234
235
236
237
238
239
240
*********************************************************************************
*                                                                               * 
                       The spontaneous-solve Stage
*                                                                               *
*********************************************************************************

\begin{code}
spontaneousSolveStage :: SimplifierStage 
241
spontaneousSolveStage workItem
242
243
244
245
246
  = do { mb_solved <- trySpontaneousSolve workItem
       ; case mb_solved of
           SPCantSolve
              | CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
              -- Unsolved equality
247
248
249
250
              -> do { n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
                    ; traceFireTcS workItem $
                      ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon 
                      <+> ppr workItem
251
252
253
254
255
256
257
258
                    ; insertInertItemTcS workItem
                    ; return Stop }
              | otherwise
              -> continueWith workItem

           SPSolved new_tv
              -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
              -- see Note [Spontaneously solved in TyBinds]
259
260
261
262
              -> do { n_kicked <- kickOutRewritable Given new_tv
                    ; traceFireTcS workItem $
                      ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon 
                      <+> ppr workItem
263
                    ; return Stop } }
264
265
266
267

ppr_kicked :: Int -> SDoc
ppr_kicked 0 = empty
ppr_kicked n = parens (int n <+> ptext (sLit "kicked out")) 
268
269
270
271
272
273
274
\end{code}
Note [Spontaneously solved in TyBinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we encounter a constraint ([W] alpha ~ tau) which can be spontaneously solved,
we record the equality on the TyBinds of the TcSMonad. In the past, we used to also
add a /given/ version of the constraint ([G] alpha ~ tau) to the inert
canonicals -- and potentially kick out other equalities that mention alpha.
275

276
277
Then, the flattener only had to look in the inert equalities during flattening of a
type (TcCanonical.flattenTyVar).
278

279
280
281
282
283
284
However it is a bit silly to record these equalities /both/ in the inerts AND the
TyBinds, so we have now eliminated spontaneously solved equalities from the inerts,
and only record them in the TyBinds of the TcS monad. The flattener is now consulting
these binds /and/ the inerts for potentially unsolved or other given equalities.

\begin{code}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
285
286
287
kickOutRewritable :: CtFlavour    -- Flavour of the equality that is 
                                  -- being added to the inert set
                  -> TcTyVar      -- The new equality is tv ~ ty
288
                  -> TcS Int
Simon Peyton Jones's avatar
Simon Peyton Jones committed
289
kickOutRewritable new_flav new_tv
290
291
292
293
  = do { wl <- modifyInertTcS kick_out
       ; traceTcS "kickOutRewritable" $ 
            vcat [ text "tv = " <+> ppr new_tv  
                 , ptext (sLit "Kicked out =") <+> ppr wl]
294
295
       ; updWorkListTcS (appendWorkList wl)
       ; return (workListSize wl)  }
296
  where
297
298
299
300
    kick_out :: InertSet -> (WorkList, InertSet)
    kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
                     , inert_dicts  = dictmap
                     , inert_funeqs = funeqmap
301
302
                     , inert_irreds = irreds
                     , inert_insols = insols } }))
303
       = (kicked_out, is { inert_cans = inert_cans_in })
dimitris's avatar
dimitris committed
304
                -- NB: Notice that don't rewrite 
305
                -- inert_solved_dicts, and inert_solved_funeqs
dimitris's avatar
dimitris committed
306
307
                -- optimistically. But when we lookup we have to take the 
                -- subsitution into account
308
309
310
311
       where
         inert_cans_in = IC { inert_eqs = tv_eqs_in
                            , inert_dicts = dicts_in
                            , inert_funeqs = feqs_in
312
313
                            , inert_irreds = irs_in
                            , inert_insols = insols_in }
314
315
316

         kicked_out = WorkList { wl_eqs    = varEnvElts tv_eqs_out
                               , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
317
318
                               , wl_rest   = bagToList (dicts_out `andCts` irs_out 
                                                        `andCts` insols_out) }
319
  
320
321
322
323
324
325
         (tv_eqs_out,  tv_eqs_in) = partitionVarEnv  kick_out_eq tv_eqs
         (feqs_out,   feqs_in)    = partCtFamHeadMap kick_out_ct funeqmap
         (dicts_out,  dicts_in)   = partitionCCanMap kick_out_ct dictmap
         (irs_out,    irs_in)     = partitionBag     kick_out_ct irreds
         (insols_out, insols_in)  = partitionBag     kick_out_ct insols
           -- Kick out even insolubles; see Note [Kick out insolubles]
326

327
328
    kick_out_ct inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
                          (new_tv `elemVarSet` tyVarsOfCt inert_ct) 
329
330
331
332
333
334
335
336
337
                    -- NB: tyVarsOfCt will return the type 
                    --     variables /and the kind variables/ that are 
                    --     directly visible in the type. Hence we will
                    --     have exposed all the rewriting we care about
                    --     to make the most precise kinds visible for 
                    --     matching classes etc. No need to kick out 
                    --     constraints that mention type variables whose
                    --     kinds could contain this variable!

338
339
340
341
342
343
344
345
346
347
348
    kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev })
      =  (new_flav `canRewrite` inert_flav)  -- See Note [Delicate equality kick-out]
      && (new_tv `elemVarSet` kind_vars ||              -- (1)
          (not (inert_flav `canRewrite` new_flav) &&    -- (2)
           new_tv `elemVarSet` (extendVarSet (tyVarsOfType rhs) tv)))
      where
        inert_flav = ctEvFlavour ev
        kind_vars = tyVarsOfType (tyVarKind tv) `unionVarSet`
                    tyVarsOfType (typeKind rhs)

    kick_out_eq other_ct = pprPanic "kick_out_eq" (ppr other_ct)
349
\end{code}
350

351
352
353
354
Note [Kick out insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an insoluble alpha ~ [alpha], which is insoluble
because an occurs check.  And then we unify alpha := [Int].  
Simon Peyton Jones's avatar
Simon Peyton Jones committed
355
Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
356
357
358
359
Now it can be decomposed.  Otherwise we end up with a "Can't match
[Int] ~ [[Int]]" which is true, but a bit confusing because the
outer type constructors match. 

360
361
Note [Delicate equality kick-out]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
When adding an equality (a ~ xi), we kick out an inert type-variable 
equality (b ~ phi) in two cases

(1) If the new tyvar can rewrite the kind LHS or RHS of the inert
    equality.  Example:
    Work item: [W] k ~ *
    Inert:     [W] (a:k) ~ ty        
               [W] (b:*) ~ c :: k
    We must kick out those blocked inerts so that we rewrite them
    and can subsequently unify.

(2) If the new tyvar can 
          Work item:  [G] a ~ b
          Inert:      [W] b ~ [a]
    Now at this point the work item cannot be further rewritten by the
    inert (due to the weaker inert flavor). But we can't add the work item
    as-is because the inert set would then have a cyclic substitution, 
    when rewriting a wanted type mentioning 'a'. So we must kick the inert out. 

    We have to do this only if the inert *cannot* rewrite the work item;
    it it can, then the work item will have been fully rewritten by the 
    inert during canonicalisation.  So for example:
         Work item: [W] a ~ Int
         Inert:     [W] b ~ [a]
    No need to kick out the inert, beause the inert substitution is not
    necessarily idemopotent.  See Note [Non-idempotent inert substitution].

See also point (8) of Note [Detailed InertCans Invariants] 
390
391

\begin{code}
392
data SPSolveResult = SPCantSolve
393
394
                   | SPSolved TcTyVar
                     -- We solved this /unification/ variable to some type using reflexivity
395

396
397
398
-- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
-- SPSolved workItem' gives us a new *given* to go on 

399
-- @trySpontaneousSolve wi@ solves equalities where one side is a
400
-- touchable unification variable.
401
--     	    See Note [Touchables and givens] 
402
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
403
trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
404
                                       , cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
405
  | isGiven gw
406
  = return SPCantSolve
407
  | Just tv2 <- tcGetTyVar_maybe xi
408
409
  = do { tch1 <- isTouchableMetaTyVarTcS tv1
       ; tch2 <- isTouchableMetaTyVarTcS tv2
410
       ; case (tch1, tch2) of
dimitris's avatar
dimitris committed
411
412
413
           (True,  True)  -> trySpontaneousEqTwoWay d gw tv1 tv2
           (True,  False) -> trySpontaneousEqOneWay d gw tv1 xi
           (False, True)  -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
414
	   _ -> return SPCantSolve }
415
  | otherwise
416
  = do { tch1 <- isTouchableMetaTyVarTcS tv1
dimitris's avatar
dimitris committed
417
       ; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
418
419
420
421
                 else do { untch <- getUntouchables
                         ; traceTcS "Untouchable LHS, can't spontaneously solve workitem" $
                           vcat [text "Untouchables =" <+> ppr untch
                                , text "Workitem =" <+> ppr workItem ]
422
                         ; return SPCantSolve }
423
       }
424
425
426
427

  -- No need for 
  --      trySpontaneousSolve (CFunEqCan ...) = ...
  -- See Note [No touchables as FunEq RHS] in TcSMonad
428
trySpontaneousSolve _ = return SPCantSolve
429
430

----------------
431
432
trySpontaneousEqOneWay :: CtLoc -> CtEvidence 
                       -> TcTyVar -> Xi -> TcS SPSolveResult
433
-- tv is a MetaTyVar, not untouchable
dimitris's avatar
dimitris committed
434
trySpontaneousEqOneWay d gw tv xi
435
  | not (isSigTyVar tv) || isTyVarTy xi
Simon Peyton Jones's avatar
Simon Peyton Jones committed
436
  , typeKind xi `tcIsSubKind` tyVarKind tv
dimitris's avatar
dimitris committed
437
  = solveWithIdentity d gw tv xi
438
  | otherwise -- Still can't solve, sig tyvar and non-variable rhs
439
  = return SPCantSolve
440
441

----------------
442
443
trySpontaneousEqTwoWay :: CtLoc -> CtEvidence 
                       -> TcTyVar -> TcTyVar -> TcS SPSolveResult
444
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
445

dimitris's avatar
dimitris committed
446
trySpontaneousEqTwoWay d gw tv1 tv2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
447
448
449
450
451
452
  | k1 `tcIsSubKind` k2 && nicer_to_update_tv2
  = solveWithIdentity d gw tv2 (mkTyVarTy tv1)
  | k2 `tcIsSubKind` k1
  = solveWithIdentity d gw tv1 (mkTyVarTy tv2)
  | otherwise
  = return SPCantSolve
453
454
455
456
457
458
  where
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
    nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
\end{code}

459
Note [Kind errors] 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
460
~~~~~~~~~~~~~~~~~~
461
462
Consider the wanted problem: 
      alpha ~ (# Int, Int #) 
463
where alpha :: ArgKind and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, 
464
but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' 
465
simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and 
466
get quantified over in inference mode. That's bad because we do know at this point that the 
467
constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
468
469

The same applies in canonicalization code in case of kind errors in the givens. 
470

471
However, when we canonicalize givens we only check for compatibility (@compatKind@). 
472
If there were a kind error in the givens, this means some form of inconsistency or dead code.
473

474
475
476
477
478
You may think that when we spontaneously solve wanteds we may have to look through the 
bindings to determine the right kind of the RHS type. E.g one may be worried that xi is 
@alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
so this situation can't happen. 
479

480
481
Note [Spontaneous solving and kind compatibility] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
482
483
484
Note that our canonical constraints insist that *all* equalities (tv ~
xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
the same kinds.  ("compatible" means one is a subKind of the other.)
485

486
487
488
489
490
491
492
493
494
495
496
497
498
499
  - It can't be *equal* kinds, because
     b) wanted constraints don't necessarily have identical kinds
               eg   alpha::? ~ Int
     b) a solved wanted constraint becomes a given

  - SPJ thinks that *given* constraints (tv ~ tau) always have that
    tau has a sub-kind of tv; and when solving wanted constraints
    in trySpontaneousEqTwoWay we re-orient to achieve this.

  - Note that the kind invariant is maintained by rewriting.
    Eg wanted1 rewrites wanted2; if both were compatible kinds before,
       wanted2 will be afterwards.  Similarly givens.

Caveat:
500
501
502
503
504
505
506
507
508
  - Givens from higher-rank, such as: 
          type family T b :: * -> * -> * 
          type instance T Bool = (->) 

          f :: forall a. ((T a ~ (->)) => ...) -> a -> ... 
          flop = f (...) True 
     Whereas we would be able to apply the type instance, we would not be able to 
     use the given (T Bool ~ (->)) in the body of 'flop' 

509
510
511
512
513
514
515

Note [Avoid double unifications] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The spontaneous solver has to return a given which mentions the unified unification
variable *on the left* of the equality. Here is what happens if not: 
  Original wanted:  (a ~ alpha),  (alpha ~ Int) 
We spontaneously solve the first wanted, without changing the order! 
516
      given : a ~ alpha      [having unified alpha := a] 
517
518
519
Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
At the end we spontaneously solve that guy, *reunifying*  [alpha := Int] 

520
We avoid this problem by orienting the resulting given so that the unification
521
522
variable is on the left.  [Note that alternatively we could attempt to
enforce this at canonicalization]
523

524
525
526
See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
double unifications is the main reason we disallow touchable
unification variables as RHS of type family equations: F xis ~ alpha.
527
528
529

\begin{code}
----------------
530

531
solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
532
533
-- Solve with the identity coercion 
-- Precondition: kind(xi) is a sub-kind of kind(tv)
534
-- Precondition: CtEvidence is Wanted or Derived
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
535
536
-- See [New Wanted Superclass Work] to see why solveWithIdentity 
--     must work for Derived as well as Wanted
537
-- Returns: workItem where 
538
--        workItem = the new Given constraint
539
540
541
542
543
--
-- NB: No need for an occurs check here, because solveWithIdentity always 
--     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
--     say that in (a ~ xi), the type variable a does not appear in xi.
--     See TcRnTypes.Ct invariants.
544
solveWithIdentity _d wd tv xi 
dimitris's avatar
dimitris committed
545
546
  = do { let tv_ty = mkTyVarTy tv
       ; traceTcS "Sneaky unification:" $ 
547
                       vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
dimitris's avatar
dimitris committed
548
549
550
                             text "Coercion:" <+> pprEq tv_ty xi,
                             text "Left Kind is:" <+> ppr (typeKind tv_ty),
                             text "Right Kind is:" <+> ppr (typeKind xi) ]
551

552
553
554
555
556
557
       ; let xi' = defaultKind xi      
               -- We only instantiate kind unification variables
               -- with simple kinds like *, not OpenKind or ArgKind
               -- cf TcUnify.uUnboundKVar

       ; setWantedTyBind tv xi'
558
       ; let refl_evtm = EvCoercion (mkTcReflCo xi')
559

dimitris's avatar
dimitris committed
560
       ; when (isWanted wd) $ 
561
              setEvBind (ctev_evar wd) refl_evtm
562

563
       ; return (SPSolved tv) }
564
565
\end{code}

566
567
568
569
570
571
572

*********************************************************************************
*                                                                               * 
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

573
574
Note [

575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

   If the work-item is Given, 
   then the inert item must Given

But this isn't quite true.  Suppose we have, 
    c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
After processing the first two, we get
     c1: [G] beta ~ [alpha], c2 : [W] blah
Now, c3 does not interact with the the given c1, so when we spontaneously
solve c3, we must re-react it with the inert set.  So we can attempt a 
reaction between inert c2 [W] and work-item c3 [G].

It *is* true that [Solver Invariant]
   If the work-item is Given, 
   AND there is a reaction
   then the inert item must Given
or, equivalently,
   If the work-item is Given, 
   and the inert item is Wanted/Derived
   then there is no reaction

600
\begin{code}
601
-- Interaction result of  WorkItem <~> Ct
602

603
data InteractResult 
604
605
606
607
    = IRWorkItemConsumed { ir_fire :: String }    -- Work item discharged by interaction; stop
    | IRReplace          { ir_fire :: String }    -- Inert item replaced by work item; stop
    | IRInertConsumed    { ir_fire :: String }    -- Inert item consumed, keep going with work item 
    | IRKeepGoing        { ir_fire :: String }    -- Inert item remains, keep going with work item
608

609
610
611
612
interactWithInertsStage :: WorkItem -> TcS StopOrContinue 
-- Precondition: if the workitem is a CTyEqCan then it will not be able to 
-- react with anything at this stage. 
interactWithInertsStage wi 
613
614
615
616
  = do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
       ; rels <- extractRelevantInerts wi 
       ; traceTcS "relevant inerts are:" $ ppr rels
       ; foldlBagM interact_next (ContinueWith wi) rels }
617
618

  where interact_next Stop atomic_inert 
619
          = do { insertInertItemTcS atomic_inert; return Stop }
620
621
622
        interact_next (ContinueWith wi) atomic_inert 
          = do { ir <- doInteractWithInert atomic_inert wi
               ; let mk_msg rule keep_doc 
623
624
625
                       = vcat [ text rule <+> keep_doc
                              , ptext (sLit "InertItem =") <+> ppr atomic_inert
                              , ptext (sLit "WorkItem  =") <+> ppr wi ]
626
627
               ; case ir of 
                   IRWorkItemConsumed { ir_fire = rule } 
628
                       -> do { traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
629
630
631
                             ; insertInertItemTcS atomic_inert
                             ; return Stop } 
                   IRReplace { ir_fire = rule }
632
                       -> do { traceFireTcS atomic_inert 
633
634
                                            (mk_msg rule (text "InertReplace"))
                             ; insertInertItemTcS wi
635
636
                             ; return Stop } 
                   IRInertConsumed { ir_fire = rule }
637
                       -> do { traceFireTcS atomic_inert 
638
639
                                            (mk_msg rule (text "InertItemConsumed"))
                             ; return (ContinueWith wi) }
640
                   IRKeepGoing {}
641
                       -> do { insertInertItemTcS atomic_inert
642
643
                             ; return (ContinueWith wi) }
               }
644
645
\end{code}

646
\begin{code}
647
648
--------------------------------------------

649
650
doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
651
652
doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1, cc_loc = loc1 })
                     workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2, cc_loc = loc2 })
653
  | cls1 == cls2  
batterseapower's avatar
batterseapower committed
654
655
  = do { let pty1 = mkClassPred cls1 tys1
             pty2 = mkClassPred cls2 tys2
656
657
             inert_pred_loc     = (pty1, pprArisingAt loc1)
             work_item_pred_loc = (pty2, pprArisingAt loc2)
658

659
       ; let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
660
       ; fd_work <- rewriteWithFunDeps fd_eqns loc2
661
662
663
664
665
666
                -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                -- NB: We do create FDs for given to report insoluble equations that arise
                -- from pairs of Givens, and also because of floating when we approximate
                -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
                -- Also see Note [When improvement happens]
       
667
668
669
       ; traceTcS "doInteractWithInert:dict" 
                  (vcat [ text "inertItem =" <+> ppr inertItem
                        , text "workItem  =" <+> ppr workItem
670
                        , text "fundeps =" <+> ppr fd_work ])
671
 
672
       ; case fd_work of
673
           -- No Functional Dependencies 
674
           []  | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
675
               | otherwise         -> return (IRKeepGoing "NOP")
676
677

           -- Actual Functional Dependencies
678
           _   | cls1 `hasKey` ipClassNameKey
679
               , isGiven fl1, isGiven fl2  -- See Note [Shadowing of Implicit Parameters]
680
681
682
               -> return (IRReplace ("Replace IP"))

               -- Standard thing: create derived fds and keep on going. Importantly we don't
683
               -- throw workitem back in the worklist because this can cause loops. See #5236.
684
               | otherwise 
685
               -> do { updWorkListTcS (extendWorkListEqs fd_work)
686
                     ; return (IRKeepGoing "Cls/Cls (new fundeps)") } -- Just keep going without droping the inert 
687
       }
688
 
dimitris's avatar
dimitris committed
689
690
691
692
-- Two pieces of irreducible evidence: if their types are *exactly identical* 
-- we can rewrite them. We can never improve using this: 
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not 
-- mean that (ty1 ~ ty2)
693
694
695
doInteractWithInert (CIrredEvCan { cc_ev = ifl })
           workItem@(CIrredEvCan { cc_ev = wfl })
  | ctEvPred ifl `eqType` ctEvPred wfl
dimitris's avatar
dimitris committed
696
  = solveOneFromTheOther "Irred/Irred" ifl workItem
697

Simon Peyton Jones's avatar
Simon Peyton Jones committed
698
doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
699
                                  , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 }) 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
700
                    wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
701
                                  , cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
702
703
  | i_solves_w && (not (w_solves_i && isMetaTyVarTy xi1))
               -- See Note [Carefully solve the right CFunEqCan]
704
705
  = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
    do { traceTcS "interact with inerts: FunEq/FunEq" $ 
706
707
708
709
710
711
712
713
714
715
         vcat [ text "workItem =" <+> ppr wi
              , text "inertItem=" <+> ppr ii ]

       ; let xev = XEvTerm xcomp xdecomp
             -- xcomp : [(xi2 ~ xi1)] -> (F args ~ xi2) 
             xcomp [x] = EvCoercion (co1 `mkTcTransCo` mk_sym_co x)
             xcomp _   = panic "No more goals!"
             -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]                 
             xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]

716
       ; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev
717
718
             -- No caching!  See Note [Cache-caused loops]
             -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
719
       ; emitWorkNC d2 ctevs 
720
       ; return (IRWorkItemConsumed "FunEq/FunEq") }
721

722
723
724
  | fl2 `canSolve` fl1
  = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
    do { traceTcS "interact with inerts: FunEq/FunEq" $ 
725
726
727
728
729
         vcat [ text "workItem =" <+> ppr wi
              , text "inertItem=" <+> ppr ii ]

       ; let xev = XEvTerm xcomp xdecomp
              -- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)]
730
             xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x)
731
732
             xcomp _ = panic "No more goals!"
             -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
733
             xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
734

735
       ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev 
736
             -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
737

738
       ; emitWorkNC d1 ctevs 
739
       ; return (IRInertConsumed "FunEq/FunEq") }
740
  where
741
    lhss_match = tc1 == tc2 && eqTypes args1 args2 
Simon Peyton Jones's avatar
Simon Peyton Jones committed
742
743
    co1 = evTermCoercion $ ctEvTerm ev1
    co2 = evTermCoercion $ ctEvTerm ev2
744
    mk_sym_co x = mkTcSymCo (evTermCoercion x)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
745
746
    fl1 = ctEvFlavour ev1
    fl2 = ctEvFlavour ev2
747
748
749

    i_solves_w = fl1 `canSolve` fl2 
    w_solves_i = fl2 `canSolve` fl1 
dimitris's avatar
dimitris committed
750
    
751

752
doInteractWithInert _ _ = return (IRKeepGoing "NOP")
753
754
\end{code}

755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
Note [Efficient Orientation] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are interacting two FunEqCans with the same LHS:
          (inert)  ci :: (F ty ~ xi_i) 
          (work)   cw :: (F ty ~ xi_w) 
We prefer to keep the inert (else we pass the work item on down
the pipeline, which is a bit silly).  If we keep the inert, we
will (a) discharge 'cw' 
     (b) produce a new equality work-item (xi_w ~ xi_i)
Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
    new_work :: xi_w ~ xi_i
    cw := ci ; sym new_work
Why?  Consider the simplest case when xi1 is a type variable.  If
we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
If we generate xi2~xi1, there is less chance of that happening.
Of course it can and should still happen if xi1=a, xi1=Int, say.
But we want to avoid it happening needlessly.

Similarly, if we *can't* keep the inert item (because inert is Wanted,
and work is Given, say), we prefer to orient the new equality (xi_i ~
xi_w).

777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
Note [Carefully solve the right CFunEqCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the constraints
  c1 :: F Int ~ a      -- Arising from an application line 5
  c2 :: F Int ~ Bool   -- Arising from an application line 10
Suppose that 'a' is a unification variable, arising only from 
flattening.  So there is no error on line 5; it's just a flattening
variable.  But there is (or might be) an error on line 10.

Two ways to combine them, leaving either (Plan A)
  c1 :: F Int ~ a      -- Arising from an application line 5
  c3 :: a ~ Bool       -- Arising from an application line 10
or (Plan B)
  c2 :: F Int ~ Bool   -- Arising from an application line 10
  c4 :: a ~ Bool       -- Arising from an application line 5

Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
on the *totally innocent* line 5.  An example is test SimpleFail16
where the expected/actual message comes out backwards if we use
the wrong plan.

The second is the right thing to do.  Hence the isMetaTyVarTy
test when solving pairwise CFunEqCan.
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851

Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Consider the following example:

f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x

The "let ?x = ..." generates an implication constraint of the form:

?x :: Char => ?x :: Char

Furthermore, the signature for `f` also generates an implication
constraint, so we end up with the following nested implication:

?x :: Char => (?x :: Char => ?x :: Char)

Note that the wanted (?x :: Char) constraint may be solved in
two incompatible ways:  either by using the parameter from the
signature, or by using the local definition.  Our intention is
that the local definition should "shadow" the parameter of the
signature, and we implement this as follows: when we add a new
given implicit parameter to the inert set, it replaces any existing
givens for the same implicit parameter.

This works for the normal cases but it has an odd side effect
in some pathological programs like this:

-- This is accepted, the second parameter shadows
f1 :: (?x :: Int, ?x :: Char) => Char
f1 = ?x

-- This is rejected, the second parameter shadows
f2 :: (?x :: Int, ?x :: Char) => Int
f2 = ?x

Both of these are actually wrong:  when we try to use either one,
we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
which would lead to an error.

I can think of two ways to fix this:

  1. Simply disallow multiple constratits for the same implicit
    parameter---this is never useful, and it can be detected completely
    syntactically.

  2. Move the shadowing machinery to the location where we nest
     implications, and add some code here that will produce an
     error if we get multiple givens for the same implicit parameter.


852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in our 
solved cache (which is the default behaviour or xCtFlavor), because the interaction 
may not be contributing towards a solution. Here is an example:

Initial inert set:
  [W] g1 : F a ~ beta1
Work item:
  [W] g2 : F a ~ beta2
The work item will react with the inert yielding the _same_ inert set plus:
    i)   Will set g2 := g1 `cast` g3   
    ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
    iii) Will emit [W] g3 : beta1 ~ beta2 
Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it 
will set 
      g1 := g ; sym g3 
and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
remember that we have this in our solved cache, and it is ... g2! In short we 
created the evidence loop:

        g2 := g1 ; g3 
        g3 := refl
        g1 := g2 ; sym g3 

To avoid this situation we do not cache as solved any workitems (or inert) 
which did not really made a 'step' towards proving some goal. Solved's are 
just an optimization so we don't lose anything in terms of completeness of 
solving.

\begin{code}
dimitris's avatar
dimitris committed
884
solveOneFromTheOther :: String    -- Info 
885
                     -> CtEvidence  -- Inert 
886
887
888
889
890
                     -> Ct        -- WorkItem 
                     -> TcS InteractResult
-- Preconditions: 
-- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only
dimitris's avatar
dimitris committed
891
solveOneFromTheOther info ifl workItem
892
  | isDerived wfl
893
  = return (IRWorkItemConsumed ("Solved[DW] " ++ info))
894

895
896
897
  | isDerived ifl -- The inert item is Derived, we can just throw it away, 
    	      	  -- The workItem is inert wrt earlier inert-set items, 
		  -- so it's safe to continue on from this point
898
  = return (IRInertConsumed ("Solved[DI] " ++ info))
899
  
Simon Peyton Jones's avatar
Simon Peyton Jones committed
900
  | CtWanted { ctev_evar = ev_id } <- wfl
901
902
  = do { setEvBind ev_id (ctEvTerm ifl); return (IRWorkItemConsumed ("Solved(w) " ++ info)) }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
903
  | CtWanted { ctev_evar = ev_id } <- ifl
904
905
906
  = do { setEvBind ev_id (ctEvTerm wfl); return (IRInertConsumed ("Solved(g) " ++ info)) }

  | otherwise	   -- If both are Given, we already have evidence; no need to duplicate
907
908
                   -- But the work item *overrides* the inert item (hence IRReplace)
                   -- See Note [Shadowing of Implicit Parameters]
909
  = return (IRReplace ("Replace(gg) " ++ info))
910
  where 
911
     wfl = cc_ev workItem
912
913
\end{code}

914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:

f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x

The "let ?x = ..." generates an implication constraint of the form:

?x :: Char => ?x :: Char


Furthermore, the signature for `f` also generates an implication
constraint, so we end up with the following nested implication:

?x :: Char => (?x :: Char => ?x :: Char)

Note that the wanted (?x :: Char) constraint may be solved in
two incompatible ways:  either by using the parameter from the
signature, or by using the local definition.  Our intention is
that the local definition should "shadow" the parameter of the
signature, and we implement this as follows: when we nest implications,
we remove any implicit parameters in the outer implication, that
have the same name as givens of the inner implication.

Here is another variation of the example:

f :: (?x :: Int) => Char
f = let ?x = 'x' in ?x

This program should also be accepted: the two constraints `?x :: Int`
and `?x :: Char` never exist in the same context, so they don't get to
interact to cause failure.

948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
Note [Superclasses and recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Overlaps with Note [SUPERCLASS-LOOP 1]
                  Note [SUPERCLASS-LOOP 2]
                  Note [Recursive instances and superclases]
    ToDo: check overlap and delete redundant stuff

Right before adding a given into the inert set, we must
produce some more work, that will bring the superclasses 
of the given into scope. The superclass constraints go into 
our worklist. 

When we simplify a wanted constraint, if we first see a matching
instance, we may produce new wanted work. To (1) avoid doing this work 
twice in the future and (2) to handle recursive dictionaries we may ``cache'' 
963
964
965
this item as given into our inert set WITHOUT adding its superclass constraints, 
otherwise we'd be in danger of creating a loop [In fact this was the exact reason
for doing the isGoodRecEv check in an older version of the type checker]. 
966
967
968
969
970
971
972
973
974
975

But now we have added partially solved constraints to the worklist which may 
interact with other wanteds. Consider the example: 

Example 1: 

    class Eq b => Foo a b        --- 0-th selector
    instance Eq a => Foo [a] a   --- fooDFun

and wanted (Foo [t] t). We are first going to see that the instance matches 
976
and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
977
978
979
980
       d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3 
Our work list is going to contain a new *wanted* goal
       d3 :_w Eq t 

981
Ok, so how do we get recursive dictionaries, at all: 
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053

Example 2:

    data D r = ZeroD | SuccD (r (D r));
    
    instance (Eq (r (D r))) => Eq (D r) where
        ZeroD     == ZeroD     = True
        (SuccD a) == (SuccD b) = a == b
        _         == _         = False;
    
    equalDC :: D [] -> D [] -> Bool;
    equalDC = (==);

We need to prove (Eq (D [])). Here's how we go:

	d1 :_w Eq (D [])

by instance decl, holds if
	d2 :_w Eq [D []]
	where 	d1 = dfEqD d2

*BUT* we have an inert set which gives us (no superclasses): 
        d1 :_g Eq (D []) 
By the instance declaration of Eq we can show the 'd2' goal if 
	d3 :_w Eq (D [])
	where	d2 = dfEqList d3
		d1 = dfEqD d2
Now, however this wanted can interact with our inert d1 to set: 
        d3 := d1 
and solve the goal. Why was this interaction OK? Because, if we chase the 
evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we 
are really setting
        d3 := dfEqD2 (dfEqList d3) 
which is FINE because the use of d3 is protected by the instance function 
applications. 

So, our strategy is to try to put solved wanted dictionaries into the
inert set along with their superclasses (when this is meaningful,
i.e. when new wanted goals are generated) but solve a wanted dictionary
from a given only in the case where the evidence variable of the
wanted is mentioned in the evidence of the given (recursively through
the evidence binds) in a protected way: more instance function applications 
than superclass selectors.

Here are some more examples from GHC's previous type checker


Example 3: 
This code arises in the context of "Scrap Your Boilerplate with Class"

    class Sat a
    class Data ctx a
    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2

    class Data Maybe a => Foo a    

    instance Foo t => Sat (Maybe t)                             -- dfunSat

    instance Data Maybe a => Foo a                              -- dfunFoo1
    instance Foo a        => Foo [a]                            -- dfunFoo2
    instance                 Foo [Char]                         -- dfunFoo3

Consider generating the superclasses of the instance declaration
	 instance Foo a => Foo [a]

So our problem is this
    d0 :_g Foo t
    d1 :_w Data Maybe [t] 

We may add the given in the inert set, along with its superclasses
[assuming we don't fail because there is a matching instance, see 
1054
 topReactionsStage, given case ]
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
  Inert:
    d0 :_g Foo t 
  WorkList 
    d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0 
    d1 :_w Data Maybe [t] 
Then d2 can readily enter the inert, and we also do solving of the wanted
  Inert: 
    d0 :_g Foo t 
    d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
  WorkList
    d2 :_w Sat (Maybe [t])          
    d3 :_w Data Maybe t
    d01 :_g Data Maybe t 
Now, we may simplify d2 more: 
  Inert:
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d1 :_g Data Maybe [t] 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
  WorkList: 
      d3 :_w Data Maybe t 
      d4 :_w Foo [t] 
      d01 :_g Data Maybe t 

Now, we can just solve d3.
  Inert
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
  WorkList
      d4 :_w Foo [t] 
      d01 :_g Data Maybe t 
And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
  Inert
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
      d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
  WorkList:
      d5 :_w Foo t 
      d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
      d01 :_g Data Maybe t 
Now, d5 can be solved! (and its superclass enter scope) 
  Inert
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
      d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
      d5 :_g Foo t                    d5 := dfunFoo1 d7
  WorkList:
      d7 :_w Data Maybe t
      d6 :_g Data Maybe [t]
      d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
      d01 :_g Data Maybe t 

Now, two problems: 
   [1] Suppose we pick d8 and we react him with d01. Which of the two givens should 
       we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence 
       that must not be used (look at case interactInert where both inert and workitem
       are givens). So we have several options: 
       - Drop the workitem always (this will drop d8)
              This feels very unsafe -- what if the work item was the "good" one
              that should be used later to solve another wanted?
       - Don't drop anyone: the inert set may contain multiple givens! 
              [This is currently implemented] 

The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2: 
  [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
      d7. Now the [isRecDictEv] function in the ineration solver 
      [case inert-given workitem-wanted] will prevent us from interacting d7 := d8 
      precisely because chasing the evidence of d8 leads us to an unguarded use of d7. 

      So, no interaction happens there. Then we meet d01 and there is no recursion 
      problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01! 
             
Note [SUPERCLASS-LOOP 1]
~~~~~~~~~~~~~~~~~~~~~~~~
We have to be very, very careful when generating superclasses, lest we
accidentally build a loop. Here's an example:

  class S a

  class S a => C a where { opc :: a -> a }
  class S b => D b where { opd :: b -> b }
  
  instance C Int where
     opc = opd
  
  instance D Int where
     opd = opc

From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
Simplifying, we may well get:
	$dfCInt = :C ds1 (opd dd)
	dd  = $dfDInt
	ds1 = $p1 dd
Notice that we spot that we can extract ds1 from dd.  

Alas!  Alack! We can do the same for (instance D Int):

	$dfDInt = :D ds2 (opc dc)
	dc  = $dfCInt
	ds2 = $p1 dc

And now we've defined the superclass in terms of itself.
Two more nasty cases are in
	tcrun021
	tcrun033

Solution: 
  - Satisfy the superclass context *all by itself* 
    (tcSimplifySuperClasses)
  - And do so completely; i.e. no left-over constraints
    to mix with the constraints arising from method declarations


Note [SUPERCLASS-LOOP 2]
~~~~~~~~~~~~~~~~~~~~~~~~
We need to be careful when adding "the constaint we are trying to prove".
Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where

	class Ord a => C a where
	instance Ord [a] => C [a] where ...

Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
superclasses of C [a] to avails.  But we must not overwrite the binding
for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
build a loop! 

Here's another variant, immortalised in tcrun020
	class Monad m => C1 m
	class C1 m => C2 m x
	instance C2 Maybe Bool
For the instance decl we need to build (C1 Maybe), and it's no good if
we run around and add (C2 Maybe Bool) and its superclasses to the avails 
before we search for C1 Maybe.

Here's another example 
 	class Eq b => Foo a b
	instance Eq a => Foo [a] a
If we are reducing
	(Foo [t] t)

we'll first deduce that it holds (via the instance decl).  We must not
then overwrite the Eq t constraint with a superclass selection!

At first I had a gross hack, whereby I simply did not add superclass constraints
in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
becuase it lost legitimate superclass sharing, and it still didn't do the job:
I found a very obscure program (now tcrun021) in which improvement meant the
simplifier got two bites a the cherry... so something seemed to be an Stop
first time, but reducible next time.

Now we implement the Right Solution, which is to check for loops directly 
when adding superclasses.  It's a bit like the occurs check in unification.

Note [Recursive instances and superclases]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this code, which arises in the context of "Scrap Your 
Boilerplate with Class".  

    class Sat a
    class Data ctx a
    instance  Sat (ctx Char)             => Data ctx Char
    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]

    class Data Maybe a => Foo a

    instance Foo t => Sat (Maybe t)

    instance Data Maybe a => Foo a
    instance Foo a        => Foo [a]
    instance                 Foo [Char]

In the instance for Foo [a], when generating evidence for the superclasses
(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
Using the instance for Data, we therefore need
        (Sat (Maybe [a], Data Maybe a)
But we are given (Foo a), and hence its superclass (Data Maybe a).
So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
we need (Foo [a]).  And that is the very dictionary we are bulding
an instance for!  So we must put that in the "givens".  So in this
case we have
	Given:  Foo a, Foo [a]
	Wanted: Data Maybe [a]

BUT we must *not not not* put the *superclasses* of (Foo [a]) in
the givens, which is what 'addGiven' would normally do. Why? Because
(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted 
by selecting a superclass from Foo [a], which simply makes a loop.

On the other hand we *must* put the superclasses of (Foo a) in
the givens, as you can see from the derivation described above.

Conclusion: in the very special case of tcSimplifySuperClasses
we have one 'given' (namely the "this" dictionary) whose superclasses
must not be added to 'givens' by addGiven.  

There is a complication though.  Suppose there are equalities
      instance (Eq a, a~b) => Num (a,b)
Then we normalise the 'givens' wrt the equalities, so the original
given "this" dictionary is cast to one of a different type.  So it's a
bit trickier than before to identify the "special" dictionary whose
superclasses must not be added. See test
   indexed-types/should_run/EqInInstance

We need a persistent property of the dictionary to record this
special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
but cool), which is maintained by dictionary normalisation.
Specifically, the InstLocOrigin is
	     NoScOrigin
then the no-superclass thing kicks in.  WATCH OUT if you fiddle
with InstLocOrigin!

Note [MATCHING-SYNONYMS]
~~~~~~~~~~~~~~~~~~~~~~~~
When trying to match a dictionary (D tau) to a top-level instance, or a 
type family equation (F taus_1 ~ tau_2) to a top-level family instance, 
we do *not* need to expand type synonyms because the matcher will do that for us.


Note [RHS-FAMILY-SYNONYMS] 
~~~~~~~~~~~~~~~~~~~~~~~~~~
The RHS of a family instance is represented as yet another constructor which is 
like a type synonym for the real RHS the programmer declared. Eg: 
    type instance F (a,a) = [a] 
Becomes: 
    :R32 a = [a]      -- internal type synonym introduced
    F (a,a) ~ :R32 a  -- instance 

When we react a family instance with a type family equation in the work list 
we keep the synonym-using RHS without expansion. 


1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
%************************************************************************
%*                                                                      *
%*          Functional dependencies, instantiation of equations
%*                                                                      *
%************************************************************************

When we spot an equality arising from a functional dependency,
we now use that equality (a "wanted") to rewrite the work-item
constraint right away.  This avoids two dangers

 Danger 1: If we send the original constraint on down the pipeline
           it may react with an instance declaration, and in delicate
	   situations (when a Given overlaps with an instance) that
	   may produce new insoluble goals: see Trac #4952

 Danger 2: If we don't rewrite the constraint, it may re-react
           with the same thing later, and produce the same equality
           again --> termination worries.

To achieve this required some refactoring of FunDeps.lhs (nicer
now!).  

\begin{code}
1312
1313
rewriteWithFunDeps :: [Equation] -> CtLoc -> TcS [Ct] 
-- NB: The returned constraints are all Derived
1314
-- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1315
1316
1317
1318
1319
rewriteWithFunDeps eqn_pred_locs loc
 = do { fd_cts <- mapM (instFunDepEqn loc) eqn_pred_locs
      ; return (concat fd_cts) }

instFunDepEqn :: CtLoc -> Equation -> TcS [Ct]
1320
-- Post: Returns the position index as well as the corresponding FunDep equality
1321
1322
instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
                         , fd_pred1 = d1, fd_pred2 = d2 })
1323
  = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
1324
1325
       ; foldM (do_one subst) [] eqs }
  where 
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
    der_loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc

    do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
       | eqType sty1 sty2 
       = return ievs -- Return no trivial equalities
       | otherwise
       = do { mb_eqv <- newDerived (mkTcEqPred sty1 sty2)
            ; case mb_eqv of
                 Just ev -> return (mkNonCanonical der_loc ev : ievs)
                 Nothing -> return ievs }
                   -- We are eventually going to emit FD work back in the work list so 
                   -- it is important that we only return the /freshly created/ and not 
                   -- some existing equality!
       where
         sty1 = Type.substTy subst ty1 
         sty2 = Type.substTy subst ty2 
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358

mkEqnMsg :: (TcPredType, SDoc) 
         -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
  = do  { zpred1 <- zonkTcPredType pred1
        ; zpred2 <- zonkTcPredType pred2
	; let { tpred1 = tidyType tidy_env zpred1
              ; tpred2 = tidyType tidy_env zpred2 }
	; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
			  nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), 
			  nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
	; return (tidy_env, msg) }
\end{code}




1359
1360
1361
1362
1363
1364
1365
*********************************************************************************
*                                                                               * 
                       The top-reaction Stage
*                                                                               *
*********************************************************************************

\begin{code}
1366
1367
topReactionsStage :: WorkItem -> TcS StopOrContinue
topReactionsStage wi 
1368
 = do { inerts <- getTcSInerts
1369
1370
      ; tir <- doTopReact inerts wi
      ; case tir of 
1371
1372
          NoTopInt -> return (ContinueWith wi)
          SomeTopInt rule what_next 
1373
                   -> do { traceFireTcS wi $
1374
1375
1376
                           vcat [ ptext (sLit "Top react:") <+> text rule
                                , text "WorkItem =" <+> ppr wi ]
                         ; return what_next } }
1377

1378
data TopInteractResult 
1379
1380
 = NoTopInt
 | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
1381
1382


dimitris's avatar
dimitris committed
1383
doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1384
1385
1386
1387
1388
1389
1390
1391
1392
-- The work item does not react with the inert set, so try interaction with top-level 
-- instances. Note:
--
--   (a) The place to add superclasses in not here in doTopReact stage. 
--       Instead superclasses are added in the worklist as part of the
--       canonicalization process. See Note [Adding superclasses].
--
--   (b) See Note [Given constraint that matches an instance declaration] 
--       for some design decisions for given dictionaries. 
1393

1394
doTopReact inerts workItem
1395
  = do { traceTcS "doTopReact" (ppr workItem)
1396
1397
       ; case workItem of
      	   CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
1398
      	            , cc_loc = d }
1399
1400
1401
      	      -> doTopReactDict inerts workItem fl cls xis d

      	   CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
1402
      	             , cc_rhs = xi, cc_loc = d }
1403
      	      -> doTopReactFunEq workItem fl tc args xi d
1404
1405
1406
1407
1408
1409

      	   _  -> -- Any other work item does not react with any top-level equations
      	         return NoTopInt  }

--------------------
doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
1410
1411
               -> CtLoc -> TcS TopInteractResult
doTopReactDict inerts workItem fl cls xis loc
1412
  = do { instEnvs <- getInstEnvs 
1413
1414
       ; let pred = mkClassPred cls xis
             fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
1415
             
1416
1417
1418
1419
       ; fd_work <- rewriteWithFunDeps fd_eqns loc
       ; if not (null fd_work) then
            do { updWorkListTcS (extendWorkListEqs fd_work)
               ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
                                   , tir_new_item = ContinueWith workItem } }
         else if not (isWanted fl) then 
            return NoTopInt
         else do

       { solved_dicts <- getTcSInerts >>= (return . inert_solved_dicts)
       ; case lookupSolvedDict solved_dicts pred of {
            Just ev -> do { setEvBind dict_id (ctEvTerm ev); 
                          ; return $ 
                            SomeTopInt { tir_rule = "Dict/Top (cached)" 
                                       , tir_new_item = Stop } } ;
            Nothing -> do

      { lkup_inst_res  <- matchClassInst inerts cls xis loc
      ; case lkup_inst_res of
           GenInst wtvs ev_term -> do { addSolvedDict fl 
                                      ; doSolveFromInstance wtvs ev_term }
           NoInstance -> return NoTopInt } } } }
1438
   where 
1439
     arising_sdoc = pprArisingAt loc
1440
1441
     dict_id = ctEvId fl
     
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
     doSolveFromInstance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
      -- Precondition: evidence term matches the predicate workItem
     doSolveFromInstance evs ev_term 
        | null evs
        = do { traceTcS "doTopReact/found nullary instance for" $
               ppr dict_id
             ; setEvBind dict_id ev_term
             ; return $ 
               SomeTopInt { tir_rule = "Dict/Top (solved, no new work)" 
                          , tir_new_item = Stop } }
        | otherwise 
        = do { traceTcS "doTopReact/found non-nullary instance for" $ 
               ppr dict_id
             ; setEvBind dict_id ev_term
             ; let mk_new_wanted ev
1457
1458
                       = CNonCanonical { cc_ev  = ev
                                       , cc_loc = bumpCtLocDepth loc }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1459
             ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1460
1461
             ; return $
               SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
1462
                          , tir_new_item = Stop } }
1463

1464
--------------------
1465
doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
1466
                -> CtLoc -> TcS TopInteractResult
1467
doTopReactFunEq _ct fl fun_tc args xi loc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1468
  = ASSERT (isSynFamilyTyCon fun_tc) -- No associated data families have 
1469
1470
                                     -- reached this far 
    -- Look in the cache of solved funeqs
1471
    do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
1472
       ; case lookupFamHead fun_eq_cache fam_ty of {
1473
           Just (ctev, rhs_ty)
1474
1475
1476
             | ctEvFlavour ctev `canRewrite` ctEvFlavour fl
             -> ASSERT( not (isDerived ctev) )
                succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
1477
           _other -> 
1478
1479

    -- Look up in top-level instances
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1480
    do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
1481
1482
       ; case match_res of {
           Nothing -> return NoTopInt ;
1483
1484
1485
           Just (FamInstMatch { fim_instance = famInst
                              , fim_index    = index
                              , fim_tys      = rep_tys }) -> 
1486
1487
1488

    -- Found a top-level instance
    do {    -- Add it to the solved goals
1489
         unless (isDerived fl) (addSolvedFunEq fam_ty fl xi)
1490
1491

       ; let coe_ax = famInstAxiom famInst 
1492
1493
       ; succeed_with "Fun/Top" (mkTcAxInstCo coe_ax index rep_tys)
                      (mkAxInstRHS coe_ax index rep_tys) } } } } }
1494
  where