[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 2 commits: Document defaulting of RuntimeReps
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Nov 15 23:13:00 UTC 2023
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
13627867 by Krzysztof Gogolewski at 2023-11-15T18:12:52-05:00
Document defaulting of RuntimeReps
Fixes #24099
- - - - -
c2325536 by Simon Peyton Jones at 2023-11-15T18:12:53-05:00
Second fix to #24083
My earlier fix turns out to be too aggressive for data/type families
See wrinkle (DTV1) in Note [Disconnected type variables]
- - - - -
9 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- docs/users_guide/extending_ghc.rst
- docs/users_guide/exts/data_kinds.rst
- docs/users_guide/exts/linear_types.rst
- docs/users_guide/exts/primitives.rst
- docs/users_guide/exts/representation_polymorphism.rst
- docs/users_guide/using-warnings.rst
- + testsuite/tests/polykinds/T24083a.hs
- testsuite/tests/polykinds/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2569,23 +2569,19 @@ kcCheckDeclHeader_sig sig_kind name flav
-- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
--
-- Also see Note [Arity of type families and type synonyms]
- ; ctx_k <- kc_res_ki
+ ; res_kind :: ContextKind <- kc_res_ki
; let sig_res_kind' = mkTyConKind excess_sig_tcbs sig_res_kind
; traceTc "kcCheckDeclHeader_sig 2" $
vcat [ text "excess_sig_tcbs" <+> ppr excess_sig_tcbs
- , text "ctx_k" <+> ppr ctx_k
+ , text "res_kind" <+> ppr res_kind
, text "sig_res_kind'" <+> ppr sig_res_kind'
]
- -- Unify res_ki (from the type declaration) with the residual kind from
- -- the kind signature. Don't forget to apply the skolemising 'subst' first.
- ; case ctx_k of
- AnyKind -> return () -- No signature
- _ -> do
- res_ki <- newExpectedKind ctx_k
- check_exp_res_ki sig_res_kind' res_ki
+ -- Unify res_ki (from the type declaration) with
+ -- sig_res_kind', the residual kind from the kind signature.
+ ; checkExpectedResKind sig_res_kind' res_kind
-- Add more binders for data/newtype, so the result kind has no arrows
-- See Note [Datatype return kinds]
@@ -2608,7 +2604,7 @@ kcCheckDeclHeader_sig sig_kind name flav
; implicit_tvs <- liftZonkM $ zonkTcTyVarsToTcTyVars implicit_tvs
; let implicit_prs = implicit_nms `zip` implicit_tvs
; checkForDuplicateScopedTyVars implicit_prs
- ; checkForDisconnectedScopedTyVars all_tcbs implicit_prs
+ ; checkForDisconnectedScopedTyVars flav all_tcbs implicit_prs
-- Swizzle the Names so that the TyCon uses the user-declared implicit names
-- E.g type T :: k -> Type
@@ -2650,18 +2646,23 @@ kcCheckDeclHeader_sig sig_kind name flav
-- | Check the result kind annotation on a type constructor against
-- the corresponding section of the standalone kind signature.
-- Drops invisible binders that interfere with unification.
-check_exp_res_ki :: TcKind -- ^ the actual kind
- -> TcKind -- ^ the expected kind
- -> TcM ()
-check_exp_res_ki act_kind exp_kind
- = discardResult $ unifyKind Nothing act_kind' exp_kind
- where
- (_, act_kind') = splitInvisPiTysN n_to_inst act_kind
+checkExpectedResKind :: TcKind -- ^ the result kind from the separate kind signature
+ -> ContextKind -- ^ the result kind from the declaration header
+ -> TcM ()
+checkExpectedResKind _ AnyKind
+ = return () -- No signature in the declaration header
+checkExpectedResKind sig_kind res_ki
+ = do { actual_res_ki <- newExpectedKind res_ki
- -- by analogy with checkExpectedKind
- n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
- n_act_invis_bndrs = invisibleTyBndrCount act_kind
- n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
+ ; let -- Drop invisible binders from sig_kind until they match up
+ -- with res_ki. By analogy with checkExpectedKind.
+ n_res_invis_bndrs = invisibleTyBndrCount actual_res_ki
+ n_sig_invis_bndrs = invisibleTyBndrCount sig_kind
+ n_to_inst = n_sig_invis_bndrs - n_res_invis_bndrs
+
+ (_, sig_kind') = splitInvisPiTysN n_to_inst sig_kind
+
+ ; discardResult $ unifyKind Nothing sig_kind' actual_res_ki }
matchUpSigWithDecl
:: Name -- Name of the type constructor for error messages
@@ -2964,13 +2965,16 @@ expectedKindInCtxt _ = OpenKind
* *
********************************************************************* -}
-checkForDisconnectedScopedTyVars :: [TcTyConBinder] -> [(Name,TcTyVar)] -> TcM ()
+checkForDisconnectedScopedTyVars :: TyConFlavour TyCon -> [TcTyConBinder]
+ -> [(Name,TcTyVar)] -> TcM ()
-- See Note [Disconnected type variables]
-- `scoped_prs` is the mapping gotten by unifying
-- - the standalone kind signature for T, with
-- - the header of the type/class declaration for T
-checkForDisconnectedScopedTyVars sig_tcbs scoped_prs
- = mapM_ report_disconnected (filterOut ok scoped_prs)
+checkForDisconnectedScopedTyVars flav sig_tcbs scoped_prs
+ = when (needsEtaExpansion flav) $
+ -- needsEtaExpansion: see wrinkle (DTV1) in Note [Disconnected type variables]
+ mapM_ report_disconnected (filterOut ok scoped_prs)
where
sig_tvs = mkVarSet (binderVars sig_tcbs)
ok (_, tc_tv) = tc_tv `elemVarSet` sig_tvs
@@ -3047,6 +3051,25 @@ phantom synonym that just discards its argument. So our plan is this:
See #24083 for dicussion of alternatives, none satisfactory. Also the fix is
easy: just add an explicit `@kk` parameter to the declaration, to bind `kk`
explicitly, rather than binding it implicitly via unification.
+
+(DTV1) We only want to make this check when there /are/ scoped type variables; and
+ that is determined by needsEtaExpansion. Examples:
+
+ type C :: x -> y -> Constraint
+ class C a :: b -> Constraint where { ... }
+ -- The a,b scope over the "..."
+
+ type D :: forall k. k -> Type
+ data family D :: kk -> Type
+ -- Nothing for `kk` to scope over!
+
+ In the latter data-family case, the match-up stuff in kcCheckDeclHeader_sig will
+ return [] for `extra_tcbs`, and in fact `all_tcbs` will be empty. So if we do
+ the check-for-disconnected-tyvars check we'll complain that `kk` is not bound
+ to one of `all_tcbs` (see #24083, comments about the `singletons` package).
+
+ The scoped-tyvar stuff is needed precisely for data/class/newtype declarations,
+ where needsEtaExpansion is True.
-}
{- *********************************************************************
=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -1383,6 +1383,7 @@ The plugin has type ``WantedConstraints -> [DefaultingProposal]``.
* It is given the currently unsolved constraints.
* It returns a list of independent "defaulting proposals".
* Each proposal of type ``DefaultingProposal`` specifies:
+
* ``deProposals``: specifies a list,
in priority order, of sets of type variable assignments
* ``deProposalCts :: [Ct]`` gives a set of constraints (always a
=====================================
docs/users_guide/exts/data_kinds.rst
=====================================
@@ -100,13 +100,13 @@ The following kinds and promoted data constructors can be used even when
:extension:`DataKinds` is not enabled:
- ``Type``
-- ``TYPE`` (see :ref:`_runtime-rep`)
+- ``TYPE`` (see :ref:`runtime-rep`)
- ``Constraint`` (see :ref:`constraint-kind`)
- ``CONSTRAINT``
- ``Multiplicity`` and its promoted data constructors (see :extension:`LinearTypes`)
-- ``LiftedRep`` (see :ref:`_runtime-rep`)
-- ``RuntimeRep`` and its promoted data constructors (see :ref:`_runtime-rep`)
-- ``Levity`` and its promoted data constructors (see :ref:`_runtime-rep`)
+- ``LiftedRep`` (see :ref:`runtime-rep`)
+- ``RuntimeRep`` and its promoted data constructors (see :ref:`runtime-rep`)
+- ``Levity`` and its promoted data constructors (see :ref:`runtime-rep`)
- ``VecCount`` and its promoted data constructors
- ``VecElem`` and its promoted data constructors
@@ -231,7 +231,7 @@ See also :ghc-ticket:`7347`.
:extension:`DataKinds` and type synonyms
----------------------------------------
-The :extensions:`DataKinds` extension interacts with type synonyms in the
+The :extension:`DataKinds` extension interacts with type synonyms in the
following ways:
1. In a *type* context: :extension:`DataKinds` is not required to use a type
=====================================
docs/users_guide/exts/linear_types.rst
=====================================
@@ -1,3 +1,5 @@
+.. _linear-types:
+
Linear types
============
@@ -58,7 +60,8 @@ partially. See, however :ref:`linear-types-limitations`.
Linear and multiplicity-polymorphic arrows are *always declared*,
never inferred. That is, if you don't give an appropriate type
signature to a function, it will be inferred as being a regular
-function of type ``a -> b``.
+function of type ``a -> b``. The same principle holds for
+representation polymorphism (see :ref:`representation-polymorphism-defaulting`).
Data types
----------
=====================================
docs/users_guide/exts/primitives.rst
=====================================
@@ -438,7 +438,7 @@ You may even declare levity-polymorphic data types: ::
While ``f`` above could reasonably be levity-polymorphic (as it evaluates its
argument either way), GHC currently disallows the more general type
``PEither @l Int Bool -> Bool``. This is a consequence of the
-`representation-polymorphic binder restriction <#representation-polymorphism-restrictions>`__,
+`representation-polymorphic binder restriction <#representation-polymorphism-restrictions>`__.
Pattern matching against an unlifted data type work just like that for lifted
types; but see :ref:`recursive-and-polymorphic-let-bindings` for the semantics of
=====================================
docs/users_guide/exts/representation_polymorphism.rst
=====================================
@@ -108,6 +108,35 @@ These functions do not bind a representation-polymorphic variable, and
so are accepted. Their polymorphism allows users to use these to conveniently
stub out functions that return unboxed types.
+.. _representation-polymorphism-defaulting:
+
+Inference and defaulting
+------------------------
+
+GHC does not infer representation-polymorphic types.
+If the representation of a variable is not specified, it will be assumed
+to be ``LiftedRep``.
+For example, if you write ``f a b = a b``, the inferred type of ``f``
+will be ::
+
+ f :: forall {a :: Type} {b :: Type}. (a -> b) -> a -> b
+
+even though ::
+
+ f :: forall {rep} {a :: Type} {b :: TYPE rep}. (a -> b) -> a -> b
+
+would also be legal, as described above.
+
+Likewise, in a user-written signature ``f :: forall a b. (a -> b) -> a -> b``
+GHC will assume that both ``a`` and ``b`` have kind ``Type``. To use
+a different representation, you have to specify the kinds of ``a`` and ``b``.
+
+During type inference, GHC does not quantify over variables of kind
+``RuntimeRep`` nor ``Levity``.
+Instead, they are defaulted to ``LiftedRep`` and ``Lifted`` respectively.
+Likewise, ``Multiplicity`` variables (:ref:`linear-types`) are defaulted
+to ``Many``.
+
.. _printing-representation-polymorphic-types:
Printing representation-polymorphic types
=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -2574,7 +2574,7 @@ of ``-W(no-)*``.
Introduced in GHC 9.10.1, this warns when an illegal use of a type or kind
(without having enabled the :extension:`DataKinds` extension) is caught in
the typechecker (hence the ``-tc`` suffix). These warnings complement the
- existing :extensions:`DataKinds` checks (that have existed since
+ existing :extension:`DataKinds` checks (that have existed since
:extension:`DataKinds` was first introduced), which result in errors
instead of warnings.
=====================================
testsuite/tests/polykinds/T24083a.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}
+
+module T24083a where
+
+type TyCon :: (k1 -> k2) -> unmatchable_fun
+data family TyCon :: (k1 -> k2) -> unmatchable_fun
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -244,3 +244,4 @@ test('T22743', normal, compile_fail, [''])
test('T22742', normal, compile_fail, [''])
test('T22793', normal, compile_fail, [''])
test('T24083', normal, compile_fail, [''])
+test('T24083a', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a6b446e81d42bc83689d25d512221679f7aa6d3a...c2325536a245eece7c96fc615a20523127c12047
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a6b446e81d42bc83689d25d512221679f7aa6d3a...c2325536a245eece7c96fc615a20523127c12047
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/20231115/0bf5fc3c/attachment-0001.html>
More information about the ghc-commits
mailing list