Commit 12864264 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Remove two old junk files

parent d2ce0f52
Normalisation of type terms relative to type instances as well as
normalisation and entailment checking of equality constraints.
\begin{code}
module TcTyFuns (
-- type normalisation wrt to toplevel equalities only
tcNormaliseFamInst,
-- instance normalisation wrt to equalities
tcReduceEqs,
-- errors
misMatchMsg, failWithMisMatch,
) where
#include "HsVersions.h"
--friends
import TcRnMonad
import TcEnv
import Inst
import TcType
import TcMType
-- GHC
import Coercion
import Type
import TypeRep ( Type(..) )
import TyCon
import HsSyn
import VarEnv
import VarSet
import Var
import Name
import Bag
import Outputable
import SrcLoc ( Located(..) )
import Maybes
import FastString
-- standard
import Data.List
import Control.Monad
\end{code}
%************************************************************************
%* *
Normalisation of types wrt toplevel equality schemata
%* *
%************************************************************************
Unfold a single synonym family instance and yield the witnessing coercion.
Return 'Nothing' if the given type is either not synonym family instance
or is a synonym family instance that has no matching instance declaration.
(Applies only if the type family application is outermost.)
For example, if we have
:Co:R42T a :: T [a] ~ :R42T a
then 'T [Int]' unfolds to (:R42T Int, :Co:R42T Int).
\begin{code}
tcUnfoldSynFamInst :: Type -> TcM (Maybe (Type, Coercion))
tcUnfoldSynFamInst (TyConApp tycon tys)
| not (isSynFamilyTyCon tycon) -- unfold *only* _synonym_ family instances
= return Nothing
| otherwise
= do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
; maybeFamInst <- tcLookupFamInst tycon tys
; case maybeFamInst of
Nothing -> return Nothing
Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
mkTyConApp coe_tc rep_tys)
where
coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst"
(tyConFamilyCoercion_maybe rep_tc)
}
tcUnfoldSynFamInst _other = return Nothing
\end{code}
Normalise 'Type's and 'PredType's by unfolding type family applications where
possible (ie, we treat family instances as a TRS). Also zonk meta variables.
tcNormaliseFamInst ty = (co, ty')
then co : ty ~ ty'
\begin{code}
-- |Normalise the given type as far as possible with toplevel equalities.
-- This results in a coercion witnessing the type equality, in addition to the
-- normalised type.
--
tcNormaliseFamInst :: TcType -> TcM (CoercionI, TcType)
tcNormaliseFamInst = tcGenericNormaliseFamInst tcUnfoldSynFamInst
\end{code}
Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
apply the normalisation function gives as the first argument to every TyConApp
and every TyVarTy subterm.
tcGenericNormaliseFamInst fun ty = (co, ty')
then co : ty ~ ty'
This function is (by way of using smart constructors) careful to ensure that
the returned coercion is exactly IdCo (and not some semantically equivalent,
but syntactically different coercion) whenever (ty' `tcEqType` ty). This
makes it easy for the caller to determine whether the type changed. BUT
even if we return IdCo, ty' may be *syntactically* different from ty due to
unfolded closed type synonyms (by way of tcCoreView). In the interest of
good error messages, callers should discard ty' in favour of ty in this case.
\begin{code}
tcGenericNormaliseFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
-- what to do with type functions and tyvars
-> TcType -- old type
-> TcM (CoercionI, TcType) -- (coercion, new type)
tcGenericNormaliseFamInst fun ty
| Just ty' <- tcView ty = tcGenericNormaliseFamInst fun ty'
tcGenericNormaliseFamInst fun (TyConApp tyCon tys)
= do { (cois, ntys) <- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
; let tycon_coi = mkTyConAppCoI tyCon ntys cois
; maybe_ty_co <- fun (mkTyConApp tyCon ntys) -- use normalised args!
; case maybe_ty_co of
-- a matching family instance exists
Just (ty', co) ->
do { let first_coi = mkTransCoI tycon_coi (ACo co)
; (rest_coi, nty) <- tcGenericNormaliseFamInst fun ty'
; let fix_coi = mkTransCoI first_coi rest_coi
; return (fix_coi, nty)
}
-- no matching family instance exists
-- we do not do anything
Nothing -> return (tycon_coi, mkTyConApp tyCon ntys)
}
tcGenericNormaliseFamInst fun (AppTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
; return (mkAppTyCoI nty1 coi1 nty2 coi2, mkAppTy nty1 nty2)
}
tcGenericNormaliseFamInst fun (FunTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormaliseFamInst fun ty1
; (coi2,nty2) <- tcGenericNormaliseFamInst fun ty2
; return (mkFunTyCoI nty1 coi1 nty2 coi2, mkFunTy nty1 nty2)
}
tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
= do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
}
tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
| isTcTyVar tv
= do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
; res <- lookupTcTyVar tv
; case res of
DoneTv _ ->
do { maybe_ty' <- fun ty
; case maybe_ty' of
Nothing -> return (IdCo, ty)
Just (ty', co1) ->
do { (coi2, ty'') <- tcGenericNormaliseFamInst fun ty'
; return (ACo co1 `mkTransCoI` coi2, ty'')
}
}
IndirectTv ty' -> tcGenericNormaliseFamInst fun ty'
}
| otherwise
= return (IdCo, ty)
tcGenericNormaliseFamInst fun (PredTy predty)
= do { (coi, pred') <- tcGenericNormaliseFamInstPred fun predty
; return (coi, PredTy pred') }
---------------------------------
tcGenericNormaliseFamInstPred :: (TcType -> TcM (Maybe (TcType,Coercion)))
-> TcPredType
-> TcM (CoercionI, TcPredType)
tcGenericNormaliseFamInstPred fun (ClassP cls tys)
= do { (cois, tys')<- mapAndUnzipM (tcGenericNormaliseFamInst fun) tys
; return (mkClassPPredCoI cls tys' cois, ClassP cls tys')
}
tcGenericNormaliseFamInstPred fun (IParam ipn ty)
= do { (coi, ty') <- tcGenericNormaliseFamInst fun ty
; return $ (mkIParamPredCoI ipn coi, IParam ipn ty')
}
tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
= do { (coi1, ty1') <- tcGenericNormaliseFamInst fun ty1
; (coi2, ty2') <- tcGenericNormaliseFamInst fun ty2
; return (mkEqPredCoI ty1' coi1 ty2' coi2, EqPred ty1' ty2') }
\end{code}
%************************************************************************
%* *
Normalisation of instances wrt to equalities
%* *
%************************************************************************
Given a set of given, local constraints and a set of wanted constraints,
simplify the wanted equalities as far as possible and normalise both local and
wanted dictionaries with respect to the equalities.
In addition to the normalised local dictionaries and simplified wanteds, the
function yields bindings for instantiated meta variables (due to solving
equality constraints) and dictionary bindings (due to simplifying class
constraints). The bag of type variable bindings only contains bindings for
non-local variables - i.e., type variables other than those newly created by
the present function. Consequently, type improvement took place iff the bag
of bindings contains any bindings for proper type variables (not just covars).
The solver does not instantiate any non-local variables; i.e., the bindings
must be executed by the caller.
All incoming constraints are assumed to be zonked already. All outgoing
constraints will be zonked again.
NB: The solver only has local effects that cannot be observed from outside.
In particular, it can be executed twice on the same constraint set with
the same result (modulo generated variables names).
\begin{code}
tcReduceEqs :: [Inst] -- locals
-> [Inst] -- wanteds
-> TcM ([Inst], -- normalised locals (w/o equalities)
[Inst], -- normalised wanteds (including equalities)
TcTyVarBinds, -- bindings for meta type variables
TcDictBinds) -- bindings for all simplified dictionaries
tcReduceEqs locals wanteds
= do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
do { let (local_eqs , local_dicts) = partition isEqInst locals
(wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
; eqCfg2 <- normaliseDicts False local_dicts
; eqCfg3 <- normaliseDicts True wanteds_dicts
; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig`
eqCfg2 `unionEqConfig`
eqCfg3)
; finaliseEqsAndDicts freeFlexibles eqCfg
}
-- execute type bindings of skolem flexibles...
; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
-- ...and zonk the constraints to propagate the bindings
; locals_z <- zonkInsts locals
; wanteds_z <- zonkInsts wanteds
; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
}
where
-- unification variables that appear in the environment and may not be
-- instantiated - this includes coercion variables
freeFlexibles = tcTyVarsOfInsts locals `unionVarSet`
tcTyVarsOfInsts wanteds
pruneTyBinds tybinds freeFlexibles
= do { let tybinds' = bagToList tybinds
(skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
; execTcTyVarBinds (listToBag skolem_tybinds)
; return $ listToBag env_tybinds
}
where
isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
\end{code}
%************************************************************************
%* *
Equality Configurations
%* *
%************************************************************************
We maintain normalised equalities together with the skolems introduced as
intermediates during flattening of equalities as well as
\begin{code}
-- |Configuration of normalised equalities used during solving.
--
data EqConfig = EqConfig { eqs :: [RewriteInst] -- all equalities
, locals :: [Inst] -- given dicts
, wanteds :: [Inst] -- wanted dicts
, binds :: TcDictBinds -- bindings
}
addEq :: EqConfig -> RewriteInst -> EqConfig
addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
unionEqConfig :: EqConfig -> EqConfig -> EqConfig
unionEqConfig eqc1 eqc2 = EqConfig
{ eqs = eqs eqc1 ++ eqs eqc2
, locals = locals eqc1 ++ locals eqc2
, wanteds = wanteds eqc1 ++ wanteds eqc2
, binds = binds eqc1 `unionBags` binds eqc2
}
emptyEqConfig :: EqConfig
emptyEqConfig = EqConfig
{ eqs = []
, locals = []
, wanteds = []
, binds = emptyBag
}
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
configuration by normalisation ('normaliseEqs'), solve the equalities by
propagation ('propagateEqs'), and eventually finalise the configuration when
no further propoagation is possible.
\begin{code}
-- |Turn a set of equalities into an equality configuration for solving.
--
-- Precondition: The Insts are zonked.
--
normaliseEqs :: [Inst] -> TcM EqConfig
normaliseEqs eqs
= do { WARNM2( anyM wantedEqInstIsUnsolved eqs, ppr eqs )
; traceTc $ ptext (sLit "Entering normaliseEqs")
; eqss <- mapM normEqInst eqs
; return $ emptyEqConfig { eqs = concat eqss }
}
-- |Flatten the type arguments of all dictionaries, returning the result as a
-- equality configuration. The dictionaries go into the 'wanted' component if
-- the second argument is 'True'.
--
-- Precondition: The Insts are zonked.
--
normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
normaliseDicts isWanted insts
= do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
ptext (if isWanted then sLit "[Wanted] for"
else sLit "[Local] for"))
4 (ppr insts)
; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
4 (ppr insts' $$ ppr eqss)
; return $ emptyEqConfig { eqs = concat eqss
, locals = if isWanted then [] else insts'
, wanteds = if isWanted then insts' else []
, binds = unionManyBags bindss
}
}
-- |Solves the equalities as far as possible by applying propagation rules.
--
propagateEqs :: EqConfig -> TcM EqConfig
propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
= 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 first returned set of instances are the locals (without
-- equalities) and the second set are all residual wanteds, including
-- equalities. In addition, we return all generated dictionary bindings.
--
finaliseEqsAndDicts :: TcTyVarSet -> EqConfig
-> TcM ([Inst], [Inst], TcDictBinds)
finaliseEqsAndDicts freeFlexibles (EqConfig { eqs = eqs
, locals = locals
, wanteds = wanteds
, binds = binds
})
= do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
; (eqs', subst_binds, locals', wanteds')
<- substitute eqs locals wanteds checkingMode freeFlexibles
; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
; let final_binds = subst_binds `unionBags` binds
-- Assert that all cotvs of wanted equalities are still unfilled, and
-- zonk all final insts, to make any improvement visible
; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
; zonked_locals <- zonkInsts locals'
; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
; return (zonked_locals, zonked_wanteds, final_binds)
}
where
checkingMode = length eqs > length wanteds || not (null locals)
-- no local equalities or dicts => checking mode
\end{code}
%************************************************************************
%* *
Normalisation of equalities
%* *
%************************************************************************
A normal equality is a properly oriented equality with associated coercion
that contains at most one family equality (in its left-hand side) is oriented
such that it may be used as a rewrite rule. It has one of the following two
forms:
(1) co :: F t1..tn ~ t (family equalities)
(2) co :: x ~ t (variable equalities)
Variable equalities fall again in two classes:
(2a) co :: x ~ t, where t is *not* a variable, or
(2b) co :: x ~ y, where x > y.
The types t, t1, ..., tn may not contain any occurrences of synonym
families. Moreover, in Forms (2) & (3), the left-hand side may not occur in
the right-hand side, and the relation x > y is an (nearly) arbitrary, but
total order on type variables. The only restriction that we impose on that
order is that for x > y, we are happy to instantiate x with y taking into
account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
\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_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_swapped :: Bool -- swapped orientation of original EqInst
}
isWantedRewriteInst :: RewriteInst -> Bool
isWantedRewriteInst = isWantedCo . rwi_co
isRewriteVar :: RewriteInst -> Bool
isRewriteVar (RewriteVar {}) = True
isRewriteVar _ = False
tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
= unitVarSet tv `unionVarSet` tyVarsOfType ty
tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
= tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
rewriteInstToInst :: RewriteInst -> TcM Inst
rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
= deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
= 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
equalities. This implements the WFlat and LFlat rules of the paper in one
sweep. However, we use flexible variables for both locals and wanteds, and
avoid to carry around the unflattening substitution \Sigma (for locals) by
already updating the skolems for locals with the family application that they
represent - i.e., they will turn into that family application on the next
zonking (which only happens after finalisation).
In a corresponding manner, normDict normalises class dictionaries by
extracting any synonym family applications and generation appropriate normal
equalities.
Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
we drop that equality and raise an error if it is a wanted or a warning if it
is a local.
\begin{code}
normEqInst :: Inst -> TcM [RewriteInst]
-- Normalise one equality.
normEqInst inst
= ASSERT( isEqInst inst )
do { traceTc $ ptext (sLit "normEqInst of ") <+>
pprEqInstCo co <+> text "::" <+>
ppr ty1 <+> text "~" <+> ppr ty2
; res <- go ty1 ty2 co
; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
; return res
}
where
(ty1, ty2) = eqInstTys inst
co = eqInstCoercion inst
-- look through synonyms
go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
-- left-to-right rule with type family head
go ty1@(TyConApp con args) ty2 co
| isSynFamilyTyConApp ty1 -- only if not oversaturated
= mkRewriteFam False con args ty2 co
-- right-to-left rule with type family head
go ty1 ty2@(TyConApp con args) co
| isSynFamilyTyConApp ty2 -- only if not oversaturated
= do { co' <- mkSymEqInstCo co (ty2, ty1)
; mkRewriteFam True con args ty1 co'
}
-- no outermost family
go ty1 ty2 co
= do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
; (ty2', co2, ty2_eqs) <- flattenType inst ty2
; let ty12_eqs = ty1_eqs ++ ty2_eqs
sym_co2 = mkSymCoercion co2
eqTys = (ty1', ty2')
; (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)
then
addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
eqInstMisMatch inst
else
warnDroppingLoopyEquality ty1 ty2
; return ([]) -- drop the equality
}
else
return (eqs ++ ty12_eqs')
}
mkRewriteFam swapped con args ty2 co
= do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
; (ty2', co2, ty2_eqs) <- flattenType inst ty2
; 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 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_swapped = swapped
}
; return $ thisRewriteFam : all_eqs'
}
-- If the original equality has the form a ~ T .. (F ...a...) ..., we will
-- have a variable equality with 'a' on the lhs as the first equality.
-- Then, check whether 'a' occurs in the lhs of any family equality
-- generated by flattening.
isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
where
inRewriteFam (RewriteFam {rwi_args = args})
= tv `elemVarSet` tyVarsOfTypes args
inRewriteFam _ = False
isLoopyEquality _ _ = False
normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
-- Normalise one dictionary or IP constraint.
normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
= do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
; let rewriteCo = PredTy $ ClassP clas cargs
eqs = concat args_eqss
pred' = ClassP clas args'
; if null eqs
then -- don't generate a binding if there is nothing to flatten
return (inst, [], emptyBag)
else do {
; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
; return (inst', eqs', bind)
}}
normDict _isWanted inst
= return (inst, [], emptyBag)
-- !!!TODO: Still need to normalise IP constraints.
checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
-- Performs the occurs check, decomposition, and proper orientation
-- (returns a singleton, or an empty list in case of a trivial equality)
-- 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
where
-- look through synonyms
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
-- identical types => trivial
go ty1 ty2
| ty1 `tcEqType` ty2
= do { mkIdEqInstCo co ty1
; return []
}
-- two tvs (distinct tvs, due to previous equation)
go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
= do { isBigger <- tv1 `tvIsBigger` tv2
; if isBigger -- left greater
then mkRewriteVar False tv1 ty2 co -- => unchanged
else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater
; mkRewriteVar True tv2 ty1 co' -- => swap
}
}