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(..) )
40 import Util ( debugIsOn )
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 { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
74 ; maybeFamInst <- tcLookupFamInst tycon tys
75 ; case maybeFamInst of
76 Nothing -> return Nothing
77 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
78 mkTyConApp coe_tc rep_tys)
80 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
81 (tyConFamilyCoercion_maybe rep_tc)
83 tcUnfoldSynFamInst _other = return Nothing
86 Normalise 'Type's and 'PredType's by unfolding type family applications where
87 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
89 tcNormaliseFamInst ty = (co, ty')
93 -- |Normalise the given type as far as possible with toplevel equalities.
94 -- This results in a coercion witnessing the type equality, in addition to the
97 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
98 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
101 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
102 apply the normalisation function gives as the first argument to every TyConApp
103 and every TyVarTy subterm.
105 tcGenericNormaliseFamInst fun ty = (co, ty')
108 This function is (by way of using smart constructors) careful to ensure that
109 the returned coercion is exactly IdCo (and not some semantically equivalent,
110 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
111 makes it easy for the caller to determine whether the type changed. BUT
112 even if we return IdCo, ty' may be *syntactically* different from ty due to
113 unfolded closed type synonyms (by way of tcCoreView). In the interest of
114 good error messages, callers should discard ty' in favour of ty in this case.
117 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
118 -- what to do with type functions and tyvars
119 -> TcType -- old type
120 -> TcM (CoercionI, TcType) -- (coercion, new type)
121 tcGenericNormaliseFamInst fun ty
122 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
123 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
124 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
125 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
126 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
127 ; case maybe_ty_co of
128 -- a matching family instance exists
130 do { let first_coi = mkTransCoI tycon_coi (ACo co)
131 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
132 ; let fix_coi = mkTransCoI first_coi rest_coi
133 ; return (fix_coi, nty)
135 -- no matching family instance exists
136 -- we do not do anything
137 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
139 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
140 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
141 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
142 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
144 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
145 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
146 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
147 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
149 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
150 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
151 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
153 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
155 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
156 ; res <- lookupTcTyVar tv
159 do { maybe_ty' <- fun ty
161 Nothing -> return (IdCo, ty)
163 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
164 ; return (ACo co1 `mkTransCoI` coi2, ty'')
167 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
171 tcGenericNormaliseFamInst fun (PredTy predty)
172 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
173 ; return (coi, PredTy pred') }
175 ---------------------------------
176 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
178 -> TcM (CoercionI, TcPredType)
180 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
181 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
182 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
184 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
185 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
186 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
188 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
189 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
190 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
191 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
195 %************************************************************************
197 Normalisation of instances wrt to equalities
199 %************************************************************************
202 tcReduceEqs :: [Inst] -- locals
204 -> TcM ([Inst], -- normalised locals (w/o equalities)
205 [Inst], -- normalised wanteds (including equalities)
206 TcDictBinds, -- bindings for all simplified dictionaries
207 Bool) -- whether any flexibles where instantiated
208 tcReduceEqs locals wanteds
209 = do { let (local_eqs , local_dicts) = partition isEqInst locals
210 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
211 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
212 ; eqCfg2 <- normaliseDicts False local_dicts
213 ; eqCfg3 <- normaliseDicts True wanteds_dicts
214 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
215 `unionEqConfig` eqCfg3)
216 ; finaliseEqsAndDicts eqCfg
221 %************************************************************************
223 Equality Configurations
225 %************************************************************************
227 We maintain normalised equalities together with the skolems introduced as
228 intermediates during flattening of equalities as well as
231 -- |Configuration of normalised equalities used during solving.
233 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
234 , locals :: [Inst] -- given dicts
235 , wanteds :: [Inst] -- wanted dicts
236 , binds :: TcDictBinds -- bindings
237 , skolems :: TyVarSet -- flattening skolems
240 addSkolems :: EqConfig -> TyVarSet -> EqConfig
241 addSkolems eqCfg newSkolems
242 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
244 addEq :: EqConfig -> RewriteInst -> EqConfig
245 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
247 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
248 unionEqConfig eqc1 eqc2 = EqConfig
249 { eqs = eqs eqc1 ++ eqs eqc2
250 , locals = locals eqc1 ++ locals eqc2
251 , wanteds = wanteds eqc1 ++ wanteds eqc2
252 , binds = binds eqc1 `unionBags` binds eqc2
253 , skolems = skolems eqc1 `unionVarSet` skolems eqc2
256 emptyEqConfig :: EqConfig
257 emptyEqConfig = EqConfig
262 , skolems = emptyVarSet
265 instance Outputable EqConfig where
266 ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
267 = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
270 The set of operations on an equality configuration. We obtain the initialise
271 configuration by normalisation ('normaliseEqs'), solve the equalities by
272 propagation ('propagateEqs'), and eventually finalise the configuration when
273 no further propoagation is possible.
276 -- |Turn a set of equalities into an equality configuration for solving.
278 -- Precondition: The Insts are zonked.
280 normaliseEqs :: [Inst] -> TcM EqConfig
282 = do { if debugIsOn then do { all_unsolved <- allM wantedEqInstIsUnsolved eqs
283 ; let msg = ptext (sLit "(This warning is harmless; for Simon & Manuel)")
284 ; WARN( not all_unsolved, msg $$ ppr eqs ) return () }
286 -- This is just a warning (not an error) because a current
287 -- harmless bug means that we sometimes solve the same
288 -- equality more than once It'll go away with the new
289 -- solver. See Trac #2999 for example
291 ; traceTc $ ptext (sLit "Entering normaliseEqs")
293 ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
294 ; return $ emptyEqConfig { eqs = concat eqss
295 , skolems = unionVarSets skolemss
299 -- |Flatten the type arguments of all dictionaries, returning the result as a
300 -- equality configuration. The dictionaries go into the 'wanted' component if
301 -- the second argument is 'True'.
303 -- Precondition: The Insts are zonked.
305 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
306 normaliseDicts isWanted insts
307 = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
308 ptext (if isWanted then sLit "[Wanted] for"
309 else sLit "[Local] for"))
311 ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
314 ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
315 4 (ppr insts' $$ ppr eqss)
316 ; return $ emptyEqConfig { eqs = concat eqss
317 , locals = if isWanted then [] else insts'
318 , wanteds = if isWanted then insts' else []
319 , binds = unionManyBags bindss
320 , skolems = unionVarSets skolemss
324 -- |Solves the equalities as far as possible by applying propagation rules.
326 propagateEqs :: EqConfig -> TcM EqConfig
327 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
328 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
331 ; propagate todoEqs (eqCfg {eqs = []})
334 -- |Finalise a set of equalities and associated dictionaries after
335 -- propagation. The returned Boolean value is `True' iff any flexible
336 -- variables, except those introduced by flattening (i.e., those in the
337 -- `skolems' component of the argument) where instantiated. The first returned
338 -- set of instances are the locals (without equalities) and the second set are
339 -- all residual wanteds, including equalities.
341 finaliseEqsAndDicts :: EqConfig
342 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
343 finaliseEqsAndDicts (EqConfig { eqs = eqs
349 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
350 ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
351 ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
352 ; let final_binds = subst_binds `unionBags` binds
354 -- Assert that all cotvs of wanted equalities are still unfilled, and
355 -- zonk all final insts, to make any improvement visible
356 ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
357 ; zonked_locals <- zonkInsts locals'
358 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
359 ; return (zonked_locals, zonked_wanteds, final_binds, improved)
364 %************************************************************************
366 Normalisation of equalities
368 %************************************************************************
370 A normal equality is a properly oriented equality with associated coercion
371 that contains at most one family equality (in its left-hand side) is oriented
372 such that it may be used as a reqrite rule. It has one of the following two
375 (1) co :: F t1..tn ~ t (family equalities)
376 (2) co :: x ~ t (variable equalities)
378 Variable equalities fall again in two classes:
380 (2a) co :: x ~ t, where t is *not* a variable, or
381 (2b) co :: x ~ y, where x > y.
383 The types t, t1, ..., tn may not contain any occurrences of synonym
384 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
385 the right-hand side, and the relation x > y is an arbitrary, but total order
390 = RewriteVar -- Form (2) above
391 { rwi_var :: TyVar -- may be rigid or flexible
392 , rwi_right :: TcType -- contains no synonym family applications
393 , rwi_co :: EqInstCo -- the wanted or given coercion
395 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
396 , rwi_swapped :: Bool -- swapped orientation of original EqInst
398 | RewriteFam -- Forms (1) above
399 { rwi_fam :: TyCon -- synonym family tycon
400 , rwi_args :: [Type] -- contain no synonym family applications
401 , rwi_right :: TcType -- contains no synonym family applications
402 , rwi_co :: EqInstCo -- the wanted or given coercion
404 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
405 , rwi_swapped :: Bool -- swapped orientation of original EqInst
408 isWantedRewriteInst :: RewriteInst -> Bool
409 isWantedRewriteInst = isWantedCo . rwi_co
411 rewriteInstToInst :: RewriteInst -> TcM Inst
412 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
413 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
414 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
415 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
417 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
420 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
421 deriveEqInst rewrite ty1 ty2 co
422 = do { co_adjusted <- if not swapped then return co
423 else mkSymEqInstCo co (ty2, ty1)
427 , tci_co = co_adjusted
428 , tci_loc = rwi_loc rewrite
429 , tci_name = rwi_name rewrite
433 swapped = rwi_swapped rewrite
434 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
436 instance Outputable RewriteInst where
437 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
438 = hsep [ pprEqInstCo co <+> text "::"
439 , ppr (mkTyConApp fam args)
443 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
444 = hsep [ pprEqInstCo co <+> text "::"
450 pprEqInstCo :: EqInstCo -> SDoc
451 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
452 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
455 The following functions turn an arbitrary equality into a set of normal
456 equalities. This implements the WFlat and LFlat rules of the paper in one
457 sweep. However, we use flexible variables for both locals and wanteds, and
458 avoid to carry around the unflattening substitution \Sigma (for locals) by
459 already updating the skolems for locals with the family application that they
460 represent - i.e., they will turn into that family application on the next
461 zonking (which only happens after finalisation).
463 In a corresponding manner, normDict normalises class dictionaries by
464 extracting any synonym family applications and generation appropriate normal
467 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
468 we drop that equality and raise an error if it is a wanted or a warning if it
472 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
473 -- Normalise one equality.
475 = ASSERT( isEqInst inst )
476 do { traceTc $ ptext (sLit "normEqInst of ") <+>
477 pprEqInstCo co <+> text "::" <+>
478 ppr ty1 <+> text "~" <+> ppr ty2
479 ; res <- go ty1 ty2 co
480 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
484 (ty1, ty2) = eqInstTys inst
485 co = eqInstCoercion inst
487 -- look through synonyms
488 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
489 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
491 -- left-to-right rule with type family head
492 go ty1@(TyConApp con args) ty2 co
493 | isOpenSynTyConApp ty1 -- only if not oversaturated
494 = mkRewriteFam False con args ty2 co
496 -- right-to-left rule with type family head
497 go ty1 ty2@(TyConApp con args) co
498 | isOpenSynTyConApp ty2 -- only if not oversaturated
499 = do { co' <- mkSymEqInstCo co (ty2, ty1)
500 ; mkRewriteFam True con args ty1 co'
503 -- no outermost family
505 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
506 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
507 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
508 sym_co2 = mkSymCoercion co2
510 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
511 ; eqs <- checkOrientation ty1' ty2' co' inst
512 ; if isLoopyEquality eqs ty12_eqs'
513 then do { if isWantedCo (tci_co inst)
515 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
518 warnDroppingLoopyEquality ty1 ty2
519 ; return ([], emptyVarSet) -- drop the equality
522 return (eqs ++ ty12_eqs',
523 ty1_skolems `unionVarSet` ty2_skolems)
526 mkRewriteFam swapped con args ty2 co
527 = do { (args', cargs, args_eqss, args_skolemss)
528 <- mapAndUnzip4M (flattenType inst) args
529 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
530 ; let co1 = mkTyConApp con cargs
531 sym_co2 = mkSymCoercion co2
532 all_eqs = concat args_eqss ++ ty2_eqs
533 eqTys = (mkTyConApp con args', ty2')
534 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
535 ; let thisRewriteFam = RewriteFam
540 , rwi_loc = tci_loc inst
541 , rwi_name = tci_name inst
542 , rwi_swapped = swapped
544 ; return $ (thisRewriteFam : all_eqs',
545 unionVarSets (ty2_skolems:args_skolemss))
548 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
549 -- have a variable equality with 'a' on the lhs as the first equality.
550 -- Then, check whether 'a' occurs in the lhs of any family equality
551 -- generated by flattening.
552 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
553 = any inRewriteFam eqs
555 inRewriteFam (RewriteFam {rwi_args = args})
556 = tv `elemVarSet` tyVarsOfTypes args
557 inRewriteFam _ = False
558 isLoopyEquality _ _ = False
560 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
561 -- Normalise one dictionary or IP constraint.
562 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
563 = do { (args', cargs, args_eqss, args_skolemss)
564 <- mapAndUnzip4M (flattenType inst) args
565 ; let rewriteCo = PredTy $ ClassP clas cargs
566 eqs = concat args_eqss
567 pred' = ClassP clas args'
569 then -- don't generate a binding if there is nothing to flatten
570 return (inst, [], emptyBag, emptyVarSet)
572 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
573 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
574 ; return (inst', eqs', bind, unionVarSets args_skolemss)
576 normDict _isWanted inst
577 = return (inst, [], emptyBag, emptyVarSet)
578 -- !!!TODO: Still need to normalise IP constraints.
580 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
581 -- Performs the occurs check, decomposition, and proper orientation
582 -- (returns a singleton, or an empty list in case of a trivial equality)
583 -- NB: We cannot assume that the two types already have outermost type
584 -- synonyms expanded due to the recursion in the case of type applications.
585 checkOrientation ty1 ty2 co inst
588 -- look through synonyms
589 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
590 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
592 -- identical types => trivial
595 = do { mkIdEqInstCo co ty1
599 -- two tvs, left greater => unchanged
600 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
602 = mkRewriteVar False tv1 ty2 co
604 -- two tvs, right greater => swap
606 = do { co' <- mkSymEqInstCo co (ty2, ty1)
607 ; mkRewriteVar True tv2 ty1 co'
610 -- only lhs is a tv => unchanged
611 go ty1@(TyVarTy tv1) ty2
612 | ty1 `tcPartOfType` ty2 -- occurs check!
613 = occurCheckErr ty1 ty2
615 = mkRewriteVar False tv1 ty2 co
617 -- only rhs is a tv => swap
618 go ty1 ty2@(TyVarTy tv2)
619 | ty2 `tcPartOfType` ty1 -- occurs check!
620 = occurCheckErr ty2 ty1
622 = do { co' <- mkSymEqInstCo co (ty2, ty1)
623 ; mkRewriteVar True tv2 ty1 co'
626 -- type applications => decompose
628 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
629 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
630 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
631 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
632 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
633 ; return $ eqs_l ++ eqs_r
635 -- !!!TODO: would be more efficient to handle the FunApp and the data
636 -- constructor application explicitly.
638 -- inconsistency => type error
640 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
643 mkRewriteVar swapped tv ty co = return [RewriteVar
647 , rwi_loc = tci_loc inst
648 , rwi_name = tci_name inst
649 , rwi_swapped = swapped
652 flattenType :: Inst -- context to get location & name
653 -> Type -- the type to flatten
654 -> TcM (Type, -- the flattened type
655 Coercion, -- coercion witness of flattening wanteds
656 [RewriteInst], -- extra equalities
657 TyVarSet) -- new intermediate skolems
658 -- Removes all family synonyms from a type by moving them into extra equalities
662 -- look through synonyms
663 go ty | Just ty' <- tcView ty
664 = do { (ty_flat, co, eqs, skolems) <- go ty'
666 then -- unchanged, keep the old type with folded synonyms
667 return (ty, ty, [], emptyVarSet)
669 return (ty_flat, co, eqs, skolems)
672 -- type variable => nothing to do
674 = return (ty, ty, [] , emptyVarSet)
676 -- type family application & family arity matches number of args
677 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
678 go ty@(TyConApp con args)
679 | isOpenSynTyConApp ty -- only if not oversaturated
680 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
681 ; alpha <- newFlexiTyVar (typeKind ty)
682 ; let alphaTy = mkTyVarTy alpha
683 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
684 ; let thisRewriteFam = RewriteFam
687 , rwi_right = alphaTy
688 , rwi_co = mkWantedCo cotv
689 , rwi_loc = tci_loc inst
690 , rwi_name = tci_name inst
694 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
695 thisRewriteFam : concat args_eqss,
696 unionVarSets args_skolemss `extendVarSet` alpha)
697 } -- adding new unflatten var inst
699 -- data constructor application => flatten subtypes
700 -- NB: Special cased for efficiency - could be handled as type application
701 go ty@(TyConApp con args)
702 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
703 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
705 then -- unchanged, keep the old type with folded synonyms
706 return (ty, ty, [], emptyVarSet)
708 return (mkTyConApp con args',
709 mkTyConApp con cargs,
711 unionVarSets args_skolemss)
714 -- function type => flatten subtypes
715 -- NB: Special cased for efficiency - could be handled as type application
716 go ty@(FunTy ty_l ty_r)
717 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
718 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
719 ; if null eqs_l && null eqs_r
720 then -- unchanged, keep the old type with folded synonyms
721 return (ty, ty, [], emptyVarSet)
723 return (mkFunTy ty_l' ty_r',
726 skolems_l `unionVarSet` skolems_r)
729 -- type application => flatten subtypes
731 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
732 -- need to use the smart split as ty may be an
733 -- oversaturated family application
734 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
735 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
736 ; if null eqs_l && null eqs_r
737 then -- unchanged, keep the old type with folded synonyms
738 return (ty, ty, [], emptyVarSet)
740 return (mkAppTy ty_l' ty_r',
743 skolems_l `unionVarSet` skolems_r)
746 -- forall type => panic if the body contains a type family
747 -- !!!TODO: As long as the family does not contain a quantified variable
748 -- we might pull it out, but what if it does contain a quantified
750 go ty@(ForAllTy _ body)
751 | null (tyFamInsts body)
752 = return (ty, ty, [] , emptyVarSet)
754 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
756 -- we should never see a predicate type
758 = panic "TcTyFuns.flattenType: unexpected PredType"
760 go _ = panic "TcTyFuns: suppress bogus warning"
762 adjustCoercions :: EqInstCo -- coercion of original equality
763 -> Coercion -- coercion witnessing the left rewrite
764 -> Coercion -- coercion witnessing the right rewrite
765 -> (Type, Type) -- types of flattened equality
766 -> [RewriteInst] -- equalities from flattening
767 -> TcM (EqInstCo, -- coercion for flattened equality
768 [RewriteInst]) -- final equalities from flattening
769 -- Depending on whether we flattened a local or wanted equality, that equality's
770 -- coercion and that of the new equalities produced during flattening are
772 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
773 -- wanted => generate a fresh coercion variable for the flattened equality
774 = do { cotv' <- newMetaCoVar ty_l ty_r
775 ; writeMetaTyVar cotv $
776 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
777 ; return (Left cotv', all_eqs)
780 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
781 -- local => turn all new equalities into locals and update (but not zonk)
783 = do { all_eqs' <- mapM wantedToLocal all_eqs
784 ; return (co, all_eqs')
787 mkDictBind :: Inst -- original instance
788 -> Bool -- is this a wanted contraint?
789 -> Coercion -- coercion witnessing the rewrite
790 -> PredType -- coerced predicate
791 -> TcM (Inst, -- new inst
792 TcDictBinds) -- binding for coerced dictionary
793 mkDictBind dict isWanted rewriteCo pred
794 = do { dict' <- newDictBndr loc pred
795 -- relate the old inst to the new one
796 -- target_dict = source_dict `cast` st_co
797 ; let (target_dict, source_dict, st_co)
798 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
799 | otherwise = (dict', dict, rewriteCo)
801 -- co :: dict ~ dict'
802 -- hence, if isWanted
803 -- dict = dict' `cast` sym co
805 -- dict' = dict `cast` co
806 expr = HsVar $ instToId source_dict
807 cast_expr = HsWrap (WpCast st_co) expr
808 rhs = L (instLocSpan loc) cast_expr
809 binds = instToDictBind target_dict rhs
810 ; return (dict', binds)
815 -- gamma ::^l Fam args ~ alpha
816 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
817 -- (the update of alpha will not be apparent during propagation, as we
818 -- never follow the indirections of meta variables; it will be revealed
819 -- when the equality is zonked)
821 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
822 -- have escaped into some other coercions during normalisation.
824 wantedToLocal :: RewriteInst -> TcM RewriteInst
825 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
827 rwi_right = TyVarTy alpha,
828 rwi_co = Left gamma})
829 = do { writeMetaTyVar alpha (mkTyConApp fam args)
830 ; writeMetaTyVar gamma (mkTyConApp fam args)
831 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
833 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
837 %************************************************************************
839 Propagation of equalities
841 %************************************************************************
843 Apply the propagation rules exhaustively.
846 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
847 propagate [] eqCfg = return eqCfg
848 propagate (eq:eqs) eqCfg
849 = do { optEqs <- applyTop eq
852 -- Top applied to 'eq' => retry with new equalities
853 Just (eqs2, skolems2)
854 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
856 -- Top doesn't apply => try subst rules with all other
857 -- equalities, after that 'eq' can go into the residual list
859 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
860 ; propagate eqs' (eqCfg' `addEq` eq)
864 applySubstRules :: RewriteInst -- currently considered eq
865 -> [RewriteInst] -- todo eqs list
866 -> EqConfig -- residual
867 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
868 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
869 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
870 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
871 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
872 eqConfig {eqs = unchangedEqs_r}
873 `addSkolems` (skolems_t `unionVarSet` skolems_r))
876 mapSubstRules :: RewriteInst -- try substituting this equality
877 -> [RewriteInst] -- into these equalities
878 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
880 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
881 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
885 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
886 4 (ppr eq1 $$ ppr eq2)
888 -- try the SubstFam rule
889 ; optEqs <- applySubstFam eq1 eq2
891 Just (eqs, skolems) -> return (eqs, [], skolems)
893 { -- try the SubstVarVar rule
894 optEqs <- applySubstVarVar eq1 eq2
896 Just (eqs, skolems) -> return (eqs, [], skolems)
898 { -- try the SubstVarFam rule
899 optEqs <- applySubstVarFam eq1 eq2
901 Just eq -> return ([eq], [], emptyVarSet)
902 Nothing -> return ([], [eq2], emptyVarSet)
903 -- if no rule matches, we return the equlity we tried to
904 -- substitute into unchanged
908 Attempt to apply the Top rule. The rule is
912 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
914 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
916 Returns Nothing if the rule could not be applied. Otherwise, the resulting
917 equality is normalised and a list of the normal equalities is returned.
920 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
922 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
923 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
925 Nothing -> return Nothing
926 Just (lhs, rewrite_co)
927 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
928 ; eq' <- deriveEqInst eq lhs rhs co'
929 ; liftM Just $ normEqInst eq'
936 applyTop _ = return Nothing
939 Attempt to apply the SubstFam rule. The rule is
941 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
943 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
945 where co1 may be a wanted only if co2 is a wanted, too.
947 Returns Nothing if the rule could not be applied. Otherwise, the equality
948 co2' is normalised and a list of the normal equalities is returned. (The
949 equality co1 is not returned as it remain unaltered.)
952 applySubstFam :: RewriteInst
954 -> TcM (Maybe ([RewriteInst], TyVarSet))
955 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
956 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
958 -- rule matches => rewrite
959 | fam1 == fam2 && tcEqTypes args1 args2 &&
960 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
961 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
962 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
963 ; liftM Just $ normEqInst eq2'
966 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
967 | fam1 == fam2 && tcEqTypes args1 args2 &&
968 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
969 = return $ Just ([eq2], emptyVarSet)
974 co1 = eqInstCoType (rwi_co eq1)
977 applySubstFam _ _ = return Nothing
980 Attempt to apply the SubstVarVar rule. The rule is
982 co1 :: x ~ t & co2 :: x ~ s
984 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
986 where co1 may be a wanted only if co2 is a wanted, too.
988 Returns Nothing if the rule could not be applied. Otherwise, the equality
989 co2' is normalised and a list of the normal equalities is returned. (The
990 equality co1 is not returned as it remain unaltered.)
993 applySubstVarVar :: RewriteInst
995 -> TcM (Maybe ([RewriteInst], TyVarSet))
996 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
997 eq2@(RewriteVar {rwi_var = tv2})
999 -- rule matches => rewrite
1001 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1002 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1003 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1004 ; liftM Just $ normEqInst eq2'
1007 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1009 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1010 = return $ Just ([eq2], emptyVarSet)
1015 co1 = eqInstCoType (rwi_co eq1)
1018 applySubstVarVar _ _ = return Nothing
1021 Attempt to apply the SubstVarFam rule. The rule is
1023 co1 :: x ~ t & co2 :: F s1..sn ~ s
1025 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1026 with co2 = [co1/x](F s1..sn) |> co2'
1028 where x occurs in F s1..sn. (co1 may be local or wanted.)
1030 Returns Nothing if the rule could not be applied. Otherwise, the equality
1031 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1034 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1036 -- rule matches => rewrite
1037 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1038 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1039 | tv1 `elemVarSet` tyVarsOfTypes args2
1040 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1041 args2' = substTysWith [tv1] [rhs1] args2
1042 lhs2 = mkTyConApp fam2 args2'
1043 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1044 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1047 rhs1 = rwi_right eq1
1048 rhs2 = rwi_right eq2
1049 co1 = eqInstCoType (rwi_co eq1)
1052 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1053 applySubstVarFam (RewriteFam {rwi_args = args1})
1054 eq2@(RewriteVar {rwi_var = tv2})
1055 | tv2 `elemVarSet` tyVarsOfTypes args1
1058 applySubstVarFam _ _ = return Nothing
1062 %************************************************************************
1064 Finalisation of equalities
1066 %************************************************************************
1068 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1069 (both local and wanted) into the left-hand sides of all other equalities. This
1070 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1071 implied by one variable equality exhaustively before turning to the next and
1072 (2) we need an occurs check.
1074 We also apply the same substitutions to the local and wanted class and IP
1077 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1078 substitute them into right-hand sides of equalities, to avoid getting two
1079 competing instantiations for a type variables; e.g., consider
1081 F s ~ alpha, alpha ~ t
1083 If we don't substitute `alpha ~ t', we may instantiate t with `F s' instead.
1084 This would be bad as `F s' is less useful, eg, as an argument to a class
1087 However, there is no reason why we would want to *substitute* `alpha ~ t' into a
1088 class constraint. We rather wait until `alpha' is instantiated to `t` and
1089 save the extra dictionary binding that substitution would introduce.
1090 Moreover, we may substitute wanted equalities only into wanted dictionaries.
1093 * Given that we apply the substitution corresponding to a single equality
1094 exhaustively, before turning to the next, and because we eliminate recursive
1095 equalities, all opportunities for subtitution will have been exhausted after
1096 we have considered each equality once.
1099 substitute :: [RewriteInst] -- equalities
1100 -> [Inst] -- local class dictionaries
1101 -> [Inst] -- wanted class dictionaries
1102 -> TcM ([RewriteInst], -- equalities after substitution
1103 TcDictBinds, -- all newly generated dictionary bindings
1104 [Inst], -- local dictionaries after substitution
1105 [Inst]) -- wanted dictionaries after substitution
1106 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1108 subst [] res binds locals wanteds
1109 = return (res, binds, locals, wanteds)
1111 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1112 res binds locals wanteds
1113 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
1115 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1116 tySubst = zipOpenTvSubst [tv] [ty]
1117 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1118 ; res' <- mapM (substEq eq coSubst tySubst) res
1120 -- only susbtitute local equalities into local dictionaries
1121 ; (lbinds, locals') <- if not (isWantedCo co)
1124 (substDict eq coSubst tySubst False)
1129 -- flexible tvs in wanteds will be instantiated anyway, there is
1130 -- no need to substitute them into dictionaries
1131 ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
1134 (substDict eq coSubst tySubst True)
1137 return ([], wanteds)
1139 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1140 ; subst eqs' (eq:res') binds' locals' wanteds'
1142 subst (eq:eqs) res binds locals wanteds
1143 = subst eqs (eq:res) binds locals wanteds
1145 -- We have, co :: tv ~ ty
1146 -- => apply [ty/tv] to right-hand side of eq2
1147 -- (but only if tv actually occurs in the right-hand side of eq2)
1148 substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1150 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1151 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1152 right2' = substTy tySubst (rwi_right eq2)
1154 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1155 RewriteFam {rwi_fam = fam,
1156 rwi_args = args} ->mkTyConApp fam args
1157 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1159 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1160 -> occurCheckErr left2 right2'
1161 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1168 -- We have, co :: tv ~ ty
1169 -- => apply [ty/tv] to dictionary predicate
1170 -- (but only if tv actually occurs in the predicate)
1171 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1173 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1174 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1175 pred' = substPred tySubst (tci_pred dict)
1176 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1177 ; return (binds, dict')
1181 substDict _ _ _ _ dict
1182 = return (emptyBag, dict)
1183 -- !!!TODO: Still need to substitute into IP constraints.
1186 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1187 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1188 Return all remaining wanted equalities. The Boolean result component is True
1189 if at least one instantiation of a flexible that is *not* a skolem from
1190 flattening was performed.
1192 We need to instantiate all flexibles that arose as skolems during flattening
1193 of wanteds before we instantiate any other flexibles. Consider F delta ~
1194 alpha, F alpha ~ delta, where alpha is a skolem and delta a free flexible. We
1195 need to produce F (F delta) ~ delta (and not F (F alpha) ~ alpha). Otherwise,
1196 we may wrongly claim to having performed an improvement, which can lead to
1197 non-termination of the combined class-family solver.
1200 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
1201 instantiateAndExtract eqs localsEmpty skolems
1202 = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
1203 4 (ppr eqs $$ ppr skolems)
1204 -- start by *only* instantiating skolem flexibles from flattening
1205 ; unflat_wanteds <- liftM catMaybes $
1206 mapM (inst (`elemVarSet` skolems)) wanteds
1207 -- only afterwards instantiate free flexibles
1208 ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds
1209 ; let improvement = length residuals < length unflat_wanteds
1210 ; residuals' <- mapM rewriteInstToInst residuals
1211 ; return (residuals', improvement)
1214 wanteds = filter (isWantedCo . rwi_co) eqs
1215 checkingMode = length eqs > length wanteds || not localsEmpty
1216 -- no local equalities or dicts => checking mode
1218 -- co :: alpha ~ t or co :: a ~ alpha
1219 inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1220 = do { flexi_tv1 <- isFlexible mayInst tv1
1221 ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2
1222 ; case (flexi_tv1, maybe_flexi_tv2) of
1224 -> -- co :: alpha ~ t
1225 doInst (rwi_swapped eq) tv1 ty2 co eq
1227 -> -- co :: a ~ alpha
1228 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1229 _ -> return $ Just eq
1232 -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
1233 inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1234 rwi_right = ty2, rwi_co = co})
1235 | Just tv2 <- tcGetTyVar_maybe ty2
1237 , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
1238 -- !!!FIXME: this is too liberal, even if tv2 is in
1239 -- skolems we shouldn't instantiate if tvs occurs
1240 -- in other equalities that may propagate it into the
1242 = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1244 inst _mayInst eq = return $ Just eq
1246 -- tv is a meta var and not filled
1247 isFlexible mayInst tv
1248 | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
1249 | otherwise = return False
1251 -- type is a tv that is a meta var and not filled
1252 isFlexibleTy mayInst ty
1253 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst tv
1254 ; if flexi then return $ Just tv
1257 | otherwise = return Nothing
1259 doInst _swapped _tv _ty (Right ty) _eq
1260 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1261 doInst swapped tv ty (Left cotv) eq
1262 = do { lookupTV <- lookupTcTyVar tv
1263 ; uMeta swapped tv lookupTV ty cotv
1266 -- meta variable has been filled already
1267 -- => keep the equality
1268 uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1270 ptext (sLit "flexible") <+> ppr tv <+>
1271 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1272 ptext (sLit "meant to fill with") <+> ppr ty
1276 -- type variable meets type variable
1277 -- => check that tv2 hasn't been updated yet and choose which to update
1278 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1280 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1283 = do { lookupTV2 <- lookupTcTyVar tv2
1286 uMeta swapped tv1 (DoneTv details1) ty cotv
1288 uMetaVar swapped tv1 details1 tv2 details2 cotv
1291 ------ Beyond this point we know that ty2 is not a type variable
1293 -- signature skolem meets non-variable type
1294 -- => cannot update (retain the equality)!
1295 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1298 -- updatable meta variable meets non-variable type
1299 -- => occurs check, monotype check, and kinds match check, then update
1300 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1301 = do { -- occurs + monotype check
1302 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1306 -- there may be a family in non_tv_ty due to an unzonked,
1307 -- but updated skolem for a local equality
1310 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1311 ; writeMetaTyVar cotv ty' -- update co var
1316 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1318 -- uMetaVar: unify two type variables
1319 -- meta variable meets skolem
1321 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1322 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1323 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1327 -- meta variable meets meta variable
1328 -- => be clever about which of the two to update
1329 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1330 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1331 = do { case (info1, info2) of
1332 -- Avoid SigTvs if poss
1333 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1334 (_, SigTv _) | k2_sub_k1 -> update_tv1
1336 (_, _) | k1_sub_k2 -> if k2_sub_k1 &&
1338 then update_tv1 -- Same kinds
1340 | k2_sub_k1 -> update_tv1
1341 | otherwise -> kind_err
1342 -- Update the variable with least kind info
1343 -- See notes on type inference in Kind.lhs
1344 -- The "nicer to" part only applies if the two kinds are the same,
1345 -- so we can choose which to do.
1347 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1351 -- Kinds should be guaranteed ok at this point
1352 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1353 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1355 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1356 unifyKindMisMatch k1 k2
1360 k1_sub_k2 = k1 `isSubKind` k2
1361 k2_sub_k1 = k2 `isSubKind` k1
1363 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1364 -- Try to update sys-y type variables in preference to ones
1365 -- gotten (say) by instantiating a polymorphic function with
1366 -- a user-written type sig
1368 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1372 %************************************************************************
1376 %************************************************************************
1378 The infamous couldn't match expected type soandso against inferred type
1379 somethingdifferent message.
1382 eqInstMisMatch :: Inst -> TcM a
1384 = ASSERT( isEqInst inst )
1385 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1387 (ty_act, ty_exp) = eqInstTys inst
1388 InstLoc _ _ ctxt = instLoc inst
1390 -----------------------
1391 failWithMisMatch :: TcType -> TcType -> TcM a
1392 -- Generate the message when two types fail to match,
1393 -- going to some trouble to make it helpful.
1394 -- The argument order is: actual type, expected type
1395 failWithMisMatch ty_act ty_exp
1396 = do { env0 <- tcInitTidyEnv
1397 ; ty_exp <- zonkTcType ty_exp
1398 ; ty_act <- zonkTcType ty_act
1399 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1402 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1403 misMatchMsg env0 (ty_act, ty_exp)
1404 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1405 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1406 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1408 ptext (sLit "against inferred type") <+> pp_act],
1409 nest 2 (extra_exp $$ extra_act)]
1414 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1416 = let (env1, tidy_ty) = tidyOpenType env ty
1417 (env2, extra) = ppr_extra env1 tidy_ty
1419 (env2, quotes (ppr tidy_ty), extra)
1421 -- (ppr_extra env ty) shows extra info about 'ty'
1422 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1423 ppr_extra env (TyVarTy tv)
1424 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1425 = (env1, pprSkolTvBinding tv1)
1427 (env1, tv1) = tidySkolemTyVar env tv
1429 ppr_extra env _ty = (env, empty) -- Normal case
1432 Warn of loopy local equalities that were dropped.
1435 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1436 warnDroppingLoopyEquality ty1 ty2
1437 = do { env0 <- tcInitTidyEnv
1438 ; ty1 <- zonkTcType ty1
1439 ; ty2 <- zonkTcType ty2
1440 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1441 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1442 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1443 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))