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(..) )
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 %************************************************************************
201 Given a set of given, local constraints and a set of wanted constraints,
202 simplify the wanted equalities as far as possible and normalise both local and
203 wanted dictionaries with respect to the equalities.
205 In addition to the normalised local dictionaries and simplified wanteds, the
206 function yields bindings for instantiated meta variables (due to solving
207 equality constraints) and dictionary bindings (due to simplifying class
208 constraints). The bag of type variable bindings only contains bindings for
209 non-local variables - i.e., type variables other than those newly created by
210 the present function. Consequently, type improvement took place iff the bag
211 of bindings contains any bindings for proper type variables (not just covars).
212 The solver does not instantiate any non-local variables; i.e., the bindings
213 must be executed by the caller.
215 All incoming constraints are assumed to be zonked already. All outgoing
216 constraints will be zonked again.
218 NB: The solver only has local effects that cannot be observed from outside.
219 In particular, it can be executed twice on the same constraint set with
220 the same result (modulo generated variables names).
223 tcReduceEqs :: [Inst] -- locals
225 -> TcM ([Inst], -- normalised locals (w/o equalities)
226 [Inst], -- normalised wanteds (including equalities)
227 TcTyVarBinds, -- bindings for meta type variables
228 TcDictBinds) -- bindings for all simplified dictionaries
229 tcReduceEqs locals wanteds
230 = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
231 do { let (local_eqs , local_dicts) = partition isEqInst locals
232 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
233 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
234 ; eqCfg2 <- normaliseDicts False local_dicts
235 ; eqCfg3 <- normaliseDicts True wanteds_dicts
236 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig`
237 eqCfg2 `unionEqConfig`
239 ; finaliseEqsAndDicts freeFlexibles eqCfg
241 -- execute type bindings of skolem flexibles...
242 ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
243 -- ...and zonk the constraints to propagate the bindings
244 ; locals_z <- zonkInsts locals
245 ; wanteds_z <- zonkInsts wanteds
246 ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
249 -- unification variables that appear in the environment and may not be
250 -- instantiated - this includes coercion variables
251 freeFlexibles = tcTyVarsOfInsts locals `unionVarSet`
252 tcTyVarsOfInsts wanteds
254 pruneTyBinds tybinds freeFlexibles
255 = do { let tybinds' = bagToList tybinds
256 (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
257 ; execTcTyVarBinds (listToBag skolem_tybinds)
258 ; return $ listToBag env_tybinds
261 isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
265 %************************************************************************
267 Equality Configurations
269 %************************************************************************
271 We maintain normalised equalities together with the skolems introduced as
272 intermediates during flattening of equalities as well as
275 -- |Configuration of normalised equalities used during solving.
277 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
278 , locals :: [Inst] -- given dicts
279 , wanteds :: [Inst] -- wanted dicts
280 , binds :: TcDictBinds -- bindings
283 addEq :: EqConfig -> RewriteInst -> EqConfig
284 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
286 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
287 unionEqConfig eqc1 eqc2 = EqConfig
288 { eqs = eqs eqc1 ++ eqs eqc2
289 , locals = locals eqc1 ++ locals eqc2
290 , wanteds = wanteds eqc1 ++ wanteds eqc2
291 , binds = binds eqc1 `unionBags` binds eqc2
294 emptyEqConfig :: EqConfig
295 emptyEqConfig = EqConfig
302 instance Outputable EqConfig where
303 ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
304 = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
307 The set of operations on an equality configuration. We obtain the initialise
308 configuration by normalisation ('normaliseEqs'), solve the equalities by
309 propagation ('propagateEqs'), and eventually finalise the configuration when
310 no further propoagation is possible.
313 -- |Turn a set of equalities into an equality configuration for solving.
315 -- Precondition: The Insts are zonked.
317 normaliseEqs :: [Inst] -> TcM EqConfig
319 = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )
320 ; traceTc $ ptext (sLit "Entering normaliseEqs")
322 ; eqss <- mapM normEqInst eqs
323 ; return $ emptyEqConfig { eqs = concat eqss }
326 -- |Flatten the type arguments of all dictionaries, returning the result as a
327 -- equality configuration. The dictionaries go into the 'wanted' component if
328 -- the second argument is 'True'.
330 -- Precondition: The Insts are zonked.
332 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
333 normaliseDicts isWanted insts
334 = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
335 ptext (if isWanted then sLit "[Wanted] for"
336 else sLit "[Local] for"))
339 ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
341 ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
342 4 (ppr insts' $$ ppr eqss)
343 ; return $ emptyEqConfig { eqs = concat eqss
344 , locals = if isWanted then [] else insts'
345 , wanteds = if isWanted then insts' else []
346 , binds = unionManyBags bindss
350 -- |Solves the equalities as far as possible by applying propagation rules.
352 propagateEqs :: EqConfig -> TcM EqConfig
353 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
354 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
357 ; propagate todoEqs (eqCfg {eqs = []})
360 -- |Finalise a set of equalities and associated dictionaries after
361 -- propagation. The first returned set of instances are the locals (without
362 -- equalities) and the second set are all residual wanteds, including
363 -- equalities. In addition, we return all generated dictionary bindings.
365 finaliseEqsAndDicts :: TcTyVarSet -> EqConfig
366 -> TcM ([Inst], [Inst], TcDictBinds)
367 finaliseEqsAndDicts freeFlexibles (EqConfig { eqs = eqs
372 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
374 ; (eqs', subst_binds, locals', wanteds')
375 <- substitute eqs locals wanteds checkingMode freeFlexibles
376 ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
377 ; let final_binds = subst_binds `unionBags` binds
379 -- Assert that all cotvs of wanted equalities are still unfilled, and
380 -- zonk all final insts, to make any improvement visible
381 ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
382 ; zonked_locals <- zonkInsts locals'
383 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
384 ; return (zonked_locals, zonked_wanteds, final_binds)
387 checkingMode = length eqs > length wanteds || not (null locals)
388 -- no local equalities or dicts => checking mode
392 %************************************************************************
394 Normalisation of equalities
396 %************************************************************************
398 A normal equality is a properly oriented equality with associated coercion
399 that contains at most one family equality (in its left-hand side) is oriented
400 such that it may be used as a rewrite rule. It has one of the following two
403 (1) co :: F t1..tn ~ t (family equalities)
404 (2) co :: x ~ t (variable equalities)
406 Variable equalities fall again in two classes:
408 (2a) co :: x ~ t, where t is *not* a variable, or
409 (2b) co :: x ~ y, where x > y.
411 The types t, t1, ..., tn may not contain any occurrences of synonym
412 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
413 the right-hand side, and the relation x > y is an (nearly) arbitrary, but
414 total order on type variables. The only restriction that we impose on that
415 order is that for x > y, we are happy to instantiate x with y taking into
416 account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
420 = RewriteVar -- Form (2) above
421 { rwi_var :: TyVar -- may be rigid or flexible
422 , rwi_right :: TcType -- contains no synonym family applications
423 , rwi_co :: EqInstCo -- the wanted or given coercion
425 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
426 , rwi_swapped :: Bool -- swapped orientation of original EqInst
428 | RewriteFam -- Forms (1) above
429 { rwi_fam :: TyCon -- synonym family tycon
430 , rwi_args :: [Type] -- contain no synonym family applications
431 , rwi_right :: TcType -- contains no synonym family applications
432 , rwi_co :: EqInstCo -- the wanted or given coercion
434 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
435 , rwi_swapped :: Bool -- swapped orientation of original EqInst
438 isWantedRewriteInst :: RewriteInst -> Bool
439 isWantedRewriteInst = isWantedCo . rwi_co
441 isRewriteVar :: RewriteInst -> Bool
442 isRewriteVar (RewriteVar {}) = True
443 isRewriteVar _ = False
445 tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
446 tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
447 = unitVarSet tv `unionVarSet` tyVarsOfType ty
448 tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
449 = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
451 rewriteInstToInst :: RewriteInst -> TcM Inst
452 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
453 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
454 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
455 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
457 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
460 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
461 deriveEqInst rewrite ty1 ty2 co
462 = do { co_adjusted <- if not swapped then return co
463 else mkSymEqInstCo co (ty2, ty1)
467 , tci_co = co_adjusted
468 , tci_loc = rwi_loc rewrite
469 , tci_name = rwi_name rewrite
473 swapped = rwi_swapped rewrite
474 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
476 instance Outputable RewriteInst where
477 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
478 = hsep [ pprEqInstCo co <+> text "::"
479 , ppr (mkTyConApp fam args)
483 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
484 = hsep [ pprEqInstCo co <+> text "::"
490 pprEqInstCo :: EqInstCo -> SDoc
491 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
492 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
495 The following functions turn an arbitrary equality into a set of normal
496 equalities. This implements the WFlat and LFlat rules of the paper in one
497 sweep. However, we use flexible variables for both locals and wanteds, and
498 avoid to carry around the unflattening substitution \Sigma (for locals) by
499 already updating the skolems for locals with the family application that they
500 represent - i.e., they will turn into that family application on the next
501 zonking (which only happens after finalisation).
503 In a corresponding manner, normDict normalises class dictionaries by
504 extracting any synonym family applications and generation appropriate normal
507 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
508 we drop that equality and raise an error if it is a wanted or a warning if it
512 normEqInst :: Inst -> TcM [RewriteInst]
513 -- Normalise one equality.
515 = ASSERT( isEqInst inst )
516 do { traceTc $ ptext (sLit "normEqInst of ") <+>
517 pprEqInstCo co <+> text "::" <+>
518 ppr ty1 <+> text "~" <+> ppr ty2
519 ; res <- go ty1 ty2 co
521 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
525 (ty1, ty2) = eqInstTys inst
526 co = eqInstCoercion inst
528 -- look through synonyms
529 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
530 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
532 -- left-to-right rule with type family head
533 go ty1@(TyConApp con args) ty2 co
534 | isOpenSynTyConApp ty1 -- only if not oversaturated
535 = mkRewriteFam False con args ty2 co
537 -- right-to-left rule with type family head
538 go ty1 ty2@(TyConApp con args) co
539 | isOpenSynTyConApp ty2 -- only if not oversaturated
540 = do { co' <- mkSymEqInstCo co (ty2, ty1)
541 ; mkRewriteFam True con args ty1 co'
544 -- no outermost family
546 = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
547 ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
548 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
549 sym_co2 = mkSymCoercion co2
551 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
552 ; eqs <- checkOrientation ty1' ty2' co' inst
553 ; if isLoopyEquality eqs ty12_eqs'
554 then do { if isWantedCo (tci_co inst)
556 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
559 warnDroppingLoopyEquality ty1 ty2
560 ; return ([]) -- drop the equality
563 return (eqs ++ ty12_eqs')
566 mkRewriteFam swapped con args ty2 co
567 = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
568 ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
569 ; let co1 = mkTyConApp con cargs
570 sym_co2 = mkSymCoercion co2
571 all_eqs = concat args_eqss ++ ty2_eqs
572 eqTys = (mkTyConApp con args', ty2')
573 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
574 ; let thisRewriteFam = RewriteFam
579 , rwi_loc = tci_loc inst
580 , rwi_name = tci_name inst
581 , rwi_swapped = swapped
583 ; return $ thisRewriteFam : all_eqs'
586 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
587 -- have a variable equality with 'a' on the lhs as the first equality.
588 -- Then, check whether 'a' occurs in the lhs of any family equality
589 -- generated by flattening.
590 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
592 inRewriteFam (RewriteFam {rwi_args = args})
593 = tv `elemVarSet` tyVarsOfTypes args
594 inRewriteFam _ = False
595 isLoopyEquality _ _ = False
597 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
598 -- Normalise one dictionary or IP constraint.
599 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
600 = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
601 ; let rewriteCo = PredTy $ ClassP clas cargs
602 eqs = concat args_eqss
603 pred' = ClassP clas args'
605 then -- don't generate a binding if there is nothing to flatten
606 return (inst, [], emptyBag)
608 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
609 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
610 ; return (inst', eqs', bind)
612 normDict _isWanted inst
613 = return (inst, [], emptyBag)
614 -- !!!TODO: Still need to normalise IP constraints.
616 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
617 -- Performs the occurs check, decomposition, and proper orientation
618 -- (returns a singleton, or an empty list in case of a trivial equality)
619 -- NB: We cannot assume that the two types already have outermost type
620 -- synonyms expanded due to the recursion in the case of type applications.
621 checkOrientation ty1 ty2 co inst
624 -- look through synonyms
625 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
626 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
628 -- identical types => trivial
631 = do { mkIdEqInstCo co ty1
635 -- two tvs (distinct tvs, due to previous equation)
636 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
637 = do { isBigger <- tv1 `tvIsBigger` tv2
638 ; if isBigger -- left greater
639 then mkRewriteVar False tv1 ty2 co -- => unchanged
640 else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater
641 ; mkRewriteVar True tv2 ty1 co' -- => swap
645 -- only lhs is a tv => unchanged
646 go ty1@(TyVarTy tv1) ty2
647 | ty1 `tcPartOfType` ty2 -- occurs check!
648 = occurCheckErr ty1 ty2
650 = mkRewriteVar False tv1 ty2 co
652 -- only rhs is a tv => swap
653 go ty1 ty2@(TyVarTy tv2)
654 | ty2 `tcPartOfType` ty1 -- occurs check!
655 = occurCheckErr ty2 ty1
657 = do { co' <- mkSymEqInstCo co (ty2, ty1)
658 ; mkRewriteVar True tv2 ty1 co'
661 -- data type constructor application => decompose
662 -- NB: Special cased for efficiency - could be handled as type application
663 go (TyConApp con1 args1) (TyConApp con2 args2)
665 && isInjectiveTyCon con1 -- don't match family synonym apps
666 = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
667 ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
669 ; return $ concat eqss
672 -- function type => decompose
673 -- NB: Special cased for efficiency - could be handled as type application
674 go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
675 = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
676 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
677 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
678 ; return $ eqs_l ++ eqs_r
681 -- type applications => decompose
683 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
684 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
685 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
686 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
687 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
688 ; return $ eqs_l ++ eqs_r
691 -- inconsistency => type error
693 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
696 mkRewriteVar swapped tv ty co = return [RewriteVar
700 , rwi_loc = tci_loc inst
701 , rwi_name = tci_name inst
702 , rwi_swapped = swapped
705 -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
706 tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
708 = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
710 isBigger tv1 (SkolemTv _) tv2 (SkolemTv _)
712 isBigger _ (MetaTv _ _) _ (SkolemTv _)
714 isBigger _ (SkolemTv _) _ (MetaTv _ _)
716 isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
717 -- meta variable meets meta variable
718 -- => be clever about which of the two to update
719 -- (from TcUnify.uUnfilledVars minus boxy stuff)
720 = case (info1, info2) of
721 -- Avoid SigTvs if poss
722 (SigTv _, SigTv _) -> return $ tv1 > tv2
723 (SigTv _, _ ) | k1_sub_k2 -> return False
724 (_, SigTv _) | k2_sub_k1 -> return True
729 -> case (nicer_to_update tv1, nicer_to_update tv2) of
730 (True, False) -> return True
731 (False, True) -> return False
732 _ -> return $ tv1 > tv2
733 | k1_sub_k2 -> return False
734 | k2_sub_k1 -> return True
735 | otherwise -> kind_err >> return True
736 -- Update the variable with least kind info
737 -- See notes on type inference in Kind.lhs
738 -- The "nicer to" part only applies if the two kinds are the same,
739 -- so we can choose which to do.
741 kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
742 unifyKindMisMatch k1 k2
746 k1_sub_k2 = k1 `isSubKind` k2
747 k2_sub_k1 = k2 `isSubKind` k1
749 nicer_to_update tv = isSystemName (Var.varName tv)
750 -- Try to update sys-y type variables in preference to ones
751 -- gotten (say) by instantiating a polymorphic function with
752 -- a user-written type sig
754 flattenType :: Inst -- context to get location & name
755 -> Type -- the type to flatten
756 -> TcM (Type, -- the flattened type
757 Coercion, -- coercion witness of flattening wanteds
758 [RewriteInst]) -- extra equalities
759 -- Removes all family synonyms from a type by moving them into extra equalities
760 flattenType inst ty = go ty
762 -- look through synonyms
763 go ty | Just ty' <- tcView ty
764 = do { (ty_flat, co, eqs) <- go ty'
766 then -- unchanged, keep the old type with folded synonyms
769 return (ty_flat, co, eqs)
772 -- type variable => nothing to do
774 = return (ty, ty, [])
776 -- type family application & family arity matches number of args
777 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
778 go ty@(TyConApp con args)
779 | isOpenSynTyConApp ty -- only if not oversaturated
780 = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
781 ; alpha <- newFlexiTyVar (typeKind ty)
782 ; let alphaTy = mkTyVarTy alpha
783 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
784 ; let thisRewriteFam = RewriteFam
787 , rwi_right = alphaTy
788 , rwi_co = mkWantedCo cotv
789 , rwi_loc = tci_loc inst
790 , rwi_name = tci_name inst
794 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
795 thisRewriteFam : concat args_eqss)
798 -- data constructor application => flatten subtypes
799 -- NB: Special cased for efficiency - could be handled as type application
800 go ty@(TyConApp con args)
801 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
802 = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
804 then -- unchanged, keep the old type with folded synonyms
807 return (mkTyConApp con args',
808 mkTyConApp con cargs,
812 -- function type => flatten subtypes
813 -- NB: Special cased for efficiency - could be handled as type application
814 go ty@(FunTy ty_l ty_r)
815 = do { (ty_l', co_l, eqs_l) <- go ty_l
816 ; (ty_r', co_r, eqs_r) <- go ty_r
817 ; if null eqs_l && null eqs_r
818 then -- unchanged, keep the old type with folded synonyms
821 return (mkFunTy ty_l' ty_r',
826 -- type application => flatten subtypes
828 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
829 -- need to use the smart split as ty may be an
830 -- oversaturated family application
831 = do { (ty_l', co_l, eqs_l) <- go ty_l
832 ; (ty_r', co_r, eqs_r) <- go ty_r
833 ; if null eqs_l && null eqs_r
834 then -- unchanged, keep the old type with folded synonyms
837 return (mkAppTy ty_l' ty_r',
842 -- forall type => panic if the body contains a type family
843 -- !!!TODO: As long as the family does not contain a quantified variable
844 -- we might pull it out, but what if it does contain a quantified
846 go ty@(ForAllTy _ body)
847 | null (tyFamInsts body)
848 = return (ty, ty, [])
850 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
852 -- we should never see a predicate type
854 = panic "TcTyFuns.flattenType: unexpected PredType"
856 go _ = panic "TcTyFuns: suppress bogus warning"
858 adjustCoercions :: EqInstCo -- coercion of original equality
859 -> Coercion -- coercion witnessing the left rewrite
860 -> Coercion -- coercion witnessing the right rewrite
861 -> (Type, Type) -- types of flattened equality
862 -> [RewriteInst] -- equalities from flattening
863 -> TcM (EqInstCo, -- coercion for flattened equality
864 [RewriteInst]) -- final equalities from flattening
865 -- Depending on whether we flattened a local or wanted equality, that equality's
866 -- coercion and that of the new equalities produced during flattening are
868 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
869 -- wanted => generate a fresh coercion variable for the flattened equality
870 = do { cotv' <- newMetaCoVar ty_l ty_r
871 ; bindMetaTyVar cotv $
872 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
873 ; return (Left cotv', all_eqs)
876 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
877 -- local => turn all new equalities into locals and update (but not zonk)
879 = do { all_eqs' <- mapM wantedToLocal all_eqs
880 ; return (co, all_eqs')
883 mkDictBind :: Inst -- original instance
884 -> Bool -- is this a wanted contraint?
885 -> Coercion -- coercion witnessing the rewrite
886 -> PredType -- coerced predicate
887 -> TcM (Inst, -- new inst
888 TcDictBinds) -- binding for coerced dictionary
889 mkDictBind dict isWanted rewriteCo pred
890 = do { dict' <- newDictBndr loc pred
891 -- relate the old inst to the new one
892 -- target_dict = source_dict `cast` st_co
893 ; let (target_dict, source_dict, st_co)
894 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
895 | otherwise = (dict', dict, rewriteCo)
897 -- co :: dict ~ dict'
898 -- hence, if isWanted
899 -- dict = dict' `cast` sym co
901 -- dict' = dict `cast` co
902 expr = HsVar $ instToId source_dict
903 cast_expr = HsWrap (WpCast st_co) expr
904 rhs = L (instLocSpan loc) cast_expr
905 binds = instToDictBind target_dict rhs
906 ; return (dict', binds)
911 -- gamma ::^l Fam args ~ alpha
912 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
913 -- (the update of alpha will not be apparent during propagation, as we
914 -- never follow the indirections of meta variables; it will be revealed
915 -- when the equality is zonked)
917 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
918 -- have escaped into some other coercions during normalisation.
920 -- We do actually update alpha and gamma by side effect (instead of
921 -- only remembering the binding with `bindMetaTyVar', as we do for all
922 -- other tyvars). We can do this as the side effects are strictly
923 -- *local*; we know that both alpha and gamma were just a moment ago
924 -- introduced by normalisation.
926 wantedToLocal :: RewriteInst -> TcM RewriteInst
927 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
929 rwi_right = TyVarTy alpha,
930 rwi_co = Left gamma})
931 = do { writeMetaTyVar alpha (mkTyConApp fam args)
932 ; writeMetaTyVar gamma (mkTyConApp fam args)
933 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
935 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
939 %************************************************************************
941 Propagation of equalities
943 %************************************************************************
945 Apply the propagation rules exhaustively.
948 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
949 propagate [] eqCfg = return eqCfg
950 propagate (eq:eqs) eqCfg
951 = do { optEqs <- applyTop eq
954 -- Top applied to 'eq' => retry with new equalities
955 Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
957 -- Top doesn't apply => try subst rules with all other
958 -- equalities, after that 'eq' can go into the residual list
959 Nothing -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
960 ; propagate eqs' (eqCfg' `addEq` eq)
964 applySubstRules :: RewriteInst -- currently considered eq
965 -> [RewriteInst] -- todo eqs list
966 -> EqConfig -- residual
967 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
968 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
969 = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
970 ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
971 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
972 eqConfig {eqs = unchangedEqs_r})
975 mapSubstRules :: RewriteInst -- try substituting this equality
976 -> [RewriteInst] -- into these equalities
977 -> TcM ([RewriteInst], [RewriteInst])
979 = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
980 ; return (concat newEqss, concat unchangedEqss)
984 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
985 4 (ppr eq1 $$ ppr eq2)
987 -- try the SubstFam rule
988 ; optEqs <- applySubstFam eq1 eq2
990 Just eqs -> return (eqs, [])
992 { -- try the SubstVarVar rule
993 optEqs <- applySubstVarVar eq1 eq2
995 Just eqs -> return (eqs, [])
997 { -- try the SubstVarFam rule
998 optEqs <- applySubstVarFam eq1 eq2
1000 Just eq -> return ([eq], [])
1001 Nothing -> return ([], [eq2])
1002 -- if no rule matches, we return the equlity we tried to
1003 -- substitute into unchanged
1007 Attempt to apply the Top rule. The rule is
1011 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
1013 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
1015 Returns Nothing if the rule could not be applied. Otherwise, the resulting
1016 equality is normalised and a list of the normal equalities is returned.
1019 applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1021 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
1022 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
1024 Nothing -> return Nothing
1025 Just (lhs, rewrite_co)
1026 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1027 ; eq' <- deriveEqInst eq lhs rhs co'
1028 ; liftM Just $ normEqInst eq'
1035 applyTop _ = return Nothing
1038 Attempt to apply the SubstFam rule. The rule is
1040 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
1042 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1044 where co1 may be a wanted only if co2 is a wanted, too.
1046 Returns Nothing if the rule could not be applied. Otherwise, the equality
1047 co2' is normalised and a list of the normal equalities is returned. (The
1048 equality co1 is not returned as it remain unaltered.)
1051 applySubstFam :: RewriteInst
1053 -> TcM (Maybe ([RewriteInst]))
1054 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1055 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1057 -- rule matches => rewrite
1058 | fam1 == fam2 && tcEqTypes args1 args2 &&
1059 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1060 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1061 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1062 ; liftM Just $ normEqInst eq2'
1065 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1066 | fam1 == fam2 && tcEqTypes args1 args2 &&
1067 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1068 = return $ Just [eq2]
1073 co1 = eqInstCoType (rwi_co eq1)
1076 applySubstFam _ _ = return Nothing
1079 Attempt to apply the SubstVarVar rule. The rule is
1081 co1 :: x ~ t & co2 :: x ~ s
1083 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1085 where co1 may be a wanted only if co2 is a wanted, too.
1087 Returns Nothing if the rule could not be applied. Otherwise, the equality
1088 co2' is normalised and a list of the normal equalities is returned. (The
1089 equality co1 is not returned as it remain unaltered.)
1092 applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1093 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1094 eq2@(RewriteVar {rwi_var = tv2})
1096 -- rule matches => rewrite
1098 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1099 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1100 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1101 ; liftM Just $ normEqInst eq2'
1104 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1106 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1107 = return $ Just [eq2]
1112 co1 = eqInstCoType (rwi_co eq1)
1115 applySubstVarVar _ _ = return Nothing
1118 Attempt to apply the SubstVarFam rule. The rule is
1120 co1 :: x ~ t & co2 :: F s1..sn ~ s
1122 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1123 with co2 = [co1/x](F s1..sn) |> co2'
1125 where x occurs in F s1..sn. (co1 may be local or wanted.)
1127 Returns Nothing if the rule could not be applied. Otherwise, the equality
1128 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1131 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1133 -- rule matches => rewrite
1134 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1135 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1136 | tv1 `elemVarSet` tyVarsOfTypes args2
1137 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1138 args2' = substTysWith [tv1] [rhs1] args2
1139 lhs2 = mkTyConApp fam2 args2'
1140 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1141 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1144 rhs1 = rwi_right eq1
1145 rhs2 = rwi_right eq2
1146 co1 = eqInstCoType (rwi_co eq1)
1149 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1150 applySubstVarFam (RewriteFam {rwi_args = args1})
1151 eq2@(RewriteVar {rwi_var = tv2})
1152 | tv2 `elemVarSet` tyVarsOfTypes args1
1155 applySubstVarFam _ _ = return Nothing
1159 %************************************************************************
1161 Finalisation of equalities
1163 %************************************************************************
1165 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1166 (both local and wanted) into the right-hand sides of all other equalities and
1167 of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
1168 other *family* equalities. This may lead to recursive equalities; i.e., (1)
1169 we need to apply the substitution implied by one equality exhaustively before
1170 turning to the next and (2) we need an occurs check.
1172 We also apply the same substitutions to the local and wanted class and IP
1175 We perform the substitutions in two steps:
1177 Step A: Substitute variable equalities into the right-hand sides of all
1178 other equalities (but wanted only into wanteds) and into class and IP
1179 constraints (again wanteds only into wanteds).
1181 Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
1182 'alpha' is a skolem flexible (i.e., not free in the environment),
1183 into the right-hand sides of all wanted variable equalities and into
1184 both sides of all wanted family equalities.
1186 Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
1187 alpha' into the right-hand sides of all wanted variable equalities
1188 and into both sides of all wanted family equalities.
1190 In inference mode, we do not substitute into variable equalities in Steps B & C.
1192 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1193 substitute variable equalities first; e.g., consider
1195 F s ~ alpha, alpha ~ t
1197 If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1198 This would be bad as `F s' is less useful, eg, as an argument to a class
1201 The restriction on substituting locals is necessary due to examples, such as
1203 F delta ~ alpha, F alpha ~ delta,
1205 where `alpha' is a skolem flexible and `delta' a environment flexible. We need
1206 to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
1207 we may wrongly claim to having performed an improvement, which can lead to
1208 non-termination of the combined class-family solver.
1210 We do also substitute flexibles, as in `alpha ~ t' into class constraints.
1211 When `alpha' is later instantiated, we'd get the same effect, but in the
1212 meantime the class constraint would miss some information, which would be a
1213 problem in an integrated equality-class solver.
1216 * Given that we apply the substitution corresponding to a single equality
1217 exhaustively, before turning to the next, and because we eliminate recursive
1218 equalities, all opportunities for subtitution will have been exhausted after
1219 we have considered each equality once.
1222 substitute :: [RewriteInst] -- equalities
1223 -> [Inst] -- local class dictionaries
1224 -> [Inst] -- wanted class dictionaries
1225 -> Bool -- True ~ checking mode; False ~ inference
1226 -> TyVarSet -- flexibles free in the environment
1227 -> TcM ([RewriteInst], -- equalities after substitution
1228 TcDictBinds, -- all newly generated dictionary bindings
1229 [Inst], -- local dictionaries after substitution
1230 [Inst]) -- wanted dictionaries after substitution
1231 substitute eqs locals wanteds checkingMode freeFlexibles
1232 = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
1233 -- sorting the equalities appropriately: first all variable, then all
1234 -- family/skolem, and then the remaining family equalities.
1235 let (var_eqs, fam_eqs) = partition isRewriteVar eqs
1236 (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
1238 subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1240 isFamSkolemEq (RewriteFam {rwi_right = ty})
1241 | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
1242 isFamSkolemEq _ = False
1244 subst [] res binds locals wanteds
1245 = return (res, binds, locals, wanteds)
1248 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1249 res binds locals wanteds
1250 = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
1253 -- create the substitution
1254 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1255 tySubst = zipOpenTvSubst [tv] [ty]
1257 -- substitute into all other equalities
1258 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1259 ; res' <- mapM (substEq eq coSubst tySubst) res
1261 -- only substitute local equalities into local dictionaries
1262 ; (lbinds, locals') <- if not (isWantedCo co)
1265 (substDict eq coSubst tySubst False)
1270 -- substitute all equalities into wanteds dictionaries
1271 ; (wbinds, wanteds') <- mapAndUnzipM
1272 (substDict eq coSubst tySubst True)
1275 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1276 ; subst eqs' (eq:res') binds' locals' wanteds'
1279 -- co ::^w F t1..tn ~ alpha
1280 subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
1282 res binds locals wanteds
1283 | Just tv <- tcGetTyVar_maybe ty
1286 = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
1289 -- create the substitution
1290 ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
1291 tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
1293 -- substitute into other wanted equalities (`substEq' makes sure
1294 -- that we only substitute into wanteds)
1295 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1296 ; res' <- mapM (substEq eq coSubst tySubst) res
1298 ; subst eqs' (eq:res') binds locals wanteds
1301 subst (eq:eqs) res binds locals wanteds
1302 = subst eqs (eq:res) binds locals wanteds
1304 -- We have, co :: tv ~ ty
1305 -- => apply [ty/tv] to right-hand side of eq2
1306 -- (but only if tv actually occurs in the right-hand side of eq2
1307 -- and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
1308 substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1310 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1311 && (isWantedRewriteInst eq2 || not (isWantedCo co))
1312 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1313 right2' = substTy tySubst (rwi_right eq2)
1315 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1316 RewriteFam {rwi_fam = fam,
1317 rwi_args = args} ->mkTyConApp fam args
1318 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1320 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1321 -> occurCheckErr left2 right2'
1322 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1325 -- We have, co ::^w F t1..tn ~ tv
1326 -- => apply [F t1..tn/tv] to eq2
1327 -- (but only if tv actually occurs in eq2
1328 -- and eq2 is a wanted equality
1329 -- and we are either in checking mode or eq2 is a family equality)
1330 substEq (RewriteFam {rwi_args = args, rwi_right = ty})
1332 | Just tv <- tcGetTyVar_maybe ty
1333 , tv `elemVarSet` tyVarsOfRewriteInst eq2
1334 , isWantedRewriteInst eq2
1335 , checkingMode || not (isRewriteVar eq2)
1336 = do { -- substitute into the right-hand side
1337 ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1338 right2' = substTy tySubst (rwi_right eq2)
1340 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1341 RewriteFam {rwi_fam = fam,
1342 rwi_args = args} -> mkTyConApp fam args
1343 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1345 RewriteVar {rwi_var = tv2}
1346 -- variable equality: perform an occurs check
1347 | tv2 `elemVarSet` tyVarsOfTypes args
1348 -> occurCheckErr left2 right2'
1350 -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1351 RewriteFam {rwi_fam = fam}
1352 -- family equality: substitute also into the left-hand side
1353 -> do { let co1Subst = substTy coSubst left2
1354 args2' = substTys tySubst (rwi_args eq2)
1355 left2' = mkTyConApp fam args2'
1356 ; co2'' <- mkRightTransEqInstCo co2' co1Subst
1358 ; return $ eq2 {rwi_args = args2', rwi_right = right2',
1367 -- We have, co :: tv ~ ty
1368 -- => apply [ty/tv] to dictionary predicate
1369 -- (but only if tv actually occurs in the predicate)
1370 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1372 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1373 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1374 pred' = substPred tySubst (tci_pred dict)
1375 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1376 ; return (binds, dict')
1380 substDict _ _ _ _ dict
1381 = return (emptyBag, dict)
1382 -- !!!TODO: Still need to substitute into IP constraints.
1385 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1386 alpha, we record a binding of alpha with t or a, respectively, and for co :=
1387 id. We do the same for equalities of the form co :: F t1..tn ~ alpha unless
1388 we are in inference mode and alpha appears in the environment - i.e., it is
1389 not a flexible introduced by flattening locals or it is local, but was
1390 propagated into the environment by the instantiation of a variable equality.
1392 We proceed in two phases: (1) first we consider all variable equalities and then
1393 (2) we consider all family equalities. The two phase structure is required as
1394 the recorded variable equalities determine which skolems flexibles escape, and
1395 hence, which family equalities may be recorded as bindings.
1397 We return all wanted equalities for which we did not generate a binding.
1398 (These can be skolem variable equalities, cyclic variable equalities, and
1401 We don't update any meta variables. Instead, instantiation simply implies
1402 putting a type variable binding into the binding pool of TcM.
1405 * We may encounter filled flexibles due to the instant filling of local
1406 skolems in local-given constraints during flattening.
1407 * Be careful with SigTVs. They can only be instantiated with other SigTVs or
1411 bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
1412 bindAndExtract eqs checkingMode freeFlexibles
1413 = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
1414 4 (ppr eqs $$ ppr freeFlexibles)
1415 ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
1416 ; escapingSkolems <- getEscapingSkolems
1417 ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
1418 ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
1419 ; mapM rewriteInstToInst residuals2
1422 -- NB: we don't have to transitively chase the relation as the substitution
1423 -- process applied before generating the bindings was exhaustive
1425 = do { tybinds_rel <- getTcTyVarBindsRelation
1426 ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
1429 isFree (tv, _) = tv `elemVarSet` freeFlexibles
1431 -- co :: alpha ~ t or co :: a ~ alpha
1432 instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1433 = do { flexi_tv1 <- isFlexible tv1
1434 ; maybe_flexi_tv2 <- isFlexibleTy ty2
1435 ; case (flexi_tv1, maybe_flexi_tv2) of
1437 | isSigTyVar tv1 && isSigTyVar tv2
1438 -> -- co :: alpha ~ beta, where both a SigTvs
1439 doInst (rwi_swapped eq) tv1 ty2 co eq
1441 | Just tv2 <- tcGetTyVar_maybe ty2
1444 -> -- co :: alpha ~ a, where alpha is a SigTv
1445 doInst (rwi_swapped eq) tv1 ty2 co eq
1447 | not (isSigTyVar tv1)
1448 -> -- co :: alpha ~ t, where alpha is not a SigTv
1449 doInst (rwi_swapped eq) tv1 ty2 co eq
1453 -> -- co :: a ~ alpha, where alpha is a SigTv
1454 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1455 | not (isSigTyVar tv2)
1456 -> -- co :: a ~ alpha, where alpha is not a SigTv
1457 -- ('a' may be filled)
1458 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1459 _ -> return $ Just eq
1461 instVarEq eq = return $ Just eq
1463 -- co :: F args ~ alpha,
1464 -- and we are either in checking mode or alpha is a skolem flexible that
1466 instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1467 rwi_right = ty2, rwi_co = co})
1468 | Just tv2 <- tcGetTyVar_maybe ty2
1469 , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
1470 = do { flexi_tv2 <- isFlexible tv2
1473 doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1477 instFamEq _ eq = return $ Just eq
1479 -- tv is a meta var, but not a SigTV and not filled
1481 | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1482 | otherwise = return False
1484 -- type is a tv that is a meta var, but not a SigTV and not filled
1486 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1487 ; if flexi then return $ Just tv
1490 | otherwise = return Nothing
1492 doInst _swapped _tv _ty (Right ty) _eq
1493 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1494 doInst swapped tv ty (Left cotv) eq
1495 = do { lookupTV <- lookupTcTyVar tv
1496 ; bMeta swapped tv lookupTV ty cotv
1499 -- Try to create a binding for a meta variable. There is *no* need to
1500 -- consider reorienting the underlying equality; `checkOrientation'
1501 -- makes sure that we get variable-variable equalities only in the
1502 -- appropriate orientation.
1504 bMeta :: Bool -- is this a swapped equality?
1505 -> TcTyVar -- tyvar to instantiate
1506 -> LookupTyVarResult -- lookup result of that tyvar
1507 -> TcType -- to to instantiate tyvar with
1508 -> TcTyVar -- coercion tyvar of current equality
1509 -> TcM (Maybe RewriteInst) -- returns the original equality if
1510 -- the tyvar could not be instantiated,
1511 -- and hence, the equality must be kept
1513 -- meta variable has been filled already
1514 -- => this should never happen due to the use of `isFlexible' above
1515 bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1516 = pprPanic "TcTyFuns.bMeta" $
1517 ptext (sLit "flexible") <+> ppr tv <+>
1518 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1519 ptext (sLit "meant to fill with") <+> ppr ty
1521 -- type variable meets type variable
1522 -- => `checkOrientation' already ensures that it is fine to instantiate
1523 -- tv1 with tv2, but chase tv2's instantiations if necessary, so that
1524 -- we eventually can perform a kinds check in bMetaInst
1525 -- NB: tv's instantiations won't alter the orientation in which we
1526 -- want to instantiate as they either constitute a family
1527 -- application or are themselves due to a properly oriented
1529 bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
1530 = do { lookupTV2 <- lookupTcTyVar tv2
1532 IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
1533 DoneTv _ -> bMetaInst swapped tv1 ty cotv
1536 -- updatable meta variable meets non-variable type
1537 -- => occurs check, monotype check, and kinds match check, then bind
1538 bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
1539 = bMetaInst swapped tv non_tv_ty cotv
1541 bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
1543 -- We know `tv' can be instantiated; check that `ty' is alright for
1544 -- instantiating `tv' with and then record a binding; we return the
1545 -- original equality if it is cyclic through a synonym family
1546 bMetaInst swapped tv ty cotv
1547 = do { -- occurs + monotype check
1548 ; mb_ty' <- checkTauTvUpdate tv ty
1552 -- there may be a family in non_tv_ty due to an unzonked,
1553 -- but updated skolem for a local equality
1554 -- (cf `wantedToLocal')
1557 do { checkKinds swapped tv ty'
1558 ; bindMetaTyVar tv ty' -- bind meta var
1559 ; bindMetaTyVar cotv ty' -- bind co var
1566 %************************************************************************
1570 %************************************************************************
1572 The infamous couldn't match expected type soandso against inferred type
1573 somethingdifferent message.
1576 eqInstMisMatch :: Inst -> TcM a
1578 = ASSERT( isEqInst inst )
1579 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1581 (ty_act, ty_exp) = eqInstTys inst
1582 InstLoc _ _ ctxt = instLoc inst
1584 -----------------------
1585 failWithMisMatch :: TcType -> TcType -> TcM a
1586 -- Generate the message when two types fail to match,
1587 -- going to some trouble to make it helpful.
1588 -- The argument order is: actual type, expected type
1589 failWithMisMatch ty_act ty_exp
1590 = do { env0 <- tcInitTidyEnv
1591 ; ty_exp <- zonkTcType ty_exp
1592 ; ty_act <- zonkTcType ty_act
1593 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1596 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1597 misMatchMsg env0 (ty_act, ty_exp)
1598 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1599 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1600 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1602 ptext (sLit "against inferred type") <+> pp_act],
1603 nest 2 (extra_exp $$ extra_act),
1604 nest 2 (vcat (map pp_open_tc (nub open_tcs)))]
1605 -- See Note [Non-injective type functions]
1610 open_tcs = [tc | TyConApp tc _ <- [ty_act, ty_exp]
1612 pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
1613 <+> ptext (sLit "is a type function") <> pp_inj
1615 pp_inj | isInjectiveTyCon tc = empty
1616 | otherwise = ptext (sLit (", and may not be injective"))
1618 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1620 = let (env1, tidy_ty) = tidyOpenType env ty
1621 (env2, extra) = ppr_extra env1 tidy_ty
1623 (env2, quotes (ppr tidy_ty), extra)
1625 -- (ppr_extra env ty) shows extra info about 'ty'
1626 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1627 ppr_extra env (TyVarTy tv)
1628 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1629 = (env1, pprSkolTvBinding tv1)
1631 (env1, tv1) = tidySkolemTyVar env tv
1633 ppr_extra env _ty = (env, empty) -- Normal case
1636 Note [Non-injective type functions]
1637 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1638 It's very confusing to get a message like
1639 Couldn't match expected type `Depend s'
1640 against inferred type `Depend s1'
1642 NB: `Depend' is type function, and hence may not be injective
1644 Currently we add this independently for each argument, so we also get
1645 Couldn't match expected type `a'
1646 against inferred type `Dual (Dual a)'
1647 NB: `Dual' is a (non-injective) type function
1648 which is arguably redundant. But on the other hand, it's probably
1649 a good idea for the programmer to know the error involves type functions
1650 so I've left it in for now. The obvious alternative is to only add
1651 this NB in the case of matching (T ...) ~ (T ...).
1654 Warn of loopy local equalities that were dropped.
1657 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1658 warnDroppingLoopyEquality ty1 ty2
1659 = do { env0 <- tcInitTidyEnv
1660 ; ty1 <- zonkTcType ty1
1661 ; ty2 <- zonkTcType ty2
1662 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1663 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1664 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1665 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))