TcTyFuns.lhs 67.7 KB
Newer Older
1
2
Normalisation of type terms relative to type instances as well as
normalisation and entailment checking of equality constraints.
3
4

\begin{code}
5
module TcTyFuns (
6
7
  -- type normalisation wrt to toplevel equalities only
  tcNormaliseFamInst,
8

9
10
  -- instance normalisation wrt to equalities
  tcReduceEqs,
11
12
13
14

  -- errors
  misMatchMsg, failWithMisMatch,

15
) where
16
17
18
19


#include "HsVersions.h"

20
--friends
21
22
23
24
25
import TcRnMonad
import TcEnv
import Inst
import TcType
import TcMType
26
27

-- GHC
28
29
import Coercion
import Type
30
31
32
33
import TypeRep 	( Type(..) )
import TyCon
import HsSyn
import VarEnv
34
import VarSet
35
36
import Var
import Name
37
38
39
40
import Bag
import Outputable
import SrcLoc	( Located(..) )
import Maybes
41
import MonadUtils
42
import FastString
43

44
-- standard
45
import Data.List
46
import Control.Monad
47
48
49
50
51
\end{code}


%************************************************************************
%*									*
52
		Normalisation of types wrt toplevel equality schemata
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
%*									*
%************************************************************************

Unfold a single synonym family instance and yield the witnessing coercion.
Return 'Nothing' if the given type is either not synonym family instance
or is a synonym family instance that has no matching instance declaration.
(Applies only if the type family application is outermost.)

For example, if we have

  :Co:R42T a :: T [a] ~ :R42T a

then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).

\begin{code}
tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
tcUnfoldSynFamInst (TyConApp tycon tys)
  | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
  = return Nothing
  | otherwise
73
74
  = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
       ; maybeFamInst <- tcLookupFamInst tycon tys
75
76
       ; case maybeFamInst of
           Nothing                -> return Nothing
77
78
           Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
		                                    mkTyConApp coe_tc rep_tys)
79
             where
80
               coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" 
81
82
83
84
85
86
87
88
                                   (tyConFamilyCoercion_maybe rep_tc)
       }
tcUnfoldSynFamInst _other = return Nothing
\end{code}

Normalise 'Type's and 'PredType's by unfolding type family applications where
possible (ie, we treat family instances as a TRS).  Also zonk meta variables.

89
	tcNormaliseFamInst ty = (co, ty')
90
91
92
	then   co : ty ~ ty'

\begin{code}
93
94
95
96
-- |Normalise the given type as far as possible with toplevel equalities.
-- This results in a coercion witnessing the type equality, in addition to the
-- normalised type.
--
97
98
tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
\end{code}

Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
apply the normalisation function gives as the first argument to every TyConApp
and every TyVarTy subterm.

	tcGenericNormaliseFamInst fun ty = (co, ty')
	then   co : ty ~ ty'

This function is (by way of using smart constructors) careful to ensure that
the returned coercion is exactly IdCo (and not some semantically equivalent,
but syntactically different coercion) whenever (ty' `tcEqType` ty).  This
makes it easy for the caller to determine whether the type changed.  BUT
even if we return IdCo, ty' may be *syntactically* different from ty due to
unfolded closed type synonyms (by way of tcCoreView).  In the interest of
good error messages, callers should discard ty' in favour of ty in this case.
115

116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
\begin{code}
tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion))) 	
                             -- what to do with type functions and tyvars
	                   -> TcType  			-- old type
	                   -> TcM (CoercionI, TcType)	-- (coercion, new type)
tcGenericNormaliseFamInst fun ty
  | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty' 
tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
  = do	{ (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
	; let tycon_coi = mkTyConAppCoI tyCon ntys cois
	; maybe_ty_co <- fun (mkTyConApp tyCon ntys)     -- use normalised args!
	; case maybe_ty_co of
	    -- a matching family instance exists
	    Just (ty', co) ->
	      do { let first_coi = mkTransCoI tycon_coi (ACo co)
		 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
		 ; let fix_coi = mkTransCoI first_coi rest_coi
	   	 ; return (fix_coi, nty)
		 }
	    -- no matching family instance exists
	    -- we do not do anything
	    Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
	}
tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
  = do	{ (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
	; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
	; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
	}
tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
  = do	{ (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
	; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
	; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
	}
tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
  = do 	{ (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
	; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
	}
tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
  | isTcTyVar tv
  = do	{ traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
	; res <- lookupTcTyVar tv
	; case res of
	    DoneTv _ -> 
	      do { maybe_ty' <- fun ty
		 ; case maybe_ty' of
		     Nothing	     -> return (IdCo, ty)
		     Just (ty', co1) -> 
                       do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
			  ; return (ACo co1 `mkTransCoI` coi2, ty'') 
			  }
		 }
	    IndirectTv ty' -> tcGenericNormaliseFamInst fun ty' 
	}
  | otherwise
  = return (IdCo, ty)
tcGenericNormaliseFamInst fun (PredTy predty)
  = do 	{ (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
	; return (coi, PredTy pred') }

---------------------------------
tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
	                      -> TcPredType
	                      -> TcM (CoercionI, TcPredType)

tcGenericNormaliseFamInstPred fun (ClassP cls tys) 
  = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
       ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
       }
tcGenericNormaliseFamInstPred fun (IParam ipn ty) 
  = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
       ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
       }
tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2) 
  = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
       ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
       ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
192
193
\end{code}

194
195
196
197
198
199
200

%************************************************************************
%*									*
		Normalisation of instances wrt to equalities
%*									*
%************************************************************************

201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
Given a set of given, local constraints and a set of wanted constraints,
simplify the wanted equalities as far as possible and normalise both local and
wanted dictionaries with respect to the equalities.

In addition to the normalised local dictionaries and simplified wanteds, the
function yields bindings for instantiated meta variables (due to solving
equality constraints) and dictionary bindings (due to simplifying class
constraints).  The bag of type variable bindings only contains bindings for
non-local variables - i.e., type variables other than those newly created by
the present function.  Consequently, type improvement took place iff the bag
of bindings contains any bindings for proper type variables (not just covars).
The solver does not instantiate any non-local variables; i.e., the bindings
must be executed by the caller.

All incoming constraints are assumed to be zonked already.  All outgoing
constraints will be zonked again.

NB: The solver only has local effects that cannot be observed from outside.
    In particular, it can be executed twice on the same constraint set with
    the same result (modulo generated variables names).

222
223
224
225
226
\begin{code}
tcReduceEqs :: [Inst]             -- locals
            -> [Inst]             -- wanteds
            -> TcM ([Inst],       -- normalised locals (w/o equalities)
                    [Inst],       -- normalised wanteds (including equalities)
227
228
                    TcTyVarBinds, -- bindings for meta type variables
                    TcDictBinds)  -- bindings for all simplified dictionaries
229
tcReduceEqs locals wanteds
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
  = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
           do { let (local_eqs  , local_dicts)   = partition isEqInst locals
                    (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
              ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
              ; eqCfg2 <- normaliseDicts False local_dicts
              ; eqCfg3 <- normaliseDicts True  wanteds_dicts
              ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` 
                                       eqCfg2 `unionEqConfig`
                                       eqCfg3) 
              ; finaliseEqsAndDicts freeFlexibles eqCfg
              }
         -- execute type bindings of skolem flexibles...
       ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
         -- ...and zonk the constraints to propagate the bindings
       ; locals_z  <- zonkInsts locals
       ; wanteds_z <- zonkInsts wanteds
       ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
247
       }
248
249
250
251
252
253
254
255
256
257
258
259
260
261
   where
     -- unification variables that appear in the environment and may not be
     -- instantiated - this includes coercion variables
     freeFlexibles = tcTyVarsOfInsts locals `unionVarSet` 
                     tcTyVarsOfInsts wanteds

     pruneTyBinds tybinds freeFlexibles
       = do { let tybinds'                      = bagToList tybinds
                  (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
            ; execTcTyVarBinds (listToBag skolem_tybinds)
            ; return $ listToBag env_tybinds
            }
       where
         isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
262
263
264
\end{code}


265
266
267
268
269
270
271
%************************************************************************
%*									*
		Equality Configurations
%*									*
%************************************************************************

We maintain normalised equalities together with the skolems introduced as
272
intermediates during flattening of equalities as well as 
273
274
275
276

\begin{code}
-- |Configuration of normalised equalities used during solving.
--
277
278
279
280
data EqConfig = EqConfig { eqs     :: [RewriteInst]     -- all equalities
                         , locals  :: [Inst]            -- given dicts
                         , wanteds :: [Inst]            -- wanted dicts
                         , binds   :: TcDictBinds       -- bindings
281
282
283
284
                         }

addEq :: EqConfig -> RewriteInst -> EqConfig
addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300

unionEqConfig :: EqConfig -> EqConfig -> EqConfig
unionEqConfig eqc1 eqc2 = EqConfig 
                          { eqs     = eqs eqc1 ++ eqs eqc2
                          , locals  = locals eqc1 ++ locals eqc2
                          , wanteds = wanteds eqc1 ++ wanteds eqc2
                          , binds   = binds eqc1 `unionBags` binds eqc2
                          }

emptyEqConfig :: EqConfig
emptyEqConfig = EqConfig
                { eqs     = []
                , locals  = []
                , wanteds = []
                , binds   = emptyBag
                }
301
302
303
304

instance Outputable EqConfig where
  ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
    = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
305
306
307
308
309
310
311
312
313
314
315
316
317
318
\end{code}

The set of operations on an equality configuration.  We obtain the initialise
configuration by normalisation ('normaliseEqs'), solve the equalities by
propagation ('propagateEqs'), and eventually finalise the configuration when
no further propoagation is possible.

\begin{code}
-- |Turn a set of equalities into an equality configuration for solving.
--
-- Precondition: The Insts are zonked.
--
normaliseEqs :: [Inst] -> TcM EqConfig
normaliseEqs eqs 
319
  = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )
320
       ; traceTc $ ptext (sLit "Entering normaliseEqs")
321

322
323
       ; eqss <- mapM normEqInst eqs
       ; return $ emptyEqConfig { eqs = concat eqss }
324
325
326
327
328
329
330
331
332
333
       }

-- |Flatten the type arguments of all dictionaries, returning the result as a 
-- equality configuration.  The dictionaries go into the 'wanted' component if 
-- the second argument is 'True'.
--
-- Precondition: The Insts are zonked.
--
normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
normaliseDicts isWanted insts
334
335
336
337
  = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
                         ptext (if isWanted then sLit "[Wanted] for" 
                                            else sLit "[Local] for"))
                     4 (ppr insts)
338
339

       ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
340
341
342

       ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
                     4 (ppr insts' $$ ppr eqss)
343
344
345
346
347
       ; return $ emptyEqConfig { eqs     = concat eqss
                                , locals  = if isWanted then [] else insts'
                                , wanteds = if isWanted then insts' else []
                                , binds   = unionManyBags bindss
                                }
348
349
350
351
352
353
       }

-- |Solves the equalities as far as possible by applying propagation rules.
--
propagateEqs :: EqConfig -> TcM EqConfig
propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) 
354
355
356
  = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
                     4 (ppr eqCfg)

357
358
       ; propagate todoEqs (eqCfg {eqs = []})
       }
359

360
-- |Finalise a set of equalities and associated dictionaries after
361
362
363
-- propagation.  The first returned set of instances are the locals (without
-- equalities) and the second set are all residual wanteds, including
-- equalities.  In addition, we return all generated dictionary bindings.
364
--
365
366
367
368
369
370
371
finaliseEqsAndDicts :: TcTyVarSet -> EqConfig 
                    -> TcM ([Inst], [Inst], TcDictBinds)
finaliseEqsAndDicts freeFlexibles (EqConfig { eqs     = eqs
                                            , locals  = locals
                                            , wanteds = wanteds
                                            , binds   = binds
                                            })
372
  = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
373
374
375
376

       ; (eqs', subst_binds, locals', wanteds') 
           <- substitute eqs locals wanteds checkingMode freeFlexibles
       ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
377
       ; let final_binds = subst_binds `unionBags` binds
378

379
380
         -- Assert that all cotvs of wanted equalities are still unfilled, and
         -- zonk all final insts, to make any improvement visible
381
       ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
382
383
       ; zonked_locals  <- zonkInsts locals'
       ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
384
       ; return (zonked_locals, zonked_wanteds, final_binds)
385
       }
386
387
388
  where
    checkingMode = length eqs > length wanteds || not (null locals)
                     -- no local equalities or dicts => checking mode
389
390
391
392
393
394
395
396
397
398
399
\end{code}


%************************************************************************
%*									*
		Normalisation of equalities
%*									*
%************************************************************************

A normal equality is a properly oriented equality with associated coercion
that contains at most one family equality (in its left-hand side) is oriented
400
such that it may be used as a rewrite rule.  It has one of the following two 
401
402
403
404
405
406
407
408
409
410
411
412
forms:

(1) co :: F t1..tn ~ t  (family equalities)
(2) co :: x ~ t         (variable equalities)

Variable equalities fall again in two classes:

(2a) co :: x ~ t, where t is *not* a variable, or
(2b) co :: x ~ y, where x > y.

The types t, t1, ..., tn may not contain any occurrences of synonym
families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
413
414
415
416
the right-hand side, and the relation x > y is an (nearly) arbitrary, but
total order on type variables.  The only restriction that we impose on that
order is that for x > y, we are happy to instantiate x with y taking into
account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
417
418
419
420

\begin{code}
data RewriteInst
  = RewriteVar  -- Form (2) above
421
422
423
424
425
426
    { rwi_var     :: TyVar    -- may be rigid or flexible
    , rwi_right   :: TcType   -- contains no synonym family applications
    , rwi_co      :: EqInstCo -- the wanted or given coercion
    , rwi_loc     :: InstLoc
    , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
    , rwi_swapped :: Bool     -- swapped orientation of original EqInst
427
428
    }
  | RewriteFam  -- Forms (1) above
429
430
431
432
433
434
435
    { rwi_fam     :: TyCon    -- synonym family tycon
    , rwi_args    :: [Type]   -- contain no synonym family applications
    , rwi_right   :: TcType   -- contains no synonym family applications
    , rwi_co      :: EqInstCo -- the wanted or given coercion
    , rwi_loc     :: InstLoc
    , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
    , rwi_swapped :: Bool     -- swapped orientation of original EqInst
436
437
438
439
440
    }

isWantedRewriteInst :: RewriteInst -> Bool
isWantedRewriteInst = isWantedCo . rwi_co

441
442
443
444
445
446
447
448
449
450
isRewriteVar :: RewriteInst -> Bool
isRewriteVar (RewriteVar {}) = True
isRewriteVar _               = False

tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
  = unitVarSet tv `unionVarSet` tyVarsOfType ty
tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
  = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty

451
rewriteInstToInst :: RewriteInst -> TcM Inst
452
rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
453
  = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
454
rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
  = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)

-- Derive an EqInst based from a RewriteInst, possibly swapping the types
-- around. 
--
deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
deriveEqInst rewrite ty1 ty2 co
  = do { co_adjusted <- if not swapped then return co 
                                       else mkSymEqInstCo co (ty2, ty1)
       ; return $ EqInst
                  { tci_left  = left
                  , tci_right = right
                  , tci_co    = co_adjusted
                  , tci_loc   = rwi_loc rewrite
                  , tci_name  = rwi_name rewrite
                  }
       }
  where
    swapped       = rwi_swapped rewrite
    (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
475
476
477

instance Outputable RewriteInst where
  ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
478
    = hsep [ pprEqInstCo co <+> text "::" 
479
480
481
482
483
           , ppr (mkTyConApp fam args)
           , text "~>"
           , ppr rhs
           ]
  ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
484
    = hsep [ pprEqInstCo co <+> text "::" 
485
486
487
488
           , ppr tv
           , text "~>"
           , ppr rhs
           ]
489
490
491
492

pprEqInstCo :: EqInstCo -> SDoc
pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
pprEqInstCo (Right co)  = ptext (sLit "Local") <+> ppr co
493
494
495
\end{code}

The following functions turn an arbitrary equality into a set of normal
496
497
498
499
500
501
502
503
504
505
equalities.  This implements the WFlat and LFlat rules of the paper in one
sweep.  However, we use flexible variables for both locals and wanteds, and
avoid to carry around the unflattening substitution \Sigma (for locals) by
already updating the skolems for locals with the family application that they
represent - i.e., they will turn into that family application on the next
zonking (which only happens after finalisation).

In a corresponding manner, normDict normalises class dictionaries by
extracting any synonym family applications and generation appropriate normal
equalities. 
506

507
508
509
510
Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
we drop that equality and raise an error if it is a wanted or a warning if it
is a local.

511
\begin{code}
512
normEqInst :: Inst -> TcM [RewriteInst]
513
-- Normalise one equality.
514
515
normEqInst inst
  = ASSERT( isEqInst inst )
516
517
518
519
    do { traceTc $ ptext (sLit "normEqInst of ") <+> 
                   pprEqInstCo co <+> text "::" <+> 
                   ppr ty1 <+> text "~" <+> ppr ty2
       ; res <- go ty1 ty2 co
520

521
522
523
       ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
       ; return res
       }
524
525
  where
    (ty1, ty2) = eqInstTys inst
526
    co         = eqInstCoercion inst
527
528
529
530
531
532

      -- look through synonyms
    go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
    go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co

      -- left-to-right rule with type family head
533
534
    go ty1@(TyConApp con args) ty2 co 
      | isOpenSynTyConApp ty1           -- only if not oversaturated
535
      = mkRewriteFam False con args ty2 co
536
537
538

      -- right-to-left rule with type family head
    go ty1 ty2@(TyConApp con args) co 
539
      | isOpenSynTyConApp ty2           -- only if not oversaturated
540
      = do { co' <- mkSymEqInstCo co (ty2, ty1)
541
           ; mkRewriteFam True con args ty1 co'
542
543
544
545
           }

      -- no outermost family
    go ty1 ty2 co
546
547
      = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
           ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
548
           ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
549
                 sym_co2   = mkSymCoercion co2
550
                 eqTys     = (ty1', ty2')
551
           ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
552
           ; eqs <- checkOrientation ty1' ty2' co' inst
553
554
555
556
557
558
559
           ; if isLoopyEquality eqs ty12_eqs' 
             then do { if isWantedCo (tci_co inst)
                       then
                          addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
                            eqInstMisMatch inst
                       else
                         warnDroppingLoopyEquality ty1 ty2
560
                     ; return ([])                 -- drop the equality
561
562
                     }
             else
563
               return (eqs ++ ty12_eqs')
564
565
           }

566
    mkRewriteFam swapped con args ty2 co
567
568
      = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
           ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
569
570
           ; let co1       = mkTyConApp con cargs
                 sym_co2   = mkSymCoercion co2
571
572
                 all_eqs   = concat args_eqss ++ ty2_eqs
                 eqTys     = (mkTyConApp con args', ty2')
573
           ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
574
           ; let thisRewriteFam = RewriteFam 
575
576
577
578
579
580
581
                                  { rwi_fam     = con
                                  , rwi_args    = args'
                                  , rwi_right   = ty2'
                                  , rwi_co      = co'
                                  , rwi_loc     = tci_loc inst
                                  , rwi_name    = tci_name inst
                                  , rwi_swapped = swapped
582
                                  }
583
           ; return $ thisRewriteFam : all_eqs'
584
585
           }

586
587
588
589
    -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
    -- have a variable equality with 'a' on the lhs as the first equality.
    -- Then, check whether 'a' occurs in the lhs of any family equality
    -- generated by flattening.
590
    isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
591
592
593
594
595
596
      where
        inRewriteFam (RewriteFam {rwi_args = args}) 
          = tv `elemVarSet` tyVarsOfTypes args
        inRewriteFam _ = False
    isLoopyEquality _ _ = False

597
normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
598
599
-- Normalise one dictionary or IP constraint.
normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
600
  = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
601
602
603
       ; let rewriteCo = PredTy $ ClassP clas cargs
             eqs       = concat args_eqss
             pred'     = ClassP clas args'
604
605
       ; if null eqs
         then  -- don't generate a binding if there is nothing to flatten
606
           return (inst, [], emptyBag)
607
608
609
         else do {
       ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
       ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
610
       ; return (inst', eqs', bind)
611
       }}
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
612
normDict _isWanted inst
613
  = return (inst, [], emptyBag)
614
615
-- !!!TODO: Still need to normalise IP constraints.

616
617
618
619
620
621
checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
-- Performs the occurs check, decomposition, and proper orientation
-- (returns a singleton, or an empty list in case of a trivial equality)
-- NB: We cannot assume that the two types already have outermost type
--     synonyms expanded due to the recursion in the case of type applications.
checkOrientation ty1 ty2 co inst
622
  = go ty1 ty2
623
624
625
626
627
628
629
630
631
632
633
634
  where
      -- look through synonyms
    go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
    go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'

      -- identical types => trivial
    go ty1 ty2
      | ty1 `tcEqType` ty2
      = do { mkIdEqInstCo co ty1
           ; return []
           }

635
      -- two tvs (distinct tvs, due to previous equation)
636
    go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
637
638
639
640
641
642
      = do { isBigger <- tv1 `tvIsBigger` tv2
           ; if isBigger                                      -- left greater
               then mkRewriteVar False tv1 ty2 co             --   => unchanged
               else do { co' <- mkSymEqInstCo co (ty2, ty1)   -- right greater
                       ; mkRewriteVar True tv2 ty1 co'        --   => swap
                       }
643
644
645
646
647
648
649
           }

      -- only lhs is a tv => unchanged
    go ty1@(TyVarTy tv1) ty2
      | ty1 `tcPartOfType` ty2      -- occurs check!
      = occurCheckErr ty1 ty2
      | otherwise 
650
      = mkRewriteVar False tv1 ty2 co
651
652
653
654
655
656
657

      -- only rhs is a tv => swap
    go ty1 ty2@(TyVarTy tv2)
      | ty2 `tcPartOfType` ty1      -- occurs check!
      = occurCheckErr ty2 ty1
      | otherwise 
      = do { co' <- mkSymEqInstCo co (ty2, ty1)
658
           ; mkRewriteVar True tv2 ty1 co'
659
660
           }

661
662
663
664
      -- data type constructor application => decompose
      -- NB: Special cased for efficiency - could be handled as type application
    go (TyConApp con1 args1) (TyConApp con2 args2)
      |  con1 == con2
665
      && isInjectiveTyCon con1   -- don't match family synonym apps
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
      = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
           ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
                     args1 args2 co_args
           ; return $ concat eqss
           }

      -- function type => decompose
      -- NB: Special cased for efficiency - could be handled as type application
    go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
      = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
           ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
           ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
           ; return $ eqs_l ++ eqs_r
           }

681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
      -- type applications => decompose
    go ty1 ty2 
      | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps
      , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
      = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
           ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
           ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
           ; return $ eqs_l ++ eqs_r
           }

      -- inconsistency => type error
    go ty1 ty2
      = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
        eqInstMisMatch inst

696
697
698
699
700
701
702
703
    mkRewriteVar swapped tv ty co = return [RewriteVar 
                                            { rwi_var     = tv
                                            , rwi_right   = ty
                                            , rwi_co      = co
                                            , rwi_loc     = tci_loc inst
                                            , rwi_name    = tci_name inst
                                            , rwi_swapped = swapped
                                            }]
704

705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
    -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
    tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
    tvIsBigger tv1 tv2 
      = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
      where
        isBigger tv1 (SkolemTv _)     tv2 (SkolemTv _)
          = return $ tv1 > tv2
        isBigger _   (MetaTv _ _)     _   (SkolemTv _)
          = return True
        isBigger _   (SkolemTv _)     _   (MetaTv _ _)
          = return False
        isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
          -- meta variable meets meta variable 
          -- => be clever about which of the two to update 
          --   (from TcUnify.uUnfilledVars minus boxy stuff)
          = case (info1, info2) of
              -- Avoid SigTvs if poss
              (SigTv _, SigTv _)             -> return $ tv1 > tv2
              (SigTv _, _      ) | k1_sub_k2 -> return False
              (_,       SigTv _) | k2_sub_k1 -> return True

              (_, _) 
                | k1_sub_k2 &&
                  k2_sub_k1    
                  -> case (nicer_to_update tv1, nicer_to_update tv2) of
                       (True, False) -> return True
                       (False, True) -> return False
                       _             -> return $ tv1 > tv2
                | k1_sub_k2    -> return False
                | k2_sub_k1    -> return True
                | otherwise    -> kind_err >> return True
              -- Update the variable with least kind info
              -- See notes on type inference in Kind.lhs
              -- The "nicer to" part only applies if the two kinds are the same,
              -- so we can choose which to do.
          where
            kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
                       unifyKindMisMatch k1 k2

            k1 = tyVarKind tv1
            k2 = tyVarKind tv2
            k1_sub_k2 = k1 `isSubKind` k2
            k2_sub_k1 = k2 `isSubKind` k1

            nicer_to_update tv = isSystemName (Var.varName tv)
                -- Try to update sys-y type variables in preference to ones
                -- gotten (say) by instantiating a polymorphic function with
                -- a user-written type sig 

754
755
756
757
flattenType :: Inst     -- context to get location  & name
            -> Type     -- the type to flatten
            -> TcM (Type,           -- the flattened type
                    Coercion,       -- coercion witness of flattening wanteds
758
                    [RewriteInst])  -- extra equalities
759
-- Removes all family synonyms from a type by moving them into extra equalities
760
flattenType inst ty = go ty
761
762
  where
      -- look through synonyms
763
    go ty | Just ty' <- tcView ty 
764
      = do { (ty_flat, co, eqs) <- go ty'
765
766
           ; if null eqs
             then     -- unchanged, keep the old type with folded synonyms
767
               return (ty, ty, [])
768
             else 
769
               return (ty_flat, co, eqs)
770
           }
771

772
773
      -- type variable => nothing to do
    go ty@(TyVarTy _)
774
      = return (ty, ty, [])
775

776
      -- type family application & family arity matches number of args
777
      -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
778
    go ty@(TyConApp con args)
779
      | isOpenSynTyConApp ty   -- only if not oversaturated
780
      = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
781
782
783
784
           ; alpha <- newFlexiTyVar (typeKind ty)
           ; let alphaTy = mkTyVarTy alpha
           ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
           ; let thisRewriteFam = RewriteFam 
785
786
787
788
789
790
791
                                  { rwi_fam     = con
                                  , rwi_args    = args'
                                  , rwi_right   = alphaTy
                                  , rwi_co      = mkWantedCo cotv
                                  , rwi_loc     = tci_loc inst
                                  , rwi_name    = tci_name inst
                                  , rwi_swapped = True
792
793
794
                                  }
           ; return (alphaTy,
                     mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
795
796
                     thisRewriteFam : concat args_eqss)
           }
797
798
799

      -- data constructor application => flatten subtypes
      -- NB: Special cased for efficiency - could be handled as type application
800
    go ty@(TyConApp con args)
801
      | not (isOpenSynTyCon con)   -- don't match oversaturated family apps
802
      = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
803
804
           ; if null args_eqss
             then     -- unchanged, keep the old type with folded synonyms
805
               return (ty, ty, [])
806
807
808
             else 
               return (mkTyConApp con args', 
                       mkTyConApp con cargs,
809
                       concat args_eqss)
810
811
812
813
           }

      -- function type => flatten subtypes
      -- NB: Special cased for efficiency - could be handled as type application
814
    go ty@(FunTy ty_l ty_r)
815
816
      = do { (ty_l', co_l, eqs_l) <- go ty_l
           ; (ty_r', co_r, eqs_r) <- go ty_r
817
818
           ; if null eqs_l && null eqs_r
             then     -- unchanged, keep the old type with folded synonyms
819
               return (ty, ty, [])
820
821
822
             else 
               return (mkFunTy ty_l' ty_r', 
                       mkFunTy co_l co_r,
823
                       eqs_l ++ eqs_r)
824
825
826
           }

      -- type application => flatten subtypes
827
828
829
830
    go ty
      | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
                             -- need to use the smart split as ty may be an
                             -- oversaturated family application
831
832
      = do { (ty_l', co_l, eqs_l) <- go ty_l
           ; (ty_r', co_r, eqs_r) <- go ty_r
833
834
           ; if null eqs_l && null eqs_r
             then     -- unchanged, keep the old type with folded synonyms
835
               return (ty, ty, [])
836
837
838
             else 
               return (mkAppTy ty_l' ty_r', 
                       mkAppTy co_l co_r, 
839
                       eqs_l ++ eqs_r)
840
841
           }

842
843
844
845
846
847
      -- forall type => panic if the body contains a type family
      -- !!!TODO: As long as the family does not contain a quantified variable
      --          we might pull it out, but what if it does contain a quantified
      --          variable???
    go ty@(ForAllTy _ body)
      | null (tyFamInsts body)
848
      = return (ty, ty, [])
849
850
851
852
853
854
      | otherwise
      = panic "TcTyFuns.flattenType: synonym family in a rank-n type"

      -- we should never see a predicate type
    go (PredTy _)
      = panic "TcTyFuns.flattenType: unexpected PredType"
855

856
857
    go _ = panic "TcTyFuns: suppress bogus warning"

858
adjustCoercions :: EqInstCo            -- coercion of original equality
859
860
                -> Coercion            -- coercion witnessing the left rewrite
                -> Coercion            -- coercion witnessing the right rewrite
861
                -> (Type, Type)        -- types of flattened equality
862
863
864
865
                -> [RewriteInst]       -- equalities from flattening
                -> TcM (EqInstCo,      -- coercion for flattened equality
                        [RewriteInst]) -- final equalities from flattening
-- Depending on whether we flattened a local or wanted equality, that equality's
866
867
-- coercion and that of the new equalities produced during flattening are
-- adjusted .
868
adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
869
    -- wanted => generate a fresh coercion variable for the flattened equality
870
  = do { cotv' <- newMetaCoVar ty_l ty_r
871
       ; bindMetaTyVar cotv $ 
872
873
           (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
       ; return (Left cotv', all_eqs)
874
       }
875

876
adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
877
878
879
880
881
882
883
884
885
886
887
    -- local => turn all new equalities into locals and update (but not zonk)
    --          the skolem
  = do { all_eqs' <- mapM wantedToLocal all_eqs
       ; return (co, all_eqs')
       }

mkDictBind :: Inst                 -- original instance
           -> Bool                 -- is this a wanted contraint?
           -> Coercion             -- coercion witnessing the rewrite
           -> PredType             -- coerced predicate
           -> TcM (Inst,           -- new inst
888
889
                   TcDictBinds)    -- binding for coerced dictionary
mkDictBind dict isWanted rewriteCo pred
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
  = do { dict' <- newDictBndr loc pred
         -- relate the old inst to the new one
         -- target_dict = source_dict `cast` st_co
       ; let (target_dict, source_dict, st_co) 
               | isWanted  = (dict,  dict', mkSymCoercion rewriteCo)
               | otherwise = (dict', dict,  rewriteCo)
                 -- we have
                 --   co :: dict ~ dict'
                 -- hence, if isWanted
                 -- 	  dict  = dict' `cast` sym co
                 --        else
                 -- 	  dict' = dict  `cast` co
             expr      = HsVar $ instToId source_dict
             cast_expr = HsWrap (WpCast st_co) expr
             rhs       = L (instLocSpan loc) cast_expr
             binds     = instToDictBind target_dict rhs
906
       ; return (dict', binds)
907
       }
908
  where
909
910
    loc = tci_loc dict

911
912
-- gamma ::^l Fam args ~ alpha
-- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
913
914
915
--    (the update of alpha will not be apparent during propagation, as we
--    never follow the indirections of meta variables; it will be revealed
--    when the equality is zonked)
916
917
918
919
--
--  NB: It's crucial to update *both* alpha and gamma, as gamma may already
--      have escaped into some other coercions during normalisation.
--
920
921
922
923
924
925
--      We do actually update alpha and gamma by side effect (instead of
--      only remembering the binding with `bindMetaTyVar', as we do for all
--      other tyvars).  We can do this as the side effects are strictly
--      *local*; we know that both alpha and gamma were just a moment ago
--      introduced by normalisation. 
--
926
927
928
wantedToLocal :: RewriteInst -> TcM RewriteInst
wantedToLocal eq@(RewriteFam {rwi_fam   = fam, 
                              rwi_args  = args, 
929
930
                              rwi_right = TyVarTy alpha,
                              rwi_co    = Left gamma})
931
  = do { writeMetaTyVar alpha (mkTyConApp fam args)
932
933
       ; writeMetaTyVar gamma (mkTyConApp fam args)
       ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
934
935
       }
wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
\end{code}


%************************************************************************
%*									*
		Propagation of equalities
%*									*
%************************************************************************

Apply the propagation rules exhaustively.

\begin{code}
propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
propagate []       eqCfg = return eqCfg
propagate (eq:eqs) eqCfg
  = do { optEqs <- applyTop eq
       ; case optEqs of

              -- Top applied to 'eq' => retry with new equalities
955
           Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
956
957
958

              -- Top doesn't apply => try subst rules with all other
              --   equalities, after that 'eq' can go into the residual list
959
960
961
962
           Nothing   -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
                           ; propagate eqs' (eqCfg' `addEq` eq)
                           }
       }
963
964
965
966
967
968

applySubstRules :: RewriteInst                    -- currently considered eq
                -> [RewriteInst]                  -- todo eqs list
                -> EqConfig                       -- residual
                -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
969
970
  = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
       ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
971
       ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
972
                 eqConfig {eqs = unchangedEqs_r})
973
974
975
976
       }

mapSubstRules :: RewriteInst     -- try substituting this equality
              -> [RewriteInst]   -- into these equalities
977
              -> TcM ([RewriteInst], [RewriteInst])
978
mapSubstRules eq eqs
979
980
  = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
       ; return (concat newEqss, concat unchangedEqss)
981
982
983
       }
  where
    substRules eq1 eq2
984
985
986
987
988
      = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
                        4 (ppr eq1 $$ ppr eq2)

               -- try the SubstFam rule
           ; optEqs <- applySubstFam eq1 eq2
989
           ; case optEqs of
990
991
               Just eqs -> return (eqs, [])
               Nothing  -> do 
992
993
994
           {   -- try the SubstVarVar rule
             optEqs <- applySubstVarVar eq1 eq2
           ; case optEqs of
995
996
               Just eqs -> return (eqs, [])
               Nothing  -> do 
997
998
999
           {   -- try the SubstVarFam rule
             optEqs <- applySubstVarFam eq1 eq2
           ; case optEqs of
1000
1001
               Just eq -> return ([eq], [])
               Nothing -> return ([], [eq2])
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
                 -- if no rule matches, we return the equlity we tried to
                 -- substitute into unchanged
           }}}
