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 { -- we only use the indexing arguments for matching,
73 -- not the additional ones
74 ; maybeFamInst <- tcLookupFamInst tycon idxTys
75 ; case maybeFamInst of
76 Nothing -> return Nothing
77 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
78 mkTyConApp coe_tc tys')
80 tys' = rep_tys ++ restTys
81 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
82 (tyConFamilyCoercion_maybe rep_tc)
86 (idxTys, restTys) = splitAt n tys
87 tcUnfoldSynFamInst _other = return Nothing
90 Normalise 'Type's and 'PredType's by unfolding type family applications where
91 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
93 tcNormaliseFamInst ty = (co, ty')
97 -- |Normalise the given type as far as possible with toplevel equalities.
98 -- This results in a coercion witnessing the type equality, in addition to the
101 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
102 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
105 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
106 apply the normalisation function gives as the first argument to every TyConApp
107 and every TyVarTy subterm.
109 tcGenericNormaliseFamInst fun ty = (co, ty')
112 This function is (by way of using smart constructors) careful to ensure that
113 the returned coercion is exactly IdCo (and not some semantically equivalent,
114 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
115 makes it easy for the caller to determine whether the type changed. BUT
116 even if we return IdCo, ty' may be *syntactically* different from ty due to
117 unfolded closed type synonyms (by way of tcCoreView). In the interest of
118 good error messages, callers should discard ty' in favour of ty in this case.
121 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
122 -- what to do with type functions and tyvars
123 -> TcType -- old type
124 -> TcM (CoercionI, TcType) -- (coercion, new type)
125 tcGenericNormaliseFamInst fun ty
126 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
127 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
128 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
129 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
130 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
131 ; case maybe_ty_co of
132 -- a matching family instance exists
134 do { let first_coi = mkTransCoI tycon_coi (ACo co)
135 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
136 ; let fix_coi = mkTransCoI first_coi rest_coi
137 ; return (fix_coi, nty)
139 -- no matching family instance exists
140 -- we do not do anything
141 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
143 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
144 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
145 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
146 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
148 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
149 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
150 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
151 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
153 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
154 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
155 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
157 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
159 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
160 ; res <- lookupTcTyVar tv
163 do { maybe_ty' <- fun ty
165 Nothing -> return (IdCo, ty)
167 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
168 ; return (ACo co1 `mkTransCoI` coi2, ty'')
171 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
175 tcGenericNormaliseFamInst fun (PredTy predty)
176 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
177 ; return (coi, PredTy pred') }
179 ---------------------------------
180 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
182 -> TcM (CoercionI, TcPredType)
184 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
185 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
186 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
188 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
189 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
190 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
192 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
193 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
194 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
195 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
199 %************************************************************************
201 Normalisation of instances wrt to equalities
203 %************************************************************************
206 tcReduceEqs :: [Inst] -- locals
208 -> TcM ([Inst], -- normalised locals (w/o equalities)
209 [Inst], -- normalised wanteds (including equalities)
210 TcDictBinds, -- bindings for all simplified dictionaries
211 Bool) -- whether any flexibles where instantiated
212 tcReduceEqs locals wanteds
213 = do { let (local_eqs , local_dicts) = partition isEqInst locals
214 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
215 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
216 ; eqCfg2 <- normaliseDicts False local_dicts
217 ; eqCfg3 <- normaliseDicts True wanteds_dicts
218 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
219 `unionEqConfig` eqCfg3)
220 ; finaliseEqsAndDicts eqCfg
225 %************************************************************************
227 Equality Configurations
229 %************************************************************************
231 We maintain normalised equalities together with the skolems introduced as
232 intermediates during flattening of equalities as well as
235 -- |Configuration of normalised equalities used during solving.
237 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
238 , locals :: [Inst] -- given dicts
239 , wanteds :: [Inst] -- wanted dicts
240 , binds :: TcDictBinds -- bindings
241 , skolems :: TyVarSet -- flattening skolems
244 addSkolems :: EqConfig -> TyVarSet -> EqConfig
245 addSkolems eqCfg newSkolems
246 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
248 addEq :: EqConfig -> RewriteInst -> EqConfig
249 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
251 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
252 unionEqConfig eqc1 eqc2 = EqConfig
253 { eqs = eqs eqc1 ++ eqs eqc2
254 , locals = locals eqc1 ++ locals eqc2
255 , wanteds = wanteds eqc1 ++ wanteds eqc2
256 , binds = binds eqc1 `unionBags` binds eqc2
257 , skolems = skolems eqc1 `unionVarSet` skolems eqc2
260 emptyEqConfig :: EqConfig
261 emptyEqConfig = EqConfig
266 , skolems = emptyVarSet
269 instance Outputable EqConfig where
270 ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
271 = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
274 The set of operations on an equality configuration. We obtain the initialise
275 configuration by normalisation ('normaliseEqs'), solve the equalities by
276 propagation ('propagateEqs'), and eventually finalise the configuration when
277 no further propoagation is possible.
280 -- |Turn a set of equalities into an equality configuration for solving.
282 -- Precondition: The Insts are zonked.
284 normaliseEqs :: [Inst] -> TcM EqConfig
286 = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )
287 ; traceTc $ ptext (sLit "Entering normaliseEqs")
289 ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
290 ; return $ emptyEqConfig { eqs = concat eqss
291 , skolems = unionVarSets skolemss
295 -- |Flatten the type arguments of all dictionaries, returning the result as a
296 -- equality configuration. The dictionaries go into the 'wanted' component if
297 -- the second argument is 'True'.
299 -- Precondition: The Insts are zonked.
301 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
302 normaliseDicts isWanted insts
303 = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
304 ptext (if isWanted then sLit "[Wanted] for"
305 else sLit "[Local] for"))
307 ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
310 ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
311 4 (ppr insts' $$ ppr eqss)
312 ; return $ emptyEqConfig { eqs = concat eqss
313 , locals = if isWanted then [] else insts'
314 , wanteds = if isWanted then insts' else []
315 , binds = unionManyBags bindss
316 , skolems = unionVarSets skolemss
320 -- |Solves the equalities as far as possible by applying propagation rules.
322 propagateEqs :: EqConfig -> TcM EqConfig
323 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
324 = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
327 ; propagate todoEqs (eqCfg {eqs = []})
330 -- |Finalise a set of equalities and associated dictionaries after
331 -- propagation. The returned Boolean value is `True' iff any flexible
332 -- variables, except those introduced by flattening (i.e., those in the
333 -- `skolems' component of the argument) where instantiated. The first returned
334 -- set of instances are the locals (without equalities) and the second set are
335 -- all residual wanteds, including equalities.
337 finaliseEqsAndDicts :: EqConfig
338 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
339 finaliseEqsAndDicts (EqConfig { eqs = eqs
345 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
346 ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
347 ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
348 ; let final_binds = subst_binds `unionBags` binds
350 -- Assert that all cotvs of wanted equalities are still unfilled, and
351 -- zonk all final insts, to make any improvement visible
352 ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
353 ; zonked_locals <- zonkInsts locals'
354 ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
355 ; return (zonked_locals, zonked_wanteds, final_binds, improved)
360 %************************************************************************
362 Normalisation of equalities
364 %************************************************************************
366 A normal equality is a properly oriented equality with associated coercion
367 that contains at most one family equality (in its left-hand side) is oriented
368 such that it may be used as a reqrite rule. It has one of the following two
371 (1) co :: F t1..tn ~ t (family equalities)
372 (2) co :: x ~ t (variable equalities)
374 Variable equalities fall again in two classes:
376 (2a) co :: x ~ t, where t is *not* a variable, or
377 (2b) co :: x ~ y, where x > y.
379 The types t, t1, ..., tn may not contain any occurrences of synonym
380 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
381 the right-hand side, and the relation x > y is an arbitrary, but total order
386 = RewriteVar -- Form (2) above
387 { rwi_var :: TyVar -- may be rigid or flexible
388 , rwi_right :: TcType -- contains no synonym family applications
389 , rwi_co :: EqInstCo -- the wanted or given coercion
391 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
392 , rwi_swapped :: Bool -- swapped orientation of original EqInst
394 | RewriteFam -- Forms (1) above
395 { rwi_fam :: TyCon -- synonym family tycon
396 , rwi_args :: [Type] -- contain no synonym family applications
397 , rwi_right :: TcType -- contains no synonym family applications
398 , rwi_co :: EqInstCo -- the wanted or given coercion
400 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
401 , rwi_swapped :: Bool -- swapped orientation of original EqInst
404 isWantedRewriteInst :: RewriteInst -> Bool
405 isWantedRewriteInst = isWantedCo . rwi_co
407 rewriteInstToInst :: RewriteInst -> TcM Inst
408 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
409 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
410 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
411 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
413 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
416 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
417 deriveEqInst rewrite ty1 ty2 co
418 = do { co_adjusted <- if not swapped then return co
419 else mkSymEqInstCo co (ty2, ty1)
423 , tci_co = co_adjusted
424 , tci_loc = rwi_loc rewrite
425 , tci_name = rwi_name rewrite
429 swapped = rwi_swapped rewrite
430 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
432 instance Outputable RewriteInst where
433 ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
434 = hsep [ pprEqInstCo co <+> text "::"
435 , ppr (mkTyConApp fam args)
439 ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
440 = hsep [ pprEqInstCo co <+> text "::"
446 pprEqInstCo :: EqInstCo -> SDoc
447 pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
448 pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
451 The following functions turn an arbitrary equality into a set of normal
452 equalities. This implements the WFlat and LFlat rules of the paper in one
453 sweep. However, we use flexible variables for both locals and wanteds, and
454 avoid to carry around the unflattening substitution \Sigma (for locals) by
455 already updating the skolems for locals with the family application that they
456 represent - i.e., they will turn into that family application on the next
457 zonking (which only happens after finalisation).
459 In a corresponding manner, normDict normalises class dictionaries by
460 extracting any synonym family applications and generation appropriate normal
463 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
464 we drop that equality and raise an error if it is a wanted or a warning if it
468 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
469 -- Normalise one equality.
471 = ASSERT( isEqInst inst )
472 do { traceTc $ ptext (sLit "normEqInst of ") <+>
473 pprEqInstCo co <+> text "::" <+>
474 ppr ty1 <+> text "~" <+> ppr ty2
475 ; res <- go ty1 ty2 co
476 ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
480 (ty1, ty2) = eqInstTys inst
481 co = eqInstCoercion inst
483 -- look through synonyms
484 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
485 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
487 -- left-to-right rule with type family head
488 go ty1@(TyConApp con args) ty2 co
489 | isOpenSynTyConApp ty1 -- only if not oversaturated
490 = mkRewriteFam False con args ty2 co
492 -- right-to-left rule with type family head
493 go ty1 ty2@(TyConApp con args) co
494 | isOpenSynTyConApp ty2 -- only if not oversaturated
495 = do { co' <- mkSymEqInstCo co (ty2, ty1)
496 ; mkRewriteFam True con args ty1 co'
499 -- no outermost family
501 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
502 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
503 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
504 sym_co2 = mkSymCoercion co2
506 ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
507 ; eqs <- checkOrientation ty1' ty2' co' inst
508 ; if isLoopyEquality eqs ty12_eqs'
509 then do { if isWantedCo (tci_co inst)
511 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
514 warnDroppingLoopyEquality ty1 ty2
515 ; return ([], emptyVarSet) -- drop the equality
518 return (eqs ++ ty12_eqs',
519 ty1_skolems `unionVarSet` ty2_skolems)
522 mkRewriteFam swapped con args ty2 co
523 = do { (args', cargs, args_eqss, args_skolemss)
524 <- mapAndUnzip4M (flattenType inst) args
525 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
526 ; let co1 = mkTyConApp con cargs
527 sym_co2 = mkSymCoercion co2
528 all_eqs = concat args_eqss ++ ty2_eqs
529 eqTys = (mkTyConApp con args', ty2')
530 ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
531 ; let thisRewriteFam = RewriteFam
536 , rwi_loc = tci_loc inst
537 , rwi_name = tci_name inst
538 , rwi_swapped = swapped
540 ; return $ (thisRewriteFam : all_eqs',
541 unionVarSets (ty2_skolems:args_skolemss))
544 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
545 -- have a variable equality with 'a' on the lhs as the first equality.
546 -- Then, check whether 'a' occurs in the lhs of any family equality
547 -- generated by flattening.
548 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
549 = any inRewriteFam eqs
551 inRewriteFam (RewriteFam {rwi_args = args})
552 = tv `elemVarSet` tyVarsOfTypes args
553 inRewriteFam _ = False
554 isLoopyEquality _ _ = False
556 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
557 -- Normalise one dictionary or IP constraint.
558 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
559 = do { (args', cargs, args_eqss, args_skolemss)
560 <- mapAndUnzip4M (flattenType inst) args
561 ; let rewriteCo = PredTy $ ClassP clas cargs
562 eqs = concat args_eqss
563 pred' = ClassP clas args'
565 then -- don't generate a binding if there is nothing to flatten
566 return (inst, [], emptyBag, emptyVarSet)
568 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
569 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
570 ; return (inst', eqs', bind, unionVarSets args_skolemss)
572 normDict _isWanted inst
573 = return (inst, [], emptyBag, emptyVarSet)
574 -- !!!TODO: Still need to normalise IP constraints.
576 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
577 -- Performs the occurs check, decomposition, and proper orientation
578 -- (returns a singleton, or an empty list in case of a trivial equality)
579 -- NB: We cannot assume that the two types already have outermost type
580 -- synonyms expanded due to the recursion in the case of type applications.
581 checkOrientation ty1 ty2 co inst
584 -- look through synonyms
585 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
586 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
588 -- identical types => trivial
591 = do { mkIdEqInstCo co ty1
595 -- two tvs, left greater => unchanged
596 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
598 = mkRewriteVar False tv1 ty2 co
600 -- two tvs, right greater => swap
602 = do { co' <- mkSymEqInstCo co (ty2, ty1)
603 ; mkRewriteVar True tv2 ty1 co'
606 -- only lhs is a tv => unchanged
607 go ty1@(TyVarTy tv1) ty2
608 | ty1 `tcPartOfType` ty2 -- occurs check!
609 = occurCheckErr ty1 ty2
611 = mkRewriteVar False tv1 ty2 co
613 -- only rhs is a tv => swap
614 go ty1 ty2@(TyVarTy tv2)
615 | ty2 `tcPartOfType` ty1 -- occurs check!
616 = occurCheckErr ty2 ty1
618 = do { co' <- mkSymEqInstCo co (ty2, ty1)
619 ; mkRewriteVar True tv2 ty1 co'
622 -- type applications => decompose
624 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
625 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
626 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
627 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
628 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
629 ; return $ eqs_l ++ eqs_r
631 -- !!!TODO: would be more efficient to handle the FunApp and the data
632 -- constructor application explicitly.
634 -- inconsistency => type error
636 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
639 mkRewriteVar swapped tv ty co = return [RewriteVar
643 , rwi_loc = tci_loc inst
644 , rwi_name = tci_name inst
645 , rwi_swapped = swapped
648 flattenType :: Inst -- context to get location & name
649 -> Type -- the type to flatten
650 -> TcM (Type, -- the flattened type
651 Coercion, -- coercion witness of flattening wanteds
652 [RewriteInst], -- extra equalities
653 TyVarSet) -- new intermediate skolems
654 -- Removes all family synonyms from a type by moving them into extra equalities
658 -- look through synonyms
659 go ty | Just ty' <- tcView ty
660 = do { (ty_flat, co, eqs, skolems) <- go ty'
662 then -- unchanged, keep the old type with folded synonyms
663 return (ty, ty, [], emptyVarSet)
665 return (ty_flat, co, eqs, skolems)
668 -- type variable => nothing to do
670 = return (ty, ty, [] , emptyVarSet)
672 -- type family application & family arity matches number of args
673 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
674 go ty@(TyConApp con args)
675 | isOpenSynTyConApp ty -- only if not oversaturated
676 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
677 ; alpha <- newFlexiTyVar (typeKind ty)
678 ; let alphaTy = mkTyVarTy alpha
679 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
680 ; let thisRewriteFam = RewriteFam
683 , rwi_right = alphaTy
684 , rwi_co = mkWantedCo cotv
685 , rwi_loc = tci_loc inst
686 , rwi_name = tci_name inst
690 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
691 thisRewriteFam : concat args_eqss,
692 unionVarSets args_skolemss `extendVarSet` alpha)
693 } -- adding new unflatten var inst
695 -- data constructor application => flatten subtypes
696 -- NB: Special cased for efficiency - could be handled as type application
697 go ty@(TyConApp con args)
698 | not (isOpenSynTyCon con) -- don't match oversaturated family apps
699 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
701 then -- unchanged, keep the old type with folded synonyms
702 return (ty, ty, [], emptyVarSet)
704 return (mkTyConApp con args',
705 mkTyConApp con cargs,
707 unionVarSets args_skolemss)
710 -- function type => flatten subtypes
711 -- NB: Special cased for efficiency - could be handled as type application
712 go ty@(FunTy ty_l ty_r)
713 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
714 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
715 ; if null eqs_l && null eqs_r
716 then -- unchanged, keep the old type with folded synonyms
717 return (ty, ty, [], emptyVarSet)
719 return (mkFunTy ty_l' ty_r',
722 skolems_l `unionVarSet` skolems_r)
725 -- type application => flatten subtypes
727 | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
728 -- need to use the smart split as ty may be an
729 -- oversaturated family application
730 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
731 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
732 ; if null eqs_l && null eqs_r
733 then -- unchanged, keep the old type with folded synonyms
734 return (ty, ty, [], emptyVarSet)
736 return (mkAppTy ty_l' ty_r',
739 skolems_l `unionVarSet` skolems_r)
742 -- forall type => panic if the body contains a type family
743 -- !!!TODO: As long as the family does not contain a quantified variable
744 -- we might pull it out, but what if it does contain a quantified
746 go ty@(ForAllTy _ body)
747 | null (tyFamInsts body)
748 = return (ty, ty, [] , emptyVarSet)
750 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
752 -- we should never see a predicate type
754 = panic "TcTyFuns.flattenType: unexpected PredType"
756 go _ = panic "TcTyFuns: suppress bogus warning"
758 adjustCoercions :: EqInstCo -- coercion of original equality
759 -> Coercion -- coercion witnessing the left rewrite
760 -> Coercion -- coercion witnessing the right rewrite
761 -> (Type, Type) -- types of flattened equality
762 -> [RewriteInst] -- equalities from flattening
763 -> TcM (EqInstCo, -- coercion for flattened equality
764 [RewriteInst]) -- final equalities from flattening
765 -- Depending on whether we flattened a local or wanted equality, that equality's
766 -- coercion and that of the new equalities produced during flattening are
768 adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
769 -- wanted => generate a fresh coercion variable for the flattened equality
770 = do { cotv' <- newMetaCoVar ty_l ty_r
771 ; writeMetaTyVar cotv $
772 (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
773 ; return (Left cotv', all_eqs)
776 adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
777 -- local => turn all new equalities into locals and update (but not zonk)
779 = do { all_eqs' <- mapM wantedToLocal all_eqs
780 ; return (co, all_eqs')
783 mkDictBind :: Inst -- original instance
784 -> Bool -- is this a wanted contraint?
785 -> Coercion -- coercion witnessing the rewrite
786 -> PredType -- coerced predicate
787 -> TcM (Inst, -- new inst
788 TcDictBinds) -- binding for coerced dictionary
789 mkDictBind dict isWanted rewriteCo pred
790 = do { dict' <- newDictBndr loc pred
791 -- relate the old inst to the new one
792 -- target_dict = source_dict `cast` st_co
793 ; let (target_dict, source_dict, st_co)
794 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
795 | otherwise = (dict', dict, rewriteCo)
797 -- co :: dict ~ dict'
798 -- hence, if isWanted
799 -- dict = dict' `cast` sym co
801 -- dict' = dict `cast` co
802 expr = HsVar $ instToId source_dict
803 cast_expr = HsWrap (WpCast st_co) expr
804 rhs = L (instLocSpan loc) cast_expr
805 binds = instToDictBind target_dict rhs
806 ; return (dict', binds)
811 -- gamma ::^l Fam args ~ alpha
812 -- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
813 -- (the update of alpha will not be apparent during propagation, as we
814 -- never follow the indirections of meta variables; it will be revealed
815 -- when the equality is zonked)
817 -- NB: It's crucial to update *both* alpha and gamma, as gamma may already
818 -- have escaped into some other coercions during normalisation.
820 wantedToLocal :: RewriteInst -> TcM RewriteInst
821 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
823 rwi_right = TyVarTy alpha,
824 rwi_co = Left gamma})
825 = do { writeMetaTyVar alpha (mkTyConApp fam args)
826 ; writeMetaTyVar gamma (mkTyConApp fam args)
827 ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
829 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
833 %************************************************************************
835 Propagation of equalities
837 %************************************************************************
839 Apply the propagation rules exhaustively.
842 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
843 propagate [] eqCfg = return eqCfg
844 propagate (eq:eqs) eqCfg
845 = do { optEqs <- applyTop eq
848 -- Top applied to 'eq' => retry with new equalities
849 Just (eqs2, skolems2)
850 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
852 -- Top doesn't apply => try subst rules with all other
853 -- equalities, after that 'eq' can go into the residual list
855 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
856 ; propagate eqs' (eqCfg' `addEq` eq)
860 applySubstRules :: RewriteInst -- currently considered eq
861 -> [RewriteInst] -- todo eqs list
862 -> EqConfig -- residual
863 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
864 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
865 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
866 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
867 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
868 eqConfig {eqs = unchangedEqs_r}
869 `addSkolems` (skolems_t `unionVarSet` skolems_r))
872 mapSubstRules :: RewriteInst -- try substituting this equality
873 -> [RewriteInst] -- into these equalities
874 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
876 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
877 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
881 = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
882 4 (ppr eq1 $$ ppr eq2)
884 -- try the SubstFam rule
885 ; optEqs <- applySubstFam eq1 eq2
887 Just (eqs, skolems) -> return (eqs, [], skolems)
889 { -- try the SubstVarVar rule
890 optEqs <- applySubstVarVar eq1 eq2
892 Just (eqs, skolems) -> return (eqs, [], skolems)
894 { -- try the SubstVarFam rule
895 optEqs <- applySubstVarFam eq1 eq2
897 Just eq -> return ([eq], [], emptyVarSet)
898 Nothing -> return ([], [eq2], emptyVarSet)
899 -- if no rule matches, we return the equlity we tried to
900 -- substitute into unchanged
904 Attempt to apply the Top rule. The rule is
908 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
910 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
912 Returns Nothing if the rule could not be applied. Otherwise, the resulting
913 equality is normalised and a list of the normal equalities is returned.
916 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
918 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
919 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
921 Nothing -> return Nothing
922 Just (lhs, rewrite_co)
923 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
924 ; eq' <- deriveEqInst eq lhs rhs co'
925 ; liftM Just $ normEqInst eq'
932 applyTop _ = return Nothing
935 Attempt to apply the SubstFam rule. The rule is
937 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
939 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
941 where co1 may be a wanted only if co2 is a wanted, too.
943 Returns Nothing if the rule could not be applied. Otherwise, the equality
944 co2' is normalised and a list of the normal equalities is returned. (The
945 equality co1 is not returned as it remain unaltered.)
948 applySubstFam :: RewriteInst
950 -> TcM (Maybe ([RewriteInst], TyVarSet))
951 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
952 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
954 -- rule matches => rewrite
955 | fam1 == fam2 && tcEqTypes args1 args2 &&
956 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
957 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
958 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
959 ; liftM Just $ normEqInst eq2'
962 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
963 | fam1 == fam2 && tcEqTypes args1 args2 &&
964 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
965 = return $ Just ([eq2], emptyVarSet)
970 co1 = eqInstCoType (rwi_co eq1)
973 applySubstFam _ _ = return Nothing
976 Attempt to apply the SubstVarVar rule. The rule is
978 co1 :: x ~ t & co2 :: x ~ s
980 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
982 where co1 may be a wanted only if co2 is a wanted, too.
984 Returns Nothing if the rule could not be applied. Otherwise, the equality
985 co2' is normalised and a list of the normal equalities is returned. (The
986 equality co1 is not returned as it remain unaltered.)
989 applySubstVarVar :: RewriteInst
991 -> TcM (Maybe ([RewriteInst], TyVarSet))
992 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
993 eq2@(RewriteVar {rwi_var = tv2})
995 -- rule matches => rewrite
997 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
998 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
999 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
1000 ; liftM Just $ normEqInst eq2'
1003 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1005 (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
1006 = return $ Just ([eq2], emptyVarSet)
1011 co1 = eqInstCoType (rwi_co eq1)
1014 applySubstVarVar _ _ = return Nothing
1017 Attempt to apply the SubstVarFam rule. The rule is
1019 co1 :: x ~ t & co2 :: F s1..sn ~ s
1021 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
1022 with co2 = [co1/x](F s1..sn) |> co2'
1024 where x occurs in F s1..sn. (co1 may be local or wanted.)
1026 Returns Nothing if the rule could not be applied. Otherwise, the equality
1027 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
1030 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
1032 -- rule matches => rewrite
1033 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
1034 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
1035 | tv1 `elemVarSet` tyVarsOfTypes args2
1036 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
1037 args2' = substTysWith [tv1] [rhs1] args2
1038 lhs2 = mkTyConApp fam2 args2'
1039 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
1040 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
1043 rhs1 = rwi_right eq1
1044 rhs2 = rwi_right eq2
1045 co1 = eqInstCoType (rwi_co eq1)
1048 -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
1049 applySubstVarFam (RewriteFam {rwi_args = args1})
1050 eq2@(RewriteVar {rwi_var = tv2})
1051 | tv2 `elemVarSet` tyVarsOfTypes args1
1054 applySubstVarFam _ _ = return Nothing
1058 %************************************************************************
1060 Finalisation of equalities
1062 %************************************************************************
1064 Exhaustive substitution of all variable equalities of the form co :: x ~ t
1065 (both local and wanted) into the left-hand sides of all other equalities. This
1066 may lead to recursive equalities; i.e., (1) we need to apply the substitution
1067 implied by one variable equality exhaustively before turning to the next and
1068 (2) we need an occurs check.
1070 We also apply the same substitutions to the local and wanted class and IP
1073 The treatment of flexibles in wanteds is quite subtle. We absolutely want to
1074 substitute them into right-hand sides of equalities, to avoid getting two
1075 competing instantiations for a type variables; e.g., consider
1077 F s ~ alpha, alpha ~ t
1079 If we don't substitute `alpha ~ t', we may instantiate t with `F s' instead.
1080 This would be bad as `F s' is less useful, eg, as an argument to a class
1083 However, there is no reason why we would want to *substitute* `alpha ~ t' into a
1084 class constraint. We rather wait until `alpha' is instantiated to `t` and
1085 save the extra dictionary binding that substitution would introduce.
1086 Moreover, we may substitute wanted equalities only into wanted dictionaries.
1089 * Given that we apply the substitution corresponding to a single equality
1090 exhaustively, before turning to the next, and because we eliminate recursive
1091 equalities, all opportunities for subtitution will have been exhausted after
1092 we have considered each equality once.
1095 substitute :: [RewriteInst] -- equalities
1096 -> [Inst] -- local class dictionaries
1097 -> [Inst] -- wanted class dictionaries
1098 -> TcM ([RewriteInst], -- equalities after substitution
1099 TcDictBinds, -- all newly generated dictionary bindings
1100 [Inst], -- local dictionaries after substitution
1101 [Inst]) -- wanted dictionaries after substitution
1102 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1104 subst [] res binds locals wanteds
1105 = return (res, binds, locals, wanteds)
1107 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1108 res binds locals wanteds
1109 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
1111 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1112 tySubst = zipOpenTvSubst [tv] [ty]
1113 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1114 ; res' <- mapM (substEq eq coSubst tySubst) res
1116 -- only susbtitute local equalities into local dictionaries
1117 ; (lbinds, locals') <- if not (isWantedCo co)
1120 (substDict eq coSubst tySubst False)
1125 -- flexible tvs in wanteds will be instantiated anyway, there is
1126 -- no need to substitute them into dictionaries
1127 ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
1130 (substDict eq coSubst tySubst True)
1133 return ([], wanteds)
1135 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1136 ; subst eqs' (eq:res') binds' locals' wanteds'
1138 subst (eq:eqs) res binds locals wanteds
1139 = subst eqs (eq:res) binds locals wanteds
1141 -- We have, co :: tv ~ ty
1142 -- => apply [ty/tv] to right-hand side of eq2
1143 -- (but only if tv actually occurs in the right-hand side of eq2)
1144 substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1146 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1147 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1148 right2' = substTy tySubst (rwi_right eq2)
1150 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1151 RewriteFam {rwi_fam = fam,
1152 rwi_args = args} ->mkTyConApp fam args
1153 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1155 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1156 -> occurCheckErr left2 right2'
1157 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1164 -- We have, co :: tv ~ ty
1165 -- => apply [ty/tv] to dictionary predicate
1166 -- (but only if tv actually occurs in the predicate)
1167 substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
1169 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1170 = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
1171 pred' = substPred tySubst (tci_pred dict)
1172 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1173 ; return (binds, dict')
1177 substDict _ _ _ _ dict
1178 = return (emptyBag, dict)
1179 -- !!!TODO: Still need to substitute into IP constraints.
1182 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1183 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1184 Return all remaining wanted equalities. The Boolean result component is True
1185 if at least one instantiation of a flexible that is *not* a skolem from
1186 flattening was performed.
1188 We need to instantiate all flexibles that arose as skolems during flattening
1189 of wanteds before we instantiate any other flexibles. Consider F delta ~
1190 alpha, F alpha ~ delta, where alpha is a skolem and delta a free flexible. We
1191 need to produce F (F delta) ~ delta (and not F (F alpha) ~ alpha). Otherwise,
1192 we may wrongly claim to having performed an improvement, which can lead to
1193 non-termination of the combined class-family solver.
1196 instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
1197 instantiateAndExtract eqs localsEmpty skolems
1198 = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
1199 4 (ppr eqs $$ ppr skolems)
1200 -- start by *only* instantiating skolem flexibles from flattening
1201 ; unflat_wanteds <- liftM catMaybes $
1202 mapM (inst (`elemVarSet` skolems)) wanteds
1203 -- only afterwards instantiate free flexibles
1204 ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds
1205 ; let improvement = length residuals < length unflat_wanteds
1206 ; residuals' <- mapM rewriteInstToInst residuals
1207 ; return (residuals', improvement)
1210 wanteds = filter (isWantedCo . rwi_co) eqs
1211 checkingMode = length eqs > length wanteds || not localsEmpty
1212 -- no local equalities or dicts => checking mode
1214 -- co :: alpha ~ t or co :: a ~ alpha
1215 inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1216 = do { flexi_tv1 <- isFlexible mayInst tv1
1217 ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2
1218 ; case (flexi_tv1, maybe_flexi_tv2) of
1220 -> -- co :: alpha ~ t
1221 doInst (rwi_swapped eq) tv1 ty2 co eq
1223 -> -- co :: a ~ alpha
1224 doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1225 _ -> return $ Just eq
1228 -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
1229 inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
1230 rwi_right = ty2, rwi_co = co})
1231 | Just tv2 <- tcGetTyVar_maybe ty2
1233 , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
1234 -- !!!FIXME: this is too liberal, even if tv2 is in
1235 -- skolems we shouldn't instantiate if tvs occurs
1236 -- in other equalities that may propagate it into the
1238 = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
1240 inst _mayInst eq = return $ Just eq
1242 -- tv is a meta var and not filled
1243 isFlexible mayInst tv
1244 | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
1245 | otherwise = return False
1247 -- type is a tv that is a meta var and not filled
1248 isFlexibleTy mayInst ty
1249 | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst tv
1250 ; if flexi then return $ Just tv
1253 | otherwise = return Nothing
1255 doInst _swapped _tv _ty (Right ty) _eq
1256 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1257 doInst swapped tv ty (Left cotv) eq
1258 = do { lookupTV <- lookupTcTyVar tv
1259 ; uMeta swapped tv lookupTV ty cotv
1262 -- meta variable has been filled already
1263 -- => keep the equality
1264 uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
1266 ptext (sLit "flexible") <+> ppr tv <+>
1267 ptext (sLit "already filled with") <+> ppr fill_ty <+>
1268 ptext (sLit "meant to fill with") <+> ppr ty
1272 -- type variable meets type variable
1273 -- => check that tv2 hasn't been updated yet and choose which to update
1274 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1276 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1279 = do { lookupTV2 <- lookupTcTyVar tv2
1282 uMeta swapped tv1 (DoneTv details1) ty cotv
1284 uMetaVar swapped tv1 details1 tv2 details2 cotv
1287 ------ Beyond this point we know that ty2 is not a type variable
1289 -- signature skolem meets non-variable type
1290 -- => cannot update (retain the equality)!
1291 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1294 -- updatable meta variable meets non-variable type
1295 -- => occurs check, monotype check, and kinds match check, then update
1296 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1297 = do { -- occurs + monotype check
1298 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1302 -- there may be a family in non_tv_ty due to an unzonked,
1303 -- but updated skolem for a local equality
1306 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1307 ; writeMetaTyVar cotv ty' -- update co var
1312 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1314 -- uMetaVar: unify two type variables
1315 -- meta variable meets skolem
1317 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1318 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1319 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1323 -- meta variable meets meta variable
1324 -- => be clever about which of the two to update
1325 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1326 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1327 = do { case (info1, info2) of
1328 -- Avoid SigTvs if poss
1329 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1330 (_, SigTv _) | k2_sub_k1 -> update_tv1
1332 (_, _) | k1_sub_k2 -> if k2_sub_k1 &&
1334 then update_tv1 -- Same kinds
1336 | k2_sub_k1 -> update_tv1
1337 | otherwise -> kind_err
1338 -- Update the variable with least kind info
1339 -- See notes on type inference in Kind.lhs
1340 -- The "nicer to" part only applies if the two kinds are the same,
1341 -- so we can choose which to do.
1343 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1347 -- Kinds should be guaranteed ok at this point
1348 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1349 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1351 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1352 unifyKindMisMatch k1 k2
1356 k1_sub_k2 = k1 `isSubKind` k2
1357 k2_sub_k1 = k2 `isSubKind` k1
1359 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1360 -- Try to update sys-y type variables in preference to ones
1361 -- gotten (say) by instantiating a polymorphic function with
1362 -- a user-written type sig
1364 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1368 %************************************************************************
1372 %************************************************************************
1374 The infamous couldn't match expected type soandso against inferred type
1375 somethingdifferent message.
1378 eqInstMisMatch :: Inst -> TcM a
1380 = ASSERT( isEqInst inst )
1381 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1383 (ty_act, ty_exp) = eqInstTys inst
1384 InstLoc _ _ ctxt = instLoc inst
1386 -----------------------
1387 failWithMisMatch :: TcType -> TcType -> TcM a
1388 -- Generate the message when two types fail to match,
1389 -- going to some trouble to make it helpful.
1390 -- The argument order is: actual type, expected type
1391 failWithMisMatch ty_act ty_exp
1392 = do { env0 <- tcInitTidyEnv
1393 ; ty_exp <- zonkTcType ty_exp
1394 ; ty_act <- zonkTcType ty_act
1395 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1398 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1399 misMatchMsg env0 (ty_act, ty_exp)
1400 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1401 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1402 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1404 ptext (sLit "against inferred type") <+> pp_act],
1405 nest 2 (extra_exp $$ extra_act)]
1410 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1412 = let (env1, tidy_ty) = tidyOpenType env ty
1413 (env2, extra) = ppr_extra env1 tidy_ty
1415 (env2, quotes (ppr tidy_ty), extra)
1417 -- (ppr_extra env ty) shows extra info about 'ty'
1418 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1419 ppr_extra env (TyVarTy tv)
1420 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1421 = (env1, pprSkolTvBinding tv1)
1423 (env1, tv1) = tidySkolemTyVar env tv
1425 ppr_extra env _ty = (env, empty) -- Normal case
1428 Warn of loopy local equalities that were dropped.
1431 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1432 warnDroppingLoopyEquality ty1 ty2
1433 = do { env0 <- tcInitTidyEnv
1434 ; ty1 <- zonkTcType ty1
1435 ; ty2 <- zonkTcType ty2
1436 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1437 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1438 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1439 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))