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 )
51 %************************************************************************
53 Normalisation of types wrt toplevel equality schemata
55 %************************************************************************
57 Unfold a single synonym family instance and yield the witnessing coercion.
58 Return 'Nothing' if the given type is either not synonym family instance
59 or is a synonym family instance that has no matching instance declaration.
60 (Applies only if the type family application is outermost.)
62 For example, if we have
64 :Co:R42T a :: T [a] ~ :R42T a
66 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
69 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
70 tcUnfoldSynFamInst (TyConApp tycon tys)
71 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
74 = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
75 ; maybeFamInst <- tcLookupFamInst tycon tys
76 ; case maybeFamInst of
77 Nothing -> return Nothing
78 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
79 mkTyConApp coe_tc rep_tys)
81 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
82 (tyConFamilyCoercion_maybe rep_tc)
84 tcUnfoldSynFamInst _other = return Nothing
87 Normalise 'Type's and 'PredType's by unfolding type family applications where
88 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
90 tcNormaliseFamInst ty = (co, ty')
94 -- |Normalise the given type as far as possible with toplevel equalities.
95 -- This results in a coercion witnessing the type equality, in addition to the
98 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
99 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
102 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
103 apply the normalisation function gives as the first argument to every TyConApp
104 and every TyVarTy subterm.
106 tcGenericNormaliseFamInst fun ty = (co, ty')
109 This function is (by way of using smart constructors) careful to ensure that
110 the returned coercion is exactly IdCo (and not some semantically equivalent,
111 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
112 makes it easy for the caller to determine whether the type changed. BUT
113 even if we return IdCo, ty' may be *syntactically* different from ty due to
114 unfolded closed type synonyms (by way of tcCoreView). In the interest of
115 good error messages, callers should discard ty' in favour of ty in this case.
118 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
119 -- what to do with type functions and tyvars
120 -> TcType -- old type
121 -> TcM (CoercionI, TcType) -- (coercion, new type)
122 tcGenericNormaliseFamInst fun ty
123 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
124 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
125 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
126 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
127 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
128 ; case maybe_ty_co of
129 -- a matching family instance exists
131 do { let first_coi = mkTransCoI tycon_coi (ACo co)
132 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
133 ; let fix_coi = mkTransCoI first_coi rest_coi
134 ; return (fix_coi, nty)
136 -- no matching family instance exists
137 -- we do not do anything
138 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
140 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
141 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
142 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
143 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
145 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
146 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
147 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
148 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
150 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
151 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
152 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
154 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
156 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
157 ; res <- lookupTcTyVar tv
160 do { maybe_ty' <- fun ty
162 Nothing -> return (IdCo, ty)
164 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
165 ; return (ACo co1 `mkTransCoI` coi2, ty'')
168 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
172 tcGenericNormaliseFamInst fun (PredTy predty)
173 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
174 ; return (coi, PredTy pred') }
176 ---------------------------------
177 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
179 -> TcM (CoercionI, TcPredType)
181 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
182 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
183 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
185 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
186 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
187 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
189 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
190 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
191 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
192 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
196 %************************************************************************
198 Normalisation of instances wrt to equalities
200 %************************************************************************
203 tcReduceEqs :: [Inst] -- locals
205 -> TcM ([Inst], -- normalised locals (w/o equalities)
206 [Inst], -- normalised wanteds (including equalities)
207 TcDictBinds, -- bindings for all simplified dictionaries
208 Bool) -- whether any flexibles where instantiated
209 tcReduceEqs locals wanteds
210 = do { let (local_eqs , local_dicts) = partition isEqInst locals
211 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
212 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
213 ; eqCfg2 <- normaliseDicts False local_dicts
214 ; eqCfg3 <- normaliseDicts True wanteds_dicts
215 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
216 `unionEqConfig` eqCfg3)
217 ; finaliseEqsAndDicts eqCfg
222 %************************************************************************
224 Equality Configurations
226 %************************************************************************
228 We maintain normalised equalities together with the skolems introduced as
229 intermediates during flattening of equalities as well as
232 -- |Configuration of normalised equalities used during solving.
234 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
235 , locals :: [Inst] -- given dicts
236 , wanteds :: [Inst] -- wanted dicts
237 , binds :: TcDictBinds -- bindings
238 , skolems :: TyVarSet -- flattening skolems
241 addSkolems :: EqConfig -> TyVarSet -> EqConfig
242 addSkolems eqCfg newSkolems
243 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
245 addEq :: EqConfig -> RewriteInst -> EqConfig
246 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
248 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
249 unionEqConfig eqc1 eqc2 = EqConfig
250 { eqs = eqs eqc1 ++ eqs eqc2
251 , locals = locals eqc1 ++ locals eqc2
252 , wanteds = wanteds eqc1 ++ wanteds eqc2
253 , binds = binds eqc1 `unionBags` binds eqc2
254 , skolems = skolems eqc1 `unionVarSet` skolems eqc2
257 emptyEqConfig :: EqConfig
258 emptyEqConfig = EqConfig
263 , skolems = emptyVarSet
266 instance Outputable EqConfig where
267 ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
268 = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
271 The set of operations on an equality configuration. We obtain the initialise
272 configuration by normalisation ('normaliseEqs'), solve the equalities by
273 propagation ('propagateEqs'), and eventually finalise the configuration when
274 no further propoagation is possible.
277 -- |Turn a set of equalities into an equality configuration for solving.
279 -- Precondition: The Insts are zonked.
281 normaliseEqs :: [Inst] -> TcM EqConfig
283 = do { if debugIsOn then do { all_unsolved <- allM wantedEqInstIsUnsolved eqs
284 ; let msg = ptext (sLit "(This warning is harmless; for Simon & Manuel)")
285 ; WARN( not all_unsolved, msg $$ ppr eqs ) return () }
287 -- This is just a warning (not an error) because a current
288 -- harmless bug means that we sometimes solve the same
289 -- equality more than once It'll go away with the new
290 -- solver. See Trac #2999 for example
292 ; traceTc $ ptext (sLit "Entering normaliseEqs")
294 ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
295 ; return $ emptyEqConfig { eqs = concat eqss
296 , skolems = unionVarSets skolemss
300 -- |Flatten the type arguments of all dictionaries, returning the result as a
301 -- equality configuration. The dictionaries go into the 'wanted' component if
302 -- the second argument is 'True'.
304 -- Precondition: The Insts are zonked.
306 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
307 normaliseDicts isWanted insts
308 = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
309 ptext (if isWanted then sLit "[Wanted] for"
310 else sLit "[Local] for"))
312 ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
315 ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
316 4 (ppr insts' $$ ppr eqss)
317 ; return $ emptyEqConfig { eqs = concat eqss
318 , locals = if isWanted then [] else insts'
319 , wanteds = if isWanted then insts' else []
320 , binds = unionManyBags bindss
321 , skolems = unionVarSets skolemss
325 -- |Solves the equalities as far as possible by applying propagation rules.
327 propagateEqs :: EqConfig -> TcM EqConfig
328 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
329 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
332 ; propagate todoEqs (eqCfg {eqs = []})
335 -- |Finalise a set of equalities and associated dictionaries after
336 -- propagation. The returned Boolean value is `True' iff any flexible
337 -- variables, except those introduced by flattening (i.e., those in the
338 -- `skolems' component of the argument) where instantiated. The first returned
339 -- set of instances are the locals (without equalities) and the second set are
340 -- all residual wanteds, including equalities.
342 finaliseEqsAndDicts :: EqConfig
343 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
344 finaliseEqsAndDicts (EqConfig { eqs = eqs
350 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
351 ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
352 ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
353 ; let final_binds = subst_binds `unionBags` binds
355 -- Assert that all cotvs of wanted equalities are still unfilled, and
356 -- zonk all final insts, to make any improvement visible
357 ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
358 ; zonked_locals <- zonkInsts locals'
359 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
360 ; return (zonked_locals, zonked_wanteds, final_binds, improved)
365 %************************************************************************
367 Normalisation of equalities
369 %************************************************************************
371 A normal equality is a properly oriented equality with associated coercion
372 that contains at most one family equality (in its left-hand side) is oriented
373 such that it may be used as a rewrite rule. It has one of the following two
376 (1) co :: F t1..tn ~ t (family equalities)
377 (2) co :: x ~ t (variable equalities)
379 Variable equalities fall again in two classes:
381 (2a) co :: x ~ t, where t is *not* a variable, or
382 (2b) co :: x ~ y, where x > y.
384 The types t, t1, ..., tn may not contain any occurrences of synonym
385 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
386 the right-hand side, and the relation x > y is an (nearly) arbitrary, but
387 total order on type variables. The only restriction that we impose on that
388 order is that for x > y, we are happy to instantiate x with y taking into
389 account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
393 = RewriteVar -- Form (2) above
394 { rwi_var :: TyVar -- may be rigid or flexible
395 , rwi_right :: TcType -- contains no synonym family applications
396 , rwi_co :: EqInstCo -- the wanted or given coercion
398 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
399 , rwi_swapped :: Bool -- swapped orientation of original EqInst
401 | RewriteFam -- Forms (1) above
402 { rwi_fam :: TyCon -- synonym family tycon
403 , rwi_args :: [Type] -- contain no synonym family applications
404 , rwi_right :: TcType -- contains no synonym family applications
405 , rwi_co :: EqInstCo -- the wanted or given coercion
407 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
408 , rwi_swapped :: Bool -- swapped orientation of original EqInst
411 isWantedRewriteInst :: RewriteInst -> Bool
412 isWantedRewriteInst = isWantedCo . rwi_co
414 rewriteInstToInst :: RewriteInst -> TcM Inst
415 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
416 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
417 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
418 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
420 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
423 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
424 deriveEqInst rewrite ty1 ty2 co
425 = do { co_adjusted <- if not swapped then return co
426 else mkSymEqInstCo co (ty2, ty1)
430 , tci_co = co_adjusted
431 , tci_loc = rwi_loc rewrite
432 , tci_name = rwi_name rewrite
436 swapped = rwi_swapped rewrite
437 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
439 instance Outputable RewriteInst where
440 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
441 = hsep [ pprEqInstCo co <+> text "::"
442 , ppr (mkTyConApp fam args)
446 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
447 = hsep [ pprEqInstCo co <+> text "::"
453 pprEqInstCo :: EqInstCo -> SDoc
454 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
455 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
458 The following functions turn an arbitrary equality into a set of normal
459 equalities. This implements the WFlat and LFlat rules of the paper in one
460 sweep. However, we use flexible variables for both locals and wanteds, and
461 avoid to carry around the unflattening substitution \Sigma (for locals) by
462 already updating the skolems for locals with the family application that they
463 represent - i.e., they will turn into that family application on the next
464 zonking (which only happens after finalisation).
466 In a corresponding manner, normDict normalises class dictionaries by
467 extracting any synonym family applications and generation appropriate normal
470 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
471 we drop that equality and raise an error if it is a wanted or a warning if it
475 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
476 -- Normalise one equality.
478 = ASSERT( isEqInst inst )
479 do { traceTc $ ptext (sLit "normEqInst of ") <+>
480 pprEqInstCo co <+> text "::" <+>
481 ppr ty1 <+> text "~" <+> ppr ty2
482 ; res <- go ty1 ty2 co
483 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
487 (ty1, ty2) = eqInstTys inst
488 co = eqInstCoercion inst
490 -- look through synonyms
491 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
492 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
494 -- left-to-right rule with type family head
495 go ty1@(TyConApp con args) ty2 co
496 | isOpenSynTyConApp ty1 -- only if not oversaturated
497 = mkRewriteFam False con args ty2 co
499 -- right-to-left rule with type family head
500 go ty1 ty2@(TyConApp con args) co
501 | isOpenSynTyConApp ty2 -- only if not oversaturated
502 = do { co' <- mkSymEqInstCo co (ty2, ty1)
503 ; mkRewriteFam True con args ty1 co'
506 -- no outermost family
508 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
509 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
510 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
511 sym_co2 = mkSymCoercion co2
513 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
514 ; eqs <- checkOrientation ty1' ty2' co' inst
515 ; if isLoopyEquality eqs ty12_eqs'
516 then do { if isWantedCo (tci_co inst)
518 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
521 warnDroppingLoopyEquality ty1 ty2
522 ; return ([], emptyVarSet) -- drop the equality
525 return (eqs ++ ty12_eqs',
526 ty1_skolems `unionVarSet` ty2_skolems)
529 mkRewriteFam swapped con args ty2 co
530 = do { (args', cargs, args_eqss, args_skolemss)
531 <- mapAndUnzip4M (flattenType inst) args
532 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
533 ; let co1 = mkTyConApp con cargs
534 sym_co2 = mkSymCoercion co2
535 all_eqs = concat args_eqss ++ ty2_eqs
536 eqTys = (mkTyConApp con args', ty2')
537 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
538 ; let thisRewriteFam = RewriteFam
543 , rwi_loc = tci_loc inst
544 , rwi_name = tci_name inst
545 , rwi_swapped = swapped
547 ; return $ (thisRewriteFam : all_eqs',
548 unionVarSets (ty2_skolems:args_skolemss))
551 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
552 -- have a variable equality with 'a' on the lhs as the first equality.
553 -- Then, check whether 'a' occurs in the lhs of any family equality
554 -- generated by flattening.
555 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
556 = any inRewriteFam eqs
558 inRewriteFam (RewriteFam {rwi_args = args})
559 = tv `elemVarSet` tyVarsOfTypes args
560 inRewriteFam _ = False
561 isLoopyEquality _ _ = False
563 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
564 -- Normalise one dictionary or IP constraint.
565 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
566 = do { (args', cargs, args_eqss, args_skolemss)
567 <- mapAndUnzip4M (flattenType inst) args
568 ; let rewriteCo = PredTy $ ClassP clas cargs
569 eqs = concat args_eqss
570 pred' = ClassP clas args'
572 then -- don't generate a binding if there is nothing to flatten
573 return (inst, [], emptyBag, emptyVarSet)
575 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
576 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
577 ; return (inst', eqs', bind, unionVarSets args_skolemss)
579 normDict _isWanted inst
580 = return (inst, [], emptyBag, emptyVarSet)
581 -- !!!TODO: Still need to normalise IP constraints.
583 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
584 -- Performs the occurs check, decomposition, and proper orientation
585 -- (returns a singleton, or an empty list in case of a trivial equality)
586 -- NB: We cannot assume that the two types already have outermost type
587 -- synonyms expanded due to the recursion in the case of type applications.
588 checkOrientation ty1 ty2 co inst
591 -- look through synonyms
592 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
593 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
595 -- identical types => trivial
598 = do { mkIdEqInstCo co ty1
602 -- two tvs (distinct tvs, due to previous equation)
603 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
604 = do { isBigger <- tv1 `tvIsBigger` tv2
605 ; if isBigger -- left greater
606 then mkRewriteVar False tv1 ty2 co -- => unchanged
607 else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater
608 ; mkRewriteVar True tv2 ty1 co' -- => swap
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 -- data type constructor application => decompose
629 -- NB: Special cased for efficiency - could be handled as type application
630 go (TyConApp con1 args1) (TyConApp con2 args2)
632 && not (isOpenSynTyCon con1) -- don't match family synonym apps
633 = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
634 ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
636 ; return $ concat eqss
639 -- function type => decompose
640 -- NB: Special cased for efficiency - could be handled as type application
641 go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
642 = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
643 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
644 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
645 ; return $ eqs_l ++ eqs_r
648 -- type applications => decompose
650 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
651 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
652 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
653 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
654 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
655 ; return $ eqs_l ++ eqs_r
658 -- inconsistency => type error
660 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
663 mkRewriteVar swapped tv ty co = return [RewriteVar
667 , rwi_loc = tci_loc inst
668 , rwi_name = tci_name inst
669 , rwi_swapped = swapped
672 -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
673 tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
675 = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
677 isBigger tv1 (SkolemTv _) tv2 (SkolemTv _)
679 isBigger _ (MetaTv _ _) _ (SkolemTv _)
681 isBigger _ (SkolemTv _) _ (MetaTv _ _)
683 isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
684 -- meta variable meets meta variable
685 -- => be clever about which of the two to update
686 -- (from TcUnify.uUnfilledVars minus boxy stuff)
687 = case (info1, info2) of
688 -- Avoid SigTvs if poss
689 (SigTv _, SigTv _) -> return $ tv1 > tv2
690 (SigTv _, _ ) | k1_sub_k2 -> return False
691 (_, SigTv _) | k2_sub_k1 -> return True
696 -> case (nicer_to_update tv1, nicer_to_update tv2) of
697 (True, False) -> return True
698 (False, True) -> return False
699 _ -> return $ tv1 > tv2
700 | k1_sub_k2 -> return False
701 | k2_sub_k1 -> return True
702 | otherwise -> kind_err >> return True
703 -- Update the variable with least kind info
704 -- See notes on type inference in Kind.lhs
705 -- The "nicer to" part only applies if the two kinds are the same,
706 -- so we can choose which to do.
708 kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
709 unifyKindMisMatch k1 k2
713 k1_sub_k2 = k1 `isSubKind` k2
714 k2_sub_k1 = k2 `isSubKind` k1
716 nicer_to_update tv = isSystemName (Var.varName tv)
717 -- Try to update sys-y type variables in preference to ones
718 -- gotten (say) by instantiating a polymorphic function with
719 -- a user-written type sig
721 flattenType :: Inst -- context to get location & name
722 -> Type -- the type to flatten
723 -> TcM (Type, -- the flattened type
724 Coercion, -- coercion witness of flattening wanteds
725 [RewriteInst], -- extra equalities
726 TyVarSet) -- new intermediate skolems
727 -- Removes all family synonyms from a type by moving them into extra equalities
731 -- look through synonyms
732 go ty | Just ty' <- tcView ty
733 = do { (ty_flat, co, eqs, skolems) <- go ty'
735 then -- unchanged, keep the old type with folded synonyms
736 return (ty, ty, [], emptyVarSet)
738 return (ty_flat, co, eqs, skolems)
741 -- type variable => nothing to do
743 = return (ty, ty, [] , emptyVarSet)
745 -- type family application & family arity matches number of args
746 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
747 go ty@(TyConApp con args)
748 | isOpenSynTyConApp ty -- only if not oversaturated
749 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
750 ; alpha <- newFlexiTyVar (typeKind ty)
751 ; let alphaTy = mkTyVarTy alpha
752 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
753 ; let thisRewriteFam = RewriteFam
756 , rwi_right = alphaTy
757 , rwi_co = mkWantedCo cotv
758 , rwi_loc = tci_loc inst
759 , rwi_name = tci_name inst
763 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
764 thisRewriteFam : concat args_eqss,
765 unionVarSets args_skolemss `extendVarSet` alpha)
766 } -- adding new unflatten var inst
768 -- data constructor application => flatten subtypes
769 -- NB: Special cased for efficiency - could be handled as type application
770 go ty@(TyConApp con args)
771 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
772 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
774 then -- unchanged, keep the old type with folded synonyms
775 return (ty, ty, [], emptyVarSet)
777 return (mkTyConApp con args',
778 mkTyConApp con cargs,
780 unionVarSets args_skolemss)
783 -- function type => flatten subtypes
784 -- NB: Special cased for efficiency - could be handled as type application
785 go ty@(FunTy ty_l ty_r)
786 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
787 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
788 ; if null eqs_l && null eqs_r
789 then -- unchanged, keep the old type with folded synonyms
790 return (ty, ty, [], emptyVarSet)
792 return (mkFunTy ty_l' ty_r',
795 skolems_l `unionVarSet` skolems_r)
798 -- type application => flatten subtypes
800 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
801 -- need to use the smart split as ty may be an
802 -- oversaturated family application
803 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
804 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
805 ; if null eqs_l && null eqs_r
806 then -- unchanged, keep the old type with folded synonyms
807 return (ty, ty, [], emptyVarSet)
809 return (mkAppTy ty_l' ty_r',
812 skolems_l `unionVarSet` skolems_r)
815 -- forall type => panic if the body contains a type family
816 -- !!!TODO: As long as the family does not contain a quantified variable
817 -- we might pull it out, but what if it does contain a quantified
819 go ty@(ForAllTy _ body)
820 | null (tyFamInsts body)
821 = return (ty, ty, [] , emptyVarSet)
823 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
825 -- we should never see a predicate type
827 = panic "TcTyFuns.flattenType: unexpected PredType"
829 go _ = panic "TcTyFuns: suppress bogus warning"
831 adjustCoercions :: EqInstCo -- coercion of original equality
832 -> Coercion -- coercion witnessing the left rewrite
833 -> Coercion -- coercion witnessing the right rewrite
834 -> (Type, Type) -- types of flattened equality
835 -> [RewriteInst] -- equalities from flattening
836 -> TcM (EqInstCo, -- coercion for flattened equality
837 [RewriteInst]) -- final equalities from flattening
838 -- Depending on whether we flattened a local or wanted equality, that equality's
839 -- coercion and that of the new equalities produced during flattening are
841 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
842 -- wanted => generate a fresh coercion variable for the flattened equality
843 = do { cotv' <- newMetaCoVar ty_l ty_r
844 ; writeMetaTyVar cotv $
845 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
846 ; return (Left cotv', all_eqs)
849 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
850 -- local => turn all new equalities into locals and update (but not zonk)
852 = do { all_eqs' <- mapM wantedToLocal all_eqs
853 ; return (co, all_eqs')
856 mkDictBind :: Inst -- original instance
857 -> Bool -- is this a wanted contraint?
858 -> Coercion -- coercion witnessing the rewrite
859 -> PredType -- coerced predicate
860 -> TcM (Inst, -- new inst
861 TcDictBinds) -- binding for coerced dictionary
862 mkDictBind dict isWanted rewriteCo pred
863 = do { dict' <- newDictBndr loc pred
864 -- relate the old inst to the new one
865 -- target_dict = source_dict `cast` st_co
866 ; let (target_dict, source_dict, st_co)
867 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
868 | otherwise = (dict', dict, rewriteCo)
870 -- co :: dict ~ dict'
871 -- hence, if isWanted
872 -- dict = dict' `cast` sym co
874 -- dict' = dict `cast` co
875 expr = HsVar $ instToId source_dict
876 cast_expr = HsWrap (WpCast st_co) expr
877 rhs = L (instLocSpan loc) cast_expr
878 binds = instToDictBind target_dict rhs
879 ; return (dict', binds)
884 -- gamma ::^l Fam args ~ alpha
885 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
886 -- (the update of alpha will not be apparent during propagation, as we
887 -- never follow the indirections of meta variables; it will be revealed
888 -- when the equality is zonked)
890 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
891 -- have escaped into some other coercions during normalisation.
893 wantedToLocal :: RewriteInst -> TcM RewriteInst
894 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
896 rwi_right = TyVarTy alpha,
897 rwi_co = Left gamma})
898 = do { writeMetaTyVar alpha (mkTyConApp fam args)
899 ; writeMetaTyVar gamma (mkTyConApp fam args)
900 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
902 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
906 %************************************************************************
908 Propagation of equalities
910 %************************************************************************
912 Apply the propagation rules exhaustively.
915 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
916 propagate [] eqCfg = return eqCfg
917 propagate (eq:eqs) eqCfg
918 = do { optEqs <- applyTop eq
921 -- Top applied to 'eq' => retry with new equalities
922 Just (eqs2, skolems2)
923 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
925 -- Top doesn't apply => try subst rules with all other
926 -- equalities, after that 'eq' can go into the residual list
928 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
929 ; propagate eqs' (eqCfg' `addEq` eq)
933 applySubstRules :: RewriteInst -- currently considered eq
934 -> [RewriteInst] -- todo eqs list
935 -> EqConfig -- residual
936 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
937 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
938 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
939 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
940 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
941 eqConfig {eqs = unchangedEqs_r}
942 `addSkolems` (skolems_t `unionVarSet` skolems_r))
945 mapSubstRules :: RewriteInst -- try substituting this equality
946 -> [RewriteInst] -- into these equalities
947 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
949 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
950 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
954 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
955 4 (ppr eq1 $$ ppr eq2)
957 -- try the SubstFam rule
958 ; optEqs <- applySubstFam eq1 eq2
960 Just (eqs, skolems) -> return (eqs, [], skolems)
962 { -- try the SubstVarVar rule
963 optEqs <- applySubstVarVar eq1 eq2
965 Just (eqs, skolems) -> return (eqs, [], skolems)
967 { -- try the SubstVarFam rule
968 optEqs <- applySubstVarFam eq1 eq2
970 Just eq -> return ([eq], [], emptyVarSet)
971 Nothing -> return ([], [eq2], emptyVarSet)
972 -- if no rule matches, we return the equlity we tried to
973 -- substitute into unchanged
977 Attempt to apply the Top rule. The rule is
981 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
983 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
985 Returns Nothing if the rule could not be applied. Otherwise, the resulting
986 equality is normalised and a list of the normal equalities is returned.
989 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
991 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
992 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
994 Nothing -> return Nothing
995 Just (lhs, rewrite_co)
996 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
997 ; eq' <- deriveEqInst eq lhs rhs co'
998 ; liftM Just $ normEqInst eq'
1005 applyTop _ = return Nothing
1008 Attempt to apply the SubstFam rule. The rule is
1010 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
1012 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1014 where co1 may be a wanted only if co2 is a wanted, too.
1016 Returns Nothing if the rule could not be applied. Otherwise, the equality
1017 co2' is normalised and a list of the normal equalities is returned. (The
1018 equality co1 is not returned as it remain unaltered.)
1021 applySubstFam :: RewriteInst
1023 -> TcM (Maybe ([RewriteInst], TyVarSet))
1024 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1025 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1027 -- rule matches => rewrite
1028 | fam1 == fam2 && tcEqTypes args1 args2 &&
1029 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1030 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1031 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1032 ; liftM Just $ normEqInst eq2'
1035 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1036 | fam1 == fam2 && tcEqTypes args1 args2 &&
1037 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1038 = return $ Just ([eq2], emptyVarSet)
1043 co1 = eqInstCoType (rwi_co eq1)
1046 applySubstFam _ _ = return Nothing
1049 Attempt to apply the SubstVarVar rule. The rule is
1051 co1 :: x ~ t & co2 :: x ~ s
1053 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1055 where co1 may be a wanted only if co2 is a wanted, too.
1057 Returns Nothing if the rule could not be applied. Otherwise, the equality
1058 co2' is normalised and a list of the normal equalities is returned. (The
1059 equality co1 is not returned as it remain unaltered.)
1062 applySubstVarVar :: RewriteInst
1064 -> TcM (Maybe ([RewriteInst], TyVarSet))
1065 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1066 eq2@(RewriteVar {rwi_var = tv2})
1068 -- rule matches => rewrite
1070 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1071 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1072 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1073 ; liftM Just $ normEqInst eq2'
1076 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1078 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1079 = return $ Just ([eq2], emptyVarSet)
1084 co1 = eqInstCoType (rwi_co eq1)
1087 applySubstVarVar _ _ = return Nothing
1090 Attempt to apply the SubstVarFam rule. The rule is
1092 co1 :: x ~ t & co2 :: F s1..sn ~ s
1094 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1095 with co2 = [co1/x](F s1..sn) |> co2'
1097 where x occurs in F s1..sn. (co1 may be local or wanted.)
1099 Returns Nothing if the rule could not be applied. Otherwise, the equality
1100 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1103 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1105 -- rule matches => rewrite
1106 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1107 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1108 | tv1 `elemVarSet` tyVarsOfTypes args2
1109 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1110 args2' = substTysWith [tv1] [rhs1] args2
1111 lhs2 = mkTyConApp fam2 args2'
1112 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1113 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1116 rhs1 = rwi_right eq1
1117 rhs2 = rwi_right eq2
1118 co1 = eqInstCoType (rwi_co eq1)
1121 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1122 applySubstVarFam (RewriteFam {rwi_args = args1})
1123 eq2@(RewriteVar {rwi_var = tv2})
1124 | tv2 `elemVarSet` tyVarsOfTypes args1
1127 applySubstVarFam _ _ = return Nothing
1131 %************************************************************************
1133 Finalisation of equalities
1135 %************************************************************************
1137 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1138 (both local and wanted) into the left-hand sides of all other equalities. This
1139 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1140 implied by one variable equality exhaustively before turning to the next and
1141 (2) we need an occurs check.
1143 We also apply the same substitutions to the local and wanted class and IP
1146 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1147 substitute them into right-hand sides of equalities, to avoid getting two
1148 competing instantiations for a type variables; e.g., consider
1150 F s ~ alpha, alpha ~ t
1152 If we don't substitute `alpha ~ t', we may instantiate t with `F s' instead.
1153 This would be bad as `F s' is less useful, eg, as an argument to a class
1156 However, there is no reason why we would want to *substitute* `alpha ~ t' into a
1157 class constraint. We rather wait until `alpha' is instantiated to `t` and
1158 save the extra dictionary binding that substitution would introduce.
1159 Moreover, we may substitute wanted equalities only into wanted dictionaries.
1162 * Given that we apply the substitution corresponding to a single equality
1163 exhaustively, before turning to the next, and because we eliminate recursive
1164 equalities, all opportunities for subtitution will have been exhausted after
1165 we have considered each equality once.
1168 substitute :: [RewriteInst] -- equalities
1169 -> [Inst] -- local class dictionaries
1170 -> [Inst] -- wanted class dictionaries
1171 -> TcM ([RewriteInst], -- equalities after substitution
1172 TcDictBinds, -- all newly generated dictionary bindings
1173 [Inst], -- local dictionaries after substitution
1174 [Inst]) -- wanted dictionaries after substitution
1175 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1177 subst [] res binds locals wanteds
1178 = return (res, binds, locals, wanteds)
1180 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1181 res binds locals wanteds
1182 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
1184 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1185 tySubst = zipOpenTvSubst [tv] [ty]
1186 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1187 ; res' <- mapM (substEq eq coSubst tySubst) res
1189 -- only susbtitute local equalities into local dictionaries
1190 ; (lbinds, locals') <- if not (isWantedCo co)
1193 (substDict eq coSubst tySubst False)
1198 -- flexible tvs in wanteds will be instantiated anyway, there is
1199 -- no need to substitute them into dictionaries
1200 ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
1203 (substDict eq coSubst tySubst True)
1206 return ([], wanteds)
1208 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1209 ; subst eqs' (eq:res') binds' locals' wanteds'
1211 subst (eq:eqs) res binds locals wanteds
1212 = subst eqs (eq:res) binds locals wanteds
1214 -- We have, co :: tv ~ ty
1215 -- => apply [ty/tv] to right-hand side of eq2
1216 -- (but only if tv actually occurs in the right-hand side of eq2)
1217 substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1219 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1220 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1221 right2' = substTy tySubst (rwi_right eq2)
1223 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1224 RewriteFam {rwi_fam = fam,
1225 rwi_args = args} ->mkTyConApp fam args
1226 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1228 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1229 -> occurCheckErr left2 right2'
1230 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1237 -- We have, co :: tv ~ ty
1238 -- => apply [ty/tv] to dictionary predicate
1239 -- (but only if tv actually occurs in the predicate)
1240 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1242 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1243 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1244 pred' = substPred tySubst (tci_pred dict)
1245 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1246 ; return (binds, dict')
1250 substDict _ _ _ _ dict
1251 = return (emptyBag, dict)
1252 -- !!!TODO: Still need to substitute into IP constraints.
1255 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1256 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1257 Return all remaining wanted equalities. The Boolean result component is True
1258 if at least one instantiation of a flexible that is *not* a skolem from
1259 flattening was performed.
1261 We need to instantiate all flexibles that arose as skolems during flattening
1262 of wanteds before we instantiate any other flexibles. Consider F delta ~
1263 alpha, F alpha ~ delta, where alpha is a skolem and delta a free flexible. We
1264 need to produce F (F delta) ~ delta (and not F (F alpha) ~ alpha). Otherwise,
1265 we may wrongly claim to having performed an improvement, which can lead to
1266 non-termination of the combined class-family solver.
1269 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
1270 instantiateAndExtract eqs localsEmpty skolems
1271 = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
1272 4 (ppr eqs $$ ppr skolems)
1273 -- start by *only* instantiating skolem flexibles from flattening
1274 ; unflat_wanteds <- liftM catMaybes $
1275 mapM (inst (`elemVarSet` skolems)) wanteds
1276 -- only afterwards instantiate free flexibles
1277 ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds
1278 ; let improvement = length residuals < length unflat_wanteds
1279 ; residuals' <- mapM rewriteInstToInst residuals
1280 ; return (residuals', improvement)
1283 wanteds = filter (isWantedCo . rwi_co) eqs
1284 checkingMode = length eqs > length wanteds || not localsEmpty
1285 -- no local equalities or dicts => checking mode
1287 -- co :: alpha ~ t or co :: a ~ alpha
1288 inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1289 = do { flexi_tv1 <- isFlexible mayInst tv1
1290 ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2
1291 ; case (flexi_tv1, maybe_flexi_tv2) of
1293 -> -- co :: alpha ~ t
1294 doInst (rwi_swapped eq) tv1 ty2 co eq
1296 -> -- co :: a ~ alpha
1297 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1298 _ -> return $ Just eq
1301 -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
1302 inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1303 rwi_right = ty2, rwi_co = co})
1304 | Just tv2 <- tcGetTyVar_maybe ty2
1306 , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
1307 -- !!!FIXME: this is too liberal, even if tv2 is in
1308 -- skolems we shouldn't instantiate if tvs occurs
1309 -- in other equalities that may propagate it into the
1311 = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1313 inst _mayInst eq = return $ Just eq
1315 -- tv is a meta var and not filled
1316 isFlexible mayInst tv
1317 | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
1318 | otherwise = return False
1320 -- type is a tv that is a meta var and not filled
1321 isFlexibleTy mayInst ty
1322 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst tv
1323 ; if flexi then return $ Just tv
1326 | otherwise = return Nothing
1328 doInst _swapped _tv _ty (Right ty) _eq
1329 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1330 doInst swapped tv ty (Left cotv) eq
1331 = do { lookupTV <- lookupTcTyVar tv
1332 ; uMeta swapped tv lookupTV ty cotv
1335 -- Try to fill in a meta variable. There is *no* need to consider
1336 -- reorienting the underlying equality; `checkOrientation' makes sure
1337 -- that we get variable-variable equalities only in the appropriate
1340 uMeta :: Bool -- is this a swapped equality?
1341 -> TcTyVar -- tyvar to instantiate
1342 -> LookupTyVarResult -- lookup result of that tyvar
1343 -> TcType -- to to instantiate tyvar with
1344 -> TcTyVar -- coercion tyvar of current equality
1345 -> TcM (Maybe RewriteInst) -- returns the original equality if
1346 -- the tyvar could not be instantiated,
1347 -- and hence, the equality must be kept
1349 -- meta variable has been filled already
1350 -- => keep the equality
1351 uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1353 ptext (sLit "flexible") <+> ppr tv <+>
1354 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1355 ptext (sLit "meant to fill with") <+> ppr ty
1360 -- => cannot update (retain the equality)!
1361 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1364 -- type variable meets type variable
1365 -- => `checkOrientation' already ensures that it is fine to instantiate
1366 -- tv1 with tv2, but chase tv2's instantiations if necessary
1367 -- NB: tv's instantiations won't alter the orientation in which we
1368 -- want to instantiate as they either constitute a family
1369 -- application or are themselves due to a properly oriented
1371 uMeta swapped tv1 details1@(DoneTv (MetaTv _ ref)) ty@(TyVarTy tv2) cotv
1372 = do { lookupTV2 <- lookupTcTyVar tv2
1375 uMeta swapped tv1 details1 ty' cotv
1377 uMetaInst swapped tv1 ref ty cotv
1380 -- updatable meta variable meets non-variable type
1381 -- => occurs check, monotype check, and kinds match check, then update
1382 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1383 = uMetaInst swapped tv ref non_tv_ty cotv
1385 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1387 -- We know `tv' can be instantiated; check that `ty' is alright for
1388 -- instantiating `tv' with and then do it; otherwise, return the original
1390 uMetaInst swapped tv ref ty cotv
1391 = do { -- occurs + monotype check
1392 ; mb_ty' <- checkTauTvUpdate tv ty
1396 -- there may be a family in non_tv_ty due to an unzonked,
1397 -- but updated skolem for a local equality
1400 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1401 ; writeMetaTyVar cotv ty' -- update co var
1408 %************************************************************************
1412 %************************************************************************
1414 The infamous couldn't match expected type soandso against inferred type
1415 somethingdifferent message.
1418 eqInstMisMatch :: Inst -> TcM a
1420 = ASSERT( isEqInst inst )
1421 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1423 (ty_act, ty_exp) = eqInstTys inst
1424 InstLoc _ _ ctxt = instLoc inst
1426 -----------------------
1427 failWithMisMatch :: TcType -> TcType -> TcM a
1428 -- Generate the message when two types fail to match,
1429 -- going to some trouble to make it helpful.
1430 -- The argument order is: actual type, expected type
1431 failWithMisMatch ty_act ty_exp
1432 = do { env0 <- tcInitTidyEnv
1433 ; ty_exp <- zonkTcType ty_exp
1434 ; ty_act <- zonkTcType ty_act
1435 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1438 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1439 misMatchMsg env0 (ty_act, ty_exp)
1440 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1441 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1442 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1444 ptext (sLit "against inferred type") <+> pp_act],
1445 nest 2 (extra_exp $$ extra_act)]
1450 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1452 = let (env1, tidy_ty) = tidyOpenType env ty
1453 (env2, extra) = ppr_extra env1 tidy_ty
1455 (env2, quotes (ppr tidy_ty), extra)
1457 -- (ppr_extra env ty) shows extra info about 'ty'
1458 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1459 ppr_extra env (TyVarTy tv)
1460 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1461 = (env1, pprSkolTvBinding tv1)
1463 (env1, tv1) = tidySkolemTyVar env tv
1465 ppr_extra env _ty = (env, empty) -- Normal case
1468 Warn of loopy local equalities that were dropped.
1471 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1472 warnDroppingLoopyEquality ty1 ty2
1473 = do { env0 <- tcInitTidyEnv
1474 ; ty1 <- zonkTcType ty1
1475 ; ty2 <- zonkTcType ty2
1476 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1477 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1478 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1479 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))