\end{code}

Attempt to apply the Top rule.  The rule is

  co :: F t1..tn ~ t
  =(Top)=>
  co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'  

where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.

Returns Nothing if the rule could not be applied.  Otherwise, the resulting
equality is normalised and a list of the normal equalities is returned.

\begin{code}
1019
applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1020
1021
1022
1023
1024
1025
1026

applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
  = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
       ; case optTyCo of
           Nothing                -> return Nothing
           Just (lhs, rewrite_co) 
             -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1027
                   ; eq' <- deriveEqInst eq lhs rhs co'
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
                   ; liftM Just $ normEqInst eq'
                   }
       }
  where
    co  = rwi_co eq
    rhs = rwi_right eq

applyTop _ = return Nothing
\end{code}

Attempt to apply the SubstFam rule.  The rule is

  co1 :: F t1..tn ~ t  &  co2 :: F t1..tn ~ s
  =(SubstFam)=>
  co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'

where co1 may be a wanted only if co2 is a wanted, too.

Returns Nothing if the rule could not be applied.  Otherwise, the equality
co2' is normalised and a list of the normal equalities is returned.  (The
equality co1 is not returned as it remain unaltered.)

\begin{code}
applySubstFam :: RewriteInst 
              -> RewriteInst 
1053
              -> TcM (Maybe ([RewriteInst]))
