WIP: Visibility subsumptionwip/int-index/visibility-subsumption

32 files changed, 418 insertions, 45 deletions

diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs
index 3629bc11a9..44ede9ca98 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,8 @@ 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')
+              -> 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..a86c03d628 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,10 +171,9 @@ 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 env (ForAllTy (Bndr tv1 _) ty1)
+           (ForAllTy (Bndr tv2 _) ty2)
+      = (vis_only || go env (varType tv1) (varType tv2))
       && go (rnBndr2 env tv1 tv2) ty1 ty2
 
     -- Make sure we handle all FunTy cases since falling through to the
@@ -224,7 +223,6 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
 
 {-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].
 
-
 -- | 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.
@@ -235,17 +233,6 @@ 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -253,7 +240,7 @@ 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`.
+First, we always compare with `eqForAllVis`.
 But what decision do we make?
 
 Should GHC type-check the following program (adapted from #15740)?
@@ -513,10 +500,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)
-        `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
+    go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2)
+      = go env (varType tv1) (varType tv2)
+          `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
 
         -- See Note [Equality on AppTys]
     go env (AppTy s1 t1) ty2
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 112268097f..9cab90b834 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1673,6 +1673,18 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2
         -- to be helpful since this is just an unimplemented feature.
     return (main_msg, [])
 
+  -- The kinds of 'tv1' and 'ty2' contain forall-bound variables that
+  -- differ in visibility (ForAllTyFlag).
+  | check_eq_result `cterHasProblem` cteForallKindVisDiff
+  = do
+    let
+        reason = ForallKindVisDiff tv1 ty2
+        main_msg =
+          CannotUnifyVariable
+            { mismatchMsg       = headline_msg
+            , cannotUnifyReason = reason }
+    return (main_msg, [])
+
   | isSkolemTyVar tv1  -- ty2 won't be a meta-tyvar; we would have
                        -- swapped in Solver.Canonical.canEqTyVarHomo
     || isTyVarTyVar tv1 && not (isTyVarTy ty2)
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 9880c13a9c..2469b772be 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1226,6 +1226,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 "Visibility of forall-bound variables is not compatible") 2 $
+        vcat
+          [ text "Expected:" <+> ppr exp
+          , text "  Actual:" <+> ppr act ]
 
     TcRnCapturedTermName tv_name shadowed_term_names
       -> mkSimpleDecorated $
@@ -1734,6 +1740,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnDuplicateMinimalSig{}
       -> ErrorWithoutFlag
+    TcRnIncompatibleForallVisibility{}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -2173,6 +2181,8 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnDuplicateMinimalSig{}
       -> noHints
+    TcRnIncompatibleForallVisibility{}
+      -> noHints
 
   diagnosticCode = constructorCode
 
@@ -2970,6 +2980,10 @@ pprCannotUnifyVariableReason ctxt (DifferentTyVars tv_info)
 pprCannotUnifyVariableReason ctxt (RepresentationalEq tv_info mb_coercible_msg)
   = pprTyVarInfo ctxt tv_info
   $$ maybe empty pprCoercibleMsg mb_coercible_msg
+pprCannotUnifyVariableReason _ (ForallKindVisDiff tv1 ty2)
+  = hang (text "Visibility of forall-bound variables in kinds differs") 2 $
+    vcat [ ppr tv1 <+> text "::" <+> ppr (tyVarKind tv1)
+         , ppr ty2 <+> text "::" <+> ppr (typeKind ty2) ]
 
 pprMismatchMsg :: SolverReportErrCtxt -> MismatchMsg -> SDoc
 pprMismatchMsg ctxt
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index c1b8461839..5cb94bac68 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -2924,6 +2924,29 @@ data TcRnMessage where
   -}
   TcRnDuplicateMinimalSig :: LSig GhcPs -> LSig GhcPs -> [LSig GhcPs] -> TcRnMessage
 
+  {-| TcRnIncompatibleForallVisibility is an error that occurs when
+      the expected and actual types contain forall-bound variables
+      that have incompatible visibility or specificity.
+
+      Example:
+        type family Invis :: Type -> forall a. a
+        type family Vis   :: Type -> forall a -> a
+        type instance Vis = Invis   -- Bad instance
+
+      Test cases:
+        T18863a
+        T15079_fail_a
+        T22648a
+        T22648b
+        T22648c
+        T22648v
+        T22648v_ql
+  -}
+  TcRnIncompatibleForallVisibility
+    :: TcType
+    -> TcType
+    -> TcRnMessage
+
   deriving Generic
 
 -- | Things forbidden in @type data@ declarations.
@@ -3787,6 +3810,20 @@ data CannotUnifyVariableReason
   -- type Int, or with a 'TyVarTv'.
   | DifferentTyVars TyVarInfo
   | RepresentationalEq TyVarInfo (Maybe CoercibleMsg)
+
+  -- | Can't unify a kind-polymorphic type variable with a type
+  -- due to visibility difference of forall-bound variables in their kinds.
+  --
+  -- Example:
+  --    data V k (a :: k) = MkV
+  --    f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+  --    bad_infer = f MkV
+  --        -- we want to unify hk := V
+  --        --   but  hk :: forall j.   j -> Type
+  --        --        V  :: forall k -> k -> Type
+  --
+  -- Test cases: T15079_fail_b T22648v
+  | ForallKindVisDiff TyVar Type
   deriving Generic
 
 -- | Report a mismatch error without any extra
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 06158cace3..d3388d0f24 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -362,6 +362,7 @@ tcApp rn_expr exp_res_ty
                  -- so with simple subsumption we can just unify them
                  -- No need to zonk; the unifier does that
                  do { co <- unifyExpectedType rn_expr app_res_rho exp_res_ty
+                    ; checkSubVis app_res_rho exp_res_ty
                     ; return (mkWpCastN co) }
 
             else -- Deep subsumption
@@ -371,6 +372,7 @@ tcApp rn_expr exp_res_ty
                  -- 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
+                    ; checkSubVis app_res_rho exp_res_ty
                     ; tcSubTypeDS rn_expr app_res_rho exp_res_ty }
 
        -- Typecheck the value arguments
@@ -1052,7 +1054,7 @@ qlUnify delta ty1 ty2
                  kappa_kind = tyVarKind kappa
            ; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
                    -- unifyKind: see Note [Actual unification in qlUnify]
-
+           ; checkSubVis ty2_kind (Check kappa_kind)
            ; 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 222755f6c9..651193bb2b 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1931,6 +1931,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind
 
        ; let res_ty = ty `mkAppTys` new_args
 
+       ; checkSubVis act_kind' (mkCheckExpType exp_kind)
        ; 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
@@ -2552,6 +2553,7 @@ kcCheckDeclHeader_sig sig_kind name flav
                  ; case ctx_k of
                       AnyKind -> return ()   -- No signature
                       _ -> do { res_ki <- newExpectedKind ctx_k
+                              ; checkSubVis res_ki (mkCheckExpType sig_res_kind')
                               ; discardResult (unifyKind Nothing sig_res_kind' res_ki) }
 
                  -- Add more binders for data/newtype, so the result kind has no arrows
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index ea2d95e80d..9dd55ede48 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -1095,9 +1095,8 @@ can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
   = canTyConApp rewritten 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/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 0623acd3d5..bad9f781a7 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -34,6 +34,7 @@ module GHC.Tc.Types.Constraint (
         CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck,
         cteOK, cteImpredicative, cteTypeFamily,
         cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble,
+        cteForallKindVisDiff,
 
         cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
         cterRemoveProblem, cterHasOccursCheck, cterFromKind,
@@ -452,12 +453,13 @@ cterHasNoProblem _        = False
 -- | An individual problem that might be logged in a 'CheckTyEqResult'
 newtype CheckTyEqProblem = CTEP Word8
 
-cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs :: CheckTyEqProblem
+cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs, cteForallKindVisDiff :: CheckTyEqProblem
 cteImpredicative   = CTEP (bit 0)   -- forall or (=>) encountered
 cteTypeFamily      = CTEP (bit 1)   -- type family encountered
 cteInsolubleOccurs = CTEP (bit 2)   -- occurs-check
 cteSolubleOccurs   = CTEP (bit 3)   -- occurs-check under a type function or in a coercion
                                     -- must be one bit to the left of cteInsolubleOccurs
+cteForallKindVisDiff = CTEP (bit 4) -- differing visibility of forall-bound variables in the kind
 -- See also Note [Insoluble occurs check] in GHC.Tc.Errors
 
 cteProblem :: CheckTyEqProblem -> CheckTyEqResult
@@ -521,7 +523,8 @@ instance Outputable CheckTyEqResult where
       all_bits = [ (cteImpredicative,   "cteImpredicative")
                  , (cteTypeFamily,      "cteTypeFamily")
                  , (cteInsolubleOccurs, "cteInsolubleOccurs")
-                 , (cteSolubleOccurs,   "cteSolubleOccurs") ]
+                 , (cteSolubleOccurs,   "cteSolubleOccurs")
+                 , (cteForallKindVisDiff, "cteForallKindVisDiff") ]
       set_bits = [ text str
                  | (bitmask, str) <- all_bits
                  , cter `cterHasProblem` bitmask ]
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index d0afe71560..6e53b6dccb 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -67,6 +67,10 @@ module GHC.Tc.Utils.TcMType (
   inferResultToType, ensureMonoType, promoteTcType,
 
   --------------------------------
+  -- Visibility subsumption
+  tcSubVis, tcEqVis, checkSubVis,
+
+  --------------------------------
   -- Zonking and tidying
   zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
   zonkTidyFRRInfos,
@@ -606,6 +610,79 @@ tc_infer mb_frr tc_check
 
 {- *********************************************************************
 *                                                                      *
+              Visibility subsumption
+*                                                                      *
+********************************************************************* -}
+
+checkSubVis :: TcType -> ExpType -> TcM ()
+checkSubVis _   (Infer _)   = return ()
+checkSubVis ty1 (Check ty2) =
+  unless (tcSubVis ty1 ty2) $
+    addErr $ TcRnIncompatibleForallVisibility ty1 ty2
+
+tcEqVis :: Type -> Type -> Bool
+tcEqVis ty1 ty2 =
+    Semi.getAll (zipForAllTyFlags eq_vis ty1 ty2)
+  where
+    eq_vis :: ForAllTyFlag -> ForAllTyFlag -> Semi.All
+    eq_vis flag1 flag2 = Semi.All (flag1 == flag2)
+
+tcSubVis
+  :: Type     -- actual
+  -> Type     -- expected
+  -> Bool
+tcSubVis actual expected =
+    Semi.getAll (zipForAllTyFlags sub_vis actual expected)
+  where
+    sub_vis :: ForAllTyFlag -> ForAllTyFlag -> Semi.All
+    sub_vis Specified Inferred = Semi.All True
+    sub_vis flag1     flag2    = Semi.All (flag1 == flag2)
+
+zipForAllTyFlags
+  :: forall m. Monoid m =>
+    (ForAllTyFlag -> ForAllTyFlag -> m)
+  -> Type     -- actual
+  -> Type     -- expected
+  -> m
+zipForAllTyFlags zip_flags actual expected =
+    go (typeKind actual) (typeKind expected) Semi.<>
+    go actual expected
+  where
+    go :: Type -> Type -> m
+
+    -- See Note [Comparing nullary type synonyms] in GHC.Core.Type
+    go (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = mempty
+
+    go t1 t2 | Just t1' <- coreView t1 = go t1' t2
+    go t1 t2 | Just t2' <- coreView t2 = go t1 t2'
+
+    go (ForAllTy (Bndr tv1 vis1) ty1) (ForAllTy (Bndr tv2 vis2) ty2)
+      =  zip_flags vis1 vis2
+      Semi.<> go (varType tv1) (varType tv2)
+      Semi.<> go ty1 ty2
+
+    go (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2) =
+      go arg1 arg2 Semi.<> go res1 res2 Semi.<> go w1 w2
+
+    -- See Note [Equality on AppTys] in GHC.Core.Type
+    go (AppTy s1 t1) ty2
+      | Just (s2, t2) <- tcSplitAppTyNoView_maybe ty2
+      = go s1 s2 Semi.<> go t1 t2
+    go ty1 (AppTy s2 t2)
+      | Just (s1, t1) <- tcSplitAppTyNoView_maybe ty1
+      = go s1 s2 Semi.<> go t1 t2
+
+    go (TyConApp _ ts1) (TyConApp _ ts2) = gos ts1 ts2
+
+    go (CastTy t1 _) t2               = go t1 t2
+    go t1            (CastTy t2 _)    = go t1 t2
+    go _             _                = mempty
+
+    gos (t1:ts1) (t2:ts2) = go t1 t2 Semi.<> gos ts1 ts2
+    gos _        _        = mempty
+
+{- *********************************************************************
+*                                                                      *
               Promoting types
 *                                                                      *
 ********************************************************************* -}
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index eea0ed95ef..8344d95389 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -21,6 +21,7 @@ module GHC.Tc.Utils.Unify (
   unifyType, unifyKind, unifyExpectedType,
   uType, promoteTcType,
   swapOverTyVars, startSolvingByUnification,
+  tcSubVis,
 
   --------------------------------
   -- Holes
@@ -2636,12 +2637,13 @@ checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult
 --      case-analysis on 'lhs')
 --    * checkEqCanLHSFinish, which does not know the form of 'lhs'
 checkTypeEq lhs ty
-  = go ty
+  = go ty S.<> check_kind_vis (canEqLHSKind lhs) (typeKind ty)
   where
     impredicative      = cteProblem cteImpredicative
     type_family        = cteProblem cteTypeFamily
     insoluble_occurs   = cteProblem cteInsolubleOccurs
     soluble_occurs     = cteProblem cteSolubleOccurs
+    forall_kind_vis_diff = cteProblem cteForallKindVisDiff
 
     -- The GHCi runtime debugger does its type-matching with
     -- unification variables that can unify with a polytype
@@ -2721,3 +2723,8 @@ checkTypeEq lhs ty
       | ghci_tv   = \ _tc -> cteOK
       | otherwise = \ tc  -> (if isTauTyCon tc then cteOK else impredicative) S.<>
                              (if isFamFreeTyCon tc then cteOK else type_family)
+
+    check_kind_vis :: TcKind -> TcKind -> CheckTyEqResult
+    check_kind_vis k1 k2
+      | tcEqVis k1 k2 = cteOK
+      | otherwise     = forall_kind_vis_diff
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index d7b57113ee..89d9a03066 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -321,6 +321,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "SkolemEscape"                                  = 46956
   GhcDiagnosticCode "DifferentTyVars"                               = 25897
   GhcDiagnosticCode "RepresentationalEq"                            = 10283
+  GhcDiagnosticCode "ForallKindVisDiff"                             = 11809
 
   -- Typechecker/renamer diagnostic codes
   GhcDiagnosticCode "TcRnRedundantConstraints"                      = 30606
@@ -512,6 +513,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnUnexpectedDefaultSig"                      = 40700
   GhcDiagnosticCode "TcRnBindInBootFile"                            = 11247
   GhcDiagnosticCode "TcRnDuplicateMinimalSig"                       = 85346
+  GhcDiagnosticCode "TcRnIncompatibleForallVisibility"              = 25115
 
   -- IllegalNewtypeReason
   GhcDiagnosticCode "DoesNotHaveSingleField"                        = 23517
diff --git a/testsuite/tests/dependent/should_compile/T11966.hs b/testsuite/tests/dependent/should_compile/T11966.hs
index daad450f13..d1b7662a43 100644
--- a/testsuite/tests/dependent/should_compile/T11966.hs
+++ b/testsuite/tests/dependent/should_compile/T11966.hs
@@ -24,7 +24,7 @@ newtype HasDefault t = HasDefault t
 -- Interpretations
 data Expr k
 
-data Record (f :: forall k. k -> Type) =
+data Record (f :: forall {k}. k -> Type) =
   Record {rX :: Col f ('Column "x" 'PGInteger)
          ,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
          ,rZ :: Col f ('HasDefault 'PGText)}
diff --git a/testsuite/tests/indexed-types/should_compile/T15740a.hs b/testsuite/tests/indexed-types/should_compile/T15740a.hs
index f209e243c6..5b8881aa50 100644
--- a/testsuite/tests/indexed-types/should_compile/T15740a.hs
+++ b/testsuite/tests/indexed-types/should_compile/T15740a.hs
@@ -5,7 +5,7 @@ module T15740a where
 import Data.Kind
 import Data.Proxy
 
-type family F2 :: forall k. k -> Type
+type family F2 :: forall {k}. k -> Type
 
 -- This should succeed
 type instance F2 = Proxy
diff --git a/testsuite/tests/saks/should_compile/saks032.hs b/testsuite/tests/saks/should_compile/saks032.hs
index 612c66d8fc..ce33110341 100644
--- a/testsuite/tests/saks/should_compile/saks032.hs
+++ b/testsuite/tests/saks/should_compile/saks032.hs
@@ -4,11 +4,13 @@
 module SAKS_032 where
 
 import Data.Kind
-import Data.Proxy
 
 type Const :: Type -> forall k. k -> Type
 data Const a b = Const a
 
+type Proxy :: forall k. k -> Type
+data Proxy a = Proxy
+
 type F :: Type -> Type -> forall k. k -> Type
 type family F a b :: forall k. k -> Type where
   F () () = Proxy
diff --git a/testsuite/tests/saks/should_fail/T18863a.stderr b/testsuite/tests/saks/should_fail/T18863a.stderr
index c36a102530..3116546dcf 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]
+    • Visibility of forall-bound variables is 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/T15079.hs b/testsuite/tests/typecheck/should_compile/T15079.hs
index 22e86abc56..c20ada216e 100644
--- a/testsuite/tests/typecheck/should_compile/T15079.hs
+++ b/testsuite/tests/typecheck/should_compile/T15079.hs
@@ -15,7 +15,7 @@ import           GHC.Exts (Any)
 infixl 4 :==
 -- | Heterogeneous Leibnizian equality.
 newtype (a :: j) :== (b :: k)
-  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
+  = HRefl { hsubst :: forall (c :: forall {i :: Type}. i -> Type). c a -> c b }
 
 -----
 
@@ -29,9 +29,9 @@ coerce f = uncoerce . hsubst f . Coerce
 
 -----
 
-newtype Flay :: (forall (i :: Type). i -> i -> Type)
+newtype Flay :: (forall {i :: Type}. i -> i -> Type)
              -> forall (j :: Type). j -> forall (k :: Type). k -> Type where
-  Flay :: forall (p :: forall (i :: Type). i -> i -> Type)
+  Flay :: forall (p :: forall {i :: Type}. i -> i -> Type)
                  (j :: Type) (k :: Type) (a :: j) (b :: k).
           { unflay :: p a (MassageKind j b) } -> Flay p a b
 
@@ -44,7 +44,7 @@ fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl
 
 -----
 
-newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int)
+newtype Foo (f :: forall {a :: Type}. a -> Type) = MkFoo (f Int)
 data InferredProxy a = MkInferredProxy
 
 foo :: Foo InferredProxy
diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_a.hs b/testsuite/tests/typecheck/should_fail/T15079_fail_a.hs
new file mode 100644
index 0000000000..7cec93872f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15079_fail_a.hs
@@ -0,0 +1,9 @@
+module T15079_fail_a where
+
+import Data.Kind (Type)
+
+newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int)
+data InferredProxy a = MkInferredProxy
+
+foo :: Foo InferredProxy
+foo = MkFoo MkInferredProxy
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_a.stderr b/testsuite/tests/typecheck/should_fail/T15079_fail_a.stderr
new file mode 100644
index 0000000000..83765d7f82
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15079_fail_a.stderr
@@ -0,0 +1,7 @@
+
+T15079_fail_a.hs:8:12: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: forall a. a -> *
+          Actual: forall {k}. k -> *
+    • In the first argument of ‘Foo’, namely ‘InferredProxy’
+      In the type signature: foo :: Foo InferredProxy
diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_b.hs b/testsuite/tests/typecheck/should_fail/T15079_fail_b.hs
new file mode 100644
index 0000000000..227839c7b9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15079_fail_b.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T15079_fail_b where
+
+import Data.Kind (Type)
+import Data.Void (Void)
+
+infixl 4 :==
+-- | Heterogeneous Leibnizian equality.
+newtype (a :: j) :== (b :: k)
+  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
+
+newtype Coerce a = Coerce { uncoerce :: Starify a }
+
+type Starify :: k -> Type
+type family Starify (a :: k) :: Type where
+  Starify (a :: Type) = a
+  Starify _           = Void
+
+coerce :: a :== b -> a -> b
+coerce f = uncoerce . hsubst f . Coerce
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr b/testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr
new file mode 100644
index 0000000000..f99f557725
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr
@@ -0,0 +1,11 @@
+
+T15079_fail_b.hs:21:23: error: [GHC-11809]
+    • Couldn't match type ‘c0’ with ‘Coerce’
+      Expected: c0 a -> Coerce b
+        Actual: c0 a -> c0 b
+      Visibility of forall-bound variables in kinds differs
+        c0 :: forall i. i -> *
+        Coerce :: forall {k}. k -> *
+    • In the first argument of ‘(.)’, namely ‘hsubst f’
+      In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
+      In the expression: uncoerce . hsubst f . Coerce
diff --git a/testsuite/tests/typecheck/should_fail/T22648a.hs b/testsuite/tests/typecheck/should_fail/T22648a.hs
new file mode 100644
index 0000000000..72ac0b14af
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648a.hs
@@ -0,0 +1,7 @@
+module T22648a where
+
+const_inf :: () -> forall {a} {b}. a -> b -> a
+const_inf _ x _ = x
+
+const_spec :: () -> forall a b. a -> b -> a
+const_spec = const_inf
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/T22648a.stderr b/testsuite/tests/typecheck/should_fail/T22648a.stderr
new file mode 100644
index 0000000000..3f8eb41adc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648a.stderr
@@ -0,0 +1,7 @@
+
+T22648a.hs:7:14: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: () -> forall a b. a -> b -> a
+          Actual: () -> forall {a} {b}. a -> b -> a
+    • In the expression: const_inf
+      In an equation for ‘const_spec’: const_spec = const_inf
diff --git a/testsuite/tests/typecheck/should_fail/T22648b.hs b/testsuite/tests/typecheck/should_fail/T22648b.hs
new file mode 100644
index 0000000000..5ec28af471
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T22648b where
+
+import Data.Kind (Type)
+
+type D1 :: forall {k1} {k2}. k1 -> k2 -> Type
+data D1 a b
+
+type family F :: forall k1 k2. k1 -> k2 -> Type
+type instance F = D1
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/T22648b.stderr b/testsuite/tests/typecheck/should_fail/T22648b.stderr
new file mode 100644
index 0000000000..50d9c95c37
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648b.stderr
@@ -0,0 +1,7 @@
+
+T22648b.hs:11:19: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: forall k1 k2. k1 -> k2 -> *
+          Actual: forall {k1} {k2}. k1 -> k2 -> *
+    • In the type ‘D1’
+      In the type instance declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/T22648c.hs b/testsuite/tests/typecheck/should_fail/T22648c.hs
new file mode 100644
index 0000000000..e81d97da0e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648c.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds #-}
+
+module T22648c where
+
+import GHC.TypeLits (Nat)
+import Data.Kind (Type)
+
+-- 1. the (i :: Nat) parameter to avoid conflicting instances
+-- 2. the (Type ->) parameter is to prevent instantiation of invisible variables
+
+type family Infer (i :: Nat) :: Type -> forall {a}. a
+type family Invis (i :: Nat) :: Type -> forall a. a
+type family Vis   (i :: Nat) :: Type -> forall a -> a
+
+type instance Vis 1 = Invis 0 -- Bad
+type instance Invis 2 = Vis 0 -- Bad
+
+type instance Vis 3 = Infer 0 -- Bad
+type instance Infer 4 = Vis 0 -- Bad
+
+type instance Invis 5 = Infer 0 -- Bad
+type instance Infer 6 = Invis 0 -- Ok
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/T22648c.stderr b/testsuite/tests/typecheck/should_fail/T22648c.stderr
new file mode 100644
index 0000000000..cb92ed89f0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648c.stderr
@@ -0,0 +1,35 @@
+
+T22648c.hs:17:23: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: * -> forall a -> a
+          Actual: * -> forall a. a
+    • In the type ‘Invis 0’
+      In the type instance declaration for ‘Vis’
+
+T22648c.hs:18:25: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: * -> forall a. a
+          Actual: * -> forall a -> a
+    • In the type ‘Vis 0’
+      In the type instance declaration for ‘Invis’
+
+T22648c.hs:20:23: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: * -> forall a -> a
+          Actual: * -> forall {a}. a
+    • In the type ‘Infer 0’
+      In the type instance declaration for ‘Vis’
+
+T22648c.hs:21:25: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: * -> forall {a}. a
+          Actual: * -> forall a -> a
+    • In the type ‘Vis 0’
+      In the type instance declaration for ‘Infer’
+
+T22648c.hs:23:25: error: [GHC-25115]
+    • Visibility of forall-bound variables is not compatible
+        Expected: * -> forall a. a
+          Actual: * -> forall {a}. a
+    • In the type ‘Infer 0’
+      In the type instance declaration for ‘Invis’
diff --git a/testsuite/tests/typecheck/should_fail/T22648v.hs b/testsuite/tests/typecheck/should_fail/T22648v.hs
new file mode 100644
index 0000000000..1de83211f7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648v.hs
@@ -0,0 +1,18 @@
+module T22648v 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/T22648v.stderr b/testsuite/tests/typecheck/should_fail/T22648v.stderr
new file mode 100644
index 0000000000..7ff1f6ed25
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648v.stderr
@@ -0,0 +1,26 @@
+
+T22648v.hs:12:16: error: [GHC-25115]
+    • Visibility of forall-bound variables is 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
+
+T22648v.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
+
+T22648v.hs:18:15: error: [GHC-11809]
+    • Couldn't match type ‘hk0’ with ‘V’
+      Expected: hk0 a0
+        Actual: V k1 a0
+      Visibility of forall-bound variables in kinds differs
+        hk0 :: forall j. j -> *
+        V :: 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/T22648v_ql.hs b/testsuite/tests/typecheck/should_fail/T22648v_ql.hs
new file mode 100644
index 0000000000..3e3107f92c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648v_ql.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module T22648v_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/T22648v_ql.stderr b/testsuite/tests/typecheck/should_fail/T22648v_ql.stderr
new file mode 100644
index 0000000000..1283f0107b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22648v_ql.stderr
@@ -0,0 +1,23 @@
+
+T22648v_ql.hs:14:16: error: [GHC-25115]
+    • Visibility of forall-bound variables is 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
+
+T22648v_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
+
+T22648v_ql.hs:20:15: error: [GHC-25115]
+    • Visibility of forall-bound variables is 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/all.T b/testsuite/tests/typecheck/should_fail/all.T
index a7e9f6a678..cd2758ad17 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -667,3 +667,10 @@ test('T22570', normal, compile_fail, [''])
 test('T22645', normal, compile_fail, [''])
 test('T20666', normal, compile_fail, [''])
 test('T20666a', normal, compile_fail, [''])
+test('T22648a', normal, compile_fail, [''])
+test('T22648b', normal, compile_fail, [''])
+test('T22648c', normal, compile_fail, [''])
+test('T22648v', normal, compile_fail, [''])
+test('T22648v_ql', normal, compile_fail, [''])
+test('T15079_fail_a', normal, compile_fail, [''])
+test('T15079_fail_b', normal, compile_fail, [''])