[Git][ghc/ghc][wip/int-index/visibility-check] Ignore forall visibility in eqType (#22762)
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Mon Feb 6 00:12:42 UTC 2023
Vladislav Zavialov pushed to branch wip/int-index/visibility-check at Glasgow Haskell Compiler / GHC
Commits:
87058d73 by Vladislav Zavialov at 2023-02-06T03:12:18+03:00
Ignore forall visibility in eqType (#22762)
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 new ad-hoc checks:
checkEqForallVis (in checking mode)
cteForallKindVisDiff (in inference mode)
- - - - -
24 changed files:
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/Error/Codes.hs
- testsuite/tests/saks/should_fail/T18863a.stderr
- + testsuite/tests/typecheck/should_compile/T22762.hs
- testsuite/tests/typecheck/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/VisFlag1.hs
- + testsuite/tests/typecheck/should_fail/VisFlag1.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag1_ql.hs
- + testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag2.hs
- + testsuite/tests/typecheck/should_fail/VisFlag2.stderr
- + testsuite/tests/typecheck/should_fail/VisFlag3.hs
- + testsuite/tests/typecheck/should_fail/VisFlag3.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
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
=====================================
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,39 @@ 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`?
+
+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 *outside* the equality relation. To that end,
+there are two ad-hoc checks:
+ * checkEqForallVis (in checking mode)
+ * cteForallKindVisDiff (in inference mode)
+
+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,12 +295,7 @@ 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:
+For now, we decide to ignore specificity. That is, we have the following:
--------------------------------------------------
| Type 1 | Type 2 | Equal? |
@@ -303,11 +313,9 @@ That is, we have the following:
| | 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.
+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 +343,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 +521,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]
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -1673,6 +1673,16 @@ 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
+ = let reason = ForallKindVisDiff tv1 ty2
+ main_msg =
+ CannotUnifyVariable
+ { mismatchMsg = headline_msg
+ , cannotUnifyReason = reason }
+ in 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)
=====================================
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 "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 $
@@ -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 "Visibilities of forall-bound variables in kinds differ") 2 $
+ vcat [ ppr tv1 <+> text "::" <+> ppr (tyVarKind tv1)
+ , ppr ty2 <+> text "::" <+> ppr (typeKind ty2) ]
pprMismatchMsg :: SolverReportErrCtxt -> MismatchMsg -> SDoc
pprMismatchMsg ctxt
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -2924,6 +2924,22 @@ 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 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
+ -}
+ TcRnIncompatibleForallVisibility
+ :: TcType
+ -> TcType
+ -> TcRnMessage
+
deriving Generic
-- | Things forbidden in @type data@ declarations.
@@ -3787,6 +3803,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 differences in visibility between 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: VisFlag1
+ | ForallKindVisDiff TyVar Type
deriving Generic
-- | Report a mismatch error without any extra
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -361,7 +361,8 @@ tcApp rn_expr exp_res_ty
-- app_res_rho and exp_res_ty are both rho-types,
-- 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
+ do { checkEqForallVis app_res_rho exp_res_ty
+ ; co <- unifyExpectedType rn_expr 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
+ ; checkEqForallVis app_res_rho exp_res_ty
; tcSubTypeDS rn_expr app_res_rho exp_res_ty }
-- Typecheck the value arguments
@@ -1050,9 +1052,9 @@ qlUnify delta ty1 ty2
-- Passes the occurs check
= do { let ty2_kind = typeKind ty2
kappa_kind = tyVarKind kappa
+ ; checkEqForallVis ty2_kind (Check kappa_kind)
; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
-- unifyKind: see Note [Actual unification in qlUnify]
-
; traceTc "qlUnify:update" $
vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
=====================================
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
+ ; checkEqForallVis 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
+ ; checkEqForallVis 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
@@ -3284,6 +3286,7 @@ bindExplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_ki
| check_parent
, Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
= do { kind <- tc_lhs_kind_sig tc_ki_mode (TyVarBndrKindCtxt name) lhs_kind
+ ; checkEqForallVis kind (Check (tyVarKind tv))
; discardResult $
unifyKind (Just . NameThing $ name) kind (tyVarKind tv)
-- This unify rejects:
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1095,9 +1095,9 @@ 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 _ _) _
+ -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare
= can_eq_nc_forall ev eq_rel s1 s2
-- See Note [Canonicalising type applications] about why we require rewritten types
=====================================
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 ]
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -66,6 +66,10 @@ module GHC.Tc.Utils.TcMType (
checkingExpType_maybe, checkingExpType,
inferResultToType, ensureMonoType, promoteTcType,
+ --------------------------------
+ -- Visibility flag check
+ tcEqForallVis, checkEqForallVis,
+
--------------------------------
-- Zonking and tidying
zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
@@ -604,6 +608,108 @@ tc_infer mb_frr tc_check
; res_ty <- readExpType res_ty
; return (result, res_ty) }
+{- *********************************************************************
+* *
+ 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]
+checkEqForallVis :: TcType -> ExpType -> TcM ()
+checkEqForallVis _ (Infer _) = return ()
+checkEqForallVis ty1 (Check 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
+
+-- 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 -- ex falso shortcut
+ | 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 -- ex falso shortcut
+ | 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 -- ex falso shortcut
+
+{- Note [Presumably equal types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In matchUpForAllTyFlags (and by extension tcEqForallVis, checkEqForallVis)
+we want to be checking the logical implication
+ (ty1 = ty2) ⊃ (forall flags satisfy the predicate)
+If the assumption (ty1 = ty2) does not hold, the correct thing to do is to
+return True (ex falso sequitur quodlibet).
+
+However, implementing these semantics precisely would make this function
+more complicated and expensive. For instance, we'd have to maintain a RnEnv2
+to check type variables for equality.
+
+As a pragmatic compromise, we say that the result of matchUpForAllTyFlags is
+not well-defined if (ty1 /= ty2). This should not matter in practice, as
+those functions are only ever used in conjunction with an actual equality check.
+The worst case scenario is that we report a less helpful error message.
+-}
+
{- *********************************************************************
* *
Promoting types
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2636,12 +2636,14 @@ 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.<>
+ go_kind (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)
+
+ go_kind :: TcKind -> TcKind -> CheckTyEqResult
+ go_kind k1 k2
+ | tcEqForallVis k1 k2 = cteOK
+ | otherwise = forall_kind_vis_diff
=====================================
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
=====================================
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’
=====================================
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
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -857,3 +857,4 @@ test('T22647', normal, compile, [''])
test('T19577', normal, compile, [''])
test('T22383', normal, compile, [''])
test('T21501', normal, compile, [''])
+test('T22762', normal, compile, [''])
=====================================
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
=====================================
testsuite/tests/typecheck/should_fail/VisFlag1.stderr
=====================================
@@ -0,0 +1,26 @@
+
+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-11809]
+ • Couldn't match type ‘hk0’ with ‘V’
+ Expected: hk0 a0
+ Actual: V k1 a0
+ Visibilities of forall-bound variables in kinds differ
+ 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
=====================================
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
=====================================
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
=====================================
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
=====================================
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’
=====================================
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)
=====================================
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’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -667,3 +667,7 @@ test('T22570', normal, compile_fail, [''])
test('T22645', normal, compile_fail, [''])
test('T20666', normal, compile_fail, [''])
test('T20666a', normal, compile_fail, [''])
+test('VisFlag1', normal, compile_fail, [''])
+test('VisFlag1_ql', normal, compile_fail, [''])
+test('VisFlag2', normal, compile_fail, [''])
+test('VisFlag3', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/87058d732cde1f178fd3fd5e1d8af378aef3d300
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/87058d732cde1f178fd3fd5e1d8af378aef3d300
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230205/1a3543fe/attachment-0001.html>
More information about the ghc-commits
mailing list