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(..) )
40 import SrcLoc ( Located(..) )
50 %************************************************************************
52 Normalisation of types wrt toplevel equality schemata
54 %************************************************************************
56 Unfold a single synonym family instance and yield the witnessing coercion.
57 Return 'Nothing' if the given type is either not synonym family instance
58 or is a synonym family instance that has no matching instance declaration.
59 (Applies only if the type family application is outermost.)
61 For example, if we have
63 :Co:R42T a :: T [a] ~ :R42T a
65 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
68 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
69 tcUnfoldSynFamInst (TyConApp tycon tys)
70 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
73 = do { -- we only use the indexing arguments for matching,
74 -- not the additional ones
75 ; maybeFamInst <- tcLookupFamInst tycon idxTys
76 ; case maybeFamInst of
77 Nothing -> return Nothing
78 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
79 mkTyConApp coe_tc tys')
81 tys' = rep_tys ++ restTys
82 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
83 (tyConFamilyCoercion_maybe rep_tc)
87 (idxTys, restTys) = splitAt n tys
88 tcUnfoldSynFamInst _other = return Nothing
91 Normalise 'Type's and 'PredType's by unfolding type family applications where
92 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
94 tcNormaliseFamInst ty = (co, ty')
98 -- |Normalise the given type as far as possible with toplevel equalities.
99 -- This results in a coercion witnessing the type equality, in addition to the
102 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
103 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
106 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
107 apply the normalisation function gives as the first argument to every TyConApp
108 and every TyVarTy subterm.
110 tcGenericNormaliseFamInst fun ty = (co, ty')
113 This function is (by way of using smart constructors) careful to ensure that
114 the returned coercion is exactly IdCo (and not some semantically equivalent,
115 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
116 makes it easy for the caller to determine whether the type changed. BUT
117 even if we return IdCo, ty' may be *syntactically* different from ty due to
118 unfolded closed type synonyms (by way of tcCoreView). In the interest of
119 good error messages, callers should discard ty' in favour of ty in this case.
122 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
123 -- what to do with type functions and tyvars
124 -> TcType -- old type
125 -> TcM (CoercionI, TcType) -- (coercion, new type)
126 tcGenericNormaliseFamInst fun ty
127 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
128 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
129 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
130 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
131 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
132 ; case maybe_ty_co of
133 -- a matching family instance exists
135 do { let first_coi = mkTransCoI tycon_coi (ACo co)
136 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
137 ; let fix_coi = mkTransCoI first_coi rest_coi
138 ; return (fix_coi, nty)
140 -- no matching family instance exists
141 -- we do not do anything
142 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
144 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
145 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
146 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
147 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
149 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
150 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
151 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
152 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
154 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
155 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
156 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
158 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
160 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
161 ; res <- lookupTcTyVar tv
164 do { maybe_ty' <- fun ty
166 Nothing -> return (IdCo, ty)
168 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
169 ; return (ACo co1 `mkTransCoI` coi2, ty'')
172 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
176 tcGenericNormaliseFamInst fun (PredTy predty)
177 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
178 ; return (coi, PredTy pred') }
180 ---------------------------------
181 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
183 -> TcM (CoercionI, TcPredType)
185 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
186 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
187 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
189 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
190 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
191 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
193 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
194 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
195 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
196 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
200 %************************************************************************
202 Normalisation of instances wrt to equalities
204 %************************************************************************
207 tcReduceEqs :: [Inst] -- locals
209 -> TcM ([Inst], -- normalised locals (w/o equalities)
210 [Inst], -- normalised wanteds (including equalities)
211 TcDictBinds, -- bindings for all simplified dictionaries
212 Bool) -- whether any flexibles where instantiated
213 tcReduceEqs locals wanteds
214 = do { let (local_eqs , local_dicts) = partition isEqInst locals
215 (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
216 ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
217 ; eqCfg2 <- normaliseDicts False local_dicts
218 ; eqCfg3 <- normaliseDicts True wanteds_dicts
219 ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2
220 `unionEqConfig` eqCfg3)
221 ; finaliseEqsAndDicts eqCfg
226 %************************************************************************
228 Equality Configurations
230 %************************************************************************
232 We maintain normalised equalities together with the skolems introduced as
233 intermediates during flattening of equalities as well as
235 !!!TODO: We probably now can do without the skolem set. It's not used during
236 finalisation in the current code.
239 -- |Configuration of normalised equalities used during solving.
241 data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
242 , locals :: [Inst] -- given dicts
243 , wanteds :: [Inst] -- wanted dicts
244 , binds :: TcDictBinds -- bindings
245 , skolems :: TyVarSet -- flattening skolems
248 addSkolems :: EqConfig -> TyVarSet -> EqConfig
249 addSkolems eqCfg newSkolems
250 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
252 addEq :: EqConfig -> RewriteInst -> EqConfig
253 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
255 unionEqConfig :: EqConfig -> EqConfig -> EqConfig
256 unionEqConfig eqc1 eqc2 = EqConfig
257 { eqs = eqs eqc1 ++ eqs eqc2
258 , locals = locals eqc1 ++ locals eqc2
259 , wanteds = wanteds eqc1 ++ wanteds eqc2
260 , binds = binds eqc1 `unionBags` binds eqc2
261 , skolems = skolems eqc1 `unionVarSet` skolems eqc2
264 emptyEqConfig :: EqConfig
265 emptyEqConfig = EqConfig
270 , skolems = emptyVarSet
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 isValidWantedEqInst eqs, ppr eqs )
287 ; traceTc $ ptext (sLit "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 $ ptext (sLit "normaliseDicts") <+>
304 ptext (if isWanted then sLit "[Wanted]" else sLit "[Local]")
305 ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted)
307 ; return $ emptyEqConfig { eqs = concat eqss
308 , locals = if isWanted then [] else insts'
309 , wanteds = if isWanted then insts' else []
310 , binds = unionManyBags bindss
311 , skolems = unionVarSets skolemss
315 -- |Solves the equalities as far as possible by applying propagation rules.
317 propagateEqs :: EqConfig -> TcM EqConfig
318 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
319 = do { traceTc $ ptext (sLit "propagateEqs")
320 ; propagate todoEqs (eqCfg {eqs = []})
323 -- |Finalise a set of equalities and associated dictionaries after
324 -- propagation. The returned Boolean value is `True' iff any flexible
325 -- variables, except those introduced by flattening (i.e., those in the
326 -- `skolems' component of the argument) where instantiated. The first returned
327 -- set of instances are the locals (without equalities) and the second set are
328 -- all residual wanteds, including equalities.
330 -- Remove all identity dictinary bindings (i.e., those whose source and target
331 -- dictionary are the same). This is important for termination, as
332 -- TcSimplify.reduceContext takes the presence of dictionary bindings as an
333 -- indicator that there was some improvement.
335 finaliseEqsAndDicts :: EqConfig
336 -> TcM ([Inst], [Inst], TcDictBinds, Bool)
337 finaliseEqsAndDicts (EqConfig { eqs = eqs
342 = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
343 ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
344 ; (eqs'', improved) <- instantiateAndExtract eqs'
345 ; final_binds <- filterM nonTrivialDictBind $
346 bagToList (subst_binds `unionBags` binds)
348 ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
349 ; return (locals', eqs'' ++ wanteds', listToBag final_binds, improved)
352 nonTrivialDictBind (L _ (VarBind { var_id = ide1
353 , var_rhs = L _ (HsWrap _ (HsVar ide2))}))
354 = do { ty1 <- zonkTcType (idType ide1)
355 ; ty2 <- zonkTcType (idType ide2)
356 ; return $ not (ty1 `tcEqType` ty2)
358 nonTrivialDictBind _ = return True
362 %************************************************************************
364 Normalisation of equalities
366 %************************************************************************
368 A normal equality is a properly oriented equality with associated coercion
369 that contains at most one family equality (in its left-hand side) is oriented
370 such that it may be used as a reqrite rule. It has one of the following two
373 (1) co :: F t1..tn ~ t (family equalities)
374 (2) co :: x ~ t (variable equalities)
376 Variable equalities fall again in two classes:
378 (2a) co :: x ~ t, where t is *not* a variable, or
379 (2b) co :: x ~ y, where x > y.
381 The types t, t1, ..., tn may not contain any occurrences of synonym
382 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
383 the right-hand side, and the relation x > y is an arbitrary, but total order
386 !!!TODO: We may need to keep track of swapping for error messages (and to
387 re-orient on finilisation).
391 = RewriteVar -- Form (2) above
392 { rwi_var :: TyVar -- may be rigid or flexible
393 , rwi_right :: TcType -- contains no synonym family applications
394 , rwi_co :: EqInstCo -- the wanted or given coercion
396 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
397 , rwi_swapped :: Bool -- swapped orientation of original EqInst
399 | RewriteFam -- Forms (1) above
400 { rwi_fam :: TyCon -- synonym family tycon
401 , rwi_args :: [Type] -- contain no synonym family applications
402 , rwi_right :: TcType -- contains no synonym family applications
403 , rwi_co :: EqInstCo -- the wanted or given coercion
405 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
406 , rwi_swapped :: Bool -- swapped orientation of original EqInst
409 isWantedRewriteInst :: RewriteInst -> Bool
410 isWantedRewriteInst = isWantedCo . rwi_co
412 rewriteInstToInst :: RewriteInst -> TcM Inst
413 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
414 = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
415 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
416 = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
418 -- Derive an EqInst based from a RewriteInst, possibly swapping the types
421 deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
422 deriveEqInst rewrite ty1 ty2 co
423 = do { co_adjusted <- if not swapped then return co
424 else mkSymEqInstCo co (ty2, ty1)
428 , tci_co = co_adjusted
429 , tci_loc = rwi_loc rewrite
430 , tci_name = rwi_name rewrite
434 swapped = rwi_swapped rewrite
435 (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
438 The following functions turn an arbitrary equality into a set of normal
439 equalities. This implements the WFlat and LFlat rules of the paper in one
440 sweep. However, we use flexible variables for both locals and wanteds, and
441 avoid to carry around the unflattening substitution \Sigma (for locals) by
442 already updating the skolems for locals with the family application that they
443 represent - i.e., they will turn into that family application on the next
444 zonking (which only happens after finalisation).
446 In a corresponding manner, normDict normalises class dictionaries by
447 extracting any synonym family applications and generation appropriate normal
450 Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
451 we drop that equality and raise an error if it is a wanted or a warning if it
455 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
456 -- Normalise one equality.
458 = ASSERT( isEqInst inst )
459 go ty1 ty2 (eqInstCoercion inst)
461 (ty1, ty2) = eqInstTys inst
463 -- look through synonyms
464 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
465 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
467 -- left-to-right rule with type family head
468 go (TyConApp con args) ty2 co
470 = mkRewriteFam False con args ty2 co
472 -- right-to-left rule with type family head
473 go ty1 ty2@(TyConApp con args) co
475 = do { co' <- mkSymEqInstCo co (ty2, ty1)
476 ; mkRewriteFam True con args ty1 co'
479 -- no outermost family
481 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
482 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
483 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
484 rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2
486 ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs
487 ; eqs <- checkOrientation ty1' ty2' co' inst
488 ; if isLoopyEquality eqs ty12_eqs'
489 then do { if isWantedCo (tci_co inst)
491 addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
494 warnDroppingLoopyEquality ty1 ty2
495 ; return ([], emptyVarSet) -- drop the equality
498 return (eqs ++ ty12_eqs',
499 ty1_skolems `unionVarSet` ty2_skolems)
502 mkRewriteFam swapped con args ty2 co
503 = do { (args', cargs, args_eqss, args_skolemss)
504 <- mapAndUnzip4M (flattenType inst) args
505 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
506 ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion`
508 all_eqs = concat args_eqss ++ ty2_eqs
509 eqTys = (mkTyConApp con args', ty2')
510 ; (co', all_eqs') <- adjustCoercions co rewriteCo eqTys all_eqs
511 ; let thisRewriteFam = RewriteFam
516 , rwi_loc = tci_loc inst
517 , rwi_name = tci_name inst
518 , rwi_swapped = swapped
520 ; return $ (thisRewriteFam : all_eqs',
521 unionVarSets (ty2_skolems:args_skolemss))
524 -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
525 -- have a variable equality with 'a' on the lhs as the first equality.
526 -- Then, check whether 'a' occurs in the lhs of any family equality
527 -- generated by flattening.
528 isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
529 = any inRewriteFam eqs
531 inRewriteFam (RewriteFam {rwi_args = args})
532 = tv `elemVarSet` tyVarsOfTypes args
533 inRewriteFam _ = False
534 isLoopyEquality _ _ = False
536 normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
537 -- Normalise one dictionary or IP constraint.
538 normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
539 = do { (args', cargs, args_eqss, args_skolemss)
540 <- mapAndUnzip4M (flattenType inst) args
541 ; let rewriteCo = PredTy $ ClassP clas cargs
542 eqs = concat args_eqss
543 pred' = ClassP clas args'
545 then -- don't generate a binding if there is nothing to flatten
546 return (inst, [], emptyBag, emptyVarSet)
548 ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
549 ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
550 ; return (inst', eqs', bind, unionVarSets args_skolemss)
552 normDict _isWanted inst
553 = return (inst, [], emptyBag, emptyVarSet)
554 -- !!!TODO: Still need to normalise IP constraints.
556 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
557 -- Performs the occurs check, decomposition, and proper orientation
558 -- (returns a singleton, or an empty list in case of a trivial equality)
559 -- NB: We cannot assume that the two types already have outermost type
560 -- synonyms expanded due to the recursion in the case of type applications.
561 checkOrientation ty1 ty2 co inst
564 -- look through synonyms
565 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
566 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
568 -- identical types => trivial
571 = do { mkIdEqInstCo co ty1
575 -- two tvs, left greater => unchanged
576 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
578 = mkRewriteVar False tv1 ty2 co
580 -- two tvs, right greater => swap
582 = do { co' <- mkSymEqInstCo co (ty2, ty1)
583 ; mkRewriteVar True tv2 ty1 co'
586 -- only lhs is a tv => unchanged
587 go ty1@(TyVarTy tv1) ty2
588 | ty1 `tcPartOfType` ty2 -- occurs check!
589 = occurCheckErr ty1 ty2
591 = mkRewriteVar False tv1 ty2 co
593 -- only rhs is a tv => swap
594 go ty1 ty2@(TyVarTy tv2)
595 | ty2 `tcPartOfType` ty1 -- occurs check!
596 = occurCheckErr ty2 ty1
598 = do { co' <- mkSymEqInstCo co (ty2, ty1)
599 ; mkRewriteVar True tv2 ty1 co'
602 -- type applications => decompose
604 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
605 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
606 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
607 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
608 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
609 ; return $ eqs_l ++ eqs_r
611 -- !!!TODO: would be more efficient to handle the FunApp and the data
612 -- constructor application explicitly.
614 -- inconsistency => type error
616 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
619 mkRewriteVar swapped tv ty co = return [RewriteVar
623 , rwi_loc = tci_loc inst
624 , rwi_name = tci_name inst
625 , rwi_swapped = swapped
628 flattenType :: Inst -- context to get location & name
629 -> Type -- the type to flatten
630 -> TcM (Type, -- the flattened type
631 Coercion, -- coercion witness of flattening wanteds
632 [RewriteInst], -- extra equalities
633 TyVarSet) -- new intermediate skolems
634 -- Removes all family synonyms from a type by moving them into extra equalities
638 -- look through synonyms
639 go ty | Just ty' <- tcView ty = go ty'
641 -- type variable => nothing to do
643 = return (ty, ty, [] , emptyVarSet)
645 -- type family application
646 -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
647 go ty@(TyConApp con args)
649 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
650 ; alpha <- newFlexiTyVar (typeKind ty)
651 ; let alphaTy = mkTyVarTy alpha
652 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
653 ; let thisRewriteFam = RewriteFam
656 , rwi_right = alphaTy
657 , rwi_co = mkWantedCo cotv
658 , rwi_loc = tci_loc inst
659 , rwi_name = tci_name inst
663 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
664 thisRewriteFam : concat args_eqss,
665 unionVarSets args_skolemss `extendVarSet` alpha)
666 } -- adding new unflatten var inst
668 -- data constructor application => flatten subtypes
669 -- NB: Special cased for efficiency - could be handled as type application
670 go (TyConApp con args)
671 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
672 ; return (mkTyConApp con args',
673 mkTyConApp con cargs,
675 unionVarSets args_skolemss)
678 -- function type => flatten subtypes
679 -- NB: Special cased for efficiency - could be handled as type application
681 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
682 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
683 ; return (mkFunTy ty_l' ty_r',
686 skolems_l `unionVarSet` skolems_r)
689 -- type application => flatten subtypes
691 -- | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
692 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
693 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
694 ; return (mkAppTy ty_l' ty_r',
697 skolems_l `unionVarSet` skolems_r)
700 -- forall type => panic if the body contains a type family
701 -- !!!TODO: As long as the family does not contain a quantified variable
702 -- we might pull it out, but what if it does contain a quantified
704 go ty@(ForAllTy _ body)
705 | null (tyFamInsts body)
706 = return (ty, ty, [] , emptyVarSet)
708 = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
710 -- we should never see a predicate type
712 = panic "TcTyFuns.flattenType: unexpected PredType"
714 adjustCoercions :: EqInstCo -- coercion of original equality
715 -> Coercion -- coercion witnessing the rewrite
716 -> (Type, Type) -- types of flattened equality
717 -> [RewriteInst] -- equalities from flattening
718 -> TcM (EqInstCo, -- coercion for flattened equality
719 [RewriteInst]) -- final equalities from flattening
720 -- Depending on whether we flattened a local or wanted equality, that equality's
721 -- coercion and that of the new equalities produced during flattening are
723 adjustCoercions co rewriteCo eqTys all_eqs
725 -- wanted => generate a fresh coercion variable for the flattened equality
727 = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys
728 ; return (co', all_eqs)
731 -- local => turn all new equalities into locals and update (but not zonk)
734 = do { all_eqs' <- mapM wantedToLocal all_eqs
735 ; return (co, all_eqs')
738 mkDictBind :: Inst -- original instance
739 -> Bool -- is this a wanted contraint?
740 -> Coercion -- coercion witnessing the rewrite
741 -> PredType -- coerced predicate
742 -> TcM (Inst, -- new inst
743 TcDictBinds) -- binding for coerced dictionary
744 mkDictBind dict isWanted rewriteCo pred
745 = do { dict' <- newDictBndr loc pred
746 -- relate the old inst to the new one
747 -- target_dict = source_dict `cast` st_co
748 ; let (target_dict, source_dict, st_co)
749 | isWanted = (dict, dict', mkSymCoercion rewriteCo)
750 | otherwise = (dict', dict, rewriteCo)
752 -- co :: dict ~ dict'
753 -- hence, if isWanted
754 -- dict = dict' `cast` sym co
756 -- dict' = dict `cast` co
757 expr = HsVar $ instToId source_dict
758 cast_expr = HsWrap (WpCast st_co) expr
759 rhs = L (instLocSpan loc) cast_expr
760 binds = instToDictBind target_dict rhs
761 ; return (dict', binds)
766 -- gamma :: Fam args ~ alpha
767 -- => alpha :: Fam args ~ alpha, with alpha := Fam args
768 -- (the update of alpha will not be apparent during propagation, as we
769 -- never follow the indirections of meta variables; it will be revealed
770 -- when the equality is zonked)
771 wantedToLocal :: RewriteInst -> TcM RewriteInst
772 wantedToLocal eq@(RewriteFam {rwi_fam = fam,
774 rwi_right = alphaTy@(TyVarTy alpha)})
775 = do { writeMetaTyVar alpha (mkTyConApp fam args)
776 ; return $ eq {rwi_co = mkGivenCo alphaTy}
778 wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
782 %************************************************************************
784 Propagation of equalities
786 %************************************************************************
788 Apply the propagation rules exhaustively.
791 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
792 propagate [] eqCfg = return eqCfg
793 propagate (eq:eqs) eqCfg
794 = do { optEqs <- applyTop eq
797 -- Top applied to 'eq' => retry with new equalities
798 Just (eqs2, skolems2)
799 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
801 -- Top doesn't apply => try subst rules with all other
802 -- equalities, after that 'eq' can go into the residual list
804 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
805 ; propagate eqs' (eqCfg' `addEq` eq)
809 applySubstRules :: RewriteInst -- currently considered eq
810 -> [RewriteInst] -- todo eqs list
811 -> EqConfig -- residual
812 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
813 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
814 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
815 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
816 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
817 eqConfig {eqs = unchangedEqs_r}
818 `addSkolems` (skolems_t `unionVarSet` skolems_r))
821 mapSubstRules :: RewriteInst -- try substituting this equality
822 -> [RewriteInst] -- into these equalities
823 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
825 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
826 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
830 = do { -- try the SubstFam rule
831 optEqs <- applySubstFam eq1 eq2
833 Just (eqs, skolems) -> return (eqs, [], skolems)
835 { -- try the SubstVarVar rule
836 optEqs <- applySubstVarVar eq1 eq2
838 Just (eqs, skolems) -> return (eqs, [], skolems)
840 { -- try the SubstVarFam rule
841 optEqs <- applySubstVarFam eq1 eq2
843 Just eq -> return ([eq], [], emptyVarSet)
844 Nothing -> return ([], [eq2], emptyVarSet)
845 -- if no rule matches, we return the equlity we tried to
846 -- substitute into unchanged
850 Attempt to apply the Top rule. The rule is
854 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
856 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
858 Returns Nothing if the rule could not be applied. Otherwise, the resulting
859 equality is normalised and a list of the normal equalities is returned.
862 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
864 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
865 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
867 Nothing -> return Nothing
868 Just (lhs, rewrite_co)
869 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
870 ; eq' <- deriveEqInst eq lhs rhs co'
871 ; liftM Just $ normEqInst eq'
878 applyTop _ = return Nothing
881 Attempt to apply the SubstFam rule. The rule is
883 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
885 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
887 where co1 may be a wanted only if co2 is a wanted, too.
889 Returns Nothing if the rule could not be applied. Otherwise, the equality
890 co2' is normalised and a list of the normal equalities is returned. (The
891 equality co1 is not returned as it remain unaltered.)
894 applySubstFam :: RewriteInst
896 -> TcM (Maybe ([RewriteInst], TyVarSet))
897 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
898 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
899 | fam1 == fam2 && tcEqTypes args1 args2 &&
900 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
901 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
902 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
903 -- !!!Should be ok and we don't want three type equalities.
904 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
905 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
906 ; liftM Just $ normEqInst eq2'
911 co1 = eqInstCoType (rwi_co eq1)
913 applySubstFam _ _ = return Nothing
916 Attempt to apply the SubstVarVar rule. The rule is
918 co1 :: x ~ t & co2 :: x ~ s
920 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
922 where co1 may be a wanted only if co2 is a wanted, too.
924 Returns Nothing if the rule could not be applied. Otherwise, the equality
925 co2' is normalised and a list of the normal equalities is returned. (The
926 equality co1 is not returned as it remain unaltered.)
929 applySubstVarVar :: RewriteInst
931 -> TcM (Maybe ([RewriteInst], TyVarSet))
932 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
933 eq2@(RewriteVar {rwi_var = tv2})
935 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
936 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
937 ; eq2' <- deriveEqInst eq2 lhs rhs co2'
938 ; liftM Just $ normEqInst eq2'
943 co1 = eqInstCoType (rwi_co eq1)
945 applySubstVarVar _ _ = return Nothing
948 Attempt to apply the SubstVarFam rule. The rule is
950 co1 :: x ~ t & co2 :: F s1..sn ~ s
952 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
953 with co2 = [co1/x](F s1..sn) |> co2'
955 where x occurs in F s1..sn. (co1 may be local or wanted.)
957 Returns Nothing if the rule could not be applied. Otherwise, the equality
958 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
961 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
962 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
963 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
964 | tv1 `elemVarSet` tyVarsOfTypes args2
965 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
966 args2' = substTysWith [tv1] [rhs1] args2
967 lhs2 = mkTyConApp fam2 args2'
968 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
969 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
974 co1 = eqInstCoType (rwi_co eq1)
976 applySubstVarFam _ _ = return Nothing
980 %************************************************************************
982 Finalisation of equalities
984 %************************************************************************
986 Exhaustive substitution of all variable equalities of the form co :: x ~ t
987 (both local and wanted) into the left-hand sides of all other equalities. This
988 may lead to recursive equalities; i.e., (1) we need to apply the substitution
989 implied by one variable equality exhaustively before turning to the next and
990 (2) we need an occurs check.
992 We also apply the same substitutions to the local and wanted class and IP
995 NB: Given that we apply the substitution corresponding to a single equality
996 exhaustively, before turning to the next, and because we eliminate recursive
997 equalities, all opportunities for subtitution will have been exhausted after
998 we have considered each equality once.
1001 substitute :: [RewriteInst] -- equalities
1002 -> [Inst] -- local class dictionaries
1003 -> [Inst] -- wanted class dictionaries
1004 -> TcM ([RewriteInst], -- equalities after substitution
1005 TcDictBinds, -- all newly generated dictionary bindings
1006 [Inst], -- local dictionaries after substitution
1007 [Inst]) -- wanted dictionaries after substitution
1008 substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
1010 subst [] res binds locals wanteds
1011 = return (res, binds, locals, wanteds)
1012 subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs)
1013 res binds locals wanteds
1014 = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+>
1015 ptext (sLit "->") <+> ppr ty
1016 ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
1017 tySubst = zipOpenTvSubst [tv] [ty]
1018 ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
1019 ; res' <- mapM (substEq eq coSubst tySubst) res
1020 ; (lbinds, locals') <- mapAndUnzipM
1021 (substDict eq coSubst tySubst False)
1023 ; (wbinds, wanteds') <- mapAndUnzipM
1024 (substDict eq coSubst tySubst True)
1026 ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
1027 ; subst eqs' (eq:res') binds' locals' wanteds'
1029 subst (eq:eqs) res binds locals wanteds
1030 = subst eqs (eq:res) binds locals wanteds
1032 -- We have, co :: tv ~ ty
1033 -- => apply [ty/tv] to right-hand side of eq2
1034 -- (but only if tv actually occurs in the right-hand side of eq2)
1035 substEq (RewriteVar {rwi_var = tv, rwi_right = ty})
1037 | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
1038 = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
1039 right2' = substTy tySubst (rwi_right eq2)
1041 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
1042 RewriteFam {rwi_fam = fam,
1043 rwi_args = args} ->mkTyConApp fam args
1044 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
1046 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
1047 -> occurCheckErr left2 right2'
1048 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
1055 -- We have, co :: tv ~ ty
1056 -- => apply [ty/tv] to dictionary predicate
1057 -- (but only if tv actually occurs in the predicate)
1058 substDict (RewriteVar {rwi_var = tv})
1059 coSubst tySubst isWanted dict
1061 , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
1062 = do { let co1Subst = mkSymCoercion $
1063 PredTy (substPred coSubst (tci_pred dict))
1064 pred' = substPred tySubst (tci_pred dict)
1065 ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
1066 ; return (binds, dict')
1070 substDict _ _ _ _ dict
1071 = return (emptyBag, dict)
1072 -- !!!TODO: Still need to substitute into IP constraints.
1075 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
1076 alpha, we instantiate alpha with t or a, respectively, and set co := id.
1077 Return all remaining wanted equalities. The Boolean result component is True
1078 if at least one instantiation of a flexible was performed.
1081 instantiateAndExtract :: [RewriteInst] -> TcM ([Inst], Bool)
1082 instantiateAndExtract eqs
1083 = do { let wanteds = filter (isWantedCo . rwi_co) eqs
1084 ; wanteds' <- mapM inst wanteds
1085 ; let residuals = catMaybes wanteds'
1086 improved = length wanteds /= length residuals
1087 ; residuals' <- mapM rewriteInstToInst residuals
1088 ; return (residuals', improved)
1091 inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
1095 = doInst (rwi_swapped eq) tv1 ty2 co eq
1098 | Just tv2 <- tcGetTyVar_maybe ty2
1100 = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
1102 inst eq = return $ Just eq
1104 doInst _swapped _tv _ty (Right ty) _eq
1105 = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
1106 doInst swapped tv ty (Left cotv) eq
1107 = do { lookupTV <- lookupTcTyVar tv
1108 ; uMeta swapped tv lookupTV ty cotv
1111 -- meta variable has been filled already
1112 -- => ignore (must be a skolem that was introduced by flattening locals)
1113 uMeta _swapped _tv (IndirectTv _) _ty _cotv
1116 -- type variable meets type variable
1117 -- => check that tv2 hasn't been updated yet and choose which to update
1118 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1120 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
1123 = do { lookupTV2 <- lookupTcTyVar tv2
1126 uMeta swapped tv1 (DoneTv details1) ty cotv
1128 uMetaVar swapped tv1 details1 tv2 details2 cotv
1131 ------ Beyond this point we know that ty2 is not a type variable
1133 -- signature skolem meets non-variable type
1134 -- => cannot update (retain the equality)!
1135 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1138 -- updatable meta variable meets non-variable type
1139 -- => occurs check, monotype check, and kinds match check, then update
1140 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1141 = do { -- occurs + monotype check
1142 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
1146 -- normalisation shouldn't leave families in non_tv_ty
1147 panic "TcTyFuns.uMeta: unexpected synonym family"
1149 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1150 ; writeMetaTyVar cotv ty' -- update co var
1155 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
1157 -- uMetaVar: unify two type variables
1158 -- meta variable meets skolem
1160 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1161 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1162 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1166 -- meta variable meets meta variable
1167 -- => be clever about which of the two to update
1168 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1169 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1170 = do { case (info1, info2) of
1171 -- Avoid SigTvs if poss
1172 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1173 (_, SigTv _) | k2_sub_k1 -> update_tv1
1175 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1176 then update_tv1 -- Same kinds
1178 | k2_sub_k1 -> update_tv1
1179 | otherwise -> kind_err
1180 -- Update the variable with least kind info
1181 -- See notes on type inference in Kind.lhs
1182 -- The "nicer to" part only applies if the two kinds are the same,
1183 -- so we can choose which to do.
1185 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1189 -- Kinds should be guaranteed ok at this point
1190 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1191 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1193 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1194 unifyKindMisMatch k1 k2
1198 k1_sub_k2 = k1 `isSubKind` k2
1199 k2_sub_k1 = k2 `isSubKind` k1
1201 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1202 -- Try to update sys-y type variables in preference to ones
1203 -- gotten (say) by instantiating a polymorphic function with
1204 -- a user-written type sig
1206 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1210 %************************************************************************
1214 %************************************************************************
1216 The infamous couldn't match expected type soandso against inferred type
1217 somethingdifferent message.
1220 eqInstMisMatch :: Inst -> TcM a
1222 = ASSERT( isEqInst inst )
1223 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1225 (ty_act, ty_exp) = eqInstTys inst
1226 InstLoc _ _ ctxt = instLoc inst
1228 -----------------------
1229 failWithMisMatch :: TcType -> TcType -> TcM a
1230 -- Generate the message when two types fail to match,
1231 -- going to some trouble to make it helpful.
1232 -- The argument order is: actual type, expected type
1233 failWithMisMatch ty_act ty_exp
1234 = do { env0 <- tcInitTidyEnv
1235 ; ty_exp <- zonkTcType ty_exp
1236 ; ty_act <- zonkTcType ty_act
1237 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1240 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1241 misMatchMsg env0 (ty_act, ty_exp)
1242 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1243 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1244 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1246 ptext (sLit "against inferred type") <+> pp_act],
1247 nest 2 (extra_exp $$ extra_act)]
1252 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
1254 = let (env1, tidy_ty) = tidyOpenType env ty
1255 (env2, extra) = ppr_extra env1 tidy_ty
1257 (env2, quotes (ppr tidy_ty), extra)
1259 -- (ppr_extra env ty) shows extra info about 'ty'
1260 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
1261 ppr_extra env (TyVarTy tv)
1262 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
1263 = (env1, pprSkolTvBinding tv1)
1265 (env1, tv1) = tidySkolemTyVar env tv
1267 ppr_extra env _ty = (env, empty) -- Normal case
1270 Warn of loopy local equalities that were dropped.
1273 warnDroppingLoopyEquality :: TcType -> TcType -> TcM ()
1274 warnDroppingLoopyEquality ty1 ty2
1275 = do { env0 <- tcInitTidyEnv
1276 ; ty1 <- zonkTcType ty1
1277 ; ty2 <- zonkTcType ty2
1278 ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
1279 (_env2, tidy_ty2) = tidyOpenType env1 ty2
1280 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
1281 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))