+Splitting of non-terminating given constraints: skolemOccurs
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This is a preconditioning rule exclusively applied to given constraints.
+Moreover, its rewriting is only temporary, as it is undone by way of
+side-effecting mutable type variables after simplification and constraint
+entailment has been completed.
+
+This version is an (attempt at, yet unproven, an) *unflattened* version of
+the SubstL-Ev completion rule.
+
+The above rule is essential to catch non-terminating rules that cannot be
+oriented properly, like
+
+ F a ~ [G (F a)]
+ or even
+ a ~ [G a] , where a is a skolem tyvar
+
+The left-to-right orientiation is not suitable because it does not
+terminate. The right-to-left orientation is not suitable because it
+does not have a type-function on the left. This is undesirable because
+it would hide information. E.g. assume
+
+ instance C [x]
+
+then rewriting C [G (F a)] to C (F a) is bad because we cannot now
+see that the C [x] instance applies.
+
+The rule also caters for badly-oriented rules of the form:
+
+ F a ~ G (F a)
+
+for which other solutions are possible, but this one will do too.
+
+It's behavior is:
+
+ co : ty1 ~ ty2{F ty1}
+ >-->
+ co : ty1 ~ ty2{b}
+ sym (F co) : F ty2{b} ~ b
+ where b is a fresh skolem variable
+
+We also cater for the symmetric situation *if* the rule cannot be used as a
+left-to-right rewrite rule.
+
+We also return an action (b := ty1) which is used to eliminate b
+after the dust of normalisation with the completed rewrite system
+has settled.
+
+A subtle point of this transformation is that both coercions in the results
+are strictly speaking incorrect. However, they are correct again after the
+action {B := ty1} has removed the skolem again. This happens immediately
+after constraint entailment has been checked; ie, code outside of the
+simplification and entailment checking framework will never see these
+temporarily incorrect coercions.
+
+NB: We perform this transformation for multiple occurences of ty1 under one
+ or multiple family applications on the left-hand side at once (ie, the
+ rule doesn't need to be applied multiple times at a single inst). As a
+ result we can get two or more insts back.
+
+Note [skolemOccurs loop]
+~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that under
+
+ type family F a
+ type instance F [a] = [F a]
+
+a signature such as
+
+ foo :: (F [a] ~ a) => a
+
+will get us into a loop. However, this is *not* the case. Here is why:
+
+ F [a<sk>] ~ a<sk>
+
+ -->(TOP)
+
+ [F a<sk>] ~ a<sk>
+
+ -->(SkolemOccurs)
+
+ [b<tau>] ~ a<sk>
+ F [b<tau>] ~ b<tau> , with b := F a
+
+ -->(TOP)
+
+ [b<tau>] ~ a<sk>
+ [F b<tau>] ~ b<tau> , with b := F a
+
+At this point (SkolemOccurs) does *not* apply anymore, as
+
+ [F b<tau>] ~ b<tau>
+
+is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
+eqInstToRewrite).
+
+(The regression test indexed-types/should_compile/Simple20 checks that the
+described property of the system does not change.)
+
+\begin{code}
+skolemOccurs :: PrecondRule
+skolemOccurs insts
+ = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
+ ; return (concat instss, sequence_ undoSkolems)
+ }
+ where
+ oneSkolemOccurs inst
+ = ASSERT( isEqInst inst )
+ case eqInstToRewrite inst of
+ Just (rewrite, swapped) -> breakRecursion rewrite swapped
+ Nothing -> return ([inst], return ())
+ where
+ -- inst is an elementary rewrite rule, check whether we need to break
+ -- it up
+ breakRecursion (Rewrite pat body _) swapped
+
+ -- skolemOccurs does not apply, leave as is
+ | null tysToLiftOut
+ = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
+ ; return ([inst], return ())
+ }
+
+ -- recursive occurence of pat in body under a type family application
+ | otherwise
+ = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
+ ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
+ ; let skTvs_tysTLO = zip skTvs tysToLiftOut
+ insertSkolems = return . replace skTvs_tysTLO
+ ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
+ ; inst' <- if swapped then mkEqInst (EqPred body' pat) co
+ else mkEqInst (EqPred pat body') co
+ -- ensure to reconstruct the inst in the
+ -- original orientation
+ ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
+ ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
+ skTvs_tysTLO
+ ; return (inst':insts, sequence_ undoSk)
+ }
+ where
+ co = eqInstCoercion inst
+
+ -- all subtypes that are (1) type family instances and (2) contain
+ -- the lhs type as part of the type arguments of the type family
+ -- constructor
+ tysToLiftOut = [mkTyConApp tc tys | (tc, tys) <- tyFamInsts body
+ , any (pat `tcPartOfType`) tys]
+
+ replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
+ replace [] _ = Nothing
+ replace ((skTv, tyTLO):rest) ty
+ | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
+ | otherwise = replace rest ty
+
+ -- create the EqInst for the equality determining the skolem and a
+ -- TcM action undoing the skolem introduction
+ mkSkolemInst inst' (skTv, tyTLO)
+ = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
+ ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
+ (mkGivenCo $ mkSymCoercion (fromACo co))
+ -- co /= IdCo due to construction of inst'
+ ; return (inst, writeMetaTyVar skTv tyTLO)
+ }
+\end{code}
+
+
+Removal of trivial equalities: trivialRule
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The following rules exploits the reflexivity of equality:
+
+ (Trivial)
+ g1 : t ~ t
+ >-->
+ g1 := t