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(..) )
39 import SrcLoc ( Located(..) )
49 %************************************************************************
51 Normalisation of types wrt toplevel equality schemata
53 %************************************************************************
55 Unfold a single synonym family instance and yield the witnessing coercion.
56 Return 'Nothing' if the given type is either not synonym family instance
57 or is a synonym family instance that has no matching instance declaration.
58 (Applies only if the type family application is outermost.)
60 For example, if we have
62 :Co:R42T a :: T [a] ~ :R42T a
64 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
67 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
68 tcUnfoldSynFamInst (TyConApp tycon tys)
69 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
72 = do { -- we only use the indexing arguments for matching,
73 -- not the additional ones
74 ; maybeFamInst <- tcLookupFamInst tycon idxTys
75 ; case maybeFamInst of
76 Nothing -> return Nothing
77 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
78 mkTyConApp coe_tc tys')
80 tys' = rep_tys ++ restTys
81 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
82 (tyConFamilyCoercion_maybe rep_tc)
86 (idxTys, restTys) = splitAt n tys
87 tcUnfoldSynFamInst _other = return Nothing
90 Normalise 'Type's and 'PredType's by unfolding type family applications where
91 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
93 tcNormaliseFamInst ty = (co, ty')
97 -- |Normalise the given type as far as possible with toplevel equalities.
98 -- This results in a coercion witnessing the type equality, in addition to the
101 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
102 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
105 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
106 apply the normalisation function gives as the first argument to every TyConApp
107 and every TyVarTy subterm.
109 tcGenericNormaliseFamInst fun ty = (co, ty')
112 This function is (by way of using smart constructors) careful to ensure that
113 the returned coercion is exactly IdCo (and not some semantically equivalent,
114 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
115 makes it easy for the caller to determine whether the type changed. BUT
116 even if we return IdCo, ty' may be *syntactically* different from ty due to
117 unfolded closed type synonyms (by way of tcCoreView). In the interest of
118 good error messages, callers should discard ty' in favour of ty in this case.
121 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
122 -- what to do with type functions and tyvars
123 -> TcType -- old type
124 -> TcM (CoercionI, TcType) -- (coercion, new type)
125 tcGenericNormaliseFamInst fun ty
126 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
127 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
128 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
129 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
130 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
131 ; case maybe_ty_co of
132 -- a matching family instance exists
134 do { let first_coi = mkTransCoI tycon_coi (ACo co)
135 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
136 ; let fix_coi = mkTransCoI first_coi rest_coi
137 ; return (fix_coi, nty)
139 -- no matching family instance exists
140 -- we do not do anything
141 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
143 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
144 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
145 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
146 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
148 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
149 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
150 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
151 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
153 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
154 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
155 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
157 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
159 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
160 ; res <- lookupTcTyVar tv
163 do { maybe_ty' <- fun ty
165 Nothing -> return (IdCo, ty)
167 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
168 ; return (ACo co1 `mkTransCoI` coi2, ty'')
171 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
175 tcGenericNormaliseFamInst fun (PredTy predty)
176 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
177 ; return (coi, PredTy pred') }
179 ---------------------------------
180 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
182 -> TcM (CoercionI, TcPredType)
184 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
185 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
186 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
188 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
189 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
190 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
192 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
193 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
194 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
195 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
199 %************************************************************************
201 Normalisation of instances wrt to equalities
203 %************************************************************************
206 tcReduceEqs :: [Inst] -- locals
208 -> TcM ([Inst], -- normalised locals (w/o equalities)
209 [Inst], -- normalised wanteds (including equalities)
210 TcDictBinds, -- bindings for all simplified dictionaries
211 Bool) -- whether any flexibles where instantiated
212 tcReduceEqs locals wanteds
213 = do { let (local_eqs , local_dicts) = partition isEqInst locals
214 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
215 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
216 ; eqCfg2 <- normaliseDicts False local_dicts
217 ; eqCfg3 <- normaliseDicts True wanteds_dicts
218 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
219 `unionEqConfig` eqCfg3)
220 ; finaliseEqsAndDicts eqCfg
225 %************************************************************************
227 Equality Configurations
229 %************************************************************************
231 We maintain normalised equalities together with the skolems introduced as
232 intermediates during flattening of equalities as well as
234 !!!TODO: We probably now can do without the skolem set. It's not used during
235 finalisation in the current code.
238 -- |Configuration of normalised equalities used during solving.
240 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
241 , locals :: [Inst] -- given dicts
242 , wanteds :: [Inst] -- wanted dicts
243 , binds :: TcDictBinds -- bindings
244 , skolems :: TyVarSet -- flattening skolems
247 addSkolems :: EqConfig -> TyVarSet -> EqConfig
248 addSkolems eqCfg newSkolems
249 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
251 addEq :: EqConfig -> RewriteInst -> EqConfig
252 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
254 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
255 unionEqConfig eqc1 eqc2 = EqConfig
256 { eqs = eqs eqc1 ++ eqs eqc2
257 , locals = locals eqc1 ++ locals eqc2
258 , wanteds = wanteds eqc1 ++ wanteds eqc2
259 , binds = binds eqc1 `unionBags` binds eqc2
260 , skolems = skolems eqc1 `unionVarSet` skolems eqc2
263 emptyEqConfig :: EqConfig
264 emptyEqConfig = EqConfig
269 , skolems = emptyVarSet
272 instance Outputable EqConfig where
273 ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
274 = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
277 The set of operations on an equality configuration. We obtain the initialise
278 configuration by normalisation ('normaliseEqs'), solve the equalities by
279 propagation ('propagateEqs'), and eventually finalise the configuration when
280 no further propoagation is possible.
283 -- |Turn a set of equalities into an equality configuration for solving.
285 -- Precondition: The Insts are zonked.
287 normaliseEqs :: [Inst] -> TcM EqConfig
289 = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
290 ; traceTc $ ptext (sLit "Entering normaliseEqs")
292 ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
293 ; return $ emptyEqConfig { eqs = concat eqss
294 , skolems = unionVarSets skolemss
298 -- |Flatten the type arguments of all dictionaries, returning the result as a
299 -- equality configuration. The dictionaries go into the 'wanted' component if
300 -- the second argument is 'True'.
302 -- Precondition: The Insts are zonked.
304 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
305 normaliseDicts isWanted insts
306 = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
307 ptext (if isWanted then sLit "[Wanted] for"
308 else sLit "[Local] for"))
310 ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
313 ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
314 4 (ppr insts' $$ ppr eqss)
315 ; return $ emptyEqConfig { eqs = concat eqss
316 , locals = if isWanted then [] else insts'
317 , wanteds = if isWanted then insts' else []
318 , binds = unionManyBags bindss
319 , skolems = unionVarSets skolemss
323 -- |Solves the equalities as far as possible by applying propagation rules.
325 propagateEqs :: EqConfig -> TcM EqConfig
326 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
327 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
330 ; propagate todoEqs (eqCfg {eqs = []})
333 -- |Finalise a set of equalities and associated dictionaries after
334 -- propagation. The returned Boolean value is `True' iff any flexible
335 -- variables, except those introduced by flattening (i.e., those in the
336 -- `skolems' component of the argument) where instantiated. The first returned
337 -- set of instances are the locals (without equalities) and the second set are
338 -- all residual wanteds, including equalities.
340 finaliseEqsAndDicts :: EqConfig
341 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
342 finaliseEqsAndDicts (EqConfig { eqs = eqs
348 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
349 ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
350 ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
351 ; let final_binds = subst_binds `unionBags` binds
353 -- Assert that all cotvs of wanted equalities are still unfilled, and
354 -- zonk all final insts, to make any improvement visible
355 ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
356 ; zonked_locals <- zonkInsts locals'
357 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
358 ; return (zonked_locals, zonked_wanteds, final_binds, improved)
363 %************************************************************************
365 Normalisation of equalities
367 %************************************************************************
369 A normal equality is a properly oriented equality with associated coercion
370 that contains at most one family equality (in its left-hand side) is oriented
371 such that it may be used as a reqrite rule. It has one of the following two
374 (1) co :: F t1..tn ~ t (family equalities)
375 (2) co :: x ~ t (variable equalities)
377 Variable equalities fall again in two classes:
379 (2a) co :: x ~ t, where t is *not* a variable, or
380 (2b) co :: x ~ y, where x > y.
382 The types t, t1, ..., tn may not contain any occurrences of synonym
383 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
384 the right-hand side, and the relation x > y is an arbitrary, but total order
387 !!!TODO: We may need to keep track of swapping for error messages (and to
388 re-orient on finilisation).
392 = RewriteVar -- Form (2) above
393 { rwi_var :: TyVar -- may be rigid or flexible
394 , rwi_right :: TcType -- contains no synonym family applications
395 , rwi_co :: EqInstCo -- the wanted or given coercion
397 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
398 , rwi_swapped :: Bool -- swapped orientation of original EqInst
400 | RewriteFam -- Forms (1) above
401 { rwi_fam :: TyCon -- synonym family tycon
402 , rwi_args :: [Type] -- contain no synonym family applications
403 , rwi_right :: TcType -- contains no synonym family applications
404 , rwi_co :: EqInstCo -- the wanted or given coercion
406 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
407 , rwi_swapped :: Bool -- swapped orientation of original EqInst
410 isWantedRewriteInst :: RewriteInst -> Bool
411 isWantedRewriteInst = isWantedCo . rwi_co
413 rewriteInstToInst :: RewriteInst -> TcM Inst
414 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
415 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
416 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
417 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
419 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
422 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
423 deriveEqInst rewrite ty1 ty2 co
424 = do { co_adjusted <- if not swapped then return co
425 else mkSymEqInstCo co (ty2, ty1)
429 , tci_co = co_adjusted
430 , tci_loc = rwi_loc rewrite
431 , tci_name = rwi_name rewrite
435 swapped = rwi_swapped rewrite
436 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
438 instance Outputable RewriteInst where
439 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
440 = hsep [ pprEqInstCo co <+> text "::"
441 , ppr (mkTyConApp fam args)
445 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
446 = hsep [ pprEqInstCo co <+> text "::"
452 pprEqInstCo :: EqInstCo -> SDoc
453 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
454 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
457 The following functions turn an arbitrary equality into a set of normal
458 equalities. This implements the WFlat and LFlat rules of the paper in one
459 sweep. However, we use flexible variables for both locals and wanteds, and
460 avoid to carry around the unflattening substitution \Sigma (for locals) by
461 already updating the skolems for locals with the family application that they
462 represent - i.e., they will turn into that family application on the next
463 zonking (which only happens after finalisation).
465 In a corresponding manner, normDict normalises class dictionaries by
466 extracting any synonym family applications and generation appropriate normal
469 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
470 we drop that equality and raise an error if it is a wanted or a warning if it
474 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
475 -- Normalise one equality.
477 = ASSERT( isEqInst inst )
478 do { traceTc $ ptext (sLit "normEqInst of ") <+>
479 pprEqInstCo co <+> text "::" <+>
480 ppr ty1 <+> text "~" <+> ppr ty2
481 ; res <- go ty1 ty2 co
482 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
486 (ty1, ty2) = eqInstTys inst
487 co = eqInstCoercion inst
489 -- look through synonyms
490 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
491 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
493 -- left-to-right rule with type family head
494 go ty1@(TyConApp con args) ty2 co
495 | isOpenSynTyConApp ty1 -- only if not oversaturated
496 = mkRewriteFam False con args ty2 co
498 -- right-to-left rule with type family head
499 go ty1 ty2@(TyConApp con args) co
500 | isOpenSynTyConApp ty2 -- only if not oversaturated
501 = do { co' <- mkSymEqInstCo co (ty2, ty1)
502 ; mkRewriteFam True con args ty1 co'
505 -- no outermost family
507 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
508 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
509 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
510 sym_co2 = mkSymCoercion co2
512 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
513 ; eqs <- checkOrientation ty1' ty2' co' inst
514 ; if isLoopyEquality eqs ty12_eqs'
515 then do { if isWantedCo (tci_co inst)
517 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
520 warnDroppingLoopyEquality ty1 ty2
521 ; return ([], emptyVarSet) -- drop the equality
524 return (eqs ++ ty12_eqs',
525 ty1_skolems `unionVarSet` ty2_skolems)
528 mkRewriteFam swapped con args ty2 co
529 = do { (args', cargs, args_eqss, args_skolemss)
530 <- mapAndUnzip4M (flattenType inst) args
531 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
532 ; let co1 = mkTyConApp con cargs
533 sym_co2 = mkSymCoercion co2
534 all_eqs = concat args_eqss ++ ty2_eqs
535 eqTys = (mkTyConApp con args', ty2')
536 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
537 ; let thisRewriteFam = RewriteFam
542 , rwi_loc = tci_loc inst
543 , rwi_name = tci_name inst
544 , rwi_swapped = swapped
546 ; return $ (thisRewriteFam : all_eqs',
547 unionVarSets (ty2_skolems:args_skolemss))
550 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
551 -- have a variable equality with 'a' on the lhs as the first equality.
552 -- Then, check whether 'a' occurs in the lhs of any family equality
553 -- generated by flattening.
554 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
555 = any inRewriteFam eqs
557 inRewriteFam (RewriteFam {rwi_args = args})
558 = tv `elemVarSet` tyVarsOfTypes args
559 inRewriteFam _ = False
560 isLoopyEquality _ _ = False
562 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
563 -- Normalise one dictionary or IP constraint.
564 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
565 = do { (args', cargs, args_eqss, args_skolemss)
566 <- mapAndUnzip4M (flattenType inst) args
567 ; let rewriteCo = PredTy $ ClassP clas cargs
568 eqs = concat args_eqss
569 pred' = ClassP clas args'
571 then -- don't generate a binding if there is nothing to flatten
572 return (inst, [], emptyBag, emptyVarSet)
574 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
575 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
576 ; return (inst', eqs', bind, unionVarSets args_skolemss)
578 normDict _isWanted inst
579 = return (inst, [], emptyBag, emptyVarSet)
580 -- !!!TODO: Still need to normalise IP constraints.
582 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
583 -- Performs the occurs check, decomposition, and proper orientation
584 -- (returns a singleton, or an empty list in case of a trivial equality)
585 -- NB: We cannot assume that the two types already have outermost type
586 -- synonyms expanded due to the recursion in the case of type applications.
587 checkOrientation ty1 ty2 co inst
590 -- look through synonyms
591 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
592 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
594 -- identical types => trivial
597 = do { mkIdEqInstCo co ty1
601 -- two tvs, left greater => unchanged
602 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
604 = mkRewriteVar False tv1 ty2 co
606 -- two tvs, right greater => swap
608 = do { co' <- mkSymEqInstCo co (ty2, ty1)
609 ; mkRewriteVar True tv2 ty1 co'
612 -- only lhs is a tv => unchanged
613 go ty1@(TyVarTy tv1) ty2
614 | ty1 `tcPartOfType` ty2 -- occurs check!
615 = occurCheckErr ty1 ty2
617 = mkRewriteVar False tv1 ty2 co
619 -- only rhs is a tv => swap
620 go ty1 ty2@(TyVarTy tv2)
621 | ty2 `tcPartOfType` ty1 -- occurs check!
622 = occurCheckErr ty2 ty1
624 = do { co' <- mkSymEqInstCo co (ty2, ty1)
625 ; mkRewriteVar True tv2 ty1 co'
628 -- type applications => decompose
630 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
631 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
632 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
633 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
634 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
635 ; return $ eqs_l ++ eqs_r
637 -- !!!TODO: would be more efficient to handle the FunApp and the data
638 -- constructor application explicitly.
640 -- inconsistency => type error
642 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
645 mkRewriteVar swapped tv ty co = return [RewriteVar
649 , rwi_loc = tci_loc inst
650 , rwi_name = tci_name inst
651 , rwi_swapped = swapped
654 flattenType :: Inst -- context to get location & name
655 -> Type -- the type to flatten
656 -> TcM (Type, -- the flattened type
657 Coercion, -- coercion witness of flattening wanteds
658 [RewriteInst], -- extra equalities
659 TyVarSet) -- new intermediate skolems
660 -- Removes all family synonyms from a type by moving them into extra equalities
664 -- look through synonyms
665 go ty | Just ty' <- tcView ty
666 = do { (ty_flat, co, eqs, skolems) <- go ty'
668 then -- unchanged, keep the old type with folded synonyms
669 return (ty, ty, [], emptyVarSet)
671 return (ty_flat, co, eqs, skolems)
674 -- type variable => nothing to do
676 = return (ty, ty, [] , emptyVarSet)
678 -- type family application & family arity matches number of args
679 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
680 go ty@(TyConApp con args)
681 | isOpenSynTyConApp ty -- only if not oversaturated
682 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
683 ; alpha <- newFlexiTyVar (typeKind ty)
684 ; let alphaTy = mkTyVarTy alpha
685 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
686 ; let thisRewriteFam = RewriteFam
689 , rwi_right = alphaTy
690 , rwi_co = mkWantedCo cotv
691 , rwi_loc = tci_loc inst
692 , rwi_name = tci_name inst
696 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
697 thisRewriteFam : concat args_eqss,
698 unionVarSets args_skolemss `extendVarSet` alpha)
699 } -- adding new unflatten var inst
701 -- data constructor application => flatten subtypes
702 -- NB: Special cased for efficiency - could be handled as type application
703 go ty@(TyConApp con args)
704 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
705 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
707 then -- unchanged, keep the old type with folded synonyms
708 return (ty, ty, [], emptyVarSet)
710 return (mkTyConApp con args',
711 mkTyConApp con cargs,
713 unionVarSets args_skolemss)
716 -- function type => flatten subtypes
717 -- NB: Special cased for efficiency - could be handled as type application
718 go ty@(FunTy ty_l ty_r)
719 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
720 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
721 ; if null eqs_l && null eqs_r
722 then -- unchanged, keep the old type with folded synonyms
723 return (ty, ty, [], emptyVarSet)
725 return (mkFunTy ty_l' ty_r',
728 skolems_l `unionVarSet` skolems_r)
731 -- type application => flatten subtypes
733 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
734 -- need to use the smart split as ty may be an
735 -- oversaturated family application
736 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
737 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
738 ; if null eqs_l && null eqs_r
739 then -- unchanged, keep the old type with folded synonyms
740 return (ty, ty, [], emptyVarSet)
742 return (mkAppTy ty_l' ty_r',
745 skolems_l `unionVarSet` skolems_r)
748 -- forall type => panic if the body contains a type family
749 -- !!!TODO: As long as the family does not contain a quantified variable
750 -- we might pull it out, but what if it does contain a quantified
752 go ty@(ForAllTy _ body)
753 | null (tyFamInsts body)
754 = return (ty, ty, [] , emptyVarSet)
756 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
758 -- we should never see a predicate type
760 = panic "TcTyFuns.flattenType: unexpected PredType"
762 go _ = panic "TcTyFuns: suppress bogus warning"
764 adjustCoercions :: EqInstCo -- coercion of original equality
765 -> Coercion -- coercion witnessing the left rewrite
766 -> Coercion -- coercion witnessing the right rewrite
767 -> (Type, Type) -- types of flattened equality
768 -> [RewriteInst] -- equalities from flattening
769 -> TcM (EqInstCo, -- coercion for flattened equality
770 [RewriteInst]) -- final equalities from flattening
771 -- Depending on whether we flattened a local or wanted equality, that equality's
772 -- coercion and that of the new equalities produced during flattening are
774 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
775 -- wanted => generate a fresh coercion variable for the flattened equality
776 = do { cotv' <- newMetaCoVar ty_l ty_r
777 ; writeMetaTyVar cotv $
778 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
779 ; return (Left cotv', all_eqs)
782 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
783 -- local => turn all new equalities into locals and update (but not zonk)
785 = do { all_eqs' <- mapM wantedToLocal all_eqs
786 ; return (co, all_eqs')
789 mkDictBind :: Inst -- original instance
790 -> Bool -- is this a wanted contraint?
791 -> Coercion -- coercion witnessing the rewrite
792 -> PredType -- coerced predicate
793 -> TcM (Inst, -- new inst
794 TcDictBinds) -- binding for coerced dictionary
795 mkDictBind dict isWanted rewriteCo pred
796 = do { dict' <- newDictBndr loc pred
797 -- relate the old inst to the new one
798 -- target_dict = source_dict `cast` st_co
799 ; let (target_dict, source_dict, st_co)
800 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
801 | otherwise = (dict', dict, rewriteCo)
803 -- co :: dict ~ dict'
804 -- hence, if isWanted
805 -- dict = dict' `cast` sym co
807 -- dict' = dict `cast` co
808 expr = HsVar $ instToId source_dict
809 cast_expr = HsWrap (WpCast st_co) expr
810 rhs = L (instLocSpan loc) cast_expr
811 binds = instToDictBind target_dict rhs
812 ; return (dict', binds)
817 -- gamma ::^l Fam args ~ alpha
818 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
819 -- (the update of alpha will not be apparent during propagation, as we
820 -- never follow the indirections of meta variables; it will be revealed
821 -- when the equality is zonked)
823 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
824 -- have escaped into some other coercions during normalisation.
826 wantedToLocal :: RewriteInst -> TcM RewriteInst
827 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
829 rwi_right = TyVarTy alpha,
830 rwi_co = Left gamma})
831 = do { writeMetaTyVar alpha (mkTyConApp fam args)
832 ; writeMetaTyVar gamma (mkTyConApp fam args)
833 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
835 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
839 %************************************************************************
841 Propagation of equalities
843 %************************************************************************
845 Apply the propagation rules exhaustively.
848 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
849 propagate [] eqCfg = return eqCfg
850 propagate (eq:eqs) eqCfg
851 = do { optEqs <- applyTop eq
854 -- Top applied to 'eq' => retry with new equalities
855 Just (eqs2, skolems2)
856 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
858 -- Top doesn't apply => try subst rules with all other
859 -- equalities, after that 'eq' can go into the residual list
861 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
862 ; propagate eqs' (eqCfg' `addEq` eq)
866 applySubstRules :: RewriteInst -- currently considered eq
867 -> [RewriteInst] -- todo eqs list
868 -> EqConfig -- residual
869 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
870 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
871 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
872 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
873 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
874 eqConfig {eqs = unchangedEqs_r}
875 `addSkolems` (skolems_t `unionVarSet` skolems_r))
878 mapSubstRules :: RewriteInst -- try substituting this equality
879 -> [RewriteInst] -- into these equalities
880 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
882 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
883 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
887 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
888 4 (ppr eq1 $$ ppr eq2)
890 -- try the SubstFam rule
891 ; optEqs <- applySubstFam eq1 eq2
893 Just (eqs, skolems) -> return (eqs, [], skolems)
895 { -- try the SubstVarVar rule
896 optEqs <- applySubstVarVar eq1 eq2
898 Just (eqs, skolems) -> return (eqs, [], skolems)
900 { -- try the SubstVarFam rule
901 optEqs <- applySubstVarFam eq1 eq2
903 Just eq -> return ([eq], [], emptyVarSet)
904 Nothing -> return ([], [eq2], emptyVarSet)
905 -- if no rule matches, we return the equlity we tried to
906 -- substitute into unchanged
910 Attempt to apply the Top rule. The rule is
914 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
916 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
918 Returns Nothing if the rule could not be applied. Otherwise, the resulting
919 equality is normalised and a list of the normal equalities is returned.
922 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
924 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
925 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
927 Nothing -> return Nothing
928 Just (lhs, rewrite_co)
929 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
930 ; eq' <- deriveEqInst eq lhs rhs co'
931 ; liftM Just $ normEqInst eq'
938 applyTop _ = return Nothing
941 Attempt to apply the SubstFam rule. The rule is
943 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
945 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
947 where co1 may be a wanted only if co2 is a wanted, too.
949 Returns Nothing if the rule could not be applied. Otherwise, the equality
950 co2' is normalised and a list of the normal equalities is returned. (The
951 equality co1 is not returned as it remain unaltered.)
954 applySubstFam :: RewriteInst
956 -> TcM (Maybe ([RewriteInst], TyVarSet))
957 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
958 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
960 -- rule matches => rewrite
961 | fam1 == fam2 && tcEqTypes args1 args2 &&
962 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
963 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
964 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
965 -- !!!Should be ok and we don't want three type equalities.
966 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
967 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
968 ; liftM Just $ normEqInst eq2'
971 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
972 | fam1 == fam2 && tcEqTypes args1 args2 &&
973 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
974 = return $ Just ([eq2], emptyVarSet)
979 co1 = eqInstCoType (rwi_co eq1)
982 applySubstFam _ _ = return Nothing
985 Attempt to apply the SubstVarVar rule. The rule is
987 co1 :: x ~ t & co2 :: x ~ s
989 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
991 where co1 may be a wanted only if co2 is a wanted, too.
993 Returns Nothing if the rule could not be applied. Otherwise, the equality
994 co2' is normalised and a list of the normal equalities is returned. (The
995 equality co1 is not returned as it remain unaltered.)
998 applySubstVarVar :: RewriteInst
1000 -> TcM (Maybe ([RewriteInst], TyVarSet))
1001 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1002 eq2@(RewriteVar {rwi_var = tv2})
1004 -- rule matches => rewrite
1006 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1007 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1008 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1009 ; liftM Just $ normEqInst eq2'
1012 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1014 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1015 = return $ Just ([eq2], emptyVarSet)
1020 co1 = eqInstCoType (rwi_co eq1)
1023 applySubstVarVar _ _ = return Nothing
1026 Attempt to apply the SubstVarFam rule. The rule is
1028 co1 :: x ~ t & co2 :: F s1..sn ~ s
1030 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1031 with co2 = [co1/x](F s1..sn) |> co2'
1033 where x occurs in F s1..sn. (co1 may be local or wanted.)
1035 Returns Nothing if the rule could not be applied. Otherwise, the equality
1036 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1039 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1041 -- rule matches => rewrite
1042 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1043 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1044 | tv1 `elemVarSet` tyVarsOfTypes args2
1045 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1046 args2' = substTysWith [tv1] [rhs1] args2
1047 lhs2 = mkTyConApp fam2 args2'
1048 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1049 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1052 rhs1 = rwi_right eq1
1053 rhs2 = rwi_right eq2
1054 co1 = eqInstCoType (rwi_co eq1)
1057 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1058 applySubstVarFam (RewriteFam {rwi_args = args1})
1059 eq2@(RewriteVar {rwi_var = tv2})
1060 | tv2 `elemVarSet` tyVarsOfTypes args1
1063 applySubstVarFam _ _ = return Nothing
1067 %************************************************************************
1069 Finalisation of equalities
1071 %************************************************************************
1073 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1074 (both local and wanted) into the left-hand sides of all other equalities. This
1075 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1076 implied by one variable equality exhaustively before turning to the next and
1077 (2) we need an occurs check.
1079 We also apply the same substitutions to the local and wanted class and IP
1082 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1083 substitute them into right-hand sides of equalities, to avoid getting two
1084 competing instantiations for a type variables; e.g., consider
1086 F s ~ alpha, alpha ~ t
1088 If we don't substitute `alpha ~ t', we may instantiate t with `F s' instead.
1089 This would be bad as `F s' is less useful, eg, as an argument to a class
1092 However, there is no reason why we would want to *substitute* `alpha ~ t' into a
1093 class constraint. We rather wait until `alpha' is instantiated to `t` and
1094 save the extra dictionary binding that substitution would introduce.
1095 Moreover, we may substitute wanted equalities only into wanted dictionaries.
1098 * Given that we apply the substitution corresponding to a single equality
1099 exhaustively, before turning to the next, and because we eliminate recursive
1100 equalities, all opportunities for subtitution will have been exhausted after
1101 we have considered each equality once.
1104 substitute :: [RewriteInst] -- equalities
1105 -> [Inst] -- local class dictionaries
1106 -> [Inst] -- wanted class dictionaries
1107 -> TcM ([RewriteInst], -- equalities after substitution
1108 TcDictBinds, -- all newly generated dictionary bindings
1109 [Inst], -- local dictionaries after substitution
1110 [Inst]) -- wanted dictionaries after substitution
1111 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1113 subst [] res binds locals wanteds
1114 = return (res, binds, locals, wanteds)
1116 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1117 res binds locals wanteds
1118 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
1120 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1121 tySubst = zipOpenTvSubst [tv] [ty]
1122 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1123 ; res' <- mapM (substEq eq coSubst tySubst) res
1125 -- only susbtitute local equalities into local dictionaries
1126 ; (lbinds, locals') <- if not (isWantedCo co)
1129 (substDict eq coSubst tySubst False)
1134 -- flexible tvs in wanteds will be instantiated anyway, there is
1135 -- no need to substitute them into dictionaries
1136 ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
1139 (substDict eq coSubst tySubst True)
1142 return ([], wanteds)
1144 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1145 ; subst eqs' (eq:res') binds' locals' wanteds'
1147 subst (eq:eqs) res binds locals wanteds
1148 = subst eqs (eq:res) binds locals wanteds
1150 -- We have, co :: tv ~ ty
1151 -- => apply [ty/tv] to right-hand side of eq2
1152 -- (but only if tv actually occurs in the right-hand side of eq2)
1153 substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1155 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1156 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1157 right2' = substTy tySubst (rwi_right eq2)
1159 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1160 RewriteFam {rwi_fam = fam,
1161 rwi_args = args} ->mkTyConApp fam args
1162 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1164 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1165 -> occurCheckErr left2 right2'
1166 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1173 -- We have, co :: tv ~ ty
1174 -- => apply [ty/tv] to dictionary predicate
1175 -- (but only if tv actually occurs in the predicate)
1176 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1178 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1179 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1180 pred' = substPred tySubst (tci_pred dict)
1181 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1182 ; return (binds, dict')
1186 substDict _ _ _ _ dict
1187 = return (emptyBag, dict)
1188 -- !!!TODO: Still need to substitute into IP constraints.
1191 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1192 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1193 Return all remaining wanted equalities. The Boolean result component is True
1194 if at least one instantiation of a flexible that is *not* a skolem from
1195 flattening was performed.
1197 We need to instantiate all flexibles that arose as skolems during flattening
1198 of wanteds before we instantiate any other flexibles. Consider F delta ~
1199 alpha, F alpha ~ delta, where alpha is a skolem and delta a free flexible. We
1200 need to produce F (F delta) ~ delta (and not F (F alpha) ~ alpha). Otherwise,
1201 we may wrongly claim to having performed an improvement, which can lead to
1202 non-termination of the combined class-family solver.
1205 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
1206 instantiateAndExtract eqs localsEmpty skolems
1207 = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
1208 4 (ppr eqs $$ ppr skolems)
1209 -- start by *only* instantiating skolem flexibles from flattening
1210 ; unflat_wanteds <- liftM catMaybes $
1211 mapM (inst (`elemVarSet` skolems)) wanteds
1212 -- only afterwards instantiate free flexibles
1213 ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds
1214 ; let improvement = length residuals < length unflat_wanteds
1215 ; residuals' <- mapM rewriteInstToInst residuals
1216 ; return (residuals', improvement)
1219 wanteds = filter (isWantedCo . rwi_co) eqs
1220 checkingMode = length eqs > length wanteds || not localsEmpty
1221 -- no local equalities or dicts => checking mode
1223 -- co :: alpha ~ t or co :: a ~ alpha
1224 inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1225 = do { flexi_tv1 <- isFlexible mayInst tv1
1226 ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2
1227 ; case (flexi_tv1, maybe_flexi_tv2) of
1229 -> -- co :: alpha ~ t
1230 doInst (rwi_swapped eq) tv1 ty2 co eq
1232 -> -- co :: a ~ alpha
1233 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1234 _ -> return $ Just eq
1237 -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
1238 inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1239 rwi_right = ty2, rwi_co = co})
1240 | Just tv2 <- tcGetTyVar_maybe ty2
1242 , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
1243 -- !!!TODO: this is too liberal, even if tv2 is in
1244 -- skolems we shouldn't instantiate if tvs occurs
1245 -- in other equalities that may propagate it into the
1247 = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1249 inst _mayInst eq = return $ Just eq
1251 -- tv is a meta var and not filled
1252 isFlexible mayInst tv
1253 | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
1254 | otherwise = return False
1256 -- type is a tv that is a meta var and not filled
1257 isFlexibleTy mayInst ty
1258 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst tv
1259 ; if flexi then return $ Just tv
1262 | otherwise = return Nothing
1264 doInst _swapped _tv _ty (Right ty) _eq
1265 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1266 doInst swapped tv ty (Left cotv) eq
1267 = do { lookupTV <- lookupTcTyVar tv
1268 ; uMeta swapped tv lookupTV ty cotv
1271 -- meta variable has been filled already
1272 -- => keep the equality
1273 uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1275 ptext (sLit "flexible") <+> ppr tv <+>
1276 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1277 ptext (sLit "meant to fill with") <+> ppr ty
1281 -- type variable meets type variable
1282 -- => check that tv2 hasn't been updated yet and choose which to update
1283 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1285 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1288 = do { lookupTV2 <- lookupTcTyVar tv2
1291 uMeta swapped tv1 (DoneTv details1) ty cotv
1293 uMetaVar swapped tv1 details1 tv2 details2 cotv
1296 ------ Beyond this point we know that ty2 is not a type variable
1298 -- signature skolem meets non-variable type
1299 -- => cannot update (retain the equality)!
1300 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1303 -- updatable meta variable meets non-variable type
1304 -- => occurs check, monotype check, and kinds match check, then update
1305 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1306 = do { -- occurs + monotype check
1307 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1311 -- there may be a family in non_tv_ty due to an unzonked,
1312 -- but updated skolem for a local equality
1315 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1316 ; writeMetaTyVar cotv ty' -- update co var
1321 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1323 -- uMetaVar: unify two type variables
1324 -- meta variable meets skolem
1326 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1327 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1328 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1332 -- meta variable meets meta variable
1333 -- => be clever about which of the two to update
1334 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1335 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1336 = do { case (info1, info2) of
1337 -- Avoid SigTvs if poss
1338 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1339 (_, SigTv _) | k2_sub_k1 -> update_tv1
1341 (_, _) | k1_sub_k2 -> if k2_sub_k1 &&
1343 then update_tv1 -- Same kinds
1345 | k2_sub_k1 -> update_tv1
1346 | otherwise -> kind_err
1347 -- Update the variable with least kind info
1348 -- See notes on type inference in Kind.lhs
1349 -- The "nicer to" part only applies if the two kinds are the same,
1350 -- so we can choose which to do.
1352 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1356 -- Kinds should be guaranteed ok at this point
1357 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1358 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1360 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1361 unifyKindMisMatch k1 k2
1365 k1_sub_k2 = k1 `isSubKind` k2
1366 k2_sub_k1 = k2 `isSubKind` k1
1368 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1369 -- Try to update sys-y type variables in preference to ones
1370 -- gotten (say) by instantiating a polymorphic function with
1371 -- a user-written type sig
1373 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1377 %************************************************************************
1381 %************************************************************************
1383 The infamous couldn't match expected type soandso against inferred type
1384 somethingdifferent message.
1387 eqInstMisMatch :: Inst -> TcM a
1389 = ASSERT( isEqInst inst )
1390 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1392 (ty_act, ty_exp) = eqInstTys inst
1393 InstLoc _ _ ctxt = instLoc inst
1395 -----------------------
1396 failWithMisMatch :: TcType -> TcType -> TcM a
1397 -- Generate the message when two types fail to match,
1398 -- going to some trouble to make it helpful.
1399 -- The argument order is: actual type, expected type
1400 failWithMisMatch ty_act ty_exp
1401 = do { env0 <- tcInitTidyEnv
1402 ; ty_exp <- zonkTcType ty_exp
1403 ; ty_act <- zonkTcType ty_act
1404 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1407 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1408 misMatchMsg env0 (ty_act, ty_exp)
1409 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1410 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1411 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1413 ptext (sLit "against inferred type") <+> pp_act],
1414 nest 2 (extra_exp $$ extra_act)]
1419 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1421 = let (env1, tidy_ty) = tidyOpenType env ty
1422 (env2, extra) = ppr_extra env1 tidy_ty
1424 (env2, quotes (ppr tidy_ty), extra)
1426 -- (ppr_extra env ty) shows extra info about 'ty'
1427 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1428 ppr_extra env (TyVarTy tv)
1429 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1430 = (env1, pprSkolTvBinding tv1)
1432 (env1, tv1) = tidySkolemTyVar env tv
1434 ppr_extra env _ty = (env, empty) -- Normal case
1437 Warn of loopy local equalities that were dropped.
1440 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1441 warnDroppingLoopyEquality ty1 ty2
1442 = do { env0 <- tcInitTidyEnv
1443 ; ty1 <- zonkTcType ty1
1444 ; ty2 <- zonkTcType ty2
1445 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1446 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1447 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1448 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))