Make matchableGivens more reliably correct.wip/T19106

This has two fixes:

1. Take TyVarTvs into account in matchableGivens. This
   fixes #19106.

2. Don't allow unifying alpha ~ Maybe alpha. This fixes
   #19107.

This patch also removes a redundant Note and redirects
references to a better replacement.

Also some refactoring/improvements around the BindFun
in the pure unifier, which now can take the RHS type
into account.

Close #19106.
Close #19107.

Test case: partial-sigs/should_compile/T19106,
           typecheck/should_compile/T19107

3 files changed, 24 insertions, 38 deletions

diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 24b7e4d93a..ed9ee9cc44 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -766,21 +766,27 @@ the thinking.
 {- Note [TyVarTv]
 ~~~~~~~~~~~~~~~~~
 A TyVarTv can unify with type *variables* only, including other TyVarTvs and
-skolems. Sometimes, they can unify with type variables that the user would
-rather keep distinct; see #11203 for an example.  So, any client of this
-function needs to either allow the TyVarTvs to unify with each other or check
-that they don't (say, with a call to findDubTyVarTvs).
-
-Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in
-patterns, to make sure these type variables only refer to other type variables,
-but this restriction was dropped, and ScopedTypeVariables can now refer to full
-types (GHC Proposal 29).
-
-The remaining uses of newTyVarTyVars are
-* In kind signatures, see
-  GHC.Tc.TyCl Note [Inferring kinds for type declarations]
-          and Note [Kind checking for GADTs]
-* In partial type signatures, see Note [Quantified variables in partial type signatures]
+skolems.  They are used in two places:
+
+1. In kind signatures, see GHC.Tc.TyCl
+      Note [Inferring kinds for type declarations]
+   and Note [Kind checking for GADTs]
+
+2. In partial type signatures.  See GHC.Tc.Types
+   Note [Quantified variables in partial type signatures]
+
+Sometimes, they can unify with type variables that the user would
+rather keep distinct; see #11203 for an example.  So, any client of
+this function needs to either allow the TyVarTvs to unify with each
+other or check that they don't. In the case of (1) the check is done
+in GHC.Tc.TyCl.swizzleTcTyConBndrs.  In case of (2) it's done by
+findDupTyVarTvs in GHC.Tc.Gen.Bind.chooseInferredQuantifiers.
+
+Historical note: Before #15050 this (under the name SigTv) was also
+used for ScopedTypeVariables in patterns, to make sure these type
+variables only refer to other type variables, but this restriction was
+dropped, and ScopedTypeVariables can now refer to full types (GHC
+Proposal 29).
 -}
 
 newMetaTyVarName :: FastString -> TcM Name
@@ -1777,7 +1783,7 @@ defaultTyVar default_kind tv
 
   | isTyVarTyVar tv
     -- Do not default TyVarTvs. Doing so would violate the invariants
-    -- on TyVarTvs; see Note [Signature skolems] in GHC.Tc.Utils.TcType.
+    -- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType.
     -- #13343 is an example; #14555 is another
     -- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
   = return False
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 9ec129ef4a..0a0d341a47 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -457,26 +457,6 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to "GHC.Types.Var".  There is no reason in principle
 why "GHC.Types.Var" shouldn't actually have the definition, but it "belongs" here.
 
-Note [Signature skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~
-A TyVarTv is a specialised variant of TauTv, with the following invariants:
-
-    * A TyVarTv can be unified only with a TyVar,
-      not with any other type
-
-    * Its MetaDetails, if filled in, will always be another TyVarTv
-      or a SkolemTv
-
-TyVarTvs are only distinguished to improve error messages.
-Consider this
-
-  data T (a:k1) = MkT (S a)
-  data S (b:k2) = MkS (T b)
-
-When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
-because they end up unifying; we want those TyVarTvs again.
-
-
 Note [TyVars and TcTyVars during type checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The Var type has constructors TyVar and TcTyVar.  They are used
@@ -547,7 +527,7 @@ data MetaInfo
 
    | TyVarTv       -- A variant of TauTv, except that it should not be
                    --   unified with a type, only with a type variable
-                   -- See Note [Signature skolems]
+                   -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType
 
    | RuntimeUnkTv  -- A unification variable used in the GHCi debugger.
                    -- It /is/ allowed to unify with a polytype, unlike TauTv
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 892ab050d5..6675e38d6b 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1583,7 +1583,7 @@ Needless to say, all three have wrinkles:
   up a fresh gamma[n], and unify beta[k] := gamma[n].
 
 * (TYVAR-TV) Unification variables.  Suppose alpha[tyv,n] is a level-n
-  TyVarTv (see Note [Signature skolems] in GHC.Tc.Types.TcType)? Now
+  TyVarTv (see Note [TyVarTv] in GHC.Tc.Types.TcMType)? Now
   consider alpha[tyv,n] ~ Bool.  We don't want to unify because that
   would break the TyVarTv invariant.