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 -- normalisation and solving of equalities
11 normaliseEqs, propagateEqs, finaliseEqs, normaliseDicts,
14 misMatchMsg, failWithMisMatch,
16 -- DEPRECATED: interface for the ICFP'08 algorithm
17 normaliseGivenEqs, normaliseGivenDicts,
18 normaliseWantedEqs, normaliseWantedDicts,
23 #include "HsVersions.h"
35 import TypeRep ( Type(..) )
44 import SrcLoc ( Located(..) )
54 %************************************************************************
56 Normalisation of types wrt toplevel equality schemata
58 %************************************************************************
60 Unfold a single synonym family instance and yield the witnessing coercion.
61 Return 'Nothing' if the given type is either not synonym family instance
62 or is a synonym family instance that has no matching instance declaration.
63 (Applies only if the type family application is outermost.)
65 For example, if we have
67 :Co:R42T a :: T [a] ~ :R42T a
69 then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
72 tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
73 tcUnfoldSynFamInst (TyConApp tycon tys)
74 | not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
77 = do { -- we only use the indexing arguments for matching,
78 -- not the additional ones
79 ; maybeFamInst <- tcLookupFamInst tycon idxTys
80 ; case maybeFamInst of
81 Nothing -> return Nothing
82 Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
83 mkTyConApp coe_tc tys')
85 tys' = rep_tys ++ restTys
86 coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
87 (tyConFamilyCoercion_maybe rep_tc)
91 (idxTys, restTys) = splitAt n tys
92 tcUnfoldSynFamInst _other = return Nothing
95 Normalise 'Type's and 'PredType's by unfolding type family applications where
96 possible (ie, we treat family instances as a TRS). Also zonk meta variables.
98 tcNormaliseFamInst ty = (co, ty')
102 -- |Normalise the given type as far as possible with toplevel equalities.
103 -- This results in a coercion witnessing the type equality, in addition to the
106 tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
107 tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
109 tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
110 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
113 %************************************************************************
115 Equality Configurations
117 %************************************************************************
119 We maintain normalised equalities together with the skolems introduced as
120 intermediates during flattening of equalities.
122 !!!TODO: Do we really need to keep track of the skolem variables? They are at
123 the moment not used in instantiateAndExtract, but it is hard to say until we
124 know exactly how finalisation will fianlly look like.
127 -- |Configuration of normalised equalities used during solving.
129 data EqConfig = EqConfig { eqs :: [RewriteInst]
130 , skolems :: TyVarSet
133 addSkolems :: EqConfig -> TyVarSet -> EqConfig
134 addSkolems eqCfg newSkolems
135 = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
137 addEq :: EqConfig -> RewriteInst -> EqConfig
138 addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
141 The set of operations on an equality configuration. We obtain the initialise
142 configuration by normalisation ('normaliseEqs'), solve the equalities by
143 propagation ('propagateEqs'), and eventually finalise the configuration when
144 no further propoagation is possible.
146 !!!TODO: Eventually, normalisation of dictionaries and dictionary
147 simplification should be included in propagation.
150 -- |Turn a set of equalities into an equality configuration for solving.
152 -- Precondition: The Insts are zonked.
154 normaliseEqs :: [Inst] -> TcM EqConfig
156 = do { (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
157 ; return $ EqConfig { eqs = concat eqss
158 , skolems = unionVarSets skolemss
162 -- |Solves the equalities as far as possible by applying propagation rules.
164 propagateEqs :: EqConfig -> TcM EqConfig
165 propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
166 = propagate todoEqs (eqCfg {eqs = []})
168 -- |Finalise a set of equalities after propagation. The Boolean value is
169 -- `True' iff any flexible variables, except those introduced by flattening
170 -- (i.e., those in the `skolems' component of the argument) where instantiated.
171 -- The returned set of instances are all residual wanteds.
173 finaliseEqs :: EqConfig -> TcM ([Inst], Bool)
174 finaliseEqs (EqConfig {eqs = eqs, skolems = skolems})
175 = do { eqs' <- substitute eqs
176 ; instantiateAndExtract eqs' skolems
179 -- |Normalise a set of class instances under a given equality configuration.
180 -- Both the class instances and the equality configuration may change. The
181 -- function returns 'Nothing' if neither changes.
183 normaliseDicts :: EqConfig -> [Inst] -> TcM (Maybe (EqConfig, [Inst]))
184 normaliseDicts = error "TcTyFuns.normaliseDicts"
188 %************************************************************************
190 Normalisation of equalities
192 %************************************************************************
194 A normal equality is a properly oriented equality with associated coercion
195 that contains at most one family equality (in its left-hand side) is oriented
196 such that it may be used as a reqrite rule. It has one of the following two
199 (1) co :: F t1..tn ~ t (family equalities)
200 (2) co :: x ~ t (variable equalities)
202 Variable equalities fall again in two classes:
204 (2a) co :: x ~ t, where t is *not* a variable, or
205 (2b) co :: x ~ y, where x > y.
207 The types t, t1, ..., tn may not contain any occurrences of synonym
208 families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
209 the right-hand side, and the relation x > y is an arbitrary, but total order
212 !!!TODO: We may need to keep track of swapping for error messages (and to
213 re-orient on finilisation).
217 = RewriteVar -- Form (2) above
218 { rwi_var :: TyVar -- may be rigid or flexible
219 , rwi_right :: TcType -- contains no synonym family applications
220 , rwi_co :: EqInstCo -- the wanted or given coercion
222 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
224 | RewriteFam -- Forms (1) above
225 { rwi_fam :: TyCon -- synonym family tycon
226 , rwi_args :: [Type] -- contain no synonym family applications
227 , rwi_right :: TcType -- contains no synonym family applications
228 , rwi_co :: EqInstCo -- the wanted or given coercion
230 , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
233 isWantedRewriteInst :: RewriteInst -> Bool
234 isWantedRewriteInst = isWantedCo . rwi_co
236 rewriteInstToInst :: RewriteInst -> Inst
237 rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
239 { tci_left = mkTyVarTy tv
240 , tci_right = rwi_right eq
242 , tci_loc = rwi_loc eq
243 , tci_name = rwi_name eq
245 rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
247 { tci_left = mkTyConApp fam args
248 , tci_right = rwi_right eq
250 , tci_loc = rwi_loc eq
251 , tci_name = rwi_name eq
255 The following functions turn an arbitrary equality into a set of normal
259 normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
261 = ASSERT( isEqInst inst )
262 go ty1 ty2 (eqInstCoercion inst)
264 (ty1, ty2) = eqInstTys inst
266 -- look through synonyms
267 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
268 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
270 -- left-to-right rule with type family head
271 go (TyConApp con args) ty2 co
273 = mkRewriteFam con args ty2 co
275 -- right-to-left rule with type family head
276 go ty1 ty2@(TyConApp con args) co
278 = do { co' <- mkSymEqInstCo co (ty2, ty1)
279 ; mkRewriteFam con args ty1 co'
282 -- no outermost family
284 = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
285 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
286 ; let ty12_eqs = ty1_eqs ++ ty2_eqs
287 rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2
289 ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs
290 ; eqs <- checkOrientation ty1' ty2' co' inst
291 ; return $ (eqs ++ ty12_eqs',
292 ty1_skolems `unionVarSet` ty2_skolems)
295 mkRewriteFam con args ty2 co
296 = do { (args', cargs, args_eqss, args_skolemss)
297 <- mapAndUnzip4M (flattenType inst) args
298 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
299 ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion`
301 all_eqs = concat args_eqss ++ ty2_eqs
302 eqTys = (mkTyConApp con args', ty2')
303 ; (co', all_eqs') <- adjustCoercions co rewriteCo eqTys all_eqs
304 ; let thisRewriteFam = RewriteFam
309 , rwi_loc = tci_loc inst
310 , rwi_name = tci_name inst
312 ; return $ (thisRewriteFam : all_eqs',
313 unionVarSets (ty2_skolems:args_skolemss))
316 checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
317 -- Performs the occurs check, decomposition, and proper orientation
318 -- (returns a singleton, or an empty list in case of a trivial equality)
319 -- NB: We cannot assume that the two types already have outermost type
320 -- synonyms expanded due to the recursion in the case of type applications.
321 checkOrientation ty1 ty2 co inst
324 -- look through synonyms
325 go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
326 go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
328 -- identical types => trivial
331 = do { mkIdEqInstCo co ty1
335 -- two tvs, left greater => unchanged
336 go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
338 = mkRewriteVar tv1 ty2 co
340 -- two tvs, right greater => swap
342 = do { co' <- mkSymEqInstCo co (ty2, ty1)
343 ; mkRewriteVar tv2 ty1 co'
346 -- only lhs is a tv => unchanged
347 go ty1@(TyVarTy tv1) ty2
348 | ty1 `tcPartOfType` ty2 -- occurs check!
349 = occurCheckErr ty1 ty2
351 = mkRewriteVar tv1 ty2 co
353 -- only rhs is a tv => swap
354 go ty1 ty2@(TyVarTy tv2)
355 | ty2 `tcPartOfType` ty1 -- occurs check!
356 = occurCheckErr ty2 ty1
358 = do { co' <- mkSymEqInstCo co (ty2, ty1)
359 ; mkRewriteVar tv2 ty1 co'
362 -- type applications => decompose
364 | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
365 , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
366 = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
367 ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
368 ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
369 ; return $ eqs_l ++ eqs_r
371 -- !!!TODO: would be more efficient to handle the FunApp and the data
372 -- constructor application explicitly.
374 -- inconsistency => type error
376 = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
379 mkRewriteVar tv ty co = return [RewriteVar
383 , rwi_loc = tci_loc inst
384 , rwi_name = tci_name inst
387 flattenType :: Inst -- context to get location & name
388 -> Type -- the type to flatten
389 -> TcM (Type, -- the flattened type
390 Coercion, -- coercion witness of flattening wanteds
391 [RewriteInst], -- extra equalities
392 TyVarSet) -- new intermediate skolems
393 -- Removes all family synonyms from a type by moving them into extra equalities
397 -- look through synonyms
398 go ty | Just ty' <- tcView ty = go ty'
400 -- type family application => flatten to "id :: F t1'..tn' ~ alpha"
401 go ty@(TyConApp con args)
403 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
404 ; alpha <- newFlexiTyVar (typeKind ty)
405 ; let alphaTy = mkTyVarTy alpha
406 ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
407 ; let thisRewriteFam = RewriteFam
410 , rwi_right = alphaTy
411 , rwi_co = mkWantedCo cotv
412 , rwi_loc = tci_loc inst
413 , rwi_name = tci_name inst
416 mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
417 thisRewriteFam : concat args_eqss,
418 unionVarSets args_skolemss `extendVarSet` alpha)
419 } -- adding new unflatten var inst
421 -- data constructor application => flatten subtypes
422 -- NB: Special cased for efficiency - could be handled as type application
423 go (TyConApp con args)
424 = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
425 ; return (mkTyConApp con args',
426 mkTyConApp con cargs,
428 unionVarSets args_skolemss)
431 -- function type => flatten subtypes
432 -- NB: Special cased for efficiency - could be handled as type application
434 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
435 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
436 ; return (mkFunTy ty_l' ty_r',
439 skolems_l `unionVarSet` skolems_r)
442 -- type application => flatten subtypes
444 -- | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
445 = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
446 ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
447 ; return (mkAppTy ty_l' ty_r',
450 skolems_l `unionVarSet` skolems_r)
453 -- free of type families => leave as is
455 = ASSERT( not . isForAllTy $ ty )
456 return (ty, ty, [] , emptyVarSet)
458 adjustCoercions :: EqInstCo -- coercion of original equality
459 -> Coercion -- coercion witnessing the rewrite
460 -> (Type, Type) -- type sof flattened equality
461 -> [RewriteInst] -- equalities from flattening
462 -> TcM (EqInstCo, -- coercion for flattened equality
463 [RewriteInst]) -- final equalities from flattening
464 -- Depending on whether we flattened a local or wanted equality, that equality's
465 -- coercion and that of the new ones are adjusted
466 adjustCoercions co rewriteCo eqTys all_eqs
468 = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys
469 ; return (co', all_eqs)
472 = return (co, map wantedToLocal all_eqs)
474 wantedToLocal eq = eq {rwi_co = mkGivenCo (rwi_right eq)}
478 %************************************************************************
480 Propagation of equalities
482 %************************************************************************
484 Apply the propagation rules exhaustively.
487 propagate :: [RewriteInst] -> EqConfig -> TcM EqConfig
488 propagate [] eqCfg = return eqCfg
489 propagate (eq:eqs) eqCfg
490 = do { optEqs <- applyTop eq
493 -- Top applied to 'eq' => retry with new equalities
494 Just (eqs2, skolems2)
495 -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
497 -- Top doesn't apply => try subst rules with all other
498 -- equalities, after that 'eq' can go into the residual list
500 -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
501 ; propagate eqs' (eqCfg' `addEq` eq)
505 applySubstRules :: RewriteInst -- currently considered eq
506 -> [RewriteInst] -- todo eqs list
507 -> EqConfig -- residual
508 -> TcM ([RewriteInst], EqConfig) -- new todo & residual
509 applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
510 = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
511 ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
512 ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
513 eqConfig {eqs = unchangedEqs_r}
514 `addSkolems` (skolems_t `unionVarSet` skolems_r))
517 mapSubstRules :: RewriteInst -- try substituting this equality
518 -> [RewriteInst] -- into these equalities
519 -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
521 = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
522 ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
526 = do { -- try the SubstFam rule
527 optEqs <- applySubstFam eq1 eq2
529 Just (eqs, skolems) -> return (eqs, [], skolems)
531 { -- try the SubstVarVar rule
532 optEqs <- applySubstVarVar eq1 eq2
534 Just (eqs, skolems) -> return (eqs, [], skolems)
536 { -- try the SubstVarFam rule
537 optEqs <- applySubstVarFam eq1 eq2
539 Just eq -> return ([eq], [], emptyVarSet)
540 Nothing -> return ([], [eq2], emptyVarSet)
541 -- if no rule matches, we return the equlity we tried to
542 -- substitute into unchanged
546 Attempt to apply the Top rule. The rule is
550 co' :: [s1/x1, .., sm/xm]s ~ t with co = g s1..sm |> co'
552 where g :: forall x1..xm. F u1..um ~ s and [s1/x1, .., sm/xm]u1 == t1.
554 Returns Nothing if the rule could not be applied. Otherwise, the resulting
555 equality is normalised and a list of the normal equalities is returned.
558 applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
560 applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
561 = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
563 Nothing -> return Nothing
564 Just (lhs, rewrite_co)
565 -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
570 , tci_loc = rwi_loc eq
571 , tci_name = rwi_name eq
573 ; liftM Just $ normEqInst eq'
580 applyTop _ = return Nothing
583 Attempt to apply the SubstFam rule. The rule is
585 co1 :: F t1..tn ~ t & co2 :: F t1..tn ~ s
587 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 |> co2'
589 where co1 may be a wanted only if co2 is a wanted, too.
591 Returns Nothing if the rule could not be applied. Otherwise, the equality
592 co2' is normalised and a list of the normal equalities is returned. (The
593 equality co1 is not returned as it remain unaltered.)
596 applySubstFam :: RewriteInst
598 -> TcM (Maybe ([RewriteInst], TyVarSet))
599 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
600 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
601 | fam1 == fam2 && tcEqTypes args1 args2 &&
602 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
603 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
604 -- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
605 -- !!!Should be ok and we don't want three type equalities.
606 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
611 , tci_loc = rwi_loc eq2
612 , tci_name = rwi_name eq2
614 ; liftM Just $ normEqInst eq2'
619 co1 = eqInstCoType (rwi_co eq1)
621 applySubstFam _ _ = return Nothing
624 Attempt to apply the SubstVarVar rule. The rule is
626 co1 :: x ~ t & co2 :: x ~ s
628 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 |> co2'
630 where co1 may be a wanted only if co2 is a wanted, too.
632 Returns Nothing if the rule could not be applied. Otherwise, the equality
633 co2' is normalised and a list of the normal equalities is returned. (The
634 equality co1 is not returned as it remain unaltered.)
637 applySubstVarVar :: RewriteInst
639 -> TcM (Maybe ([RewriteInst], TyVarSet))
640 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
641 eq2@(RewriteVar {rwi_var = tv2})
643 (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
644 = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
649 , tci_loc = rwi_loc eq2
650 , tci_name = rwi_name eq2
652 ; liftM Just $ normEqInst eq2'
657 co1 = eqInstCoType (rwi_co eq1)
659 applySubstVarVar _ _ = return Nothing
662 Attempt to apply the SubstVarFam rule. The rule is
664 co1 :: x ~ t & co2 :: F s1..sn ~ s
666 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s
667 with co2 = [co1/x](F s1..sn) |> co2'
669 where x occurs in F s1..sn. (co1 may be local or wanted.)
671 Returns Nothing if the rule could not be applied. Otherwise, the equality
672 co2' is returned. (The equality co1 is not returned as it remain unaltered.)
675 applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
676 applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
677 eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
678 | tv1 `elemVarSet` tyVarsOfTypes args2
679 = do { let co1Subst = substTyWith [tv1] [co1] (mkTyConApp fam2 args2)
680 args2' = substTysWith [tv1] [rhs1] args2
681 lhs2 = mkTyConApp fam2 args2'
682 ; co2' <- mkRightTransEqInstCo co2 co1Subst (lhs2, rhs2)
683 ; return $ Just (eq2 {rwi_args = args2', rwi_co = co2'})
688 co1 = eqInstCoType (rwi_co eq1)
690 applySubstVarFam _ _ = return Nothing
694 %************************************************************************
696 Finalisation of equalities
698 %************************************************************************
700 Exhaustive substitution of all variable equalities of the form co :: x ~ t
701 (both local and wanted) into the left-hand sides all other equalities. This
702 may lead to recursive equalities; i.e., (1) we need to apply the substitution
703 implied by one variable equality exhaustively before turning to the next and
704 (2) we need an occurs check.
706 NB: Gievn that we apply the substitution corresponding to a single equality
707 exhaustively, before turning to the next, and because we eliminate recursive
708 eqaulities, all opportunities for subtitution will have been exhausted after
709 we have considered each equality once.
712 substitute :: [RewriteInst] -> TcM [RewriteInst]
713 substitute eqs = subst eqs []
715 subst [] res = return res
717 = do { eqs' <- mapM (substOne eq) eqs
718 ; res' <- mapM (substOne eq) res
719 ; subst eqs' (eq:res')
722 -- apply [ty/tv] to left-hand side of eq2
723 substOne (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) eq2
724 = do { let co1Subst = mkSymCoercion $
725 substTyWith [tv] [eqInstCoType co] (rwi_right eq2)
726 right2' = substTyWith [tv] [ty] (rwi_right eq2)
728 RewriteVar {rwi_var = tv2} -> mkTyVarTy tv2
729 RewriteFam {rwi_fam = fam,
730 rwi_args = args} ->mkTyConApp fam args
731 ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
733 RewriteVar {rwi_var = tv2} | tv2 `elemVarSet` tyVarsOfType ty
734 -> occurCheckErr left2 right2'
735 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
743 For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
744 alpha, we instantiate alpha with t or a, respectively, and set co := id.
745 Return all remaining wanted equalities. The Boolean result component is True
746 if at least one instantiation of a flexible was performed.
749 instantiateAndExtract :: [RewriteInst] -> TyVarSet -> TcM ([Inst], Bool)
750 instantiateAndExtract eqs _skolems
751 = do { let wanteds = filter (isWantedCo . rwi_co) eqs
752 ; wanteds' <- mapM inst wanteds
753 ; let residuals = catMaybes wanteds'
754 improved = length wanteds /= length residuals
755 ; return (map rewriteInstToInst residuals, improved)
758 inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
762 = doInst tv1 ty2 co eq
765 | Just tv2 <- tcGetTyVar_maybe ty2
767 = doInst tv2 (mkTyVarTy tv1) co eq
769 inst eq = return $ Just eq
771 doInst _ _ (Right ty) _eq = pprPanic "TcTyFuns.doInst: local eq: "
773 doInst tv ty (Left cotv) eq = do { lookupTV <- lookupTcTyVar tv
774 ; uMeta False tv lookupTV ty cotv
777 -- meta variable has been filled already
778 -- => panic (all equalities should have been zonked on normalisation)
779 uMeta _swapped _tv (IndirectTv _) _ty _cotv
780 = panic "TcTyFuns.uMeta: expected zonked equalities"
782 -- type variable meets type variable
783 -- => check that tv2 hasn't been updated yet and choose which to update
784 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
786 = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
789 = do { lookupTV2 <- lookupTcTyVar tv2
792 uMeta swapped tv1 (DoneTv details1) ty cotv
794 uMetaVar swapped tv1 details1 tv2 details2 cotv
797 ------ Beyond this point we know that ty2 is not a type variable
799 -- signature skolem meets non-variable type
800 -- => cannot update (retain the equality)!
801 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
804 -- updatable meta variable meets non-variable type
805 -- => occurs check, monotype check, and kinds match check, then update
806 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
807 = do { -- occurs + monotype check
808 ; mb_ty' <- checkTauTvUpdate tv non_tv_ty
812 -- normalisation shouldn't leave families in non_tv_ty
813 panic "TcTyFuns.uMeta: unexpected synonym family"
815 do { checkUpdateMeta swapped tv ref ty' -- update meta var
816 ; writeMetaTyVar cotv ty' -- update co var
821 uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
823 -- uMetaVar: unify two type variables
824 -- meta variable meets skolem
826 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
827 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
828 ; writeMetaTyVar cotv (mkTyVarTy tv2)
832 -- meta variable meets meta variable
833 -- => be clever about which of the two to update
834 -- (from TcUnify.uUnfilledVars minus boxy stuff)
835 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
836 = do { case (info1, info2) of
837 -- Avoid SigTvs if poss
838 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
839 (_, SigTv _) | k2_sub_k1 -> update_tv1
841 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
842 then update_tv1 -- Same kinds
844 | k2_sub_k1 -> update_tv1
845 | otherwise -> kind_err
846 -- Update the variable with least kind info
847 -- See notes on type inference in Kind.lhs
848 -- The "nicer to" part only applies if the two kinds are the same,
849 -- so we can choose which to do.
851 ; writeMetaTyVar cotv (mkTyVarTy tv2)
855 -- Kinds should be guaranteed ok at this point
856 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
857 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
859 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
860 unifyKindMisMatch k1 k2
864 k1_sub_k2 = k1 `isSubKind` k2
865 k2_sub_k1 = k2 `isSubKind` k1
867 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
868 -- Try to update sys-y type variables in preference to ones
869 -- gotten (say) by instantiating a polymorphic function with
870 -- a user-written type sig
872 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
877 ==================== CODE FOR THE OLD ICFP'08 ALGORITHM ======================
879 An elementary rewrite is a properly oriented equality with associated coercion
880 that has one of the following two forms:
882 (1) co :: F t1..tn ~ t
883 (2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
885 NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
886 reqrite rule. Instead, such equalities are solved by unification. This is
887 essential; cf Note [skolemOccurs loop].
889 The following functions takes an equality instance and turns it into an
890 elementary rewrite if possible.
893 data Rewrite = Rewrite TcType -- lhs of rewrite rule
894 TcType -- rhs of rewrite rule
895 TcType -- coercion witnessing the rewrite rule
897 eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
898 -- True iff rewrite swapped equality
900 = ASSERT( isEqInst inst )
901 go ty1 ty2 (eqInstType inst)
903 (ty1,ty2) = eqInstTys inst
905 -- look through synonyms
906 go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
907 go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
909 -- left-to-right rule with type family head
910 go ty1@(TyConApp con _) ty2 co
912 = Just (Rewrite ty1 ty2 co, False) -- not swapped
914 -- left-to-right rule with type variable head
915 go ty1@(TyVarTy tv) ty2 co
917 = Just (Rewrite ty1 ty2 co, False) -- not swapped
919 -- right-to-left rule with type family head, only after
920 -- having checked whether we can work left-to-right
921 go ty1 ty2@(TyConApp con _) co
923 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
925 -- right-to-left rule with type variable head, only after
926 -- having checked whether we can work left-to-right
927 go ty1 ty2@(TyVarTy tv) co
929 = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
931 -- this equality is not a rewrite rule => ignore
935 Normalise a type relative to an elementary rewrite implied by an EqInst or an
936 explicitly given elementary rewrite.
940 -- Precondition: the EqInst passes the occurs check
941 tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
942 tcEqInstNormaliseFamInst inst ty
943 = case eqInstToRewrite inst of
944 Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
945 Nothing -> return (IdCo, ty)
947 -- Rewrite by equality rewrite rule
948 tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
949 -> TcType -- type to rewrite
950 -> TcM (CoercionI, -- witnessing coercion
951 TcType) -- rewritten type
952 tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
953 = tcGenericNormaliseFamInst matchEqRule ty
955 matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
956 | otherwise = return $ Nothing
959 Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
960 apply the normalisation function gives as the first argument to every TyConApp
961 and every TyVarTy subterm.
963 tcGenericNormaliseFamInst fun ty = (co, ty')
966 This function is (by way of using smart constructors) careful to ensure that
967 the returned coercion is exactly IdCo (and not some semantically equivalent,
968 but syntactically different coercion) whenever (ty' `tcEqType` ty). This
969 makes it easy for the caller to determine whether the type changed. BUT
970 even if we return IdCo, ty' may be *syntactically* different from ty due to
971 unfolded closed type synonyms (by way of tcCoreView). In the interest of
972 good error messages, callers should discard ty' in favour of ty in this case.
975 tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
976 -- what to do with type functions and tyvars
977 -> TcType -- old type
978 -> TcM (CoercionI, TcType) -- (coercion, new type)
979 tcGenericNormaliseFamInst fun ty
980 | Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
981 tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
982 = do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
983 ; let tycon_coi = mkTyConAppCoI tyCon ntys cois
984 ; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
985 ; case maybe_ty_co of
986 -- a matching family instance exists
988 do { let first_coi = mkTransCoI tycon_coi (ACo co)
989 ; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
990 ; let fix_coi = mkTransCoI first_coi rest_coi
991 ; return (fix_coi, nty)
993 -- no matching family instance exists
994 -- we do not do anything
995 Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
997 tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
998 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
999 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
1000 ; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
1002 tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
1003 = do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
1004 ; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
1005 ; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
1007 tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
1008 = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
1009 ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
1011 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
1013 = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
1014 ; res <- lookupTcTyVar tv
1017 do { maybe_ty' <- fun ty
1019 Nothing -> return (IdCo, ty)
1021 do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
1022 ; return (ACo co1 `mkTransCoI` coi2, ty'')
1025 IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
1029 tcGenericNormaliseFamInst fun (PredTy predty)
1030 = do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
1031 ; return (coi, PredTy pred') }
1033 ---------------------------------
1034 tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
1036 -> TcM (CoercionI, TcPredType)
1038 tcGenericNormaliseFamInstPred fun (ClassP cls tys)
1039 = do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
1040 ; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
1042 tcGenericNormaliseFamInstPred fun (IParam ipn ty)
1043 = do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
1044 ; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
1046 tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
1047 = do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
1048 ; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
1049 ; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
1053 %************************************************************************
1055 \section{Normalisation of equality constraints}
1057 %************************************************************************
1059 Note [Inconsistencies in equality constraints]
1060 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1061 We guarantee that we raise an error if we discover any inconsistencies (i.e.,
1062 equalities that if presented to the unifer in TcUnify would result in an
1063 error) during normalisation of wanted constraints. This is especially so that
1064 we don't solve wanted constraints under an inconsistent given set. In
1065 particular, we don't want to permit signatures, such as
1067 bad :: (Int ~ Bool => Int) -> a -> a
1070 normaliseGivenEqs :: [Inst] -> TcM ([Inst], TcM ())
1071 normaliseGivenEqs givens
1072 = do { traceTc (text "normaliseGivenEqs <-" <+> ppr givens)
1073 ; (result, deSkolem) <-
1074 rewriteToFixedPoint (Just ("(SkolemOccurs)", skolemOccurs))
1075 [ ("(ZONK)", dontRerun $ zonkInsts)
1076 , ("(TRIVIAL)", dontRerun $ trivialRule)
1077 , ("(DECOMP)", decompRule)
1078 , ("(TOP)", topRule)
1079 , ("(SUBST)", substRule) -- incl. occurs check
1081 ; traceTc (text "normaliseGivenEqs ->" <+> ppr result)
1082 ; return (result, deSkolem)
1087 normaliseWantedEqs :: [Inst] -- givens
1088 -> [Inst] -- wanteds
1089 -> TcM [Inst] -- irreducible wanteds
1090 normaliseWantedEqs givens wanteds
1091 = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds
1092 <+> text "with" <+> ppr givens
1093 ; result <- liftM fst $ rewriteToFixedPoint Nothing
1094 [ ("(ZONK)", dontRerun $ zonkInsts)
1095 , ("(TRIVIAL)", dontRerun $ trivialRule)
1096 , ("(DECOMP)", decompRule)
1097 , ("(TOP)", topRule)
1098 , ("(GIVEN)", substGivens givens) -- incl. occurs check
1099 , ("(UNIFY)", unifyMetaRule) -- incl. occurs check
1100 , ("(SUBST)", substRule) -- incl. occurs check
1102 ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
1106 -- Use `substInst' with every given on all the wanteds.
1107 substGivens :: [Inst] -> [Inst] -> TcM ([Inst], Bool)
1108 substGivens [] wanteds = return (wanteds, False)
1109 substGivens (g:gs) wanteds
1110 = do { (wanteds1, changed1) <- substGivens gs wanteds
1111 ; (wanteds2, changed2) <- substInst g wanteds1
1112 ; return (wanteds2, changed1 || changed2)
1117 %************************************************************************
1119 \section{Normalisation of non-equality dictionaries}
1121 %************************************************************************
1124 normaliseGivenDicts, normaliseWantedDicts
1125 :: [Inst] -- given equations
1126 -> [Inst] -- dictionaries
1127 -> TcM ([Inst],TcDictBinds)
1129 normaliseGivenDicts eqs dicts = normalise_dicts eqs dicts False
1130 normaliseWantedDicts eqs dicts = normalise_dicts eqs dicts True
1133 :: [Inst] -- given equations
1134 -> [Inst] -- dictionaries
1135 -> Bool -- True <=> the dicts are wanted
1136 -- Fals <=> they are given
1137 -> TcM ([Inst],TcDictBinds)
1138 normalise_dicts given_eqs dicts is_wanted
1139 = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
1140 | otherwise = "normaliseGivenDicts <-"
1142 text name <+> ppr dicts <+>
1143 text "with" <+> ppr given_eqs
1144 ; (dicts0, binds0) <- normaliseInsts is_wanted dicts
1145 ; (dicts1, binds1) <- substEqInDictInsts is_wanted given_eqs dicts0
1146 ; let binds01 = binds0 `unionBags` binds1
1147 ; if isEmptyBag binds1
1148 then return (dicts1, binds01)
1149 else do { (dicts2, binds2) <-
1150 normalise_dicts given_eqs dicts1 is_wanted
1151 ; return (dicts2, binds01 `unionBags` binds2) } }
1155 %************************************************************************
1157 \section{Normalisation rules and iterative rule application}
1159 %************************************************************************
1161 We have three kinds of normalising rewrite rules:
1163 (1) Normalisation rules that rewrite a set of insts and return a flag indicating
1164 whether any changes occurred during rewriting that necessitate re-running
1165 the current rule set.
1167 (2) Precondition rules that rewrite a set of insts and return a monadic action
1168 that reverts the effect of preconditioning.
1170 (3) Idempotent normalisation rules that never require re-running the rule set.
1173 type RewriteRule = [Inst] -> TcM ([Inst], Bool) -- rewrite, maybe re-run
1174 type PrecondRule = [Inst] -> TcM ([Inst], TcM ()) -- rewrite, revertable
1175 type IdemRewriteRule = [Inst] -> TcM [Inst] -- rewrite, don't re-run
1177 type NamedRule = (String, RewriteRule) -- rule with description
1178 type NamedPreRule = (String, PrecondRule) -- precond with desc
1181 Template lifting idempotent rules to full rules (which can be put into a rule
1185 dontRerun :: IdemRewriteRule -> RewriteRule
1186 dontRerun rule insts = liftM addFalse $ rule insts
1188 addFalse x = (x, False)
1191 The following function applies a set of rewrite rules until a fixed point is
1192 reached; i.e., none of the `RewriteRule's require re-running the rule set.
1193 Optionally, there may be a pre-conditing rule that is applied before any other
1194 rules are applied and before the rule set is re-run.
1196 The result is the set of rewritten (i.e., normalised) insts and, in case of a
1197 pre-conditing rule, a monadic action that reverts the effects of
1198 pre-conditioning - specifically, this is removing introduced skolems.
1201 rewriteToFixedPoint :: Maybe NamedPreRule -- optional preconditioning rule
1202 -> [NamedRule] -- rule set
1203 -> [Inst] -- insts to rewrite
1204 -> TcM ([Inst], TcM ())
1205 rewriteToFixedPoint precondRule rules insts
1206 = completeRewrite (return ()) precondRule insts
1208 completeRewrite :: TcM () -> Maybe NamedPreRule -> [Inst]
1209 -> TcM ([Inst], TcM ())
1210 completeRewrite dePrecond (Just (precondName, precond)) insts
1211 = do { traceTc $ text precondName <+> text " <- " <+> ppr insts
1212 ; (insts', dePrecond') <- precond insts
1213 ; traceTc $ text precondName <+> text " -> " <+> ppr insts'
1214 ; tryRules (dePrecond >> dePrecond') rules insts'
1216 completeRewrite dePrecond Nothing insts
1217 = tryRules dePrecond rules insts
1219 tryRules dePrecond _ [] = return ([] , dePrecond)
1220 tryRules dePrecond [] insts = return (insts, dePrecond)
1221 tryRules dePrecond ((name, rule):rules) insts
1222 = do { traceTc $ text name <+> text " <- " <+> ppr insts
1223 ; (insts', rerun) <- rule insts
1224 ; traceTc $ text name <+> text " -> " <+> ppr insts'
1225 ; if rerun then completeRewrite dePrecond precondRule insts'
1226 else tryRules dePrecond rules insts'
1231 %************************************************************************
1233 \section{Different forms of Inst rewrite rules}
1235 %************************************************************************
1237 Splitting of non-terminating given constraints: skolemOccurs
1238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1239 This is a preconditioning rule exclusively applied to given constraints.
1240 Moreover, its rewriting is only temporary, as it is undone by way of
1241 side-effecting mutable type variables after simplification and constraint
1242 entailment has been completed.
1244 This version is an (attempt at, yet unproven, an) *unflattened* version of
1245 the SubstL-Ev completion rule.
1247 The above rule is essential to catch non-terminating rules that cannot be
1248 oriented properly, like
1252 a ~ [G a] , where a is a skolem tyvar
1254 The left-to-right orientiation is not suitable because it does not
1255 terminate. The right-to-left orientation is not suitable because it
1256 does not have a type-function on the left. This is undesirable because
1257 it would hide information. E.g. assume
1261 then rewriting C [G (F a)] to C (F a) is bad because we cannot now
1262 see that the C [x] instance applies.
1264 The rule also caters for badly-oriented rules of the form:
1268 for which other solutions are possible, but this one will do too.
1272 co : ty1 ~ ty2{F ty1}
1275 sym (F co) : F ty2{b} ~ b
1276 where b is a fresh skolem variable
1278 We also cater for the symmetric situation *if* the rule cannot be used as a
1279 left-to-right rewrite rule.
1281 We also return an action (b := ty1) which is used to eliminate b
1282 after the dust of normalisation with the completed rewrite system
1285 A subtle point of this transformation is that both coercions in the results
1286 are strictly speaking incorrect. However, they are correct again after the
1287 action {B := ty1} has removed the skolem again. This happens immediately
1288 after constraint entailment has been checked; ie, code outside of the
1289 simplification and entailment checking framework will never see these
1290 temporarily incorrect coercions.
1292 NB: We perform this transformation for multiple occurences of ty1 under one
1293 or multiple family applications on the left-hand side at once (ie, the
1294 rule doesn't need to be applied multiple times at a single inst). As a
1295 result we can get two or more insts back.
1297 Note [skolemOccurs loop]
1298 ~~~~~~~~~~~~~~~~~~~~~~~~
1299 You might think that under
1302 type instance F [a] = [F a]
1306 foo :: (F [a] ~ a) => a
1308 will get us into a loop. However, this is *not* the case. Here is why:
1319 F [b<tau>] ~ b<tau> , with b := F a
1324 [F b<tau>] ~ b<tau> , with b := F a
1326 At this point (SkolemOccurs) does *not* apply anymore, as
1330 is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
1333 (The regression test indexed-types/should_compile/Simple20 checks that the
1334 described property of the system does not change.)
1337 skolemOccurs :: PrecondRule
1339 = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
1340 ; return (concat instss, sequence_ undoSkolems)
1343 oneSkolemOccurs inst
1344 = ASSERT( isEqInst inst )
1345 case eqInstToRewrite inst of
1346 Just (rewrite, swapped) -> breakRecursion rewrite swapped
1347 Nothing -> return ([inst], return ())
1349 -- inst is an elementary rewrite rule, check whether we need to break
1351 breakRecursion (Rewrite pat body _) swapped
1353 -- skolemOccurs does not apply, leave as is
1355 = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
1356 ; return ([inst], return ())
1359 -- recursive occurence of pat in body under a type family application
1361 = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
1362 ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
1363 ; let skTvs_tysTLO = zip skTvs tysToLiftOut
1364 insertSkolems = return . replace skTvs_tysTLO
1365 ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
1366 ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
1367 else mkEqInst (EqPred pat body') co
1368 -- ensure to reconstruct the inst in the
1369 -- original orientation
1370 ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
1371 ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
1373 ; return (inst':insts, sequence_ undoSk)
1376 co = eqInstCoercion inst
1378 -- all subtypes that are (1) type family instances and (2) contain
1379 -- the lhs type as part of the type arguments of the type family
1381 tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
1382 , any (pat `tcPartOfType`) tys]
1384 replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
1385 replace [] _ = Nothing
1386 replace ((skTv, tyTLO):rest) ty
1387 | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
1388 | otherwise = replace rest ty
1390 -- create the EqInst for the equality determining the skolem and a
1391 -- TcM action undoing the skolem introduction
1392 mkSkolemInst inst' (skTv, tyTLO)
1393 = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
1394 ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
1395 (mkGivenCo $ mkSymCoercion (fromACo co))
1396 -- co /= IdCo due to construction of inst'
1397 ; return (inst, writeMetaTyVar skTv tyTLO)
1402 Removal of trivial equalities: trivialRule
1403 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1404 The following rules exploits the reflexivity of equality:
1412 trivialRule :: IdemRewriteRule
1414 = liftM catMaybes $ mapM trivial insts
1417 | ASSERT( isEqInst inst )
1419 = do { eitherEqInst inst
1420 (\cotv -> writeMetaTyVar cotv ty1)
1425 = return $ Just inst
1427 (ty1,ty2) = eqInstTys inst
1431 Decomposition of data type constructors: decompRule
1432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1433 Whenever, the same *data* constructors occurs on both sides of an equality, we
1434 can decompose as in standard unification.
1439 g21 : c1 ~ d1, ..., g2n : cn ~ dn
1442 Works also for the case where T is actually an application of a type family
1443 constructor to a set of types, provided the applications on both sides of the
1444 ~ are identical; see also Note [OpenSynTyCon app] in TcUnify.
1446 We guarantee to raise an error for any inconsistent equalities;
1447 cf Note [Inconsistencies in equality constraints].
1450 decompRule :: RewriteRule
1452 = do { (insts, changed) <- mapAndUnzipM decomp insts
1453 ; return (concat insts, or changed)
1457 = ASSERT( isEqInst inst )
1460 (ty1,ty2) = eqInstTys inst
1462 | Just ty1' <- tcView ty1 = go ty1' ty2
1463 | Just ty2' <- tcView ty2 = go ty1 ty2'
1465 go (TyConApp con1 tys1) (TyConApp con2 tys2)
1466 | con1 == con2 && identicalHead
1467 = mkArgInsts (mkTyConApp con1) tys1 tys2
1469 | con1 /= con2 && not (isOpenSynTyCon con1 || isOpenSynTyCon con2)
1470 -- not matching data constructors (of any flavour) are bad news
1471 = eqInstMisMatch inst
1474 (idxTys1, _) = splitAt n tys1
1475 (idxTys2, _) = splitAt n tys2
1476 identicalHead = not (isOpenSynTyCon con1) ||
1477 idxTys1 `tcEqTypes` idxTys2
1479 go (FunTy fun1 arg1) (FunTy fun2 arg2)
1480 = mkArgInsts (\[funCo, argCo] -> mkFunTy funCo argCo) [fun1, arg1]
1483 -- Applications need a bit of care!
1484 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1485 go (AppTy s1 t1) ty2
1486 | Just (s2, t2) <- tcSplitAppTy_maybe ty2
1487 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
1490 go ty1 (AppTy s2 t2)
1491 | Just (s1, t1) <- tcSplitAppTy_maybe ty1
1492 = mkArgInsts (\[s, t] -> mkAppTy s t) [s1, t1] [s2, t2]
1494 -- We already covered all the consistent cases of rigid types on both
1495 -- sides; so, if we see two rigid types here, we discovered an
1498 | isRigid ty1 && isRigid ty2
1499 = eqInstMisMatch inst
1501 -- We can neither assert consistency nor inconsistency => defer
1502 go _ _ = return ([inst], False)
1504 isRigid (TyConApp con _) = not (isOpenSynTyCon con)
1505 isRigid (FunTy _ _) = True
1506 isRigid (AppTy _ _) = True
1509 -- Create insts for matching argument positions (ie, the bit after
1510 -- '>-->' in the rule description above)
1511 mkArgInsts con tys1 tys2
1512 = do { cos <- eitherEqInst inst
1513 -- old_co := Con1 cos
1515 do { cotvs <- zipWithM newMetaCoVar tys1 tys2
1516 ; let cos = map mkTyVarTy cotvs
1517 ; writeMetaTyVar old_covar (con cos)
1518 ; return $ map mkWantedCo cotvs
1520 -- co_i := Con_i old_co
1522 return $ map mkGivenCo $
1523 mkRightCoercions (length tys1) old_co)
1524 ; insts <- zipWithM mkEqInst (zipWith EqPred tys1 tys2) cos
1525 ; traceTc (text "decomp identicalHead" <+> ppr insts)
1526 ; return (insts, not $ null insts)
1531 Rewriting with type instances: topRule
1532 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1533 We use (toplevel) type instances to normalise both sides of equalities.
1537 >--> co1 :: t ~ t' / co2 :: s ~ s'
1539 g1 := co1 * g2 * sym co2
1542 topRule :: RewriteRule
1544 = do { (insts, changed) <- mapAndUnzipM top insts
1545 ; return (insts, or changed)
1549 = ASSERT( isEqInst inst )
1550 do { (coi1, ty1') <- tcNormaliseFamInst ty1
1551 ; (coi2, ty2') <- tcNormaliseFamInst ty2
1552 ; case (coi1, coi2) of
1553 (IdCo, IdCo) -> return (inst, False)
1557 -- old_co = co1 * new_co * sym co2
1559 do { new_cotv <- newMetaCoVar ty1' ty2'
1560 ; let new_co = mkTyVarTy new_cotv
1561 old_coi = coi1 `mkTransCoI`
1562 ACo new_co `mkTransCoI`
1564 ; writeMetaTyVar old_covar (fromACo old_coi)
1565 ; return $ mkWantedCo new_cotv
1567 -- new_co = sym co1 * old_co * co2
1572 mkSymCoI coi1 `mkTransCoI`
1573 ACo old_co `mkTransCoI` coi2)
1574 ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
1575 ; return (new_inst, True)
1579 (ty1,ty2) = eqInstTys inst
1583 Rewriting with equalities: substRule
1584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1585 From a set of insts, use all insts that can be read as rewrite rules to
1586 rewrite the types in all other insts.
1590 forall g1 : s1{F c} ~ s2{F c}
1593 g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
1595 Alternatively, the rewrite rule may have the form (g : a ~ t).
1597 To avoid having to swap rules of the form (g : t ~ F c) and (g : t ~ a),
1598 where t is neither a variable nor a type family application, we use them for
1599 rewriting from right-to-left. However, it is crucial to only apply rules
1600 from right-to-left if they cannot be used left-to-right.
1602 The workhorse is substInst, which performs an occurs check before actually
1603 using an equality for rewriting. If the type pattern occurs in the type we
1604 substitute for the pattern, normalisation would diverge.
1607 substRule :: RewriteRule
1608 substRule insts = tryAllInsts insts []
1610 -- for every inst check whether it can be used to rewrite the others
1611 -- (we make an effort to keep the insts in order; it makes debugging
1613 tryAllInsts [] triedInsts = return (reverse triedInsts, False)
1614 tryAllInsts (inst:insts) triedInsts
1615 = do { (insts', changed) <- substInst inst (reverse triedInsts ++ insts)
1616 ; if changed then return (insertAt (length triedInsts) inst insts',
1618 else tryAllInsts insts (inst:triedInsts)
1621 insertAt n x xs = let (xs1, xs2) = splitAt n xs
1622 in xs1 ++ [x] ++ xs2
1624 -- Use the given inst as a rewrite rule to normalise the insts in the second
1625 -- argument. Don't do anything if the inst cannot be used as a rewrite rule,
1626 -- but do apply it right-to-left, if possible, and if it cannot be used
1629 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
1630 substInst inst insts
1631 = case eqInstToRewrite inst of
1632 Just (rewrite, _) -> substEquality rewrite insts
1633 Nothing -> return (insts, False)
1635 substEquality :: Rewrite -- elementary rewrite
1636 -> [Inst] -- insts to rewrite
1637 -> TcM ([Inst], Bool)
1638 substEquality eqRule@(Rewrite pat rhs _) insts
1639 | pat `tcPartOfType` rhs -- occurs check!
1640 = occurCheckErr pat rhs
1642 = do { (insts', changed) <- mapAndUnzipM substOne insts
1643 ; return (insts', or changed)
1647 = ASSERT( isEqInst inst )
1648 do { (coi1, ty1') <- tcEqRuleNormaliseFamInst eqRule ty1
1649 ; (coi2, ty2') <- tcEqRuleNormaliseFamInst eqRule ty2
1650 ; case (coi1, coi2) of
1651 (IdCo, IdCo) -> return (inst, False)
1655 -- old_co := co1 * new_co * sym co2
1657 do { new_cotv <- newMetaCoVar ty1' ty2'
1658 ; let new_co = mkTyVarTy new_cotv
1659 old_coi = coi1 `mkTransCoI`
1660 ACo new_co `mkTransCoI`
1662 ; writeMetaTyVar old_covar (fromACo old_coi)
1663 ; return $ mkWantedCo new_cotv
1665 -- new_co := sym co1 * old_co * co2
1670 mkSymCoI coi1 `mkTransCoI`
1671 ACo old_co `mkTransCoI` coi2)
1672 ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
1673 ; return (new_inst, True)
1677 (ty1,ty2) = eqInstTys inst
1681 Instantiate meta variables: unifyMetaRule
1682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1683 If an equality equates a meta type variable with a type, we simply instantiate
1692 Meta variables can only appear in wanted constraints, and this rule should
1693 only be applied to wanted constraints. We also know that t definitely is
1694 distinct from alpha (as the trivialRule) has been run on the insts beforehand.
1696 NB: We cannot assume that meta tyvars are empty. They may have been updated
1697 by another inst in the currently processed wanted list. We need to be very
1698 careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
1699 we know that we have no boxes. It's unclear that it would be an advantage to
1700 common up the code in TcUnify and the code below. Firstly, we don't want
1701 calls to TcUnify.defer_unification here, and secondly, TcUnify import the
1702 current module, so we would have to move everything here (Yuk!) or to
1703 TcMType. Besides, the code here is much simpler due to the lack of boxes.
1706 unifyMetaRule :: RewriteRule
1708 = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
1709 ; return (concat insts', or changed)
1713 = ASSERT( isEqInst inst )
1715 (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
1717 (ty1,ty2) = eqInstTys inst
1719 | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
1720 | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
1722 | TyVarTy tv1 <- ty1
1723 , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
1724 ; uMeta False tv1 lookupTV ty2 cotv
1726 | TyVarTy tv2 <- ty2
1727 , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
1728 ; uMeta True tv2 lookupTV ty1 cotv
1730 | otherwise = return ([inst], False)
1732 -- meta variable has been filled already
1733 -- => ignore this inst (we'll come around again, after zonking)
1734 uMeta _swapped _tv (IndirectTv _) _ty _cotv
1735 = return ([inst], False)
1737 -- type variable meets type variable
1738 -- => check that tv2 hasn't been updated yet and choose which to update
1739 uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
1741 = return ([inst], False) -- The two types are already identical
1744 = do { lookupTV2 <- lookupTcTyVar tv2
1746 IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
1747 DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
1750 ------ Beyond this point we know that ty2 is not a type variable
1752 -- signature skolem meets non-variable type
1753 -- => cannot update!
1754 uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
1755 = return ([inst], False)
1757 -- updatable meta variable meets non-variable type
1758 -- => occurs check, monotype check, and kinds match check, then update
1759 uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
1760 = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check
1762 Nothing -> return ([inst], False) -- tv occurs in faminst
1764 do { checkUpdateMeta swapped tv ref ty' -- update meta var
1765 ; writeMetaTyVar cotv ty' -- update co var
1770 uMeta _ _ _ _ _ = panic "uMeta"
1772 -- uMetaVar: unify two type variables
1773 -- meta variable meets skolem
1775 uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
1776 = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
1777 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1781 -- meta variable meets meta variable
1782 -- => be clever about which of the two to update
1783 -- (from TcUnify.uUnfilledVars minus boxy stuff)
1784 uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
1785 = do { case (info1, info2) of
1786 -- Avoid SigTvs if poss
1787 (SigTv _, _ ) | k1_sub_k2 -> update_tv2
1788 (_, SigTv _) | k2_sub_k1 -> update_tv1
1790 (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
1791 then update_tv1 -- Same kinds
1793 | k2_sub_k1 -> update_tv1
1794 | otherwise -> kind_err
1795 -- Update the variable with least kind info
1796 -- See notes on type inference in Kind.lhs
1797 -- The "nicer to" part only applies if the two kinds are the same,
1798 -- so we can choose which to do.
1800 ; writeMetaTyVar cotv (mkTyVarTy tv2)
1804 -- Kinds should be guaranteed ok at this point
1805 update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
1806 update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
1808 kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
1809 unifyKindMisMatch k1 k2
1813 k1_sub_k2 = k1 `isSubKind` k2
1814 k2_sub_k1 = k2 `isSubKind` k1
1816 nicer_to_update_tv1 = isSystemName (Var.varName tv1)
1817 -- Try to update sys-y type variables in preference to ones
1818 -- gotten (say) by instantiating a polymorphic function with
1819 -- a user-written type sig
1821 uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
1825 %************************************************************************
1827 \section{Normalisation of Insts}
1829 %************************************************************************
1831 Normalises a set of dictionaries relative to a set of given equalities (which
1832 are interpreted as rewrite rules). We only consider given equalities of the
1837 where F is a type family.
1840 substEqInDictInsts :: Bool -- whether the *dictionaries* are wanted/given
1841 -> [Inst] -- given equalities (used as rewrite rules)
1842 -> [Inst] -- dictinaries to be normalised
1843 -> TcM ([Inst], TcDictBinds)
1844 substEqInDictInsts isWanted eqInsts dictInsts
1845 = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
1847 foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
1848 ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
1852 -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
1853 rewriteWithOneEquality (dictInsts, dictBinds)
1854 eqInst@(EqInst {tci_left = pattern,
1855 tci_right = target})
1856 | isOpenSynTyConApp pattern || isTyVarTy pattern
1857 = do { (dictInsts', moreDictBinds) <-
1858 genericNormaliseInsts isWanted applyThisEq dictInsts
1859 ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
1862 applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
1864 -- rewrite in case of an exact match
1865 matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
1866 | otherwise = Nothing
1868 -- (2) Given equality has the wrong form: ignore
1869 rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
1870 = return (dictInsts, dictBinds)
1874 Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
1875 type-function equations, where
1877 (norm_insts, binds) = normaliseInsts is_wanted insts
1880 = True, (binds + norm_insts) defines insts (wanteds)
1881 = False, (binds + insts) defines norm_insts (givens)
1883 Ie, in the case of normalising wanted dictionaries, we use the normalised
1884 dictionaries to define the originally wanted ones. However, in the case of
1885 given dictionaries, we use the originally given ones to define the normalised
1889 normaliseInsts :: Bool -- True <=> wanted insts
1890 -> [Inst] -- wanted or given insts
1891 -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
1892 normaliseInsts isWanted insts
1893 = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
1895 genericNormaliseInsts :: Bool -- True <=> wanted insts
1896 -> (TcPredType -> TcM (CoercionI, TcPredType))
1898 -> [Inst] -- wanted or given insts
1899 -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
1900 genericNormaliseInsts isWanted fun insts
1901 = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
1902 ; return (insts', unionManyBags binds)
1905 normaliseOneInst isWanted fun
1906 dict@(Dict {tci_pred = pred,
1908 = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
1909 ; (coi, pred') <- fun pred
1913 do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
1914 ; return (dict, emptyBag)
1916 -- don't use pred' in this case; otherwise, we get
1917 -- more unfolded closed type synonyms in error messages
1919 do { -- an inst for the new pred
1920 ; dict' <- newDictBndr loc pred'
1921 -- relate the old inst to the new one
1922 -- target_dict = source_dict `cast` st_co
1923 ; let (target_dict, source_dict, st_co)
1924 | isWanted = (dict, dict', mkSymCoercion co)
1925 | otherwise = (dict', dict, co)
1927 -- co :: dict ~ dict'
1928 -- hence, if isWanted
1929 -- dict = dict' `cast` sym co
1931 -- dict' = dict `cast` co
1932 expr = HsVar $ instToId source_dict
1933 cast_expr = HsWrap (WpCast st_co) expr
1934 rhs = L (instLocSpan loc) cast_expr
1935 binds = instToDictBind target_dict rhs
1936 -- return the new inst
1937 ; traceTc $ let name | isWanted
1938 = "genericNormaliseInst (wanted) ->"
1940 = "genericNormaliseInst (given) ->"
1942 text name <+> ppr dict' <+>
1943 text "with" <+> ppr binds
1944 ; return (dict', binds)
1948 -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
1949 normaliseOneInst _isWanted _fun inst
1950 = do { inst' <- zonkInst inst
1951 ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
1953 ; return (inst', emptyBag)
1958 %************************************************************************
1962 %************************************************************************
1964 The infamous couldn't match expected type soandso against inferred type
1965 somethingdifferent message.
1968 eqInstMisMatch :: Inst -> TcM a
1970 = ASSERT( isEqInst inst )
1971 setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
1973 (ty_act, ty_exp) = eqInstTys inst
1974 InstLoc _ _ ctxt = instLoc inst
1976 -----------------------
1977 failWithMisMatch :: TcType -> TcType -> TcM a
1978 -- Generate the message when two types fail to match,
1979 -- going to some trouble to make it helpful.
1980 -- The argument order is: actual type, expected type
1981 failWithMisMatch ty_act ty_exp
1982 = do { env0 <- tcInitTidyEnv
1983 ; ty_exp <- zonkTcType ty_exp
1984 ; ty_act <- zonkTcType ty_act
1985 ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
1988 misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
1989 misMatchMsg env0 (ty_act, ty_exp)
1990 = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
1991 (env2, pp_act, extra_act) = ppr_ty env1 ty_act
1992 msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp,
1994 ptext (sLit "against inferred type") <+> pp_act],
1995 nest 2 (extra_exp $$ extra_act)]
2000 ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
2002 = let (env1, tidy_ty) = tidyOpenType env ty
2003 (env2, extra) = ppr_extra env1 tidy_ty
2005 (env2, quotes (ppr tidy_ty), extra)
2007 -- (ppr_extra env ty) shows extra info about 'ty'
2008 ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
2009 ppr_extra env (TyVarTy tv)
2010 | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
2011 = (env1, pprSkolTvBinding tv1)
2013 (env1, tv1) = tidySkolemTyVar env tv
2015 ppr_extra env _ty = (env, empty) -- Normal case