1054
1055
applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
              eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1056
1057

    -- rule matches => rewrite
1058
1059
1060
  | fam1 == fam2 && tcEqTypes args1 args2 &&
    (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
  = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1061
       ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1062
1063
       ; liftM Just $ normEqInst eq2'
       }
1064
1065
1066
1067

    -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
  | fam1 == fam2 && tcEqTypes args1 args2 &&
    (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1068
  = return $ Just [eq2]
1069

1070
1071
1072
1073
1074
  where
    lhs = rwi_right eq1
    rhs = rwi_right eq2
    co1 = eqInstCoType (rwi_co eq1)
    co2 = rwi_co eq2
1075

1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
applySubstFam _ _ = return Nothing
\end{code}

Attempt to apply the SubstVarVar rule.  The rule is

  co1 :: x ~ t  &  co2 :: x ~ s
  =(SubstVarVar)=>
  co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2'

where co1 may be a wanted only if co2 is a wanted, too.

Returns Nothing if the rule could not be applied.  Otherwise, the equality
co2' is normalised and a list of the normal equalities is returned.  (The
equality co1 is not returned as it remain unaltered.)

\begin{code}
1092
applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1093
1094
applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
                 eq2@(RewriteVar {rwi_var = tv2})
1095
1096

    -- rule matches => rewrite
