[Git][ghc/ghc][wip/sand-witch/DIB-INSTANCES] Remove arity inference in type declarations (#23514)

Andrei Borzenkov (@sand-witch) gitlab at gitlab.haskell.org
Fri Jun 16 08:39:20 UTC 2023



Andrei Borzenkov pushed to branch wip/sand-witch/DIB-INSTANCES at Glasgow Haskell Compiler / GHC


Commits:
7cfbb301 by Andrei Borzenkov at 2023-06-16T12:39:05+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/Iface/Syntax.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Splice.hs
- libraries/template-haskell/Language/Haskell/TH/Syntax.hs
- libraries/template-haskell/changelog.md
- testsuite/tests/perf/compiler/CoOpt_Singletons.hs
- 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/th/CodeQ_HKD.hs
- testsuite/tests/th/all.T
- + testsuite/tests/typecheck/should_compile/T23514b.hs
- + testsuite/tests/typecheck/should_compile/T23514c.hs
- testsuite/tests/typecheck/should_compile/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
- + testsuite/tests/typecheck/should_fail/T23514a.hs
- + testsuite/tests/typecheck/should_fail/T23514a.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
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,30 @@ 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" $
+                    vcat [ text "excess_sig_tcbs" <+> ppr excess_sig_tcbs
+                         , text "ctx_k" <+> ppr ctx_k
+                         , 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
-                              ; discardResult (unifyKind Nothing sig_res_kind' res_ki) }
+                      _ -> do
+                        res_ki <- newExpectedKind ctx_k
+                        check_exp_res_ki 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)
           }
 
@@ -2641,6 +2634,22 @@ kcCheckDeclHeader_sig sig_kind name flav
           ]
         ; return tc }
 
+-- | 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
+
+      -- 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
+
 matchUpSigWithDecl
   :: Name                        -- Name of the type constructor for error messages
   -> [TcTyConBinder]             -- TcTyConBinders (with skolem TcTyVars) from the separate kind signature
@@ -2738,8 +2747,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 +2789,43 @@ 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:
+Consider
 
-    type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
-    type family F a b
+  type F0 :: forall k. k -> k -> Type
+  type family F0
 
-    type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
-    type family G a b :: forall r2. (r1, r2) -> Type
+  type F1 :: forall k. k -> k -> Type
+  type family F1 @k
 
-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)))]
+  type F2a :: forall k. k -> k -> Type
+  type family F2a @k a
 
-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)))]
+  type F2b :: forall k. k -> k -> Type
+  type family F2b a
 
-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.
+  type F3 :: forall k. k -> k -> Type
+  type family F3 a b
 
-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'.
+All five 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.
 
-    res_ki  =  forall    r2. (r1, r2) -> Type
-    kisig   =  forall k1 k2. (k1, k2) -> Type
-                     ^^^
-                     split off this one.
+The arity is not determined by the kind signature (all five have the same signature).
+Rather, it is determined by the declaration of the family:
+* `F0` has arity 0.
+* `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 resulting arity of G is 3+1=4.
+The matching-up of kind signature with the declaration itself is done by
+`matchUpWithSigDecl`.
 
 Note [discardResult in kcCheckDeclHeader_sig]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2949,6 +2916,12 @@ data ContextKind = TheKind TcKind   -- ^ a specific kind
                  | AnyKind        -- ^ any kind will do
                  | OpenKind       -- ^ something of the form @TYPE _@
 
+-- debug only
+instance Outputable ContextKind where
+  ppr AnyKind = text "AnyKind"
+  ppr OpenKind = text "OpenKind"
+  ppr (TheKind k) = text "TheKind" <+> ppr k
+
 -----------------------
 newExpectedKind :: ContextKind -> TcM TcKind
 newExpectedKind (TheKind k)   = return k


=====================================
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,13 @@ 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
+  -- The nested `forall` makes it possible to assign the arity of 0 to
+  --   type CodeQ = Code Q
+#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


=====================================
libraries/template-haskell/changelog.md
=====================================
@@ -1,10 +1,15 @@
 # Changelog for [`template-haskell` package](http://hackage.haskell.org/package/template-haskell)
 
+## 2.22.0.0
+
+  * The kind of `Code` was changed from `forall r. (Type -> Type) -> TYPE r -> Type`
+    to `(Type -> Type) -> forall r. TYPE r -> Type`. This enables higher-kinded usage.
+
 ## 2.21.0.0
 
   * Record fields now belong to separate `NameSpace`s, keyed by the parent of
     the record field. This is the name of the first constructor of the parent type,
-    even if this constructor does not have the field in question.  
+    even if this constructor does not have the field in question.
 
     This change enables TemplateHaskell support for `DuplicateRecordFields`.
 
@@ -21,7 +26,7 @@
 
 ## 2.20.0.0
 
-  * The `Ppr.pprInfixT` function has gained a `Precedence` argument. 
+  * The `Ppr.pprInfixT` function has gained a `Precedence` argument.
   * The values of named precedence levels like `Ppr.appPrec` have changed.
 
   * Add `TypeDataD` constructor to the `Dec` type for `type data`


=====================================
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) =
@@ -386,7 +386,7 @@ 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)
@@ -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
@@ -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


=====================================
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/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_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/typecheck/should_compile/T23514c.hs
=====================================
@@ -0,0 +1,21 @@
+module T23514c where
+import Data.Kind
+
+
+type P1 :: forall k (a :: k) . k -> Type
+data P1 :: k -> Type
+
+type P2 :: forall k (a :: k) . k -> Type
+data P2 @k :: k -> Type
+
+type P3 :: forall k (a :: k) . k -> Type
+data P3 @k @a :: k -> Type
+
+type P4 :: forall k (a :: k) . k -> Type
+data P4 :: forall k (a :: k) . k -> Type
+
+type P5 :: forall k (a :: k) . k -> Type
+data P5 :: forall a . k -> Type
+
+type P6 :: forall k (a :: k) . k -> Type
+data P6 @k :: forall a . k -> Type


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -880,3 +880,5 @@ test('T22560b', normal, compile, [''])
 test('T22560c', normal, compile, [''])
 test('T22560d', extra_files(['T22560d.hs']), ghci_script, ['T22560d.script'])
 test('T22560e', normal, compile, [''])
+test('T23514b', normal, compile, [''])
+test('T23514c', 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’


=====================================
testsuite/tests/typecheck/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/typecheck/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/typecheck/should_fail/all.T
=====================================
@@ -690,3 +690,4 @@ 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, [''])
+test('T23514a', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7cfbb301a3d8cd2af5e5cc801ae5933ccd198bf4

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7cfbb301a3d8cd2af5e5cc801ae5933ccd198bf4
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/20230616/447f84e2/attachment-0001.html>


More information about the ghc-commits mailing list