1 files changed, 0 insertions, 86 deletions
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index c253770616..a039630887 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -631,92 +631,6 @@ getHasGivenEqs tclvl
     insoluble_given_equality ct
        = insolubleEqCt ct && isGivenCt ct
 
-{- Note [What might equal later?]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We must determine whether a Given might later equal a Wanted. We
-definitely need to account for the possibility that any metavariable
-might be arbitrarily instantiated. Yet we do *not* want
-to allow skolems in to be instantiated, as we've already rewritten
-with respect to any Givens. (We're solving a Wanted here, and so
-all Givens have already been processed.)
-
-This is best understood by example.
-
-1. C alpha  ~?  C Int
-
-   That given certainly might match later.
-
-2. C a  ~?  C Int
-
-   No. No new givens are going to arise that will get the `a` to rewrite
-   to Int.
-
-3. C alpha[tv]   ~?  C Int
-
-   That alpha[tv] is a TyVarTv, unifiable only with other type variables.
-   It cannot equal later.
-
-4. C (F alpha)   ~?   C Int
-
-   Sure -- that can equal later, if we learn something useful about alpha.
-
-5. C (F alpha[tv])  ~?  C Int
-
-   This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
-   Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
-   and F x x = Int. Remember: returning True doesn't commit ourselves to
-   anything.
-
-6. C (F a)  ~?  C a
-
-   No, this won't match later. If we could rewrite (F a) or a, we would
-   have by now.
-
-7. C (Maybe alpha)  ~?  C alpha
-
-   We say this cannot equal later, because it would require
-   alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
-   we choose not to worry about it. See Note [Infinitary substitution in lookup]
-   in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in
-   typecheck/should_compile/T19107.
-
-8. C cbv   ~?  C Int
-   where cbv = F a
-
-   The cbv is a cycle-breaker var which stands for F a. See
-   Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
-   This is just like case 6, and we say "no". Saying "no" here is
-   essential in getting the parser to type-check, with its use of DisambECP.
-
-9. C cbv   ~?   C Int
-   where cbv = F alpha
-
-   Here, we might indeed equal later. Distinguishing between
-   this case and Example 8 is why we need the InertSet in mightEqualLater.
-
-10. C (F alpha, Int)  ~?  C (Bool, F alpha)
-
-   This cannot equal later, because F a would have to equal both Bool and
-   Int.
-
-To deal with type family applications, we use the Core flattener. See
-Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
-The Core flattener replaces all type family applications with
-fresh variables. The next question: should we allow these fresh
-variables in the domain of a unifying substitution?
-
-A type family application that mentions only skolems (example 6) is settled:
-any skolems would have been rewritten w.r.t. Givens by now. These type family
-applications match only themselves. A type family application that mentions
-metavariables, on the other hand, can match anything. So, if the original type
-family application contains a metavariable, we use BindMe to tell the unifier
-to allow it in the substitution. On the other hand, a type family application
-with only skolems is considered rigid.
-
-This treatment fixes #18910 and is tested in
-typecheck/should_compile/InstanceGivenOverlap{,2}
--}
-
 removeInertCts :: [Ct] -> InertCans -> InertCans
 -- ^ Remove inert constraints from the 'InertCans', for use when a
 -- typechecker plugin wishes to discard a given.