[Git][ghc/ghc][wip/int-index/decl-invis-binders] Bye bye kind inference
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Fri Jan 27 17:48:10 UTC 2023
Vladislav Zavialov pushed to branch wip/int-index/decl-invis-binders at Glasgow Haskell Compiler / GHC
Commits:
2865bcef by Vladislav Zavialov at 2023-01-27T20:47:31+03:00
Bye bye kind inference
- - - - -
21 changed files:
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Types/Error/Codes.hs
- compiler/GHC/Types/Hint.hs
- compiler/GHC/Types/Hint/Ppr.hs
- compiler/GHC/Types/Var.hs
- docs/users_guide/9.8.1-notes.rst
- docs/users_guide/exts/type_abstractions.rst
- testsuite/tests/typecheck/should_compile/T22560d.hs
- testsuite/tests/typecheck/should_compile/T22560d.stdout
- testsuite/tests/typecheck/should_fail/T22560_fail_a.stderr
- testsuite/tests/typecheck/should_fail/T22560_fail_b.stderr
- testsuite/tests/typecheck/should_fail/T22560_fail_c.hs
- testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr
- + testsuite/tests/typecheck/should_fail/T22560_fail_d.hs
- + testsuite/tests/typecheck/should_fail/T22560_fail_d.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -24,7 +24,6 @@ module GHC.Core.TyCon(
mkNamedTyConBinder, mkNamedTyConBinders,
mkRequiredTyConBinder,
mkAnonTyConBinder, mkAnonTyConBinders,
- anonToRequiredTcb,
tyConBinderForAllTyFlag, tyConBndrVisForAllTyFlag, isNamedTyConBinder,
isVisibleTyConBinder, isInvisibleTyConBinder,
isVisibleTcbVis, isInvisSpecTcbVis,
@@ -488,13 +487,6 @@ mkRequiredTyConBinder dep_set tv
| tv `elemVarSet` dep_set = mkNamedTyConBinder Required tv
| otherwise = mkAnonTyConBinder tv
--- | Turn AnonTCB into a NamedTCB if the tv is mentioned in the dependent set
-anonToRequiredTcb :: TyCoVarSet -- variables that are used dependently
- -> TyConBinder
- -> TyConBinder
-anonToRequiredTcb dep_set (Bndr tv AnonTCB) = mkRequiredTyConBinder dep_set tv
-anonToRequiredTcb _ bndr = bndr
-
tyConBinderForAllTyFlag :: TyConBinder -> ForAllTyFlag
tyConBinderForAllTyFlag (Bndr _ vis) = tyConBndrVisForAllTyFlag vis
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1244,12 +1244,20 @@ instance Diagnostic TcRnMessage where
hang (text "Illegal invisible type variable binder:")
2 (ppr bndr)
- TcRnInvalidInvisTyVarBndr hs_bndr ->
+ TcRnInvalidInvisTyVarBndr name hs_bndr ->
mkSimpleDecorated $
vcat [ text "Invalid invisible type variable binder:"
, nest 2 (ppr hs_bndr)
- , text "There is no matching forall-bound variable" <+>
- text "in the standalone kind signature." ]
+ , text "There is no matching forall-bound variable"
+ , text "in the standalone kind signature for" <+> quotes (ppr name) <> dot ]
+
+ TcRnInvisBndrWithoutSig _ hs_bndr ->
+ mkSimpleDecorated $
+ vcat [ text "Invalid invisible type variable binder:"
+ , nest 2 (ppr hs_bndr)
+ , text "Either a standalone kind signature (SAKS)"
+ , nest 2 (text "or a complete user-supplied kind (CUSK)")
+ , text "is required to use invisible binders." ]
diagnosticReason = \case
TcRnUnknownMessage m
@@ -1662,6 +1670,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnInvalidInvisTyVarBndr{}
-> ErrorWithoutFlag
+ TcRnInvisBndrWithoutSig{}
+ -> ErrorWithoutFlag
diagnosticHints = \case
TcRnUnknownMessage m
@@ -2079,6 +2089,8 @@ instance Diagnostic TcRnMessage where
-> [suggestExtension LangExt.TypeAbstractions]
TcRnInvalidInvisTyVarBndr{}
-> noHints
+ TcRnInvisBndrWithoutSig name _
+ -> [SuggestAddStandaloneKindSignature name]
diagnosticCode = constructorCode
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -2796,10 +2796,25 @@ data TcRnMessage where
type P :: forall a -> Type
data P @a = MkP
- Test case: T22560_fail_a T22560_fail_b
+ Test cases: T22560_fail_a T22560_fail_b
-}
TcRnInvalidInvisTyVarBndr
- :: !(LHsTyVarBndr (HsBndrVis GhcRn) GhcRn)
+ :: !Name
+ -> !(LHsTyVarBndr (HsBndrVis GhcRn) GhcRn)
+ -> TcRnMessage
+
+ {-| 'TcRnInvisBndrWithoutSig' is an error triggered by attempting to use
+ an invisible type variable binder in without a standalone kind signature
+ or a complete user-specified kind.
+
+ Example:
+ data T @k (a :: k) -- No CUSK, no SAKS
+
+ Test case: T22560_fail_d
+ -}
+ TcRnInvisBndrWithoutSig
+ :: !Name
+ -> !(LHsTyVarBndr (HsBndrVis GhcRn) GhcRn)
-> TcRnMessage
deriving Generic
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2437,6 +2437,15 @@ kcCheckDeclHeader_cusk name flav
ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
| otherwise = AnyKind
+-- | Create a TyConBinder for a user-written type variable binder.
+mkExplicitTyConBinder :: TyCoVarSet -- variables that are used dependently
+ -> VarBndr TyVar (HsBndrVis GhcRn)
+ -> TyConBinder
+mkExplicitTyConBinder dep_set (Bndr tv flag) =
+ case flag of
+ HsBndrRequired -> mkRequiredTyConBinder dep_set tv
+ HsBndrInvisible{} -> mkNamedTyConBinder Specified tv
+
-- | Kind-check a 'LHsQTyVars'. Used in 'inferInitialKind' (for tycon kinds and
-- other kinds).
--
@@ -2449,15 +2458,16 @@ kcInferDeclHeader
-> TcM MonoTcTyCon -- ^ A suitably-kinded non-generalized TcTyCon
kcInferDeclHeader name flav
(HsQTvs { hsq_ext = kv_ns
- , hsq_explicit = hs_tvs }) kc_res_ki
+ , hsq_explicit = hs_bndrs }) kc_res_ki
-- No standalone kind signature and no CUSK.
-- See Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
= addTyConFlavCtxt name flav $
- do { (scoped_kvs, (tc_bndrs, res_kind))
+ do { rejectInvisibleBinders name hs_bndrs
+ ; (scoped_kvs, (tc_bndrs, res_kind))
-- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
-- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
- <- bindImplicitTKBndrs_Q_Tv kv_ns $
- bindExplicitTKBndrs_Q_Tv ctxt_kind hs_tvs $
+ <- bindImplicitTKBndrs_Q_Tv kv_ns $
+ bindExplicitTKBndrs_Q_Tv ctxt_kind hs_bndrs $
newExpectedKind =<< kc_res_ki
-- Why "_Tv" not "_Skol"? See third wrinkle in
-- Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
@@ -2467,14 +2477,18 @@ kcInferDeclHeader name flav
-- recursive group.
-- See Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
- dep_set = emptyVarSet -- See Note [Empty dep_set in kcInferDeclHeader]
+ tc_tvs = binderVars tc_bndrs
+ -- Discard visibility flags. We made sure all of them are HsBndrRequired
+ -- by the call to rejectInvisibleBinders above.
- tc_binders = map (mkExplicitTyConBinder dep_set) tc_bndrs
+ tc_binders = mkAnonTyConBinders tc_tvs
-- Also, note that tc_binders has the tyvars from only the
-- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
-- in GHC.Tc.TyCl
+ --
+ -- mkAnonTyConBinder: see Note [No polymorphic recursion]
- all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ binderVars tc_bndrs)
+ all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
-- NB: bindExplicitTKBndrs_Q_Tv does not clone;
-- ditto Implicit
-- See Note [Cloning for type variable binders]
@@ -2484,82 +2498,21 @@ kcInferDeclHeader name flav
flav
; traceTc "kcInferDeclHeader: not-cusk" $
- vcat [ ppr name, ppr kv_ns, ppr hs_tvs
+ vcat [ ppr name, ppr kv_ns, ppr hs_bndrs
, ppr scoped_kvs
- , ppr (binderVars tc_bndrs)
- , ppr (mkTyConKind tc_binders res_kind) ]
+ , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
; return tycon }
where
ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
| otherwise = AnyKind
-{- Note [Empty dep_set in kcInferDeclHeader]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The dep_set determines the choice between
- 1. non-dependent quantification (AnonTCB):
- k -> r
- 2. dependent quantification (NamedTCB Required):
- forall (a::k) -> r
-
-We want dependent quantification if the variable 'a' is mentioned in 'r'.
-This is checked in mkRequiredTyConBinder.
-
-* In kcCheckDeclHeader_cusk we compute the dep_set using candidateQTyVarsOfKinds.
-* In kcInferDeclHeader we can't do that because this set can be affected when
- metavariables are filled in during kind inference.
-
-By using emptyVarSet, we end up with AnonTCB even for dependent variables.
-But no worries: we can compute the dep_set later, in generaliseTcTyCon,
-and use anonToRequiredTcb to change AnonTCB to NamedTCB Required.
-
-Consider:
- data T (k :: Type) (a :: k) @(j :: Type) (b :: j)
-
-1. kcInferDeclHeader returns a MonoTcTyCon with the following tyConBinders:
- AnonTCB k[tyv:1] :: Type
- AnonTCB a[tyv:1] :: k[tyv:1]
- NamedTCB Specified j[tyv:1] :: Type
- AnonTCB b[tyv:1] :: j[tyv:1]
- The invisible binder is NamedTCB from the get go, but the visible binder
- starts out as AnonTCB.
-
-2. generaliseTcTyCon skolemises the variables and computes the dep_set:
- req_tvs = k[sk:1] :: Type
- a[sk:1] :: k[sk:1]
- j[sk:1] :: Type
- b[sk:1] :: j[sk:1]
- dep_set = { k[sk:1], j[sk:1] }
-
-3. generaliseTcTyCon transfers the binder flags (ForAllTyFlag) from tyConBinders
- to the skolemised variables, relying on the 1-1 correspondence
- between tyConBinders and req_tvs:
- AnonTCB k[sk:1] :: Type
- AnonTCB a[sk:1] :: k[sk:1]
- NamedTCB Specified j[sk:1] :: Type
- AnonTCB b[sk:1] :: j[sk:1]
-
-4. generaliseTcTyCon changes AnonTCB to NamedTCB Required for dependent binders
- (i.e. binders whose bound variable is in the dep_set):
- NamedTCB Required k[sk:1] :: Type
- AnonTCB a[sk:1] :: k[sk:1]
- NamedTCB Specified j[sk:1] :: Type
- AnonTCB b[sk:1] :: j[sk:1]
- That is:
- * The dependent variable 'k' was updated from AnonTCB to NamedTCB Required.
- * The dependent variable 'j' was left intact because it is already NamedTCB Specified.
- * The non-dependent variables 'a' and 'b' were left intact.
-
-See also: Note [No polymorphic recursion]
--}
-
--- | Create a TyConBinder for a user-written type variable binder.
-mkExplicitTyConBinder :: TyCoVarSet -- variables that are used dependently
- -> VarBndr TyVar (HsBndrVis GhcRn)
- -> TyConBinder
-mkExplicitTyConBinder dep_set (Bndr tv flag) =
- case flag of
- HsBndrRequired -> mkRequiredTyConBinder dep_set tv
- HsBndrInvisible{} -> mkNamedTyConBinder Specified tv
+rejectInvisibleBinders :: Name -> [LHsTyVarBndr (HsBndrVis GhcRn) GhcRn] -> TcM ()
+rejectInvisibleBinders name = mapM_ check_bndr_vis
+ where
+ check_bndr_vis :: LHsTyVarBndr (HsBndrVis GhcRn) GhcRn -> TcM ()
+ check_bndr_vis bndr =
+ when (isHsBndrInvisible (hsTyVarBndrFlag (unLoc bndr))) $
+ addErr (TcRnInvisBndrWithoutSig name bndr)
-- | Kind-check a declaration header against a standalone kind signature.
-- See Note [kcCheckDeclHeader_sig]
@@ -2590,7 +2543,7 @@ kcCheckDeclHeader_sig sig_kind name flav
; (tclvl, wanted, (implicit_tvs, (skol_tcbs, (extra_tcbs, tycon_res_kind))))
<- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_sig" $ -- #16687
bindImplicitTKBndrs_Q_Tv implicit_nms $ -- Q means don't clone
- matchUpSigWithDecl sig_tcbs sig_res_kind hs_tv_bndrs $ \ excess_sig_tcbs sig_res_kind ->
+ matchUpSigWithDecl name sig_tcbs sig_res_kind hs_tv_bndrs $ \ excess_sig_tcbs sig_res_kind ->
do { -- Kind-check the result kind annotation, if present:
-- data T a b :: res_ki where ...
-- ^^^^^^^^^
@@ -2681,7 +2634,8 @@ kcCheckDeclHeader_sig sig_kind name flav
; return tc }
matchUpSigWithDecl
- :: [TcTyConBinder] -- TcTyConBinders (with skolem TcTyVars) from the separate kind signature
+ :: Name -- Name of the type constructor for error messages
+ -> [TcTyConBinder] -- TcTyConBinders (with skolem TcTyVars) from the separate kind signature
-> TcKind -- The tail end of the kind signature
-> [LHsTyVarBndr (HsBndrVis GhcRn) GhcRn] -- User-written binders in decl
-> ([TcTyConBinder] -> TcKind -> TcM a) -- All user-written binders are in scope
@@ -2691,7 +2645,7 @@ matchUpSigWithDecl
-- See Note [Matching a kind signature with a declaration]
-- Invariant: Length of returned TyConBinders + length of excess TyConBinders
-- = length of incoming TyConBinders
-matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside
+matchUpSigWithDecl name sig_tcbs sig_res_kind hs_bndrs thing_inside
= go emptySubst sig_tcbs hs_bndrs
where
go subst tcbs []
@@ -2730,7 +2684,7 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside
-- * the quantifier (tcb) is visible: (ty -> ...), (forall a -> ...)
-- * the binder (hs_bndr) is invisible: @t, @(t :: k)
-- Any other combination should have been handled by the zippable/skippable clauses.
- failWithTc (TcRnInvalidInvisTyVarBndr hs_bndr)
+ failWithTc (TcRnInvalidInvisTyVarBndr name hs_bndr)
tc_hs_bndr :: HsTyVarBndr (HsBndrVis GhcRn) GhcRn -> TcKind -> TcM ()
tc_hs_bndr (UserTyVar _ _ _) _
=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -2256,8 +2256,9 @@ reifyDataCon isGadtDataCon tys dc
subst_tv_binders subst tv_bndrs =
let tvs = binderVars tv_bndrs
+ flags = binderFlags tv_bndrs
(subst', tvs') = substTyVarBndrs subst tvs
- tv_bndrs' = setBndrVars "subst_tv_binders" tvs' tv_bndrs
+ tv_bndrs' = map (\(tv,fl) -> Bndr tv fl) (zip tvs' flags)
in (subst', tv_bndrs')
{-
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -929,14 +929,12 @@ generaliseTcTyCon (tc, skol_info, scoped_prs, tc_res_kind)
; let dep_fv_set = candidateKindVars dvs1
inferred_tcbs = mkNamedTyConBinders Inferred inferred
specified_tcbs = mkNamedTyConBinders Specified sorted_spec_tvs
- explicit_tcbs =
- map (anonToRequiredTcb dep_fv_set) $ -- See Note [Empty dep_set in kcInferDeclHeader] in GHC.Tc.Gen.HsType
- setBndrVars "explicit_tcbs" req_tvs (tyConBinders tc)
+ required_tcbs = map (mkRequiredTyConBinder dep_fv_set) req_tvs
-- Step 5: Assemble the final list.
all_tcbs = concat [ inferred_tcbs
, specified_tcbs
- , explicit_tcbs ]
+ , required_tcbs ]
flav = tyConFlavour tc
-- Eta expand
@@ -956,7 +954,7 @@ generaliseTcTyCon (tc, skol_info, scoped_prs, tc_res_kind)
, text "dep_fv_set =" <+> ppr dep_fv_set
, text "inferred_tcbs =" <+> ppr inferred_tcbs
, text "specified_tcbs =" <+> ppr specified_tcbs
- , text "explicit_tcbs =" <+> ppr explicit_tcbs
+ , text "required_tcbs =" <+> ppr required_tcbs
, text "final_tcbs =" <+> ppr final_tcbs ]
-- Step 7: Check for validity.
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -503,6 +503,7 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnCapturedTermName" = 54201
GhcDiagnosticCode "TcRnIllegalInvisTyVarBndr" = 58589
GhcDiagnosticCode "TcRnInvalidInvisTyVarBndr" = 57916
+ GhcDiagnosticCode "TcRnInvisBndrWithoutSig" = 92337
-- IllegalNewtypeReason
GhcDiagnosticCode "DoesNotHaveSingleField" = 23517
=====================================
compiler/GHC/Types/Hint.hs
=====================================
@@ -318,6 +318,14 @@ data GhcHint
-}
| SuggestAddStandaloneDerivation
+ {-| Suggests to add a standalone kind signature when GHC
+ can't perform kind inference.
+
+ Triggered by: 'GHC.Tc.Errors.Types.TcRnInvisBndrWithoutSig'
+ Test case(s): typecheck/should_fail/T22560_fail_d
+ -}
+ | SuggestAddStandaloneKindSignature Name
+
{-| Suggests the user to fill in the wildcard constraint to
disambiguate which constraint that is.
=====================================
compiler/GHC/Types/Hint/Ppr.hs
=====================================
@@ -137,6 +137,8 @@ instance Outputable GhcHint where
]
SuggestAddStandaloneDerivation
-> text "Use a standalone deriving declaration instead"
+ SuggestAddStandaloneKindSignature name
+ -> text "Add a standalone kind signature for" <+> quotes (ppr name)
SuggestFillInWildcardConstraint
-> text "Fill in the wildcard constraint yourself"
SuggestRenameForall
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -93,7 +93,6 @@ module GHC.Types.Var (
isTyVarBinder,
tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders,
mapVarBndr, mapVarBndrs,
- setBndrVar, setBndrVars,
-- ** Constructing TyVar's
mkTyVar, mkTcTyVar,
@@ -762,12 +761,6 @@ mapVarBndr f (Bndr v fl) = Bndr (f v) fl
mapVarBndrs :: (var -> var') -> [VarBndr var flag] -> [VarBndr var' flag]
mapVarBndrs f = map (mapVarBndr f)
-setBndrVar :: var' -> VarBndr var flag -> VarBndr var' flag
-setBndrVar v (Bndr _ flag) = Bndr v flag
-
-setBndrVars :: String -> [var'] -> [VarBndr var flag] -> [VarBndr var' flag]
-setBndrVars msg = zipWithEqual msg setBndrVar
-
instance Outputable tv => Outputable (VarBndr tv ForAllTyFlag) where
ppr (Bndr v Required) = ppr v
ppr (Bndr v Specified) = char '@' <> ppr v
=====================================
docs/users_guide/9.8.1-notes.rst
=====================================
@@ -10,6 +10,7 @@ Language
<https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>`_
has been partially implemented. Namely, the ``@k``-binders in type declarations are now permitted::
+ type T :: forall k. k -> forall j. j -> Type
data T @k (a :: k) @(j :: Type) (b :: j)
This feature is guarded behind :extension:`TypeAbstractions`.
=====================================
docs/users_guide/exts/type_abstractions.rst
=====================================
@@ -106,18 +106,22 @@ The type abstraction syntax can be used in type declaration headers, including
``type``, ``data``, ``newtype``, ``class``, ``type family``, and ``data family``
declarations. Here are a few examples::
- class C @k (a :: k) where ...
+ type C :: forall k. k -> Constraint
+ class C @k a where ...
^^
+ type D :: forall k j. k -> j -> Type
data D @k @j (a :: k) (b :: j) = ...
^^ ^^
- type family F @p @q (a :: p) (b :: q) where ...
+ type F :: forall p q. p -> q -> (p, q)
+ type family F @p @q a b where ...
^^ ^^
Just as ordinary type parameters, invisible type variable binders may have kind
annotations::
+ type F :: forall p q. p -> q -> (p, q)
type family F @(p :: Type) @(q :: Type) (a :: p) (b :: q) where ...
Scope
@@ -137,13 +141,8 @@ method signature instead.
Type checking
~~~~~~~~~~~~~
-When the type declaration has no standalone kind signature, a ``@k``-binder gives rise
-to a ``forall k.`` quantifier in the inferred kind signature. The inferred
-``forall k.`` does not float to the left; the order of quantifiers continues to
-match the order of binders in the header::
-
- -- Inferred kind: forall k. k -> forall j. j -> Type
- data B @k (a :: k) @j (b :: j)
+Invisible type variable binders require either a standalone kind signature or a
+complete user-supplied kind.
If a standalone kind signature is given, GHC will match up ``@k``-binders with
the corresponding ``forall k.`` quantifiers in the signature::
@@ -180,4 +179,13 @@ In this example, ``@k`` is matched with ``forall a.``, not ``forall b.``:
| ``a ->`` | ``x`` |
+--------------+----------------------+
| ``b ->`` | ``y`` |
-+--------------+----------------------+
\ No newline at end of file
++--------------+----------------------+
+
+When a standalone kind signature is absent but the definition has a complete
+user-supplied kind (and the :extension:`CUSKs` extension is enabled),
+a ``@k``-binder gives rise to a ``forall k.`` quantifier in the inferred kind
+signature. The inferred ``forall k.`` does not float to the left; the order of
+quantifiers continues to match the order of binders in the header::
+
+ -- Inferred kind: forall k. k -> forall j. j -> Type
+ data B @(k :: Type) (a :: k) @(j :: Type) (b :: j)
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_compile/T22560d.hs
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE CUSKs #-}
module T22560d where
@@ -6,27 +7,27 @@ import Data.Kind
import Data.Proxy
-- type B :: forall k. k -> forall j. j -> Type
-data B @k (a :: k) @j (b :: j)
+data B @(k :: Type) (a :: k) @(j :: Type) (b :: j)
-- type D :: forall k. k -> Type
-data D @k (a :: k) = MkD (Proxy k) (Proxy a)
+data D @(k :: Type) (a :: k) = MkD (Proxy k) (Proxy a)
-- type N :: forall k. k -> Type
-newtype N @k (a :: k) = MkN (Proxy a -> Proxy k)
+newtype N @(k :: Type) (a :: k) = MkN (Proxy a -> Proxy k)
-- type S :: forall k. k -> Type
-type S @k (a :: k) = Proxy a -> Proxy k
+type S @(k :: Type) (a :: k) = Proxy a -> Proxy k :: Type
-- type C :: forall k. k -> Constraint
-class C @k (a :: k) where
+class C @(k :: Type) (a :: k) where
f :: Proxy a -> Proxy k
-- type F :: forall k. k -> k
-type family F @k (a :: k) :: k where
+type family F @(k :: Type) (a :: k) :: k where
F a = a
--- type U :: forall {k} (a :: k). Type
-type U @a = Int
+-- type U :: forall k (a :: k). Type
+type U @(a :: k) = Int :: Type
-- type Z :: forall k -> forall (a :: k). Type
-type Z k @(a :: k) = Proxy a
\ No newline at end of file
+type Z (k :: Type) @(a :: k) = Proxy a :: Type
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_compile/T22560d.stdout
=====================================
@@ -4,5 +4,5 @@ N :: forall k. k -> Type
S :: forall k. k -> Type
C :: forall k. k -> Constraint
F :: forall k. k -> k
-U :: forall {k} (a :: k). Type
+U :: forall k (a :: k). Type
Z :: forall k -> forall (a :: k). Type
=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_a.stderr
=====================================
@@ -2,5 +2,6 @@
T22560_fail_a.hs:7:1: error: [GHC-57916]
• Invalid invisible type variable binder:
@k
- There is no matching forall-bound variable in the standalone kind signature.
+ There is no matching forall-bound variable
+ in the standalone kind signature for ‘P’.
• In the data type declaration for ‘P’
=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_b.stderr
=====================================
@@ -2,5 +2,6 @@
T22560_fail_b.hs:6:1: error: [GHC-57916]
• Invalid invisible type variable binder:
@a
- There is no matching forall-bound variable in the standalone kind signature.
+ There is no matching forall-bound variable
+ in the standalone kind signature for ‘P’.
• In the data type declaration for ‘P’
=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_c.hs
=====================================
@@ -1,3 +1,6 @@
module T22560_fail_c where
+import Data.Kind
+
+type Dup :: forall k j. k -> Type
data Dup @k @k (a :: k)
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_c.stderr
=====================================
@@ -1,5 +1,5 @@
-T22560_fail_c.hs:3:11: error:
+T22560_fail_c.hs:6:11: error:
Conflicting definitions for ‘k’
- Bound at: T22560_fail_c.hs:3:11
- T22560_fail_c.hs:3:14
+ Bound at: T22560_fail_c.hs:6:11
+ T22560_fail_c.hs:6:14
=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_d.hs
=====================================
@@ -0,0 +1,5 @@
+module T22560_fail_d where
+
+import Data.Kind
+
+data T @k (a :: k) -- No CUSK, no SAKS
\ No newline at end of file
=====================================
testsuite/tests/typecheck/should_fail/T22560_fail_d.stderr
=====================================
@@ -0,0 +1,9 @@
+
+T22560_fail_d.hs:5:1: error: [GHC-92337]
+ • Invalid invisible type variable binder:
+ @k
+ Either a standalone kind signature (SAKS)
+ or a complete user-supplied kind (CUSK)
+ is required to use invisible binders.
+ • In the data type declaration for ‘T’
+ Suggested fix: Add a standalone kind signature for ‘T’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -671,4 +671,5 @@ test('T20666a', normal, compile_fail, [''])
test('T22560_fail_a', normal, compile_fail, [''])
test('T22560_fail_b', normal, compile_fail, [''])
test('T22560_fail_c', normal, compile_fail, [''])
+test('T22560_fail_d', normal, compile_fail, [''])
test('T22560_fail_ext', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2865bcef720fb2ef8be860854b801b0e22fa8430
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2865bcef720fb2ef8be860854b801b0e22fa8430
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/20230127/00b9acbb/attachment-0001.html>
More information about the ghc-commits
mailing list