1 Normalisation of type terms relative to type instances as well as
2 normalisation and entailment checking of equality constraints.
6 -- type normalisation wrt to toplevel equalities only
9 -- instance normalisation wrt to equalities
13 misMatchMsg, failWithMisMatch,
18 #include "HsVersions.h"
30 import TypeRep ( Type(..) )
39 import SrcLoc ( Located(..) )
49 %************************************************************************
51 Normalisation of types wrt toplevel equality schemata
53 %************************************************************************
55 Unfold a single synonym family instance and yield the witnessing coercion.
56 Return 'Nothing' if the given type is either not synonym family instance
57 or is a synonym family instance that has no matching instance declaration.
58 (Applies only if the type family application is outermost.)
60 For example, if we have
62 :Co:R42T a :: T [a] ~ :R42T a
64 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
67 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
68 tcUnfoldSynFamInst (TyConApp tycon tys)
69 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
72 = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
73 ; maybeFamInst <- tcLookupFamInst tycon tys
74 ; case maybeFamInst of
75 Nothing -> return Nothing
76 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
77 mkTyConApp coe_tc rep_tys)
79 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
80 (tyConFamilyCoercion_maybe rep_tc)
82 tcUnfoldSynFamInst _other = return Nothing
85 Normalise 'Type's and 'PredType's by unfolding type family applications where
86 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
88 tcNormaliseFamInst ty = (co, ty')
92 -- |Normalise the given type as far as possible with toplevel equalities.
93 -- This results in a coercion witnessing the type equality, in addition to the
96 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
97 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
100 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
101 apply the normalisation function gives as the first argument to every TyConApp
102 and every TyVarTy subterm.
104 tcGenericNormaliseFamInst fun ty = (co, ty')
107 This function is (by way of using smart constructors) careful to ensure that
108 the returned coercion is exactly IdCo (and not some semantically equivalent,
109 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
110 makes it easy for the caller to determine whether the type changed. BUT
111 even if we return IdCo, ty' may be *syntactically* different from ty due to
112 unfolded closed type synonyms (by way of tcCoreView). In the interest of
113 good error messages, callers should discard ty' in favour of ty in this case.
116 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
117 -- what to do with type functions and tyvars
118 -> TcType -- old type
119 -> TcM (CoercionI, TcType) -- (coercion, new type)
120 tcGenericNormaliseFamInst fun ty
121 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
122 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
123 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
124 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
125 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
126 ; case maybe_ty_co of
127 -- a matching family instance exists
129 do { let first_coi = mkTransCoI tycon_coi (ACo co)
130 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
131 ; let fix_coi = mkTransCoI first_coi rest_coi
132 ; return (fix_coi, nty)
134 -- no matching family instance exists
135 -- we do not do anything
136 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
138 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
139 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
140 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
141 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
143 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
144 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
145 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
146 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
148 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
149 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
150 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
152 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
154 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
155 ; res <- lookupTcTyVar tv
158 do { maybe_ty' <- fun ty
160 Nothing -> return (IdCo, ty)
162 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
163 ; return (ACo co1 `mkTransCoI` coi2, ty'')
166 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
170 tcGenericNormaliseFamInst fun (PredTy predty)
171 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
172 ; return (coi, PredTy pred') }
174 ---------------------------------
175 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
177 -> TcM (CoercionI, TcPredType)
179 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
180 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
181 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
183 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
184 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
185 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
187 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
188 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
189 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
190 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
194 %************************************************************************
196 Normalisation of instances wrt to equalities
198 %************************************************************************
200 Given a set of given, local constraints and a set of wanted constraints,
201 simplify the wanted equalities as far as possible and normalise both local and
202 wanted dictionaries with respect to the equalities.
204 In addition to the normalised local dictionaries and simplified wanteds, the
205 function yields bindings for instantiated meta variables (due to solving
206 equality constraints) and dictionary bindings (due to simplifying class
207 constraints). The bag of type variable bindings only contains bindings for
208 non-local variables - i.e., type variables other than those newly created by
209 the present function. Consequently, type improvement took place iff the bag
210 of bindings contains any bindings for proper type variables (not just covars).
211 The solver does not instantiate any non-local variables; i.e., the bindings
212 must be executed by the caller.
214 All incoming constraints are assumed to be zonked already. All outgoing
215 constraints will be zonked again.
217 NB: The solver only has local effects that cannot be observed from outside.
218 In particular, it can be executed twice on the same constraint set with
219 the same result (modulo generated variables names).
222 tcReduceEqs :: [Inst] -- locals
224 -> TcM ([Inst], -- normalised locals (w/o equalities)
225 [Inst], -- normalised wanteds (including equalities)
226 TcTyVarBinds, -- bindings for meta type variables
227 TcDictBinds) -- bindings for all simplified dictionaries
228 tcReduceEqs locals wanteds
229 = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
230 do { let (local_eqs , local_dicts) = partition isEqInst locals
231 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
232 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
233 ; eqCfg2 <- normaliseDicts False local_dicts
234 ; eqCfg3 <- normaliseDicts True wanteds_dicts
235 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig`
236 eqCfg2 `unionEqConfig`
238 ; finaliseEqsAndDicts freeFlexibles eqCfg
240 -- execute type bindings of skolem flexibles...
241 ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
242 -- ...and zonk the constraints to propagate the bindings
243 ; locals_z <- zonkInsts locals
244 ; wanteds_z <- zonkInsts wanteds
245 ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
248 -- unification variables that appear in the environment and may not be
249 -- instantiated - this includes coercion variables
250 freeFlexibles = tcTyVarsOfInsts locals `unionVarSet`
251 tcTyVarsOfInsts wanteds
253 pruneTyBinds tybinds freeFlexibles
254 = do { let tybinds' = bagToList tybinds
255 (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
256 ; execTcTyVarBinds (listToBag skolem_tybinds)
257 ; return $ listToBag env_tybinds
260 isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
264 %************************************************************************
266 Equality Configurations
268 %************************************************************************
270 We maintain normalised equalities together with the skolems introduced as
271 intermediates during flattening of equalities as well as
274 -- |Configuration of normalised equalities used during solving.
276 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
277 , locals :: [Inst] -- given dicts
278 , wanteds :: [Inst] -- wanted dicts
279 , binds :: TcDictBinds -- bindings
282 addEq :: EqConfig -> RewriteInst -> EqConfig
283 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
285 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
286 unionEqConfig eqc1 eqc2 = EqConfig
287 { eqs = eqs eqc1 ++ eqs eqc2
288 , locals = locals eqc1 ++ locals eqc2
289 , wanteds = wanteds eqc1 ++ wanteds eqc2
290 , binds = binds eqc1 `unionBags` binds eqc2
293 emptyEqConfig :: EqConfig
294 emptyEqConfig = EqConfig
301 instance Outputable EqConfig where
302 ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
303 = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
306 The set of operations on an equality configuration. We obtain the initialise
307 configuration by normalisation ('normaliseEqs'), solve the equalities by
308 propagation ('propagateEqs'), and eventually finalise the configuration when
309 no further propoagation is possible.
312 -- |Turn a set of equalities into an equality configuration for solving.
314 -- Precondition: The Insts are zonked.
316 normaliseEqs :: [Inst] -> TcM EqConfig
318 = do { WARNM2( anyM wantedEqInstIsUnsolved eqs, ppr eqs )
319 ; traceTc $ ptext (sLit "Entering normaliseEqs")
321 ; eqss <- mapM normEqInst eqs
322 ; return $ emptyEqConfig { eqs = concat eqss }
325 -- |Flatten the type arguments of all dictionaries, returning the result as a
326 -- equality configuration. The dictionaries go into the 'wanted' component if
327 -- the second argument is 'True'.
329 -- Precondition: The Insts are zonked.
331 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
332 normaliseDicts isWanted insts
333 = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
334 ptext (if isWanted then sLit "[Wanted] for"
335 else sLit "[Local] for"))
338 ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
340 ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
341 4 (ppr insts' $$ ppr eqss)
342 ; return $ emptyEqConfig { eqs = concat eqss
343 , locals = if isWanted then [] else insts'
344 , wanteds = if isWanted then insts' else []
345 , binds = unionManyBags bindss
349 -- |Solves the equalities as far as possible by applying propagation rules.
351 propagateEqs :: EqConfig -> TcM EqConfig
352 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
353 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
356 ; propagate todoEqs (eqCfg {eqs = []})
359 -- |Finalise a set of equalities and associated dictionaries after
360 -- propagation. The first returned set of instances are the locals (without
361 -- equalities) and the second set are all residual wanteds, including
362 -- equalities. In addition, we return all generated dictionary bindings.
364 finaliseEqsAndDicts :: TcTyVarSet -> EqConfig
365 -> TcM ([Inst], [Inst], TcDictBinds)
366 finaliseEqsAndDicts freeFlexibles (EqConfig { eqs = eqs
371 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
373 ; (eqs', subst_binds, locals', wanteds')
374 <- substitute eqs locals wanteds checkingMode freeFlexibles
375 ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
376 ; let final_binds = subst_binds `unionBags` binds
378 -- Assert that all cotvs of wanted equalities are still unfilled, and
379 -- zonk all final insts, to make any improvement visible
380 ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
381 ; zonked_locals <- zonkInsts locals'
382 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
383 ; return (zonked_locals, zonked_wanteds, final_binds)
386 checkingMode = length eqs > length wanteds || not (null locals)
387 -- no local equalities or dicts => checking mode
391 %************************************************************************
393 Normalisation of equalities
395 %************************************************************************
397 A normal equality is a properly oriented equality with associated coercion
398 that contains at most one family equality (in its left-hand side) is oriented
399 such that it may be used as a rewrite rule. It has one of the following two
402 (1) co :: F t1..tn ~ t (family equalities)
403 (2) co :: x ~ t (variable equalities)
405 Variable equalities fall again in two classes:
407 (2a) co :: x ~ t, where t is *not* a variable, or
408 (2b) co :: x ~ y, where x > y.
410 The types t, t1, ..., tn may not contain any occurrences of synonym
411 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
412 the right-hand side, and the relation x > y is an (nearly) arbitrary, but
413 total order on type variables. The only restriction that we impose on that
414 order is that for x > y, we are happy to instantiate x with y taking into
415 account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
419 = RewriteVar -- Form (2) above
420 { rwi_var :: TyVar -- may be rigid or flexible
421 , rwi_right :: TcType -- contains no synonym family applications
422 , rwi_co :: EqInstCo -- the wanted or given coercion
424 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
425 , rwi_swapped :: Bool -- swapped orientation of original EqInst
427 | RewriteFam -- Forms (1) above
428 { rwi_fam :: TyCon -- synonym family tycon
429 , rwi_args :: [Type] -- contain no synonym family applications
430 , rwi_right :: TcType -- contains no synonym family applications
431 , rwi_co :: EqInstCo -- the wanted or given coercion
433 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
434 , rwi_swapped :: Bool -- swapped orientation of original EqInst
437 isWantedRewriteInst :: RewriteInst -> Bool
438 isWantedRewriteInst = isWantedCo . rwi_co
440 isRewriteVar :: RewriteInst -> Bool
441 isRewriteVar (RewriteVar {}) = True
442 isRewriteVar _ = False
444 tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
445 tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
446 = unitVarSet tv `unionVarSet` tyVarsOfType ty
447 tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
448 = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
450 rewriteInstToInst :: RewriteInst -> TcM Inst
451 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
452 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
453 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
454 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
456 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
459 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
460 deriveEqInst rewrite ty1 ty2 co
461 = do { co_adjusted <- if not swapped then return co
462 else mkSymEqInstCo co (ty2, ty1)
466 , tci_co = co_adjusted
467 , tci_loc = rwi_loc rewrite
468 , tci_name = rwi_name rewrite
472 swapped = rwi_swapped rewrite
473 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
475 instance Outputable RewriteInst where
476 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
477 = hsep [ pprEqInstCo co <+> text "::"
478 , ppr (mkTyConApp fam args)
482 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
483 = hsep [ pprEqInstCo co <+> text "::"
489 pprEqInstCo :: EqInstCo -> SDoc
490 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
491 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
494 The following functions turn an arbitrary equality into a set of normal
495 equalities. This implements the WFlat and LFlat rules of the paper in one
496 sweep. However, we use flexible variables for both locals and wanteds, and
497 avoid to carry around the unflattening substitution \Sigma (for locals) by
498 already updating the skolems for locals with the family application that they
499 represent - i.e., they will turn into that family application on the next
500 zonking (which only happens after finalisation).
502 In a corresponding manner, normDict normalises class dictionaries by
503 extracting any synonym family applications and generation appropriate normal
506 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
507 we drop that equality and raise an error if it is a wanted or a warning if it
511 normEqInst :: Inst -> TcM [RewriteInst]
512 -- Normalise one equality.
514 = ASSERT( isEqInst inst )
515 do { traceTc $ ptext (sLit "normEqInst of ") <+>
516 pprEqInstCo co <+> text "::" <+>
517 ppr ty1 <+> text "~" <+> ppr ty2
518 ; res <- go ty1 ty2 co
520 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
524 (ty1, ty2) = eqInstTys inst
525 co = eqInstCoercion inst
527 -- look through synonyms
528 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
529 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
531 -- left-to-right rule with type family head
532 go ty1@(TyConApp con args) ty2 co
533 | isOpenSynTyConApp ty1 -- only if not oversaturated
534 = mkRewriteFam False con args ty2 co
536 -- right-to-left rule with type family head
537 go ty1 ty2@(TyConApp con args) co
538 | isOpenSynTyConApp ty2 -- only if not oversaturated
539 = do { co' <- mkSymEqInstCo co (ty2, ty1)
540 ; mkRewriteFam True con args ty1 co'
543 -- no outermost family
545 = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
546 ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
547 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
548 sym_co2 = mkSymCoercion co2
550 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
551 ; eqs <- checkOrientation ty1' ty2' co' inst
552 ; if isLoopyEquality eqs ty12_eqs'
553 then do { if isWantedCo (tci_co inst)
555 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
558 warnDroppingLoopyEquality ty1 ty2
559 ; return ([]) -- drop the equality
562 return (eqs ++ ty12_eqs')
565 mkRewriteFam swapped con args ty2 co
566 = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
567 ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
568 ; let co1 = mkTyConApp con cargs
569 sym_co2 = mkSymCoercion co2
570 all_eqs = concat args_eqss ++ ty2_eqs
571 eqTys = (mkTyConApp con args', ty2')
572 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
573 ; let thisRewriteFam = RewriteFam
578 , rwi_loc = tci_loc inst
579 , rwi_name = tci_name inst
580 , rwi_swapped = swapped
582 ; return $ thisRewriteFam : all_eqs'
585 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
586 -- have a variable equality with 'a' on the lhs as the first equality.
587 -- Then, check whether 'a' occurs in the lhs of any family equality
588 -- generated by flattening.
589 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
591 inRewriteFam (RewriteFam {rwi_args = args})
592 = tv `elemVarSet` tyVarsOfTypes args
593 inRewriteFam _ = False
594 isLoopyEquality _ _ = False
596 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
597 -- Normalise one dictionary or IP constraint.
598 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
599 = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
600 ; let rewriteCo = PredTy $ ClassP clas cargs
601 eqs = concat args_eqss
602 pred' = ClassP clas args'
604 then -- don't generate a binding if there is nothing to flatten
605 return (inst, [], emptyBag)
607 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
608 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
609 ; return (inst', eqs', bind)
611 normDict _isWanted inst
612 = return (inst, [], emptyBag)
613 -- !!!TODO: Still need to normalise IP constraints.
615 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
616 -- Performs the occurs check, decomposition, and proper orientation
617 -- (returns a singleton, or an empty list in case of a trivial equality)
618 -- NB: We cannot assume that the two types already have outermost type
619 -- synonyms expanded due to the recursion in the case of type applications.
620 checkOrientation ty1 ty2 co inst
623 -- look through synonyms
624 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
625 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
627 -- identical types => trivial
630 = do { mkIdEqInstCo co ty1
634 -- two tvs (distinct tvs, due to previous equation)
635 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
636 = do { isBigger <- tv1 `tvIsBigger` tv2
637 ; if isBigger -- left greater
638 then mkRewriteVar False tv1 ty2 co -- => unchanged
639 else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater
640 ; mkRewriteVar True tv2 ty1 co' -- => swap
644 -- only lhs is a tv => unchanged
645 go ty1@(TyVarTy tv1) ty2
646 | ty1 `tcPartOfType` ty2 -- occurs check!
647 = occurCheckErr ty1 ty2
649 = mkRewriteVar False tv1 ty2 co
651 -- only rhs is a tv => swap
652 go ty1 ty2@(TyVarTy tv2)
653 | ty2 `tcPartOfType` ty1 -- occurs check!
654 = occurCheckErr ty2 ty1
656 = do { co' <- mkSymEqInstCo co (ty2, ty1)
657 ; mkRewriteVar True tv2 ty1 co'
660 -- data type constructor application => decompose
661 -- NB: Special cased for efficiency - could be handled as type application
662 go (TyConApp con1 args1) (TyConApp con2 args2)
664 && isInjectiveTyCon con1 -- don't match family synonym apps
665 = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
666 ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
668 ; return $ concat eqss
671 -- function type => decompose
672 -- NB: Special cased for efficiency - could be handled as type application
673 go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
674 = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
675 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
676 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
677 ; return $ eqs_l ++ eqs_r
680 -- type applications => decompose
682 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
683 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
684 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
685 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
686 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
687 ; return $ eqs_l ++ eqs_r
690 -- inconsistency => type error
692 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
695 mkRewriteVar swapped tv ty co = return [RewriteVar
699 , rwi_loc = tci_loc inst
700 , rwi_name = tci_name inst
701 , rwi_swapped = swapped
704 -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
705 tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
707 = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
709 isBigger tv1 (SkolemTv _) tv2 (SkolemTv _)
711 isBigger _ (MetaTv _ _) _ (SkolemTv _)
713 isBigger _ (SkolemTv _) _ (MetaTv _ _)
715 isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
716 -- meta variable meets meta variable
717 -- => be clever about which of the two to update
718 -- (from TcUnify.uUnfilledVars minus boxy stuff)
719 = case (info1, info2) of
720 -- Avoid SigTvs if poss
721 (SigTv _, SigTv _) -> return $ tv1 > tv2
722 (SigTv _, _ ) | k1_sub_k2 -> return False
723 (_, SigTv _) | k2_sub_k1 -> return True
728 -> case (nicer_to_update tv1, nicer_to_update tv2) of
729 (True, False) -> return True
730 (False, True) -> return False
731 _ -> return $ tv1 > tv2
732 | k1_sub_k2 -> return False
733 | k2_sub_k1 -> return True
734 | otherwise -> kind_err >> return True
735 -- Update the variable with least kind info
736 -- See notes on type inference in Kind.lhs
737 -- The "nicer to" part only applies if the two kinds are the same,
738 -- so we can choose which to do.
740 kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
741 unifyKindMisMatch k1 k2
745 k1_sub_k2 = k1 `isSubKind` k2
746 k2_sub_k1 = k2 `isSubKind` k1
748 nicer_to_update tv = isSystemName (Var.varName tv)
749 -- Try to update sys-y type variables in preference to ones
750 -- gotten (say) by instantiating a polymorphic function with
751 -- a user-written type sig
753 flattenType :: Inst -- context to get location & name
754 -> Type -- the type to flatten
755 -> TcM (Type, -- the flattened type
756 Coercion, -- coercion witness of flattening wanteds
757 [RewriteInst]) -- extra equalities
758 -- Removes all family synonyms from a type by moving them into extra equalities
759 flattenType inst ty = go ty
761 -- look through synonyms
762 go ty | Just ty' <- tcView ty
763 = do { (ty_flat, co, eqs) <- go ty'
765 then -- unchanged, keep the old type with folded synonyms
768 return (ty_flat, co, eqs)
771 -- type variable => nothing to do
773 = return (ty, ty, [])
775 -- type family application & family arity matches number of args
776 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
777 go ty@(TyConApp con args)
778 | isOpenSynTyConApp ty -- only if not oversaturated
779 = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
780 ; alpha <- newFlexiTyVar (typeKind ty)
781 ; let alphaTy = mkTyVarTy alpha
782 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
783 ; let thisRewriteFam = RewriteFam
786 , rwi_right = alphaTy
787 , rwi_co = mkWantedCo cotv
788 , rwi_loc = tci_loc inst
789 , rwi_name = tci_name inst
793 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
794 thisRewriteFam : concat args_eqss)
797 -- datatype constructor application => flatten subtypes
798 -- NB: Special cased for efficiency - could be handled as type application
799 go ty@(TyConApp con args)
800 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
801 = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
802 ; let args_eqs = concat args_eqss
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 -- predicate type => handle like a datatype constructor application
853 go (PredTy (ClassP cls tys))
854 = do { (tys', ctys, tys_eqss) <- mapAndUnzip3M go tys
855 ; let tys_eqs = concat tys_eqss
857 then -- unchanged, keep the old type with folded synonyms
860 return (PredTy (ClassP cls tys'),
861 PredTy (ClassP cls ctys),
865 -- implicit parameter => flatten subtype
866 go ty@(PredTy (IParam ipn ity))
867 = do { (ity', co, eqs) <- go ity
869 then return (ty, ty, [])
870 else return (PredTy (IParam ipn ity'),
871 PredTy (IParam ipn co),
875 -- we should never see a equality
876 go (PredTy (EqPred _ _))
877 = panic "TcTyFuns.flattenType: malformed type"
879 go _ = panic "TcTyFuns: suppress bogus warning"
881 adjustCoercions :: EqInstCo -- coercion of original equality
882 -> Coercion -- coercion witnessing the left rewrite
883 -> Coercion -- coercion witnessing the right rewrite
884 -> (Type, Type) -- types of flattened equality
885 -> [RewriteInst] -- equalities from flattening
886 -> TcM (EqInstCo, -- coercion for flattened equality
887 [RewriteInst]) -- final equalities from flattening
888 -- Depending on whether we flattened a local or wanted equality, that equality's
889 -- coercion and that of the new equalities produced during flattening are
891 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
892 -- wanted => generate a fresh coercion variable for the flattened equality
893 = do { cotv' <- newMetaCoVar ty_l ty_r
894 ; bindMetaTyVar cotv $
895 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
896 ; return (Left cotv', all_eqs)
899 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
900 -- local => turn all new equalities into locals and update (but not zonk)
902 = do { all_eqs' <- mapM wantedToLocal all_eqs
903 ; return (co, all_eqs')
906 mkDictBind :: Inst -- original instance
907 -> Bool -- is this a wanted contraint?
908 -> Coercion -- coercion witnessing the rewrite
909 -> PredType -- coerced predicate
910 -> TcM (Inst, -- new inst
911 TcDictBinds) -- binding for coerced dictionary
912 mkDictBind dict isWanted rewriteCo pred
913 = do { dict' <- newDictBndr loc pred
914 -- relate the old inst to the new one
915 -- target_dict = source_dict `cast` st_co
916 ; let (target_dict, source_dict, st_co)
917 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
918 | otherwise = (dict', dict, rewriteCo)
920 -- co :: dict ~ dict'
921 -- hence, if isWanted
922 -- dict = dict' `cast` sym co
924 -- dict' = dict `cast` co
925 expr = HsVar $ instToId source_dict
926 cast_expr = HsWrap (WpCast st_co) expr
927 rhs = L (instLocSpan loc) cast_expr
928 binds = instToDictBind target_dict rhs
929 ; return (dict', binds)
934 -- gamma ::^l Fam args ~ alpha
935 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
936 -- (the update of alpha will not be apparent during propagation, as we
937 -- never follow the indirections of meta variables; it will be revealed
938 -- when the equality is zonked)
940 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
941 -- have escaped into some other coercions during normalisation.
943 -- We do actually update alpha and gamma by side effect (instead of
944 -- only remembering the binding with `bindMetaTyVar', as we do for all
945 -- other tyvars). We can do this as the side effects are strictly
946 -- *local*; we know that both alpha and gamma were just a moment ago
947 -- introduced by normalisation.
949 wantedToLocal :: RewriteInst -> TcM RewriteInst
950 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
952 rwi_right = TyVarTy alpha,
953 rwi_co = Left gamma})
954 = do { writeMetaTyVar alpha (mkTyConApp fam args)
955 ; writeMetaTyVar gamma (mkTyConApp fam args)
956 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
958 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
962 %************************************************************************
964 Propagation of equalities
966 %************************************************************************
968 Apply the propagation rules exhaustively.
971 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
972 propagate [] eqCfg = return eqCfg
973 propagate (eq:eqs) eqCfg
974 = do { optEqs <- applyTop eq
977 -- Top applied to 'eq' => retry with new equalities
978 Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
980 -- Top doesn't apply => try subst rules with all other
981 -- equalities, after that 'eq' can go into the residual list
982 Nothing -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
983 ; propagate eqs' (eqCfg' `addEq` eq)
987 applySubstRules :: RewriteInst -- currently considered eq
988 -> [RewriteInst] -- todo eqs list
989 -> EqConfig -- residual
990 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
991 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
992 = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
993 ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
994 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
995 eqConfig {eqs = unchangedEqs_r})
998 mapSubstRules :: RewriteInst -- try substituting this equality
999 -> [RewriteInst] -- into these equalities
1000 -> TcM ([RewriteInst], [RewriteInst])
1001 mapSubstRules eq eqs
1002 = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
1003 ; return (concat newEqss, concat unchangedEqss)
1007 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
1008 4 (ppr eq1 $$ ppr eq2)
1010 -- try the SubstFam rule
1011 ; optEqs <- applySubstFam eq1 eq2
1013 Just eqs -> return (eqs, [])
1015 { -- try the SubstVarVar rule
1016 optEqs <- applySubstVarVar eq1 eq2
1018 Just eqs -> return (eqs, [])
1020 { -- try the SubstVarFam rule
1021 optEqs <- applySubstVarFam eq1 eq2
1023 Just eq -> return ([eq], [])
1024 Nothing -> return ([], [eq2])
1025 -- if no rule matches, we return the equlity we tried to
1026 -- substitute into unchanged
1030 Attempt to apply the Top rule. The rule is
1034 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
1036 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
1038 Returns Nothing if the rule could not be applied. Otherwise, the resulting
1039 equality is normalised and a list of the normal equalities is returned.
1042 applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1044 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
1045 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
1047 Nothing -> return Nothing
1048 Just (lhs, rewrite_co)
1049 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1050 ; eq' <- deriveEqInst eq lhs rhs co'
1051 ; liftM Just $ normEqInst eq'
1058 applyTop _ = return Nothing
1061 Attempt to apply the SubstFam rule. The rule is
1063 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
1065 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1067 where co1 may be a wanted only if co2 is a wanted, too.
1069 Returns Nothing if the rule could not be applied. Otherwise, the equality
1070 co2' is normalised and a list of the normal equalities is returned. (The
1071 equality co1 is not returned as it remain unaltered.)
1074 applySubstFam :: RewriteInst
1076 -> TcM (Maybe ([RewriteInst]))
1077 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1078 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1080 -- rule matches => rewrite
1081 | fam1 == fam2 && tcEqTypes args1 args2 &&
1082 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1083 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1084 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1085 ; liftM Just $ normEqInst eq2'
1088 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1089 | fam1 == fam2 && tcEqTypes args1 args2 &&
1090 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1091 = return $ Just [eq2]
1096 co1 = eqInstCoType (rwi_co eq1)
1099 applySubstFam _ _ = return Nothing
1102 Attempt to apply the SubstVarVar rule. The rule is
1104 co1 :: x ~ t & co2 :: x ~ s
1106 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1108 where co1 may be a wanted only if co2 is a wanted, too.
1110 Returns Nothing if the rule could not be applied. Otherwise, the equality
1111 co2' is normalised and a list of the normal equalities is returned. (The
1112 equality co1 is not returned as it remain unaltered.)
1115 applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1116 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1117 eq2@(RewriteVar {rwi_var = tv2})
1119 -- rule matches => rewrite
1121 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1122 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1123 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1124 ; liftM Just $ normEqInst eq2'
1127 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1129 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1130 = return $ Just [eq2]
1135 co1 = eqInstCoType (rwi_co eq1)
1138 applySubstVarVar _ _ = return Nothing
1141 Attempt to apply the SubstVarFam rule. The rule is
1143 co1 :: x ~ t & co2 :: F s1..sn ~ s
1145 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1146 with co2 = [co1/x](F s1..sn) |> co2'
1148 where x occurs in F s1..sn. (co1 may be local or wanted.)
1150 Returns Nothing if the rule could not be applied. Otherwise, the equality
1151 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1154 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1156 -- rule matches => rewrite
1157 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1158 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1159 | tv1 `elemVarSet` tyVarsOfTypes args2
1160 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1161 args2' = substTysWith [tv1] [rhs1] args2
1162 lhs2 = mkTyConApp fam2 args2'
1163 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1164 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1167 rhs1 = rwi_right eq1
1168 rhs2 = rwi_right eq2
1169 co1 = eqInstCoType (rwi_co eq1)
1172 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1173 applySubstVarFam (RewriteFam {rwi_args = args1})
1174 eq2@(RewriteVar {rwi_var = tv2})
1175 | tv2 `elemVarSet` tyVarsOfTypes args1
1178 applySubstVarFam _ _ = return Nothing
1182 %************************************************************************
1184 Finalisation of equalities
1186 %************************************************************************
1188 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1189 (both local and wanted) into the right-hand sides of all other equalities and
1190 of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
1191 other *family* equalities. This may lead to recursive equalities; i.e., (1)
1192 we need to apply the substitution implied by one equality exhaustively before
1193 turning to the next and (2) we need an occurs check.
1195 We also apply the same substitutions to the local and wanted class and IP
1198 We perform the substitutions in two steps:
1200 Step A: Substitute variable equalities into the right-hand sides of all
1201 other equalities (but wanted only into wanteds) and into class and IP
1202 constraints (again wanteds only into wanteds).
1204 Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
1205 'alpha' is a skolem flexible (i.e., not free in the environment),
1206 into the right-hand sides of all wanted variable equalities and into
1207 both sides of all wanted family equalities.
1209 Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
1210 alpha' into the right-hand sides of all wanted variable equalities
1211 and into both sides of all wanted family equalities.
1213 In inference mode, we do not substitute into variable equalities in Steps B & C.
1215 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1216 substitute variable equalities first; e.g., consider
1218 F s ~ alpha, alpha ~ t
1220 If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1221 This would be bad as `F s' is less useful, eg, as an argument to a class
1224 The restriction on substituting locals is necessary due to examples, such as
1226 F delta ~ alpha, F alpha ~ delta,
1228 where `alpha' is a skolem flexible and `delta' a environment flexible. We need
1229 to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
1230 we may wrongly claim to having performed an improvement, which can lead to
1231 non-termination of the combined class-family solver.
1233 We do also substitute flexibles, as in `alpha ~ t' into class constraints.
1234 When `alpha' is later instantiated, we'd get the same effect, but in the
1235 meantime the class constraint would miss some information, which would be a
1236 problem in an integrated equality-class solver.
1239 * Given that we apply the substitution corresponding to a single equality
1240 exhaustively, before turning to the next, and because we eliminate recursive
1241 equalities, all opportunities for subtitution will have been exhausted after
1242 we have considered each equality once.
1245 substitute :: [RewriteInst] -- equalities
1246 -> [Inst] -- local class dictionaries
1247 -> [Inst] -- wanted class dictionaries
1248 -> Bool -- True ~ checking mode; False ~ inference
1249 -> TyVarSet -- flexibles free in the environment
1250 -> TcM ([RewriteInst], -- equalities after substitution
1251 TcDictBinds, -- all newly generated dictionary bindings
1252 [Inst], -- local dictionaries after substitution
1253 [Inst]) -- wanted dictionaries after substitution
1254 substitute eqs locals wanteds checkingMode freeFlexibles
1255 = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
1256 -- sorting the equalities appropriately: first all variable, then all
1257 -- family/skolem, and then the remaining family equalities.
1258 let (var_eqs, fam_eqs) = partition isRewriteVar eqs
1259 (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
1261 subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1263 isFamSkolemEq (RewriteFam {rwi_right = ty})
1264 | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
1265 isFamSkolemEq _ = False
1267 subst [] res binds locals wanteds
1268 = return (res, binds, locals, wanteds)
1271 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1272 res binds locals wanteds
1273 = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
1276 -- create the substitution
1277 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1278 tySubst = zipOpenTvSubst [tv] [ty]
1280 -- substitute into all other equalities
1281 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1282 ; res' <- mapM (substEq eq coSubst tySubst) res
1284 -- only substitute local equalities into local dictionaries
1285 ; (lbinds, locals') <- if not (isWantedCo co)
1288 (substDict eq coSubst tySubst False)
1293 -- substitute all equalities into wanteds dictionaries
1294 ; (wbinds, wanteds') <- mapAndUnzipM
1295 (substDict eq coSubst tySubst True)
1298 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1299 ; subst eqs' (eq:res') binds' locals' wanteds'
1302 -- co ::^w F t1..tn ~ alpha
1303 subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
1305 res binds locals wanteds
1306 | Just tv <- tcGetTyVar_maybe ty
1309 = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
1312 -- create the substitution
1313 ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
1314 tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
1316 -- substitute into other wanted equalities (`substEq' makes sure
1317 -- that we only substitute into wanteds)
1318 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1319 ; res' <- mapM (substEq eq coSubst tySubst) res
1321 ; subst eqs' (eq:res') binds locals wanteds
1324 subst (eq:eqs) res binds locals wanteds
1325 = subst eqs (eq:res) binds locals wanteds
1327 -- We have, co :: tv ~ ty
1328 -- => apply [ty/tv] to right-hand side of eq2
1329 -- (but only if tv actually occurs in the right-hand side of eq2
1330 -- and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
1331 substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1333 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1334 && (isWantedRewriteInst eq2 || not (isWantedCo co))
1335 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1336 right2' = substTy tySubst (rwi_right eq2)
1338 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1339 RewriteFam {rwi_fam = fam,
1340 rwi_args = args} ->mkTyConApp fam args
1341 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1343 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1344 -> occurCheckErr left2 right2'
1345 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1348 -- We have, co ::^w F t1..tn ~ tv
1349 -- => apply [F t1..tn/tv] to eq2
1350 -- (but only if tv actually occurs in eq2
1351 -- and eq2 is a wanted equality
1352 -- and we are either in checking mode or eq2 is a family equality)
1353 substEq (RewriteFam {rwi_args = args, rwi_right = ty})
1355 | Just tv <- tcGetTyVar_maybe ty
1356 , tv `elemVarSet` tyVarsOfRewriteInst eq2
1357 , isWantedRewriteInst eq2
1358 , checkingMode || not (isRewriteVar eq2)
1359 = do { -- substitute into the right-hand side
1360 ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1361 right2' = substTy tySubst (rwi_right eq2)
1363 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1364 RewriteFam {rwi_fam = fam,
1365 rwi_args = args} -> mkTyConApp fam args
1366 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1368 RewriteVar {rwi_var = tv2}
1369 -- variable equality: perform an occurs check
1370 | tv2 `elemVarSet` tyVarsOfTypes args
1371 -> occurCheckErr left2 right2'
1373 -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1374 RewriteFam {rwi_fam = fam}
1375 -- family equality: substitute also into the left-hand side
1376 -> do { let co1Subst = substTy coSubst left2
1377 args2' = substTys tySubst (rwi_args eq2)
1378 left2' = mkTyConApp fam args2'
1379 ; co2'' <- mkRightTransEqInstCo co2' co1Subst
1381 ; return $ eq2 {rwi_args = args2', rwi_right = right2',
1390 -- We have, co :: tv ~ ty
1391 -- => apply [ty/tv] to dictionary predicate
1392 -- (but only if tv actually occurs in the predicate)
1393 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1395 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1396 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1397 pred' = substPred tySubst (tci_pred dict)
1398 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1399 ; return (binds, dict')
1403 substDict _ _ _ _ dict
1404 = return (emptyBag, dict)
1405 -- !!!TODO: Still need to substitute into IP constraints.
1408 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1409 alpha, we record a binding of alpha with t or a, respectively, and for co :=
1410 id. We do the same for equalities of the form co :: F t1..tn ~ alpha unless
1411 we are in inference mode and alpha appears in the environment - i.e., it is
1412 not a flexible introduced by flattening locals or it is local, but was
1413 propagated into the environment by the instantiation of a variable equality.
1415 We proceed in two phases: (1) first we consider all variable equalities and then
1416 (2) we consider all family equalities. The two phase structure is required as
1417 the recorded variable equalities determine which skolems flexibles escape, and
1418 hence, which family equalities may be recorded as bindings.
1420 We return all wanted equalities for which we did not generate a binding.
1421 (These can be skolem variable equalities, cyclic variable equalities, and
1424 We don't update any meta variables. Instead, instantiation simply implies
1425 putting a type variable binding into the binding pool of TcM.
1428 * We may encounter filled flexibles due to the instant filling of local
1429 skolems in local-given constraints during flattening.
1430 * Be careful with SigTVs. They can only be instantiated with other SigTVs or
1434 bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
1435 bindAndExtract eqs checkingMode freeFlexibles
1436 = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
1437 4 (ppr eqs $$ ppr freeFlexibles)
1438 ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
1439 ; escapingSkolems <- getEscapingSkolems
1440 ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
1441 ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
1442 ; mapM rewriteInstToInst residuals2
1445 -- NB: we don't have to transitively chase the relation as the substitution
1446 -- process applied before generating the bindings was exhaustive
1448 = do { tybinds_rel <- getTcTyVarBindsRelation
1449 ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
1452 isFree (tv, _) = tv `elemVarSet` freeFlexibles
1454 -- co :: alpha ~ t or co :: a ~ alpha
1455 instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1456 = do { flexi_tv1 <- isFlexible tv1
1457 ; maybe_flexi_tv2 <- isFlexibleTy ty2
1458 ; case (flexi_tv1, maybe_flexi_tv2) of
1460 | isSigTyVar tv1 && isSigTyVar tv2
1461 -> -- co :: alpha ~ beta, where both a SigTvs
1462 doInst (rwi_swapped eq) tv1 ty2 co eq
1464 | Just tv2 <- tcGetTyVar_maybe ty2
1467 -> -- co :: alpha ~ a, where alpha is a SigTv
1468 doInst (rwi_swapped eq) tv1 ty2 co eq
1470 | not (isSigTyVar tv1)
1471 -> -- co :: alpha ~ t, where alpha is not a SigTv
1472 doInst (rwi_swapped eq) tv1 ty2 co eq
1476 -> -- co :: a ~ alpha, where alpha is a SigTv
1477 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1478 | not (isSigTyVar tv2)
1479 -> -- co :: a ~ alpha, where alpha is not a SigTv
1480 -- ('a' may be filled)
1481 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1482 _ -> return $ Just eq
1484 instVarEq eq = return $ Just eq
1486 -- co :: F args ~ alpha,
1487 -- and we are either in checking mode or alpha is a skolem flexible that
1489 instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1490 rwi_right = ty2, rwi_co = co})
1491 | Just tv2 <- tcGetTyVar_maybe ty2
1492 , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
1493 = do { flexi_tv2 <- isFlexible tv2
1496 doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1500 instFamEq _ eq = return $ Just eq
1502 -- tv is a meta var, but not a SigTV and not filled
1504 | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1505 | otherwise = return False
1507 -- type is a tv that is a meta var, but not a SigTV and not filled
1509 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1510 ; if flexi then return $ Just tv
1513 | otherwise = return Nothing
1515 doInst _swapped _tv _ty (Right ty) _eq
1516 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1517 doInst swapped tv ty (Left cotv) eq
1518 = do { lookupTV <- lookupTcTyVar tv
1519 ; bMeta swapped tv lookupTV ty cotv
1522 -- Try to create a binding for a meta variable. There is *no* need to
1523 -- consider reorienting the underlying equality; `checkOrientation'
1524 -- makes sure that we get variable-variable equalities only in the
1525 -- appropriate orientation.
1527 bMeta :: Bool -- is this a swapped equality?
1528 -> TcTyVar -- tyvar to instantiate
1529 -> LookupTyVarResult -- lookup result of that tyvar
1530 -> TcType -- to to instantiate tyvar with
1531 -> TcTyVar -- coercion tyvar of current equality
1532 -> TcM (Maybe RewriteInst) -- returns the original equality if
1533 -- the tyvar could not be instantiated,
1534 -- and hence, the equality must be kept
1536 -- meta variable has been filled already
1537 -- => this should never happen due to the use of `isFlexible' above
1538 bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1539 = pprPanic "TcTyFuns.bMeta" $
1540 ptext (sLit "flexible") <+> ppr tv <+>
1541 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1542 ptext (sLit "meant to fill with") <+> ppr ty
1544 -- type variable meets type variable
1545 -- => `checkOrientation' already ensures that it is fine to instantiate
1546 -- tv1 with tv2, but chase tv2's instantiations if necessary, so that
1547 -- we eventually can perform a kinds check in bMetaInst
1548 -- NB: tv's instantiations won't alter the orientation in which we
1549 -- want to instantiate as they either constitute a family
1550 -- application or are themselves due to a properly oriented
1552 bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
1553 = do { lookupTV2 <- lookupTcTyVar tv2
1555 IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
1556 DoneTv _ -> bMetaInst swapped tv1 ty cotv
1559 -- updatable meta variable meets non-variable type
1560 -- => occurs check, monotype check, and kinds match check, then bind
1561 bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
1562 = bMetaInst swapped tv non_tv_ty cotv
1564 bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
1566 -- We know `tv' can be instantiated; check that `ty' is alright for
1567 -- instantiating `tv' with and then record a binding; we return the
1568 -- original equality if it is cyclic through a synonym family
1569 bMetaInst swapped tv ty cotv
1570 = do { -- occurs + monotype check
1571 ; mb_ty' <- checkTauTvUpdate tv ty
1575 -- there may be a family in non_tv_ty due to an unzonked,
1576 -- but updated skolem for a local equality
1577 -- (cf `wantedToLocal')
1580 do { checkKinds swapped tv ty'
1581 ; bindMetaTyVar tv ty' -- bind meta var
1582 ; bindMetaTyVar cotv ty' -- bind co var
1589 %************************************************************************
1593 %************************************************************************
1595 The infamous couldn't match expected type soandso against inferred type
1596 somethingdifferent message.
1599 eqInstMisMatch :: Inst -> TcM a
1601 = ASSERT( isEqInst inst )
1602 setInstCtxt (instLoc inst) $ failWithMisMatch ty_act ty_exp
1604 (ty_act, ty_exp) = eqInstTys inst
1606 -----------------------
1607 failWithMisMatch :: TcType -> TcType -> TcM a
1608 -- Generate the message when two types fail to match,
1609 -- going to some trouble to make it helpful.
1610 -- The argument order is: actual type, expected type
1611 failWithMisMatch ty_act ty_exp
1612 = do { env0 <- tcInitTidyEnv
1613 ; ty_exp <- zonkTcType ty_exp
1614 ; ty_act <- zonkTcType ty_act
1615 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1618 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1619 misMatchMsg env0 (ty_act, ty_exp)
1620 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1621 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1622 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1624 ptext (sLit "against inferred type") <+> pp_act],
1625 nest 2 (extra_exp $$ extra_act $$ extra_tyfun) ]
1626 -- See Note [Non-injective type functions]
1632 = case (tcSplitTyConApp_maybe ty_act, tcSplitTyConApp_maybe ty_exp) of
1633 (Just (tc_act,_), Just (tc_exp,_)) | tc_act == tc_exp
1634 -> if isOpenSynTyCon tc_act then pp_open_tc tc_act
1635 else WARN( True, ppr tc_act) -- If there's a mis-match, then
1636 empty -- it should be a family
1639 pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
1640 <+> ptext (sLit "is a type function") <> pp_inj
1642 pp_inj | isInjectiveTyCon tc = empty
1643 | otherwise = ptext (sLit (", and may not be injective"))
1645 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1647 = let (env1, tidy_ty) = tidyOpenType env ty
1648 (env2, extra) = ppr_extra env1 tidy_ty
1650 (env2, quotes (ppr tidy_ty), extra)
1652 -- (ppr_extra env ty) shows extra info about 'ty'
1653 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1654 ppr_extra env (TyVarTy tv)
1655 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1656 = (env1, pprSkolTvBinding tv1)
1658 (env1, tv1) = tidySkolemTyVar env tv
1660 ppr_extra env _ty = (env, empty) -- Normal case
1663 Note [Non-injective type functions]
1664 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1665 It's very confusing to get a message like
1666 Couldn't match expected type `Depend s'
1667 against inferred type `Depend s1'
1669 NB: `Depend' is type function, and hence may not be injective
1671 Warn of loopy local equalities that were dropped.
1674 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1675 warnDroppingLoopyEquality ty1 ty2
1676 = do { env0 <- tcInitTidyEnv
1677 ; ty1 <- zonkTcType ty1
1678 ; ty2 <- zonkTcType ty2
1679 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1680 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1681 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1682 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))