X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcTyFuns.lhs;h=ba73891fa4945365d6940ad8929a491d28fb3e47;hb=c7ae8f20f93b4e36837fc3ecafccd3f49c95cb6b;hp=0b026e14858849aec1caf04fbcf382ed605bda8d;hpb=488da9e2096994a3a8dd6d559785c792a4527f73;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs index 0b026e1..ba73891 100644 --- a/compiler/typecheck/TcTyFuns.lhs +++ b/compiler/typecheck/TcTyFuns.lhs @@ -269,6 +269,10 @@ emptyEqConfig = EqConfig , binds = emptyBag , skolems = emptyVarSet } + +instance Outputable EqConfig where + ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds}) + = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds] \end{code} The set of operations on an equality configuration. We obtain the initialise @@ -283,7 +287,10 @@ no further propoagation is possible. -- normaliseEqs :: [Inst] -> TcM EqConfig normaliseEqs eqs - = do { (eqss, skolemss) <- mapAndUnzipM normEqInst eqs + = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs ) + ; traceTc $ ptext (sLit "Entering normaliseEqs") + + ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs ; return $ emptyEqConfig { eqs = concat eqss , skolems = unionVarSets skolemss } @@ -297,7 +304,9 @@ normaliseEqs eqs -- normaliseDicts :: Bool -> [Inst] -> TcM EqConfig normaliseDicts isWanted insts - = do { (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted) + = do { traceTc $ ptext (sLit "Entering normaliseDicts") <+> + ptext (if isWanted then sLit "[Wanted]" else sLit "[Local]") + ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted) insts ; return $ emptyEqConfig { eqs = concat eqss , locals = if isWanted then [] else insts' @@ -311,7 +320,11 @@ normaliseDicts isWanted insts -- propagateEqs :: EqConfig -> TcM EqConfig propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) - = propagate todoEqs (eqCfg {eqs = []}) + = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:")) + 4 (ppr eqCfg) + + ; propagate todoEqs (eqCfg {eqs = []}) + } -- |Finalise a set of equalities and associated dictionaries after -- propagation. The returned Boolean value is `True' iff any flexible @@ -332,10 +345,13 @@ finaliseEqsAndDicts (EqConfig { eqs = eqs , wanteds = wanteds , binds = binds }) - = do { (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds - ; (eqs'', improved) <- instantiateAndExtract eqs' + = do { traceTc $ ptext (sLit "finaliseEqsAndDicts") + ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds + ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) ; final_binds <- filterM nonTrivialDictBind $ bagToList (subst_binds `unionBags` binds) + + ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' ) ; return (locals', eqs'' ++ wanteds', listToBag final_binds, improved) } where @@ -379,41 +395,68 @@ re-orient on finilisation). \begin{code} data RewriteInst = RewriteVar -- Form (2) above - { rwi_var :: TyVar -- may be rigid or flexible - , rwi_right :: TcType -- contains no synonym family applications - , rwi_co :: EqInstCo -- the wanted or given coercion - , rwi_loc :: InstLoc - , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst) + { rwi_var :: TyVar -- may be rigid or flexible + , rwi_right :: TcType -- contains no synonym family applications + , rwi_co :: EqInstCo -- the wanted or given coercion + , rwi_loc :: InstLoc + , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst) + , rwi_swapped :: Bool -- swapped orientation of original EqInst } | RewriteFam -- Forms (1) above - { rwi_fam :: TyCon -- synonym family tycon - , rwi_args :: [Type] -- contain no synonym family applications - , rwi_right :: TcType -- contains no synonym family applications - , rwi_co :: EqInstCo -- the wanted or given coercion - , rwi_loc :: InstLoc - , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst) + { rwi_fam :: TyCon -- synonym family tycon + , rwi_args :: [Type] -- contain no synonym family applications + , rwi_right :: TcType -- contains no synonym family applications + , rwi_co :: EqInstCo -- the wanted or given coercion + , rwi_loc :: InstLoc + , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst) + , rwi_swapped :: Bool -- swapped orientation of original EqInst } isWantedRewriteInst :: RewriteInst -> Bool isWantedRewriteInst = isWantedCo . rwi_co -rewriteInstToInst :: RewriteInst -> Inst +rewriteInstToInst :: RewriteInst -> TcM Inst rewriteInstToInst eq@(RewriteVar {rwi_var = tv}) - = EqInst - { tci_left = mkTyVarTy tv - , tci_right = rwi_right eq - , tci_co = rwi_co eq - , tci_loc = rwi_loc eq - , tci_name = rwi_name eq - } + = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq) rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args}) - = EqInst - { tci_left = mkTyConApp fam args - , tci_right = rwi_right eq - , tci_co = rwi_co eq - , tci_loc = rwi_loc eq - , tci_name = rwi_name eq - } + = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq) + +-- Derive an EqInst based from a RewriteInst, possibly swapping the types +-- around. +-- +deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst +deriveEqInst rewrite ty1 ty2 co + = do { co_adjusted <- if not swapped then return co + else mkSymEqInstCo co (ty2, ty1) + ; return $ EqInst + { tci_left = left + , tci_right = right + , tci_co = co_adjusted + , tci_loc = rwi_loc rewrite + , tci_name = rwi_name rewrite + } + } + where + swapped = rwi_swapped rewrite + (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1) + +instance Outputable RewriteInst where + ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co}) + = hsep [ pprEqInstCo co <+> text "::" + , ppr (mkTyConApp fam args) + , text "~>" + , ppr rhs + ] + ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co}) + = hsep [ pprEqInstCo co <+> text "::" + , ppr tv + , text "~>" + , ppr rhs + ] + +pprEqInstCo :: EqInstCo -> SDoc +pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv +pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co \end{code} The following functions turn an arbitrary equality into a set of normal @@ -448,13 +491,13 @@ normEqInst inst -- left-to-right rule with type family head go (TyConApp con args) ty2 co | isOpenSynTyCon con - = mkRewriteFam con args ty2 co + = mkRewriteFam False con args ty2 co -- right-to-left rule with type family head go ty1 ty2@(TyConApp con args) co | isOpenSynTyCon con = do { co' <- mkSymEqInstCo co (ty2, ty1) - ; mkRewriteFam con args ty1 co' + ; mkRewriteFam True con args ty1 co' } -- no outermost family @@ -462,9 +505,9 @@ normEqInst inst = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1 ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2 ; let ty12_eqs = ty1_eqs ++ ty2_eqs - rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2 + sym_co2 = mkSymCoercion co2 eqTys = (ty1', ty2') - ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs + ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs ; eqs <- checkOrientation ty1' ty2' co' inst ; if isLoopyEquality eqs ty12_eqs' then do { if isWantedCo (tci_co inst) @@ -480,22 +523,23 @@ normEqInst inst ty1_skolems `unionVarSet` ty2_skolems) } - mkRewriteFam con args ty2 co + mkRewriteFam swapped con args ty2 co = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M (flattenType inst) args ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2 - ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion` - mkSymCoercion co2 + ; let co1 = mkTyConApp con cargs + sym_co2 = mkSymCoercion co2 all_eqs = concat args_eqss ++ ty2_eqs eqTys = (mkTyConApp con args', ty2') - ; (co', all_eqs') <- adjustCoercions co rewriteCo eqTys all_eqs + ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs ; let thisRewriteFam = RewriteFam - { rwi_fam = con - , rwi_args = args' - , rwi_right = ty2' - , rwi_co = co' - , rwi_loc = tci_loc inst - , rwi_name = tci_name inst + { rwi_fam = con + , rwi_args = args' + , rwi_right = ty2' + , rwi_co = co' + , rwi_loc = tci_loc inst + , rwi_name = tci_name inst + , rwi_swapped = swapped } ; return $ (thisRewriteFam : all_eqs', unionVarSets (ty2_skolems:args_skolemss)) @@ -529,7 +573,7 @@ normDict isWanted inst@(Dict {tci_pred = ClassP clas args}) ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs ; return (inst', eqs', bind, unionVarSets args_skolemss) }} -normDict isWanted inst +normDict _isWanted inst = return (inst, [], emptyBag, emptyVarSet) -- !!!TODO: Still need to normalise IP constraints. @@ -539,7 +583,13 @@ checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst] -- NB: We cannot assume that the two types already have outermost type -- synonyms expanded due to the recursion in the case of type applications. checkOrientation ty1 ty2 co inst - = go ty1 ty2 + = do { traceTc $ ptext (sLit "checkOrientation of ") <+> + pprEqInstCo co <+> text "::" <+> + ppr ty1 <+> text "~" <+> ppr ty2 + ; eqs <- go ty1 ty2 + ; traceTc $ ptext (sLit "checkOrientation returns") <+> ppr eqs + ; return eqs + } where -- look through synonyms go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 @@ -555,12 +605,12 @@ checkOrientation ty1 ty2 co inst -- two tvs, left greater => unchanged go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2) | tv1 > tv2 - = mkRewriteVar tv1 ty2 co + = mkRewriteVar False tv1 ty2 co -- two tvs, right greater => swap | otherwise = do { co' <- mkSymEqInstCo co (ty2, ty1) - ; mkRewriteVar tv2 ty1 co' + ; mkRewriteVar True tv2 ty1 co' } -- only lhs is a tv => unchanged @@ -568,7 +618,7 @@ checkOrientation ty1 ty2 co inst | ty1 `tcPartOfType` ty2 -- occurs check! = occurCheckErr ty1 ty2 | otherwise - = mkRewriteVar tv1 ty2 co + = mkRewriteVar False tv1 ty2 co -- only rhs is a tv => swap go ty1 ty2@(TyVarTy tv2) @@ -576,7 +626,7 @@ checkOrientation ty1 ty2 co inst = occurCheckErr ty2 ty1 | otherwise = do { co' <- mkSymEqInstCo co (ty2, ty1) - ; mkRewriteVar tv2 ty1 co' + ; mkRewriteVar True tv2 ty1 co' } -- type applications => decompose @@ -596,13 +646,14 @@ checkOrientation ty1 ty2 co inst = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) ) eqInstMisMatch inst - mkRewriteVar tv ty co = return [RewriteVar - { rwi_var = tv - , rwi_right = ty - , rwi_co = co - , rwi_loc = tci_loc inst - , rwi_name = tci_name inst - }] + mkRewriteVar swapped tv ty co = return [RewriteVar + { rwi_var = tv + , rwi_right = ty + , rwi_co = co + , rwi_loc = tci_loc inst + , rwi_name = tci_name inst + , rwi_swapped = swapped + }] flattenType :: Inst -- context to get location & name -> Type -- the type to flatten @@ -615,7 +666,18 @@ flattenType inst ty = go ty where -- look through synonyms - go ty | Just ty' <- tcView ty = go ty' + go ty | Just ty' <- tcView ty + = do { (ty_flat, co, eqs, skolems) <- go ty' + ; if null eqs + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (ty_flat, co, eqs, skolems) + } + + -- type variable => nothing to do + go ty@(TyVarTy _) + = return (ty, ty, [] , emptyVarSet) -- type family application -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh) @@ -626,12 +688,13 @@ flattenType inst ty ; let alphaTy = mkTyVarTy alpha ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy ; let thisRewriteFam = RewriteFam - { rwi_fam = con - , rwi_args = args' - , rwi_right = alphaTy - , rwi_co = mkWantedCo cotv - , rwi_loc = tci_loc inst - , rwi_name = tci_name inst + { rwi_fam = con + , rwi_args = args' + , rwi_right = alphaTy + , rwi_co = mkWantedCo cotv + , rwi_loc = tci_loc inst + , rwi_name = tci_name inst + , rwi_swapped = True } ; return (alphaTy, mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv, @@ -641,43 +704,64 @@ flattenType inst ty -- data constructor application => flatten subtypes -- NB: Special cased for efficiency - could be handled as type application - go (TyConApp con args) + go ty@(TyConApp con args) = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args - ; return (mkTyConApp con args', - mkTyConApp con cargs, - concat args_eqss, - unionVarSets args_skolemss) + ; if null args_eqss + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (mkTyConApp con args', + mkTyConApp con cargs, + concat args_eqss, + unionVarSets args_skolemss) } -- function type => flatten subtypes -- NB: Special cased for efficiency - could be handled as type application - go (FunTy ty_l ty_r) + go ty@(FunTy ty_l ty_r) = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r - ; return (mkFunTy ty_l' ty_r', - mkFunTy co_l co_r, - eqs_l ++ eqs_r, - skolems_l `unionVarSet` skolems_r) + ; if null eqs_l && null eqs_r + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (mkFunTy ty_l' ty_r', + mkFunTy co_l co_r, + eqs_l ++ eqs_r, + skolems_l `unionVarSet` skolems_r) } -- type application => flatten subtypes - go (AppTy ty_l ty_r) --- | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty + go ty@(AppTy ty_l ty_r) = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r - ; return (mkAppTy ty_l' ty_r', - mkAppTy co_l co_r, - eqs_l ++ eqs_r, - skolems_l `unionVarSet` skolems_r) + ; if null eqs_l && null eqs_r + then -- unchanged, keep the old type with folded synonyms + return (ty, ty, [], emptyVarSet) + else + return (mkAppTy ty_l' ty_r', + mkAppTy co_l co_r, + eqs_l ++ eqs_r, + skolems_l `unionVarSet` skolems_r) } - -- free of type families => leave as is - go ty - = ASSERT( not . isForAllTy $ ty ) - return (ty, ty, [] , emptyVarSet) + -- forall type => panic if the body contains a type family + -- !!!TODO: As long as the family does not contain a quantified variable + -- we might pull it out, but what if it does contain a quantified + -- variable??? + go ty@(ForAllTy _ body) + | null (tyFamInsts body) + = return (ty, ty, [] , emptyVarSet) + | otherwise + = panic "TcTyFuns.flattenType: synonym family in a rank-n type" + + -- we should never see a predicate type + go (PredTy _) + = panic "TcTyFuns.flattenType: unexpected PredType" adjustCoercions :: EqInstCo -- coercion of original equality - -> Coercion -- coercion witnessing the rewrite + -> Coercion -- coercion witnessing the left rewrite + -> Coercion -- coercion witnessing the right rewrite -> (Type, Type) -- types of flattened equality -> [RewriteInst] -- equalities from flattening -> TcM (EqInstCo, -- coercion for flattened equality @@ -685,17 +769,17 @@ adjustCoercions :: EqInstCo -- coercion of original equality -- Depending on whether we flattened a local or wanted equality, that equality's -- coercion and that of the new equalities produced during flattening are -- adjusted . -adjustCoercions co rewriteCo eqTys all_eqs - +adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs -- wanted => generate a fresh coercion variable for the flattened equality - | isWantedCo co - = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys - ; return (co', all_eqs) + = do { cotv' <- newMetaCoVar ty_l ty_r + ; writeMetaTyVar cotv $ + (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2) + ; return (Left cotv', all_eqs) } +adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs -- local => turn all new equalities into locals and update (but not zonk) -- the skolem - | otherwise = do { all_eqs' <- mapM wantedToLocal all_eqs ; return (co, all_eqs') } @@ -832,13 +916,7 @@ applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args}) Nothing -> return Nothing Just (lhs, rewrite_co) -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs) - ; let eq' = EqInst - { tci_left = lhs - , tci_right = rhs - , tci_co = co' - , tci_loc = rwi_loc eq - , tci_name = rwi_name eq - } + ; eq' <- deriveEqInst eq lhs rhs co' ; liftM Just $ normEqInst eq' } } @@ -873,13 +951,7 @@ applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1}) -- !!!Check whether anything breaks by making tcEqTypes look through synonyms. -- !!!Should be ok and we don't want three type equalities. = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs) - ; let eq2' = EqInst - { tci_left = lhs - , tci_right = rhs - , tci_co = co2' - , tci_loc = rwi_loc eq2 - , tci_name = rwi_name eq2 - } + ; eq2' <- deriveEqInst eq2 lhs rhs co2' ; liftM Just $ normEqInst eq2' } where @@ -911,13 +983,7 @@ applySubstVarVar eq1@(RewriteVar {rwi_var = tv1}) | tv1 == tv2 && (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1)) = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs) - ; let eq2' = EqInst - { tci_left = lhs - , tci_right = rhs - , tci_co = co2' - , tci_loc = rwi_loc eq2 - , tci_name = rwi_name eq2 - } + ; eq2' <- deriveEqInst eq2 lhs rhs co2' ; liftM Just $ normEqInst eq2' } where @@ -994,8 +1060,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds = return (res, binds, locals, wanteds) subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) res binds locals wanteds - = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+> - ptext (sLit "->") <+> ppr ty + = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co] tySubst = zipOpenTvSubst [tv] [ty] ; eqs' <- mapM (substEq eq coSubst tySubst) eqs @@ -1015,7 +1080,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds -- We have, co :: tv ~ ty -- => apply [ty/tv] to right-hand side of eq2 -- (but only if tv actually occurs in the right-hand side of eq2) - substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) + substEq (RewriteVar {rwi_var = tv, rwi_right = ty}) coSubst tySubst eq2 | tv `elemVarSet` tyVarsOfType (rwi_right eq2) = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2) @@ -1038,12 +1103,11 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds -- We have, co :: tv ~ ty -- => apply [ty/tv] to dictionary predicate -- (but only if tv actually occurs in the predicate) - substDict (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) + substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict | isClassDict dict , tv `elemVarSet` tyVarsOfPred (tci_pred dict) - = do { let co1Subst = mkSymCoercion $ - PredTy (substPred coSubst (tci_pred dict)) + = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict)) pred' = substPred tySubst (tci_pred dict) ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred' ; return (binds, dict') @@ -1061,33 +1125,46 @@ Return all remaining wanted equalities. The Boolean result component is True if at least one instantiation of a flexible was performed. \begin{code} -instantiateAndExtract :: [RewriteInst] -> TcM ([Inst], Bool) -instantiateAndExtract eqs - = do { let wanteds = filter (isWantedCo . rwi_co) eqs - ; wanteds' <- mapM inst wanteds +instantiateAndExtract :: [RewriteInst] -> Bool -> TcM ([Inst], Bool) +instantiateAndExtract eqs localsEmpty + = do { wanteds' <- mapM inst wanteds ; let residuals = catMaybes wanteds' improved = length wanteds /= length residuals - ; return (map rewriteInstToInst residuals, improved) + ; residuals' <- mapM rewriteInstToInst residuals + ; return (residuals', improved) } where + wanteds = filter (isWantedCo . rwi_co) eqs + checkingMode = length eqs > length wanteds || not localsEmpty + -- no local equalities or dicts => checking mode + inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co}) -- co :: alpha ~ t | isMetaTyVar tv1 - = doInst tv1 ty2 co eq + = doInst (rwi_swapped eq) tv1 ty2 co eq -- co :: a ~ alpha | Just tv2 <- tcGetTyVar_maybe ty2 , isMetaTyVar tv2 - = doInst tv2 (mkTyVarTy tv1) co eq + = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq + + -- co :: F args ~ alpha, and we are in checking mode (ie, no locals) + inst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty2, + rwi_co = co}) + | checkingMode + , Just tv2 <- tcGetTyVar_maybe ty2 + , isMetaTyVar tv2 + = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq inst eq = return $ Just eq - doInst _ _ (Right ty) _eq = pprPanic "TcTyFuns.doInst: local eq: " - (ppr ty) - doInst tv ty (Left cotv) eq = do { lookupTV <- lookupTcTyVar tv - ; uMeta False tv lookupTV ty cotv - } + doInst _swapped _tv _ty (Right ty) _eq + = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty) + doInst swapped tv ty (Left cotv) eq + = do { lookupTV <- lookupTcTyVar tv + ; uMeta swapped tv lookupTV ty cotv + } where -- meta variable has been filled already -- => ignore (must be a skolem that was introduced by flattening locals) @@ -1256,7 +1333,9 @@ warnDroppingLoopyEquality ty1 ty2 = do { env0 <- tcInitTidyEnv ; ty1 <- zonkTcType ty1 ; ty2 <- zonkTcType ty2 + ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1 + (_env2, tidy_ty2) = tidyOpenType env1 ty2 ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality")) - 2 (ppr ty1 <+> text "~" <+> ppr ty2) + 2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2)) } \end{code}