1 Normalisation of type terms relative to type instances as well as
2 normalisation and entailment checking of equality constraints.
6 -- type normalisation wrt to toplevel equalities only
9 -- instance normalisation wrt to equalities
13 misMatchMsg, failWithMisMatch,
18 #include "HsVersions.h"
30 import TypeRep ( Type(..) )
40 import SrcLoc ( Located(..) )
50 %************************************************************************
52 Normalisation of types wrt toplevel equality schemata
54 %************************************************************************
56 Unfold a single synonym family instance and yield the witnessing coercion.
57 Return 'Nothing' if the given type is either not synonym family instance
58 or is a synonym family instance that has no matching instance declaration.
59 (Applies only if the type family application is outermost.)
61 For example, if we have
63 :Co:R42T a :: T [a] ~ :R42T a
65 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
68 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
69 tcUnfoldSynFamInst (TyConApp tycon tys)
70 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
73 = do { -- we only use the indexing arguments for matching,
74 -- not the additional ones
75 ; maybeFamInst <- tcLookupFamInst tycon idxTys
76 ; case maybeFamInst of
77 Nothing -> return Nothing
78 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
79 mkTyConApp coe_tc tys')
81 tys' = rep_tys ++ restTys
82 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
83 (tyConFamilyCoercion_maybe rep_tc)
87 (idxTys, restTys) = splitAt n tys
88 tcUnfoldSynFamInst _other = return Nothing
91 Normalise 'Type's and 'PredType's by unfolding type family applications where
92 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
94 tcNormaliseFamInst ty = (co, ty')
98 -- |Normalise the given type as far as possible with toplevel equalities.
99 -- This results in a coercion witnessing the type equality, in addition to the
102 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
103 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
106 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
107 apply the normalisation function gives as the first argument to every TyConApp
108 and every TyVarTy subterm.
110 tcGenericNormaliseFamInst fun ty = (co, ty')
113 This function is (by way of using smart constructors) careful to ensure that
114 the returned coercion is exactly IdCo (and not some semantically equivalent,
115 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
116 makes it easy for the caller to determine whether the type changed. BUT
117 even if we return IdCo, ty' may be *syntactically* different from ty due to
118 unfolded closed type synonyms (by way of tcCoreView). In the interest of
119 good error messages, callers should discard ty' in favour of ty in this case.
122 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
123 -- what to do with type functions and tyvars
124 -> TcType -- old type
125 -> TcM (CoercionI, TcType) -- (coercion, new type)
126 tcGenericNormaliseFamInst fun ty
127 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
128 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
129 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
130 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
131 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
132 ; case maybe_ty_co of
133 -- a matching family instance exists
135 do { let first_coi = mkTransCoI tycon_coi (ACo co)
136 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
137 ; let fix_coi = mkTransCoI first_coi rest_coi
138 ; return (fix_coi, nty)
140 -- no matching family instance exists
141 -- we do not do anything
142 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
144 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
145 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
146 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
147 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
149 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
150 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
151 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
152 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
154 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
155 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
156 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
158 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
160 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
161 ; res <- lookupTcTyVar tv
164 do { maybe_ty' <- fun ty
166 Nothing -> return (IdCo, ty)
168 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
169 ; return (ACo co1 `mkTransCoI` coi2, ty'')
172 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
176 tcGenericNormaliseFamInst fun (PredTy predty)
177 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
178 ; return (coi, PredTy pred') }
180 ---------------------------------
181 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
183 -> TcM (CoercionI, TcPredType)
185 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
186 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
187 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
189 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
190 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
191 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
193 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
194 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
195 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
196 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
200 %************************************************************************
202 Normalisation of instances wrt to equalities
204 %************************************************************************
207 tcReduceEqs :: [Inst] -- locals
209 -> TcM ([Inst], -- normalised locals (w/o equalities)
210 [Inst], -- normalised wanteds (including equalities)
211 TcDictBinds, -- bindings for all simplified dictionaries
212 Bool) -- whether any flexibles where instantiated
213 tcReduceEqs locals wanteds
214 = do { let (local_eqs , local_dicts) = partition isEqInst locals
215 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
216 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
217 ; eqCfg2 <- normaliseDicts False local_dicts
218 ; eqCfg3 <- normaliseDicts True wanteds_dicts
219 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
220 `unionEqConfig` eqCfg3)
221 ; finaliseEqsAndDicts eqCfg
226 %************************************************************************
228 Equality Configurations
230 %************************************************************************
232 We maintain normalised equalities together with the skolems introduced as
233 intermediates during flattening of equalities as well as
235 !!!TODO: We probably now can do without the skolem set. It's not used during
236 finalisation in the current code.
239 -- |Configuration of normalised equalities used during solving.
241 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
242 , locals :: [Inst] -- given dicts
243 , wanteds :: [Inst] -- wanted dicts
244 , binds :: TcDictBinds -- bindings
245 , skolems :: TyVarSet -- flattening skolems
248 addSkolems :: EqConfig -> TyVarSet -> EqConfig
249 addSkolems eqCfg newSkolems
250 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
252 addEq :: EqConfig -> RewriteInst -> EqConfig
253 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
255 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
256 unionEqConfig eqc1 eqc2 = EqConfig
257 { eqs = eqs eqc1 ++ eqs eqc2
258 , locals = locals eqc1 ++ locals eqc2
259 , wanteds = wanteds eqc1 ++ wanteds eqc2
260 , binds = binds eqc1 `unionBags` binds eqc2
261 , skolems = skolems eqc1 `unionVarSet` skolems eqc2
264 emptyEqConfig :: EqConfig
265 emptyEqConfig = EqConfig
270 , skolems = emptyVarSet
274 The set of operations on an equality configuration. We obtain the initialise
275 configuration by normalisation ('normaliseEqs'), solve the equalities by
276 propagation ('propagateEqs'), and eventually finalise the configuration when
277 no further propoagation is possible.
280 -- |Turn a set of equalities into an equality configuration for solving.
282 -- Precondition: The Insts are zonked.
284 normaliseEqs :: [Inst] -> TcM EqConfig
286 = do { (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
287 ; return $ emptyEqConfig { eqs = concat eqss
288 , skolems = unionVarSets skolemss
292 -- |Flatten the type arguments of all dictionaries, returning the result as a
293 -- equality configuration. The dictionaries go into the 'wanted' component if
294 -- the second argument is 'True'.
296 -- Precondition: The Insts are zonked.
298 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
299 normaliseDicts isWanted insts
300 = do { (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
302 ; return $ emptyEqConfig { eqs = concat eqss
303 , locals = if isWanted then [] else insts'
304 , wanteds = if isWanted then insts' else []
305 , binds = unionManyBags bindss
306 , skolems = unionVarSets skolemss
310 -- |Solves the equalities as far as possible by applying propagation rules.
312 propagateEqs :: EqConfig -> TcM EqConfig
313 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
314 = propagate todoEqs (eqCfg {eqs = []})
316 -- |Finalise a set of equalities and associated dictionaries after
317 -- propagation. The returned Boolean value is `True' iff any flexible
318 -- variables, except those introduced by flattening (i.e., those in the
319 -- `skolems' component of the argument) where instantiated. The first returned
320 -- set of instances are the locals (without equalities) and the second set are
321 -- all residual wanteds, including equalities.
323 -- Remove all identity dictinary bindings (i.e., those whose source and target
324 -- dictionary are the same). This is important for termination, as
325 -- TcSimplify.reduceContext takes the presence of dictionary bindings as an
326 -- indicator that there was some improvement.
328 finaliseEqsAndDicts :: EqConfig
329 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
330 finaliseEqsAndDicts (EqConfig { eqs = eqs
335 = do { (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
336 ; (eqs'', improved) <- instantiateAndExtract eqs'
337 ; final_binds <- filterM nonTrivialDictBind $
338 bagToList (subst_binds `unionBags` binds)
339 ; return (locals', eqs'' ++ wanteds', listToBag final_binds, improved)
342 nonTrivialDictBind (L _ (VarBind { var_id = ide1
343 , var_rhs = L _ (HsWrap _ (HsVar ide2))}))
344 = do { ty1 <- zonkTcType (idType ide1)
345 ; ty2 <- zonkTcType (idType ide2)
346 ; return $ not (ty1 `tcEqType` ty2)
348 nonTrivialDictBind _ = return True
352 %************************************************************************
354 Normalisation of equalities
356 %************************************************************************
358 A normal equality is a properly oriented equality with associated coercion
359 that contains at most one family equality (in its left-hand side) is oriented
360 such that it may be used as a reqrite rule. It has one of the following two
363 (1) co :: F t1..tn ~ t (family equalities)
364 (2) co :: x ~ t (variable equalities)
366 Variable equalities fall again in two classes:
368 (2a) co :: x ~ t, where t is *not* a variable, or
369 (2b) co :: x ~ y, where x > y.
371 The types t, t1, ..., tn may not contain any occurrences of synonym
372 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
373 the right-hand side, and the relation x > y is an arbitrary, but total order
376 !!!TODO: We may need to keep track of swapping for error messages (and to
377 re-orient on finilisation).
381 = RewriteVar -- Form (2) above
382 { rwi_var :: TyVar -- may be rigid or flexible
383 , rwi_right :: TcType -- contains no synonym family applications
384 , rwi_co :: EqInstCo -- the wanted or given coercion
386 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
388 | RewriteFam -- Forms (1) above
389 { rwi_fam :: TyCon -- synonym family tycon
390 , rwi_args :: [Type] -- contain no synonym family applications
391 , rwi_right :: TcType -- contains no synonym family applications
392 , rwi_co :: EqInstCo -- the wanted or given coercion
394 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
397 isWantedRewriteInst :: RewriteInst -> Bool
398 isWantedRewriteInst = isWantedCo . rwi_co
400 rewriteInstToInst :: RewriteInst -> Inst
401 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
403 { tci_left = mkTyVarTy tv
404 , tci_right = rwi_right eq
406 , tci_loc = rwi_loc eq
407 , tci_name = rwi_name eq
409 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
411 { tci_left = mkTyConApp fam args
412 , tci_right = rwi_right eq
414 , tci_loc = rwi_loc eq
415 , tci_name = rwi_name eq
419 The following functions turn an arbitrary equality into a set of normal
420 equalities. This implements the WFlat and LFlat rules of the paper in one
421 sweep. However, we use flexible variables for both locals and wanteds, and
422 avoid to carry around the unflattening substitution \Sigma (for locals) by
423 already updating the skolems for locals with the family application that they
424 represent - i.e., they will turn into that family application on the next
425 zonking (which only happens after finalisation).
427 In a corresponding manner, normDict normalises class dictionaries by
428 extracting any synonym family applications and generation appropriate normal
431 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
432 we drop that equality and raise an error if it is a wanted or a warning if it
436 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
437 -- Normalise one equality.
439 = ASSERT( isEqInst inst )
440 go ty1 ty2 (eqInstCoercion inst)
442 (ty1, ty2) = eqInstTys inst
444 -- look through synonyms
445 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
446 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
448 -- left-to-right rule with type family head
449 go (TyConApp con args) ty2 co
451 = mkRewriteFam con args ty2 co
453 -- right-to-left rule with type family head
454 go ty1 ty2@(TyConApp con args) co
456 = do { co' <- mkSymEqInstCo co (ty2, ty1)
457 ; mkRewriteFam con args ty1 co'
460 -- no outermost family
462 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
463 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
464 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
465 rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2
467 ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs
468 ; eqs <- checkOrientation ty1' ty2' co' inst
469 ; if isLoopyEquality eqs ty12_eqs'
470 then do { if isWantedCo (tci_co inst)
472 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
475 warnDroppingLoopyEquality ty1 ty2
476 ; return ([], emptyVarSet) -- drop the equality
479 return (eqs ++ ty12_eqs',
480 ty1_skolems `unionVarSet` ty2_skolems)
483 mkRewriteFam con args ty2 co
484 = do { (args', cargs, args_eqss, args_skolemss)
485 <- mapAndUnzip4M (flattenType inst) args
486 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
487 ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion`
489 all_eqs = concat args_eqss ++ ty2_eqs
490 eqTys = (mkTyConApp con args', ty2')
491 ; (co', all_eqs') <- adjustCoercions co rewriteCo eqTys all_eqs
492 ; let thisRewriteFam = RewriteFam
497 , rwi_loc = tci_loc inst
498 , rwi_name = tci_name inst
500 ; return $ (thisRewriteFam : all_eqs',
501 unionVarSets (ty2_skolems:args_skolemss))
504 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
505 -- have a variable equality with 'a' on the lhs as the first equality.
506 -- Then, check whether 'a' occurs in the lhs of any family equality
507 -- generated by flattening.
508 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
509 = any inRewriteFam eqs
511 inRewriteFam (RewriteFam {rwi_args = args})
512 = tv `elemVarSet` tyVarsOfTypes args
513 inRewriteFam _ = False
514 isLoopyEquality _ _ = False
516 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
517 -- Normalise one dictionary or IP constraint.
518 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
519 = do { (args', cargs, args_eqss, args_skolemss)
520 <- mapAndUnzip4M (flattenType inst) args
521 ; let rewriteCo = PredTy $ ClassP clas cargs
522 eqs = concat args_eqss
523 pred' = ClassP clas args'
525 then -- don't generate a binding if there is nothing to flatten
526 return (inst, [], emptyBag, emptyVarSet)
528 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
529 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
530 ; return (inst', eqs', bind, unionVarSets args_skolemss)
532 normDict isWanted inst
533 = return (inst, [], emptyBag, emptyVarSet)
534 -- !!!TODO: Still need to normalise IP constraints.
536 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
537 -- Performs the occurs check, decomposition, and proper orientation
538 -- (returns a singleton, or an empty list in case of a trivial equality)
539 -- NB: We cannot assume that the two types already have outermost type
540 -- synonyms expanded due to the recursion in the case of type applications.
541 checkOrientation ty1 ty2 co inst
544 -- look through synonyms
545 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
546 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
548 -- identical types => trivial
551 = do { mkIdEqInstCo co ty1
555 -- two tvs, left greater => unchanged
556 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
558 = mkRewriteVar tv1 ty2 co
560 -- two tvs, right greater => swap
562 = do { co' <- mkSymEqInstCo co (ty2, ty1)
563 ; mkRewriteVar tv2 ty1 co'
566 -- only lhs is a tv => unchanged
567 go ty1@(TyVarTy tv1) ty2
568 | ty1 `tcPartOfType` ty2 -- occurs check!
569 = occurCheckErr ty1 ty2
571 = mkRewriteVar tv1 ty2 co
573 -- only rhs is a tv => swap
574 go ty1 ty2@(TyVarTy tv2)
575 | ty2 `tcPartOfType` ty1 -- occurs check!
576 = occurCheckErr ty2 ty1
578 = do { co' <- mkSymEqInstCo co (ty2, ty1)
579 ; mkRewriteVar tv2 ty1 co'
582 -- type applications => decompose
584 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
585 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
586 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
587 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
588 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
589 ; return $ eqs_l ++ eqs_r
591 -- !!!TODO: would be more efficient to handle the FunApp and the data
592 -- constructor application explicitly.
594 -- inconsistency => type error
596 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
599 mkRewriteVar tv ty co = return [RewriteVar
603 , rwi_loc = tci_loc inst
604 , rwi_name = tci_name inst
607 flattenType :: Inst -- context to get location & name
608 -> Type -- the type to flatten
609 -> TcM (Type, -- the flattened type
610 Coercion, -- coercion witness of flattening wanteds
611 [RewriteInst], -- extra equalities
612 TyVarSet) -- new intermediate skolems
613 -- Removes all family synonyms from a type by moving them into extra equalities
617 -- look through synonyms
618 go ty | Just ty' <- tcView ty = go ty'
620 -- type family application
621 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
622 go ty@(TyConApp con args)
624 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
625 ; alpha <- newFlexiTyVar (typeKind ty)
626 ; let alphaTy = mkTyVarTy alpha
627 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
628 ; let thisRewriteFam = RewriteFam
631 , rwi_right = alphaTy
632 , rwi_co = mkWantedCo cotv
633 , rwi_loc = tci_loc inst
634 , rwi_name = tci_name inst
637 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
638 thisRewriteFam : concat args_eqss,
639 unionVarSets args_skolemss `extendVarSet` alpha)
640 } -- adding new unflatten var inst
642 -- data constructor application => flatten subtypes
643 -- NB: Special cased for efficiency - could be handled as type application
644 go (TyConApp con args)
645 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
646 ; return (mkTyConApp con args',
647 mkTyConApp con cargs,
649 unionVarSets args_skolemss)
652 -- function type => flatten subtypes
653 -- NB: Special cased for efficiency - could be handled as type application
655 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
656 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
657 ; return (mkFunTy ty_l' ty_r',
660 skolems_l `unionVarSet` skolems_r)
663 -- type application => flatten subtypes
665 -- | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
666 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
667 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
668 ; return (mkAppTy ty_l' ty_r',
671 skolems_l `unionVarSet` skolems_r)
674 -- free of type families => leave as is
676 = ASSERT( not . isForAllTy $ ty )
677 return (ty, ty, [] , emptyVarSet)
679 adjustCoercions :: EqInstCo -- coercion of original equality
680 -> Coercion -- coercion witnessing the rewrite
681 -> (Type, Type) -- types of flattened equality
682 -> [RewriteInst] -- equalities from flattening
683 -> TcM (EqInstCo, -- coercion for flattened equality
684 [RewriteInst]) -- final equalities from flattening
685 -- Depending on whether we flattened a local or wanted equality, that equality's
686 -- coercion and that of the new equalities produced during flattening are
688 adjustCoercions co rewriteCo eqTys all_eqs
690 -- wanted => generate a fresh coercion variable for the flattened equality
692 = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys
693 ; return (co', all_eqs)
696 -- local => turn all new equalities into locals and update (but not zonk)
699 = do { all_eqs' <- mapM wantedToLocal all_eqs
700 ; return (co, all_eqs')
703 mkDictBind :: Inst -- original instance
704 -> Bool -- is this a wanted contraint?
705 -> Coercion -- coercion witnessing the rewrite
706 -> PredType -- coerced predicate
707 -> TcM (Inst, -- new inst
708 TcDictBinds) -- binding for coerced dictionary
709 mkDictBind dict isWanted rewriteCo pred
710 = do { dict' <- newDictBndr loc pred
711 -- relate the old inst to the new one
712 -- target_dict = source_dict `cast` st_co
713 ; let (target_dict, source_dict, st_co)
714 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
715 | otherwise = (dict', dict, rewriteCo)
717 -- co :: dict ~ dict'
718 -- hence, if isWanted
719 -- dict = dict' `cast` sym co
721 -- dict' = dict `cast` co
722 expr = HsVar $ instToId source_dict
723 cast_expr = HsWrap (WpCast st_co) expr
724 rhs = L (instLocSpan loc) cast_expr
725 binds = instToDictBind target_dict rhs
726 ; return (dict', binds)
731 -- gamma :: Fam args ~ alpha
732 -- => alpha :: Fam args ~ alpha, with alpha := Fam args
733 -- (the update of alpha will not be apparent during propagation, as we
734 -- never follow the indirections of meta variables; it will be revealed
735 -- when the equality is zonked)
736 wantedToLocal :: RewriteInst -> TcM RewriteInst
737 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
739 rwi_right = alphaTy@(TyVarTy alpha)})
740 = do { writeMetaTyVar alpha (mkTyConApp fam args)
741 ; return $ eq {rwi_co = mkGivenCo alphaTy}
743 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
747 %************************************************************************
749 Propagation of equalities
751 %************************************************************************
753 Apply the propagation rules exhaustively.
756 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
757 propagate [] eqCfg = return eqCfg
758 propagate (eq:eqs) eqCfg
759 = do { optEqs <- applyTop eq
762 -- Top applied to 'eq' => retry with new equalities
763 Just (eqs2, skolems2)
764 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
766 -- Top doesn't apply => try subst rules with all other
767 -- equalities, after that 'eq' can go into the residual list
769 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
770 ; propagate eqs' (eqCfg' `addEq` eq)
774 applySubstRules :: RewriteInst -- currently considered eq
775 -> [RewriteInst] -- todo eqs list
776 -> EqConfig -- residual
777 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
778 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
779 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
780 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
781 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
782 eqConfig {eqs = unchangedEqs_r}
783 `addSkolems` (skolems_t `unionVarSet` skolems_r))
786 mapSubstRules :: RewriteInst -- try substituting this equality
787 -> [RewriteInst] -- into these equalities
788 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
790 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
791 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
795 = do { -- try the SubstFam rule
796 optEqs <- applySubstFam eq1 eq2
798 Just (eqs, skolems) -> return (eqs, [], skolems)
800 { -- try the SubstVarVar rule
801 optEqs <- applySubstVarVar eq1 eq2
803 Just (eqs, skolems) -> return (eqs, [], skolems)
805 { -- try the SubstVarFam rule
806 optEqs <- applySubstVarFam eq1 eq2
808 Just eq -> return ([eq], [], emptyVarSet)
809 Nothing -> return ([], [eq2], emptyVarSet)
810 -- if no rule matches, we return the equlity we tried to
811 -- substitute into unchanged
815 Attempt to apply the Top rule. The rule is
819 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
821 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
823 Returns Nothing if the rule could not be applied. Otherwise, the resulting
824 equality is normalised and a list of the normal equalities is returned.
827 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
829 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
830 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
832 Nothing -> return Nothing
833 Just (lhs, rewrite_co)
834 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
839 , tci_loc = rwi_loc eq
840 , tci_name = rwi_name eq
842 ; liftM Just $ normEqInst eq'
849 applyTop _ = return Nothing
852 Attempt to apply the SubstFam rule. The rule is
854 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
856 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
858 where co1 may be a wanted only if co2 is a wanted, too.
860 Returns Nothing if the rule could not be applied. Otherwise, the equality
861 co2' is normalised and a list of the normal equalities is returned. (The
862 equality co1 is not returned as it remain unaltered.)
865 applySubstFam :: RewriteInst
867 -> TcM (Maybe ([RewriteInst], TyVarSet))
868 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
869 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
870 | fam1 == fam2 && tcEqTypes args1 args2 &&
871 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
872 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
873 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
874 -- !!!Should be ok and we don't want three type equalities.
875 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
880 , tci_loc = rwi_loc eq2
881 , tci_name = rwi_name eq2
883 ; liftM Just $ normEqInst eq2'
888 co1 = eqInstCoType (rwi_co eq1)
890 applySubstFam _ _ = return Nothing
893 Attempt to apply the SubstVarVar rule. The rule is
895 co1 :: x ~ t & co2 :: x ~ s
897 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
899 where co1 may be a wanted only if co2 is a wanted, too.
901 Returns Nothing if the rule could not be applied. Otherwise, the equality
902 co2' is normalised and a list of the normal equalities is returned. (The
903 equality co1 is not returned as it remain unaltered.)
906 applySubstVarVar :: RewriteInst
908 -> TcM (Maybe ([RewriteInst], TyVarSet))
909 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
910 eq2@(RewriteVar {rwi_var = tv2})
912 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
913 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
918 , tci_loc = rwi_loc eq2
919 , tci_name = rwi_name eq2
921 ; liftM Just $ normEqInst eq2'
926 co1 = eqInstCoType (rwi_co eq1)
928 applySubstVarVar _ _ = return Nothing
931 Attempt to apply the SubstVarFam rule. The rule is
933 co1 :: x ~ t & co2 :: F s1..sn ~ s
935 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
936 with co2 = [co1/x](F s1..sn) |> co2'
938 where x occurs in F s1..sn. (co1 may be local or wanted.)
940 Returns Nothing if the rule could not be applied. Otherwise, the equality
941 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
944 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
945 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
946 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
947 | tv1 `elemVarSet` tyVarsOfTypes args2
948 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
949 args2' = substTysWith [tv1] [rhs1] args2
950 lhs2 = mkTyConApp fam2 args2'
951 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
952 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
957 co1 = eqInstCoType (rwi_co eq1)
959 applySubstVarFam _ _ = return Nothing
963 %************************************************************************
965 Finalisation of equalities
967 %************************************************************************
969 Exhaustive substitution of all variable equalities of the form co :: x ~ t
970 (both local and wanted) into the left-hand sides of all other equalities. This
971 may lead to recursive equalities; i.e., (1) we need to apply the substitution
972 implied by one variable equality exhaustively before turning to the next and
973 (2) we need an occurs check.
975 We also apply the same substitutions to the local and wanted class and IP
978 NB: Given that we apply the substitution corresponding to a single equality
979 exhaustively, before turning to the next, and because we eliminate recursive
980 equalities, all opportunities for subtitution will have been exhausted after
981 we have considered each equality once.
984 substitute :: [RewriteInst] -- equalities
985 -> [Inst] -- local class dictionaries
986 -> [Inst] -- wanted class dictionaries
987 -> TcM ([RewriteInst], -- equalities after substitution
988 TcDictBinds, -- all newly generated dictionary bindings
989 [Inst], -- local dictionaries after substitution
990 [Inst]) -- wanted dictionaries after substitution
991 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
993 subst [] res binds locals wanteds
994 = return (res, binds, locals, wanteds)
995 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
996 res binds locals wanteds
997 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+>
998 ptext (sLit "->") <+> ppr ty
999 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1000 tySubst = zipOpenTvSubst [tv] [ty]
1001 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1002 ; res' <- mapM (substEq eq coSubst tySubst) res
1003 ; (lbinds, locals') <- mapAndUnzipM
1004 (substDict eq coSubst tySubst False)
1006 ; (wbinds, wanteds') <- mapAndUnzipM
1007 (substDict eq coSubst tySubst True)
1009 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1010 ; subst eqs' (eq:res') binds' locals' wanteds'
1012 subst (eq:eqs) res binds locals wanteds
1013 = subst eqs (eq:res) binds locals wanteds
1015 -- We have, co :: tv ~ ty
1016 -- => apply [ty/tv] to right-hand side of eq2
1017 -- (but only if tv actually occurs in the right-hand side of eq2)
1018 substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1020 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1021 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1022 right2' = substTy tySubst (rwi_right eq2)
1024 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1025 RewriteFam {rwi_fam = fam,
1026 rwi_args = args} ->mkTyConApp fam args
1027 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1029 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1030 -> occurCheckErr left2 right2'
1031 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1038 -- We have, co :: tv ~ ty
1039 -- => apply [ty/tv] to dictionary predicate
1040 -- (but only if tv actually occurs in the predicate)
1041 substDict (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1042 coSubst tySubst isWanted dict
1044 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1045 = do { let co1Subst = mkSymCoercion $
1046 PredTy (substPred coSubst (tci_pred dict))
1047 pred' = substPred tySubst (tci_pred dict)
1048 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1049 ; return (binds, dict')
1053 substDict _ _ _ _ dict
1054 = return (emptyBag, dict)
1055 -- !!!TODO: Still need to substitute into IP constraints.
1058 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1059 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1060 Return all remaining wanted equalities. The Boolean result component is True
1061 if at least one instantiation of a flexible was performed.
1064 instantiateAndExtract :: [RewriteInst] -> TcM ([Inst], Bool)
1065 instantiateAndExtract eqs
1066 = do { let wanteds = filter (isWantedCo . rwi_co) eqs
1067 ; wanteds' <- mapM inst wanteds
1068 ; let residuals = catMaybes wanteds'
1069 improved = length wanteds /= length residuals
1070 ; return (map rewriteInstToInst residuals, improved)
1073 inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1077 = doInst tv1 ty2 co eq
1080 | Just tv2 <- tcGetTyVar_maybe ty2
1082 = doInst tv2 (mkTyVarTy tv1) co eq
1084 inst eq = return $ Just eq
1086 doInst _ _ (Right ty) _eq = pprPanic "TcTyFuns.doInst: local eq: "
1088 doInst tv ty (Left cotv) eq = do { lookupTV <- lookupTcTyVar tv
1089 ; uMeta False tv lookupTV ty cotv
1092 -- meta variable has been filled already
1093 -- => ignore (must be a skolem that was introduced by flattening locals)
1094 uMeta _swapped _tv (IndirectTv _) _ty _cotv
1097 -- type variable meets type variable
1098 -- => check that tv2 hasn't been updated yet and choose which to update
1099 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1101 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1104 = do { lookupTV2 <- lookupTcTyVar tv2
1107 uMeta swapped tv1 (DoneTv details1) ty cotv
1109 uMetaVar swapped tv1 details1 tv2 details2 cotv
1112 ------ Beyond this point we know that ty2 is not a type variable
1114 -- signature skolem meets non-variable type
1115 -- => cannot update (retain the equality)!
1116 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1119 -- updatable meta variable meets non-variable type
1120 -- => occurs check, monotype check, and kinds match check, then update
1121 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1122 = do { -- occurs + monotype check
1123 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1127 -- normalisation shouldn't leave families in non_tv_ty
1128 panic "TcTyFuns.uMeta: unexpected synonym family"
1130 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1131 ; writeMetaTyVar cotv ty' -- update co var
1136 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1138 -- uMetaVar: unify two type variables
1139 -- meta variable meets skolem
1141 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1142 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1143 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1147 -- meta variable meets meta variable
1148 -- => be clever about which of the two to update
1149 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1150 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1151 = do { case (info1, info2) of
1152 -- Avoid SigTvs if poss
1153 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1154 (_, SigTv _) | k2_sub_k1 -> update_tv1
1156 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1157 then update_tv1 -- Same kinds
1159 | k2_sub_k1 -> update_tv1
1160 | otherwise -> kind_err
1161 -- Update the variable with least kind info
1162 -- See notes on type inference in Kind.lhs
1163 -- The "nicer to" part only applies if the two kinds are the same,
1164 -- so we can choose which to do.
1166 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1170 -- Kinds should be guaranteed ok at this point
1171 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1172 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1174 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1175 unifyKindMisMatch k1 k2
1179 k1_sub_k2 = k1 `isSubKind` k2
1180 k2_sub_k1 = k2 `isSubKind` k1
1182 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1183 -- Try to update sys-y type variables in preference to ones
1184 -- gotten (say) by instantiating a polymorphic function with
1185 -- a user-written type sig
1187 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1191 %************************************************************************
1195 %************************************************************************
1197 The infamous couldn't match expected type soandso against inferred type
1198 somethingdifferent message.
1201 eqInstMisMatch :: Inst -> TcM a
1203 = ASSERT( isEqInst inst )
1204 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1206 (ty_act, ty_exp) = eqInstTys inst
1207 InstLoc _ _ ctxt = instLoc inst
1209 -----------------------
1210 failWithMisMatch :: TcType -> TcType -> TcM a
1211 -- Generate the message when two types fail to match,
1212 -- going to some trouble to make it helpful.
1213 -- The argument order is: actual type, expected type
1214 failWithMisMatch ty_act ty_exp
1215 = do { env0 <- tcInitTidyEnv
1216 ; ty_exp <- zonkTcType ty_exp
1217 ; ty_act <- zonkTcType ty_act
1218 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1221 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1222 misMatchMsg env0 (ty_act, ty_exp)
1223 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1224 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1225 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1227 ptext (sLit "against inferred type") <+> pp_act],
1228 nest 2 (extra_exp $$ extra_act)]
1233 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1235 = let (env1, tidy_ty) = tidyOpenType env ty
1236 (env2, extra) = ppr_extra env1 tidy_ty
1238 (env2, quotes (ppr tidy_ty), extra)
1240 -- (ppr_extra env ty) shows extra info about 'ty'
1241 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1242 ppr_extra env (TyVarTy tv)
1243 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1244 = (env1, pprSkolTvBinding tv1)
1246 (env1, tv1) = tidySkolemTyVar env tv
1248 ppr_extra env _ty = (env, empty) -- Normal case
1251 Warn of loopy local equalities that were dropped.
1254 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1255 warnDroppingLoopyEquality ty1 ty2
1256 = do { env0 <- tcInitTidyEnv
1257 ; ty1 <- zonkTcType ty1
1258 ; ty2 <- zonkTcType ty2
1259 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1260 2 (ppr ty1 <+> text "~" <+> ppr ty2)