diff options
Diffstat (limited to 'testsuite/tests/polykinds')
60 files changed, 149 insertions, 142 deletions
diff --git a/testsuite/tests/polykinds/MonoidsTF.hs b/testsuite/tests/polykinds/MonoidsTF.hs index 365c3766bc..8e3b378046 100644 --- a/testsuite/tests/polykinds/MonoidsTF.hs +++ b/testsuite/tests/polykinds/MonoidsTF.hs @@ -12,13 +12,15 @@ {-# LANGUAGE TypeFamilies #-} module Main where + +import Data.Kind import Control.Monad (Monad(..), join, ap, liftM) import Data.Monoid (Monoid(..)) import Data.Semigroup (Semigroup(..)) -- First we define the type class Monoidy: -class Monoidy (to :: k0 -> k1 -> *) (m :: k1) where +class Monoidy (to :: k0 -> k1 -> Type) (m :: k1) where type MComp to m :: k1 -> k1 -> k0 type MId to m :: k0 munit :: MId to m `to` m diff --git a/testsuite/tests/polykinds/PolyKinds10.hs b/testsuite/tests/polykinds/PolyKinds10.hs index b023fd092f..70c5d70606 100644 --- a/testsuite/tests/polykinds/PolyKinds10.hs +++ b/testsuite/tests/polykinds/PolyKinds10.hs @@ -9,6 +9,7 @@ module Main where +import Data.Kind -- Type-level peano naturals (value-level too, but we don't use those) data Nat = Ze | Su Nat @@ -18,15 +19,15 @@ type T1 = Su T0 type T2 = Su T1 -- (!) at the type level -type family El (n :: Nat) (l :: [*]) :: * +type family El (n :: Nat) (l :: [Type]) :: Type type instance El Ze (h ': t) = h type instance El (Su n) (h ': t) = El n t {- -- The following might be useful, but are not used at the moment -- ($) at the type level (well, not quite ($), in fact...) -class Apply (fs :: [*]) (es :: [*]) where - type ApplyT (fs :: [*]) (es :: [*]) :: [*] +class Apply (fs :: [Type]) (es :: [Type]) where + type ApplyT (fs :: [Type]) (es :: [Type]) :: [Type] apply :: ListV fs -> ListV es -> ListV (ApplyT fs es) instance Apply '[] '[] where @@ -39,11 +40,11 @@ instance (Apply fs es) => Apply ((e1 -> e2) ': fs) (e1 ': es) where -} -- Value mirror for the list kind -data ListV :: [*] -> * where +data ListV :: [Type] -> Type where NilV :: ListV '[] ConsV :: a -> ListV t -> ListV (a ': t) -data ListV2 :: [[*]] -> * where +data ListV2 :: [[Type]] -> Type where NilV2 :: ListV2 '[] ConsV2 :: ListV a -> ListV2 t -> ListV2 (a ': t) @@ -53,26 +54,26 @@ listv1 = ConsV 3 NilV listv2 :: ListV2 ((Int ': '[]) ': '[]) listv2 = ConsV2 listv1 NilV2 ---data ListVX :: Maybe -> * where +--data ListVX :: Maybe -> Type where -data TripleV :: (*, * -> *, *) -> * where +data TripleV :: (Type, Type -> Type, Type) -> Type where TripleV :: a -> c -> TripleV '(a, [], c) -- Value mirror for the Nat kind -data NatV :: Nat -> * where +data NatV :: Nat -> Type where ZeW :: NatV Ze SuW :: NatV n -> NatV (Su n) -- Generic universe data MultiP x = UNIT - | KK x -- wish I could just write * instead of x + | KK x -- wish I could just write Type instead of x | SUM (MultiP x) (MultiP x) | PROD (MultiP x) (MultiP x) | PAR Nat | REC -- Universe interpretation -data Interprt :: MultiP * -> [*] -> * -> * where +data Interprt :: MultiP Type -> [Type] -> Type -> Type where Unit :: Interprt UNIT lp r K :: x -> Interprt (KK x) lp r L :: Interprt a lp r -> Interprt (SUM a b) lp r @@ -83,13 +84,13 @@ data Interprt :: MultiP * -> [*] -> * -> * where -- Embedding values into the universe class Generic a where - type Rep a :: MultiP * - type Es a :: [*] + type Rep a :: MultiP Type + type Es a :: [Type] from :: a -> Interprt (Rep a) (Es a) a to :: Interprt (Rep a) (Es a) a -> a -- Parameter map over the universe -class PMap (rep :: MultiP *) where +class PMap (rep :: MultiP Type) where pmap :: (forall n. NatV n -> El n lp1 -> El n lp2) -> (r -> s) -> Interprt rep lp1 r -> Interprt rep lp2 s diff --git a/testsuite/tests/polykinds/SigTvKinds3.hs b/testsuite/tests/polykinds/SigTvKinds3.hs index b27be2e9c6..7c9dace054 100644 --- a/testsuite/tests/polykinds/SigTvKinds3.hs +++ b/testsuite/tests/polykinds/SigTvKinds3.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, ExplicitForAll, TypeInType #-} +{-# LANGUAGE GADTs, ExplicitForAll, PolyKinds #-} module SigTvKinds3 where diff --git a/testsuite/tests/polykinds/T10134a.hs b/testsuite/tests/polykinds/T10134a.hs index 0d84d56b5e..9412705e4c 100644 --- a/testsuite/tests/polykinds/T10134a.hs +++ b/testsuite/tests/polykinds/T10134a.hs @@ -4,8 +4,9 @@ {-# LANGUAGE TypeOperators #-} module T10134a where +import Data.Kind (Type) import GHC.TypeLits -data Vec :: Nat -> * -> * where +data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a (:>) :: a -> Vec n a -> Vec (n + 1) a diff --git a/testsuite/tests/polykinds/T10934.hs b/testsuite/tests/polykinds/T10934.hs index fb7a538ebd..35ea20f225 100644 --- a/testsuite/tests/polykinds/T10934.hs +++ b/testsuite/tests/polykinds/T10934.hs @@ -11,6 +11,8 @@ module KeyValue where +import Data.Kind + data AccValidation err a = AccFailure err | AccSuccess a data KeyValueError = MissingValue @@ -23,11 +25,11 @@ missing = rpure missingField missingField :: forall x. (WithKeyValueError :. f) x missingField = Compose $ AccFailure [MissingValue] -data Rec :: (u -> *) -> [u] -> * where +data Rec :: (u -> Type) -> [u] -> Type where RNil :: Rec f '[] (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) -newtype Compose (f :: l -> *) (g :: k -> l) (x :: k) +newtype Compose (f :: l -> Type) (g :: k -> l) (x :: k) = Compose { getCompose :: f (g x) } type (:.) f g = Compose f g diff --git a/testsuite/tests/polykinds/T11142.hs b/testsuite/tests/polykinds/T11142.hs index 58eb3b6c94..a96566a371 100644 --- a/testsuite/tests/polykinds/T11142.hs +++ b/testsuite/tests/polykinds/T11142.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, RankNTypes #-} +{-# LANGUAGE PolyKinds, RankNTypes #-} module T11142 where diff --git a/testsuite/tests/polykinds/T11399.hs b/testsuite/tests/polykinds/T11399.hs index bc9e60d7f3..56f3c11ef7 100644 --- a/testsuite/tests/polykinds/T11399.hs +++ b/testsuite/tests/polykinds/T11399.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleInstances, TypeInType #-} +{-# LANGUAGE FlexibleInstances, PolyKinds #-} module T11399 where import Data.Kind diff --git a/testsuite/tests/polykinds/T11480b.hs b/testsuite/tests/polykinds/T11480b.hs index 12802e8de3..2684c6de4e 100644 --- a/testsuite/tests/polykinds/T11480b.hs +++ b/testsuite/tests/polykinds/T11480b.hs @@ -21,25 +21,25 @@ module T11480b where -import GHC.Types (Constraint) +import Data.Kind (Constraint, Type) import Data.Type.Equality as Equality import Data.Type.Coercion as Coercion import qualified Prelude import Prelude (Either(..)) -newtype Y (p :: i -> j -> *) (a :: j) (b :: i) = Y { getY :: p b a } +newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a } -type family Op (p :: i -> j -> *) :: j -> i -> * where +type family Op (p :: i -> j -> Type) :: j -> i -> Type where Op (Y p) = p Op p = Y p -class Vacuous (p :: i -> i -> *) (a :: i) +class Vacuous (p :: i -> i -> Type) (a :: i) instance Vacuous p a data Dict (p :: Constraint) where Dict :: p => Dict p -class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> *) where +class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> Type) where type Ob p :: i -> Constraint type Ob p = Vacuous p @@ -62,11 +62,16 @@ class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> *) where default unop :: Op p ~ Y p => Op p b a -> p a b unop = getY -class (Category p, Category q) => Functor (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) | f -> p q where +class (Category p, Category q) => + Functor (p :: i -> i -> Type) + (q :: j -> j -> Type) + (f :: i -> j) | f -> p q where fmap :: p a b -> q (f a) (f b) -data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where - Nat :: (Functor p q f, Functor p q g) => { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g +data Nat (p :: i -> i -> Type) + (q :: j -> j -> Type) (f :: i -> j) (g :: i -> j) where + Nat :: (Functor p q f, Functor p q g) => + { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = Functor p q @@ -80,7 +85,8 @@ instance (Category p, Category q) => Category (Nat p q) where ob :: forall p q f a. Functor p q f => Ob p a :- Ob q (f a) ob = Sub (case source (fmap (id :: p a a) :: q (f a) (f a)) of Dict -> Dict) -instance (Category p, Category q) => Functor (Y (Nat p q)) (Nat (Nat p q) (->)) (Nat p q) where +instance (Category p, Category q) => + Functor (Y (Nat p q)) (Nat (Nat p q) (->)) (Nat p q) where fmap (Y f) = Nat (. f) instance (Category p, Category q) => Functor (Nat p q) (->) (Nat p q f) where diff --git a/testsuite/tests/polykinds/T11520.hs b/testsuite/tests/polykinds/T11520.hs index fa5a3bf4a4..eef999d4ba 100644 --- a/testsuite/tests/polykinds/T11520.hs +++ b/testsuite/tests/polykinds/T11520.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-} +{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses #-} module T11520 where diff --git a/testsuite/tests/polykinds/T11523.hs b/testsuite/tests/polykinds/T11523.hs index 0313b0c46e..aff0f9ed90 100644 --- a/testsuite/tests/polykinds/T11523.hs +++ b/testsuite/tests/polykinds/T11523.hs @@ -15,7 +15,6 @@ {-# language FunctionalDependencies #-} {-# language UndecidableSuperClasses #-} {-# language UndecidableInstances #-} -{-# language TypeInType #-} module T11523 where diff --git a/testsuite/tests/polykinds/T11554.hs b/testsuite/tests/polykinds/T11554.hs index e7a35bd9d8..bca6b8277c 100644 --- a/testsuite/tests/polykinds/T11554.hs +++ b/testsuite/tests/polykinds/T11554.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, TypeInType, RankNTypes #-} +{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-} module T11554 where diff --git a/testsuite/tests/polykinds/T11616.hs b/testsuite/tests/polykinds/T11616.hs index 378032b7ed..16a62b33b2 100644 --- a/testsuite/tests/polykinds/T11616.hs +++ b/testsuite/tests/polykinds/T11616.hs @@ -1,6 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} module T11616 where class Whoami a where diff --git a/testsuite/tests/polykinds/T11640.hs b/testsuite/tests/polykinds/T11640.hs index bbb4a53bfc..ade4cbc79d 100644 --- a/testsuite/tests/polykinds/T11640.hs +++ b/testsuite/tests/polykinds/T11640.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, RankNTypes, TypeInType #-} +{-# LANGUAGE GADTs, RankNTypes, PolyKinds #-} module T11640 where diff --git a/testsuite/tests/polykinds/T11648.hs b/testsuite/tests/polykinds/T11648.hs index 15fcfa4e05..b8b70e8733 100644 --- a/testsuite/tests/polykinds/T11648.hs +++ b/testsuite/tests/polykinds/T11648.hs @@ -3,6 +3,8 @@ module T11648 where -class Monoidy (to :: k0 -> k1 -> *) (m :: k1) where +import Data.Kind + +class Monoidy (to :: k0 -> k1 -> Type) (m :: k1) where type MComp to m :: k1 -> k1 -> k0 mjoin :: MComp to m m m `to` m diff --git a/testsuite/tests/polykinds/T11648b.hs b/testsuite/tests/polykinds/T11648b.hs index 2ab27a6166..d50854d237 100644 --- a/testsuite/tests/polykinds/T11648b.hs +++ b/testsuite/tests/polykinds/T11648b.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T11648b where diff --git a/testsuite/tests/polykinds/T11821a.hs b/testsuite/tests/polykinds/T11821a.hs index da96fe2c56..c5de2bbe53 100644 --- a/testsuite/tests/polykinds/T11821a.hs +++ b/testsuite/tests/polykinds/T11821a.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, TypeInType, ConstraintKinds #-} +{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds #-} module T11821a where import Data.Proxy type SameKind (a :: k1) (b :: k2) = ('Proxy :: Proxy k1) ~ ('Proxy :: Proxy k2) diff --git a/testsuite/tests/polykinds/T12055.hs b/testsuite/tests/polykinds/T12055.hs index 3ffc221b7b..cabc2dfbba 100644 --- a/testsuite/tests/polykinds/T12055.hs +++ b/testsuite/tests/polykinds/T12055.hs @@ -3,9 +3,9 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} -- The code from the ticket lacked these extensions, -- but crashed the compiler with "GHC internal error" diff --git a/testsuite/tests/polykinds/T12055a.hs b/testsuite/tests/polykinds/T12055a.hs index dab523861b..ebc4dc7cad 100644 --- a/testsuite/tests/polykinds/T12055a.hs +++ b/testsuite/tests/polykinds/T12055a.hs @@ -3,9 +3,9 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances, FunctionalDependencies #-} diff --git a/testsuite/tests/polykinds/T12593.hs b/testsuite/tests/polykinds/T12593.hs index 867fb89284..8fd4f26578 100644 --- a/testsuite/tests/polykinds/T12593.hs +++ b/testsuite/tests/polykinds/T12593.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, ConstraintKinds, PolyKinds, TypeInType, KindSignatures, RankNTypes #-} +{-# LANGUAGE GADTs, ConstraintKinds, PolyKinds, KindSignatures, RankNTypes #-} module T12593 where diff --git a/testsuite/tests/polykinds/T12668.hs b/testsuite/tests/polykinds/T12668.hs index 4640903cc5..c3d2902a25 100644 --- a/testsuite/tests/polykinds/T12668.hs +++ b/testsuite/tests/polykinds/T12668.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} module T12668 where diff --git a/testsuite/tests/polykinds/T12718.hs b/testsuite/tests/polykinds/T12718.hs index 82d6dcd177..7bbe1d572e 100644 --- a/testsuite/tests/polykinds/T12718.hs +++ b/testsuite/tests/polykinds/T12718.hs @@ -1,5 +1,5 @@ {-# Language RebindableSyntax, NoImplicitPrelude, MagicHash, RankNTypes, - PolyKinds, ViewPatterns, TypeInType, FlexibleInstances #-} + PolyKinds, ViewPatterns, FlexibleInstances #-} module Main where diff --git a/testsuite/tests/polykinds/T13391.hs b/testsuite/tests/polykinds/T13391.hs deleted file mode 100644 index 6de3c3aa40..0000000000 --- a/testsuite/tests/polykinds/T13391.hs +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE PolyKinds, GADTs #-} - -module T13391 where - -data G (a :: k) where - GInt :: G Int - GMaybe :: G Maybe diff --git a/testsuite/tests/polykinds/T13391.stderr b/testsuite/tests/polykinds/T13391.stderr deleted file mode 100644 index 55fff35b3a..0000000000 --- a/testsuite/tests/polykinds/T13391.stderr +++ /dev/null @@ -1,7 +0,0 @@ - -T13391.hs:6:3: error: - • Data constructor ‘GInt’ constrains the choice of kind parameter: - k ~ * - Use TypeInType to allow this - • In the definition of data constructor ‘GInt’ - In the data type declaration for ‘G’ diff --git a/testsuite/tests/polykinds/T13625.hs b/testsuite/tests/polykinds/T13625.hs index 62d34611be..9367aa694f 100644 --- a/testsuite/tests/polykinds/T13625.hs +++ b/testsuite/tests/polykinds/T13625.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T13625 where diff --git a/testsuite/tests/polykinds/T13659.hs b/testsuite/tests/polykinds/T13659.hs index 199ff08a8d..118a04f122 100644 --- a/testsuite/tests/polykinds/T13659.hs +++ b/testsuite/tests/polykinds/T13659.hs @@ -4,8 +4,10 @@ module T13659 where +import Data.Kind (Type) + -- format string parameterized by a list of types -data Format (fmt :: [*]) where +data Format (fmt :: [Type]) where X :: Format '[] -- empty string, i.e. "" L :: a -> String -> Format '[] -- string literal, e.g. "hello" S :: a -> Format '[String] -- "%s" diff --git a/testsuite/tests/polykinds/T13659.stderr b/testsuite/tests/polykinds/T13659.stderr index fac5cbb952..84e81d04c0 100644 --- a/testsuite/tests/polykinds/T13659.stderr +++ b/testsuite/tests/polykinds/T13659.stderr @@ -1,5 +1,5 @@ -T13659.hs:12:27: error: +T13659.hs:14:27: error: • Expected a type, but ‘a’ has kind ‘[*]’ • In the first argument of ‘Format’, namely ‘'[Int, a]’ In the type ‘Format '[Int, a]’ diff --git a/testsuite/tests/polykinds/T13738.hs b/testsuite/tests/polykinds/T13738.hs index 85a1048f53..8420ca9158 100644 --- a/testsuite/tests/polykinds/T13738.hs +++ b/testsuite/tests/polykinds/T13738.hs @@ -1,9 +1,9 @@ {-# LANGUAGE PolyKinds #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} + module T13738 where import Data.Coerce diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr index ec829dec4d..f60314a443 100644 --- a/testsuite/tests/polykinds/T13985.stderr +++ b/testsuite/tests/polykinds/T13985.stderr @@ -3,21 +3,21 @@ T13985.hs:12:1: error: • Kind variable ‘k’ is implicitly bound in data family ‘Fam’, but does not appear as the kind of any of its type variables. Perhaps you meant - to bind it (with TypeInType) explicitly somewhere? + to bind it explicitly somewhere? • In the data instance declaration for ‘Fam’ T13985.hs:15:15: error: • Kind variable ‘a’ is implicitly bound in type family ‘T’, but does not appear as the kind of any of its type variables. Perhaps you meant - to bind it (with TypeInType) explicitly somewhere? + to bind it explicitly somewhere? • In the type instance declaration for ‘T’ T13985.hs:22:3: error: • Kind variable ‘k’ is implicitly bound in associated data family ‘CD’, but does not appear as the kind of any of its type variables. Perhaps you meant - to bind it (with TypeInType) explicitly somewhere? + to bind it explicitly somewhere? • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Type’ @@ -25,7 +25,7 @@ T13985.hs:23:8: error: • Kind variable ‘a’ is implicitly bound in associated type family ‘CT’, but does not appear as the kind of any of its type variables. Perhaps you meant - to bind it (with TypeInType) explicitly somewhere? + to bind it explicitly somewhere? • In the type instance declaration for ‘CT’ In the instance declaration for ‘C Type’ @@ -33,7 +33,7 @@ T13985.hs:27:3: error: • Kind variable ‘x’ is implicitly bound in associated type family ‘ZT’, but does not appear as the kind of any of its type variables. Perhaps you meant - to bind it (with TypeInType) explicitly somewhere? + to bind it explicitly somewhere? Type variables with inferred kinds: (k :: *) (a :: k) • In the default type instance declaration for ‘ZT’ In the class declaration for ‘Z’ diff --git a/testsuite/tests/polykinds/T14174.hs b/testsuite/tests/polykinds/T14174.hs index 7a58b70fc6..3fe4996225 100644 --- a/testsuite/tests/polykinds/T14174.hs +++ b/testsuite/tests/polykinds/T14174.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, RankNTypes, KindSignatures, PolyKinds #-} +{-# LANGUAGE RankNTypes, KindSignatures, PolyKinds #-} module T14174 where data T k (x :: k) = MkT diff --git a/testsuite/tests/polykinds/T14174a.hs b/testsuite/tests/polykinds/T14174a.hs index 82f418bc9d..bdd3d7ee88 100644 --- a/testsuite/tests/polykinds/T14174a.hs +++ b/testsuite/tests/polykinds/T14174a.hs @@ -1,14 +1,15 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module T14174a where import Data.Kind -data TyFun :: * -> * -> * -type a ~> b = TyFun a b -> * +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 diff --git a/testsuite/tests/polykinds/T14209.hs b/testsuite/tests/polykinds/T14209.hs index 3e0181c4ed..0f0648bd79 100644 --- a/testsuite/tests/polykinds/T14209.hs +++ b/testsuite/tests/polykinds/T14209.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T14209 where data MyProxy k (a :: k) = MyProxy diff --git a/testsuite/tests/polykinds/T14270.hs b/testsuite/tests/polykinds/T14270.hs index 2d11a29993..3eed83c657 100644 --- a/testsuite/tests/polykinds/T14270.hs +++ b/testsuite/tests/polykinds/T14270.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE TypeInType #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} @@ -8,6 +7,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE PolyKinds #-} module T14270 (pattern App) where import Data.Kind (Type) diff --git a/testsuite/tests/polykinds/T14450.hs b/testsuite/tests/polykinds/T14450.hs index 3b8f5b7e70..8571829619 100644 --- a/testsuite/tests/polykinds/T14450.hs +++ b/testsuite/tests/polykinds/T14450.hs @@ -1,4 +1,6 @@ -{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-} +{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, + ConstraintKinds, TypeFamilies, DataKinds, GADTs, + AllowAmbiguousTypes, InstanceSigs #-} module T14450 where diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr index c7caf04220..e8ff4aeae3 100644 --- a/testsuite/tests/polykinds/T14450.stderr +++ b/testsuite/tests/polykinds/T14450.stderr @@ -1,5 +1,5 @@ -T14450.hs:31:12: error: +T14450.hs:33:12: error: • Expected kind ‘k ~> k’, but ‘(IddSym0 :: Type ~> Type)’ has kind ‘* ~> *’ • In the first argument of ‘Dom’, namely diff --git a/testsuite/tests/polykinds/T14515.hs b/testsuite/tests/polykinds/T14515.hs index 15bdbfe31d..4a2540b925 100644 --- a/testsuite/tests/polykinds/T14515.hs +++ b/testsuite/tests/polykinds/T14515.hs @@ -1,5 +1,6 @@ {-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} module Bug where import Data.Kind diff --git a/testsuite/tests/polykinds/T14520.hs b/testsuite/tests/polykinds/T14520.hs index ed87035b24..23e903773b 100644 --- a/testsuite/tests/polykinds/T14520.hs +++ b/testsuite/tests/polykinds/T14520.hs @@ -1,4 +1,4 @@ -{-# Language TypeInType, TypeFamilies, TypeOperators #-} +{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators #-} module T14520 where @@ -10,7 +10,7 @@ data family Sing (a::k) type family XXX (f::a~>>b) (x::a) :: b -type family Id :: (kat :: a ~>> (a ~>> *)) `XXX` (b :: a) `XXX` b +type family Id :: (kat :: a ~>> (a ~>> Type)) `XXX` (b :: a) `XXX` b sId :: Sing w -> Sing (Id :: bat w w) sId = sId diff --git a/testsuite/tests/polykinds/T14555.hs b/testsuite/tests/polykinds/T14555.hs index 0ab71b1b76..7f37a5ec9c 100644 --- a/testsuite/tests/polykinds/T14555.hs +++ b/testsuite/tests/polykinds/T14555.hs @@ -1,10 +1,10 @@ -{-# Language TypeInType #-} {-# Language TypeOperators, DataKinds, PolyKinds, GADTs #-} + module T14555 where import Data.Kind -import GHC.Types (TYPE) +import GHC.Types (TYPE, Type) data Exp :: [TYPE rep] -> TYPE rep -> Type where --data Exp (x :: [TYPE rep]) (y :: TYPE rep) where diff --git a/testsuite/tests/polykinds/T14561.hs b/testsuite/tests/polykinds/T14561.hs index f528e7c813..7b1f17e08e 100644 --- a/testsuite/tests/polykinds/T14561.hs +++ b/testsuite/tests/polykinds/T14561.hs @@ -1,5 +1,5 @@ -{-# LANGUAGE TypeInType #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE MagicHash #-} diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs index bedc99f54b..bdc05dd6df 100644 --- a/testsuite/tests/polykinds/T14563.hs +++ b/testsuite/tests/polykinds/T14563.hs @@ -1,6 +1,6 @@ -{-# Language TypeInType #-} {-# Language RankNTypes, KindSignatures, PolyKinds #-} {-# OPTIONS_GHC -fprint-explicit-runtime-reps #-} + import GHC.Types (TYPE) import Data.Kind diff --git a/testsuite/tests/polykinds/T14580.hs b/testsuite/tests/polykinds/T14580.hs index 6d11d78dfe..58983cc117 100644 --- a/testsuite/tests/polykinds/T14580.hs +++ b/testsuite/tests/polykinds/T14580.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE PolyKinds, DataKinds, TypeInType, TypeOperators #-} +{-# LANGUAGE PolyKinds, DataKinds, TypeOperators #-} module T14580 where import Data.Kind diff --git a/testsuite/tests/polykinds/T14710.stderr b/testsuite/tests/polykinds/T14710.stderr index 8d8a9785a8..0bbfb0d641 100644 --- a/testsuite/tests/polykinds/T14710.stderr +++ b/testsuite/tests/polykinds/T14710.stderr @@ -20,19 +20,11 @@ T14710.hs:18:24: error: In the type signature for ‘g2’ T14710.hs:21:31: error: - Variable ‘k’ used as both a kind and a type - Did you intend to use TypeInType? - -T14710.hs:21:31: error: Unexpected kind variable ‘k’ Perhaps you intended to use PolyKinds In the type signature for ‘h1’ T14710.hs:24:22: error: - Variable ‘k’ used as both a kind and a type - Did you intend to use TypeInType? - -T14710.hs:24:22: error: Unexpected kind variable ‘k’ Perhaps you intended to use PolyKinds In the type signature for ‘h2’ diff --git a/testsuite/tests/polykinds/T14846.hs b/testsuite/tests/polykinds/T14846.hs index 7b96e942f3..0f70962562 100644 --- a/testsuite/tests/polykinds/T14846.hs +++ b/testsuite/tests/polykinds/T14846.hs @@ -6,7 +6,7 @@ {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T14846 where import Data.Kind diff --git a/testsuite/tests/polykinds/T14873.hs b/testsuite/tests/polykinds/T14873.hs index 6bb66ec640..9450a019bc 100644 --- a/testsuite/tests/polykinds/T14873.hs +++ b/testsuite/tests/polykinds/T14873.hs @@ -2,8 +2,9 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} module T14873 where import Data.Kind (Type) diff --git a/testsuite/tests/polykinds/T15170.hs b/testsuite/tests/polykinds/T15170.hs index a105ca5344..02de90ae12 100644 --- a/testsuite/tests/polykinds/T15170.hs +++ b/testsuite/tests/polykinds/T15170.hs @@ -1,7 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} {-# LANGUAGE TypeOperators #-} module T15170 where diff --git a/testsuite/tests/polykinds/T5716.hs b/testsuite/tests/polykinds/T5716.hs index 1b705a36b1..217e4c399a 100644 --- a/testsuite/tests/polykinds/T5716.hs +++ b/testsuite/tests/polykinds/T5716.hs @@ -4,10 +4,11 @@ module T5716 where +import Data.Kind (Type) data family DF a data instance DF Int = DFInt data U = U1 (DF Int) -data I :: U -> * where I1 :: I (U1 DFInt) +data I :: U -> Type where I1 :: I (U1 DFInt) diff --git a/testsuite/tests/polykinds/T5716.stderr b/testsuite/tests/polykinds/T5716.stderr index 0e3596da32..41bf517339 100644 --- a/testsuite/tests/polykinds/T5716.stderr +++ b/testsuite/tests/polykinds/T5716.stderr @@ -1,7 +1,7 @@ -T5716.hs:13:33: error: - • Data constructor ‘U1’ cannot be used here - (perhaps you intended to use TypeInType) - • In the first argument of ‘I’, namely ‘(U1 DFInt)’ +T5716.hs:14:39: error: + • Data constructor ‘DFInt’ cannot be used here + (it comes from a data family instance) + • In the first argument of ‘U1’, namely ‘DFInt’ + In the first argument of ‘I’, namely ‘(U1 DFInt)’ In the type ‘I (U1 DFInt)’ - In the definition of data constructor ‘I1’ diff --git a/testsuite/tests/polykinds/T6021.stderr b/testsuite/tests/polykinds/T6021.stderr deleted file mode 100644 index d747043d27..0000000000 --- a/testsuite/tests/polykinds/T6021.stderr +++ /dev/null @@ -1,4 +0,0 @@ - -T6021.hs:5:22: error: - Variable ‘b’ used as both a kind and a type - Did you intend to use TypeInType? diff --git a/testsuite/tests/polykinds/T6035.hs b/testsuite/tests/polykinds/T6035.hs index a6f5ffe54a..c89de8e73d 100644 --- a/testsuite/tests/polykinds/T6035.hs +++ b/testsuite/tests/polykinds/T6035.hs @@ -3,9 +3,11 @@ module T6035 where +import Data.Kind (Type) + data Nat = Zero | Succ Nat -type family Sing (a :: k) :: k -> * +type family Sing (a :: k) :: k -> Type data SNat n where SZero :: SNat Zero diff --git a/testsuite/tests/polykinds/T6039.stderr b/testsuite/tests/polykinds/T6039.stderr index 048efd538f..bcaa2e1b4c 100644 --- a/testsuite/tests/polykinds/T6039.stderr +++ b/testsuite/tests/polykinds/T6039.stderr @@ -1,4 +1,10 @@ -T6039.hs:5:14: error: - • Expected kind ‘* -> *’, but ‘j’ has kind ‘*’ - • In the kind ‘j k’ +T6039.hs:5:1: error: + You have written a *complete user-suppled kind signature*, + but the following variable is undetermined: k0 :: * + Perhaps add a kind signature. + Inferred kinds of user-written variables: + j :: k0 -> * + k :: k0 + a :: j k + Inferred result kind: * diff --git a/testsuite/tests/polykinds/T6093.hs b/testsuite/tests/polykinds/T6093.hs index 3fdeb207f8..1063b8661d 100644 --- a/testsuite/tests/polykinds/T6093.hs +++ b/testsuite/tests/polykinds/T6093.hs @@ -1,13 +1,12 @@ -{-# LANGUAGE GADTs, PolyKinds #-} +{-# LANGUAGE GADTs, RankNTypes, PolyKinds #-} module T6093 where -- Polymorphic kind recursion -data R :: k -> * where +data R :: forall k. k -> * where MkR :: R f -> R (f ()) - data IOWitness (a :: k) = IOW -data Type :: k -> * where +data Type :: forall k. k -> * where SimpleType :: IOWitness a -> Type a ConstructedType :: Type f -> Type a -> Type (f a) diff --git a/testsuite/tests/polykinds/T7404.stderr b/testsuite/tests/polykinds/T7404.stderr deleted file mode 100644 index abae5a6215..0000000000 --- a/testsuite/tests/polykinds/T7404.stderr +++ /dev/null @@ -1,4 +0,0 @@ - -T7404.hs:4:32: error: - Variable ‘x’ used as both a kind and a type - Did you intend to use TypeInType? diff --git a/testsuite/tests/polykinds/T7594.hs b/testsuite/tests/polykinds/T7594.hs index ae21956d45..925b3f9ace 100644 --- a/testsuite/tests/polykinds/T7594.hs +++ b/testsuite/tests/polykinds/T7594.hs @@ -10,9 +10,11 @@ module T7594 where -import GHC.Exts (Constraint) +import Data.Kind (Constraint, Type) -class (c1 t, c2 t) => (:&:) (c1 :: * -> Constraint) (c2 :: * -> Constraint) (t :: *) +class (c1 t, c2 t) => (:&:) (c1 :: Type -> Constraint) + (c2 :: Type -> Constraint) + (t :: Type) instance (c1 t, c2 t) => (:&:) c1 c2 t data ColD c where diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr index 3ea08a3fb8..1b4b9017f7 100644 --- a/testsuite/tests/polykinds/T7594.stderr +++ b/testsuite/tests/polykinds/T7594.stderr @@ -1,17 +1,18 @@ -T7594.hs:35:12: error: +T7594.hs:37:12: error: • Couldn't match type ‘b’ with ‘IO ()’ ‘b’ is untouchable inside the constraints: (:&:) c0 Real a bound by a type expected by the context: forall a. (:&:) c0 Real a => a -> b - at T7594.hs:35:8-19 + at T7594.hs:37:8-19 ‘b’ is a rigid type variable bound by - the inferred type of bar2 :: b at T7594.hs:35:1-19 + the inferred type of bar2 :: b + at T7594.hs:37:1-19 Possible fix: add a type signature for ‘bar2’ Expected type: a -> b Actual type: a -> IO () • In the first argument of ‘app’, namely ‘print’ In the expression: app print q2 In an equation for ‘bar2’: bar2 = app print q2 - • Relevant bindings include bar2 :: b (bound at T7594.hs:35:1) + • Relevant bindings include bar2 :: b (bound at T7594.hs:37:1) diff --git a/testsuite/tests/polykinds/T8566.hs b/testsuite/tests/polykinds/T8566.hs index 248febb586..2ffdecfd6e 100644 --- a/testsuite/tests/polykinds/T8566.hs +++ b/testsuite/tests/polykinds/T8566.hs @@ -10,10 +10,12 @@ module T8566 where -data U (s :: *) = forall v. AA v [U s] +import Data.Kind (Type) + +data U (s :: Type) = forall v. AA v [U s] -- AA :: forall (s:*) (v:*). v -> [U s] -> U s -data I (u :: U *) (r :: [*]) :: * where +data I (u :: U Type) (r :: [Type]) :: Type where A :: I (AA t as) r -- Existential k -- A :: forall (u:U *) (r:[*]) Universal @@ -22,7 +24,7 @@ data I (u :: U *) (r :: [*]) :: * where -- I u r -- fs unused, but needs to be present for the bug -class C (u :: U *) (r :: [*]) (fs :: [*]) where +class C (u :: U Type) (r :: [Type]) (fs :: [Type]) where c :: I u r -> I u r -- c :: forall (u :: U *) (r :: [*]) (fs :: [*]). C u r fs => I u r -> I u r diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr index d368d055f0..23dddf66c7 100644 --- a/testsuite/tests/polykinds/T8566.stderr +++ b/testsuite/tests/polykinds/T8566.stderr @@ -1,18 +1,18 @@ -T8566.hs:32:9: error: +T8566.hs:34:9: error: • Could not deduce (C ('AA (t (I a ps)) as) ps fs0) arising from a use of ‘c’ from the context: C ('AA (t (I a ps)) as) ps fs - bound by the instance declaration at T8566.hs:30:10-67 + bound by the instance declaration at T8566.hs:32:10-67 or from: 'AA t (a : as) ~ 'AA t1 as1 bound by a pattern with constructor: A :: forall v (t :: v) (as :: [U *]) (r :: [*]). I ('AA t as) r, in an equation for ‘c’ - at T8566.hs:32:5 + at T8566.hs:34:5 The type variable ‘fs0’ is ambiguous Relevant bindings include c :: I ('AA t (a : as)) ps -> I ('AA t (a : as)) ps - (bound at T8566.hs:32:3) + (bound at T8566.hs:34:3) • In the expression: c undefined In an equation for ‘c’: c A = c undefined In the instance declaration for ‘C ('AA t (a : as)) ps fs’ diff --git a/testsuite/tests/polykinds/T8566a.hs b/testsuite/tests/polykinds/T8566a.hs index 3d20c3e27d..22b628553f 100644 --- a/testsuite/tests/polykinds/T8566a.hs +++ b/testsuite/tests/polykinds/T8566a.hs @@ -6,13 +6,15 @@ {-# LANGUAGE TypeOperators #-} module T8566a where +import Data.Kind (Type) + data Field = forall k. APP k [Field] -data InField (u :: Field) :: * where +data InField (u :: Field) :: Type where A :: AppVars t (ExpandField args) -> InField (APP t args) -type family ExpandField (args :: [Field]) :: [*] -type family AppVars (t :: k) (vs :: [*]) :: * +type family ExpandField (args :: [Field]) :: [Type] +type family AppVars (t :: k) (vs :: [Type]) :: Type -- This function fails to compile, because we discard -- 'given' kind equalities. See comment 7 in Trac #8566 diff --git a/testsuite/tests/polykinds/T8985.hs b/testsuite/tests/polykinds/T8985.hs index 28a354be27..d9e8d2c66a 100644 --- a/testsuite/tests/polykinds/T8985.hs +++ b/testsuite/tests/polykinds/T8985.hs @@ -1,12 +1,14 @@ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators #-} -module T8905 where +module T8985 where + +import Data.Kind (Type) data X (xs :: [k]) = MkX -data Y :: (k -> *) -> [k] -> * where +data Y :: (k -> Type) -> [k] -> Type where MkY :: f x -> Y f (x ': xs) -type family F (a :: [[*]]) :: * +type family F (a :: [[Type]]) :: Type type instance F xss = Y X xss works :: Y X '[ '[ ] ] -> () diff --git a/testsuite/tests/polykinds/T9222.hs b/testsuite/tests/polykinds/T9222.hs index 8e46ccb3c5..3af1458427 100644 --- a/testsuite/tests/polykinds/T9222.hs +++ b/testsuite/tests/polykinds/T9222.hs @@ -1,6 +1,7 @@ {-# LANGUAGE RankNTypes, GADTs, DataKinds, PolyKinds, TypeOperators, TypeFamilies #-} module T9222 where +import Data.Kind import Data.Proxy -- Nov 2014: actually the type of Want is ambiguous if we @@ -9,5 +10,5 @@ import Data.Proxy -- So this program is erroneous. (But the original ticket was -- a crash, and that's still fixed!) -data Want :: (i,j) -> * where +data Want :: (i,j) -> Type where Want :: (a ~ '(b,c) => Proxy b) -> Want a diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr index 604cc1b7ec..be80a79198 100644 --- a/testsuite/tests/polykinds/T9222.stderr +++ b/testsuite/tests/polykinds/T9222.stderr @@ -1,16 +1,16 @@ -T9222.hs:13:3: error: +T9222.hs:14:3: error: • Couldn't match type ‘c0’ with ‘c’ ‘c0’ is untouchable inside the constraints: a ~ '(b0, c0) bound by the type of the constructor ‘Want’: (a ~ '(b0, c0)) => Proxy b0 - at T9222.hs:13:3-43 + at T9222.hs:14:3-43 ‘c’ is a rigid type variable bound by the type of the constructor ‘Want’: forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1). ((a ~ '(b, c)) => Proxy b) -> Want a - at T9222.hs:13:3-43 + at T9222.hs:14:3-43 • In the ambiguity check for ‘Want’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the definition of data constructor ‘Want’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 4fe88b2385..c3250b7ffd 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -38,7 +38,7 @@ test('T6036', normal, compile, ['']) test('T6025', normal, run_command, ['$MAKE -s --no-print-directory T6025']) test('T6002', normal, compile, ['']) test('T6039', normal, compile_fail, ['']) -test('T6021', normal, compile_fail, ['']) +test('T6021', normal, compile, ['']) test('T6020a', normal, compile, ['']) test('T6044', normal, compile, ['']) test('T6054', normal, run_command, ['$MAKE -s --no-print-directory T6054']) @@ -74,7 +74,7 @@ test('T7341', normal, compile_fail,['']) test('T7422', normal, compile,['']) test('T7433', normal, compile_fail,['']) test('T7438', normal, run_command, ['$MAKE -s --no-print-directory T7438']) -test('T7404', normal, compile_fail,['']) +test('T7404', normal, compile,['']) test('T7502', normal, compile,['']) test('T7488', normal, compile,['']) test('T7594', normal, compile_fail,['']) @@ -170,7 +170,6 @@ test('BadKindVar', normal, compile_fail, ['']) test('T13738', normal, compile_fail, ['']) test('T14209', normal, compile, ['']) test('T14265', normal, compile_fail, ['']) -test('T13391', normal, compile_fail, ['']) test('T13391a', normal, compile, ['']) test('T14270', normal, compile, ['']) test('T14450', normal, compile_fail, ['']) |