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

9 files changed, 160 insertions, 7 deletions

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