1097
1098
1099
  | tv1 == tv2 &&
    (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
  = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1100
       ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1101
1102
       ; liftM Just $ normEqInst eq2'
       }
1103
1104
1105
1106

    -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
  | tv1 == tv2 &&
    (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1107
  = return $ Just [eq2]
1108

1109
1110
1111
1112
1113
  where
    lhs = rwi_right eq1
    rhs = rwi_right eq2
    co1 = eqInstCoType (rwi_co eq1)
    co2 = rwi_co eq2
1114

1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
applySubstVarVar _ _ = return Nothing
\end{code}

Attempt to apply the SubstVarFam rule.  The rule is

  co1 :: x ~ t  &  co2 :: F s1..sn ~ s
  =(SubstVarFam)=>
  co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s 
    with co2 = [co1/x](F s1..sn) |> co2'

where x occurs in F s1..sn. (co1 may be local or wanted.)

Returns Nothing if the rule could not be applied.  Otherwise, the equality
co2' is returned.  (The equality co1 is not returned as it remain unaltered.)

\begin{code}
applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1132
1133

  -- rule matches => rewrite
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
                 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
  | tv1 `elemVarSet` tyVarsOfTypes args2
  = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
             args2'   = substTysWith [tv1] [rhs1] args2
             lhs2     = mkTyConApp fam2 args2'
       ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
       ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
       }
  where
    rhs1 = rwi_right eq1
    rhs2 = rwi_right eq2
    co1  = eqInstCoType (rwi_co eq1)
    co2  = rwi_co eq2
