[Git][ghc/ghc][wip/sand-witch/DIB-INSTANCES] Remove arity inference in type declarations (#23514)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Thu Jun 15 13:46:15 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/DIB-INSTANCES at Glasgow Haskell Compiler / GHC
Commits:
29e2c8a4 by Andrei Borzenkov at 2023-06-15T17:45:56+04:00
Remove arity inference in type declarations (#23514)
Arity inference in type declarations was introduced
as a workaround for the lack of @k-binders.
They were added in 4aea0a72040, so I simplified all
of this by simply removing arity inference altogether.
This is part of GHC Proposal #425 "Invisible binders in type
declarations".
- - - - -
22 changed files:
- compiler/GHC/Core/Type.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Splice.hs
- libraries/template-haskell/Language/Haskell/TH/Syntax.hs
- testsuite/tests/perf/compiler/CoOpt_Singletons.hs
- + testsuite/tests/rename/should_compile/T23514b.hs
- testsuite/tests/rename/should_compile/all.T
- + testsuite/tests/rename/should_fail/T23514a.hs
- + testsuite/tests/rename/should_fail/T23514a.stderr
- testsuite/tests/rename/should_fail/all.T
- testsuite/tests/saks/should_compile/T16724.stdout
- testsuite/tests/saks/should_compile/saks020.hs
- testsuite/tests/saks/should_compile/saks030.hs
- testsuite/tests/saks/should_compile/saks032.hs
- testsuite/tests/saks/should_fail/T18863b.stderr
- + testsuite/tests/th/CodeQ_HKD.hs
- testsuite/tests/th/all.T
- testsuite/tests/typecheck/should_fail/T18640a.hs
- testsuite/tests/typecheck/should_fail/T18640a.stderr
- testsuite/tests/typecheck/should_fail/T18640c.hs
- testsuite/tests/typecheck/should_fail/T18640c.stderr
Changes:
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -60,7 +60,7 @@ module GHC.Core.Type (
mkTyConBindersPreferAnon,
mkPiTy, mkPiTys,
piResultTy, piResultTys,
- applyTysX, dropForAlls,
+ applyTysX, dropForAlls, dropInvisForAlls,
mkFamilyTyConApp,
buildSynTyCon,
@@ -1937,6 +1937,14 @@ dropForAlls ty = go ty
go ty | Just ty' <- coreView ty = go ty'
go res = res
+-- | Drops all invisible ForAllTys
+dropInvisForAlls :: Type -> Type
+dropInvisForAlls ty = go ty
+ where
+ go (ForAllTy (Bndr _ Invisible{}) res) = go res
+ go ty | Just ty' <- coreView ty = go ty'
+ go res = res
+
-- | Attempts to take a forall type apart, but only if it's a proper forall,
-- with a named binder
splitForAllTyCoVar_maybe :: Type -> Maybe (TyCoVar, Type)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -863,12 +863,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
cons = visibleIfConDecls condecls
pp_where = ppWhen (gadt && not (null cons)) $ text "where"
pp_cons = ppr_trim (map show_con cons) :: [SDoc]
- pp_kind = ppUnless (if ki_sig_printable
- then isIfaceRhoType kind
- -- Even in the presence of a standalone kind signature, a non-tau
- -- result kind annotation cannot be discarded as it determines the arity.
- -- See Note [Arity inference in kcCheckDeclHeader_sig] in GHC.Tc.Gen.HsType
- else isIfaceLiftedTypeKind kind)
+ pp_kind = ppUnless (ki_sig_printable || isIfaceLiftedTypeKind kind)
(dcolon <+> ppr kind)
pp_lhs = case parent of
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2555,37 +2555,29 @@ kcCheckDeclHeader_sig sig_kind name flav
-- ^^^^^^^^^
-- We do it here because at this point the environment has been
-- 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
- -- Work out extra_arity, the number of extra invisible binders from
- -- the kind signature that should be part of the TyCon's arity.
- -- See Note [Arity inference in kcCheckDeclHeader_sig]
- ; let n_invis_tcbs = countWhile isInvisibleTyConBinder excess_sig_tcbs
- invis_arity = case ctx_k of
- AnyKind -> n_invis_tcbs -- No kind signature, so make all the invisible binders
- -- the signature into part of the arity of the TyCon
- OpenKind -> n_invis_tcbs -- Result kind is (TYPE rr), so again make all the
- -- invisible binders part of the arity of the TyCon
- TheKind ki -> 0 `max` (n_invis_tcbs - invisibleTyBndrCount ki)
+ ; let sig_res_kind' = mkTyConKind excess_sig_tcbs sig_res_kind
- ; let (invis_tcbs, resid_tcbs) = splitAt invis_arity excess_sig_tcbs
- ; let sig_res_kind' = mkTyConKind resid_tcbs sig_res_kind
-
- ; traceTc "kcCheckDeclHeader_sig 2" $ vcat [ ppr excess_sig_tcbs
- , ppr invis_arity, ppr invis_tcbs
- , ppr n_invis_tcbs ]
+ ; traceTc "kcCheckDeclHeader_sig 2" (ppr excess_sig_tcbs)
-- 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
- ; discardResult (unifyKind Nothing sig_res_kind' res_ki) }
+ OpenKind ->
+ do { res_ki <- newExpectedKind ctx_k
+ ; discardResult (unifyKind Nothing (dropInvisForAlls sig_res_kind') res_ki) }
+ TheKind _ ->
+ do { res_ki <- newExpectedKind ctx_k
+ ; discardResult (unifyKind Nothing sig_res_kind' res_ki) }
-- Add more binders for data/newtype, so the result kind has no arrows
-- See Note [Datatype return kinds]
- ; if null resid_tcbs || not (needsEtaExpansion flav)
- then return (invis_tcbs, sig_res_kind')
+ ; if null excess_sig_tcbs || not (needsEtaExpansion flav)
+ then return ([], sig_res_kind')
else return (excess_sig_tcbs, sig_res_kind)
}
@@ -2738,8 +2730,8 @@ swizzleTcb swizzle_env subst (Bndr tv vis)
-- See Note [Source locations for implicitly bound type variables]
-- in GHC.Tc.Rename.HsType
-{- See Note [kcCheckDeclHeader_sig]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [kcCheckDeclHeader_sig]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given a kind signature 'sig_kind' and a declaration header,
kcCheckDeclHeader_sig verifies that the declaration conforms to the
signature. The end result is a PolyTcTyCon 'tc' such that:
@@ -2780,85 +2772,39 @@ Basic plan is this:
part of the signature (k -> Type) with the kind signature of the decl,
(j -> Type). This unification, done in kcCheckDeclHeader, needs TcTyVars.
- * The tricky extra_arity part is described in
- Note [Arity inference in kcCheckDeclHeader_sig]
-
-Note [Arity inference in kcCheckDeclHeader_sig]
+Note [Arity of type families and type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider these declarations:
- type family S1 :: forall k2. k1 -> k2 -> Type
- type family S2 (a :: k1) (b :: k2) :: Type
-
-Both S1 and S2 can be given the same standalone kind signature:
- type S1 :: forall k1 k2. k1 -> k2 -> Type
- type S2 :: forall k1 k2. k1 -> k2 -> Type
-
-And, indeed, tyConKind S1 == tyConKind S2. However,
-tyConBinders and tyConResKind for S1 and S2 are different:
-
- tyConBinders S1 == [spec k1]
- tyConResKind S1 == forall k2. k1 -> k2 -> Type
- tyConKind S1 == forall k1 k2. k1 -> k2 -> Type
-
- tyConBinders S2 == [spec k1, spec k2, anon-vis (a :: k1), anon-vis (b :: k2)]
- tyConResKind S2 == Type
- tyConKind S1 == forall k1 k2. k1 -> k2 -> Type
-
-This difference determines the /arity/:
- tyConArity tc == length (tyConBinders tc)
-That is, the arity of S1 is 1, while the arity of S2 is 4.
-
-'kcCheckDeclHeader_sig' needs to infer the desired arity, to split the
-standalone kind signature into binders and the result kind. It does so
-in two rounds:
-
-1. matchUpSigWithDecl matches up
- - the [TyConBinder] from (applying splitTyConKind to) the kind signature
- - with the [LHsTyVarBndr] from the type declaration.
- That may leave some excess TyConBinder: in the case of S2 there are
- no excess TyConBinders, but in the case of S1 there are two (since
- there are no LHsTYVarBndrs.
-
-2. Split off further TyConBinders (in the case of S1, one more) to
- make it possible to unify the residual return kind with the
- signature in the type declaration. More precisely, split off such
- enough invisible that the remainder of the standalone kind
- signature and the user-written result kind signature have the same
- number of invisible quantifiers.
-
-As another example consider the following declarations:
-
- type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
- type family F a b
-
- type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
- type family G a b :: forall r2. (r1, r2) -> Type
-
-For both F and G, the signature (after splitTyConKind) has
- sig_tcbs :: [TyConBinder]
- = [ anon-vis (@a_aBq), spec (@j_auA), anon-vis (@(b_aBr :: j_auA))
- , spec (@k1_auB), spec (@k2_auC)
- , anon-vis (@(c_aBs :: (k1_auB, k2_auC)))]
-
-matchUpSigWithDecl will consume the first three of these, passing on
- excess_sig_tcbs
- = [ spec (@k1_auB), spec (@k2_auC)
- , anon-vis (@(c_aBs :: (k1_auB, k2_auC)))]
-
-For F, there is no result kind signature in the declaration for F, so
-we absorb all invisible binders into F's arity. The resulting arity of
-F is 3+2=5.
-
-Now, in the case of G, we have a result kind sig 'forall r2. (r2,r2)->Type'.
-This has one invisible binder, so we split of enough extra binders from
-our excess_sig_tcbs to leave just one to match 'r2'.
-
- res_ki = forall r2. (r1, r2) -> Type
- kisig = forall k1 k2. (k1, k2) -> Type
- ^^^
- split off this one.
-
-The resulting arity of G is 3+1=4.
+Consider
+
+ type F1 :: forall k. k -> k -> Type
+ type family F1 @k
+
+ type F2a :: forall k. k -> k -> Type
+ type family F2a @k a
+
+ type F2b :: forall k. k -> k -> Type
+ type family F2b a
+
+ type F3 :: forall k. k -> k -> Type
+ type family F3 a b
+
+All four have the same /kind/, but what /arity/ do they have?
+For a type family, the arity is critical:
+* A type family must always appear saturated (up to its arity)
+* A type family can match only on `arity` arguments, not further ones
+* The arity is recorded by `tyConArity`, and is equal to the number of
+ `TyConBinders` in the `TyCon`.
+* In this context "arity" includes both kind and type arguments.
+
+The arity is not determined by the kind signature (all four have the same signature).
+Rather, it is determined by the declaration of the family:
+* `F1` has arity 1.
+* `F2a` has arity 2.
+* `F2b` also has arity 2: the kind argument is invisible.
+* `F3` has arity 3; again the kind argument is invisible.
+
+The matching-up of kind signature with the declaration itself is done by
+`matchUpWithSigDecl`.
Note [discardResult in kcCheckDeclHeader_sig]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -796,7 +796,7 @@ tcTExpTy m_ty exp_ty
TcRnTHError $ TypedTHError $ TypedTHWithPolyType exp_ty
; codeCon <- tcLookupTyCon codeTyConName
; let rep = getRuntimeRep exp_ty
- ; return (mkTyConApp codeCon [rep, m_ty, exp_ty]) }
+ ; return (mkTyConApp codeCon [m_ty, rep, exp_ty]) }
quotationCtxtDoc :: LHsExpr GhcRn -> SDoc
quotationCtxtDoc br_body
=====================================
libraries/template-haskell/Language/Haskell/TH/Syntax.hs
=====================================
@@ -378,8 +378,11 @@ The splice will evaluate to (MkAge 3) and you can't add that to
4::Int. So you can't coerce a (Code Q Age) to a (Code Q Int). -}
-- Code constructor
-
+#if __GLASGOW_HASKELL__ >= 907
+type Code :: (Kind.Type -> Kind.Type) -> forall r. TYPE r -> Kind.Type
+#else
type Code :: (Kind.Type -> Kind.Type) -> TYPE r -> Kind.Type
+#endif
type role Code representational nominal -- See Note [Role of TExp]
newtype Code m a = Code
{ examineCode :: m (TExp a) -- ^ Underlying monadic value
=====================================
testsuite/tests/perf/compiler/CoOpt_Singletons.hs
=====================================
@@ -52,7 +52,7 @@ type SameKind :: k -> k -> Constraint
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type Sing :: k -> Type
-type family Sing :: k -> Type
+type family Sing @k :: k -> Type
type SLambda :: (k1 ~> k2) -> Type
newtype SLambda (f :: k1 ~> k2) =
@@ -159,7 +159,7 @@ type instance Apply (Lambda_6989586621679038878Sym3 f6989586621679038875 g698958
type family Lambda_6989586621679038878Sym4 f6989586621679038875 g6989586621679038876 a_69895866216790388666989586621679038877 x6989586621679038880 where
Lambda_6989586621679038878Sym4 f6989586621679038875 g6989586621679038876 a_69895866216790388666989586621679038877 x6989586621679038880 = Lambda_6989586621679038878_a7z9 f6989586621679038875 g6989586621679038876 a_69895866216790388666989586621679038877 x6989586621679038880
type ($!@#@$) :: (~>) ((~>) a_a7yq b_a7yr) ((~>) a_a7yq b_a7yr)
-data ($!@#@$) :: (~>) ((~>) a_a7yq b_a7yr) ((~>) a_a7yq b_a7yr)
+data ($!@#@$) @a_a7yq @b_a7yr :: (~>) ((~>) a_a7yq b_a7yr) ((~>) a_a7yq b_a7yr)
where
(:$!@#@$###) :: SameKind (Apply ($!@#@$) arg_a7yP) (($!@#@$$) arg_a7yP) =>
($!@#@$) a6989586621679038860
@@ -177,7 +177,7 @@ type family ($!@#@$$$) (a6989586621679038860 :: (~>) a_a7yq b_a7yr) (a6989586621
($!@#@$$$) a6989586621679038860 a6989586621679038861 = ($!) a6989586621679038860 a6989586621679038861
infixr 0 $!@#@$$$
type (.@#@$) :: (~>) ((~>) b_a7ys c_a7yt) ((~>) ((~>) a_a7yu b_a7ys) ((~>) a_a7yu c_a7yt))
-data (.@#@$) :: (~>) ((~>) b_a7ys c_a7yt) ((~>) ((~>) a_a7yu b_a7ys) ((~>) a_a7yu c_a7yt))
+data (.@#@$) @b_a7ys @c_a7yt @a_a7yu :: (~>) ((~>) b_a7ys c_a7yt) ((~>) ((~>) a_a7yu b_a7ys) ((~>) a_a7yu c_a7yt))
where
(:.@#@$###) :: SameKind (Apply (.@#@$) arg_a7z1) ((.@#@$$) arg_a7z1) =>
(.@#@$) a6989586621679038872
@@ -205,7 +205,7 @@ type family (.@#@$$$$) (a6989586621679038872 :: (~>) b_a7ys c_a7yt) (a6989586621
(.@#@$$$$) a6989586621679038872 a6989586621679038873 a6989586621679038874 = (.) a6989586621679038872 a6989586621679038873 a6989586621679038874
infixr 9 .@#@$$$$
type FlipSym0 :: (~>) ((~>) a_a7yv ((~>) b_a7yw c_a7yx)) ((~>) b_a7yw ((~>) a_a7yv c_a7yx))
-data FlipSym0 :: (~>) ((~>) a_a7yv ((~>) b_a7yw c_a7yx)) ((~>) b_a7yw ((~>) a_a7yv c_a7yx))
+data FlipSym0 @a_a7yv @b_a7yw @c_a7yx :: (~>) ((~>) a_a7yv ((~>) b_a7yw c_a7yx)) ((~>) b_a7yw ((~>) a_a7yv c_a7yx))
where
FlipSym0KindInference :: SameKind (Apply FlipSym0 arg_a7zf) (FlipSym1 arg_a7zf) =>
FlipSym0 a6989586621679038886
@@ -229,7 +229,7 @@ type FlipSym3 :: (~>) a_a7yv ((~>) b_a7yw c_a7yx)
type family FlipSym3 (a6989586621679038886 :: (~>) a_a7yv ((~>) b_a7yw c_a7yx)) (a6989586621679038887 :: b_a7yw) (a6989586621679038888 :: a_a7yv) :: c_a7yx where
FlipSym3 a6989586621679038886 a6989586621679038887 a6989586621679038888 = Flip a6989586621679038886 a6989586621679038887 a6989586621679038888
type IdSym0 :: (~>) a_a7yy a_a7yy
-data IdSym0 :: (~>) a_a7yy a_a7yy
+data IdSym0 @a_a7yy :: (~>) a_a7yy a_a7yy
where
IdSym0KindInference :: SameKind (Apply IdSym0 arg_a7zn) (IdSym1 arg_a7zn) =>
IdSym0 a6989586621679038894
@@ -314,7 +314,7 @@ $(genSingletons [''Dual])
-}
type DualSym0 :: forall (a_a5fi :: Type). (~>) a_a5fi (Dual (a_a5fi :: Type))
-data DualSym0 :: (~>) a_a5fi (Dual (a_a5fi :: Type))
+data DualSym0 @a_a5fi :: (~>) a_a5fi (Dual (a_a5fi :: Type))
where
DualSym0KindInference :: SameKind (Apply DualSym0 arg_a9sh) (DualSym1 arg_a9sh) =>
DualSym0 a6989586621679046142
@@ -324,7 +324,7 @@ type DualSym1 :: forall (a_a5fi :: Type). a_a5fi
type family DualSym1 (a6989586621679046142 :: a_a5fi) :: Dual (a_a5fi :: Type) where
DualSym1 a6989586621679046142 = 'Dual a6989586621679046142
type GetDualSym0 :: forall (a_a5fi :: Type). (~>) (Dual (a_a5fi :: Type)) a_a5fi
-data GetDualSym0 :: (~>) (Dual (a_a5fi :: Type)) a_a5fi
+data GetDualSym0 @a_a5fi :: (~>) (Dual (a_a5fi :: Type)) a_a5fi
where
GetDualSym0KindInference :: SameKind (Apply GetDualSym0 arg_a9sk) (GetDualSym1 arg_a9sk) =>
GetDualSym0 a6989586621679046145
@@ -369,7 +369,7 @@ $(singletonsOnly [d|
-}
type (<>@#@$) :: forall a_a9GJ. (~>) a_a9GJ ((~>) a_a9GJ a_a9GJ)
-data (<>@#@$) :: (~>) a_a9GJ ((~>) a_a9GJ a_a9GJ)
+data (<>@#@$) @a_a9GJ :: (~>) a_a9GJ ((~>) a_a9GJ a_a9GJ)
where
(:<>@#@$###) :: SameKind (Apply (<>@#@$) arg_a9GZ) ((<>@#@$$) arg_a9GZ) =>
(<>@#@$) a6989586621679047054
@@ -386,10 +386,10 @@ type family (<>@#@$$$) (a6989586621679047054 :: a_a9GJ) (a6989586621679047055 ::
class PSemigroup a_a9GJ where
type family (<>) (arg_a9GX :: a_a9GJ) (arg_a9GY :: a_a9GJ) :: a_a9GJ
type MemptySym0 :: forall a_a9GK. a_a9GK
-type family MemptySym0 :: a_a9GK where
+type family MemptySym0 @a_a9GK :: a_a9GK where
MemptySym0 = Mempty
type MappendSym0 :: forall a_a9GK. (~>) a_a9GK ((~>) a_a9GK a_a9GK)
-data MappendSym0 :: (~>) a_a9GK ((~>) a_a9GK a_a9GK)
+data MappendSym0 @a_a9GK :: (~>) a_a9GK ((~>) a_a9GK a_a9GK)
where
MappendSym0KindInference :: SameKind (Apply MappendSym0 arg_a9H5) (MappendSym1 arg_a9H5) =>
MappendSym0 a6989586621679047060
@@ -407,7 +407,7 @@ type Mappend_6989586621679047064 :: a_a9GK -> a_a9GK -> a_a9GK
type family Mappend_6989586621679047064 (a_a9Hg :: a_a9GK) (a_a9Hh :: a_a9GK) :: a_a9GK where
Mappend_6989586621679047064 a_6989586621679047066_a9Hl a_6989586621679047068_a9Hm = Apply (Apply (<>@#@$) a_6989586621679047066_a9Hl) a_6989586621679047068_a9Hm
type Mappend_6989586621679047064Sym0 :: (~>) a_a9GK ((~>) a_a9GK a_a9GK)
-data Mappend_6989586621679047064Sym0 :: (~>) a_a9GK ((~>) a_a9GK a_a9GK)
+data Mappend_6989586621679047064Sym0 @a_a9GK :: (~>) a_a9GK ((~>) a_a9GK a_a9GK)
where
Mappend_6989586621679047064Sym0KindInference :: SameKind (Apply Mappend_6989586621679047064Sym0 arg_a9Hi) (Mappend_6989586621679047064Sym1 arg_a9Hi) =>
Mappend_6989586621679047064Sym0 a6989586621679047073
@@ -431,7 +431,7 @@ type TFHelper_6989586621679047079 :: Dual a_a9GL
type family TFHelper_6989586621679047079 (a_a9Hr :: Dual a_a9GL) (a_a9Hs :: Dual a_a9GL) :: Dual a_a9GL where
TFHelper_6989586621679047079 ('Dual a_a9Hw) ('Dual b_a9Hx) = Apply DualSym0 (Apply (Apply (<>@#@$) b_a9Hx) a_a9Hw)
type TFHelper_6989586621679047079Sym0 :: (~>) (Dual a_a9GL) ((~>) (Dual a_a9GL) (Dual a_a9GL))
-data TFHelper_6989586621679047079Sym0 :: (~>) (Dual a_a9GL) ((~>) (Dual a_a9GL) (Dual a_a9GL))
+data TFHelper_6989586621679047079Sym0 @a_a9GL :: (~>) (Dual a_a9GL) ((~>) (Dual a_a9GL) (Dual a_a9GL))
where
TFHelper_6989586621679047079Sym0KindInference :: SameKind (Apply TFHelper_6989586621679047079Sym0 arg_a9Ht) (TFHelper_6989586621679047079Sym1 arg_a9Ht) =>
TFHelper_6989586621679047079Sym0 a6989586621679047084
@@ -450,10 +450,10 @@ type family TFHelper_6989586621679047079Sym2 (a6989586621679047084 :: Dual a_a9G
instance PSemigroup (Dual a_a9GL) where
type (<>) a_a9Hn a_a9Ho = Apply (Apply TFHelper_6989586621679047079Sym0 a_a9Hn) a_a9Ho
type Mempty_6989586621679047088 :: Dual a_a9GO
-type family Mempty_6989586621679047088 :: Dual a_a9GO where
+type family Mempty_6989586621679047088 @a_a9GO :: Dual a_a9GO where
Mempty_6989586621679047088 = Apply DualSym0 MemptySym0
type Mempty_6989586621679047088Sym0 :: Dual a_a9GO
-type family Mempty_6989586621679047088Sym0 :: Dual a_a9GO where
+type family Mempty_6989586621679047088Sym0 @a_a9GO :: Dual a_a9GO where
Mempty_6989586621679047088Sym0 = Mempty_6989586621679047088
instance PMonoid (Dual a_a9GO) where
type Mempty = Mempty_6989586621679047088Sym0
@@ -508,7 +508,7 @@ $(singletonsOnly [d|
-}
type AppEndoSym0 :: (~>) (Endo a_agCh) ((~>) a_agCh a_agCh)
-data AppEndoSym0 :: (~>) (Endo a_agCh) ((~>) a_agCh a_agCh)
+data AppEndoSym0 @a_agCh :: (~>) (Endo a_agCh) ((~>) a_agCh a_agCh)
where
AppEndoSym0KindInference :: SameKind (Apply AppEndoSym0 arg_agUE) (AppEndoSym1 arg_agUE) =>
AppEndoSym0 a6989586621679074809
@@ -530,7 +530,7 @@ type TFHelper_6989586621679075091 :: Endo a_agCk
type family TFHelper_6989586621679075091 (a_agZf :: Endo a_agCk) (a_agZg :: Endo a_agCk) :: Endo a_agCk where
TFHelper_6989586621679075091 ('Endo x_agZk) ('Endo y_agZl) = Apply EndoSym0 (Apply (Apply (.@#@$) x_agZk) y_agZl)
type TFHelper_6989586621679075091Sym0 :: (~>) (Endo a_agCk) ((~>) (Endo a_agCk) (Endo a_agCk))
-data TFHelper_6989586621679075091Sym0 :: (~>) (Endo a_agCk) ((~>) (Endo a_agCk) (Endo a_agCk))
+data TFHelper_6989586621679075091Sym0 @a_agCk :: (~>) (Endo a_agCk) ((~>) (Endo a_agCk) (Endo a_agCk))
where
TFHelper_6989586621679075091Sym0KindInference :: SameKind (Apply TFHelper_6989586621679075091Sym0 arg_agZh) (TFHelper_6989586621679075091Sym1 arg_agZh) =>
TFHelper_6989586621679075091Sym0 a6989586621679075096
@@ -549,10 +549,10 @@ type family TFHelper_6989586621679075091Sym2 (a6989586621679075096 :: Endo a_agC
instance PSemigroup (Endo a_agCk) where
type (<>) a_agZb a_agZc = Apply (Apply TFHelper_6989586621679075091Sym0 a_agZb) a_agZc
type Mempty_6989586621679075313 :: Endo a_agCn
-type family Mempty_6989586621679075313 :: Endo a_agCn where
+type family Mempty_6989586621679075313 @a_agCn :: Endo a_agCn where
Mempty_6989586621679075313 = Apply EndoSym0 IdSym0
type Mempty_6989586621679075313Sym0 :: Endo a_agCn
-type family Mempty_6989586621679075313Sym0 :: Endo a_agCn where
+type family Mempty_6989586621679075313Sym0 @a_agCn :: Endo a_agCn where
Mempty_6989586621679075313Sym0 = Mempty_6989586621679075313
instance PMonoid (Endo a_agCn) where
type Mempty = Mempty_6989586621679075313Sym0
@@ -602,7 +602,7 @@ $(singletonsOnly [d|
type FoldMapSym0 :: forall a_ahBz
m_ahBy
t_ahBx. (~>) ((~>) a_ahBz m_ahBy) ((~>) (t_ahBx a_ahBz) m_ahBy)
-data FoldMapSym0 :: (~>) ((~>) a_ahBz m_ahBy) ((~>) (t_ahBx a_ahBz) m_ahBy)
+data FoldMapSym0 @a_ahBz @m_ahBy @t_ahBx :: (~>) ((~>) a_ahBz m_ahBy) ((~>) (t_ahBx a_ahBz) m_ahBy)
where
FoldMapSym0KindInference :: SameKind (Apply FoldMapSym0 arg_ahBS) (FoldMapSym1 arg_ahBS) =>
FoldMapSym0 a6989586621679077489
@@ -621,7 +621,7 @@ type family FoldMapSym2 (a6989586621679077489 :: (~>) a_ahBz m_ahBy) (a698958662
type FoldrSym0 :: forall a_ahBA
b_ahBB
t_ahBx. (~>) ((~>) a_ahBA ((~>) b_ahBB b_ahBB)) ((~>) b_ahBB ((~>) (t_ahBx a_ahBA) b_ahBB))
-data FoldrSym0 :: (~>) ((~>) a_ahBA ((~>) b_ahBB b_ahBB)) ((~>) b_ahBB ((~>) (t_ahBx a_ahBA) b_ahBB))
+data FoldrSym0 @a_ahBA @b_ahBB @t_ahBx :: (~>) ((~>) a_ahBA ((~>) b_ahBB b_ahBB)) ((~>) b_ahBB ((~>) (t_ahBx a_ahBA) b_ahBB))
where
FoldrSym0KindInference :: SameKind (Apply FoldrSym0 arg_ahBY) (FoldrSym1 arg_ahBY) =>
FoldrSym0 a6989586621679077495
@@ -653,7 +653,7 @@ type family FoldrSym3 (a6989586621679077495 :: (~>) a_ahBA ((~>) b_ahBB b_ahBB))
type Foldr'Sym0 :: forall a_ahBC
b_ahBD
t_ahBx. (~>) ((~>) a_ahBC ((~>) b_ahBD b_ahBD)) ((~>) b_ahBD ((~>) (t_ahBx a_ahBC) b_ahBD))
-data Foldr'Sym0 :: (~>) ((~>) a_ahBC ((~>) b_ahBD b_ahBD)) ((~>) b_ahBD ((~>) (t_ahBx a_ahBC) b_ahBD))
+data Foldr'Sym0 @a_ahBC @b_ahBD @t_ahBx :: (~>) ((~>) a_ahBC ((~>) b_ahBD b_ahBD)) ((~>) b_ahBD ((~>) (t_ahBx a_ahBC) b_ahBD))
where
Foldr'Sym0KindInference :: SameKind (Apply Foldr'Sym0 arg_ahC5) (Foldr'Sym1 arg_ahC5) =>
Foldr'Sym0 a6989586621679077502
@@ -685,7 +685,7 @@ type family Foldr'Sym3 (a6989586621679077502 :: (~>) a_ahBC ((~>) b_ahBD b_ahBD)
type FoldlSym0 :: forall b_ahBE
a_ahBF
t_ahBx. (~>) ((~>) b_ahBE ((~>) a_ahBF b_ahBE)) ((~>) b_ahBE ((~>) (t_ahBx a_ahBF) b_ahBE))
-data FoldlSym0 :: (~>) ((~>) b_ahBE ((~>) a_ahBF b_ahBE)) ((~>) b_ahBE ((~>) (t_ahBx a_ahBF) b_ahBE))
+data FoldlSym0 @b_ahBE @a_ahBF @t_ahBx :: (~>) ((~>) b_ahBE ((~>) a_ahBF b_ahBE)) ((~>) b_ahBE ((~>) (t_ahBx a_ahBF) b_ahBE))
where
FoldlSym0KindInference :: SameKind (Apply FoldlSym0 arg_ahCc) (FoldlSym1 arg_ahCc) =>
FoldlSym0 a6989586621679077509
@@ -753,7 +753,7 @@ type Foldr'_6989586621679077515 :: (~>) a_ahBC ((~>) b_ahBD b_ahBD)
type family Foldr'_6989586621679077515 (a_ahCl :: (~>) a_ahBC ((~>) b_ahBD b_ahBD)) (a_ahCm :: b_ahBD) (a_ahCn :: t_ahBx a_ahBC) :: b_ahBD where
Foldr'_6989586621679077515 f_ahCs z0_ahCt xs_ahCu = Apply (Apply (Apply (Apply FoldlSym0 (Let6989586621679077527F'Sym3 f_ahCs z0_ahCt xs_ahCu)) IdSym0) xs_ahCu) z0_ahCt
type Foldr'_6989586621679077515Sym0 :: (~>) ((~>) a_ahBC ((~>) b_ahBD b_ahBD)) ((~>) b_ahBD ((~>) (t_ahBx a_ahBC) b_ahBD))
-data Foldr'_6989586621679077515Sym0 :: (~>) ((~>) a_ahBC ((~>) b_ahBD b_ahBD)) ((~>) b_ahBD ((~>) (t_ahBx a_ahBC) b_ahBD))
+data Foldr'_6989586621679077515Sym0 @a_ahBC @b_ahBD @t_ahBx :: (~>) ((~>) a_ahBC ((~>) b_ahBD b_ahBD)) ((~>) b_ahBD ((~>) (t_ahBx a_ahBC) b_ahBD))
where
Foldr'_6989586621679077515Sym0KindInference :: SameKind (Apply Foldr'_6989586621679077515Sym0 arg_ahCo) (Foldr'_6989586621679077515Sym1 arg_ahCo) =>
Foldr'_6989586621679077515Sym0 a6989586621679077521
@@ -781,7 +781,7 @@ type Foldl_6989586621679077538 :: (~>) b_ahBE ((~>) a_ahBF b_ahBE)
type family Foldl_6989586621679077538 (a_ahCI :: (~>) b_ahBE ((~>) a_ahBF b_ahBE)) (a_ahCJ :: b_ahBE) (a_ahCK :: t_ahBx a_ahBF) :: b_ahBE where
Foldl_6989586621679077538 f_ahCP z_ahCQ t_ahCR = Apply (Apply AppEndoSym0 (Apply GetDualSym0 (Apply (Apply FoldMapSym0 (Apply (Apply (.@#@$) DualSym0) (Apply (Apply (.@#@$) EndoSym0) (Apply FlipSym0 f_ahCP)))) t_ahCR))) z_ahCQ
type Foldl_6989586621679077538Sym0 :: (~>) ((~>) b_ahBE ((~>) a_ahBF b_ahBE)) ((~>) b_ahBE ((~>) (t_ahBx a_ahBF) b_ahBE))
-data Foldl_6989586621679077538Sym0 :: (~>) ((~>) b_ahBE ((~>) a_ahBF b_ahBE)) ((~>) b_ahBE ((~>) (t_ahBx a_ahBF) b_ahBE))
+data Foldl_6989586621679077538Sym0 @b_ahBE @a_ahBF @t_ahBx :: (~>) ((~>) b_ahBE ((~>) a_ahBF b_ahBE)) ((~>) b_ahBE ((~>) (t_ahBx a_ahBF) b_ahBE))
where
Foldl_6989586621679077538Sym0KindInference :: SameKind (Apply Foldl_6989586621679077538Sym0 arg_ahCL) (Foldl_6989586621679077538Sym1 arg_ahCL) =>
Foldl_6989586621679077538Sym0 a6989586621679077544
@@ -946,7 +946,7 @@ type FoldMap_6989586621679081137 :: (~>) a_ahBz_acmX m_ahBy_acmY
type family FoldMap_6989586621679081137 (a_aiyL :: (~>) a_ahBz_acmX m_ahBy_acmY) (a_aiyM :: Tuple2 a_aikY a_ahBz_acmX) :: m_ahBy_acmY where
FoldMap_6989586621679081137 _f_6989586621679081117_aiyQ ('Tuple2 a_6989586621679081123_aiyR a_6989586621679081125_aiyS) = Apply (Apply MappendSym0 (Apply (Apply (Apply (Apply Lambda_6989586621679081147Sym0 _f_6989586621679081117_aiyQ) a_6989586621679081123_aiyR) a_6989586621679081125_aiyS) a_6989586621679081123_aiyR)) (Apply _f_6989586621679081117_aiyQ a_6989586621679081125_aiyS)
type FoldMap_6989586621679081137Sym0 :: (~>) ((~>) a_ahBz_acmX m_ahBy_acmY) ((~>) (Tuple2 a_aikY a_ahBz_acmX) m_ahBy_acmY)
-data FoldMap_6989586621679081137Sym0 :: (~>) ((~>) a_ahBz_acmX m_ahBy_acmY) ((~>) (Tuple2 a_aikY a_ahBz_acmX) m_ahBy_acmY)
+data FoldMap_6989586621679081137Sym0 @a_ahBz_acmX @m_ahBy_acmY @a_aikY :: (~>) ((~>) a_ahBz_acmX m_ahBy_acmY) ((~>) (Tuple2 a_aikY a_ahBz_acmX) m_ahBy_acmY)
where
FoldMap_6989586621679081137Sym0KindInference :: SameKind (Apply FoldMap_6989586621679081137Sym0 arg_aiyN) (FoldMap_6989586621679081137Sym1 arg_aiyN) =>
FoldMap_6989586621679081137Sym0 a6989586621679081142
@@ -1001,7 +1001,7 @@ type Foldr_6989586621679081154 :: (~>) a_ahBA_acn1 ((~>) b_ahBB_acn2 b_ahBB_acn2
type family Foldr_6989586621679081154 (a_aiz2 :: (~>) a_ahBA_acn1 ((~>) b_ahBB_acn2 b_ahBB_acn2)) (a_aiz3 :: b_ahBB_acn2) (a_aiz4 :: Tuple2 a_aikY a_ahBA_acn1) :: b_ahBB_acn2 where
Foldr_6989586621679081154 _f_6989586621679081117_aiz9 _z_6989586621679081119_aiza ('Tuple2 a_6989586621679081131_aizb a_6989586621679081133_aizc) = Apply (Apply (Apply (Apply (Apply (Apply Lambda_6989586621679081167Sym0 _f_6989586621679081117_aiz9) _z_6989586621679081119_aiza) a_6989586621679081131_aizb) a_6989586621679081133_aizc) a_6989586621679081131_aizb) (Apply (Apply _f_6989586621679081117_aiz9 a_6989586621679081133_aizc) _z_6989586621679081119_aiza)
type Foldr_6989586621679081154Sym0 :: (~>) ((~>) a_ahBA_acn1 ((~>) b_ahBB_acn2 b_ahBB_acn2)) ((~>) b_ahBB_acn2 ((~>) (Tuple2 a_aikY a_ahBA_acn1) b_ahBB_acn2))
-data Foldr_6989586621679081154Sym0 :: (~>) ((~>) a_ahBA_acn1 ((~>) b_ahBB_acn2 b_ahBB_acn2)) ((~>) b_ahBB_acn2 ((~>) (Tuple2 a_aikY a_ahBA_acn1) b_ahBB_acn2))
+data Foldr_6989586621679081154Sym0 @a_ahBA_acn1 @b_ahBB_acn2 @a_aikY :: (~>) ((~>) a_ahBA_acn1 ((~>) b_ahBB_acn2 b_ahBB_acn2)) ((~>) b_ahBB_acn2 ((~>) (Tuple2 a_aikY a_ahBA_acn1) b_ahBB_acn2))
where
Foldr_6989586621679081154Sym0KindInference :: SameKind (Apply Foldr_6989586621679081154Sym0 arg_aiz5) (Foldr_6989586621679081154Sym1 arg_aiz5) =>
Foldr_6989586621679081154Sym0 a6989586621679081160
=====================================
testsuite/tests/rename/should_compile/T23514b.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, DataKinds #-}
+module T23514b where
+
+import GHC.Types
+
+type F :: Type -> forall k. Maybe k
+type family F x @k where
+ F Int @Type = Just Bool
+ F Int = Just Either
=====================================
testsuite/tests/rename/should_compile/all.T
=====================================
@@ -213,3 +213,4 @@ test('T23240', [req_th, extra_files(['T23240_aux.hs'])], multimod_compile, ['T23
test('T23318', normal, compile, ['-Wduplicate-exports'])
test('T23434', normal, compile, [''])
test('T23510b', normal, compile, [''])
+test('T23514b', normal, compile, [''])
=====================================
testsuite/tests/rename/should_fail/T23514a.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, DataKinds #-}
+module T23514a where
+
+import GHC.Types
+
+type F :: Type -> forall k. Maybe k
+type family F x where
+ F Int @Type = Just Bool
+ F Int = Just Either
=====================================
testsuite/tests/rename/should_fail/T23514a.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T23514a.hs:9:17: error: [GHC-83865]
+ • Expected kind ‘forall k. Maybe k’,
+ but ‘Just Either’ has kind ‘Maybe (* -> * -> *)’
+ • In the type ‘Just Either’
+ In the type family declaration for ‘F’
=====================================
testsuite/tests/rename/should_fail/all.T
=====================================
@@ -200,3 +200,4 @@ test('RnStupidThetaInGadt', normal, compile_fail, [''])
test('PackageImportsDisabled', normal, compile_fail, [''])
test('ImportLookupIllegal', normal, compile_fail, [''])
test('T23510a', normal, compile_fail, [''])
+test('T23514a', normal, compile_fail, [''])
=====================================
testsuite/tests/saks/should_compile/T16724.stdout
=====================================
@@ -1,6 +1,6 @@
type T1 :: forall k (a :: k). Type
-type family T1 @k @a
+type family T1
-- Defined at T16724.hs:11:1
type T2 :: forall {k} (a :: k). Type
-type family T2 @{k} @a
+type family T2
-- Defined at T16724.hs:15:1
=====================================
testsuite/tests/saks/should_compile/saks020.hs
=====================================
@@ -6,4 +6,4 @@ module SAKS_020 where
import Data.Kind (Type)
type T :: forall k. k -> forall j. j -> Type
-data T (x :: hk) :: hj -> Type
+data T (x :: hk) @hj :: hj -> Type
=====================================
testsuite/tests/saks/should_compile/saks030.hs
=====================================
@@ -10,7 +10,7 @@ import Data.Type.Equality
type T1 :: forall k (a :: k). Bool
type T2 :: k -> Bool
-type family T1 where
+type family T1 @k @a where
T1 @Bool @True = False
T1 @Bool @False = True
=====================================
testsuite/tests/saks/should_compile/saks032.hs
=====================================
@@ -18,4 +18,4 @@ type F1 :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
type family F1 a b
type F2 :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
-type family F2 a b :: forall r2. (r1, r2) -> Type
+type family F2 a b @r1 :: forall r2. (r1, r2) -> Type
=====================================
testsuite/tests/saks/should_fail/T18863b.stderr
=====================================
@@ -1,5 +1,5 @@
T18863b.hs:9:1: error: [GHC-83865]
• Couldn't match expected kind: forall i -> i -> *
- with actual kind: i -> *
+ with actual kind: forall i. i -> *
• In the data type declaration for ‘IDb’
=====================================
testsuite/tests/th/CodeQ_HKD.hs
=====================================
@@ -0,0 +1,13 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module CodeQ_HKD where
+import GHC.Exts
+import Data.Kind
+import Language.Haskell.TH hiding (Type)
+
+data T (f :: forall r . (TYPE r) -> Type) = MkT (f Int) (f Int#)
+
+
+tcodeq :: T CodeQ
+tcodeq = MkT [||5||] [||5#||]
=====================================
testsuite/tests/th/all.T
=====================================
@@ -576,3 +576,4 @@ test('T21050', normal, compile_fail, [''])
test('T22559a', normal, compile_fail, [''])
test('T22559b', normal, compile_fail, [''])
test('T22559c', normal, compile_fail, [''])
+test('CodeQ_HKD', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T18640a.hs
=====================================
@@ -8,4 +8,4 @@ module T18640a where
import Data.Kind
type F2 :: forall a b. Type -> a
-type family F2 :: forall b. Type -> Type where
+type family F2 @a :: forall b. Type -> Type where
=====================================
testsuite/tests/typecheck/should_fail/T18640a.stderr
=====================================
@@ -5,5 +5,5 @@ T18640a.hs:11:1: error: [GHC-25897]
Actual: forall (b :: k). * -> a
‘a’ is a rigid type variable bound by
the type family declaration for ‘F2’
- at T18640a.hs:10:19
+ at T18640a.hs:11:17
• In the type family declaration for ‘F2’
=====================================
testsuite/tests/typecheck/should_fail/T18640c.hs
=====================================
@@ -11,4 +11,4 @@ type F1 :: forall k -> Type
type family F1 k :: Type
type F2 :: forall x. forall k -> x
-type F2 = F1
+type F2 k = F1 k
=====================================
testsuite/tests/typecheck/should_fail/T18640c.stderr
=====================================
@@ -1,10 +1,8 @@
-T18640c.hs:14:11: error: [GHC-25897]
- • Couldn't match kind ‘x’ with ‘*’
- Expected kind ‘forall (k1 :: k) -> x’,
- but ‘F1’ has kind ‘forall (k1 :: k) -> *’
+T18640c.hs:14:13: error: [GHC-25897]
+ • Expected kind ‘x’, but ‘F1 k’ has kind ‘*’
‘x’ is a rigid type variable bound by
the type synonym declaration for ‘F2’
at T18640c.hs:13:19
- • In the type ‘F1’
+ • In the type ‘F1 k’
In the type declaration for ‘F2’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/29e2c8a4c4ec582a367096ec48cf4d36f8e1507d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/29e2c8a4c4ec582a367096ec48cf4d36f8e1507d
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/20230615/e650955e/attachment-0001.html>
More information about the ghc-commits
mailing list