Ignore forall visibility in eqType (#22762)wip/int-index/visibility-check

Prior to this change, the equality relation on types took ForAllTyFlag
into account, making a distinction between:

	1. forall a.   blah
	2. forall a -> blah

Not anymore.

This distinction is important in surface Haskell, but it has no meaning
in Core where type abstraction and type application are always explicit.
At the same time, if we are not careful to track this flag, Core Lint
will fail, as reported in #22762:

	*** Core Lint errors : in result of TcGblEnv axioms ***
	From-kind of Cast differs from kind of enclosed type
	From-kind: forall (b :: Bool) -> *
	Kind of enclosed type: forall {b :: Bool}. *

The solution is to compare types for equality modulo visibility (ForAllTyFlag).
Updated functions:

	nonDetCmpType   (worker for eqType)
	eqDeBruijnType
	tc_eq_type      (worker for tcEqType)
	can_eq_nc

In order to retain the distinction between visible and invisible forall
in user-written code, we introduce a new ad-hoc check: checkEqForallVis.

27 files changed, 508 insertions, 80 deletions

diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs
index d94f97fb19..80595ce80e 100644
--- a/compiler/GHC/Core/Map/Type.hs
+++ b/compiler/GHC/Core/Map/Type.hs
@@ -38,7 +38,6 @@ import GHC.Prelude
 import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.TyCo.Rep
-import GHC.Core.TyCo.Compare( eqForAllVis )
 import GHC.Data.TrieMap
 
 import GHC.Data.FastString
@@ -261,11 +260,9 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
               -> liftEquality (tc == tc') `andEq` gos env env' tys tys'
           (LitTy l, LitTy l')
               -> liftEquality (l == l')
-          (ForAllTy (Bndr tv vis) ty, ForAllTy (Bndr tv' vis') ty')
-              -> -- See Note [ForAllTy and type equality] in
-                 -- GHC.Core.TyCo.Compare for why we use `eqForAllVis` here
-                 liftEquality (vis `eqForAllVis` vis') `andEq`
-                 go (D env (varType tv)) (D env' (varType tv')) `andEq`
+          (ForAllTy (Bndr tv _) ty, ForAllTy (Bndr tv' _) ty')
+              -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare
+              -> go (D env (varType tv)) (D env' (varType tv')) `andEq`
                  go (D (extendCME env tv) ty) (D (extendCME env' tv') ty')
           (CoercionTy {}, CoercionTy {})
               -> TEQ
diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs
index 4ef9d04eb8..564c38490f 100644
--- a/compiler/GHC/Core/TyCo/Compare.hs
+++ b/compiler/GHC/Core/TyCo/Compare.hs
@@ -16,7 +16,7 @@ module GHC.Core.TyCo.Compare (
     tcEqTyConApps,
 
    -- * Visiblity comparision
-   eqForAllVis, cmpForAllVis
+   eqForAllVis,
 
    ) where
 
@@ -171,11 +171,13 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
     go _   (LitTy lit1) (LitTy lit2)
       = lit1 == lit2
 
-    go env (ForAllTy (Bndr tv1 vis1) ty1)
-           (ForAllTy (Bndr tv2 vis2) ty2)
-      =  vis1 `eqForAllVis` vis2
-      && (vis_only || go env (varType tv1) (varType tv2))
-      && go (rnBndr2 env tv1 tv2) ty1 ty2
+    go env (ForAllTy (Bndr tv1 _) ty1)
+           (ForAllTy (Bndr tv2 _) ty2)
+      -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality]
+      = kinds_eq && go (rnBndr2 env tv1 tv2) ty1 ty2
+      where
+        kinds_eq | vis_only  = True
+                 | otherwise = go env (varType tv1) (varType tv2)
 
     -- Make sure we handle all FunTy cases since falling through to the
     -- AppTy case means that tcSplitAppTyNoView_maybe may see an unzonked
@@ -227,7 +229,9 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
 
 -- | Do these denote the same level of visibility? 'Required'
 -- arguments are visible, others are not. So this function
--- equates 'Specified' and 'Inferred'. Used for printing.
+-- equates 'Specified' and 'Inferred'.
+--
+-- Used for printing and in tcEqForallVis.
 eqForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Bool
 -- See Note [ForAllTy and type equality]
 -- If you change this, see IMPORTANT NOTE in the above Note
@@ -235,28 +239,41 @@ eqForAllVis Required      Required      = True
 eqForAllVis (Invisible _) (Invisible _) = True
 eqForAllVis _             _             = False
 
--- | Do these denote the same level of visibility? 'Required'
--- arguments are visible, others are not. So this function
--- equates 'Specified' and 'Inferred'. Used for printing.
-cmpForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Ordering
--- See Note [ForAllTy and type equality]
--- If you change this, see IMPORTANT NOTE in the above Note
-cmpForAllVis Required      Required       = EQ
-cmpForAllVis Required      (Invisible {}) = LT
-cmpForAllVis (Invisible _) Required       = GT
-cmpForAllVis (Invisible _) (Invisible _)  = EQ
-
-
 {- Note [ForAllTy and type equality]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we compare (ForAllTy (Bndr tv1 vis1) ty1)
          and    (ForAllTy (Bndr tv2 vis2) ty2)
-what should we do about `vis1` vs `vis2`.
-
-First, we always compare with `eqForAllVis` and `cmpForAllVis`.
-But what decision do we make?
-
-Should GHC type-check the following program (adapted from #15740)?
+what should we do about `vis1` vs `vis2`?
+
+An extensive discussion can be found at https://github.com/ghc-proposals/ghc-proposals/issues/558.
+A short summary of our options and the currently implemented design are described below.
+
+One option is to take those flags into account and check (vis1==vis2).
+But in Core, the visibilities of forall-bound variables have no meaning,
+as type abstraction and type application are always explicit.
+Going to great lengths to carry them around is counterproductive,
+but not going far enough may lead to Core Lint errors (#22762).
+
+The other option (the one we take) is to ignore those flags.
+Neither the name of a forall-bound variable nor its visibility flag
+affect GHC's notion of type equality.
+
+That said, the visibilities of foralls do matter
+a great deal in user-written programs. For example, if we unify tv := T, where
+  tv :: forall k.   k -> Type
+  T  :: forall k -> k -> Type
+then the user cannot substitute `T Maybe` for `tv Maybe` in their program
+by hand. They'd have to write `T (Type -> Type) Maybe` instead.
+This entails a loss of referential transparency. We solve this issue by
+checking the flags in the (source-language) type checker, not in the
+(Core language) equality relation `eqType`. All checks of forall visibility
+are listed in Note [Use sites of checkEqForallVis].
+
+These checks use `eqForAllVis` to compare the `ForAllTyFlag`s.
+But should we perhaps use (==) instead?
+Do we only care about visibility (Required vs Invisible)
+or do we also care about specificity (Specified vs Inferred)?
+For example, should GHC type-check the following program (adapted from #15740)?
 
   {-# LANGUAGE PolyKinds, ... #-}
   data D a
@@ -280,34 +297,15 @@ programs like the one above. Whether a kind variable binder ends up being
 specified or inferred can be somewhat subtle, however, especially for kinds
 that aren't explicitly written out in the source code (like in D above).
 
-For now, we decide
-
-    the specified/inferred status of an invisible type variable binder
-    does not affect GHC's notion of equality.
-
-That is, we have the following:
-
-  --------------------------------------------------
-  | Type 1            | Type 2            | Equal? |
-  --------------------|-----------------------------
-  | forall k. <...>   | forall k. <...>   | Yes    |
-  |                   | forall {k}. <...> | Yes    |
-  |                   | forall k -> <...> | No     |
-  --------------------------------------------------
-  | forall {k}. <...> | forall k. <...>   | Yes    |
-  |                   | forall {k}. <...> | Yes    |
-  |                   | forall k -> <...> | No     |
-  --------------------------------------------------
-  | forall k -> <...> | forall k. <...>   | No     |
-  |                   | forall {k}. <...> | No     |
-  |                   | forall k -> <...> | Yes    |
-  --------------------------------------------------
-
-IMPORTANT NOTE: if we want to change this decision, ForAllCo will need to carry
-visiblity (by taking a ForAllTyBinder rathre than a TyCoVar), so that
-coercionLKind/RKind build forall types that match (are equal to) the desired
-ones.  Otherwise we get an infinite loop in the solver via canEqCanLHSHetero.
-Examples: T16946, T15079.
+For now, we decide to ignore specificity. That is, we have the following:
+
+  eqForAllVis Required      Required      = True
+  eqForAllVis (Invisible _) (Invisible _) = True
+  eqForAllVis _             _             = False
+
+One unfortunate consequence of this setup is that it can be exploited
+to observe the order of inferred quantification (#22648). However, fixing this
+would be a breaking change, so we choose not to (at least for now).
 
 Historical Note [Typechecker equality vs definitional equality]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -335,7 +333,7 @@ is more finer-grained than definitional equality in two places:
   Constraint, but typechecker treats them as distinct types.
 
 * Unlike definitional equality, which does not care about the ForAllTyFlag of a
-  ForAllTy, typechecker equality treats Required type variable binders as
+  ForAllTy, typechecker equality treated Required type variable binders as
   distinct from Invisible type variable binders.
   See Note [ForAllTy and type equality]
 
@@ -513,9 +511,9 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
 
     go env (TyVarTy tv1)       (TyVarTy tv2)
       = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
-    go env (ForAllTy (Bndr tv1 vis1) t1) (ForAllTy (Bndr tv2 vis2) t2)
-      = liftOrdering (vis1 `cmpForAllVis` vis2)
-        `thenCmpTy` go env (varType tv1) (varType tv2)
+    go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2)
+      -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality]
+      = go env (varType tv1) (varType tv2)
         `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
 
         -- See Note [Equality on AppTys]
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 5cc8ab5f64..94f4d7b7df 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1315,6 +1315,12 @@ instance Diagnostic TcRnMessage where
     TcRnSectionWithoutParentheses expr -> mkSimpleDecorated $
       hang (text "A section must be enclosed in parentheses")
          2 (text "thus:" <+> (parens (ppr expr)))
+    TcRnIncompatibleForallVisibility act exp ->
+      mkSimpleDecorated $
+        hang (text "Visibilities of forall-bound variables are not compatible") 2 $
+        vcat
+          [ text "Expected:" <+> ppr exp
+          , text "  Actual:" <+> ppr act ]
 
     TcRnCapturedTermName tv_name shadowed_term_names
       -> mkSimpleDecorated $
@@ -2311,7 +2317,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnInterfaceError err
       -> interfaceErrorReason err
-
+    TcRnIncompatibleForallVisibility{}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -2913,6 +2920,8 @@ instance Diagnostic TcRnMessage where
       -> [SuggestAddTypeSignatures UnnamedBinding]
     TcRnInterfaceError reason
       -> interfaceErrorHints reason
+    TcRnIncompatibleForallVisibility{}
+      -> noHints
 
   diagnosticCode = constructorCode
 
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 38615d0f0d..e80aaae161 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -3804,6 +3804,22 @@ data TcRnMessage where
   TcRnTypeSynonymCycle :: !TySynCycleTyCons -- ^ The tycons involved in the cycle
                        -> TcRnMessage
 
+  {-| TcRnIncompatibleForallVisibility is an error that occurs when
+      the expected and actual types contain forall-bound variables
+      that have incompatible visibilities.
+
+      Example:
+        type family Invis :: Type -> forall a. a
+        type family Vis   :: Type -> forall a -> a
+        type instance Vis = Invis   -- Bad instance
+
+      Test cases: T18863a VisFlag1 VisFlag1_ql VisFlag2 VisFlag3 VisFlag4 VisFlag5
+  -}
+  TcRnIncompatibleForallVisibility
+    :: TcType
+    -> TcType
+    -> TcRnMessage
+
   deriving Generic
 
 -- | Things forbidden in @type data@ declarations.
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 818ec4e991..4bfcf3128a 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -352,6 +352,11 @@ tcApp rn_expr exp_res_ty
                  = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $
                    thing_inside
 
+       -- QL may have instantiated some delta variables to polytypes.
+       -- Zonk before we call checkEqForallVis (and possibly tcSubTypeDS),
+       -- as those functions do not expect polytypes inside unification variables.
+       ; app_res_rho <- zonkQuickLook do_ql app_res_rho
+
        -- Match up app_res_rho: the result type of rn_expr
        --     with exp_res_ty:  the expected result type
        ; do_ds <- xoptM LangExt.DeepSubsumption
@@ -368,10 +373,14 @@ tcApp rn_expr exp_res_ty
                  -- Even though both app_res_rho and exp_res_ty are rho-types,
                  -- they may have nested polymorphism, so if deep subsumption
                  -- is on we must call tcSubType.
-                 -- Zonk app_res_rho first, because QL may have instantiated some
-                 -- delta variables to polytypes, and tcSubType doesn't expect that
-                 do { app_res_rho <- zonkQuickLook do_ql app_res_rho
-                    ; tcSubTypeDS rn_expr app_res_rho exp_res_ty }
+                 tcSubTypeDS rn_expr app_res_rho exp_res_ty
+
+       -- See Note [Use sites of checkEqForallVis]
+       --   This particular call is commented out because we do not have
+       --   visible forall in types of terms yet (#281), so it is a no-op.
+       -- ; case exp_res_ty of
+       --     Check res_ty -> checkEqForallVis app_res_rho res_ty
+       --     Infer _      -> return ()
 
        -- Typecheck the value arguments
        ; tc_args <- tcValArgs do_ql inst_args
@@ -1041,14 +1050,14 @@ qlUnify delta ty1 ty2
       | -- See Note [Actual unification in qlUnify]
         let ty2_tvs = shallowTyCoVarsOfType ty2
       , not (ty2_tvs `intersectsVarSet` bvs2)
-          -- Can't instantiate a delta-varto a forall-bound variable
+          -- Can't instantiate a delta-var to a forall-bound variable
       , Just ty2 <- occCheckExpand [kappa] ty2
           -- Passes the occurs check
       = do { let ty2_kind   = typeKind ty2
                  kappa_kind = tyVarKind kappa
            ; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
                    -- unifyKind: see Note [Actual unification in qlUnify]
-
+           ; checkEqForallVis ty2_kind kappa_kind  -- See Note [Use sites of checkEqForallVis]
            ; traceTc "qlUnify:update" $
              vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
                        2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 9e8375b47d..4ab6147081 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1930,13 +1930,16 @@ checkExpectedKind hs_ty ty act_kind exp_kind
 
        ; let res_ty = ty `mkAppTys` new_args
 
-       ; if act_kind' `tcEqType` exp_kind
+       ; res_ty' <-
+         if act_kind' `tcEqType` exp_kind
          then return res_ty  -- This is very common
          else do { co_k <- uType KindLevel origin act_kind' exp_kind
                  ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
                                                      , ppr exp_kind
                                                      , ppr co_k ])
-                ; return (res_ty `mkCastTy` co_k) } }
+                 ; return (res_ty `mkCastTy` co_k) }
+       ; checkEqForallVis act_kind' exp_kind   -- See Note [Use sites of checkEqForallVis]
+       ; return res_ty' }
     where
       -- We need to make sure that both kinds have the same number of implicit
       -- foralls out front. If the actual kind has more, instantiate accordingly.
@@ -2551,7 +2554,8 @@ kcCheckDeclHeader_sig sig_kind name flav
                  ; case ctx_k of
                       AnyKind -> return ()   -- No signature
                       _ -> do { res_ki <- newExpectedKind ctx_k
-                              ; discardResult (unifyKind Nothing sig_res_kind' res_ki) }
+                              ; discardResult (unifyKind Nothing sig_res_kind' res_ki)
+                              ; checkEqForallVis sig_res_kind' res_ki }  -- See Note [Use sites of checkEqForallVis]
 
                  -- Add more binders for data/newtype, so the result kind has no arrows
                  -- See Note [Datatype return kinds]
@@ -2662,7 +2666,8 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside
     tc_hs_bndr (KindedTyVar _ _ (L _ hs_nm) lhs_kind) expected_kind
       = do { sig_kind <- tcLHsKindSig (TyVarBndrKindCtxt hs_nm) lhs_kind
            ; discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
-             unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind }
+             unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind
+           ; checkEqForallVis sig_kind expected_kind }  -- See Note [Use sites of checkEqForallVis]
 
 substTyConBinderX :: Subst -> TyConBinder -> (Subst, TyConBinder)
 substTyConBinderX subst (Bndr tv vis)
@@ -3288,6 +3293,7 @@ bindExplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_ki
                           -- This unify rejects:
                           --    class C (m :: * -> *) where
                           --      type F (m :: *) = ...
+           ; checkEqForallVis kind (tyVarKind tv)  -- See Note [Use sites of checkEqForallVis]
            ; return tv }
 
       | otherwise
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index 2a76792790..6614dbdc51 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -216,9 +216,8 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
   = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
 
 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-           s1@(ForAllTy (Bndr _ vis1) _) _
-           s2@(ForAllTy (Bndr _ vis2) _) _
-  | vis1 `eqForAllVis` vis2 -- Note [ForAllTy and type equality]
+           s1@ForAllTy{} _
+           s2@ForAllTy{} _
   = can_eq_nc_forall ev eq_rel s1 s2
 
 -- See Note [Canonicalising type applications] about why we require rewritten types
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index caae46ce36..6a5b7230bc 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -922,6 +922,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity
                   -- is none)
                   ; let hs_lhs = nlHsTyConApp NotPromoted fixity (getName fam_tc) hs_pats
                   ; _ <- unifyKind (Just . HsTypeRnThing $ unLoc hs_lhs) lhs_applied_kind res_kind
+                  ; checkEqForallVis lhs_applied_kind res_kind  -- See Note [Use sites of checkEqForallVis]
 
                   ; traceTc "tcDataFamInstHeader" $
                     vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind, ppr m_ksig]
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 873ff2979a..1bf4121501 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -68,6 +68,10 @@ module GHC.Tc.Utils.TcMType (
   inferResultToType, ensureMonoType, promoteTcType,
 
   --------------------------------
+  -- Visibility flag check
+  tcEqForallVis, checkEqForallVis,
+
+  --------------------------------
   -- Zonking and tidying
   zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
   zonkTidyFRRInfos,
@@ -606,6 +610,213 @@ tc_infer mb_frr tc_check
 
 {- *********************************************************************
 *                                                                      *
+              Visibility flag check
+*                                                                      *
+********************************************************************* -}
+
+-- Check if two presumably equal types actually differ in the visibility
+-- of their foralls. Example (from #18863):
+--
+--   type IDa :: forall i -> i -> Type
+--   data IDa :: forall i.   i -> Type
+--
+-- Report TcRnIncompatibleForallVisibility if the visibilities differ,
+-- as in the example above.
+--
+-- See Note [Presumably equal types] and Note [Use sites of checkEqForallVis]
+checkEqForallVis :: TcType -> TcType -> TcM ()
+checkEqForallVis ty1 ty2 =
+  unless (tcEqForallVis ty1 ty2) $
+    addErr $ TcRnIncompatibleForallVisibility ty1 ty2
+
+-- Structurally match two presumably equal types, checking that all pairs of
+-- foralls have equal visibilities.
+--
+-- See Note [Presumably equal types]
+tcEqForallVis :: Type -> Type -> Bool
+tcEqForallVis = matchUpForAllTyFlags eqForAllVis
+  -- This is the only use of matchUpForAllTyFlags at the moment.
+
+-- Structurally match two presumably equal types, checking that all pairs of
+-- forall visibility flags (ForAllTyFlag) satisfy a predicate.
+--
+-- For example, given the types
+--     ty1 = forall a1. Bool -> forall b1.   ...
+--     ty2 = forall a2. Bool -> forall b2 -> ...
+-- We have
+--     matchUpForAllTyFlags f ty1 ty2 =
+--        f Specified Specified &&   -- from (a1, a2)
+--        f Specified Required       -- from (b1, b2)
+--
+-- Metavariables are of no interest to us: they stand for monotypes, so there
+-- are no forall flags to be found. We do not look through metavariables.
+--
+-- See Note [Presumably equal types]
+matchUpForAllTyFlags
+  :: (ForAllTyFlag -> ForAllTyFlag -> Bool)
+  -> TcType     -- actual
+  -> TcType     -- expected
+  -> Bool
+matchUpForAllTyFlags zip_flags actual expected =
+    go actual expected True
+  where
+    go :: TcType -> TcType -> Bool -> Bool
+    -- See Note [Comparing nullary type synonyms] in GHC.Core.Type
+    go (TyConApp tc1 []) (TyConApp tc2 []) cont | tc1 == tc2 = cont
+
+    go t1 t2 cont | Just t1' <- coreView t1 = go t1' t2 cont
+    go t1 t2 cont | Just t2' <- coreView t2 = go t1 t2' cont
+
+    go (LitTy lit1) (LitTy lit2) cont
+      | lit1 /= lit2 = True  -- See Note [Presumably equal types]
+      | otherwise    = cont
+
+    go (ForAllTy (Bndr tv1 vis1) ty1) (ForAllTy (Bndr tv2 vis2) ty2) cont
+      = go (varType tv1) (varType tv2) $
+        go ty1 ty2 $
+        zip_flags vis1 vis2 && cont
+
+    go (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2) cont =
+      go arg1 arg2 $ go res1 res2 $ go w1 w2 $ cont
+    go (AppTy s1 t1) (AppTy s2 t2) cont =
+      go s1 s2 $ go t1 t2 $ cont
+    go (TyConApp tc1 ts1) (TyConApp tc2 ts2) cont
+      | tc1 /= tc2 = True    -- See Note [Presumably equal types]
+      | otherwise  = gos ts1 ts2 cont
+
+    go (CastTy t1 _) t2               cont = go t1 t2 cont
+    go t1            (CastTy t2 _)    cont = go t1 t2 cont
+    go _             _                cont = cont
+
+    gos (t1:ts1) (t2:ts2) cont = gos ts1 ts2 $ go t1 t2 cont
+    gos []       []       cont = cont
+    gos _        _        _    = True    -- See Note [Presumably equal types]
+
+{- Note [Presumably equal types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In matchUpForAllTyFlags (and by extension tcEqForallVis, checkEqForallVis)
+we assume that there is always a separate (possibly subsequent) check for
+  t1 `eqType` t2
+eqType defines the equality relation that we are checking, but the actual
+check may be performed by tcEqType or uType (unifyType/unifyKind).
+
+So `matchUpForAllTyFlags` should return True (i.e. "no problem") if the types
+appear to differ. Examples:
+* t1 is a unification variable and t2 is Int.
+  Later they will be unified -- no problems here!
+* t1 is Int and t2 is Bool.
+  Later that will cause an error -- and it's bad for `checkEqForallVis`
+  to complain instead about mismatched visibilities.
+
+Note carefully that foralls can't hide inside unification variables
+(unification variables stand for monotypes) so there is no danger of
+missing a visiblitly mismatch with
+   alpha ~ (forall a -> blah)
+where alpha is subsequently unified with (forall a. blah).
+That latter unification can't happen. Quick Look does use unification variables
+(so called "instantiation variables") but they are short lived.
+
+To reiterate, the ideal scenario is that `matchUpForAllTyFlags` returns True
+when (ty1 /= ty2). In practice, however, it would make the check more
+complicated and expensive. For instance, we'd have to maintain a RnEnv2
+to check type variables for equality. To make our lives easier, we follow
+this principle on a best-effort basis. The worst case scenario is that
+we report a less helpful error message.
+-}
+
+{- Note [Use sites of checkEqForallVis]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The calls to checkEqForallVis must be carefully placed to cover all cases
+but at the same time not incur the performance cost of excessive checking.
+
+Here we list all use sites of checkEqForallVis and examples of code covered
+by that particular call. First, some helper definitions used in the examples:
+
+    type family InvisF :: Type -> forall a.   a
+    type family VisF   :: Type -> forall a -> a
+
+    type V :: forall k -> k -> Type
+    data V k (a :: k) = MkV
+
+    f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+    f _ = ()
+
+With those definitions in mind, here are the examples of code
+for each call to checkEqForallVis:
+
+1. The call in GHC.Tc.Gen.HsType.checkExpectedKind
+  1a)
+    Used when kind-checking type family instances (test: VisFlag2)
+        type instance VisF = InvisF
+        type instance InvisF = VisF
+    Here we try to unify the kinds of VisF and InvisF:
+        (Type -> forall a -> a) ~ (Type -> forall a. a)
+  1b)
+    Used when kind-checking type applications (test: VisFlag1)
+        bad_tyapp :: ()
+        bad_tyapp = f @V MkV
+    Here we use type applications to instantiatie hk := V (where hk is a type parameter of f),
+    therefore we unify their kinds
+        (forall j. j -> Type) ~ (forall k -> k -> Type)
+
+2. The call in GHC.Tc.Gen.App.qlUnify
+    Used when kind-checking Quick Look instantiations (test: VisFlag1_ql)
+        {-# LANGUAGE ImpredicativeTypes #-}
+        bad_infer :: ()
+        bad_infer = f MkV
+    Here Quick Look tries to instantiate hk := V (where hk is a type parameter of f),
+    therefore we unify their kinds
+        (forall j. j -> Type) ~ (forall k -> k -> Type)
+
+3. The call in GHC.Tc.Utils.Unify.uUnfilledVar2
+    Used when kind-checking inferred type variable instantiations (test: VisFlag1)
+        bad_infer :: ()
+        bad_infer = f MkV
+    Here the unifier tries to fill in hk := V (where hk is a type parameter of f),
+    therefore we unify their kinds
+        (forall j. j -> Type) ~ (forall k -> k -> Type)
+
+4. The call in GHC.Tc.Gen.HsType.kcCheckDeclHeader_sig
+    Used when checking the result kind annotation
+    in type declarations with standalone kind signatures (test: T18863a)
+        type IDa :: forall i -> i -> Type
+        data IDa :: forall i.   i -> Type
+    Here we unify the inline kind signature with the SAKS
+        (forall i -> i -> Type) ~ (forall i. i -> Type)
+
+5. The call in GHC.Tc.Gen.HsType.matchUpSigWithDecl
+    Used when checking kind annotations on type parameters
+    in type declarations with standalone kind signatures (test: VisFlag4)
+        type C :: (forall k -> k -> k) -> Constraint
+        class C (hk :: forall k. k -> k) where
+    Here we unify the inline kind signature on hk with the relevant
+    part of the SAKS
+        (forall k -> k -> k) ~ (forall k. k -> k)
+
+6. The call in GHC.Tc.Gen.HsType.bindExplicitTKBndrsX
+    Used when checking kind annotations on type parameters
+    of associated type families (test: VisFlag3)
+        class C (hk :: forall k. k -> k) where
+          type F (hk :: forall k -> k -> k)
+    Here we unify the kinds given to hk in F and C
+        (forall k. k -> k) ~ (forall k -> k -> k)
+
+7. The call in GHC.Tc.TyCl.Instance.tcDataFamInstHeader
+    Used when checking the result kind annotation
+    of data family instances (test: VisFlag5)
+        data family   D a   :: (forall i -> i -> i) -> Type
+        data instance D Int :: (forall i.   i -> i) -> Type
+    Here we unify the result kinds in the data family header
+    and the data instance
+        ((forall i -> i -> i) -> Type) ~ ((forall i. i -> i) -> Type)
+
+8. The call in GHC.Tc.Gen.App.tcApp (commented out)
+    The commented out call in tcApp marks the spot where we should
+    perform the check when we implement visible forall in terms (#281).
+-}
+
+{- *********************************************************************
+*                                                                      *
               Promoting types
 *                                                                      *
 ********************************************************************* -}
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index fc5728cc81..2d8e70ff64 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -2080,6 +2080,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
          then not_ok_so_defer
          else
     do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1)
+       ; checkEqForallVis (typeKind ty2) (tyVarKind tv1)  -- See Note [Use sites of checkEqForallVis]
        ; traceTc "uUnfilledVar2 ok" $
          vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
               , ppr ty2 <+> dcolon <+> ppr (typeKind  ty2)
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index e5d7a84bb6..a42e8e4191 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -577,6 +577,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnIncoherentRoles"                           = 18273
   GhcDiagnosticCode "TcRnTyFamNameMismatch"                         = 88221
   GhcDiagnosticCode "TcRnTypeSynonymCycle"                          = 97522
+  GhcDiagnosticCode "TcRnIncompatibleForallVisibility"              = 25115
 
   -- PatSynInvalidRhsReason
   GhcDiagnosticCode "PatSynNotInvertible"                           = 69317
diff --git a/testsuite/tests/saks/should_fail/T18863a.stderr b/testsuite/tests/saks/should_fail/T18863a.stderr
index c36a102530..a9808fe760 100644
--- a/testsuite/tests/saks/should_fail/T18863a.stderr
+++ b/testsuite/tests/saks/should_fail/T18863a.stderr
@@ -1,5 +1,6 @@
 
-T18863a.hs:9:1: error: [GHC-83865]
-    • Couldn't match expected kind: forall i. i -> *
-                  with actual kind: forall i -> i -> *
+T18863a.hs:9:1: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall i. i -> *
+          Actual: forall i -> i -> *
     • In the data type declaration for ‘IDa’
diff --git a/testsuite/tests/typecheck/should_compile/T22762.hs b/testsuite/tests/typecheck/should_compile/T22762.hs
new file mode 100644
index 0000000000..512e6e8ecd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22762.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T22762 where
+
+import Data.Kind
+
+type Const :: a -> b -> a
+type family Const x y where
+  Const x _ = x
+
+type F :: (forall (b :: Bool) -> Const Type b) -> Type
+data F f
+
+type G :: forall (b :: Bool) -> Type
+data G b
+
+type H :: Type
+type family H where
+  H = F G
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 7ef8cc4fa6..776fb4669d 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -874,3 +874,4 @@ test('QualifiedRecordUpdate',
 test('T23171', normal, compile, [''])
 test('T23192', normal, compile, [''])
 test('T23199', normal, compile, [''])
+test('T22762', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag1.hs b/testsuite/tests/typecheck/should_fail/VisFlag1.hs
new file mode 100644
index 0000000000..55dfdf80f4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag1.hs
@@ -0,0 +1,18 @@
+module VisFlag1 where
+
+import Data.Kind (Type)
+
+type V :: forall k -> k -> Type
+data V k (a :: k) = MkV
+
+f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+f _ = ()
+
+bad_tyapp :: ()
+bad_tyapp = f @V MkV
+
+bad_wild :: ()
+bad_wild = f @_ MkV
+
+bad_infer :: ()
+bad_infer = f MkV
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag1.stderr b/testsuite/tests/typecheck/should_fail/VisFlag1.stderr
new file mode 100644
index 0000000000..6593233fb9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag1.stderr
@@ -0,0 +1,23 @@
+
+VisFlag1.hs:12:16: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall j. j -> *
+          Actual: forall k -> k -> *
+    • In the type ‘V’
+      In the expression: f @V MkV
+      In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
+
+VisFlag1.hs:15:15: error: [GHC-91028]
+    • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall j. j -> *
+    • In the expression: f @_ MkV
+      In an equation for ‘bad_wild’: bad_wild = f @_ MkV
+
+VisFlag1.hs:18:15: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall j. j -> *
+          Actual: forall k -> k -> *
+    • In the first argument of ‘f’, namely ‘MkV’
+      In the expression: f MkV
+      In an equation for ‘bad_infer’: bad_infer = f MkV
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag1_ql.hs b/testsuite/tests/typecheck/should_fail/VisFlag1_ql.hs
new file mode 100644
index 0000000000..009cb5643f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag1_ql.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module VisFlag1_ql where
+
+import Data.Kind (Type)
+
+type V :: forall k -> k -> Type
+data V k (a :: k) = MkV
+
+f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+f _ = ()
+
+bad_tyapp :: ()
+bad_tyapp = f @V MkV
+
+bad_wild :: ()
+bad_wild = f @_ MkV
+
+bad_infer :: ()
+bad_infer = f MkV
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr b/testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr
new file mode 100644
index 0000000000..ef5476f69b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr
@@ -0,0 +1,23 @@
+
+VisFlag1_ql.hs:14:16: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall j. j -> *
+          Actual: forall k -> k -> *
+    • In the type ‘V’
+      In the expression: f @V MkV
+      In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
+
+VisFlag1_ql.hs:17:15: error: [GHC-91028]
+    • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall j. j -> *
+    • In the expression: f @_ MkV
+      In an equation for ‘bad_wild’: bad_wild = f @_ MkV
+
+VisFlag1_ql.hs:20:15: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall j. j -> *
+          Actual: forall k -> k -> *
+    • In the first argument of ‘f’, namely ‘MkV’
+      In the expression: f MkV
+      In an equation for ‘bad_infer’: bad_infer = f MkV
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag2.hs b/testsuite/tests/typecheck/should_fail/VisFlag2.hs
new file mode 100644
index 0000000000..0c68bfee2b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module VisFlag2 where
+
+import Data.Kind (Type)
+
+-- the (Type ->) parameter is to prevent instantiation of invisible variables
+
+type family Invis :: Type -> forall a.   a
+type family Vis   :: Type -> forall a -> a
+
+type instance Vis = Invis  -- Bad
+type instance Invis = Vis  -- Bad
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag2.stderr b/testsuite/tests/typecheck/should_fail/VisFlag2.stderr
new file mode 100644
index 0000000000..efe0bd6fa2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag2.stderr
@@ -0,0 +1,14 @@
+
+VisFlag2.hs:13:21: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: * -> forall a -> a
+          Actual: * -> forall a. a
+    • In the type ‘Invis’
+      In the type instance declaration for ‘Vis’
+
+VisFlag2.hs:14:23: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: * -> forall a. a
+          Actual: * -> forall a -> a
+    • In the type ‘Vis’
+      In the type instance declaration for ‘Invis’
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag3.hs b/testsuite/tests/typecheck/should_fail/VisFlag3.hs
new file mode 100644
index 0000000000..518522b8ea
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag3.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module VisFlag3 where
+
+class C (hk :: forall k. k -> k) where
+  type F (hk :: forall k -> k -> k)
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag3.stderr b/testsuite/tests/typecheck/should_fail/VisFlag3.stderr
new file mode 100644
index 0000000000..244c9c8bb7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag3.stderr
@@ -0,0 +1,6 @@
+
+VisFlag3.hs:6:3: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall k. k -> k
+          Actual: forall k -> k -> k
+    • In the associated type family declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag4.hs b/testsuite/tests/typecheck/should_fail/VisFlag4.hs
new file mode 100644
index 0000000000..752007f92e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag4.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module VisFlag4 where
+
+import Data.Kind
+
+type C :: (forall k -> k -> k) -> Constraint
+class C (hk :: forall k. k -> k) where
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag4.stderr b/testsuite/tests/typecheck/should_fail/VisFlag4.stderr
new file mode 100644
index 0000000000..9a67cb0a5f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag4.stderr
@@ -0,0 +1,6 @@
+
+VisFlag4.hs:8:1: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: forall k -> k -> k
+          Actual: forall k. k -> k
+    • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag5.hs b/testsuite/tests/typecheck/should_fail/VisFlag5.hs
new file mode 100644
index 0000000000..35da87b3e8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag5.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module VisFlag5 where
+
+import Data.Kind
+
+data family   D a   :: (forall i -> i -> i) -> Type
+data instance D Int :: (forall i.   i -> i) -> Type
diff --git a/testsuite/tests/typecheck/should_fail/VisFlag5.stderr b/testsuite/tests/typecheck/should_fail/VisFlag5.stderr
new file mode 100644
index 0000000000..5725a70c70
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/VisFlag5.stderr
@@ -0,0 +1,6 @@
+
+VisFlag5.hs:8:1: error: [GHC-25115]
+    • Visibilities of forall-bound variables are not compatible
+        Expected: (forall i. i -> i) -> *
+          Actual: (forall i -> i -> i) -> *
+    • In the data instance declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 0ae1fdd646..d949c6ab75 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -681,3 +681,9 @@ test('LazyFieldsDisabled', normal, compile_fail, [''])
 test('TyfamsDisabled', normal, compile_fail, [''])
 test('CommonFieldResultTypeMismatch', normal, compile_fail, [''])
 test('CommonFieldTypeMismatch', normal, compile_fail, [''])
+test('VisFlag1', normal, compile_fail, [''])
+test('VisFlag1_ql', normal, compile_fail, [''])
+test('VisFlag2', normal, compile_fail, [''])
+test('VisFlag3', normal, compile_fail, [''])
+test('VisFlag4', normal, compile_fail, [''])
+test('VisFlag5', normal, compile_fail, [''])