1148
1149

  -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
1150
applySubstVarFam (RewriteFam {rwi_args = args1})
1151
1152
1153
1154
                 eq2@(RewriteVar {rwi_var = tv2})
  | tv2 `elemVarSet` tyVarsOfTypes args1
  = return $ Just eq2

1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
applySubstVarFam _ _ = return Nothing
\end{code}


%************************************************************************
%*									*
		Finalisation of equalities
%*									*
%************************************************************************

Exhaustive substitution of all variable equalities of the form co :: x ~ t
1166
1167
1168
1169
1170
(both local and wanted) into the right-hand sides of all other equalities and
of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
other *family* equalities.  This may lead to recursive equalities; i.e., (1)
we need to apply the substitution implied by one equality exhaustively before
turning to the next and (2) we need an occurs check.
1171

1172
We also apply the same substitutions to the local and wanted class and IP
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
dictionaries.  

We perform the substitutions in two steps:

  Step A: Substitute variable equalities into the right-hand sides of all
          other equalities (but wanted only into wanteds) and into class and IP 
          constraints (again wanteds only into wanteds).

  Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
          'alpha' is a skolem flexible (i.e., not free in the environment),
          into the right-hand sides of all wanted variable equalities and into
          both sides of all wanted family equalities.

  Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
          alpha' into the right-hand sides of all wanted variable equalities
          and into both sides of all wanted family equalities.

