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 { ASSERTM2( allM 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 -- data 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
803 then -- unchanged, keep the old type with folded synonyms
806 return (mkTyConApp con args',
807 mkTyConApp con cargs,
811 -- function type => flatten subtypes
812 -- NB: Special cased for efficiency - could be handled as type application
813 go ty@(FunTy ty_l ty_r)
814 = do { (ty_l', co_l, eqs_l) <- go ty_l
815 ; (ty_r', co_r, eqs_r) <- go ty_r
816 ; if null eqs_l && null eqs_r
817 then -- unchanged, keep the old type with folded synonyms
820 return (mkFunTy ty_l' ty_r',
825 -- type application => flatten subtypes
827 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
828 -- need to use the smart split as ty may be an
829 -- oversaturated family application
830 = do { (ty_l', co_l, eqs_l) <- go ty_l
831 ; (ty_r', co_r, eqs_r) <- go ty_r
832 ; if null eqs_l && null eqs_r
833 then -- unchanged, keep the old type with folded synonyms
836 return (mkAppTy ty_l' ty_r',
841 -- forall type => panic if the body contains a type family
842 -- !!!TODO: As long as the family does not contain a quantified variable
843 -- we might pull it out, but what if it does contain a quantified
845 go ty@(ForAllTy _ body)
846 | null (tyFamInsts body)
847 = return (ty, ty, [])
849 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
851 -- we should never see a predicate type
853 = panic "TcTyFuns.flattenType: unexpected PredType"
855 go _ = panic "TcTyFuns: suppress bogus warning"
857 adjustCoercions :: EqInstCo -- coercion of original equality
858 -> Coercion -- coercion witnessing the left rewrite
859 -> Coercion -- coercion witnessing the right rewrite
860 -> (Type, Type) -- types of flattened equality
861 -> [RewriteInst] -- equalities from flattening
862 -> TcM (EqInstCo, -- coercion for flattened equality
863 [RewriteInst]) -- final equalities from flattening
864 -- Depending on whether we flattened a local or wanted equality, that equality's
865 -- coercion and that of the new equalities produced during flattening are
867 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
868 -- wanted => generate a fresh coercion variable for the flattened equality
869 = do { cotv' <- newMetaCoVar ty_l ty_r
870 ; bindMetaTyVar cotv $
871 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
872 ; return (Left cotv', all_eqs)
875 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
876 -- local => turn all new equalities into locals and update (but not zonk)
878 = do { all_eqs' <- mapM wantedToLocal all_eqs
879 ; return (co, all_eqs')
882 mkDictBind :: Inst -- original instance
883 -> Bool -- is this a wanted contraint?
884 -> Coercion -- coercion witnessing the rewrite
885 -> PredType -- coerced predicate
886 -> TcM (Inst, -- new inst
887 TcDictBinds) -- binding for coerced dictionary
888 mkDictBind dict isWanted rewriteCo pred
889 = do { dict' <- newDictBndr loc pred
890 -- relate the old inst to the new one
891 -- target_dict = source_dict `cast` st_co
892 ; let (target_dict, source_dict, st_co)
893 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
894 | otherwise = (dict', dict, rewriteCo)
896 -- co :: dict ~ dict'
897 -- hence, if isWanted
898 -- dict = dict' `cast` sym co
900 -- dict' = dict `cast` co
901 expr = HsVar $ instToId source_dict
902 cast_expr = HsWrap (WpCast st_co) expr
903 rhs = L (instLocSpan loc) cast_expr
904 binds = instToDictBind target_dict rhs
905 ; return (dict', binds)
910 -- gamma ::^l Fam args ~ alpha
911 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
912 -- (the update of alpha will not be apparent during propagation, as we
913 -- never follow the indirections of meta variables; it will be revealed
914 -- when the equality is zonked)
916 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
917 -- have escaped into some other coercions during normalisation.
919 -- We do actually update alpha and gamma by side effect (instead of
920 -- only remembering the binding with `bindMetaTyVar', as we do for all
921 -- other tyvars). We can do this as the side effects are strictly
922 -- *local*; we know that both alpha and gamma were just a moment ago
923 -- introduced by normalisation.
925 wantedToLocal :: RewriteInst -> TcM RewriteInst
926 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
928 rwi_right = TyVarTy alpha,
929 rwi_co = Left gamma})
930 = do { writeMetaTyVar alpha (mkTyConApp fam args)
931 ; writeMetaTyVar gamma (mkTyConApp fam args)
932 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
934 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
938 %************************************************************************
940 Propagation of equalities
942 %************************************************************************
944 Apply the propagation rules exhaustively.
947 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
948 propagate [] eqCfg = return eqCfg
949 propagate (eq:eqs) eqCfg
950 = do { optEqs <- applyTop eq
953 -- Top applied to 'eq' => retry with new equalities
954 Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
956 -- Top doesn't apply => try subst rules with all other
957 -- equalities, after that 'eq' can go into the residual list
958 Nothing -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
959 ; propagate eqs' (eqCfg' `addEq` eq)
963 applySubstRules :: RewriteInst -- currently considered eq
964 -> [RewriteInst] -- todo eqs list
965 -> EqConfig -- residual
966 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
967 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
968 = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
969 ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
970 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
971 eqConfig {eqs = unchangedEqs_r})
974 mapSubstRules :: RewriteInst -- try substituting this equality
975 -> [RewriteInst] -- into these equalities
976 -> TcM ([RewriteInst], [RewriteInst])
978 = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
979 ; return (concat newEqss, concat unchangedEqss)
983 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
984 4 (ppr eq1 $$ ppr eq2)
986 -- try the SubstFam rule
987 ; optEqs <- applySubstFam eq1 eq2
989 Just eqs -> return (eqs, [])
991 { -- try the SubstVarVar rule
992 optEqs <- applySubstVarVar eq1 eq2
994 Just eqs -> return (eqs, [])
996 { -- try the SubstVarFam rule
997 optEqs <- applySubstVarFam eq1 eq2
999 Just eq -> return ([eq], [])
1000 Nothing -> return ([], [eq2])
1001 -- if no rule matches, we return the equlity we tried to
1002 -- substitute into unchanged
1006 Attempt to apply the Top rule. The rule is
1010 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
1012 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
1014 Returns Nothing if the rule could not be applied. Otherwise, the resulting
1015 equality is normalised and a list of the normal equalities is returned.
1018 applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
1020 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
1021 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
1023 Nothing -> return Nothing
1024 Just (lhs, rewrite_co)
1025 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
1026 ; eq' <- deriveEqInst eq lhs rhs co'
1027 ; liftM Just $ normEqInst eq'
1034 applyTop _ = return Nothing
1037 Attempt to apply the SubstFam rule. The rule is
1039 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
1041 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1043 where co1 may be a wanted only if co2 is a wanted, too.
1045 Returns Nothing if the rule could not be applied. Otherwise, the equality
1046 co2' is normalised and a list of the normal equalities is returned. (The
1047 equality co1 is not returned as it remain unaltered.)
1050 applySubstFam :: RewriteInst
1052 -> TcM (Maybe ([RewriteInst]))
1053 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
1054 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1056 -- rule matches => rewrite
1057 | fam1 == fam2 && tcEqTypes args1 args2 &&
1058 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1059 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1060 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1061 ; liftM Just $ normEqInst eq2'
1064 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1065 | fam1 == fam2 && tcEqTypes args1 args2 &&
1066 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1067 = return $ Just [eq2]
1072 co1 = eqInstCoType (rwi_co eq1)
1075 applySubstFam _ _ = return Nothing
1078 Attempt to apply the SubstVarVar rule. The rule is
1080 co1 :: x ~ t & co2 :: x ~ s
1082 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
1084 where co1 may be a wanted only if co2 is a wanted, too.
1086 Returns Nothing if the rule could not be applied. Otherwise, the equality
1087 co2' is normalised and a list of the normal equalities is returned. (The
1088 equality co1 is not returned as it remain unaltered.)
1091 applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
1092 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
1093 eq2@(RewriteVar {rwi_var = tv2})
1095 -- rule matches => rewrite
1097 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
1098 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
1099 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1100 ; liftM Just $ normEqInst eq2'
1103 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1105 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1106 = return $ Just [eq2]
1111 co1 = eqInstCoType (rwi_co eq1)
1114 applySubstVarVar _ _ = return Nothing
1117 Attempt to apply the SubstVarFam rule. The rule is
1119 co1 :: x ~ t & co2 :: F s1..sn ~ s
1121 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1122 with co2 = [co1/x](F s1..sn) |> co2'
1124 where x occurs in F s1..sn. (co1 may be local or wanted.)
1126 Returns Nothing if the rule could not be applied. Otherwise, the equality
1127 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1130 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1132 -- rule matches => rewrite
1133 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1134 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1135 | tv1 `elemVarSet` tyVarsOfTypes args2
1136 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1137 args2' = substTysWith [tv1] [rhs1] args2
1138 lhs2 = mkTyConApp fam2 args2'
1139 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1140 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1143 rhs1 = rwi_right eq1
1144 rhs2 = rwi_right eq2
1145 co1 = eqInstCoType (rwi_co eq1)
1148 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1149 applySubstVarFam (RewriteFam {rwi_args = args1})
1150 eq2@(RewriteVar {rwi_var = tv2})
1151 | tv2 `elemVarSet` tyVarsOfTypes args1
1154 applySubstVarFam _ _ = return Nothing
1158 %************************************************************************
1160 Finalisation of equalities
1162 %************************************************************************
1164 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1165 (both local and wanted) into the right-hand sides of all other equalities and
1166 of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
1167 other *family* equalities. This may lead to recursive equalities; i.e., (1)
1168 we need to apply the substitution implied by one equality exhaustively before
1169 turning to the next and (2) we need an occurs check.
1171 We also apply the same substitutions to the local and wanted class and IP
1174 We perform the substitutions in two steps:
1176 Step A: Substitute variable equalities into the right-hand sides of all
1177 other equalities (but wanted only into wanteds) and into class and IP
1178 constraints (again wanteds only into wanteds).
1180 Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
1181 'alpha' is a skolem flexible (i.e., not free in the environment),
1182 into the right-hand sides of all wanted variable equalities and into
1183 both sides of all wanted family equalities.
1185 Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
1186 alpha' into the right-hand sides of all wanted variable equalities
1187 and into both sides of all wanted family equalities.
1189 In inference mode, we do not substitute into variable equalities in Steps B & C.
1191 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1192 substitute variable equalities first; e.g., consider
1194 F s ~ alpha, alpha ~ t
1196 If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
1197 This would be bad as `F s' is less useful, eg, as an argument to a class
1200 The restriction on substituting locals is necessary due to examples, such as
1202 F delta ~ alpha, F alpha ~ delta,
1204 where `alpha' is a skolem flexible and `delta' a environment flexible. We need
1205 to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
1206 we may wrongly claim to having performed an improvement, which can lead to
1207 non-termination of the combined class-family solver.
1209 We do also substitute flexibles, as in `alpha ~ t' into class constraints.
1210 When `alpha' is later instantiated, we'd get the same effect, but in the
1211 meantime the class constraint would miss some information, which would be a
1212 problem in an integrated equality-class solver.
1215 * Given that we apply the substitution corresponding to a single equality
1216 exhaustively, before turning to the next, and because we eliminate recursive
1217 equalities, all opportunities for subtitution will have been exhausted after
1218 we have considered each equality once.
1221 substitute :: [RewriteInst] -- equalities
1222 -> [Inst] -- local class dictionaries
1223 -> [Inst] -- wanted class dictionaries
1224 -> Bool -- True ~ checking mode; False ~ inference
1225 -> TyVarSet -- flexibles free in the environment
1226 -> TcM ([RewriteInst], -- equalities after substitution
1227 TcDictBinds, -- all newly generated dictionary bindings
1228 [Inst], -- local dictionaries after substitution
1229 [Inst]) -- wanted dictionaries after substitution
1230 substitute eqs locals wanteds checkingMode freeFlexibles
1231 = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
1232 -- sorting the equalities appropriately: first all variable, then all
1233 -- family/skolem, and then the remaining family equalities.
1234 let (var_eqs, fam_eqs) = partition isRewriteVar eqs
1235 (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
1237 subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
1239 isFamSkolemEq (RewriteFam {rwi_right = ty})
1240 | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
1241 isFamSkolemEq _ = False
1243 subst [] res binds locals wanteds
1244 = return (res, binds, locals, wanteds)
1247 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1248 res binds locals wanteds
1249 = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+>
1252 -- create the substitution
1253 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1254 tySubst = zipOpenTvSubst [tv] [ty]
1256 -- substitute into all other equalities
1257 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1258 ; res' <- mapM (substEq eq coSubst tySubst) res
1260 -- only substitute local equalities into local dictionaries
1261 ; (lbinds, locals') <- if not (isWantedCo co)
1264 (substDict eq coSubst tySubst False)
1269 -- substitute all equalities into wanteds dictionaries
1270 ; (wbinds, wanteds') <- mapAndUnzipM
1271 (substDict eq coSubst tySubst True)
1274 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1275 ; subst eqs' (eq:res') binds' locals' wanteds'
1278 -- co ::^w F t1..tn ~ alpha
1279 subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty,
1281 res binds locals wanteds
1282 | Just tv <- tcGetTyVar_maybe ty
1285 = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+>
1288 -- create the substitution
1289 ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
1290 tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
1292 -- substitute into other wanted equalities (`substEq' makes sure
1293 -- that we only substitute into wanteds)
1294 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1295 ; res' <- mapM (substEq eq coSubst tySubst) res
1297 ; subst eqs' (eq:res') binds locals wanteds
1300 subst (eq:eqs) res binds locals wanteds
1301 = subst eqs (eq:res) binds locals wanteds
1303 -- We have, co :: tv ~ ty
1304 -- => apply [ty/tv] to right-hand side of eq2
1305 -- (but only if tv actually occurs in the right-hand side of eq2
1306 -- and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
1307 substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co})
1309 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1310 && (isWantedRewriteInst eq2 || not (isWantedCo co))
1311 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1312 right2' = substTy tySubst (rwi_right eq2)
1314 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1315 RewriteFam {rwi_fam = fam,
1316 rwi_args = args} ->mkTyConApp fam args
1317 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1319 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1320 -> occurCheckErr left2 right2'
1321 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1324 -- We have, co ::^w F t1..tn ~ tv
1325 -- => apply [F t1..tn/tv] to eq2
1326 -- (but only if tv actually occurs in eq2
1327 -- and eq2 is a wanted equality
1328 -- and we are either in checking mode or eq2 is a family equality)
1329 substEq (RewriteFam {rwi_args = args, rwi_right = ty})
1331 | Just tv <- tcGetTyVar_maybe ty
1332 , tv `elemVarSet` tyVarsOfRewriteInst eq2
1333 , isWantedRewriteInst eq2
1334 , checkingMode || not (isRewriteVar eq2)
1335 = do { -- substitute into the right-hand side
1336 ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1337 right2' = substTy tySubst (rwi_right eq2)
1339 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1340 RewriteFam {rwi_fam = fam,
1341 rwi_args = args} -> mkTyConApp fam args
1342 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1344 RewriteVar {rwi_var = tv2}
1345 -- variable equality: perform an occurs check
1346 | tv2 `elemVarSet` tyVarsOfTypes args
1347 -> occurCheckErr left2 right2'
1349 -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1350 RewriteFam {rwi_fam = fam}
1351 -- family equality: substitute also into the left-hand side
1352 -> do { let co1Subst = substTy coSubst left2
1353 args2' = substTys tySubst (rwi_args eq2)
1354 left2' = mkTyConApp fam args2'
1355 ; co2'' <- mkRightTransEqInstCo co2' co1Subst
1357 ; return $ eq2 {rwi_args = args2', rwi_right = right2',
1366 -- We have, co :: tv ~ ty
1367 -- => apply [ty/tv] to dictionary predicate
1368 -- (but only if tv actually occurs in the predicate)
1369 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1371 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1372 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1373 pred' = substPred tySubst (tci_pred dict)
1374 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1375 ; return (binds, dict')
1379 substDict _ _ _ _ dict
1380 = return (emptyBag, dict)
1381 -- !!!TODO: Still need to substitute into IP constraints.
1384 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1385 alpha, we record a binding of alpha with t or a, respectively, and for co :=
1386 id. We do the same for equalities of the form co :: F t1..tn ~ alpha unless
1387 we are in inference mode and alpha appears in the environment - i.e., it is
1388 not a flexible introduced by flattening locals or it is local, but was
1389 propagated into the environment by the instantiation of a variable equality.
1391 We proceed in two phases: (1) first we consider all variable equalities and then
1392 (2) we consider all family equalities. The two phase structure is required as
1393 the recorded variable equalities determine which skolems flexibles escape, and
1394 hence, which family equalities may be recorded as bindings.
1396 We return all wanted equalities for which we did not generate a binding.
1397 (These can be skolem variable equalities, cyclic variable equalities, and
1400 We don't update any meta variables. Instead, instantiation simply implies
1401 putting a type variable binding into the binding pool of TcM.
1404 * We may encounter filled flexibles due to the instant filling of local
1405 skolems in local-given constraints during flattening.
1406 * Be careful with SigTVs. They can only be instantiated with other SigTVs or
1410 bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
1411 bindAndExtract eqs checkingMode freeFlexibles
1412 = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
1413 4 (ppr eqs $$ ppr freeFlexibles)
1414 ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
1415 ; escapingSkolems <- getEscapingSkolems
1416 ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
1417 ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
1418 ; mapM rewriteInstToInst residuals2
1421 -- NB: we don't have to transitively chase the relation as the substitution
1422 -- process applied before generating the bindings was exhaustive
1424 = do { tybinds_rel <- getTcTyVarBindsRelation
1425 ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
1428 isFree (tv, _) = tv `elemVarSet` freeFlexibles
1430 -- co :: alpha ~ t or co :: a ~ alpha
1431 instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1432 = do { flexi_tv1 <- isFlexible tv1
1433 ; maybe_flexi_tv2 <- isFlexibleTy ty2
1434 ; case (flexi_tv1, maybe_flexi_tv2) of
1436 | isSigTyVar tv1 && isSigTyVar tv2
1437 -> -- co :: alpha ~ beta, where both a SigTvs
1438 doInst (rwi_swapped eq) tv1 ty2 co eq
1440 | Just tv2 <- tcGetTyVar_maybe ty2
1443 -> -- co :: alpha ~ a, where alpha is a SigTv
1444 doInst (rwi_swapped eq) tv1 ty2 co eq
1446 | not (isSigTyVar tv1)
1447 -> -- co :: alpha ~ t, where alpha is not a SigTv
1448 doInst (rwi_swapped eq) tv1 ty2 co eq
1452 -> -- co :: a ~ alpha, where alpha is a SigTv
1453 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1454 | not (isSigTyVar tv2)
1455 -> -- co :: a ~ alpha, where alpha is not a SigTv
1456 -- ('a' may be filled)
1457 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1458 _ -> return $ Just eq
1460 instVarEq eq = return $ Just eq
1462 -- co :: F args ~ alpha,
1463 -- and we are either in checking mode or alpha is a skolem flexible that
1465 instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1466 rwi_right = ty2, rwi_co = co})
1467 | Just tv2 <- tcGetTyVar_maybe ty2
1468 , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
1469 = do { flexi_tv2 <- isFlexible tv2
1472 doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1476 instFamEq _ eq = return $ Just eq
1478 -- tv is a meta var, but not a SigTV and not filled
1480 | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
1481 | otherwise = return False
1483 -- type is a tv that is a meta var, but not a SigTV and not filled
1485 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
1486 ; if flexi then return $ Just tv
1489 | otherwise = return Nothing
1491 doInst _swapped _tv _ty (Right ty) _eq
1492 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1493 doInst swapped tv ty (Left cotv) eq
1494 = do { lookupTV <- lookupTcTyVar tv
1495 ; bMeta swapped tv lookupTV ty cotv
1498 -- Try to create a binding for a meta variable. There is *no* need to
1499 -- consider reorienting the underlying equality; `checkOrientation'
1500 -- makes sure that we get variable-variable equalities only in the
1501 -- appropriate orientation.
1503 bMeta :: Bool -- is this a swapped equality?
1504 -> TcTyVar -- tyvar to instantiate
1505 -> LookupTyVarResult -- lookup result of that tyvar
1506 -> TcType -- to to instantiate tyvar with
1507 -> TcTyVar -- coercion tyvar of current equality
1508 -> TcM (Maybe RewriteInst) -- returns the original equality if
1509 -- the tyvar could not be instantiated,
1510 -- and hence, the equality must be kept
1512 -- meta variable has been filled already
1513 -- => this should never happen due to the use of `isFlexible' above
1514 bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1515 = pprPanic "TcTyFuns.bMeta" $
1516 ptext (sLit "flexible") <+> ppr tv <+>
1517 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1518 ptext (sLit "meant to fill with") <+> ppr ty
1520 -- type variable meets type variable
1521 -- => `checkOrientation' already ensures that it is fine to instantiate
1522 -- tv1 with tv2, but chase tv2's instantiations if necessary, so that
1523 -- we eventually can perform a kinds check in bMetaInst
1524 -- NB: tv's instantiations won't alter the orientation in which we
1525 -- want to instantiate as they either constitute a family
1526 -- application or are themselves due to a properly oriented
1528 bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
1529 = do { lookupTV2 <- lookupTcTyVar tv2
1531 IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
1532 DoneTv _ -> bMetaInst swapped tv1 ty cotv
1535 -- updatable meta variable meets non-variable type
1536 -- => occurs check, monotype check, and kinds match check, then bind
1537 bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
1538 = bMetaInst swapped tv non_tv_ty cotv
1540 bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
1542 -- We know `tv' can be instantiated; check that `ty' is alright for
1543 -- instantiating `tv' with and then record a binding; we return the
1544 -- original equality if it is cyclic through a synonym family
1545 bMetaInst swapped tv ty cotv
1546 = do { -- occurs + monotype check
1547 ; mb_ty' <- checkTauTvUpdate tv ty
1551 -- there may be a family in non_tv_ty due to an unzonked,
1552 -- but updated skolem for a local equality
1553 -- (cf `wantedToLocal')
1556 do { checkKinds swapped tv ty'
1557 ; bindMetaTyVar tv ty' -- bind meta var
1558 ; bindMetaTyVar cotv ty' -- bind co var
1565 %************************************************************************
1569 %************************************************************************
1571 The infamous couldn't match expected type soandso against inferred type
1572 somethingdifferent message.
1575 eqInstMisMatch :: Inst -> TcM a
1577 = ASSERT( isEqInst inst )
1578 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1580 (ty_act, ty_exp) = eqInstTys inst
1581 InstLoc _ _ ctxt = instLoc inst
1583 -----------------------
1584 failWithMisMatch :: TcType -> TcType -> TcM a
1585 -- Generate the message when two types fail to match,
1586 -- going to some trouble to make it helpful.
1587 -- The argument order is: actual type, expected type
1588 failWithMisMatch ty_act ty_exp
1589 = do { env0 <- tcInitTidyEnv
1590 ; ty_exp <- zonkTcType ty_exp
1591 ; ty_act <- zonkTcType ty_act
1592 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1595 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1596 misMatchMsg env0 (ty_act, ty_exp)
1597 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1598 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1599 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1601 ptext (sLit "against inferred type") <+> pp_act],
1602 nest 2 (extra_exp $$ extra_act),
1603 nest 2 (vcat (map pp_open_tc (nub open_tcs)))]
1604 -- See Note [Non-injective type functions]
1609 open_tcs = [tc | TyConApp tc _ <- [ty_act, ty_exp]
1611 pp_open_tc tc = ptext (sLit "NB:") <+> quotes (ppr tc)
1612 <+> ptext (sLit "is a type function") <> pp_inj
1614 pp_inj | isInjectiveTyCon tc = empty
1615 | otherwise = ptext (sLit (", and may not be injective"))
1617 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1619 = let (env1, tidy_ty) = tidyOpenType env ty
1620 (env2, extra) = ppr_extra env1 tidy_ty
1622 (env2, quotes (ppr tidy_ty), extra)
1624 -- (ppr_extra env ty) shows extra info about 'ty'
1625 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1626 ppr_extra env (TyVarTy tv)
1627 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1628 = (env1, pprSkolTvBinding tv1)
1630 (env1, tv1) = tidySkolemTyVar env tv
1632 ppr_extra env _ty = (env, empty) -- Normal case
1635 Note [Non-injective type functions]
1636 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1637 It's very confusing to get a message like
1638 Couldn't match expected type `Depend s'
1639 against inferred type `Depend s1'
1641 NB: `Depend' is type function, and hence may not be injective
1643 Currently we add this independently for each argument, so we also get
1644 Couldn't match expected type `a'
1645 against inferred type `Dual (Dual a)'
1646 NB: `Dual' is a (non-injective) type function
1647 which is arguably redundant. But on the other hand, it's probably
1648 a good idea for the programmer to know the error involves type functions
1649 so I've left it in for now. The obvious alternative is to only add
1650 this NB in the case of matching (T ...) ~ (T ...).
1653 Warn of loopy local equalities that were dropped.
1656 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1657 warnDroppingLoopyEquality ty1 ty2
1658 = do { env0 <- tcInitTidyEnv
1659 ; ty1 <- zonkTcType ty1
1660 ; ty2 <- zonkTcType ty2
1661 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1662 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1663 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1664 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))