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 $ ptext (sLit "Entering normaliseDicts") <+>
307 ptext (if isWanted then sLit "[Wanted]" else sLit "[Local]")
308 ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
310 ; return $ emptyEqConfig { eqs = concat eqss
311 , locals = if isWanted then [] else insts'
312 , wanteds = if isWanted then insts' else []
313 , binds = unionManyBags bindss
314 , skolems = unionVarSets skolemss
318 -- |Solves the equalities as far as possible by applying propagation rules.
320 propagateEqs :: EqConfig -> TcM EqConfig
321 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
322 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
325 ; propagate todoEqs (eqCfg {eqs = []})
328 -- |Finalise a set of equalities and associated dictionaries after
329 -- propagation. The returned Boolean value is `True' iff any flexible
330 -- variables, except those introduced by flattening (i.e., those in the
331 -- `skolems' component of the argument) where instantiated. The first returned
332 -- set of instances are the locals (without equalities) and the second set are
333 -- all residual wanteds, including equalities.
335 finaliseEqsAndDicts :: EqConfig
336 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
337 finaliseEqsAndDicts (EqConfig { eqs = eqs
343 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
344 ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
345 ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
346 ; let final_binds = subst_binds `unionBags` binds
348 -- Assert that all cotvs of wanted equalities are still unfilled, and
349 -- zonk all final insts, to make any improvement visible
350 ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
351 ; zonked_locals <- zonkInsts locals'
352 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
353 ; return (zonked_locals, zonked_wanteds, final_binds, improved)
358 %************************************************************************
360 Normalisation of equalities
362 %************************************************************************
364 A normal equality is a properly oriented equality with associated coercion
365 that contains at most one family equality (in its left-hand side) is oriented
366 such that it may be used as a reqrite rule. It has one of the following two
369 (1) co :: F t1..tn ~ t (family equalities)
370 (2) co :: x ~ t (variable equalities)
372 Variable equalities fall again in two classes:
374 (2a) co :: x ~ t, where t is *not* a variable, or
375 (2b) co :: x ~ y, where x > y.
377 The types t, t1, ..., tn may not contain any occurrences of synonym
378 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
379 the right-hand side, and the relation x > y is an arbitrary, but total order
382 !!!TODO: We may need to keep track of swapping for error messages (and to
383 re-orient on finilisation).
387 = RewriteVar -- Form (2) above
388 { rwi_var :: TyVar -- may be rigid or flexible
389 , rwi_right :: TcType -- contains no synonym family applications
390 , rwi_co :: EqInstCo -- the wanted or given coercion
392 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
393 , rwi_swapped :: Bool -- swapped orientation of original EqInst
395 | RewriteFam -- Forms (1) above
396 { rwi_fam :: TyCon -- synonym family tycon
397 , rwi_args :: [Type] -- contain no synonym family applications
398 , rwi_right :: TcType -- contains no synonym family applications
399 , rwi_co :: EqInstCo -- the wanted or given coercion
401 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
402 , rwi_swapped :: Bool -- swapped orientation of original EqInst
405 isWantedRewriteInst :: RewriteInst -> Bool
406 isWantedRewriteInst = isWantedCo . rwi_co
408 rewriteInstToInst :: RewriteInst -> TcM Inst
409 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
410 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
411 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
412 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
414 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
417 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
418 deriveEqInst rewrite ty1 ty2 co
419 = do { co_adjusted <- if not swapped then return co
420 else mkSymEqInstCo co (ty2, ty1)
424 , tci_co = co_adjusted
425 , tci_loc = rwi_loc rewrite
426 , tci_name = rwi_name rewrite
430 swapped = rwi_swapped rewrite
431 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
433 instance Outputable RewriteInst where
434 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
435 = hsep [ pprEqInstCo co <+> text "::"
436 , ppr (mkTyConApp fam args)
440 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
441 = hsep [ pprEqInstCo co <+> text "::"
447 pprEqInstCo :: EqInstCo -> SDoc
448 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
449 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
452 The following functions turn an arbitrary equality into a set of normal
453 equalities. This implements the WFlat and LFlat rules of the paper in one
454 sweep. However, we use flexible variables for both locals and wanteds, and
455 avoid to carry around the unflattening substitution \Sigma (for locals) by
456 already updating the skolems for locals with the family application that they
457 represent - i.e., they will turn into that family application on the next
458 zonking (which only happens after finalisation).
460 In a corresponding manner, normDict normalises class dictionaries by
461 extracting any synonym family applications and generation appropriate normal
464 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
465 we drop that equality and raise an error if it is a wanted or a warning if it
469 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
470 -- Normalise one equality.
472 = ASSERT( isEqInst inst )
473 do { traceTc $ ptext (sLit "normEqInst of ") <+>
474 pprEqInstCo co <+> text "::" <+>
475 ppr ty1 <+> text "~" <+> ppr ty2
476 ; res <- go ty1 ty2 co
477 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
481 (ty1, ty2) = eqInstTys inst
482 co = eqInstCoercion inst
484 -- look through synonyms
485 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
486 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
488 -- left-to-right rule with type family head
489 go ty1@(TyConApp con args) ty2 co
490 | isOpenSynTyConApp ty1 -- only if not oversaturated
491 = mkRewriteFam False con args ty2 co
493 -- right-to-left rule with type family head
494 go ty1 ty2@(TyConApp con args) co
495 | isOpenSynTyConApp ty2 -- only if not oversaturated
496 = do { co' <- mkSymEqInstCo co (ty2, ty1)
497 ; mkRewriteFam True con args ty1 co'
500 -- no outermost family
502 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
503 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
504 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
505 sym_co2 = mkSymCoercion co2
507 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
508 ; eqs <- checkOrientation ty1' ty2' co' inst
509 ; if isLoopyEquality eqs ty12_eqs'
510 then do { if isWantedCo (tci_co inst)
512 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
515 warnDroppingLoopyEquality ty1 ty2
516 ; return ([], emptyVarSet) -- drop the equality
519 return (eqs ++ ty12_eqs',
520 ty1_skolems `unionVarSet` ty2_skolems)
523 mkRewriteFam swapped con args ty2 co
524 = do { (args', cargs, args_eqss, args_skolemss)
525 <- mapAndUnzip4M (flattenType inst) args
526 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
527 ; let co1 = mkTyConApp con cargs
528 sym_co2 = mkSymCoercion co2
529 all_eqs = concat args_eqss ++ ty2_eqs
530 eqTys = (mkTyConApp con args', ty2')
531 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
532 ; let thisRewriteFam = RewriteFam
537 , rwi_loc = tci_loc inst
538 , rwi_name = tci_name inst
539 , rwi_swapped = swapped
541 ; return $ (thisRewriteFam : all_eqs',
542 unionVarSets (ty2_skolems:args_skolemss))
545 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
546 -- have a variable equality with 'a' on the lhs as the first equality.
547 -- Then, check whether 'a' occurs in the lhs of any family equality
548 -- generated by flattening.
549 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
550 = any inRewriteFam eqs
552 inRewriteFam (RewriteFam {rwi_args = args})
553 = tv `elemVarSet` tyVarsOfTypes args
554 inRewriteFam _ = False
555 isLoopyEquality _ _ = False
557 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
558 -- Normalise one dictionary or IP constraint.
559 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
560 = do { (args', cargs, args_eqss, args_skolemss)
561 <- mapAndUnzip4M (flattenType inst) args
562 ; let rewriteCo = PredTy $ ClassP clas cargs
563 eqs = concat args_eqss
564 pred' = ClassP clas args'
566 then -- don't generate a binding if there is nothing to flatten
567 return (inst, [], emptyBag, emptyVarSet)
569 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
570 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
571 ; return (inst', eqs', bind, unionVarSets args_skolemss)
573 normDict _isWanted inst
574 = return (inst, [], emptyBag, emptyVarSet)
575 -- !!!TODO: Still need to normalise IP constraints.
577 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
578 -- Performs the occurs check, decomposition, and proper orientation
579 -- (returns a singleton, or an empty list in case of a trivial equality)
580 -- NB: We cannot assume that the two types already have outermost type
581 -- synonyms expanded due to the recursion in the case of type applications.
582 checkOrientation ty1 ty2 co inst
585 -- look through synonyms
586 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
587 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
589 -- identical types => trivial
592 = do { mkIdEqInstCo co ty1
596 -- two tvs, left greater => unchanged
597 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
599 = mkRewriteVar False tv1 ty2 co
601 -- two tvs, right greater => swap
603 = do { co' <- mkSymEqInstCo co (ty2, ty1)
604 ; mkRewriteVar True tv2 ty1 co'
607 -- only lhs is a tv => unchanged
608 go ty1@(TyVarTy tv1) ty2
609 | ty1 `tcPartOfType` ty2 -- occurs check!
610 = occurCheckErr ty1 ty2
612 = mkRewriteVar False tv1 ty2 co
614 -- only rhs is a tv => swap
615 go ty1 ty2@(TyVarTy tv2)
616 | ty2 `tcPartOfType` ty1 -- occurs check!
617 = occurCheckErr ty2 ty1
619 = do { co' <- mkSymEqInstCo co (ty2, ty1)
620 ; mkRewriteVar True tv2 ty1 co'
623 -- type applications => decompose
625 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
626 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
627 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
628 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
629 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
630 ; return $ eqs_l ++ eqs_r
632 -- !!!TODO: would be more efficient to handle the FunApp and the data
633 -- constructor application explicitly.
635 -- inconsistency => type error
637 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
640 mkRewriteVar swapped tv ty co = return [RewriteVar
644 , rwi_loc = tci_loc inst
645 , rwi_name = tci_name inst
646 , rwi_swapped = swapped
649 flattenType :: Inst -- context to get location & name
650 -> Type -- the type to flatten
651 -> TcM (Type, -- the flattened type
652 Coercion, -- coercion witness of flattening wanteds
653 [RewriteInst], -- extra equalities
654 TyVarSet) -- new intermediate skolems
655 -- Removes all family synonyms from a type by moving them into extra equalities
659 -- look through synonyms
660 go ty | Just ty' <- tcView ty
661 = do { (ty_flat, co, eqs, skolems) <- go ty'
663 then -- unchanged, keep the old type with folded synonyms
664 return (ty, ty, [], emptyVarSet)
666 return (ty_flat, co, eqs, skolems)
669 -- type variable => nothing to do
671 = return (ty, ty, [] , emptyVarSet)
673 -- type family application & family arity matches number of args
674 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
675 go ty@(TyConApp con args)
676 | isOpenSynTyConApp ty -- only if not oversaturated
677 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
678 ; alpha <- newFlexiTyVar (typeKind ty)
679 ; let alphaTy = mkTyVarTy alpha
680 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
681 ; let thisRewriteFam = RewriteFam
684 , rwi_right = alphaTy
685 , rwi_co = mkWantedCo cotv
686 , rwi_loc = tci_loc inst
687 , rwi_name = tci_name inst
691 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
692 thisRewriteFam : concat args_eqss,
693 unionVarSets args_skolemss `extendVarSet` alpha)
694 } -- adding new unflatten var inst
696 -- data constructor application => flatten subtypes
697 -- NB: Special cased for efficiency - could be handled as type application
698 go ty@(TyConApp con args)
699 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
700 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
702 then -- unchanged, keep the old type with folded synonyms
703 return (ty, ty, [], emptyVarSet)
705 return (mkTyConApp con args',
706 mkTyConApp con cargs,
708 unionVarSets args_skolemss)
711 -- function type => flatten subtypes
712 -- NB: Special cased for efficiency - could be handled as type application
713 go ty@(FunTy ty_l ty_r)
714 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
715 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
716 ; if null eqs_l && null eqs_r
717 then -- unchanged, keep the old type with folded synonyms
718 return (ty, ty, [], emptyVarSet)
720 return (mkFunTy ty_l' ty_r',
723 skolems_l `unionVarSet` skolems_r)
726 -- type application => flatten subtypes
728 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
729 -- need to use the smart split as ty may be an
730 -- oversaturated family application
731 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
732 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
733 ; if null eqs_l && null eqs_r
734 then -- unchanged, keep the old type with folded synonyms
735 return (ty, ty, [], emptyVarSet)
737 return (mkAppTy ty_l' ty_r',
740 skolems_l `unionVarSet` skolems_r)
743 -- forall type => panic if the body contains a type family
744 -- !!!TODO: As long as the family does not contain a quantified variable
745 -- we might pull it out, but what if it does contain a quantified
747 go ty@(ForAllTy _ body)
748 | null (tyFamInsts body)
749 = return (ty, ty, [] , emptyVarSet)
751 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
753 -- we should never see a predicate type
755 = panic "TcTyFuns.flattenType: unexpected PredType"
757 go _ = panic "TcTyFuns: suppress bogus warning"
759 adjustCoercions :: EqInstCo -- coercion of original equality
760 -> Coercion -- coercion witnessing the left rewrite
761 -> Coercion -- coercion witnessing the right rewrite
762 -> (Type, Type) -- types of flattened equality
763 -> [RewriteInst] -- equalities from flattening
764 -> TcM (EqInstCo, -- coercion for flattened equality
765 [RewriteInst]) -- final equalities from flattening
766 -- Depending on whether we flattened a local or wanted equality, that equality's
767 -- coercion and that of the new equalities produced during flattening are
769 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
770 -- wanted => generate a fresh coercion variable for the flattened equality
771 = do { cotv' <- newMetaCoVar ty_l ty_r
772 ; writeMetaTyVar cotv $
773 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
774 ; return (Left cotv', all_eqs)
777 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
778 -- local => turn all new equalities into locals and update (but not zonk)
780 = do { all_eqs' <- mapM wantedToLocal all_eqs
781 ; return (co, all_eqs')
784 mkDictBind :: Inst -- original instance
785 -> Bool -- is this a wanted contraint?
786 -> Coercion -- coercion witnessing the rewrite
787 -> PredType -- coerced predicate
788 -> TcM (Inst, -- new inst
789 TcDictBinds) -- binding for coerced dictionary
790 mkDictBind dict isWanted rewriteCo pred
791 = do { dict' <- newDictBndr loc pred
792 -- relate the old inst to the new one
793 -- target_dict = source_dict `cast` st_co
794 ; let (target_dict, source_dict, st_co)
795 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
796 | otherwise = (dict', dict, rewriteCo)
798 -- co :: dict ~ dict'
799 -- hence, if isWanted
800 -- dict = dict' `cast` sym co
802 -- dict' = dict `cast` co
803 expr = HsVar $ instToId source_dict
804 cast_expr = HsWrap (WpCast st_co) expr
805 rhs = L (instLocSpan loc) cast_expr
806 binds = instToDictBind target_dict rhs
807 ; return (dict', binds)
812 -- gamma :: Fam args ~ alpha
813 -- => alpha :: Fam args ~ alpha, with alpha := Fam args
814 -- (the update of alpha will not be apparent during propagation, as we
815 -- never follow the indirections of meta variables; it will be revealed
816 -- when the equality is zonked)
817 wantedToLocal :: RewriteInst -> TcM RewriteInst
818 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
820 rwi_right = alphaTy@(TyVarTy alpha)})
821 = do { writeMetaTyVar alpha (mkTyConApp fam args)
822 ; return $ eq {rwi_co = mkGivenCo alphaTy}
824 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
828 %************************************************************************
830 Propagation of equalities
832 %************************************************************************
834 Apply the propagation rules exhaustively.
837 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
838 propagate [] eqCfg = return eqCfg
839 propagate (eq:eqs) eqCfg
840 = do { optEqs <- applyTop eq
843 -- Top applied to 'eq' => retry with new equalities
844 Just (eqs2, skolems2)
845 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
847 -- Top doesn't apply => try subst rules with all other
848 -- equalities, after that 'eq' can go into the residual list
850 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
851 ; propagate eqs' (eqCfg' `addEq` eq)
855 applySubstRules :: RewriteInst -- currently considered eq
856 -> [RewriteInst] -- todo eqs list
857 -> EqConfig -- residual
858 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
859 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
860 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
861 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
862 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
863 eqConfig {eqs = unchangedEqs_r}
864 `addSkolems` (skolems_t `unionVarSet` skolems_r))
867 mapSubstRules :: RewriteInst -- try substituting this equality
868 -> [RewriteInst] -- into these equalities
869 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
871 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
872 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
876 = do { -- try the SubstFam rule
877 optEqs <- applySubstFam eq1 eq2
879 Just (eqs, skolems) -> return (eqs, [], skolems)
881 { -- try the SubstVarVar rule
882 optEqs <- applySubstVarVar eq1 eq2
884 Just (eqs, skolems) -> return (eqs, [], skolems)
886 { -- try the SubstVarFam rule
887 optEqs <- applySubstVarFam eq1 eq2
889 Just eq -> return ([eq], [], emptyVarSet)
890 Nothing -> return ([], [eq2], emptyVarSet)
891 -- if no rule matches, we return the equlity we tried to
892 -- substitute into unchanged
896 Attempt to apply the Top rule. The rule is
900 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
902 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
904 Returns Nothing if the rule could not be applied. Otherwise, the resulting
905 equality is normalised and a list of the normal equalities is returned.
908 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
910 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
911 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
913 Nothing -> return Nothing
914 Just (lhs, rewrite_co)
915 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
916 ; eq' <- deriveEqInst eq lhs rhs co'
917 ; liftM Just $ normEqInst eq'
924 applyTop _ = return Nothing
927 Attempt to apply the SubstFam rule. The rule is
929 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
931 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
933 where co1 may be a wanted only if co2 is a wanted, too.
935 Returns Nothing if the rule could not be applied. Otherwise, the equality
936 co2' is normalised and a list of the normal equalities is returned. (The
937 equality co1 is not returned as it remain unaltered.)
940 applySubstFam :: RewriteInst
942 -> TcM (Maybe ([RewriteInst], TyVarSet))
943 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
944 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
945 | fam1 == fam2 && tcEqTypes args1 args2 &&
946 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
947 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
948 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
949 -- !!!Should be ok and we don't want three type equalities.
950 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
951 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
952 ; liftM Just $ normEqInst eq2'
957 co1 = eqInstCoType (rwi_co eq1)
959 applySubstFam _ _ = return Nothing
962 Attempt to apply the SubstVarVar rule. The rule is
964 co1 :: x ~ t & co2 :: x ~ s
966 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
968 where co1 may be a wanted only if co2 is a wanted, too.
970 Returns Nothing if the rule could not be applied. Otherwise, the equality
971 co2' is normalised and a list of the normal equalities is returned. (The
972 equality co1 is not returned as it remain unaltered.)
975 applySubstVarVar :: RewriteInst
977 -> TcM (Maybe ([RewriteInst], TyVarSet))
978 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
979 eq2@(RewriteVar {rwi_var = tv2})
981 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
982 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
983 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
984 ; liftM Just $ normEqInst eq2'
989 co1 = eqInstCoType (rwi_co eq1)
991 applySubstVarVar _ _ = return Nothing
994 Attempt to apply the SubstVarFam rule. The rule is
996 co1 :: x ~ t & co2 :: F s1..sn ~ s
998 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
999 with co2 = [co1/x](F s1..sn) |> co2'
1001 where x occurs in F s1..sn. (co1 may be local or wanted.)
1003 Returns Nothing if the rule could not be applied. Otherwise, the equality
1004 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1007 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1008 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1009 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1010 | tv1 `elemVarSet` tyVarsOfTypes args2
1011 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1012 args2' = substTysWith [tv1] [rhs1] args2
1013 lhs2 = mkTyConApp fam2 args2'
1014 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1015 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1018 rhs1 = rwi_right eq1
1019 rhs2 = rwi_right eq2
1020 co1 = eqInstCoType (rwi_co eq1)
1022 applySubstVarFam _ _ = return Nothing
1026 %************************************************************************
1028 Finalisation of equalities
1030 %************************************************************************
1032 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1033 (both local and wanted) into the left-hand sides of all other equalities. This
1034 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1035 implied by one variable equality exhaustively before turning to the next and
1036 (2) we need an occurs check.
1038 We also apply the same substitutions to the local and wanted class and IP
1041 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1042 substitute them into right-hand sides of equalities, to avoid getting two
1043 competing instantiations for a type variables; e.g., consider
1045 F s ~ alpha, alpha ~ t
1047 If we don't substitute `alpha ~ t', we may instantiate t with `F s' instead.
1048 This would be bad as `F s' is less useful, eg, as an argument to a class
1051 However, there is no reason why we would want to *substitute* `alpha ~ t' into a
1052 class constraint. We rather wait until `alpha' is instantiated to `t` and
1053 save the extra dictionary binding that substitution would introduce.
1054 Moreover, we may substitute wanted equalities only into wanted dictionaries.
1057 * Given that we apply the substitution corresponding to a single equality
1058 exhaustively, before turning to the next, and because we eliminate recursive
1059 equalities, all opportunities for subtitution will have been exhausted after
1060 we have considered each equality once.
1063 substitute :: [RewriteInst] -- equalities
1064 -> [Inst] -- local class dictionaries
1065 -> [Inst] -- wanted class dictionaries
1066 -> TcM ([RewriteInst], -- equalities after substitution
1067 TcDictBinds, -- all newly generated dictionary bindings
1068 [Inst], -- local dictionaries after substitution
1069 [Inst]) -- wanted dictionaries after substitution
1070 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1072 subst [] res binds locals wanteds
1073 = return (res, binds, locals, wanteds)
1075 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1076 res binds locals wanteds
1077 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
1079 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1080 tySubst = zipOpenTvSubst [tv] [ty]
1081 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1082 ; res' <- mapM (substEq eq coSubst tySubst) res
1084 -- only susbtitute local equalities into local dictionaries
1085 ; (lbinds, locals') <- if not (isWantedCo co)
1088 (substDict eq coSubst tySubst False)
1093 -- flexible tvs in wanteds will be instantiated anyway, there is
1094 -- no need to substitute them into dictionaries
1095 ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
1098 (substDict eq coSubst tySubst True)
1101 return ([], wanteds)
1103 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1104 ; subst eqs' (eq:res') binds' locals' wanteds'
1106 subst (eq:eqs) res binds locals wanteds
1107 = subst eqs (eq:res) binds locals wanteds
1109 -- We have, co :: tv ~ ty
1110 -- => apply [ty/tv] to right-hand side of eq2
1111 -- (but only if tv actually occurs in the right-hand side of eq2)
1112 substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1114 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1115 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1116 right2' = substTy tySubst (rwi_right eq2)
1118 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1119 RewriteFam {rwi_fam = fam,
1120 rwi_args = args} ->mkTyConApp fam args
1121 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1123 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1124 -> occurCheckErr left2 right2'
1125 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1132 -- We have, co :: tv ~ ty
1133 -- => apply [ty/tv] to dictionary predicate
1134 -- (but only if tv actually occurs in the predicate)
1135 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1137 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1138 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1139 pred' = substPred tySubst (tci_pred dict)
1140 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1141 ; return (binds, dict')
1145 substDict _ _ _ _ dict
1146 = return (emptyBag, dict)
1147 -- !!!TODO: Still need to substitute into IP constraints.
1150 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1151 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1152 Return all remaining wanted equalities. The Boolean result component is True
1153 if at least one instantiation of a flexible that is *not* a skolem from
1154 flattening was performed.
1157 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
1158 instantiateAndExtract eqs localsEmpty skolems
1159 = do { results <- mapM inst wanteds
1160 ; let residuals = [eq | Left eq <- results]
1161 only_skolems = and [tv `elemVarSet` skolems | Right tv <- results]
1162 ; residuals' <- mapM rewriteInstToInst residuals
1163 ; return (residuals', not only_skolems)
1166 wanteds = filter (isWantedCo . rwi_co) eqs
1167 checkingMode = length eqs > length wanteds || not localsEmpty
1168 -- no local equalities or dicts => checking mode
1170 inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1174 = doInst (rwi_swapped eq) tv1 ty2 co eq
1177 | Just tv2 <- tcGetTyVar_maybe ty2
1179 = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1181 -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
1182 inst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty2,
1184 | Just tv2 <- tcGetTyVar_maybe ty2
1186 , checkingMode || tv2 `elemVarSet` skolems
1187 -- !!!TODO: this is too liberal, even if tv2 is in
1188 -- skolems we shouldn't instantiate if tvs occurs
1189 -- in other equalities that may propagate it into the
1191 = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1193 inst eq = return $ Left eq
1195 doInst _swapped _tv _ty (Right ty) _eq
1196 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1197 doInst swapped tv ty (Left cotv) eq
1198 = do { lookupTV <- lookupTcTyVar tv
1199 ; uMeta swapped tv lookupTV ty cotv
1202 -- meta variable has been filled already
1203 -- => keep the equality
1204 uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1206 ptext (sLit "flexible") <+> ppr tv <+>
1207 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1208 ptext (sLit "meant to fill with") <+> ppr ty
1212 -- type variable meets type variable
1213 -- => check that tv2 hasn't been updated yet and choose which to update
1214 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1216 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1219 = do { lookupTV2 <- lookupTcTyVar tv2
1222 uMeta swapped tv1 (DoneTv details1) ty cotv
1224 uMetaVar swapped tv1 details1 tv2 details2 cotv
1227 ------ Beyond this point we know that ty2 is not a type variable
1229 -- signature skolem meets non-variable type
1230 -- => cannot update (retain the equality)!
1231 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1234 -- updatable meta variable meets non-variable type
1235 -- => occurs check, monotype check, and kinds match check, then update
1236 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1237 = do { -- occurs + monotype check
1238 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1242 -- normalisation shouldn't leave families in non_tv_ty
1243 panic "TcTyFuns.uMeta: unexpected synonym family"
1245 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1246 ; writeMetaTyVar cotv ty' -- update co var
1251 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1253 -- uMetaVar: unify two type variables
1254 -- meta variable meets skolem
1256 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1257 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1258 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1259 ; return $ Right tv1
1262 -- meta variable meets meta variable
1263 -- => be clever about which of the two to update
1264 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1265 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1266 = do { tv <- case (info1, info2) of
1267 -- Avoid SigTvs if poss
1268 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1269 (_, SigTv _) | k2_sub_k1 -> update_tv1
1271 (_, _) | k1_sub_k2 -> if k2_sub_k1 &&
1273 then update_tv1 -- Same kinds
1275 | k2_sub_k1 -> update_tv1
1276 | otherwise -> kind_err >> return tv1
1277 -- Update the variable with least kind info
1278 -- See notes on type inference in Kind.lhs
1279 -- The "nicer to" part only applies if the two kinds are the same,
1280 -- so we can choose which to do.
1282 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1286 -- Kinds should be guaranteed ok at this point
1287 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1289 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1292 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1293 unifyKindMisMatch k1 k2
1297 k1_sub_k2 = k1 `isSubKind` k2
1298 k2_sub_k1 = k2 `isSubKind` k1
1300 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1301 -- Try to update sys-y type variables in preference to ones
1302 -- gotten (say) by instantiating a polymorphic function with
1303 -- a user-written type sig
1305 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1309 %************************************************************************
1313 %************************************************************************
1315 The infamous couldn't match expected type soandso against inferred type
1316 somethingdifferent message.
1319 eqInstMisMatch :: Inst -> TcM a
1321 = ASSERT( isEqInst inst )
1322 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1324 (ty_act, ty_exp) = eqInstTys inst
1325 InstLoc _ _ ctxt = instLoc inst
1327 -----------------------
1328 failWithMisMatch :: TcType -> TcType -> TcM a
1329 -- Generate the message when two types fail to match,
1330 -- going to some trouble to make it helpful.
1331 -- The argument order is: actual type, expected type
1332 failWithMisMatch ty_act ty_exp
1333 = do { env0 <- tcInitTidyEnv
1334 ; ty_exp <- zonkTcType ty_exp
1335 ; ty_act <- zonkTcType ty_act
1336 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1339 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1340 misMatchMsg env0 (ty_act, ty_exp)
1341 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1342 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1343 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1345 ptext (sLit "against inferred type") <+> pp_act],
1346 nest 2 (extra_exp $$ extra_act)]
1351 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1353 = let (env1, tidy_ty) = tidyOpenType env ty
1354 (env2, extra) = ppr_extra env1 tidy_ty
1356 (env2, quotes (ppr tidy_ty), extra)
1358 -- (ppr_extra env ty) shows extra info about 'ty'
1359 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1360 ppr_extra env (TyVarTy tv)
1361 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1362 = (env1, pprSkolTvBinding tv1)
1364 (env1, tv1) = tidySkolemTyVar env tv
1366 ppr_extra env _ty = (env, empty) -- Normal case
1369 Warn of loopy local equalities that were dropped.
1372 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1373 warnDroppingLoopyEquality ty1 ty2
1374 = do { env0 <- tcInitTidyEnv
1375 ; ty1 <- zonkTcType ty1
1376 ; ty2 <- zonkTcType ty2
1377 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1378 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1379 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1380 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))