In inference mode, we do not substitute into variable equalities in Steps B & C.
1191

1192
The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
1193
substitute variable equalities first; e.g., consider
1194
1195
1196

  F s ~ alpha, alpha ~ t

1197
If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1198
This would be bad as `F s' is less useful, eg, as an argument to a class
1199
1200
1201
constraint.  

The restriction on substituting locals is necessary due to examples, such as
1202

1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
  F delta ~ alpha, F alpha ~ delta,

where `alpha' is a skolem flexible and `delta' a environment flexible. We need
to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
we may wrongly claim to having performed an improvement, which can lead to
non-termination of the combined class-family solver.

We do also substitute flexibles, as in `alpha ~ t' into class constraints.
When `alpha' is later instantiated, we'd get the same effect, but in the
meantime the class constraint would miss some information, which would be a
problem in an integrated equality-class solver.
1214
1215
1216
1217
1218
1219

NB: 
* Given that we apply the substitution corresponding to a single equality
  exhaustively, before turning to the next, and because we eliminate recursive
  equalities, all opportunities for subtitution will have been exhausted after
  we have considered each equality once.
1220
1221

\begin{code}
1222
1223
1224
substitute :: [RewriteInst]       -- equalities
           -> [Inst]              -- local class dictionaries
           -> [Inst]              -- wanted class dictionaries
1225
1226
           -> Bool                -- True ~ checking mode; False ~ inference
           -> TyVarSet            -- flexibles free in the environment
1227
1228
1229
1230
           -> TcM ([RewriteInst], -- equalities after substitution
                   TcDictBinds,   -- all newly generated dictionary bindings
                   [Inst],        -- local dictionaries after substitution
                   [Inst])        -- wanted dictionaries after substitution
1231
1232
1233
1234
1235
1236
1237
1238
substitute eqs locals wanteds checkingMode freeFlexibles
  = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
    -- sorting the equalities appropriately: first all variable, then all
    -- family/skolem, and then the remaining family equalities. 
    let (var_eqs, fam_eqs)             = partition isRewriteVar eqs
        (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
    in 
    subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1239
  where
1240
1241
1242
1243
    isFamSkolemEq (RewriteFam {rwi_right = ty})
      | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
    isFamSkolemEq _ = False

1244
1245
    subst [] res binds locals wanteds 
      = return (res, binds, locals, wanteds)
1246

1247
    -- co :: x ~ t
1248
1249
    subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) 
          res binds locals wanteds
1250
1251
      = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+> 
                       ppr eq
1252

1253
             -- create the substitution
1254
           ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1255
                 tySubst = zipOpenTvSubst [tv] [ty]
1256
1257

             -- substitute into all other equalities
1258
1259
1260
           ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
           ; res' <- mapM (substEq eq coSubst tySubst) res

1261
             -- only substitute local equalities into local dictionaries
