diff options
| author | Vladislav Zavialov <vlad.z.4096@gmail.com> | 2019-05-31 15:03:37 +0300 |
|---|---|---|
| committer | Vladislav Zavialov <vlad.z.4096@gmail.com> | 2019-09-28 14:33:10 +0300 |
| commit | 8a85b4b0cc7643637d3b32a72a9775664d1ebdec (patch) | |
| tree | df372ad3d8aa458ff4b53aa27ca7995b781c9376 | |
| parent | 6f9fa0be8d43a7c9618f6e27e3190dc08bf86bfa (diff) | |
| download | haskell-wip/testsuite-no-cusks.tar.gz | |
Disable CUSKs by defaultwip/testsuite-no-cusks
119 files changed, 902 insertions, 528 deletions
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index f809bc330f..42c719c0d5 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -2311,7 +2311,6 @@ languageExtensions (Just Haskell98) = [LangExt.ImplicitPrelude, -- See Note [When is StarIsType enabled] LangExt.StarIsType, - LangExt.CUSKs, LangExt.MonomorphismRestriction, LangExt.NPlusKPatterns, LangExt.DatatypeContexts, @@ -2328,7 +2327,6 @@ languageExtensions (Just Haskell2010) = [LangExt.ImplicitPrelude, -- See Note [When is StarIsType enabled] LangExt.StarIsType, - LangExt.CUSKs, LangExt.MonomorphismRestriction, LangExt.DatatypeContexts, LangExt.TraditionalRecordSyntax, @@ -4417,7 +4415,8 @@ xFlagsDeps = [ flagSpec "BinaryLiterals" LangExt.BinaryLiterals, flagSpec "CApiFFI" LangExt.CApiFFI, flagSpec "CPP" LangExt.Cpp, - flagSpec "CUSKs" LangExt.CUSKs, + depFlagSpec "CUSKs" LangExt.CUSKs + "Use standalone kind signatures instead", flagSpec "ConstrainedClassMethods" LangExt.ConstrainedClassMethods, flagSpec "ConstraintKinds" LangExt.ConstraintKinds, flagSpec "DataKinds" LangExt.DataKinds, diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs index f9c9cc23da..e900546671 100644 --- a/libraries/base/Data/Type/Equality.hs +++ b/libraries/base/Data/Type/Equality.hs @@ -12,6 +12,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE Trustworthy #-} ----------------------------------------------------------------------------- @@ -122,7 +123,8 @@ deriving instance a ~ b => Bounded (a :~: b) -- inhabited by a terminating value if and only if @a@ is the same type as @b@. -- -- @since 4.10.0.0 -data (a :: k1) :~~: (b :: k2) where +type (:~~:) :: k1 -> k2 -> Type +data a :~~: b where HRefl :: a :~~: a -- | @since 4.10.0.0 @@ -163,7 +165,8 @@ instance TestEquality ((:~~:) a) where infix 4 == -- | A type family to compute Boolean equality. -type family (a :: k) == (b :: k) :: Bool where +type (==) :: k -> k -> Bool +type family a == b where f a == g b = f == g && a == b a == a = 'True _ == _ = 'False diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs index 5c087272fa..6135487e6e 100644 --- a/libraries/base/Data/Typeable/Internal.hs +++ b/libraries/base/Data/Typeable/Internal.hs @@ -18,6 +18,7 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} ----------------------------------------------------------------------------- -- | @@ -178,7 +179,8 @@ rnfTyCon (TyCon _ _ m n _ k) = rnfModule m `seq` rnfTrName n `seq` rnfKindRep k -- | A concrete representation of a (monomorphic) type. -- 'TypeRep' supports reasonably efficient equality. -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where -- The TypeRep of Type. See Note [Kind caching], Wrinkle 2 TrType :: TypeRep Type TrTyCon :: { -- See Note [TypeRep fingerprints] diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/dependent/should_compile/Dep2.hs index 34be3cffc6..ca84c79fae 100644 --- a/testsuite/tests/dependent/should_compile/Dep2.hs +++ b/testsuite/tests/dependent/should_compile/Dep2.hs @@ -1,7 +1,10 @@ -{-# LANGUAGE PolyKinds, GADTs #-} +{-# LANGUAGE PolyKinds, GADTs, StandaloneKindSignatures #-} module Dep2 where -data G (a :: k) where +import Data.Kind (Type) + +type G :: k -> Type +data G a where G1 :: G Int G2 :: G Maybe diff --git a/testsuite/tests/dependent/should_compile/DkNameRes.hs b/testsuite/tests/dependent/should_compile/DkNameRes.hs index 4110b33882..bc468f872d 100644 --- a/testsuite/tests/dependent/should_compile/DkNameRes.hs +++ b/testsuite/tests/dependent/should_compile/DkNameRes.hs @@ -1,9 +1,10 @@ -{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneKindSignatures #-} module DkNameRes where import Data.Proxy import Data.Kind -type family IfK (e :: Proxy (j :: Bool)) :: Type where +type IfK :: Proxy (j :: Bool) -> Type +type family IfK e where IfK (_ :: Proxy True) = () diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs index d24502bc71..24ccf84acc 100644 --- a/testsuite/tests/dependent/should_compile/KindEqualities2.hs +++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll, - TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-} + TemplateHaskell, UndecidableInstances, ScopedTypeVariables, + StandaloneKindSignatures #-} module KindEqualities2 where @@ -15,7 +16,8 @@ data Ty :: Kind -> Type where TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2 -data TyRep (k :: Kind) (t :: Ty k) where +type TyRep :: forall (k :: Kind) -> Ty k -> Type +data TyRep k t where TyInt :: TyRep Star TInt TyBool :: TyRep Star TBool TyMaybe :: TyRep (Arr Star Star) TMaybe diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs index b048a49e44..eb20b62bcd 100644 --- a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs +++ b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-} module RaeBlogPost where @@ -22,7 +23,8 @@ data E :: D c -> Type -- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> Type -- a kind-indexed GADT -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where TInt :: TypeRep Int TMaybe :: TypeRep Maybe TApp :: TypeRep a -> TypeRep b -> TypeRep (a b) @@ -36,13 +38,15 @@ type family a + b where 'Zero + b = b ('Succ a) + b = 'Succ (a + b) -data Vec :: Type -> Nat -> Type where +type Vec :: Type -> Nat -> Type +data Vec a n where Nil :: Vec a 'Zero (:>) :: a -> Vec a n -> Vec a ('Succ n) infixr 5 :> -- promoted GADT, and using + as a "kind family": -type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where +type (++) :: Vec a n -> Vec a m -> Vec a (n + m) +type family x ++ y where 'Nil ++ y = y (h ':> t) ++ y = h ':> (t ++ y) diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs index 6c74e10a7c..c2173d38f5 100644 --- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs +++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs @@ -6,7 +6,7 @@ DataKinds, PolyKinds , ConstraintKinds, UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, StandaloneDeriving, InstanceSigs, - RankNTypes, UndecidableSuperClasses #-} + RankNTypes, UndecidableSuperClasses, StandaloneKindSignatures #-} module RaeJobTalk where @@ -24,7 +24,8 @@ import Data.Maybe -- Utilities -- Heterogeneous propositional equality -data (a :: k1) :~~: (b :: k2) where +type (:~~:) :: k1 -> k2 -> Type +data a :~~: b where HRefl :: a :~~: a -- Type-level inequality @@ -73,7 +74,8 @@ Nil %:++ x = x -- Type-indexed type representations -- Based on "A reflection on types" -data TyCon (a :: k) where +type TyCon :: k -> Type +data TyCon a where Int :: TyCon Int Bool :: TyCon Bool Char :: TyCon Char @@ -103,7 +105,8 @@ type family Primitive (a :: k) :: Constraint where Primitive (_ _) = ('False ~ 'True) Primitive _ = (() :: Constraint) -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where TyCon :: forall k (a :: k). (Primitive a, Typeable k) => TyCon a -> TypeRep a TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b) diff --git a/testsuite/tests/dependent/should_compile/T11711.hs b/testsuite/tests/dependent/should_compile/T11711.hs index 814b2a4a68..ec33ceeb66 100644 --- a/testsuite/tests/dependent/should_compile/T11711.hs +++ b/testsuite/tests/dependent/should_compile/T11711.hs @@ -7,22 +7,26 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T11711 where -import Data.Kind (Type) +import Data.Kind -data (:~~:) (a :: k1) (b :: k2) where +type (:~~:) :: k1 -> k2 -> Type +data (:~~:) a b where HRefl :: a :~~: a -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where TrTyCon :: String -> TypeRep k -> TypeRep (a :: k) TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep (a :: k1 -> k2) -> TypeRep (b :: k1) -> TypeRep (a b) -class Typeable (a :: k) where +type Typeable :: k -> Constraint +class Typeable a where typeRep :: TypeRep a data SomeTypeRep where diff --git a/testsuite/tests/dependent/should_compile/T12176.hs b/testsuite/tests/dependent/should_compile/T12176.hs index a11c151567..8c73918905 100644 --- a/testsuite/tests/dependent/should_compile/T12176.hs +++ b/testsuite/tests/dependent/should_compile/T12176.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies #-} +{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, + StandaloneKindSignatures #-} module T12176 where @@ -10,7 +11,8 @@ data Proxy :: forall k. k -> Type where data X where MkX :: forall (k :: Type) (a :: k). Proxy a -> X -type Expr = (MkX :: forall (a :: Bool). Proxy a -> X) +type Expr :: forall (a :: Bool). Proxy a -> X +type Expr = MkX :: forall (a :: Bool). Proxy a -> X type family Foo (x :: forall (a :: k). Proxy a -> X) where Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k) diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs index b4bcdb9d62..81e80eec37 100644 --- a/testsuite/tests/dependent/should_compile/T12442.hs +++ b/testsuite/tests/dependent/should_compile/T12442.hs @@ -1,7 +1,8 @@ -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr {-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators, - TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes #-} + TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes, + StandaloneKindSignatures #-} module T12442 where @@ -33,9 +34,15 @@ data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where data instance Sing (elem :: EffElem x a xs) where SHere :: Sing Here -type family UpdateResTy (b :: Type) (t :: Type) - (xs :: [EFFECT]) (elem :: EffElem e a xs) - (thing :: e @@ a @@ b @@ t) :: [EFFECT] where +type UpdateResTy :: + forall a e. + forall (b :: Type) -> + forall (t :: Type) -> + forall (xs :: [EFFECT]) -> + EffElem e a xs -> + (e @@ a @@ b @@ t) -> + [EFFECT] +type family UpdateResTy b t xs elem thing where UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs index 1d6b72491e..b743568673 100644 --- a/testsuite/tests/dependent/should_compile/T14066a.hs +++ b/testsuite/tests/dependent/should_compile/T14066a.hs @@ -1,5 +1,6 @@ {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs, - UndecidableInstances, RankNTypes, ScopedTypeVariables #-} + UndecidableInstances, RankNTypes, ScopedTypeVariables, + StandaloneKindSignatures #-} module T14066a where @@ -31,7 +32,8 @@ type family G x a where -- this last example just checks that GADT pattern-matching on kinds still works. -- nothing new here. -data T (a :: k) where +type T :: k -> Type +data T a where MkT :: T (a :: Type -> Type) data S (a :: Type -> Type) where @@ -53,9 +55,12 @@ type P k a = Proxy (a :: k) -- Naively, we don't know about c's kind early enough. data SameKind :: forall k. k -> k -> Type -type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where + +type IfK :: Proxy (j :: Bool) -> m -> n -> If j m n +type family IfK e f g where IfK (_ :: Proxy True) f _ = f IfK (_ :: Proxy False) _ g = g + x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True)) x _ = Proxy diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr index 906695f3f7..a393e474df 100644 --- a/testsuite/tests/dependent/should_compile/T14066a.stderr +++ b/testsuite/tests/dependent/should_compile/T14066a.stderr @@ -1,5 +1,5 @@ -T14066a.hs:13:3: warning: +T14066a.hs:14:3: warning: Type family instance equation is overlapped: forall c d (x :: c) (y :: d). - Bar x y = Bool -- Defined at T14066a.hs:13:3 + Bar x y = Bool -- Defined at T14066a.hs:14:3 diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs index 133a9e6a44..b6b1f48a85 100644 --- a/testsuite/tests/dependent/should_compile/T14556.hs +++ b/testsuite/tests/dependent/should_compile/T14556.hs @@ -1,5 +1,6 @@ {-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds, - TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} + TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables, + StandaloneKindSignatures #-} module T14556 where @@ -9,8 +10,8 @@ import Data.Proxy data Fn a b where IdSym :: Fn Type Type -type family - (@@) (f::Fn k k') (a::k)::k' where +type (@@) :: Fn k k' -> k -> k' +type family f @@ a where IdSym @@ a = a data KIND = X | FNARR KIND KIND @@ -19,19 +20,20 @@ data TY :: KIND -> Type where ID :: TY (FNARR X X) FNAPP :: TY (FNARR k k') -> TY k -> TY k' -data TyRep (kind::KIND) :: TY kind -> Type where +type TyRep :: forall (kind::KIND) -> TY kind -> Type +data TyRep k t where TID :: TyRep (FNARR X X) ID TFnApp :: TyRep (FNARR k k') f -> TyRep k a -> TyRep k' (FNAPP f a) -type family - IK (kind::KIND) :: Type where +type IK :: KIND -> Type +type family IK kind where IK X = Type IK (FNARR k k') = Fn (IK k) (IK k') -type family - IT (ty::TY kind) :: IK kind where +type IT :: TY kind -> IK kind +type family IT ty where IT ID = IdSym IT (FNAPP f x) = IT f @@ IT x diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs index bf3d5c488a..833f7d82c1 100644 --- a/testsuite/tests/dependent/should_compile/T14749.hs +++ b/testsuite/tests/dependent/should_compile/T14749.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, PolyKinds, TypeFamilyDependencies #-} +{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, PolyKinds, + ExplicitForAll, TypeFamilyDependencies, StandaloneKindSignatures #-} module T14749 where @@ -14,11 +15,13 @@ type family IK (k :: KIND) = (res :: Type) where IK STAR = Type IK (a:>b) = IK a -> IK b -type family I (t :: Ty k) = (res :: IK k) where +type I :: Ty k -> IK k +type family I t = res where I TMaybe = Maybe I (TApp f a) = (I f) (I a) -data TyRep (k :: KIND) (t :: Ty k) where +type TyRep :: forall (k :: KIND) -> Ty k -> Type +data TyRep k t where TyMaybe :: TyRep (STAR:>STAR) TMaybe TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x) diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs index 138ab486ca..bdffcf758f 100644 --- a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs +++ b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs @@ -4,6 +4,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE UnicodeSyntax #-} module T16326_Compile1 where @@ -20,14 +21,15 @@ type DComp a (x :: a) = f (g x) --- Ensure that ElimList has a CUSK, beuas it is --- is used polymorphically its RHS (c.f. #16344) -type family ElimList (a :: Type) - (p :: [a] -> Type) - (s :: [a]) - (pNil :: p '[]) - (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)) - :: p s where + +type ElimList :: + forall (a :: Type) + (p :: [a] -> Type) + (s :: [a]) + (pNil :: p '[]) + (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)) + -> p s +type family ElimList a p s pNil pCons where forall a p pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)). ElimList a p '[] pNil pCons = pNil diff --git a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs index 0e2f0c7744..f698d5d687 100644 --- a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs +++ b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs @@ -1,5 +1,5 @@ {-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude, - TypeOperators, TypeFamilies #-} + TypeOperators, TypeFamilies, StandaloneKindSignatures #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} module TypeLevelVec where @@ -20,7 +20,8 @@ data Vec ∷ ℕ → Type → Type where (:>) ∷ a → Vec n a → Vec (S n) a infixr 8 :> -type family (x ∷ Vec n a) ++ (y ∷ Vec m a) ∷ Vec (n + m) a where +type (++) :: Vec n a -> Vec m a -> Vec (n + m) a +type family x ++ y where Nil ++ y = y (x :> xs) ++ y = x :> (xs ++ y) infixl 5 ++ diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs index 1188bf17d4..01e5c5c615 100644 --- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs +++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs @@ -7,7 +7,7 @@ Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -} {-# LANGUAGE RankNTypes, PolyKinds, TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances, UndecidableInstances, RebindableSyntax, - DataKinds, MagicHash #-} + DataKinds, MagicHash, StandaloneKindSignatures #-} {-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-} {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} -- Because we define a local Typeable class and have @@ -185,7 +185,8 @@ dynFst (Dyn (rpab :: TypeRep pab) (x :: pab)) eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b) -data (a :: k1) :~: (b :: k2) where +type (:~:) :: k1 -> k2 -> Type +data a :~: b where Refl :: forall k (a :: k). a :~: a castDance :: (Typeable a, Typeable b) => a -> Maybe b @@ -235,7 +236,8 @@ data OrderingT a b where EQT :: OrderingT t t GTT :: OrderingT a b -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b) TrTyCon :: TyCon -> TypeRep k -> TypeRep (a :: k) diff --git a/testsuite/tests/dependent/should_compile/mkGADTVars.hs b/testsuite/tests/dependent/should_compile/mkGADTVars.hs index 13ac0248bf..ecedbedb15 100644 --- a/testsuite/tests/dependent/should_compile/mkGADTVars.hs +++ b/testsuite/tests/dependent/should_compile/mkGADTVars.hs @@ -1,9 +1,10 @@ -{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-} +{-# LANGUAGE GADTs, PolyKinds, RankNTypes, StandaloneKindSignatures #-} module GADTVars where import Data.Kind import Data.Proxy -data T (k1 :: Type) (k2 :: Type) (a :: k2) (b :: k2) where +type T :: Type -> forall (k2 :: Type) -> k2 -> k2 -> Type +data T k1 k2 a b where MkT :: T x1 Type (Proxy (y :: x1), z) z diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr index 3c90f5444b..8ac4be8c0c 100644 --- a/testsuite/tests/dependent/should_fail/SelfDep.stderr +++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr @@ -3,4 +3,3 @@ SelfDep.hs:5:11: error: • Type constructor ‘T’ cannot be used here (it is defined and used in the same recursive group) • In the kind ‘T -> *’ - In the data type declaration for ‘T’ diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs index a8fa34d4a0..ff85c333c3 100644 --- a/testsuite/tests/dependent/should_fail/T13601.hs +++ b/testsuite/tests/dependent/should_fail/T13601.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneKindSignatures, + FlexibleContexts, UndecidableSuperClasses #-} import GHC.Exts import Prelude (Bool(True,False),Integer,Ordering,undefined) @@ -15,25 +16,32 @@ type family -- Rep PtrRepUnlifted = IntRep -- Rep PtrRepLifted = PtrRepLifted +type Eq :: TYPE rep -> Constraint class Boolean (Logic a) => Eq (a :: TYPE rep) where type Logic (a :: TYPE rep) :: TYPE (Rep rep) (==) :: a -> a -> Logic a +type POrd :: TYPE rep -> Constraint class Eq a => POrd (a :: TYPE rep) where inf :: a -> a -> a +type MinBound :: TYPE rep -> Constraint class POrd a => MinBound (a :: TYPE rep) where minBound :: () -> a +type Lattice :: TYPE rep -> Constraint class POrd a => Lattice (a :: TYPE rep) where sup :: a -> a -> a +type Bounded :: TYPE rep -> Constraint class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where maxBound :: () -> a +type Complemented :: TYPE rep -> Constraint class Bounded a => Complemented (a :: TYPE rep) where not :: a -> a +type Heyting :: TYPE rep -> Constraint class Bounded a => Heyting (a :: TYPE rep) where infixr 3 ==> (==>) :: a -> a -> a diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr index bc2877c3e6..486d5a17cc 100644 --- a/testsuite/tests/dependent/should_fail/T13601.stderr +++ b/testsuite/tests/dependent/should_fail/T13601.stderr @@ -1,5 +1,5 @@ -T13601.hs:18:16: error: +T13601.hs:20:16: error: • Expected a type, but ‘Logic a’ has kind ‘TYPE (Rep rep)’ • In the first argument of ‘Boolean’, namely ‘(Logic a)’ In the class declaration for ‘Eq’ diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs index 78e09f5ef1..3afcd6c24b 100644 --- a/testsuite/tests/dependent/should_fail/T13780c.hs +++ b/testsuite/tests/dependent/should_fail/T13780c.hs @@ -1,12 +1,19 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds, PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures, ExplicitForAll #-} module T13780c where import Data.Kind import T13780b -type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b) - (pFalse :: p False) (pTrue :: p True) :: p b where +type ElimBool :: + forall (p :: Bool -> Type) -> + forall (b :: Bool) -> + Sing b -> + p False -> + p True -> + p b +type family ElimBool p b s pFalse pTrue where ElimBool _ _ SFalse pFalse _ = pFalse ElimBool _ _ STrue _ pTrue = pTrue diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr index 9a196f4bd7..843b8a8232 100644 --- a/testsuite/tests/dependent/should_fail/T13780c.stderr +++ b/testsuite/tests/dependent/should_fail/T13780c.stderr @@ -1,13 +1,13 @@ [1 of 2] Compiling T13780b ( T13780b.hs, T13780b.o ) [2 of 2] Compiling T13780c ( T13780c.hs, T13780c.o ) -T13780c.hs:11:16: error: +T13780c.hs:18:16: error: • Data constructor ‘SFalse’ cannot be used here (it comes from a data family instance) • In the third argument of ‘ElimBool’, namely ‘SFalse’ In the type family declaration for ‘ElimBool’ -T13780c.hs:12:16: error: +T13780c.hs:19:16: error: • Data constructor ‘STrue’ cannot be used here (it comes from a data family instance) • In the third argument of ‘ElimBool’, namely ‘STrue’ diff --git a/testsuite/tests/dependent/should_fail/T15380.hs b/testsuite/tests/dependent/should_fail/T15380.hs index 32ea8ec724..c896ee5474 100644 --- a/testsuite/tests/dependent/should_fail/T15380.hs +++ b/testsuite/tests/dependent/should_fail/T15380.hs @@ -1,6 +1,8 @@ {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T15380 where @@ -12,7 +14,8 @@ class Generic a where class PGeneric a where type To a (x :: Rep a) :: a -type family MDefault (x :: a) :: a where +type MDefault :: a -> a +type family MDefault x where MDefault x = To (M x) class C a where diff --git a/testsuite/tests/dependent/should_fail/T15380.stderr b/testsuite/tests/dependent/should_fail/T15380.stderr index 9b30078c64..1ec63b7f29 100644 --- a/testsuite/tests/dependent/should_fail/T15380.stderr +++ b/testsuite/tests/dependent/should_fail/T15380.stderr @@ -1,5 +1,5 @@ -T15380.hs:16:16: error: +T15380.hs:19:16: error: • Expecting one more argument to ‘To (M x)’ Expected a type, but ‘To (M x)’ has kind ‘Rep (M x) -> M x’ • In the type ‘To (M x)’ diff --git a/testsuite/tests/ghci/scripts/T7939.hs b/testsuite/tests/ghci/scripts/T7939.hs index 04a1f1a623..e27c39b84b 100644 --- a/testsuite/tests/ghci/scripts/T7939.hs +++ b/testsuite/tests/ghci/scripts/T7939.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators #-} +{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures #-} module T7939 where import Data.Kind (Type) @@ -22,6 +22,7 @@ type family K a where K '[] = Nothing K (h ': t) = Just h -type family L (a :: k) (b :: Type) :: k where +type L :: k -> Type -> k +type family L a b where L Int Int = Bool L Maybe Bool = IO diff --git a/testsuite/tests/indexed-types/should_compile/T14554.hs b/testsuite/tests/indexed-types/should_compile/T14554.hs index 6049b1934e..5ed70e026f 100644 --- a/testsuite/tests/indexed-types/should_compile/T14554.hs +++ b/testsuite/tests/indexed-types/should_compile/T14554.hs @@ -1,5 +1,6 @@ {-# Language UndecidableInstances, DataKinds, TypeOperators, TypeFamilies, - PolyKinds, GADTs, LambdaCase, ScopedTypeVariables #-} + PolyKinds, GADTs, LambdaCase, ScopedTypeVariables, + StandaloneKindSignatures #-} module T14554 where @@ -16,17 +17,20 @@ data TY :: KIND -> Type where ID :: TY (FNARR X X) FNAPP :: TY (FNARR k k') -> TY k -> TY k' -data TyRep (kind::KIND) :: TY kind -> Type where +type TyRep :: forall (kind::KIND) -> TY kind -> Type +data TyRep k t where TID :: TyRep (FNARR X X) ID TFnApp :: TyRep (FNARR k k') f -> TyRep k a -> TyRep k' (FNAPP f a) -type family IK (kind::KIND) :: Type where +type IK :: KIND -> Type +type family IK kind where IK X = Type IK (FNARR k k') = IK k ~> IK k' -type family IT (ty::TY kind) :: IK kind +type IT :: TY kind -> IK kind +type family IT ty zero :: TyRep X a -> IT a zero x = case x of diff --git a/testsuite/tests/indexed-types/should_compile/T15122.hs b/testsuite/tests/indexed-types/should_compile/T15122.hs index c05bd3a8a0..f56c49b934 100644 --- a/testsuite/tests/indexed-types/should_compile/T15122.hs +++ b/testsuite/tests/indexed-types/should_compile/T15122.hs @@ -1,12 +1,14 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T15122 where import Data.Kind import Data.Proxy -data IsStar (a :: k) where +type IsStar :: k -> Type +data IsStar a where IsStar :: IsStar (a :: Type) type family F (a :: k) :: k diff --git a/testsuite/tests/indexed-types/should_compile/T15352.hs b/testsuite/tests/indexed-types/should_compile/T15352.hs index d83512f085..802f42e898 100644 --- a/testsuite/tests/indexed-types/should_compile/T15352.hs +++ b/testsuite/tests/indexed-types/should_compile/T15352.hs @@ -1,6 +1,9 @@ -{-# LANGUAGE TypeInType #-} -- or PolyKinds +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T15352 where @@ -14,18 +17,17 @@ type Hom k = k -> k -> Type type family Ob (p :: Hom k) :: k -> Constraint +type Functor' :: + forall i j. + (i -> Constraint) -> Hom i -> Hom i -> + (j -> Constraint) -> Hom j -> Hom j -> + (i -> j) -> Constraint class ( obP ~ Ob p , opP ~ Dom p , obQ ~ Ob q , opQ ~ Dom q , p ~ Dom f , q ~ Cod f - ) => Functor' (obP :: i -> Constraint) - (opP :: Hom i) - (p :: Hom i) - (obQ :: j -> Constraint) - (opQ :: Hom j) - (q :: Hom j) - (f :: i -> j) where + ) => Functor' obP opP p obQ opQ q f where type Dom f :: Hom i type Cod f :: Hom j diff --git a/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs b/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs index 74dee38ac4..fd6a650eba 100644 --- a/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs +++ b/testsuite/tests/indexed-types/should_compile/T16356_Compile1.hs @@ -2,13 +2,15 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T16356_Compile1 where import Data.Kind (Type) data B (a :: k) -type family FClosed :: k -> Type where +type FClosed :: k -> Type +type family FClosed where FClosed @k = B @k type family FOpen :: k -> Type diff --git a/testsuite/tests/indexed-types/should_compile/T17008b.hs b/testsuite/tests/indexed-types/should_compile/T17008b.hs index 25763684e4..dc10afdf09 100644 --- a/testsuite/tests/indexed-types/should_compile/T17008b.hs +++ b/testsuite/tests/indexed-types/should_compile/T17008b.hs @@ -1,6 +1,9 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} + module T17008b where import Data.Kind @@ -8,19 +11,27 @@ import Data.Kind type family ConstType1 (a :: Type) :: Type where ConstType1 _ = Type -type family F1 (x :: ConstType1 a) :: Type where +type F1 :: ConstType1 a -> Type +type family F1 x where F1 @a (x :: ConstType1 a) = a -type family F2 (x :: ConstType1 a) :: ConstType1 a where + +type F2 :: ConstType1 a -> ConstType1 a +type family F2 x where F2 @a (x :: ConstType1 a) = x :: ConstType1 a + type F3 (x :: ConstType1 a) = a type F4 (x :: ConstType1 a) = x :: ConstType1 a type ConstType2 (a :: Type) = Type -type family G1 (x :: ConstType2 a) :: Type where +type G1 :: ConstType2 a -> Type +type family G1 x where G1 @a (x :: ConstType2 a) = a -type family G2 (x :: ConstType2 a) :: ConstType2 a where + +type G2 :: ConstType2 a -> ConstType2 a +type family G2 x where G2 @a (x :: ConstType2 a) = x :: ConstType1 a + type G3 (x :: ConstType2 a) = a type G4 (x :: ConstType2 a) = x :: ConstType2 a diff --git a/testsuite/tests/indexed-types/should_fail/ClosedFam3.hs-boot b/testsuite/tests/indexed-types/should_fail/ClosedFam3.hs-boot index 5a10841ba4..5b603e8cd7 100644 --- a/testsuite/tests/indexed-types/should_fail/ClosedFam3.hs-boot +++ b/testsuite/tests/indexed-types/should_fail/ClosedFam3.hs-boot @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, PolyKinds #-} +{-# LANGUAGE TypeFamilies, PolyKinds, StandaloneKindSignatures #-} module ClosedFam3 where @@ -11,5 +11,6 @@ type family Bar a where Bar Int = Bool Bar Double = Char -type family Baz (a :: k) :: Type where +type Baz :: k -> Type +type family Baz a where Baz Int = Bool diff --git a/testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr b/testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr index f0a5614560..8160147e53 100644 --- a/testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr +++ b/testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr @@ -22,7 +22,7 @@ ClosedFam3.hs-boot:10:1: error: Bar Int = Bool Bar Double = Char -ClosedFam3.hs-boot:14:1: error: +ClosedFam3.hs-boot:15:1: error: Type constructor ‘Baz’ has conflicting definitions in the module and its hs-boot file Main module: type Baz :: * -> * diff --git a/testsuite/tests/indexed-types/should_fail/T14175.stderr b/testsuite/tests/indexed-types/should_fail/T14175.stderr index e177036e9e..dbadbe1f46 100644 --- a/testsuite/tests/indexed-types/should_fail/T14175.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14175.stderr @@ -3,4 +3,3 @@ T14175.hs:7:42: error: • Expecting one more argument to ‘k’ Expected a type, but ‘k’ has kind ‘j -> *’ • In the kind ‘k’ - In the type family declaration for ‘PComp’ diff --git a/testsuite/tests/indexed-types/should_fail/T14246.hs b/testsuite/tests/indexed-types/should_fail/T14246.hs index 6ae8760c84..e3fba67df7 100644 --- a/testsuite/tests/indexed-types/should_fail/T14246.hs +++ b/testsuite/tests/indexed-types/should_fail/T14246.hs @@ -1,4 +1,6 @@ -{-# LANGUAGE RankNTypes, GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilies, AllowAmbiguousTypes, UndecidableInstances, TypeInType #-} +{-# LANGUAGE RankNTypes, GADTs, TypeOperators, PolyKinds, DataKinds, + TypeFamilies, AllowAmbiguousTypes, UndecidableInstances, + StandaloneKindSignatures #-} module T14246 where @@ -6,7 +8,8 @@ import Data.Kind data Nat = Z | S Nat -data Vect :: Nat -> Type -> Type where +type Vect :: Nat -> Type -> Type +data Vect n a where Nil :: Vect Z a Cons :: a -> Vect n a -> Vect (S n) a @@ -14,10 +17,12 @@ data Label a = Label a data L -type family KLN (n :: k) :: Nat where +type KLN :: k -> Nat +type family KLN n where KLN (f :: v -> k) = S (KLN (forall t. f t)) KLN (f :: Type) = Z -type family Reveal (n :: k) (l :: Vect (KLN n) L) :: Type where +type Reveal :: forall n -> Vect (KLN n) L -> Type +type family Reveal n l where Reveal (f :: v -> k) (Cons (Label (t :: v)) l) = Reveal (f t) l Reveal (a :: Type) Nil = a diff --git a/testsuite/tests/indexed-types/should_fail/T14246.stderr b/testsuite/tests/indexed-types/should_fail/T14246.stderr index 4bb45d6399..78d87dbef5 100644 --- a/testsuite/tests/indexed-types/should_fail/T14246.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14246.stderr @@ -1,24 +1,24 @@ -T14246.hs:18:5: error: +T14246.hs:22:5: error: • Illegal polymorphic type: forall (t :: v). f t • In the equations for closed type family ‘KLN’ In the type family declaration for ‘KLN’ -T14246.hs:22:27: error: +T14246.hs:27:27: error: • Expected kind ‘Vect (KLN f) L’, but ‘Cons (Label (t :: v)) l’ has kind ‘Vect ('S (KLN (f t))) *’ • In the second argument of ‘Reveal’, namely ‘(Cons (Label (t :: v)) l)’ In the type family declaration for ‘Reveal’ -T14246.hs:22:67: error: +T14246.hs:27:67: error: • Expected kind ‘Vect (KLN (f t)) L’, but ‘l’ has kind ‘Vect (KLN (f t)) *’ • In the second argument of ‘Reveal’, namely ‘l’ In the type ‘Reveal (f t) l’ In the type family declaration for ‘Reveal’ -T14246.hs:23:24: error: +T14246.hs:28:24: error: • Expected kind ‘Vect (KLN a) L’, but ‘Nil’ has kind ‘Vect 'Z L’ • In the second argument of ‘Reveal’, namely ‘Nil’ In the type family declaration for ‘Reveal’ diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.hs b/testsuite/tests/parser/should_compile/DumpParsedAst.hs index f2bf433324..cedc3537de 100644 --- a/testsuite/tests/parser/should_compile/DumpParsedAst.hs +++ b/testsuite/tests/parser/should_compile/DumpParsedAst.hs @@ -1,11 +1,12 @@ -{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies - , TypeApplications, TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, + TypeApplications, StandaloneKindSignatures #-} module DumpParsedAst where import Data.Kind data Peano = Zero | Succ Peano +type Length :: [k] -> Peano type family Length (as :: [k]) :: Peano where Length (a : as) = Succ (Length as) Length '[] = Zero @@ -13,6 +14,7 @@ type family Length (as :: [k]) :: Peano where -- vis kind app data T f (a :: k) = MkT (f a) +type F1 :: k -> (k -> Type) -> Type type family F1 (a :: k) (f :: k -> Type) :: Type where F1 @Peano a f = T @Peano f a diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr index d7996df404..decf2df00b 100644 --- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr @@ -73,7 +73,37 @@ (Nothing)))] ({ <no location info> } []))))) - ,({ DumpParsedAst.hs:9:1-39 } + ,({ DumpParsedAst.hs:9:1-27 } + (KindSigD + (NoExtField) + (StandaloneKindSig + (NoExtField) + ({ DumpParsedAst.hs:9:6-11 } + (Unqual + {OccName: Length})) + (HsIB + (NoExtField) + ({ DumpParsedAst.hs:9:16-27 } + (HsFunTy + (NoExtField) + ({ DumpParsedAst.hs:9:16-18 } + (HsListTy + (NoExtField) + ({ DumpParsedAst.hs:9:17 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpParsedAst.hs:9:17 } + (Unqual + {OccName: k})))))) + ({ DumpParsedAst.hs:9:23-27 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpParsedAst.hs:9:23-27 } + (Unqual + {OccName: Peano})))))))))) + ,({ DumpParsedAst.hs:10:1-39 } (TyClD (NoExtField) (FamDecl @@ -82,153 +112,153 @@ (NoExtField) (ClosedTypeFamily (Just - [({ DumpParsedAst.hs:10:3-36 } + [({ DumpParsedAst.hs:11:3-36 } (HsIB (NoExtField) (FamEqn (NoExtField) - ({ DumpParsedAst.hs:10:3-8 } + ({ DumpParsedAst.hs:11:3-8 } (Unqual {OccName: Length})) (Nothing) [(HsValArg - ({ DumpParsedAst.hs:10:10-17 } + ({ DumpParsedAst.hs:11:10-17 } (HsParTy (NoExtField) - ({ DumpParsedAst.hs:10:11-16 } + ({ DumpParsedAst.hs:11:11-16 } (HsOpTy (NoExtField) - ({ DumpParsedAst.hs:10:11 } + ({ DumpParsedAst.hs:11:11 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:10:11 } + ({ DumpParsedAst.hs:11:11 } (Unqual {OccName: a})))) - ({ DumpParsedAst.hs:10:13 } + ({ DumpParsedAst.hs:11:13 } (Exact {Name: :})) - ({ DumpParsedAst.hs:10:15-16 } + ({ DumpParsedAst.hs:11:15-16 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:10:15-16 } + ({ DumpParsedAst.hs:11:15-16 } (Unqual {OccName: as})))))))))] (Prefix) - ({ DumpParsedAst.hs:10:21-36 } + ({ DumpParsedAst.hs:11:21-36 } (HsAppTy (NoExtField) - ({ DumpParsedAst.hs:10:21-24 } + ({ DumpParsedAst.hs:11:21-24 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:10:21-24 } + ({ DumpParsedAst.hs:11:21-24 } (Unqual {OccName: Succ})))) - ({ DumpParsedAst.hs:10:26-36 } + ({ DumpParsedAst.hs:11:26-36 } (HsParTy (NoExtField) - ({ DumpParsedAst.hs:10:27-35 } + ({ DumpParsedAst.hs:11:27-35 } (HsAppTy (NoExtField) - ({ DumpParsedAst.hs:10:27-32 } + ({ DumpParsedAst.hs:11:27-32 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:10:27-32 } + ({ DumpParsedAst.hs:11:27-32 } (Unqual {OccName: Length})))) - ({ DumpParsedAst.hs:10:34-35 } + ({ DumpParsedAst.hs:11:34-35 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:10:34-35 } + ({ DumpParsedAst.hs:11:34-35 } (Unqual {OccName: as}))))))))))))) - ,({ DumpParsedAst.hs:11:3-24 } + ,({ DumpParsedAst.hs:12:3-24 } (HsIB (NoExtField) (FamEqn (NoExtField) - ({ DumpParsedAst.hs:11:3-8 } + ({ DumpParsedAst.hs:12:3-8 } (Unqual {OccName: Length})) (Nothing) [(HsValArg - ({ DumpParsedAst.hs:11:10-12 } + ({ DumpParsedAst.hs:12:10-12 } (HsExplicitListTy (NoExtField) (IsPromoted) [])))] (Prefix) - ({ DumpParsedAst.hs:11:21-24 } + ({ DumpParsedAst.hs:12:21-24 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:11:21-24 } + ({ DumpParsedAst.hs:12:21-24 } (Unqual {OccName: Zero})))))))])) - ({ DumpParsedAst.hs:9:13-18 } + ({ DumpParsedAst.hs:10:13-18 } (Unqual {OccName: Length})) (HsQTvs (NoExtField) - [({ DumpParsedAst.hs:9:21-29 } + [({ DumpParsedAst.hs:10:21-29 } (KindedTyVar (NoExtField) - ({ DumpParsedAst.hs:9:21-22 } + ({ DumpParsedAst.hs:10:21-22 } (Unqual {OccName: as})) - ({ DumpParsedAst.hs:9:27-29 } + ({ DumpParsedAst.hs:10:27-29 } (HsListTy (NoExtField) - ({ DumpParsedAst.hs:9:28 } + ({ DumpParsedAst.hs:10:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:9:28 } + ({ DumpParsedAst.hs:10:28 } (Unqual {OccName: k}))))))))]) (Prefix) - ({ DumpParsedAst.hs:9:32-39 } + ({ DumpParsedAst.hs:10:32-39 } (KindSig (NoExtField) - ({ DumpParsedAst.hs:9:35-39 } + ({ DumpParsedAst.hs:10:35-39 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:9:35-39 } + ({ DumpParsedAst.hs:10:35-39 } (Unqual {OccName: Peano})))))) (Nothing))))) - ,({ DumpParsedAst.hs:14:1-29 } + ,({ DumpParsedAst.hs:15:1-29 } (TyClD (NoExtField) (DataDecl (NoExtField) - ({ DumpParsedAst.hs:14:6 } + ({ DumpParsedAst.hs:15:6 } (Unqual {OccName: T})) (HsQTvs (NoExtField) - [({ DumpParsedAst.hs:14:8 } + [({ DumpParsedAst.hs:15:8 } (UserTyVar (NoExtField) - ({ DumpParsedAst.hs:14:8 } + ({ DumpParsedAst.hs:15:8 } (Unqual {OccName: f})))) - ,({ DumpParsedAst.hs:14:11-16 } + ,({ DumpParsedAst.hs:15:11-16 } (KindedTyVar (NoExtField) - ({ DumpParsedAst.hs:14:11 } + ({ DumpParsedAst.hs:15:11 } (Unqual {OccName: a})) - ({ DumpParsedAst.hs:14:16 } + ({ DumpParsedAst.hs:15:16 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:14:16 } + ({ DumpParsedAst.hs:15:16 } (Unqual {OccName: k}))))))]) (Prefix) @@ -239,10 +269,10 @@ []) (Nothing) (Nothing) - [({ DumpParsedAst.hs:14:21-29 } + [({ DumpParsedAst.hs:15:21-29 } (ConDeclH98 (NoExtField) - ({ DumpParsedAst.hs:14:21-23 } + ({ DumpParsedAst.hs:15:21-23 } (Unqual {OccName: MkT})) ({ <no location info> } @@ -250,30 +280,80 @@ [] (Nothing) (PrefixCon - [({ DumpParsedAst.hs:14:25-29 } + [({ DumpParsedAst.hs:15:25-29 } (HsParTy (NoExtField) - ({ DumpParsedAst.hs:14:26-28 } + ({ DumpParsedAst.hs:15:26-28 } (HsAppTy (NoExtField) - ({ DumpParsedAst.hs:14:26 } + ({ DumpParsedAst.hs:15:26 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:14:26 } + ({ DumpParsedAst.hs:15:26 } (Unqual {OccName: f})))) - ({ DumpParsedAst.hs:14:28 } + ({ DumpParsedAst.hs:15:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:14:28 } + ({ DumpParsedAst.hs:15:28 } (Unqual {OccName: a}))))))))]) (Nothing)))] ({ <no location info> } []))))) - ,({ DumpParsedAst.hs:16:1-48 } + ,({ DumpParsedAst.hs:17:1-35 } + (KindSigD + (NoExtField) + (StandaloneKindSig + (NoExtField) + ({ DumpParsedAst.hs:17:6-7 } + (Unqual + {OccName: F1})) + (HsIB + (NoExtField) + ({ DumpParsedAst.hs:17:12-35 } + (HsFunTy + (NoExtField) + ({ DumpParsedAst.hs:17:12 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpParsedAst.hs:17:12 } + (Unqual + {OccName: k})))) + ({ DumpParsedAst.hs:17:17-35 } + (HsFunTy + (NoExtField) + ({ DumpParsedAst.hs:17:17-27 } + (HsParTy + (NoExtField) + ({ DumpParsedAst.hs:17:18-26 } + (HsFunTy + (NoExtField) + ({ DumpParsedAst.hs:17:18 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpParsedAst.hs:17:18 } + (Unqual + {OccName: k})))) + ({ DumpParsedAst.hs:17:23-26 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpParsedAst.hs:17:23-26 } + (Unqual + {OccName: Type})))))))) + ({ DumpParsedAst.hs:17:32-35 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpParsedAst.hs:17:32-35 } + (Unqual + {OccName: Type})))))))))))) + ,({ DumpParsedAst.hs:18:1-48 } (TyClD (NoExtField) (FamDecl @@ -282,147 +362,147 @@ (NoExtField) (ClosedTypeFamily (Just - [({ DumpParsedAst.hs:17:3-30 } + [({ DumpParsedAst.hs:19:3-30 } (HsIB (NoExtField) (FamEqn (NoExtField) - ({ DumpParsedAst.hs:17:3-4 } + ({ DumpParsedAst.hs:19:3-4 } (Unqual {OccName: F1})) (Nothing) [(HsTypeArg - { DumpParsedAst.hs:17:6-11 } - ({ DumpParsedAst.hs:17:7-11 } + { DumpParsedAst.hs:19:6-11 } + ({ DumpParsedAst.hs:19:7-11 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:7-11 } + ({ DumpParsedAst.hs:19:7-11 } (Unqual {OccName: Peano}))))) ,(HsValArg - ({ DumpParsedAst.hs:17:13 } + ({ DumpParsedAst.hs:19:13 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:13 } + ({ DumpParsedAst.hs:19:13 } (Unqual {OccName: a}))))) ,(HsValArg - ({ DumpParsedAst.hs:17:15 } + ({ DumpParsedAst.hs:19:15 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:15 } + ({ DumpParsedAst.hs:19:15 } (Unqual {OccName: f})))))] (Prefix) - ({ DumpParsedAst.hs:17:19-30 } + ({ DumpParsedAst.hs:19:19-30 } (HsAppTy (NoExtField) - ({ DumpParsedAst.hs:17:19-28 } + ({ DumpParsedAst.hs:19:19-28 } (HsAppTy (NoExtField) - ({ DumpParsedAst.hs:17:19-26 } + ({ DumpParsedAst.hs:19:19-26 } (HsAppKindTy - { DumpParsedAst.hs:17:21-26 } - ({ DumpParsedAst.hs:17:19 } + { DumpParsedAst.hs:19:21-26 } + ({ DumpParsedAst.hs:19:19 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:19 } + ({ DumpParsedAst.hs:19:19 } (Unqual {OccName: T})))) - ({ DumpParsedAst.hs:17:22-26 } + ({ DumpParsedAst.hs:19:22-26 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:22-26 } + ({ DumpParsedAst.hs:19:22-26 } (Unqual {OccName: Peano})))))) - ({ DumpParsedAst.hs:17:28 } + ({ DumpParsedAst.hs:19:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:28 } + ({ DumpParsedAst.hs:19:28 } (Unqual {OccName: f})))))) - ({ DumpParsedAst.hs:17:30 } + ({ DumpParsedAst.hs:19:30 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:17:30 } + ({ DumpParsedAst.hs:19:30 } (Unqual {OccName: a})))))))))])) - ({ DumpParsedAst.hs:16:13-14 } + ({ DumpParsedAst.hs:18:13-14 } (Unqual {OccName: F1})) (HsQTvs (NoExtField) - [({ DumpParsedAst.hs:16:17-22 } + [({ DumpParsedAst.hs:18:17-22 } (KindedTyVar (NoExtField) - ({ DumpParsedAst.hs:16:17 } + ({ DumpParsedAst.hs:18:17 } (Unqual {OccName: a})) - ({ DumpParsedAst.hs:16:22 } + ({ DumpParsedAst.hs:18:22 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:16:22 } + ({ DumpParsedAst.hs:18:22 } (Unqual {OccName: k})))))) - ,({ DumpParsedAst.hs:16:26-39 } + ,({ DumpParsedAst.hs:18:26-39 } (KindedTyVar (NoExtField) - ({ DumpParsedAst.hs:16:26 } + ({ DumpParsedAst.hs:18:26 } (Unqual {OccName: f})) - ({ DumpParsedAst.hs:16:31-39 } + ({ DumpParsedAst.hs:18:31-39 } (HsFunTy (NoExtField) - ({ DumpParsedAst.hs:16:31 } + ({ DumpParsedAst.hs:18:31 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:16:31 } + ({ DumpParsedAst.hs:18:31 } (Unqual {OccName: k})))) - ({ DumpParsedAst.hs:16:36-39 } + ({ DumpParsedAst.hs:18:36-39 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:16:36-39 } + ({ DumpParsedAst.hs:18:36-39 } (Unqual {OccName: Type}))))))))]) (Prefix) - ({ DumpParsedAst.hs:16:42-48 } + ({ DumpParsedAst.hs:18:42-48 } (KindSig (NoExtField) - ({ DumpParsedAst.hs:16:45-48 } + ({ DumpParsedAst.hs:18:45-48 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpParsedAst.hs:16:45-48 } + ({ DumpParsedAst.hs:18:45-48 } (Unqual {OccName: Type})))))) (Nothing))))) - ,({ DumpParsedAst.hs:19:1-23 } + ,({ DumpParsedAst.hs:21:1-23 } (ValD (NoExtField) (FunBind (NoExtField) - ({ DumpParsedAst.hs:19:1-4 } + ({ DumpParsedAst.hs:21:1-4 } (Unqual {OccName: main})) (MG (NoExtField) - ({ DumpParsedAst.hs:19:1-23 } - [({ DumpParsedAst.hs:19:1-23 } + ({ DumpParsedAst.hs:21:1-23 } + [({ DumpParsedAst.hs:21:1-23 } (Match (NoExtField) (FunRhs - ({ DumpParsedAst.hs:19:1-4 } + ({ DumpParsedAst.hs:21:1-4 } (Unqual {OccName: main})) (Prefix) @@ -430,20 +510,20 @@ [] (GRHSs (NoExtField) - [({ DumpParsedAst.hs:19:6-23 } + [({ DumpParsedAst.hs:21:6-23 } (GRHS (NoExtField) [] - ({ DumpParsedAst.hs:19:8-23 } + ({ DumpParsedAst.hs:21:8-23 } (HsApp (NoExtField) - ({ DumpParsedAst.hs:19:8-15 } + ({ DumpParsedAst.hs:21:8-15 } (HsVar (NoExtField) - ({ DumpParsedAst.hs:19:8-15 } + ({ DumpParsedAst.hs:21:8-15 } (Unqual {OccName: putStrLn})))) - ({ DumpParsedAst.hs:19:17-23 } + ({ DumpParsedAst.hs:21:17-23 } (HsLit (NoExtField) (HsString diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs index d5be8627be..100bbb1bb2 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs @@ -1,5 +1,5 @@ {-# LANGUAGE DataKinds, GADTs, PolyKinds, RankNTypes, TypeOperators, - TypeFamilies, StarIsType, TypeApplications #-} + TypeFamilies, TypeApplications, StandaloneKindSignatures #-} module DumpRenamedAst where import Data.Kind @@ -8,6 +8,7 @@ import Data.Kind (Type) data Peano = Zero | Succ Peano +type Length :: [k] -> Peano type family Length (as :: [k]) :: Peano where Length (a : as) = Succ (Length as) Length '[] = Zero @@ -20,6 +21,7 @@ newtype instance Nat (a :: k -> Type) :: (k -> Type) -> Type where data T f (a :: k) = MkT (f a) +type F1 :: k -> (k -> Type) -> Type type family F1 (a :: k) (f :: k -> Type) :: Type where F1 @Peano a f = T @Peano f a diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr index 53d4f37acf..965b6280b2 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr @@ -10,39 +10,39 @@ [((,) (NonRecursive) {Bag(Located (HsBind Name)): - [({ DumpRenamedAst.hs:26:1-23 } + [({ DumpRenamedAst.hs:28:1-23 } (FunBind {NameSet: []} - ({ DumpRenamedAst.hs:26:1-4 } + ({ DumpRenamedAst.hs:28:1-4 } {Name: DumpRenamedAst.main}) (MG (NoExtField) - ({ DumpRenamedAst.hs:26:1-23 } - [({ DumpRenamedAst.hs:26:1-23 } + ({ DumpRenamedAst.hs:28:1-23 } + [({ DumpRenamedAst.hs:28:1-23 } (Match (NoExtField) (FunRhs - ({ DumpRenamedAst.hs:26:1-4 } + ({ DumpRenamedAst.hs:28:1-4 } {Name: DumpRenamedAst.main}) (Prefix) (NoSrcStrict)) [] (GRHSs (NoExtField) - [({ DumpRenamedAst.hs:26:6-23 } + [({ DumpRenamedAst.hs:28:6-23 } (GRHS (NoExtField) [] - ({ DumpRenamedAst.hs:26:8-23 } + ({ DumpRenamedAst.hs:28:8-23 } (HsApp (NoExtField) - ({ DumpRenamedAst.hs:26:8-15 } + ({ DumpRenamedAst.hs:28:8-15 } (HsVar (NoExtField) - ({ DumpRenamedAst.hs:26:8-15 } + ({ DumpRenamedAst.hs:28:8-15 } {Name: System.IO.putStrLn}))) - ({ DumpRenamedAst.hs:26:17-23 } + ({ DumpRenamedAst.hs:28:17-23 } (HsLit (NoExtField) (HsString @@ -114,169 +114,193 @@ []) ,(TyClGroup (NoExtField) - [({ DumpRenamedAst.hs:11:1-39 } + [({ DumpRenamedAst.hs:12:1-39 } (FamDecl (NoExtField) (FamilyDecl (NoExtField) (ClosedTypeFamily (Just - [({ DumpRenamedAst.hs:12:3-36 } + [({ DumpRenamedAst.hs:13:3-36 } (HsIB [{Name: a} ,{Name: as}] (FamEqn (NoExtField) - ({ DumpRenamedAst.hs:12:3-8 } + ({ DumpRenamedAst.hs:13:3-8 } {Name: DumpRenamedAst.Length}) (Nothing) [(HsValArg - ({ DumpRenamedAst.hs:12:10-17 } + ({ DumpRenamedAst.hs:13:10-17 } (HsParTy (NoExtField) - ({ DumpRenamedAst.hs:12:11-16 } + ({ DumpRenamedAst.hs:13:11-16 } (HsOpTy (NoExtField) - ({ DumpRenamedAst.hs:12:11 } + ({ DumpRenamedAst.hs:13:11 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:12:11 } + ({ DumpRenamedAst.hs:13:11 } {Name: a}))) - ({ DumpRenamedAst.hs:12:13 } + ({ DumpRenamedAst.hs:13:13 } {Name: :}) - ({ DumpRenamedAst.hs:12:15-16 } + ({ DumpRenamedAst.hs:13:15-16 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:12:15-16 } + ({ DumpRenamedAst.hs:13:15-16 } {Name: as}))))))))] (Prefix) - ({ DumpRenamedAst.hs:12:21-36 } + ({ DumpRenamedAst.hs:13:21-36 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:12:21-24 } + ({ DumpRenamedAst.hs:13:21-24 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:12:21-24 } + ({ DumpRenamedAst.hs:13:21-24 } {Name: DumpRenamedAst.Succ}))) - ({ DumpRenamedAst.hs:12:26-36 } + ({ DumpRenamedAst.hs:13:26-36 } (HsParTy (NoExtField) - ({ DumpRenamedAst.hs:12:27-35 } + ({ DumpRenamedAst.hs:13:27-35 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:12:27-32 } + ({ DumpRenamedAst.hs:13:27-32 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:12:27-32 } + ({ DumpRenamedAst.hs:13:27-32 } {Name: DumpRenamedAst.Length}))) - ({ DumpRenamedAst.hs:12:34-35 } + ({ DumpRenamedAst.hs:13:34-35 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:12:34-35 } + ({ DumpRenamedAst.hs:13:34-35 } {Name: as})))))))))))) - ,({ DumpRenamedAst.hs:13:3-24 } + ,({ DumpRenamedAst.hs:14:3-24 } (HsIB [] (FamEqn (NoExtField) - ({ DumpRenamedAst.hs:13:3-8 } + ({ DumpRenamedAst.hs:14:3-8 } {Name: DumpRenamedAst.Length}) (Nothing) [(HsValArg - ({ DumpRenamedAst.hs:13:10-12 } + ({ DumpRenamedAst.hs:14:10-12 } (HsExplicitListTy (NoExtField) (IsPromoted) [])))] (Prefix) - ({ DumpRenamedAst.hs:13:21-24 } + ({ DumpRenamedAst.hs:14:21-24 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:13:21-24 } + ({ DumpRenamedAst.hs:14:21-24 } {Name: DumpRenamedAst.Zero}))))))])) - ({ DumpRenamedAst.hs:11:13-18 } + ({ DumpRenamedAst.hs:12:13-18 } {Name: DumpRenamedAst.Length}) (HsQTvs [{Name: k}] - [({ DumpRenamedAst.hs:11:21-29 } + [({ DumpRenamedAst.hs:12:21-29 } (KindedTyVar (NoExtField) - ({ DumpRenamedAst.hs:11:21-22 } + ({ DumpRenamedAst.hs:12:21-22 } {Name: as}) - ({ DumpRenamedAst.hs:11:27-29 } + ({ DumpRenamedAst.hs:12:27-29 } (HsListTy (NoExtField) - ({ DumpRenamedAst.hs:11:28 } + ({ DumpRenamedAst.hs:12:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:11:28 } + ({ DumpRenamedAst.hs:12:28 } {Name: k})))))))]) (Prefix) - ({ DumpRenamedAst.hs:11:32-39 } + ({ DumpRenamedAst.hs:12:32-39 } (KindSig (NoExtField) - ({ DumpRenamedAst.hs:11:35-39 } + ({ DumpRenamedAst.hs:12:35-39 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:11:35-39 } + ({ DumpRenamedAst.hs:12:35-39 } {Name: DumpRenamedAst.Peano}))))) (Nothing))))] [] - [] + [({ DumpRenamedAst.hs:11:1-27 } + (StandaloneKindSig + (NoExtField) + ({ DumpRenamedAst.hs:11:6-11 } + {Name: DumpRenamedAst.Length}) + (HsIB + [{Name: k}] + ({ DumpRenamedAst.hs:11:16-27 } + (HsFunTy + (NoExtField) + ({ DumpRenamedAst.hs:11:16-18 } + (HsListTy + (NoExtField) + ({ DumpRenamedAst.hs:11:17 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpRenamedAst.hs:11:17 } + {Name: k}))))) + ({ DumpRenamedAst.hs:11:23-27 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpRenamedAst.hs:11:23-27 } + {Name: DumpRenamedAst.Peano}))))))))] []) ,(TyClGroup (NoExtField) - [({ DumpRenamedAst.hs:15:1-33 } + [({ DumpRenamedAst.hs:16:1-33 } (FamDecl (NoExtField) (FamilyDecl (NoExtField) (DataFamily) - ({ DumpRenamedAst.hs:15:13-15 } + ({ DumpRenamedAst.hs:16:13-15 } {Name: DumpRenamedAst.Nat}) (HsQTvs [{Name: k}] []) (Prefix) - ({ DumpRenamedAst.hs:15:17-33 } + ({ DumpRenamedAst.hs:16:17-33 } (KindSig (NoExtField) - ({ DumpRenamedAst.hs:15:20-33 } + ({ DumpRenamedAst.hs:16:20-33 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:15:20 } + ({ DumpRenamedAst.hs:16:20 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:15:20 } + ({ DumpRenamedAst.hs:16:20 } {Name: k}))) - ({ DumpRenamedAst.hs:15:25-33 } + ({ DumpRenamedAst.hs:16:25-33 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:15:25 } + ({ DumpRenamedAst.hs:16:25 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:15:25 } + ({ DumpRenamedAst.hs:16:25 } {Name: k}))) - ({ DumpRenamedAst.hs:15:30-33 } + ({ DumpRenamedAst.hs:16:30-33 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:15:30-33 } + ({ DumpRenamedAst.hs:16:30-33 } {Name: GHC.Types.Type}))))))))) (Nothing))))] [] [] - [({ DumpRenamedAst.hs:(18,1)-(19,45) } + [({ DumpRenamedAst.hs:(19,1)-(20,45) } (DataFamInstD (NoExtField) (DataFamInstDecl @@ -285,36 +309,36 @@ ,{Name: k}] (FamEqn (NoExtField) - ({ DumpRenamedAst.hs:18:18-20 } + ({ DumpRenamedAst.hs:19:18-20 } {Name: DumpRenamedAst.Nat}) (Nothing) [(HsValArg - ({ DumpRenamedAst.hs:18:22-37 } + ({ DumpRenamedAst.hs:19:22-37 } (HsParTy (NoExtField) - ({ DumpRenamedAst.hs:18:23-36 } + ({ DumpRenamedAst.hs:19:23-36 } (HsKindSig (NoExtField) - ({ DumpRenamedAst.hs:18:23 } + ({ DumpRenamedAst.hs:19:23 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:18:23 } + ({ DumpRenamedAst.hs:19:23 } {Name: a}))) - ({ DumpRenamedAst.hs:18:28-36 } + ({ DumpRenamedAst.hs:19:28-36 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:18:28 } + ({ DumpRenamedAst.hs:19:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:18:28 } + ({ DumpRenamedAst.hs:19:28 } {Name: k}))) - ({ DumpRenamedAst.hs:18:33-36 } + ({ DumpRenamedAst.hs:19:33-36 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:18:33-36 } + ({ DumpRenamedAst.hs:19:33-36 } {Name: GHC.Types.Type}))))))))))] (Prefix) (HsDataDefn @@ -324,39 +348,39 @@ []) (Nothing) (Just - ({ DumpRenamedAst.hs:18:42-60 } + ({ DumpRenamedAst.hs:19:42-60 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:18:42-52 } + ({ DumpRenamedAst.hs:19:42-52 } (HsParTy (NoExtField) - ({ DumpRenamedAst.hs:18:43-51 } + ({ DumpRenamedAst.hs:19:43-51 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:18:43 } + ({ DumpRenamedAst.hs:19:43 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:18:43 } + ({ DumpRenamedAst.hs:19:43 } {Name: k}))) - ({ DumpRenamedAst.hs:18:48-51 } + ({ DumpRenamedAst.hs:19:48-51 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:18:48-51 } + ({ DumpRenamedAst.hs:19:48-51 } {Name: GHC.Types.Type}))))))) - ({ DumpRenamedAst.hs:18:57-60 } + ({ DumpRenamedAst.hs:19:57-60 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:18:57-60 } + ({ DumpRenamedAst.hs:19:57-60 } {Name: GHC.Types.Type})))))) - [({ DumpRenamedAst.hs:19:3-45 } + [({ DumpRenamedAst.hs:20:3-45 } (ConDeclGADT (NoExtField) - [({ DumpRenamedAst.hs:19:3-5 } + [({ DumpRenamedAst.hs:20:3-5 } {Name: DumpRenamedAst.Nat})] - ({ DumpRenamedAst.hs:19:10-45 } + ({ DumpRenamedAst.hs:20:10-45 } (False)) (HsQTvs [{Name: f} @@ -364,106 +388,106 @@ []) (Nothing) (PrefixCon - [({ DumpRenamedAst.hs:19:10-34 } + [({ DumpRenamedAst.hs:20:10-34 } (HsParTy (NoExtField) - ({ DumpRenamedAst.hs:19:11-33 } + ({ DumpRenamedAst.hs:20:11-33 } (HsForAllTy (NoExtField) (ForallInvis) - [({ DumpRenamedAst.hs:19:18-19 } + [({ DumpRenamedAst.hs:20:18-19 } (UserTyVar (NoExtField) - ({ DumpRenamedAst.hs:19:18-19 } + ({ DumpRenamedAst.hs:20:18-19 } {Name: xx})))] - ({ DumpRenamedAst.hs:19:22-33 } + ({ DumpRenamedAst.hs:20:22-33 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:19:22-25 } + ({ DumpRenamedAst.hs:20:22-25 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:19:22 } + ({ DumpRenamedAst.hs:20:22 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:22 } + ({ DumpRenamedAst.hs:20:22 } {Name: f}))) - ({ DumpRenamedAst.hs:19:24-25 } + ({ DumpRenamedAst.hs:20:24-25 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:24-25 } + ({ DumpRenamedAst.hs:20:24-25 } {Name: xx}))))) - ({ DumpRenamedAst.hs:19:30-33 } + ({ DumpRenamedAst.hs:20:30-33 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:19:30 } + ({ DumpRenamedAst.hs:20:30 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:30 } + ({ DumpRenamedAst.hs:20:30 } {Name: g}))) - ({ DumpRenamedAst.hs:19:32-33 } + ({ DumpRenamedAst.hs:20:32-33 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:32-33 } + ({ DumpRenamedAst.hs:20:32-33 } {Name: xx})))))))))))]) - ({ DumpRenamedAst.hs:19:39-45 } + ({ DumpRenamedAst.hs:20:39-45 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:19:39-43 } + ({ DumpRenamedAst.hs:20:39-43 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:19:39-41 } + ({ DumpRenamedAst.hs:20:39-41 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:39-41 } + ({ DumpRenamedAst.hs:20:39-41 } {Name: DumpRenamedAst.Nat}))) - ({ DumpRenamedAst.hs:19:43 } + ({ DumpRenamedAst.hs:20:43 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:43 } + ({ DumpRenamedAst.hs:20:43 } {Name: f}))))) - ({ DumpRenamedAst.hs:19:45 } + ({ DumpRenamedAst.hs:20:45 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:19:45 } + ({ DumpRenamedAst.hs:20:45 } {Name: g}))))) (Nothing)))] ({ <no location info> } [])))))))]) ,(TyClGroup (NoExtField) - [({ DumpRenamedAst.hs:21:1-29 } + [({ DumpRenamedAst.hs:22:1-29 } (DataDecl (DataDeclRn (False) {NameSet: [{Name: a} ,{Name: f}]}) - ({ DumpRenamedAst.hs:21:6 } + ({ DumpRenamedAst.hs:22:6 } {Name: DumpRenamedAst.T}) (HsQTvs [{Name: k}] - [({ DumpRenamedAst.hs:21:8 } + [({ DumpRenamedAst.hs:22:8 } (UserTyVar (NoExtField) - ({ DumpRenamedAst.hs:21:8 } + ({ DumpRenamedAst.hs:22:8 } {Name: f}))) - ,({ DumpRenamedAst.hs:21:11-16 } + ,({ DumpRenamedAst.hs:22:11-16 } (KindedTyVar (NoExtField) - ({ DumpRenamedAst.hs:21:11 } + ({ DumpRenamedAst.hs:22:11 } {Name: a}) - ({ DumpRenamedAst.hs:21:16 } + ({ DumpRenamedAst.hs:22:16 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:21:16 } + ({ DumpRenamedAst.hs:22:16 } {Name: k})))))]) (Prefix) (HsDataDefn @@ -473,33 +497,33 @@ []) (Nothing) (Nothing) - [({ DumpRenamedAst.hs:21:21-29 } + [({ DumpRenamedAst.hs:22:21-29 } (ConDeclH98 (NoExtField) - ({ DumpRenamedAst.hs:21:21-23 } + ({ DumpRenamedAst.hs:22:21-23 } {Name: DumpRenamedAst.MkT}) ({ <no location info> } (False)) [] (Nothing) (PrefixCon - [({ DumpRenamedAst.hs:21:25-29 } + [({ DumpRenamedAst.hs:22:25-29 } (HsParTy (NoExtField) - ({ DumpRenamedAst.hs:21:26-28 } + ({ DumpRenamedAst.hs:22:26-28 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:21:26 } + ({ DumpRenamedAst.hs:22:26 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:21:26 } + ({ DumpRenamedAst.hs:22:26 } {Name: f}))) - ({ DumpRenamedAst.hs:21:28 } + ({ DumpRenamedAst.hs:22:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:21:28 } + ({ DumpRenamedAst.hs:22:28 } {Name: a})))))))]) (Nothing)))] ({ <no location info> } @@ -509,126 +533,168 @@ []) ,(TyClGroup (NoExtField) - [({ DumpRenamedAst.hs:23:1-48 } + [({ DumpRenamedAst.hs:25:1-48 } (FamDecl (NoExtField) (FamilyDecl (NoExtField) (ClosedTypeFamily (Just - [({ DumpRenamedAst.hs:24:3-30 } + [({ DumpRenamedAst.hs:26:3-30 } (HsIB [{Name: a} ,{Name: f}] (FamEqn (NoExtField) - ({ DumpRenamedAst.hs:24:3-4 } + ({ DumpRenamedAst.hs:26:3-4 } {Name: DumpRenamedAst.F1}) (Nothing) [(HsTypeArg - { DumpRenamedAst.hs:24:6-11 } - ({ DumpRenamedAst.hs:24:7-11 } + { DumpRenamedAst.hs:26:6-11 } + ({ DumpRenamedAst.hs:26:7-11 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:7-11 } + ({ DumpRenamedAst.hs:26:7-11 } {Name: DumpRenamedAst.Peano})))) ,(HsValArg - ({ DumpRenamedAst.hs:24:13 } + ({ DumpRenamedAst.hs:26:13 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:13 } + ({ DumpRenamedAst.hs:26:13 } {Name: a})))) ,(HsValArg - ({ DumpRenamedAst.hs:24:15 } + ({ DumpRenamedAst.hs:26:15 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:15 } + ({ DumpRenamedAst.hs:26:15 } {Name: f}))))] (Prefix) - ({ DumpRenamedAst.hs:24:19-30 } + ({ DumpRenamedAst.hs:26:19-30 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:24:19-28 } + ({ DumpRenamedAst.hs:26:19-28 } (HsAppTy (NoExtField) - ({ DumpRenamedAst.hs:24:19-26 } + ({ DumpRenamedAst.hs:26:19-26 } (HsAppKindTy - { DumpRenamedAst.hs:24:21-26 } - ({ DumpRenamedAst.hs:24:19 } + { DumpRenamedAst.hs:26:21-26 } + ({ DumpRenamedAst.hs:26:19 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:19 } + ({ DumpRenamedAst.hs:26:19 } {Name: DumpRenamedAst.T}))) - ({ DumpRenamedAst.hs:24:22-26 } + ({ DumpRenamedAst.hs:26:22-26 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:22-26 } + ({ DumpRenamedAst.hs:26:22-26 } {Name: DumpRenamedAst.Peano}))))) - ({ DumpRenamedAst.hs:24:28 } + ({ DumpRenamedAst.hs:26:28 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:28 } + ({ DumpRenamedAst.hs:26:28 } {Name: f}))))) - ({ DumpRenamedAst.hs:24:30 } + ({ DumpRenamedAst.hs:26:30 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:24:30 } + ({ DumpRenamedAst.hs:26:30 } {Name: a}))))))))])) - ({ DumpRenamedAst.hs:23:13-14 } + ({ DumpRenamedAst.hs:25:13-14 } {Name: DumpRenamedAst.F1}) (HsQTvs [{Name: k}] - [({ DumpRenamedAst.hs:23:17-22 } + [({ DumpRenamedAst.hs:25:17-22 } (KindedTyVar (NoExtField) - ({ DumpRenamedAst.hs:23:17 } + ({ DumpRenamedAst.hs:25:17 } {Name: a}) - ({ DumpRenamedAst.hs:23:22 } + ({ DumpRenamedAst.hs:25:22 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:23:22 } + ({ DumpRenamedAst.hs:25:22 } {Name: k}))))) - ,({ DumpRenamedAst.hs:23:26-39 } + ,({ DumpRenamedAst.hs:25:26-39 } (KindedTyVar (NoExtField) - ({ DumpRenamedAst.hs:23:26 } + ({ DumpRenamedAst.hs:25:26 } {Name: f}) - ({ DumpRenamedAst.hs:23:31-39 } + ({ DumpRenamedAst.hs:25:31-39 } (HsFunTy (NoExtField) - ({ DumpRenamedAst.hs:23:31 } + ({ DumpRenamedAst.hs:25:31 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:23:31 } + ({ DumpRenamedAst.hs:25:31 } {Name: k}))) - ({ DumpRenamedAst.hs:23:36-39 } + ({ DumpRenamedAst.hs:25:36-39 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:23:36-39 } + ({ DumpRenamedAst.hs:25:36-39 } {Name: GHC.Types.Type})))))))]) (Prefix) - ({ DumpRenamedAst.hs:23:42-48 } + ({ DumpRenamedAst.hs:25:42-48 } (KindSig (NoExtField) - ({ DumpRenamedAst.hs:23:45-48 } + ({ DumpRenamedAst.hs:25:45-48 } (HsTyVar (NoExtField) (NotPromoted) - ({ DumpRenamedAst.hs:23:45-48 } + ({ DumpRenamedAst.hs:25:45-48 } {Name: GHC.Types.Type}))))) (Nothing))))] [] - [] + [({ DumpRenamedAst.hs:24:1-35 } + (StandaloneKindSig + (NoExtField) + ({ DumpRenamedAst.hs:24:6-7 } + {Name: DumpRenamedAst.F1}) + (HsIB + [{Name: k}] + ({ DumpRenamedAst.hs:24:12-35 } + (HsFunTy + (NoExtField) + ({ DumpRenamedAst.hs:24:12 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpRenamedAst.hs:24:12 } + {Name: k}))) + ({ DumpRenamedAst.hs:24:17-35 } + (HsFunTy + (NoExtField) + ({ DumpRenamedAst.hs:24:17-27 } + (HsParTy + (NoExtField) + ({ DumpRenamedAst.hs:24:18-26 } + (HsFunTy + (NoExtField) + ({ DumpRenamedAst.hs:24:18 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpRenamedAst.hs:24:18 } + {Name: k}))) + ({ DumpRenamedAst.hs:24:23-26 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpRenamedAst.hs:24:23-26 } + {Name: GHC.Types.Type}))))))) + ({ DumpRenamedAst.hs:24:32-35 } + (HsTyVar + (NoExtField) + (NotPromoted) + ({ DumpRenamedAst.hs:24:32-35 } + {Name: GHC.Types.Type}))))))))))] [])] [] [] diff --git a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs index 82cf107e5d..9f01cc9fc8 100644 --- a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs +++ b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.hs @@ -1,17 +1,19 @@ -{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies - , TypeApplications #-} +{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, + TypeApplications, StandaloneKindSignatures #-} module DumpTypecheckedAst where import Data.Kind data Peano = Zero | Succ Peano +type Length :: [k] -> Peano type family Length (as :: [k]) :: Peano where Length (a : as) = Succ (Length as) Length '[] = Zero data T f (a :: k) = MkT (f a) +type F :: k -> (k -> Type) -> Type type family F (a :: k) (f :: k -> Type) :: Type where F @Peano a f = T @Peano f a diff --git a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr index 6aa8aa4578..4ce02e7dd1 100644 --- a/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr @@ -702,7 +702,7 @@ (NoSourceText) "DumpTypecheckedAst"))))))))) (False))) - ,({ DumpTypecheckedAst.hs:18:1-23 } + ,({ DumpTypecheckedAst.hs:20:1-23 } (AbsBinds (NoExtField) [] @@ -716,11 +716,11 @@ []))] [({abstract:TcEvBinds})] {Bag(Located (HsBind Var)): - [({ DumpTypecheckedAst.hs:18:1-23 } + [({ DumpTypecheckedAst.hs:20:1-23 } (FunBind {NameSet: []} - ({ DumpTypecheckedAst.hs:18:1-4 } + ({ DumpTypecheckedAst.hs:20:1-4 } {Var: main}) (MG (MatchGroupTc @@ -730,31 +730,31 @@ [(TyConApp ({abstract:TyCon}) [])])) - ({ DumpTypecheckedAst.hs:18:1-23 } - [({ DumpTypecheckedAst.hs:18:1-23 } + ({ DumpTypecheckedAst.hs:20:1-23 } + [({ DumpTypecheckedAst.hs:20:1-23 } (Match (NoExtField) (FunRhs - ({ DumpTypecheckedAst.hs:18:1-4 } + ({ DumpTypecheckedAst.hs:20:1-4 } {Name: main}) (Prefix) (NoSrcStrict)) [] (GRHSs (NoExtField) - [({ DumpTypecheckedAst.hs:18:6-23 } + [({ DumpTypecheckedAst.hs:20:6-23 } (GRHS (NoExtField) [] - ({ DumpTypecheckedAst.hs:18:8-23 } + ({ DumpTypecheckedAst.hs:20:8-23 } (HsApp (NoExtField) - ({ DumpTypecheckedAst.hs:18:8-15 } + ({ DumpTypecheckedAst.hs:20:8-15 } (HsVar (NoExtField) ({ <no location info> } {Var: putStrLn}))) - ({ DumpTypecheckedAst.hs:18:17-23 } + ({ DumpTypecheckedAst.hs:20:17-23 } (HsLit (NoExtField) (HsString diff --git a/testsuite/tests/patsyn/should_compile/T10997_1a.hs b/testsuite/tests/patsyn/should_compile/T10997_1a.hs index 11af525c53..aac19b0319 100644 --- a/testsuite/tests/patsyn/should_compile/T10997_1a.hs +++ b/testsuite/tests/patsyn/should_compile/T10997_1a.hs @@ -1,9 +1,11 @@ -{-# LANGUAGE PatternSynonyms, ViewPatterns, ConstraintKinds, TypeFamilies, PolyKinds, KindSignatures #-} +{-# LANGUAGE PatternSynonyms, ViewPatterns, ConstraintKinds, TypeFamilies, + PolyKinds, KindSignatures, StandaloneKindSignatures #-} module T10997_1a where import Data.Kind -type family Showable (a :: k) :: Constraint where +type Showable :: k -> Constraint +type family Showable a where Showable (a :: Type) = (Show a) Showable a = () diff --git a/testsuite/tests/patsyn/should_compile/T12698.hs b/testsuite/tests/patsyn/should_compile/T12698.hs index 68cd817677..db4b003177 100644 --- a/testsuite/tests/patsyn/should_compile/T12698.hs +++ b/testsuite/tests/patsyn/should_compile/T12698.hs @@ -1,6 +1,7 @@ {-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds, StandaloneDeriving, GADTs, RebindableSyntax, - RankNTypes, LambdaCase, PatternSynonyms, TypeApplications #-} + RankNTypes, LambdaCase, PatternSynonyms, TypeApplications, + StandaloneKindSignatures #-} module T12698 where @@ -36,7 +37,8 @@ splitApp = \case TP -> Nothing TA f x -> Just (App f x) -data (a :: k1) :~~: (b :: k2) where +type (:~~:) :: k1 -> k2 -> Type +data a :~~: b where HRefl :: a :~~: a eqT :: T a -> T b -> Maybe (a :~~: b) diff --git a/testsuite/tests/patsyn/should_fail/T14507.hs b/testsuite/tests/patsyn/should_fail/T14507.hs index 9599b73c77..6c8326733c 100644 --- a/testsuite/tests/patsyn/should_fail/T14507.hs +++ b/testsuite/tests/patsyn/should_fail/T14507.hs @@ -1,6 +1,7 @@ {-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, PolyKinds, ScopedTypeVariables, DataKinds, TypeOperators, - TypeApplications, TypeFamilies, TypeFamilyDependencies #-} + TypeApplications, TypeFamilies, TypeFamilyDependencies, + StandaloneKindSignatures #-} module T14507 where @@ -10,7 +11,8 @@ import Data.Kind foo :: TypeRep a -> (Bool :~~: k, TypeRep a) foo rep = error "urk" -type family SING :: k -> Type where +type SING :: k -> Type +type family SING where SING = (TypeRep :: Bool -> Type) pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk) diff --git a/testsuite/tests/patsyn/should_fail/T14507.stderr b/testsuite/tests/patsyn/should_fail/T14507.stderr index 1279ec1e4e..de0bd77abb 100644 --- a/testsuite/tests/patsyn/should_fail/T14507.stderr +++ b/testsuite/tests/patsyn/should_fail/T14507.stderr @@ -1,5 +1,5 @@ -T14507.hs:20:9: error: +T14507.hs:22:9: error: • Iceland Jack! Iceland Jack! Stop torturing me! Pattern-bound variable x :: TypeRep a has a type that mentions pattern-bound coercion: co diff --git a/testsuite/tests/patsyn/should_fail/T15694.hs b/testsuite/tests/patsyn/should_fail/T15694.hs index 915ad7e7dd..ac424f1d24 100644 --- a/testsuite/tests/patsyn/should_fail/T15694.hs +++ b/testsuite/tests/patsyn/should_fail/T15694.hs @@ -1,4 +1,5 @@ -{-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, KindSignatures, GADTs #-} +{-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, + StandaloneKindSignatures, GADTs #-} module T15694 where @@ -9,7 +10,8 @@ data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as) -data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where +type ApplyT :: forall (kind::Type) -> kind -> Ctx(kind) -> Type +data ApplyT k t ctx where AO :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) ctx -> ApplyT(k -> ks) f (a:&:ctx) diff --git a/testsuite/tests/patsyn/should_fail/T15694.stderr b/testsuite/tests/patsyn/should_fail/T15694.stderr index 360fb30ba2..efcdc7c421 100644 --- a/testsuite/tests/patsyn/should_fail/T15694.stderr +++ b/testsuite/tests/patsyn/should_fail/T15694.stderr @@ -1,4 +1,4 @@ -T15694.hs:22:35: error: +T15694.hs:24:35: error: • Expected kind ‘k1 -> k00’, but ‘f a1’ has kind ‘ks’ • In the first argument of ‘(~~)’, namely ‘f a1 a2’ diff --git a/testsuite/tests/patsyn/should_fail/T15695.hs b/testsuite/tests/patsyn/should_fail/T15695.hs index de8035c728..8c075ce8f6 100644 --- a/testsuite/tests/patsyn/should_fail/T15695.hs +++ b/testsuite/tests/patsyn/should_fail/T15695.hs @@ -1,6 +1,7 @@ {-# Language RankNTypes, PatternSynonyms, DataKinds, PolyKinds, GADTs, TypeOperators, MultiParamTypeClasses, TypeFamilies, - TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts #-} + TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts, + StandaloneKindSignatures #-} {-# Options_GHC -fdefer-type-errors #-} @@ -30,7 +31,8 @@ data NA a type SOP(kind::Type) code = NS (NP NA) code -data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where +type ApplyT :: forall (kind::Type) -> kind -> Ctx(kind) -> Type +data ApplyT k t ctx where AO :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) ctx -> ApplyT(k -> ks) f (a:&:ctx) diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr index 6ef415ad9b..0281ca0a4e 100644 --- a/testsuite/tests/patsyn/should_fail/T15695.stderr +++ b/testsuite/tests/patsyn/should_fail/T15695.stderr @@ -1,5 +1,5 @@ -T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)] +T15695.hs:41:14: warning: [-Wdeferred-type-errors (in -Wdefault)] • Could not deduce: a2 ~ NA 'VO from the context: ((* -> * -> *) ~ (k1 -> k2 -> *), Either ~~ f, ctx ~~ (a2 ':&: (a3 ':&: 'E)), f a2 ~~ f1, f1 a3 ~~ a4) @@ -12,7 +12,7 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)] f a1 ~~ f1, f1 a2 ~~ a3) => a3 -> ApplyT kind a b, in an equation for ‘from'’ - at T15695.hs:39:8-21 + at T15695.hs:41:8-21 ‘a2’ is a rigid type variable bound by a pattern with pattern synonym: ASSO :: forall kind (a :: kind) (b :: Ctx kind). @@ -23,7 +23,7 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)] f a1 ~~ f1, f1 a2 ~~ a3) => a3 -> ApplyT kind a b, in an equation for ‘from'’ - at T15695.hs:39:8-21 + at T15695.hs:41:8-21 Expected type: a4 Actual type: Either (NA 'VO) a3 • In the pattern: Left a @@ -31,9 +31,9 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)] In an equation for ‘from'’: from' (ASSO (Left a)) = Here (a :* Nil) • Relevant bindings include from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]] - (bound at T15695.hs:39:1) + (bound at T15695.hs:41:1) -T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)] +T15695.hs:42:26: warning: [-Wdeferred-type-errors (in -Wdefault)] • Couldn't match type ‘a0 : as0’ with ‘'[]’ Expected type: NS (NP NA) '[ '[ 'VO]] Actual type: NS (NP NA) ('[ 'VO] : a0 : as0) @@ -42,4 +42,4 @@ T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)] from' (ASSO (Right b)) = There (Here undefined) • Relevant bindings include from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]] - (bound at T15695.hs:39:1) + (bound at T15695.hs:41:1) diff --git a/testsuite/tests/pmcheck/complete_sigs/T14253.hs b/testsuite/tests/pmcheck/complete_sigs/T14253.hs index bb56d437bf..083d0d0830 100644 --- a/testsuite/tests/pmcheck/complete_sigs/T14253.hs +++ b/testsuite/tests/pmcheck/complete_sigs/T14253.hs @@ -3,13 +3,15 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T14253 where import GHC.Exts import Data.Kind -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where Con :: TypeRep (a :: k) TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2). diff --git a/testsuite/tests/polykinds/PolyKinds06.stderr b/testsuite/tests/polykinds/PolyKinds06.stderr index e5c9daa8c3..83da173005 100644 --- a/testsuite/tests/polykinds/PolyKinds06.stderr +++ b/testsuite/tests/polykinds/PolyKinds06.stderr @@ -3,4 +3,3 @@ PolyKinds06.hs:9:11: error: • Type constructor ‘A’ cannot be used here (it is defined and used in the same recursive group) • In the kind ‘A -> *’ - In the data type declaration for ‘B’ diff --git a/testsuite/tests/polykinds/T10670a.hs b/testsuite/tests/polykinds/T10670a.hs index d398cb72a8..1a91c63a56 100644 --- a/testsuite/tests/polykinds/T10670a.hs +++ b/testsuite/tests/polykinds/T10670a.hs @@ -1,7 +1,8 @@ -{-# LANGUAGE GADTs , PolyKinds #-} +{-# LANGUAGE GADTs, PolyKinds, StandaloneKindSignatures #-} module Bug2 where +import Data.Kind import Unsafe.Coerce data TyConT (a::k) = TyConT String @@ -14,8 +15,8 @@ eqTyConT (TyConT a) (TyConT b) = a == b tyConTArr :: TyConT (->) tyConTArr = TyConT "(->)" - -data TypeRepT (a::k) where +type TypeRepT :: k -> Type +data TypeRepT a where TRCon :: TyConT a -> TypeRepT a TRApp :: TypeRepT a -> TypeRepT b -> TypeRepT (a b) diff --git a/testsuite/tests/polykinds/T11362.hs b/testsuite/tests/polykinds/T11362.hs index d08ebe2461..8614a8aa2d 100644 --- a/testsuite/tests/polykinds/T11362.hs +++ b/testsuite/tests/polykinds/T11362.hs @@ -3,6 +3,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T11362 where -- this file when compiled with -dunique-increment=-1 made GHC crash @@ -24,5 +25,6 @@ data instance In (F f) r o where MkIn :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o -- Requires polymorphic recursion -data In' (f :: Code i o) :: (i -> Type) -> o -> Type where +type In' :: Code i o -> (i -> Type) -> o -> Type +data In' f r t where MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t diff --git a/testsuite/tests/polykinds/T11480a.hs b/testsuite/tests/polykinds/T11480a.hs index b491a21518..87460a2e61 100644 --- a/testsuite/tests/polykinds/T11480a.hs +++ b/testsuite/tests/polykinds/T11480a.hs @@ -2,7 +2,8 @@ NoImplicitPrelude, FlexibleContexts, MultiParamTypeClasses, GADTs, ConstraintKinds, FlexibleInstances, UndecidableInstances, - FunctionalDependencies, UndecidableSuperClasses #-} + FunctionalDependencies, UndecidableSuperClasses, + StandaloneKindSignatures #-} module T11480a where @@ -11,7 +12,8 @@ import qualified Prelude data Nat (c :: i -> i -> Type) (d :: j -> j -> Type) (f :: i -> j) (g :: i -> j) -class Functor p (Nat p (->)) p => Category (p :: i -> i -> Type) +type Category :: (i -> i -> Type) -> Constraint +class Functor p (Nat p (->)) p => Category p class (Category dom, Category cod) => Functor (dom :: i -> i -> Type) (cod :: j -> j -> Type) (f :: i -> j) diff --git a/testsuite/tests/polykinds/T11480b.hs b/testsuite/tests/polykinds/T11480b.hs index 0ec19753a0..575df745de 100644 --- a/testsuite/tests/polykinds/T11480b.hs +++ b/testsuite/tests/polykinds/T11480b.hs @@ -14,6 +14,7 @@ {-# language DefaultSignatures #-} {-# language FunctionalDependencies #-} {-# language UndecidableSuperClasses #-} +{-# language StandaloneKindSignatures #-} -- This code, supplied by Edward Kmett, uses UndecidableSuperClasses along -- with a bunch of other stuff, so it's a useful stress test. @@ -39,6 +40,7 @@ instance Vacuous p a data Dict (p :: Constraint) where Dict :: p => Dict p +type Category :: (i -> i -> Type) -> Constraint class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> Type) where type Ob p :: i -> Constraint type Ob p = Vacuous p diff --git a/testsuite/tests/polykinds/T11520.hs b/testsuite/tests/polykinds/T11520.hs index 9c1d4fe1be..801a9254c4 100644 --- a/testsuite/tests/polykinds/T11520.hs +++ b/testsuite/tests/polykinds/T11520.hs @@ -1,11 +1,15 @@ {-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses, UndecidableInstances #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T11520 where +import Data.Kind (Type, Constraint) import GHC.Types hiding (TyCon) -data TypeRep (a :: k) +type TypeRep :: k -> Type +data TypeRep a +type Typeable :: k -> Constraint class Typeable k => Typeable (a :: k) where typeRep :: TypeRep a diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr index 11a81baf62..4f44d56796 100644 --- a/testsuite/tests/polykinds/T11520.stderr +++ b/testsuite/tests/polykinds/T11520.stderr @@ -1,5 +1,5 @@ -T11520.hs:15:77: error: +T11520.hs:19:77: error: • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’ • In the second argument of ‘Compose’, namely ‘g’ In the first argument of ‘Typeable’, namely ‘(Compose f g)’ diff --git a/testsuite/tests/polykinds/T11523.hs b/testsuite/tests/polykinds/T11523.hs index aff0f9ed90..0630c53a32 100644 --- a/testsuite/tests/polykinds/T11523.hs +++ b/testsuite/tests/polykinds/T11523.hs @@ -15,6 +15,7 @@ {-# language FunctionalDependencies #-} {-# language UndecidableSuperClasses #-} {-# language UndecidableInstances #-} +{-# language StandaloneKindSignatures #-} module T11523 where @@ -28,6 +29,7 @@ newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a } class Vacuous (a :: i) instance Vacuous a +type Category :: Cat i -> Constraint class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where type Op p :: Cat i type Op p = Y p diff --git a/testsuite/tests/polykinds/T12055.hs b/testsuite/tests/polykinds/T12055.hs index cabc2dfbba..2a348c0f35 100644 --- a/testsuite/tests/polykinds/T12055.hs +++ b/testsuite/tests/polykinds/T12055.hs @@ -6,6 +6,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} -- The code from the ticket lacked these extensions, -- but crashed the compiler with "GHC internal error" @@ -21,9 +22,11 @@ import GHC.Exts ( type (~~) ) type Cat k = k -> k -> Type +type Category :: Cat k -> Constraint class Category (p :: Cat k) where type Ob p :: k -> Constraint +type Functor :: (j -> k) -> Constraint class (Category (Dom f), Category (Cod f)) => Functor (f :: j -> k) where type Dom f :: Cat j type Cod f :: Cat k diff --git a/testsuite/tests/polykinds/T12055a.hs b/testsuite/tests/polykinds/T12055a.hs index ebc4dc7cad..e1fcd07663 100644 --- a/testsuite/tests/polykinds/T12055a.hs +++ b/testsuite/tests/polykinds/T12055a.hs @@ -6,6 +6,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances, FunctionalDependencies #-} @@ -21,9 +22,11 @@ import GHC.Exts ( type (~~) ) type Cat k = k -> k -> Type +type Category :: Cat k -> Constraint class Category (p :: Cat k) where type Ob p :: k -> Constraint +type Functor :: (j -> k) -> Constraint class (Category (Dom f), Category (Cod f)) => Functor (f :: j -> k) where type Dom f :: Cat j type Cod f :: Cat k diff --git a/testsuite/tests/polykinds/T12055a.stderr b/testsuite/tests/polykinds/T12055a.stderr index fb76dd4989..8274ab7179 100644 --- a/testsuite/tests/polykinds/T12055a.stderr +++ b/testsuite/tests/polykinds/T12055a.stderr @@ -1,5 +1,5 @@ -T12055a.hs:27:1: error: +T12055a.hs:30:1: error: • Non type-variable argument in the constraint: Category (Dom f) (Use FlexibleContexts to permit this) • In the context: (Category (Dom f), Category (Cod f)) diff --git a/testsuite/tests/polykinds/T13625.stderr b/testsuite/tests/polykinds/T13625.stderr index 98208fcde3..4e0d4b68d6 100644 --- a/testsuite/tests/polykinds/T13625.stderr +++ b/testsuite/tests/polykinds/T13625.stderr @@ -3,4 +3,3 @@ T13625.hs:5:11: error: • Data constructor ‘Y’ cannot be used here (it is defined and used in the same recursive group) • In the kind ‘Y’ - In the data type declaration for ‘X’ diff --git a/testsuite/tests/polykinds/T14270.hs b/testsuite/tests/polykinds/T14270.hs index d578be344e..cf8c238efe 100644 --- a/testsuite/tests/polykinds/T14270.hs +++ b/testsuite/tests/polykinds/T14270.hs @@ -8,16 +8,19 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T14270 (pattern App) where -import Data.Kind (Type) +import Data.Kind (Type, Constraint) import GHC.Fingerprint (Fingerprint, fingerprintFingerprints) import GHC.Types (RuntimeRep, TYPE, TyCon) -data (a :: k1) :~~: (b :: k2) where +type (:~~:) :: k1 -> k2 -> Type +data a :~~: b where HRefl :: a :~~: a -data TypeRep (a :: k) where +type TypeRep :: k -> Type +data TypeRep a where TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep] -> TypeRep (a :: k) @@ -63,7 +66,8 @@ pattern App :: forall k2 (t :: k2). () pattern App f x <- (splitApp -> Just (IsApp f x)) where App f x = mkTrApp f x -data IsApp (a :: k) where +type IsApp :: k -> Type +data IsApp a where IsApp :: forall k k' (f :: k' -> k) (x :: k'). () => TypeRep f -> TypeRep x -> IsApp (f x) @@ -91,13 +95,15 @@ bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) -> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type) bareArrow = undefined -data IsTYPE (a :: Type) where +type IsTYPE :: Type -> Type +data IsTYPE a where IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r) isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a) isTYPE = undefined -class Typeable (a :: k) where +type Typeable :: k -> Constraint +class Typeable a where typeRep :: Typeable a => TypeRep a typeRep = undefined diff --git a/testsuite/tests/polykinds/T14450.hs b/testsuite/tests/polykinds/T14450.hs index 8571829619..6e37bf96bd 100644 --- a/testsuite/tests/polykinds/T14450.hs +++ b/testsuite/tests/polykinds/T14450.hs @@ -1,6 +1,6 @@ {-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, GADTs, - AllowAmbiguousTypes, InstanceSigs #-} + AllowAmbiguousTypes, InstanceSigs, StandaloneKindSignatures #-} module T14450 where @@ -12,9 +12,11 @@ type a ~> b = TyFun a b -> Type type Cat ob = ob -> ob -> Type -type SameKind (a :: k) (b :: k) = (() :: Constraint) +type SameKind :: k -> k -> Constraint +type SameKind a b = () -type family Apply (f :: a ~> b) (x :: a) :: b where +type Apply :: (a ~> b) -> a -> b +type family Apply f x where Apply IddSym0 x = Idd x class Varpi (f :: i ~> j) where diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr index 927ae6a720..1f0d0a83ca 100644 --- a/testsuite/tests/polykinds/T14450.stderr +++ b/testsuite/tests/polykinds/T14450.stderr @@ -1,5 +1,5 @@ -T14450.hs:33:3: error: +T14450.hs:35:3: error: • Type indexes must match class instance head Expected: Dom @k @k (IddSym0 @k) Actual: Dom @* @* (IddSym0 @*) diff --git a/testsuite/tests/polykinds/T16247.stderr b/testsuite/tests/polykinds/T16247.stderr index 34a1319996..ff0f82919a 100644 --- a/testsuite/tests/polykinds/T16247.stderr +++ b/testsuite/tests/polykinds/T16247.stderr @@ -4,4 +4,3 @@ T16247.hs:9:13: error: are out of dependency order. Perhaps try this ordering: k (a :: k) (b :: k) • In the kind ‘forall a k (b :: k). SameKind a b -> Type’ - In the data type declaration for ‘Foo’ diff --git a/testsuite/tests/polykinds/T16247a.stderr b/testsuite/tests/polykinds/T16247a.stderr index ce75878f38..e6184da25a 100644 --- a/testsuite/tests/polykinds/T16247a.stderr +++ b/testsuite/tests/polykinds/T16247a.stderr @@ -5,4 +5,3 @@ T16247a.hs:21:21: error: k (p :: k) • In the kind ‘forall p k. (U1 :: k -> Type) p ~> Rep1 (U1 :: k -> Type) p’ - In the data type declaration for ‘From1U1Sym0’ diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr index e265866119..00bb3ba696 100644 --- a/testsuite/tests/polykinds/T16902.stderr +++ b/testsuite/tests/polykinds/T16902.stderr @@ -1,6 +1,9 @@ T16902.hs:11:10: error: - • Expected a type, but found something with kind ‘a1’ + • Couldn't match kind ‘k’ with ‘*’ + When matching kinds + a :: k + k :: * • In the type ‘F a’ In the definition of data constructor ‘MkF’ In the data declaration for ‘F’ diff --git a/testsuite/tests/polykinds/T6137.hs b/testsuite/tests/polykinds/T6137.hs index b3f0c02ba6..57a50d54ee 100644 --- a/testsuite/tests/polykinds/T6137.hs +++ b/testsuite/tests/polykinds/T6137.hs @@ -1,6 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} -{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} @@ -42,5 +42,6 @@ data instance In (F f) r x where D:R:InioFrx0 :: R:InioFrx o i f ~ In i o ('F i o f) -} -- Requires polymorphic recursion -data In' (f :: Code i o) :: (i -> Type) -> o -> Type where +type In' :: Code i o -> (i -> Type) -> (o -> Type) +data In' g r t where MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t diff --git a/testsuite/tests/polykinds/T7053.hs b/testsuite/tests/polykinds/T7053.hs index d45dbadaee..13d45fcfa5 100644 --- a/testsuite/tests/polykinds/T7053.hs +++ b/testsuite/tests/polykinds/T7053.hs @@ -2,6 +2,7 @@ module T7053 where +-- no standalone kind signature data TypeRep (a :: k) where TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b) diff --git a/testsuite/tests/polykinds/T7053.stderr b/testsuite/tests/polykinds/T7053.stderr new file mode 100644 index 0000000000..6ccfa947c1 --- /dev/null +++ b/testsuite/tests/polykinds/T7053.stderr @@ -0,0 +1,6 @@ + +T7053.hs:7:50: error: + • Occurs check: cannot construct the infinite kind: k ~ k -> k + • In the first argument of ‘TypeRep’, namely ‘(a b)’ + In the type ‘TypeRep (a b)’ + In the definition of data constructor ‘TyApp’ diff --git a/testsuite/tests/polykinds/T7053a.hs b/testsuite/tests/polykinds/T7053a.hs index d5ae04690b..5539d107d9 100644 --- a/testsuite/tests/polykinds/T7053a.hs +++ b/testsuite/tests/polykinds/T7053a.hs @@ -1,10 +1,10 @@ -{-# LANGUAGE PolyKinds, GADTs #-} +{-# LANGUAGE PolyKinds, GADTs, StandaloneKindSignatures #-} module T7053a where import Data.Kind (Type) --- This time with a fully-specified kind signature -data TypeRep (a :: k) :: Type where +type TypeRep :: k -> Type +data TypeRep a where TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b) diff --git a/testsuite/tests/polykinds/T9200.hs b/testsuite/tests/polykinds/T9200.hs index 63c934c91b..9eb0e4b617 100644 --- a/testsuite/tests/polykinds/T9200.hs +++ b/testsuite/tests/polykinds/T9200.hs @@ -1,31 +1,34 @@ {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FlexibleContexts, DataKinds, - TypeFamilies #-} + TypeFamilies, StandaloneKindSignatures #-} module T9200 where -import Data.Kind (Type) +import Data.Kind import Data.Proxy ------ --- test CUSK on classes - -class C (f :: k) (a :: k2) where +-- test SAKS on classes +type C :: k -> k2 -> Constraint +class C f a where c_meth :: D a => Proxy f -> Proxy a -> () - + class C () a => D a --------- ---- test CUSK on type synonyms +--- test SAKS on type synonyms data T1 a b c = MkT1 (S True b c) data T2 p q r = MkT2 (S p 5 r) data T3 x y q = MkT3 (S x y '()) -type S (f :: k1) (g :: k2) (h :: k3) = ((T1 f g h, T2 f g h, T3 f g h) :: Type) + +type S :: k1 -> k2 -> k3 -> Type +type S f g h = (T1 f g h, T2 f g h, T3 f g h) ---------- --- test CUSK on closed type families -type family F (a :: k) :: k where +-- test SAKS on closed type families +type F :: k -> k +type family F a where F True = False F False = True F x = x diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 74ab266308..7f2bbfd5aa 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -52,7 +52,7 @@ test('T6137', normal, compile,['']) test('T6093', normal, compile,['']) test('T6049', normal, compile,['']) test('T6129', normal, compile_fail,['']) -test('T7053', normal, compile,['']) +test('T7053', normal, compile_fail,['']) test('T7053a', normal, compile,['']) test('T7020', normal, compile,['']) test('T7022', normal, makefile_test, []) diff --git a/testsuite/tests/simplCore/should_compile/T14270a.hs b/testsuite/tests/simplCore/should_compile/T14270a.hs index d8cc497f62..7424d821f4 100644 --- a/testsuite/tests/simplCore/should_compile/T14270a.hs +++ b/testsuite/tests/simplCore/should_compile/T14270a.hs @@ -1,5 +1,5 @@ {-# LANGUAGE TypeApplications, ScopedTypeVariables, GADTs, RankNTypes, - PolyKinds, KindSignatures #-} + PolyKinds, StandaloneKindSignatures #-} {-# OPTIONS_GHC -O2 #-} -- We are provoking a bug in SpecConstr module T14270a where @@ -9,7 +9,8 @@ import Data.Proxy data T a = T1 (T a) | T2 -data K (a :: k) where +type K :: k -> Type +data K a where K1 :: K (a :: Type) K2 :: K a diff --git a/testsuite/tests/simplCore/should_compile/T16979b.hs b/testsuite/tests/simplCore/should_compile/T16979b.hs index d2b5712674..7d130b44c1 100644 --- a/testsuite/tests/simplCore/should_compile/T16979b.hs +++ b/testsuite/tests/simplCore/should_compile/T16979b.hs @@ -13,6 +13,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T16979 (strs) where import Control.Applicative @@ -159,7 +160,8 @@ iso :: (s -> a) -> (b -> t) -> Iso s t a b iso sa bt = dimap sa (fmap bt) {-# INLINE iso #-} -type family LookupParam (a :: k) (p :: Nat) :: Maybe Nat where +type LookupParam :: k -> Nat -> Maybe Nat +type family LookupParam a p where LookupParam (param (n :: Nat)) m = 'Nothing LookupParam (a (_ (m :: Nat))) n = IfEq m n ('Just 0) (MaybeAdd (LookupParam a n) 1) LookupParam (a _) n = MaybeAdd (LookupParam a n) 1 @@ -176,20 +178,24 @@ type family IfEq (a :: k) (b :: k) (t :: l) (f :: l) :: l where data Sub where Sub :: Nat -> k -> Sub -type family ReplaceArg (t :: k) (pos :: Nat) (to :: j) :: k where +type ReplaceArg :: k -> Nat -> j -> k +type family ReplaceArg t pos to where ReplaceArg (t a) 0 to = t to ReplaceArg (t a) pos to = ReplaceArg t (pos - 1) to a ReplaceArg t _ _ = t -type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where +type ReplaceArgs :: k -> [Sub] -> k +type family ReplaceArgs t subs where ReplaceArgs t '[] = t ReplaceArgs t ('Sub n arg ': ss) = ReplaceArgs (ReplaceArg t n arg) ss -type family ArgAt (t :: k) (n :: Nat) :: j where +type ArgAt :: k -> Nat -> j +type family ArgAt t n where ArgAt (t a) 0 = a ArgAt (t a) n = ArgAt t (n - 1) -type family Unify (a :: k) (b :: k) :: [Sub] where +type Unify :: k -> k -> [Sub] +type family Unify a b where Unify (p n _ 'PTag) a' = '[ 'Sub n a'] Unify (a x) (b y) = Unify x y ++ Unify a b Unify a a = '[] @@ -207,7 +213,8 @@ data PTag = PTag type family P :: Nat -> k -> PTag -> k type family Param :: Nat -> k where -type family Indexed (t :: k) (i :: Nat) :: k where +type Indexed :: k -> Nat -> k +type family Indexed t i where Indexed (t a) i = Indexed t (i + 1) (Param i) Indexed t _ = t diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs index abe2ddca3b..01df123b1a 100644 --- a/testsuite/tests/th/ClosedFam2TH.hs +++ b/testsuite/tests/th/ClosedFam2TH.hs @@ -1,10 +1,15 @@ -{-# LANGUAGE TemplateHaskell, TypeFamilies, PolyKinds, TypeApplications, TypeFamilyDependencies #-} +{-# LANGUAGE TemplateHaskell, TypeFamilies, PolyKinds, TypeApplications, TypeFamilyDependencies, + StandaloneKindSignatures #-} module ClosedFam2 where import Language.Haskell.TH -$( return [ ClosedTypeFamilyD +$( return [ KiSigD (mkName "Equals") + (ArrowT `AppT` VarT (mkName "k") `AppT` + (ArrowT `AppT` VarT (mkName "k") `AppT` + VarT (mkName "k"))) + , ClosedTypeFamilyD (TypeFamilyHead (mkName "Equals") [ KindedTV (mkName "a") (VarT (mkName "k")) @@ -26,7 +31,8 @@ a = (5 :: Int) b :: Equals Int Bool b = False -$( return [ ClosedTypeFamilyD +$( return [ KiSigD (mkName "Foo") (ArrowT `AppT` VarT (mkName "k") `AppT` StarT) + , ClosedTypeFamilyD (TypeFamilyHead (mkName "Foo") [ KindedTV (mkName "a") (VarT (mkName "k"))] diff --git a/testsuite/tests/th/T12045TH1.hs b/testsuite/tests/th/T12045TH1.hs index c16bab29f9..43db0069b6 100644 --- a/testsuite/tests/th/T12045TH1.hs +++ b/testsuite/tests/th/T12045TH1.hs @@ -1,11 +1,12 @@ -{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds - , TypeInType, TypeApplications, TypeFamilies #-} +{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, + StandaloneKindSignatures, TypeApplications, TypeFamilies #-} module T12045TH1 where import Data.Kind import Language.Haskell.TH hiding (Type) -$([d| type family F (a :: k) :: Type where +$([d| type F :: k -> Type + type family F a where F @Type Int = Bool F @(Type->Type) Maybe = Char |]) diff --git a/testsuite/tests/th/T12045TH1.stderr b/testsuite/tests/th/T12045TH1.stderr index aede24c7a0..b27c2dec0c 100644 --- a/testsuite/tests/th/T12045TH1.stderr +++ b/testsuite/tests/th/T12045TH1.stderr @@ -1,18 +1,21 @@ -T12045TH1.hs:(8,3)-(10,52): Splicing declarations - [d| type family F (a :: k) :: Type where +T12045TH1.hs:(8,3)-(11,52): Splicing declarations + [d| type F :: k -> Type + + type family F a where F @Type Int = Bool F @(Type -> Type) Maybe = Char |] ======> - type family F (a :: k) :: Type where + type F :: k -> Type + type family F a where F @Type Int = Bool F @(Type -> Type) Maybe = Char -T12045TH1.hs:13:3-31: Splicing declarations +T12045TH1.hs:14:3-31: Splicing declarations [d| data family D (a :: k) |] ======> data family D (a :: k) -T12045TH1.hs:15:3-40: Splicing declarations +T12045TH1.hs:16:3-40: Splicing declarations [d| data instance D @Type a = DBool |] ======> data instance D @Type a = DBool -T12045TH1.hs:17:3-50: Splicing declarations +T12045TH1.hs:18:3-50: Splicing declarations [d| data instance D @(Type -> Type) b = DChar |] ======> data instance D @(Type -> Type) b = DChar diff --git a/testsuite/tests/th/T12045TH2.hs b/testsuite/tests/th/T12045TH2.hs index 21d04cb826..7f28fe5326 100644 --- a/testsuite/tests/th/T12045TH2.hs +++ b/testsuite/tests/th/T12045TH2.hs @@ -1,5 +1,5 @@ -{-# LANGUAGE TemplateHaskell, TypeApplications, PolyKinds - , TypeFamilies, DataKinds #-} +{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, + StandaloneKindSignatures, TypeApplications, TypeFamilies #-} module T12045TH2 where @@ -7,7 +7,8 @@ import Data.Kind import Language.Haskell.TH hiding (Type) import System.IO -type family Foo (a :: k) :: Type where +type Foo :: k -> Type +type family Foo a where Foo @Type a = Bool type family Baz (a :: k) @@ -16,13 +17,16 @@ type instance Baz @(Type->Type->Type) a = Char $( do FamilyI foo@(ClosedTypeFamilyD (TypeFamilyHead _ tvbs1 res1 m_kind1) [TySynEqn (Just bndrs1) (AppT _ lhs1) rhs1]) [] <- reify ''Foo + sig1 <- reifyType ''Foo FamilyI baz@(OpenTypeFamilyD (TypeFamilyHead _ tvbs2 res2 m_kind2)) [inst@(TySynInstD (TySynEqn (Just bndrs2) (AppT _ lhs2) rhs2))] <- reify ''Baz + runIO $ putStrLn $ pprint sig1 runIO $ putStrLn $ pprint foo runIO $ putStrLn $ pprint baz runIO $ putStrLn $ pprint inst runIO $ hFlush stdout - return [ ClosedTypeFamilyD + return [ KiSigD (mkName "Foo'") sig1 + , ClosedTypeFamilyD (TypeFamilyHead (mkName "Foo'") tvbs1 res1 m_kind1) [TySynEqn (Just bndrs1) (AppT (ConT (mkName "Foo'")) lhs1) rhs1] , OpenTypeFamilyD diff --git a/testsuite/tests/th/T12045TH2.stderr b/testsuite/tests/th/T12045TH2.stderr index ce626e5e01..5516e7d480 100644 --- a/testsuite/tests/th/T12045TH2.stderr +++ b/testsuite/tests/th/T12045TH2.stderr @@ -1,3 +1,4 @@ +forall (k_0 :: *) . k_0 -> * type family T12045TH2.Foo (a_0 :: k_1) :: * where forall (a_2 :: *). T12045TH2.Foo (a_2 :: *) = GHC.Types.Bool type family T12045TH2.Baz (a_0 :: k_1) :: * diff --git a/testsuite/tests/th/T12646.hs b/testsuite/tests/th/T12646.hs index b3ba86e54c..507b1ba8bf 100644 --- a/testsuite/tests/th/T12646.hs +++ b/testsuite/tests/th/T12646.hs @@ -1,13 +1,15 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T12646 where import Language.Haskell.TH hiding (Type) import System.IO import Data.Kind (Type) -type family F (a :: k) :: Type where +type F :: k -> Type +type family F a where F (a :: Type -> Type) = Int F (a :: k) = Char diff --git a/testsuite/tests/th/T15243.hs b/testsuite/tests/th/T15243.hs index 8b366404c8..61d2aabed2 100644 --- a/testsuite/tests/th/T15243.hs +++ b/testsuite/tests/th/T15243.hs @@ -2,12 +2,14 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} {-# OPTIONS_GHC -ddump-splices #-} module T15243 where data Unit = Unit -$([d| type family F (a :: k) :: k where +$([d| type F :: k -> k + type family F a where F 'Unit = 'Unit F '(,) = '(,) F '[] = '[] diff --git a/testsuite/tests/th/T15243.stderr b/testsuite/tests/th/T15243.stderr index 4e50186c1f..59f921ab8a 100644 --- a/testsuite/tests/th/T15243.stderr +++ b/testsuite/tests/th/T15243.stderr @@ -1,12 +1,15 @@ -T15243.hs:(10,3)-(15,6): Splicing declarations - [d| type family F (a :: k) :: k where - F 'Unit = 'Unit - F '(,) = '(,) +T15243.hs:(11,3)-(17,6): Splicing declarations + [d| type F :: k -> k + + type family F a where + F 'Unit = 'Unit + F '(,) = '(,) F '[] = '[] - F '(:) = '(:) |] + F '(:) = '(:) |] ======> - type family F (a :: k) :: k where - F 'Unit = 'Unit - F '(,) = '(,) + type F :: k -> k + type family F a where + F 'Unit = 'Unit + F '(,) = '(,) F '[] = '[] - F '(:) = '(:) + F '(:) = '(:) diff --git a/testsuite/tests/typecheck/should_compile/SplitWD.hs b/testsuite/tests/typecheck/should_compile/SplitWD.hs index 5281cdbf0e..37a766ecef 100644 --- a/testsuite/tests/typecheck/should_compile/SplitWD.hs +++ b/testsuite/tests/typecheck/should_compile/SplitWD.hs @@ -1,5 +1,5 @@ {-# LANGUAGE ScopedTypeVariables, TypeOperators, DataKinds, PolyKinds, - TypeFamilies, GADTs, StandaloneDeriving #-} + TypeFamilies, GADTs, StandaloneDeriving, StandaloneKindSignatures #-} module SplitWD where @@ -17,7 +17,8 @@ data Vec :: Type -> Nat -> Type where (:>) :: a -> Vec a n -> Vec a (Succ n) infixr 5 :> -type family (xs :: Vec a n) +++ (ys :: Vec a m) :: Vec a (n + m) where +type (+++) :: Vec a n -> Vec a m -> Vec a (n + m) +type family xs +++ ys where VNil +++ ys = ys (x :> xs) +++ ys = x :> (xs +++ ys) infixr 5 +++ diff --git a/testsuite/tests/typecheck/should_compile/T11524.hs b/testsuite/tests/typecheck/should_compile/T11524.hs index d6e2adf4f4..90a3ecbc84 100644 --- a/testsuite/tests/typecheck/should_compile/T11524.hs +++ b/testsuite/tests/typecheck/should_compile/T11524.hs @@ -2,10 +2,14 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T11524 where -data AType (a :: k) where +import Data.Kind (Type) + +type AType :: k -> Type +data AType a where AMaybe :: AType Maybe AInt :: AType Int AApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). diff --git a/testsuite/tests/typecheck/should_compile/T11811.hs b/testsuite/tests/typecheck/should_compile/T11811.hs index e3e0f810b3..c96ffb97b7 100644 --- a/testsuite/tests/typecheck/should_compile/T11811.hs +++ b/testsuite/tests/typecheck/should_compile/T11811.hs @@ -1,8 +1,10 @@ {-# LANGUAGE PolyKinds, GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T11811 where import Data.Kind -data Test (a :: x) (b :: x) :: x -> Type +type Test :: x -> x -> x -> Type +data Test a b c where K :: Test Int Bool Double diff --git a/testsuite/tests/typecheck/should_compile/T12919.hs b/testsuite/tests/typecheck/should_compile/T12919.hs index 778abfa1e7..38bbda2ccf 100644 --- a/testsuite/tests/typecheck/should_compile/T12919.hs +++ b/testsuite/tests/typecheck/should_compile/T12919.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, ConstraintKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T12919 where @@ -12,7 +13,8 @@ data V :: N -> Type where type family VC (n :: N) :: Type where VC Z = Type -type family VF (xs :: V n) (f :: VC n) :: Type where +type VF :: V n -> VC n -> Type +type family VF xs f where VF VZ f = f data Dict c where diff --git a/testsuite/tests/typecheck/should_compile/T13333.hs b/testsuite/tests/typecheck/should_compile/T13333.hs index 9a84e87265..ce6af77e3d 100644 --- a/testsuite/tests/typecheck/should_compile/T13333.hs +++ b/testsuite/tests/typecheck/should_compile/T13333.hs @@ -6,14 +6,16 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T13333 where import Data.Data -import GHC.Exts (Constraint) +import Data.Kind data T (phantom :: k) = T -data D (p :: k -> Constraint) (x :: j) where +type D :: (k -> Constraint) -> j -> Type +data D p x where D :: forall k (p :: k -> Constraint) (x :: k). p x => D p x class Possibly p x where diff --git a/testsuite/tests/typecheck/should_compile/T13822.hs b/testsuite/tests/typecheck/should_compile/T13822.hs index 88c14c2aff..376c01491a 100644 --- a/testsuite/tests/typecheck/should_compile/T13822.hs +++ b/testsuite/tests/typecheck/should_compile/T13822.hs @@ -1,5 +1,6 @@ {-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, - TypeFamilyDependencies, RankNTypes, LambdaCase, EmptyCase #-} + TypeFamilyDependencies, RankNTypes, LambdaCase, EmptyCase, + StandaloneKindSignatures #-} module T13822 where @@ -18,14 +19,16 @@ type family IK STAR = Type IK (a:>b) = IK a -> IK b +type I :: Ty k -> IK k type family - I (t :: Ty k) = (res :: IK k) | res -> t where + I t = res | res -> t where I TInt = Int I TBool = Bool I TMaybe = Maybe I (TApp f a) = (I f) (I a) -data TyRep (k :: KIND) (t :: Ty k) where +type TyRep :: forall (k :: KIND) -> Ty k -> Type +data TyRep k t where TyInt :: TyRep STAR TInt TyBool :: TyRep STAR TBool TyMaybe :: TyRep (STAR:>STAR) TMaybe diff --git a/testsuite/tests/typecheck/should_compile/T13871.hs b/testsuite/tests/typecheck/should_compile/T13871.hs index 623923eaca..53e026e194 100644 --- a/testsuite/tests/typecheck/should_compile/T13871.hs +++ b/testsuite/tests/typecheck/should_compile/T13871.hs @@ -3,6 +3,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds, PolyKinds #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE StandaloneKindSignatures #-} module Foo where import Data.Kind @@ -11,5 +12,7 @@ data Foo (a :: Type) (b :: Type) where MkFoo :: (a ~ Int, b ~ Char) => Foo a b data family Sing (a :: k) -data SFoo (z :: Foo a b) where + +type SFoo :: Foo a b -> Type +data SFoo z where SMkFoo :: SFoo MkFoo diff --git a/testsuite/tests/typecheck/should_compile/T13879.hs b/testsuite/tests/typecheck/should_compile/T13879.hs index 2e10c472fb..e3f9e4bbed 100644 --- a/testsuite/tests/typecheck/should_compile/T13879.hs +++ b/testsuite/tests/typecheck/should_compile/T13879.hs @@ -4,13 +4,15 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds, PolyKinds #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE StandaloneKindSignatures #-} module Bug where import Data.Kind data family Sing (a :: k) -data HR (a :: j) (b :: k) where +type HR :: j -> k -> Type +data HR a b where HRefl :: HR a a data instance Sing (z :: HR a b) where diff --git a/testsuite/tests/typecheck/should_compile/T14366.hs b/testsuite/tests/typecheck/should_compile/T14366.hs index 56abad5d30..8a78468cc4 100644 --- a/testsuite/tests/typecheck/should_compile/T14366.hs +++ b/testsuite/tests/typecheck/should_compile/T14366.hs @@ -1,13 +1,19 @@ {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T14366 where + import Data.Kind import Data.Type.Equality -type family Cast (a :: Type) (b :: Type) (e :: a :~: b) (x :: a) :: b where +type Cast :: forall (a :: Type) (b :: Type) -> a :~: b -> a -> b +type family Cast a b e x where Cast _ _ Refl x = x -type family F (a :: Type) :: Type where +type F :: Type -> Type +type family F a where F (a :: _) = a diff --git a/testsuite/tests/typecheck/should_compile/T14451.hs b/testsuite/tests/typecheck/should_compile/T14451.hs index a67ce74537..7987a722ea 100644 --- a/testsuite/tests/typecheck/should_compile/T14451.hs +++ b/testsuite/tests/typecheck/should_compile/T14451.hs @@ -1,4 +1,4 @@ -{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-} +{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances, StandaloneKindSignatures #-} module T14451 where import Data.Kind @@ -9,8 +9,8 @@ type a ~> b = TyFun a b -> Type type Cat ob = ob -> ob -> Type -type family - Apply (f :: a ~> b) (x :: a) :: b where +type Apply :: (a ~> b) -> a -> b +type family Apply f x where Apply (CompSym2 f g) a = Comp f g a data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c) @@ -23,6 +23,6 @@ class Varpi (f :: i ~> j) where varpa :: Dom f a a' -> Cod f (f·a) (f·a') -type family - Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where +type Comp :: (k1 ~> k) -> (k2 ~> k1) -> k2 -> k +type family Comp f g a where Comp f g a = f · (g · a) diff --git a/testsuite/tests/typecheck/should_compile/T6018.hs b/testsuite/tests/typecheck/should_compile/T6018.hs index 8605cec1a7..99b99d9294 100644 --- a/testsuite/tests/typecheck/should_compile/T6018.hs +++ b/testsuite/tests/typecheck/should_compile/T6018.hs @@ -5,6 +5,7 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T6018 where @@ -199,6 +200,7 @@ class Kcl a b where -- Declaring kind injectivity. Here we only claim that knowing the RHS -- determines the LHS kind but not the type. +type L :: k1 -> k2 type family L (a :: k1) = (r :: k2) | r -> k1 where L 'True = Int L 'False = Int diff --git a/testsuite/tests/typecheck/should_compile/T6018.stderr b/testsuite/tests/typecheck/should_compile/T6018.stderr index c4baec422d..9423a0e706 100644 --- a/testsuite/tests/typecheck/should_compile/T6018.stderr +++ b/testsuite/tests/typecheck/should_compile/T6018.stderr @@ -2,10 +2,10 @@ [2 of 3] Compiling T6018a ( T6018a.hs, T6018a.o ) [3 of 3] Compiling T6018 ( T6018.hs, T6018.o ) -T6018.hs:108:5: warning: +T6018.hs:109:5: warning: Type family instance equation is overlapped: - Foo Bool = Bool -- Defined at T6018.hs:108:5 + Foo Bool = Bool -- Defined at T6018.hs:109:5 -T6018.hs:115:5: warning: +T6018.hs:116:5: warning: Type family instance equation is overlapped: - Bar Bool = Char -- Defined at T6018.hs:115:5 + Bar Bool = Char -- Defined at T6018.hs:116:5 diff --git a/testsuite/tests/typecheck/should_compile/T7503a.hs b/testsuite/tests/typecheck/should_compile/T7503a.hs index 61c0fb34e2..a3c66952ec 100644 --- a/testsuite/tests/typecheck/should_compile/T7503a.hs +++ b/testsuite/tests/typecheck/should_compile/T7503a.hs @@ -1,11 +1,13 @@ -{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-} +{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, + StandaloneKindSignatures, GADTs #-} module T7503a where import Data.Kind import GHC.Exts hiding (Any) data WrappedType = forall a. WrapType a - data A :: WrappedType -> Type where + type A :: WrappedType -> Type + data A a where MkA :: forall (a :: Type). AW a -> A (WrapType a) type AW (a :: k) = A (WrapType a) diff --git a/testsuite/tests/typecheck/should_compile/T9151.hs b/testsuite/tests/typecheck/should_compile/T9151.hs index 351c563b67..a3cbee4a24 100644 --- a/testsuite/tests/typecheck/should_compile/T9151.hs +++ b/testsuite/tests/typecheck/should_compile/T9151.hs @@ -1,9 +1,12 @@ -{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-} +{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, + StandaloneKindSignatures #-} module T9151 where +import Data.Kind import Data.Proxy +type PEnum :: KProxy a -> Constraint class PEnum (kproxy :: KProxy a) where type ToEnum (x :: a) :: Bool type ToEnum x = TEHelper diff --git a/testsuite/tests/typecheck/should_compile/tc269.hs b/testsuite/tests/typecheck/should_compile/tc269.hs index 3ac88ce8e9..5f133462b9 100644 --- a/testsuite/tests/typecheck/should_compile/tc269.hs +++ b/testsuite/tests/typecheck/should_compile/tc269.hs @@ -1,5 +1,6 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} module Tc269 where import GHC.Types @@ -18,4 +19,6 @@ type TSyn = T -- everything. Need an explicit type signature. data K (a :: k) = K data S (p :: forall k. k -> Type) = S (SSyn K) -type SSyn = (S :: (forall k. k -> Type) -> Type) + +type SSyn :: (forall k. k -> Type) -> Type +type SSyn = S diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs b/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs index 0a68a69a38..101bae825a 100644 --- a/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs +++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs @@ -1,11 +1,13 @@ -- inspired by comment:25 on #12708 -{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE PolyKinds, StandaloneKindSignatures #-} module LevPolyBounded where +import Data.Kind import GHC.Exts -class XBounded (a :: TYPE r) where +type XBounded :: TYPE r -> Constraint +class XBounded a where minBound :: a maxBound :: a diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr index afa8330765..2f428804ac 100644 --- a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr +++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr @@ -1,10 +1,10 @@ -LevPolyBounded.hs:10:15: error: +LevPolyBounded.hs:12:15: error: • Expected a type, but ‘a’ has kind ‘TYPE r’ • In the type signature: LevPolyBounded.minBound :: a In the class declaration for ‘XBounded’ -LevPolyBounded.hs:11:15: error: +LevPolyBounded.hs:13:15: error: • Expected a type, but ‘a’ has kind ‘TYPE r’ • In the type signature: LevPolyBounded.maxBound :: a In the class declaration for ‘XBounded’ diff --git a/testsuite/tests/typecheck/should_fail/T12785b.hs b/testsuite/tests/typecheck/should_fail/T12785b.hs index 951b04c6cd..6de914d2b3 100644 --- a/testsuite/tests/typecheck/should_fail/T12785b.hs +++ b/testsuite/tests/typecheck/should_fail/T12785b.hs @@ -1,6 +1,7 @@ {-# LANGUAGE RankNTypes, TypeOperators, ViewPatterns #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds, PolyKinds, GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T12785b where @@ -13,7 +14,8 @@ data HTree n a where Leaf :: HTree (S n) a Branch :: a -> HTree n (HTree (S n) a) -> HTree (S n) a -data STree (n ::Peano) :: forall a . (a -> Type) -> HTree n a -> Type where +type STree :: forall (n :: Peano) -> forall a. (a -> Type) -> HTree n a -> Type +data STree n f s where SPoint :: f a -> STree Z f (Point a) SLeaf :: STree (S n) f Leaf SBranch :: f a -> STree n (STree (S n) f) stru -> STree (S n) f (a `Branch` stru) @@ -33,6 +35,7 @@ hmap f (Point a) = Point (f a) hmap f Leaf = Leaf hmap f (a `Branch` tr) = f a `Branch` hmap (hmap f) tr -type family Payload (n :: Peano) (s :: HTree n x) :: x where +type Payload :: forall x. forall (n :: Peano) (s :: HTree n x) -> x +type family Payload n s where Payload Z (Point a) = a Payload (S n) (a `Branch` stru) = a diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr index 44937c3c45..18c0964894 100644 --- a/testsuite/tests/typecheck/should_fail/T12785b.stderr +++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr @@ -1,5 +1,5 @@ -T12785b.hs:29:63: error: +T12785b.hs:31:63: error: • Could not deduce: Payload ('S n) (Payload n s1) ~ s arising from a use of ‘SBranchX’ from the context: m ~ 'S n @@ -7,13 +7,13 @@ T12785b.hs:29:63: error: Branch :: forall a (n :: Peano). a -> HTree n (HTree ('S n) a) -> HTree ('S n) a, in an equation for ‘nest’ - at T12785b.hs:29:7-51 + at T12785b.hs:31:7-51 ‘s’ is a rigid type variable bound by a pattern with constructor: Hide :: forall a (n :: Peano) (f :: a -> *) (s :: HTree n a). STree n f s -> Hidden n f, in an equation for ‘nest’ - at T12785b.hs:29:7-12 + at T12785b.hs:31:7-12 • In the second argument of ‘($)’, namely ‘a `SBranchX` tr’ In the expression: Hide $ a `SBranchX` tr In an equation for ‘nest’: @@ -21,7 +21,7 @@ T12785b.hs:29:63: error: = Hide $ a `SBranchX` tr • Relevant bindings include tr :: STree n (STree ('S n) (STree ('S ('S n)) f)) s1 - (bound at T12785b.hs:29:49) - a :: STree ('S m) f s (bound at T12785b.hs:29:12) + (bound at T12785b.hs:31:49) + a :: STree ('S m) f s (bound at T12785b.hs:31:12) nest :: HTree m (Hidden ('S m) f) -> Hidden m (STree ('S m) f) - (bound at T12785b.hs:27:1) + (bound at T12785b.hs:29:1) diff --git a/testsuite/tests/typecheck/should_fail/T15552a.hs b/testsuite/tests/typecheck/should_fail/T15552a.hs index 86c71dc9c0..71e41b3f1a 100644 --- a/testsuite/tests/typecheck/should_fail/T15552a.hs +++ b/testsuite/tests/typecheck/should_fail/T15552a.hs @@ -1,5 +1,5 @@ {-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-} -{-# LANGUAGE TypeInType, TypeFamilies #-} +{-# LANGUAGE TypeFamilies, StandaloneKindSignatures #-} {- # LANGUAGE UndecidableInstances #-} module T15552 where @@ -21,8 +21,9 @@ type family GetEntryOfVal (eov :: EntryOfVal v kvs) where GetEntryOfVal ('EntryOfVal e) = e -type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs - where FirstEntryOfVal v (_ : kvs) +type FirstEntryOfVal :: forall (v :: Type) (kvs :: [Type]) -> EntryOfVal v kvs +type family FirstEntryOfVal v kvs where + FirstEntryOfVal v (_ : kvs) = 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs))) --type instance FirstEntryOfVal v (_ : kvs) -- = 'EntryOfVal ('There (GetEntryOfVal (FirstEntryOfVal v kvs))) diff --git a/testsuite/tests/typecheck/should_fail/T15552a.stderr b/testsuite/tests/typecheck/should_fail/T15552a.stderr index f24c6d1285..c61a6f5cb4 100644 --- a/testsuite/tests/typecheck/should_fail/T15552a.stderr +++ b/testsuite/tests/typecheck/should_fail/T15552a.stderr @@ -1,19 +1,19 @@ -T15552a.hs:25:9: error: +T15552a.hs:26:3: error: • Illegal nested type family application ‘EntryOfValKey (FirstEntryOfVal v kvs)’ (Use UndecidableInstances to permit this) • In the equations for closed type family ‘FirstEntryOfVal’ In the type family declaration for ‘FirstEntryOfVal’ -T15552a.hs:25:9: error: +T15552a.hs:26:3: error: • Illegal nested type family application ‘EntryOfValKey (FirstEntryOfVal v kvs)’ (Use UndecidableInstances to permit this) • In the equations for closed type family ‘FirstEntryOfVal’ In the type family declaration for ‘FirstEntryOfVal’ -T15552a.hs:25:9: error: +T15552a.hs:26:3: error: • Illegal nested type family application ‘GetEntryOfVal (FirstEntryOfVal v kvs)’ (Use UndecidableInstances to permit this) diff --git a/testsuite/tests/typecheck/should_fail/T16255.hs b/testsuite/tests/typecheck/should_fail/T16255.hs index ef2f0a9cb6..f9805a1b4e 100644 --- a/testsuite/tests/typecheck/should_fail/T16255.hs +++ b/testsuite/tests/typecheck/should_fail/T16255.hs @@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T16255 where import Data.Kind @@ -17,5 +18,6 @@ data family D1 :: forall k. k -> Type -- instances permit oversaturation in their equations. data instance D1 @Bool :: Bool -> Type +type F2 :: j -> forall k. Either j k type family F2 (x :: j) :: forall k. Either j k where F2 5 @Symbol = Left 4 diff --git a/testsuite/tests/typecheck/should_fail/T16255.stderr b/testsuite/tests/typecheck/should_fail/T16255.stderr index 74379a316c..21e2328e4f 100644 --- a/testsuite/tests/typecheck/should_fail/T16255.stderr +++ b/testsuite/tests/typecheck/should_fail/T16255.stderr @@ -1,10 +1,10 @@ -T16255.hs:13:3: error: +T16255.hs:14:3: error: • Illegal oversaturated visible kind argument: ‘@Bool’ • In the equations for closed type family ‘F1’ In the type family declaration for ‘F1’ -T16255.hs:21:3: error: +T16255.hs:23:3: error: • Illegal oversaturated visible kind argument: ‘@Symbol’ • In the equations for closed type family ‘F2’ In the type family declaration for ‘F2’ diff --git a/testsuite/tests/typecheck/should_fail/T7892.hs b/testsuite/tests/typecheck/should_fail/T7892.hs index 3e9bad3b69..ae71e645c9 100644 --- a/testsuite/tests/typecheck/should_fail/T7892.hs +++ b/testsuite/tests/typecheck/should_fail/T7892.hs @@ -1,7 +1,11 @@ {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} module T7892 where -class C (f :: * -> *) where - type F (f :: *) :: * +import Data.Kind + +type C :: (Type -> Type) -> Constraint +class C f where + type F (f :: Type) :: Type diff --git a/testsuite/tests/typecheck/should_fail/T7892.stderr b/testsuite/tests/typecheck/should_fail/T7892.stderr index fa332c745e..3fbca2ce8d 100644 --- a/testsuite/tests/typecheck/should_fail/T7892.stderr +++ b/testsuite/tests/typecheck/should_fail/T7892.stderr @@ -1,4 +1,4 @@ -T7892.hs:5:4: error: +T7892.hs:9:4: error: • Expected kind ‘* -> *’, but ‘f’ has kind ‘*’ • In the associated type family declaration for ‘F’ diff --git a/testsuite/tests/typecheck/should_fail/T9201.hs b/testsuite/tests/typecheck/should_fail/T9201.hs index 7702fa369c..463003602e 100644 --- a/testsuite/tests/typecheck/should_fail/T9201.hs +++ b/testsuite/tests/typecheck/should_fail/T9201.hs @@ -1,6 +1,10 @@ -{-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds, FunctionalDependencies, MultiParamTypeClasses, + StandaloneKindSignatures #-} module T9201 where -class MonoidalCCC (f :: x -> y) (d :: y -> y -> *) | f -> d where +import Data.Kind + +type MonoidalCCC :: (x -> y) -> (y -> y -> Type) -> Constraint +class MonoidalCCC f d | f -> d where ret :: d a (f a) diff --git a/testsuite/tests/typecheck/should_fail/T9201.stderr b/testsuite/tests/typecheck/should_fail/T9201.stderr index 5e8f0173c5..3e1f8eb5ed 100644 --- a/testsuite/tests/typecheck/should_fail/T9201.stderr +++ b/testsuite/tests/typecheck/should_fail/T9201.stderr @@ -1,5 +1,5 @@ -T9201.hs:6:17: error: +T9201.hs:10:17: error: • Expected kind ‘x’, but ‘a’ has kind ‘y’ • In the first argument of ‘f’, namely ‘a’ In the second argument of ‘d’, namely ‘(f a)’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr index c868a1321e..4afc740096 100644 --- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr @@ -2,4 +2,3 @@ UnliftedNewtypesFamilyKindFail1.hs:11:31: error: • Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’ • In the kind ‘5’ - In the data family declaration for ‘DF’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs index f5d134e3b1..c53c028f53 100644 --- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs @@ -3,13 +3,14 @@ {-# LANGUAGE UnliftedNewtypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE StandaloneKindSignatures #-} module UnliftedNewtypesLevityBinder where import GHC.Types (RuntimeRep,TYPE,Coercible) -newtype Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r where +type Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r +newtype Ident a where IdentC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a bad :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr index 90cf5b23aa..0025b444bf 100644 --- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr @@ -1,4 +1,5 @@ -UnliftedNewtypesLevityBinder.hs:16:7: + +UnliftedNewtypesLevityBinder.hs:17:7: error: Cannot use function with levity-polymorphic arguments: UnliftedNewtypesLevityBinder.IdentC :: a -> Ident a Levity-polymorphic arguments: a :: TYPE r diff --git a/testsuite/tests/typecheck/should_fail/tcfail225.hs b/testsuite/tests/typecheck/should_fail/tcfail225.hs index c01f49fdd1..39cfbfaf43 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail225.hs +++ b/testsuite/tests/typecheck/should_fail/tcfail225.hs @@ -1,5 +1,4 @@ {-# LANGUAGE PolyKinds, GADTs #-} -{-# LANGUAGE NoCUSKs #-} module TcFail225 where diff --git a/testsuite/tests/typecheck/should_fail/tcfail225.stderr b/testsuite/tests/typecheck/should_fail/tcfail225.stderr index 5a3ba3681f..7eec5ae517 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail225.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail225.stderr @@ -1,5 +1,5 @@ -tcfail225.hs:9:19: error: +tcfail225.hs:8:19: error: • Expected kind ‘k -> *’, but ‘Maybe’ has kind ‘* -> *’ • In the first argument of ‘T’, namely ‘Maybe’ In the type ‘T Maybe (m a)’ diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs index f81367268b..b94b4a4649 100644 --- a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs @@ -6,8 +6,9 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE UnboxedTuples #-} {-# LANGUAGE UnboxedSums #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} import GHC.Int (Int(I#)) import GHC.Word (Word(W#)) @@ -23,11 +24,12 @@ main = case (IdentityC 5#) of print (maybeInt# 12 increment# (Maybe# (# 42# | #))) print (maybeInt# 27 increment# (Maybe# (# | (# #) #))) -newtype Identity :: forall (r :: RuntimeRep). TYPE r -> TYPE r where +type Identity :: forall (r :: RuntimeRep). TYPE r -> TYPE r +newtype Identity a where IdentityC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity a -newtype Maybe# :: forall (r :: RuntimeRep). - TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where +type Maybe# :: forall (r :: RuntimeRep). TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) +newtype Maybe# a where Maybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a maybeInt# :: a -> (Int# -> a) -> Maybe# Int# -> a |