1262
1263
1264
1265
1266
1267
1268
1269
           ; (lbinds, locals')  <- if not (isWantedCo co)
                                   then 
                                     mapAndUnzipM 
                                       (substDict eq coSubst tySubst False) 
                                       locals
                                   else
                                     return ([], locals)

1270
1271
1272
1273
              -- substitute all equalities into wanteds dictionaries
           ; (wbinds, wanteds') <- mapAndUnzipM 
                                     (substDict eq coSubst tySubst True) 
                                     wanteds
1274

1275
1276
           ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
           ; subst eqs' (eq:res') binds' locals' wanteds'
1277
           }
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300

    -- co ::^w F t1..tn ~ alpha
    subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty, 
                           rwi_co = co}):eqs) 
          res binds locals wanteds
      | Just tv <- tcGetTyVar_maybe ty
      , isMetaTyVar tv
      , isWantedCo co
      = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+> 
                       ppr eq

             -- create the substitution
           ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
                 tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]

             -- substitute into other wanted equalities (`substEq' makes sure
             -- that we only substitute into wanteds)
           ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
           ; res' <- mapM (substEq eq coSubst tySubst) res

           ; subst eqs' (eq:res') binds locals wanteds
           }

1301
1302
1303
1304
1305
    subst (eq:eqs) res binds locals wanteds
      = subst eqs (eq:res) binds locals wanteds

      -- We have, co :: tv ~ ty 
      -- => apply [ty/tv] to right-hand side of eq2
1306
1307
1308
      --    (but only if tv actually occurs in the right-hand side of eq2
      --    and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
    substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) 
1309
            coSubst tySubst eq2
1310
1311
      |  tv `elemVarSet` tyVarsOfType (rwi_right eq2)
      && (isWantedRewriteInst eq2 || not (isWantedCo co))
1312
1313
      = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
                 right2'  = substTy tySubst (rwi_right eq2)
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
                 left2    = case eq2 of
                              RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
                              RewriteFam {rwi_fam = fam,
                                          rwi_args = args} ->mkTyConApp fam args
           ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
           ; case eq2 of
               RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
                 -> occurCheckErr left2 right2'
               _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
           }

1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
      -- We have, co ::^w F t1..tn ~ tv
      -- => apply [F t1..tn/tv] to eq2
      --    (but only if tv actually occurs in eq2
      --    and eq2 is a wanted equality
      --    and we are either in checking mode or eq2 is a family equality)
    substEq (RewriteFam {rwi_args = args, rwi_right = ty}) 
            coSubst tySubst eq2
      | Just tv <- tcGetTyVar_maybe ty
      , tv `elemVarSet` tyVarsOfRewriteInst eq2
      , isWantedRewriteInst eq2
      , checkingMode || not (isRewriteVar eq2)
      = do { -- substitute into the right-hand side
           ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
                 right2'  = substTy tySubst (rwi_right eq2)
                 left2    = case eq2 of
                              RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
                              RewriteFam {rwi_fam = fam,
                                          rwi_args = args} -> mkTyConApp fam args
           ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
           ; case eq2 of
               RewriteVar {rwi_var = tv2} 
                 -- variable equality: perform an occurs check
                 | tv2 `elemVarSet` tyVarsOfTypes args
                 -> occurCheckErr left2 right2'
                 | otherwise
                 -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
               RewriteFam {rwi_fam = fam}
                 -- family equality: substitute also into the left-hand side
                 -> do { let co1Subst = substTy coSubst left2
                             args2'   = substTys tySubst (rwi_args  eq2)
                             left2'   = mkTyConApp fam args2'
                       ; co2'' <- mkRightTransEqInstCo co2' co1Subst 
                                                       (left2', right2')
                       ; return $ eq2 {rwi_args = args2', rwi_right = right2', 
                                       rwi_co = co2''}
                       }
           }

1363
1364
      -- unchanged
    substEq _ _ _ eq2
1365
      = return eq2
1366
1367
1368
1369

      -- We have, co :: tv ~ ty 
      -- => apply [ty/tv] to dictionary predicate
      --    (but only if tv actually occurs in the predicate)
1370
    substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1371
1372
      | isClassDict dict
      , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1373
      = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1374
                 pred'    = substPred tySubst (tci_pred dict)
1375
           ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1376
1377
1378
1379
1380
1381
1382
           ; return (binds, dict')
           }

      -- unchanged
    substDict _ _ _ _ dict
      = return (emptyBag, dict)
-- !!!TODO: Still need to substitute into IP constraints.
1383
1384
1385
\end{code}

For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
alpha, we record a binding of alpha with t or a, respectively, and for co :=
id.  We do the same for equalities of the form co :: F t1..tn ~ alpha unless
we are in inference mode and alpha appears in the environment - i.e., it is
not a flexible introduced by flattening locals or it is local, but was
propagated into the environment by the instantiation of a variable equality.

We proceed in two phases: (1) first we consider all variable equalities and then
(2) we consider all family equalities.  The two phase structure is required as
the recorded variable equalities determine which skolems flexibles escape, and
hence, which family equalities may be recorded as bindings.

We return all wanted equalities for which we did not generate a binding.
(These can be skolem variable equalities, cyclic variable equalities, and
family equalities.)

We don't update any meta variables.  Instead, instantiation simply implies
putting a type variable binding into the binding pool of TcM.

NB:
 * We may encounter filled flexibles due to the instant filling of local
   skolems in local-given constraints during flattening.
 * Be careful with SigTVs.  They can only be instantiated with other SigTVs or
   rigid skolems.
1409

1410
\begin{code}
1411
1412
1413
1414
1415
1416
1417
1418
1419
bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
bindAndExtract eqs checkingMode freeFlexibles
  = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
                     4 (ppr eqs $$ ppr freeFlexibles)
       ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
       ; escapingSkolems <- getEscapingSkolems
       ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
       ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
       ; mapM rewriteInstToInst residuals2
1420
1421
       }
  where
1422
1423
1424
1425
1426
1427
1428
1429
    -- NB: we don't have to transitively chase the relation as the substitution
    --     process applied before generating the bindings was exhaustive
    getEscapingSkolems
      = do { tybinds_rel <- getTcTyVarBindsRelation
           ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
           }
      where
        isFree (tv, _) = tv `elemVarSet` freeFlexibles
1430

1431
        -- co :: alpha ~ t or co :: a ~ alpha
1432
1433
1434
    instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
      = do { flexi_tv1       <- isFlexible   tv1
           ; maybe_flexi_tv2 <- isFlexibleTy ty2
1435
           ; case (flexi_tv1, maybe_flexi_tv2) of
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
               (True, Just tv2)
                 | isSigTyVar tv1 && isSigTyVar tv2
                 -> -- co :: alpha ~ beta, where both a SigTvs
                    doInst (rwi_swapped eq) tv1 ty2 co eq
               (True, Nothing) 
                 | Just tv2 <- tcGetTyVar_maybe ty2
                 , isSigTyVar tv1
                 , isSkolemTyVar tv2
                 -> -- co :: alpha ~ a, where alpha is a SigTv
                    doInst (rwi_swapped eq) tv1 ty2 co eq
1446
               (True, _) 
1447
1448
                 | not (isSigTyVar tv1)
                 -> -- co :: alpha ~ t, where alpha is not a SigTv
1449
1450
                    doInst (rwi_swapped eq) tv1 ty2 co eq
               (False, Just tv2) 
1451
1452
1453
1454
1455
1456
1457
                 | isSigTyVar tv2
                 , isSkolemTyVar tv1
                 -> -- co :: a ~ alpha, where alpha is a SigTv
                    doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
                 | not (isSigTyVar tv2)
                 -> -- co :: a ~ alpha, where alpha is not a SigTv 
                    --                        ('a' may be filled)
1458
                    doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1459
               _ -> return $ Just eq
1460
           }
1461
    instVarEq eq = return $ Just eq
1462

1463
1464
1465
1466
1467
        -- co :: F args ~ alpha, 
        -- and we are either in checking mode or alpha is a skolem flexible that
        --     doesn't escape
    instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args, 
                                               rwi_right = ty2, rwi_co = co})
1468
      | Just tv2 <- tcGetTyVar_maybe ty2
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483