diff options
Diffstat (limited to 'testsuite/tests/polykinds')
118 files changed, 1435 insertions, 209 deletions
diff --git a/testsuite/tests/polykinds/BadKindVar.hs b/testsuite/tests/polykinds/BadKindVar.hs new file mode 100644 index 0000000000..c24657f3d2 --- /dev/null +++ b/testsuite/tests/polykinds/BadKindVar.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE RankNTypes, KindSignatures #-} + +module Foo where + +import Data.Proxy + +-- Should be illegal without PolyKinds +f :: forall (a :: k). Proxy a +f = f diff --git a/testsuite/tests/polykinds/BadKindVar.stderr b/testsuite/tests/polykinds/BadKindVar.stderr new file mode 100644 index 0000000000..beeed2b3c8 --- /dev/null +++ b/testsuite/tests/polykinds/BadKindVar.stderr @@ -0,0 +1,5 @@ + +BadKindVar.hs:8:19: error: + Unexpected kind variable ‘k’ + Perhaps you intended to use PolyKinds + In the type signature for ‘f’ diff --git a/testsuite/tests/polykinds/KindVType.stderr b/testsuite/tests/polykinds/KindVType.stderr index 7ce3404579..27e2e588a5 100644 --- a/testsuite/tests/polykinds/KindVType.stderr +++ b/testsuite/tests/polykinds/KindVType.stderr @@ -1,6 +1,6 @@ KindVType.hs:8:8: error: - • Couldn't match type ‘*’ with ‘* -> *’ + • Couldn't match type ‘Int’ with ‘Maybe’ Expected type: Proxy Maybe Actual type: Proxy Int • In the expression: (Proxy :: Proxy Int) diff --git a/testsuite/tests/polykinds/MonoidsFD.hs b/testsuite/tests/polykinds/MonoidsFD.hs index f093d77663..67be60d60a 100644 --- a/testsuite/tests/polykinds/MonoidsFD.hs +++ b/testsuite/tests/polykinds/MonoidsFD.hs @@ -15,6 +15,7 @@ module Main where import Control.Monad (Monad(..), join, ap) import Data.Monoid (Monoid(..)) +import Data.Semigroup (Semigroup(..)) -- First we define the type class Monoidy: @@ -81,9 +82,11 @@ test2 = print (Sum 1 <+> Sum 2 <+> Sum 4) -- Sum 7 -- rather cumbersome in actual use. So, we can give traditional Monad and -- Monoid instances for instances of Monoidy: +instance Monoidy (→) (,) () m ⇒ Semigroup m where + (<>) = curry mjoin + instance Monoidy (→) (,) () m ⇒ Monoid m where mempty = munit () - mappend = curry mjoin instance Applicative Wrapper where pure = return diff --git a/testsuite/tests/polykinds/MonoidsTF.hs b/testsuite/tests/polykinds/MonoidsTF.hs index 9097e53af2..8e3b378046 100644 --- a/testsuite/tests/polykinds/MonoidsTF.hs +++ b/testsuite/tests/polykinds/MonoidsTF.hs @@ -12,12 +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 @@ -91,10 +94,13 @@ test2 = print (Sum 1 <+> Sum 2 <+> Sum 4) -- Sum 7 -- rather cumbersome in actual use. So, we can give traditional Monad and -- Monoid instances for instances of Monoidy: -instance (MId (→) m ~ (), MComp (→) m ~ (,), Monoidy (→) m) +instance (MId (→) m ~ (), MComp (→) m ~ (,), Monoidy (→) m) + ⇒ Semigroup m where + (<>) = curry mjoin + +instance (MId (→) m ~ (), MComp (→) m ~ (,), Monoidy (→) m) ⇒ Monoid m where mempty = munit () - mappend = curry mjoin instance Applicative Wrapper where pure = return 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/T10134.hs b/testsuite/tests/polykinds/T10134.hs index 0b64625f28..746758ce2f 100644 --- a/testsuite/tests/polykinds/T10134.hs +++ b/testsuite/tests/polykinds/T10134.hs @@ -3,7 +3,7 @@ module T10134 where -import GHC.TypeLits +import GHC.TypeLits as L import T10134a import Prelude @@ -11,9 +11,9 @@ type Positive n = ((n-1)+1)~n data Dummy n d = Dummy { vec :: Vec n (Vec d Bool) } -nextDummy :: Positive (2*(n+d)) => Dummy n d -> Dummy n d +nextDummy :: Positive (2 L.* (n+d)) => Dummy n d -> Dummy n d nextDummy d = Dummy { vec = vec dFst } where (dFst,dSnd) = nextDummy' d -nextDummy' :: Positive (2*(n+d)) => Dummy n d -> ( Dummy n d, Bool ) +nextDummy' :: Positive (2 L.* (n+d)) => Dummy n d -> ( Dummy n d, Bool ) nextDummy' _ = undefined 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/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr index 731a14b117..2309cdaaae 100644 --- a/testsuite/tests/polykinds/T10503.stderr +++ b/testsuite/tests/polykinds/T10503.stderr @@ -2,8 +2,8 @@ T10503.hs:8:6: error: • Could not deduce: k ~ * from the context: Proxy 'KProxy ~ Proxy 'KProxy - bound by the type signature for: - h :: (Proxy 'KProxy ~ Proxy 'KProxy) => r + bound by a type expected by the context: + (Proxy 'KProxy ~ Proxy 'KProxy) => r at T10503.hs:8:6-85 ‘k’ is a rigid type variable bound by the type signature for: 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/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr index 2cb4e61f19..a3b40c1222 100644 --- a/testsuite/tests/polykinds/T11142.stderr +++ b/testsuite/tests/polykinds/T11142.stderr @@ -1,7 +1,17 @@ -T11142.hs:9:8: error: - • The kind of variable ‘b’, namely ‘k’, - depends on variable ‘k’ from an inner scope - Perhaps bind ‘b’ sometime after binding ‘k’ - • In the type signature: +T11142.hs:9:49: error: + • Expected kind ‘k1’, but ‘b’ has kind ‘k0’ + • In the second argument of ‘SameKind’, namely ‘b’ + In the type signature: foo :: forall b. (forall k (a :: k). SameKind a b) -> () + +T11142.hs:10:7: error: + • Cannot instantiate unification variable ‘a0’ + with a type involving foralls: + (forall k1 (a :: k1). SameKind a b) -> () + GHC doesn't yet support impredicative polymorphism + • In the expression: undefined + In an equation for ‘foo’: foo = undefined + • Relevant bindings include + foo :: (forall k1 (a :: k1). SameKind a b) -> () + (bound at T11142.hs:10:1) diff --git a/testsuite/tests/polykinds/T11203.hs b/testsuite/tests/polykinds/T11203.hs new file mode 100644 index 0000000000..cff89dff79 --- /dev/null +++ b/testsuite/tests/polykinds/T11203.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PolyKinds, KindSignatures #-} + +module T11203 where + +data SameKind :: k -> k -> * + +data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b) diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr new file mode 100644 index 0000000000..5d62e00304 --- /dev/null +++ b/testsuite/tests/polykinds/T11203.stderr @@ -0,0 +1,4 @@ + +T11203.hs:7:24: error: + • Couldn't match ‘k1’ with ‘k2’ + • In the data declaration for ‘Q’ 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/T11466.stderr b/testsuite/tests/polykinds/T11466.stderr index f584731934..616f317250 100644 --- a/testsuite/tests/polykinds/T11466.stderr +++ b/testsuite/tests/polykinds/T11466.stderr @@ -1,6 +1,4 @@ T11466.hs:15:10: error: • Illegal implicit parameter ‘?x::Int’ - • In the context: Bla - While checking an instance declaration - In the instance declaration for ‘Eq T’ + • In the instance declaration for ‘Eq T’ 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/T11516.hs b/testsuite/tests/polykinds/T11516.hs index 3b19a997f9..66feeec387 100644 --- a/testsuite/tests/polykinds/T11516.hs +++ b/testsuite/tests/polykinds/T11516.hs @@ -3,6 +3,7 @@ {-# language ConstraintKinds #-} {-# language FlexibleInstances #-} {-# language FunctionalDependencies #-} +{-# language UndecidableInstances #-} import GHC.Exts (Constraint) diff --git a/testsuite/tests/polykinds/T11516.stderr b/testsuite/tests/polykinds/T11516.stderr index 5db11c8f83..5f8083309c 100644 --- a/testsuite/tests/polykinds/T11516.stderr +++ b/testsuite/tests/polykinds/T11516.stderr @@ -1,5 +1,5 @@ -T11516.hs:11:16: error: +T11516.hs:12:16: error: • Expected kind ‘i0 -> i0 -> *’, but ‘()’ has kind ‘*’ • In the first argument of ‘Varpi’, namely ‘()’ In the instance declaration for ‘Varpi (->) (->) (Either f)’ diff --git a/testsuite/tests/polykinds/T11520.hs b/testsuite/tests/polykinds/T11520.hs index fa5a3bf4a4..9c1d4fe1be 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, UndecidableInstances #-} module T11520 where diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr index 11a81baf62..93078aa23c 100644 --- a/testsuite/tests/polykinds/T11520.stderr +++ b/testsuite/tests/polykinds/T11520.stderr @@ -1,4 +1,10 @@ +T11520.hs:15:57: error: + • Illegal type synonym family application ‘Any’ in instance: + Typeable (Compose f g) + Use -fprint-explicit-kinds to see the kind arguments + • In the instance declaration for ‘Typeable (Compose f g)’ + T11520.hs:15:77: error: • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’ • In the second argument of ‘Compose’, namely ‘g’ 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 16d9f7ccff..ade4cbc79d 100644 --- a/testsuite/tests/polykinds/T11640.hs +++ b/testsuite/tests/polykinds/T11640.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE 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/T11648b.stderr b/testsuite/tests/polykinds/T11648b.stderr deleted file mode 100644 index e709e006b0..0000000000 --- a/testsuite/tests/polykinds/T11648b.stderr +++ /dev/null @@ -1,8 +0,0 @@ - -T11648b.hs:7: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: - k :: k0 - a :: Proxy k 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/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr new file mode 100644 index 0000000000..2e443e637b --- /dev/null +++ b/testsuite/tests/polykinds/T11821a.stderr @@ -0,0 +1,4 @@ + +T11821a.hs:4:31: error: + • Couldn't match ‘k1’ with ‘k2’ + • In the type declaration for ‘SameKind’ 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/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr index 4b551558a1..27123a8bc8 100644 --- a/testsuite/tests/polykinds/T12593.stderr +++ b/testsuite/tests/polykinds/T12593.stderr @@ -1,7 +1,6 @@ T12593.hs:11:16: error: - • Expecting two fewer arguments to ‘Free k k4 k5 p’ - Expected kind ‘k0 -> k1 -> *’, but ‘Free k k4 k5 p’ has kind ‘*’ + • Expected kind ‘k0 -> k1 -> *’, but ‘Free k k1 k2 p’ has kind ‘*’ • In the type signature: run :: k2 q => Free k k1 k2 p a b @@ -11,7 +10,7 @@ T12593.hs:12:31: error: • Expecting one more argument to ‘k’ Expected a type, but ‘k’ has kind - ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *) + ‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) -> Constraint’ • In the kind ‘k’ In the type signature: @@ -20,12 +19,98 @@ T12593.hs:12:31: error: -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b T12593.hs:12:40: error: - • Expecting two more arguments to ‘k4’ + • Expecting two more arguments to ‘k1’ Expected a type, but - ‘k4’ has kind - ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’ + ‘k1’ has kind + ‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’ • In the kind ‘k1’ In the type signature: run :: k2 q => Free k k1 k2 p a b -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:12:47: error: + • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint) + -> (k3 -> k4 -> *) -> *) + -> Constraint’ + with ‘*’ + When matching kinds + k3 :: * + k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint + • In the first argument of ‘p’, namely ‘c’ + In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:12:49: error: + • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) + -> (k3 -> k4 -> *) -> *’ + with ‘*’ + When matching kinds + k4 :: * + k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> * + • In the second argument of ‘p’, namely ‘d’ + In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:12:56: error: + • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint) + -> (k3 -> k4 -> *) -> *) + -> Constraint’ + with ‘*’ + When matching kinds + k0 :: * + k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint + • In the first argument of ‘q’, namely ‘c’ + In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:12:58: error: + • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) + -> (k3 -> k4 -> *) -> *’ + with ‘*’ + When matching kinds + k1 :: * + k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> * + • In the second argument of ‘q’, namely ‘d’ + In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:14:6: error: + • Couldn't match type ‘Free k2 p0’ with ‘Free k6 k7 k8 p’ + Expected type: Free k6 k7 k8 p a b + Actual type: Free k2 p0 a b + • In the pattern: Free cat + In an equation for ‘run’: run (Free cat) = cat + • Relevant bindings include + run :: Free k6 k7 k8 p a b + -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b + (bound at T12593.hs:14:1) + +T12593.hs:14:18: error: + • Couldn't match kind ‘*’ + with ‘(((k3 -> k4 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint’ + When matching kinds + k0 :: * + k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint + • In the expression: cat + In an equation for ‘run’: run (Free cat) = cat + • Relevant bindings include + cat :: forall (q :: k0 -> k1 -> *). + k2 q => + (forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b + (bound at T12593.hs:14:11) + run :: Free k6 k7 k8 p a b + -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b + (bound at T12593.hs:14:1) 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/T13391a.hs b/testsuite/tests/polykinds/T13391a.hs new file mode 100644 index 0000000000..4d5cc607c0 --- /dev/null +++ b/testsuite/tests/polykinds/T13391a.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module T13391a where + +-- this caused a panic during the work on T13391. + +data A a where + A3 :: b ~ Int => b -> A Int diff --git a/testsuite/tests/polykinds/T13393.stderr b/testsuite/tests/polykinds/T13393.stderr index 39ea640633..beea4732eb 100644 --- a/testsuite/tests/polykinds/T13393.stderr +++ b/testsuite/tests/polykinds/T13393.stderr @@ -8,7 +8,7 @@ T13393.hs:61:3: error: instance Traversable Identity -- Defined in ‘Data.Traversable’ instance Traversable Maybe -- Defined in ‘Data.Traversable’ ...plus two others - ...plus 24 instances involving out-of-scope types + ...plus 28 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In a stmt of a 'do' block: mapM putBackLeftOverInputAndReturnOutput undefined diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr deleted file mode 100644 index eaea0335cf..0000000000 --- a/testsuite/tests/polykinds/T13555.stderr +++ /dev/null @@ -1,40 +0,0 @@ - -T13555.hs:25:14: error: - • Couldn't match type ‘k0’ with ‘k2’ - because type variable ‘k2’ would escape its scope - This (rigid, skolem) type variable is bound by - the type signature for: - crtInfo :: forall k2 (m :: k2). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - at T13555.hs:25:14-79 - Expected type: TaggedT m Maybe (CRTInfo (GF fp d)) - Actual type: TaggedT m Maybe (CRTInfo (GF fp d)) - • When checking that instance signature for ‘crtInfo’ - is more general than its signature in the class - Instance sig: forall (m :: k0). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - Class sig: forall k2 (m :: k2). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - In the instance declaration for ‘CRTrans Maybe (GF fp d)’ - -T13555.hs:25:14: error: - • Could not deduce (Reflects m Int) - from the context: Reflects m Int - bound by the type signature for: - crtInfo :: forall k2 (m :: k2). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - at T13555.hs:25:14-79 - The type variable ‘k0’ is ambiguous - • When checking that instance signature for ‘crtInfo’ - is more general than its signature in the class - Instance sig: forall (m :: k0). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - Class sig: forall k2 (m :: k2). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - In the instance declaration for ‘CRTrans Maybe (GF fp d)’ 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 new file mode 100644 index 0000000000..8420ca9158 --- /dev/null +++ b/testsuite/tests/polykinds/T13738.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + + +module T13738 where + +import Data.Coerce +import Data.Proxy + +foo x = coerce @(forall (a :: k). Proxy a -> Int) + @(forall (a :: k). Proxy a -> Int) + x diff --git a/testsuite/tests/polykinds/T13738.stderr b/testsuite/tests/polykinds/T13738.stderr new file mode 100644 index 0000000000..0bcce304ba --- /dev/null +++ b/testsuite/tests/polykinds/T13738.stderr @@ -0,0 +1,4 @@ + +T13738.hs:12:31: error: Not in scope: type variable ‘k’ + +T13738.hs:13:31: error: Not in scope: type variable ‘k’ diff --git a/testsuite/tests/polykinds/T13985.hs b/testsuite/tests/polykinds/T13985.hs new file mode 100644 index 0000000000..c0555d8f69 --- /dev/null +++ b/testsuite/tests/polykinds/T13985.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module T13985 where + +import Data.Kind +import Data.Proxy + +data family Fam +data instance Fam = MkFam (forall (a :: k). Proxy a) + +type family T +type instance T = Proxy (Nothing :: Maybe a) + +class C k where + data CD :: k + type CT :: k + +instance C Type where + data CD = forall (a :: k). CD (Proxy a) + type CT = Proxy (Nothing :: Maybe a) + +class Z a where + type ZT a + type ZT a = Proxy (Nothing :: Maybe x) diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr new file mode 100644 index 0000000000..f60314a443 --- /dev/null +++ b/testsuite/tests/polykinds/T13985.stderr @@ -0,0 +1,39 @@ + +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 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 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 explicitly somewhere? + • In the data instance declaration for ‘CD’ + In the instance declaration for ‘C Type’ + +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 explicitly somewhere? + • In the type instance declaration for ‘CT’ + In the instance declaration for ‘C Type’ + +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 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/T14110.hs b/testsuite/tests/polykinds/T14110.hs new file mode 100644 index 0000000000..d2e8e71896 --- /dev/null +++ b/testsuite/tests/polykinds/T14110.hs @@ -0,0 +1,9 @@ +{-# Language TypeFamilies, ScopedTypeVariables, PolyKinds, DataKinds #-} + +import Data.Kind + +class R (c :: k -> Constraint) where + type R_ (c :: k -> Constraint) :: k -> Type + +instance R Eq where + type R_ Eq a = a -> a -> Bool diff --git a/testsuite/tests/polykinds/T14110.stderr b/testsuite/tests/polykinds/T14110.stderr new file mode 100644 index 0000000000..aedfacb324 --- /dev/null +++ b/testsuite/tests/polykinds/T14110.stderr @@ -0,0 +1,5 @@ + +T14110.hs:9:8: error: + • Number of parameters must match family declaration; expected 1 + • In the type instance declaration for ‘R_’ + In the instance declaration for ‘R Eq’ diff --git a/testsuite/tests/polykinds/T14172.hs b/testsuite/tests/polykinds/T14172.hs new file mode 100644 index 0000000000..10fff5af69 --- /dev/null +++ b/testsuite/tests/polykinds/T14172.hs @@ -0,0 +1,7 @@ +module T14172 where + +import Data.Functor.Compose +import T14172a + +traverseCompose :: (a -> f b) -> g a -> f (h _) +traverseCompose = _Wrapping Compose . traverse diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr new file mode 100644 index 0000000000..487b006ec1 --- /dev/null +++ b/testsuite/tests/polykinds/T14172.stderr @@ -0,0 +1,40 @@ + +T14172.hs:6:46: error: + • Found type wildcard ‘_’ standing for ‘a'’ + Where: ‘a'’ is a rigid type variable bound by + the inferred type of + traverseCompose :: (a -> f b) -> g a -> f (h a') + at T14172.hs:7:1-46 + To use the inferred type, enable PartialTypeSignatures + • In the type signature: + traverseCompose :: (a -> f b) -> g a -> f (h _) + +T14172.hs:7:19: error: + • Occurs check: cannot construct the infinite type: a ~ g'1 a + Expected type: (f'0 a -> f (f'0 b)) + -> Compose f'0 g'1 a -> f (h a') + Actual type: (Unwrapped (Compose f'0 g'1 a) + -> f (Unwrapped (h a'))) + -> Compose f'0 g'1 a -> f (h a') + • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’ + In the expression: _Wrapping Compose . traverse + In an equation for ‘traverseCompose’: + traverseCompose = _Wrapping Compose . traverse + • Relevant bindings include + traverseCompose :: (a -> f b) -> g a -> f (h a') + (bound at T14172.hs:7:1) + +T14172.hs:7:19: error: + • Couldn't match type ‘g’ with ‘Compose f'0 g'1’ + ‘g’ is a rigid type variable bound by + the inferred type of + traverseCompose :: (a -> f b) -> g a -> f (h a') + at T14172.hs:7:1-46 + Expected type: (a -> f b) -> g a -> f (h a') + Actual type: (a -> f b) -> Compose f'0 g'1 a -> f (h a') + • In the expression: _Wrapping Compose . traverse + In an equation for ‘traverseCompose’: + traverseCompose = _Wrapping Compose . traverse + • Relevant bindings include + traverseCompose :: (a -> f b) -> g a -> f (h a') + (bound at T14172.hs:7:1) diff --git a/testsuite/tests/polykinds/T14172a.hs b/testsuite/tests/polykinds/T14172a.hs new file mode 100644 index 0000000000..b831372781 --- /dev/null +++ b/testsuite/tests/polykinds/T14172a.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module T14172a where + +import Data.Coerce +import Data.Functor.Compose +import Data.Functor.Identity + +class Profunctor p where + dimap :: (a -> b) -> (c -> d) -> p b c -> p a d + (#.) :: Coercible c b => (b -> c) -> p a b -> p a c + +instance Profunctor (->) where + dimap ab cd bc = cd . bc . ab + {-# INLINE dimap #-} + (#.) _ = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b + {-# INLINE (#.) #-} + +type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t) +type Iso' s a = Iso s s a a + +iso :: (s -> a) -> (b -> t) -> Iso s t a b +iso sa bt = dimap sa (fmap bt) +{-# INLINE iso #-} + +type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t) + +data Exchange a b s t = Exchange (s -> a) (b -> t) + +instance Profunctor (Exchange a b) where + dimap f g (Exchange sa bt) = Exchange (sa . f) (g . bt) + {-# INLINE dimap #-} + (#.) _ = coerce + {-# INLINE ( #. ) #-} + +withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r +withIso ai k = case ai (Exchange id Identity) of + Exchange sa bt -> k sa (runIdentity #. bt) +{-# INLINE withIso #-} + +class Wrapped s where + type Unwrapped s :: * + _Wrapped' :: Iso' s (Unwrapped s) + +class Wrapped s => Rewrapped (s :: *) (t :: *) + +class (Rewrapped s t, Rewrapped t s) => Rewrapping s t +instance (Rewrapped s t, Rewrapped t s) => Rewrapping s t + +instance (t ~ Compose f' g' a') => Rewrapped (Compose f g a) t +instance Wrapped (Compose f g a) where + type Unwrapped (Compose f g a) = f (g a) + _Wrapped' = iso getCompose Compose + +_Wrapping :: Rewrapping s t => (Unwrapped s -> s) -> Iso s t (Unwrapped s) (Unwrapped t) +_Wrapping _ = _Wrapped +{-# INLINE _Wrapping #-} + +_Wrapped :: Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t) +_Wrapped = withIso _Wrapped' $ \ sa _ -> withIso _Wrapped' $ \ _ bt -> iso sa bt +{-# INLINE _Wrapped #-} diff --git a/testsuite/tests/polykinds/T14174.hs b/testsuite/tests/polykinds/T14174.hs new file mode 100644 index 0000000000..3fe4996225 --- /dev/null +++ b/testsuite/tests/polykinds/T14174.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE RankNTypes, KindSignatures, PolyKinds #-} +module T14174 where + +data T k (x :: k) = MkT + +data S x = MkS (T (x Int) x) diff --git a/testsuite/tests/polykinds/T14174.stderr b/testsuite/tests/polykinds/T14174.stderr new file mode 100644 index 0000000000..4aafa647fd --- /dev/null +++ b/testsuite/tests/polykinds/T14174.stderr @@ -0,0 +1,7 @@ + +T14174.hs:6:27: error: + • Expecting one more argument to ‘x’ + Expected kind ‘x Int’, but ‘x’ has kind ‘* -> *’ + • In the second argument of ‘T’, namely ‘x’ + In the type ‘(T (x Int) x)’ + In the definition of data constructor ‘MkS’ diff --git a/testsuite/tests/polykinds/T14174a.hs b/testsuite/tests/polykinds/T14174a.hs new file mode 100644 index 0000000000..bdd3d7ee88 --- /dev/null +++ b/testsuite/tests/polykinds/T14174a.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module T14174a where + +import Data.Kind + +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 +type a @@ b = Apply a b +infixl 9 @@ + +data FunArrow = (:->) | (:~>) + +class FunType (arr :: FunArrow) where + type Fun (k1 :: Type) arr (k2 :: Type) :: Type + +class FunType arr => AppType (arr :: FunArrow) where + type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 + +type FunApp arr = (FunType arr, AppType arr) + +instance FunType (:->) where + type Fun k1 (:->) k2 = k1 -> k2 + +instance AppType (:->) where + type App k1 (:->) k2 (f :: k1 -> k2) x = f x + +instance FunType (:~>) where + type Fun k1 (:~>) k2 = k1 ~> k2 + +instance AppType (:~>) where + type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x + +infixr 0 -?> +type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 + +type family ElimBool (p :: Bool -> Type) + (z :: Bool) + (pFalse :: p False) + (pTrue :: p True) + :: p z where + -- Commenting out the line below makes the panic go away + ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue + +type family ElimBoolPoly (arr :: FunArrow) + (p :: (Bool -?> Type) arr) + (z :: Bool) + (pFalse :: App Bool arr Type p False) + (pTrue :: App Bool arr Type p True) + :: App Bool arr Type p z diff --git a/testsuite/tests/polykinds/T14174a.stderr b/testsuite/tests/polykinds/T14174a.stderr new file mode 100644 index 0000000000..139597f9cb --- /dev/null +++ b/testsuite/tests/polykinds/T14174a.stderr @@ -0,0 +1,2 @@ + + diff --git a/testsuite/tests/polykinds/T14209.hs b/testsuite/tests/polykinds/T14209.hs new file mode 100644 index 0000000000..0f0648bd79 --- /dev/null +++ b/testsuite/tests/polykinds/T14209.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE DataKinds, PolyKinds #-} +module T14209 where + +data MyProxy k (a :: k) = MyProxy +data Foo (z :: MyProxy k (a :: k)) diff --git a/testsuite/tests/polykinds/T14265.hs b/testsuite/tests/polykinds/T14265.hs new file mode 100644 index 0000000000..84c1a025a1 --- /dev/null +++ b/testsuite/tests/polykinds/T14265.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE PolyKinds #-} + +module T124265 where + +import Control.Monad.Trans.State( StateT ) + +f :: proxy _ -> () +f _ = () + +foo :: StateT _ _ () +foo = undefined diff --git a/testsuite/tests/polykinds/T14265.stderr b/testsuite/tests/polykinds/T14265.stderr new file mode 100644 index 0000000000..be6868fdc4 --- /dev/null +++ b/testsuite/tests/polykinds/T14265.stderr @@ -0,0 +1,24 @@ + +T14265.hs:7:12: error: + • Found type wildcard ‘_’ standing for ‘w :: k’ + Where: ‘w’, ‘k’ are rigid type variables bound by + the inferred type of f :: proxy w -> () + at T14265.hs:8:1-8 + To use the inferred type, enable PartialTypeSignatures + • In the type signature: f :: proxy _ -> () + +T14265.hs:10:15: error: + • Found type wildcard ‘_’ standing for ‘w’ + Where: ‘w’ is a rigid type variable bound by + the inferred type of foo :: StateT w w1 () + at T14265.hs:11:1-15 + To use the inferred type, enable PartialTypeSignatures + • In the type signature: foo :: StateT _ _ () + +T14265.hs:10:17: error: + • Found type wildcard ‘_’ standing for ‘w1 :: * -> *’ + Where: ‘w1’ is a rigid type variable bound by + the inferred type of foo :: StateT w w1 () + at T14265.hs:11:1-15 + To use the inferred type, enable PartialTypeSignatures + • In the type signature: foo :: StateT _ _ () diff --git a/testsuite/tests/polykinds/T14270.hs b/testsuite/tests/polykinds/T14270.hs new file mode 100644 index 0000000000..3eed83c657 --- /dev/null +++ b/testsuite/tests/polykinds/T14270.hs @@ -0,0 +1,110 @@ +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE PolyKinds #-} +module T14270 (pattern App) where + +import Data.Kind (Type) +import GHC.Fingerprint (Fingerprint, fingerprintFingerprints) +import GHC.Types (RuntimeRep, TYPE, TyCon) + +data (a :: k1) :~~: (b :: k2) where + HRefl :: a :~~: a + +data TypeRep (a :: k) where + TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep] + -> TypeRep (a :: k) + + TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). + {-# UNPACK #-} !Fingerprint + -> TypeRep (a :: k1 -> k2) + -> TypeRep (b :: k1) + -> TypeRep (a b) + + TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + {-# UNPACK #-} !Fingerprint + -> TypeRep a + -> TypeRep b + -> TypeRep (a -> b) + +data SomeTypeRep where + SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep + +typeRepFingerprint :: TypeRep a -> Fingerprint +typeRepFingerprint = undefined + +mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). + TypeRep (a :: k1 -> k2) + -> TypeRep (b :: k1) + -> TypeRep (a b) +mkTrApp rep@(TrApp _ (TrTyCon _ con _) (x :: TypeRep x)) (y :: TypeRep y) + | con == funTyCon -- cheap check first + , Just (IsTYPE (rx :: TypeRep rx)) <- isTYPE (typeRepKind x) + , Just (IsTYPE (ry :: TypeRep ry)) <- isTYPE (typeRepKind y) + , Just HRefl <- withTypeable x $ withTypeable rx $ withTypeable ry + $ typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep + = undefined +mkTrApp a b = TrApp fpr a b + where + fpr_a = typeRepFingerprint a + fpr_b = typeRepFingerprint b + fpr = fingerprintFingerprints [fpr_a, fpr_b] + +pattern App :: forall k2 (t :: k2). () + => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b) + => TypeRep a -> TypeRep b -> TypeRep t +pattern App f x <- (splitApp -> Just (IsApp f x)) + where App f x = mkTrApp f x + +data IsApp (a :: k) where + IsApp :: forall k k' (f :: k' -> k) (x :: k'). () + => TypeRep f -> TypeRep x -> IsApp (f x) + +splitApp :: forall k (a :: k). () + => TypeRep a + -> Maybe (IsApp a) +splitApp (TrApp _ f x) = Just (IsApp f x) +splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b) + where arr = bareArrow rep +splitApp (TrTyCon{}) = Nothing + +withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r +withTypeable = undefined + +eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). + TypeRep a -> TypeRep b -> Maybe (a :~~: b) +eqTypeRep = undefined + +typeRepKind :: TypeRep (a :: k) -> TypeRep k +typeRepKind = undefined + +bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). () + => TypeRep (a -> b) + -> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type) +bareArrow = undefined + +data IsTYPE (a :: Type) where + IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r) + +isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a) +isTYPE = undefined + +class Typeable (a :: k) where + +typeRep :: Typeable a => TypeRep a +typeRep = undefined + +funTyCon :: TyCon +funTyCon = undefined + +instance (Typeable f, Typeable a) => Typeable (f a) +instance Typeable ((->) :: TYPE r -> TYPE s -> Type) +instance Typeable TYPE diff --git a/testsuite/tests/polykinds/T14450.hs b/testsuite/tests/polykinds/T14450.hs new file mode 100644 index 0000000000..8571829619 --- /dev/null +++ b/testsuite/tests/polykinds/T14450.hs @@ -0,0 +1,33 @@ +{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, + ConstraintKinds, TypeFamilies, DataKinds, GADTs, + AllowAmbiguousTypes, InstanceSigs #-} + +module T14450 where + +import Data.Kind + +data TyFun :: Type -> Type -> Type + +type a ~> b = TyFun a b -> Type + +type Cat ob = ob -> ob -> Type + +type SameKind (a :: k) (b :: k) = (() :: Constraint) + +type family Apply (f :: a ~> b) (x :: a) :: b where + Apply IddSym0 x = Idd x + +class Varpi (f :: i ~> j) where + type Dom (f :: i ~> j) :: Cat i + type Cod (f :: i ~> j) :: Cat j + + varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a') + +type family Idd (a::k) :: k where + Idd (a::k) = a + +data IddSym0 :: k ~> k where + IddSym0KindInference :: IddSym0 l + +instance Varpi (IddSym0 :: k ~> k) where + type Dom (IddSym0 :: Type ~> Type) = (->) diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr new file mode 100644 index 0000000000..e8ff4aeae3 --- /dev/null +++ b/testsuite/tests/polykinds/T14450.stderr @@ -0,0 +1,8 @@ + +T14450.hs:33:12: error: + • Expected kind ‘k ~> k’, + but ‘(IddSym0 :: Type ~> Type)’ has kind ‘* ~> *’ + • In the first argument of ‘Dom’, namely + ‘(IddSym0 :: Type ~> Type)’ + In the type instance declaration for ‘Dom’ + In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’ diff --git a/testsuite/tests/polykinds/T14515.hs b/testsuite/tests/polykinds/T14515.hs new file mode 100644 index 0000000000..4a2540b925 --- /dev/null +++ b/testsuite/tests/polykinds/T14515.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +module Bug where + +import Data.Kind + +type HRank1 ty = forall k1. k1 -> ty +type HRank2 ty = forall k2. k2 -> ty + +data HREFL11 :: HRank1 (HRank1 Type) -- FAILS +data HREFL12 :: HRank1 (HRank2 Type) +data HREFL21 :: HRank2 (HRank1 Type) +data HREFL22 :: HRank2 (HRank2 Type) -- FAILS diff --git a/testsuite/tests/polykinds/T14520.hs b/testsuite/tests/polykinds/T14520.hs new file mode 100644 index 0000000000..44dc2ee18d --- /dev/null +++ b/testsuite/tests/polykinds/T14520.hs @@ -0,0 +1,16 @@ +{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators, AllowAmbiguousTypes #-} + +module T14520 where + +import Data.Kind + +type a ~>> b = (a, b) -> Type + +data family Sing (a::k) + +type family XXX (f::a~>>b) (x::a) :: 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/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr new file mode 100644 index 0000000000..9c290ff4a5 --- /dev/null +++ b/testsuite/tests/polykinds/T14520.stderr @@ -0,0 +1,6 @@ + +T14520.hs:15:24: error: + • Expected kind ‘bat w w’, + but ‘Id’ has kind ‘XXX a0 * (XXX a0 (a0 ~>> *) kat0 b0) b0’ + • In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’ + In the type signature: sId :: Sing w -> Sing (Id :: bat w w) diff --git a/testsuite/tests/polykinds/T14555.hs b/testsuite/tests/polykinds/T14555.hs new file mode 100644 index 0000000000..7f37a5ec9c --- /dev/null +++ b/testsuite/tests/polykinds/T14555.hs @@ -0,0 +1,12 @@ +{-# Language TypeOperators, DataKinds, PolyKinds, GADTs #-} + + +module T14555 where + +import Data.Kind +import GHC.Types (TYPE, Type) + +data Exp :: [TYPE rep] -> TYPE rep -> Type where +--data Exp (x :: [TYPE rep]) (y :: TYPE rep) where +--data Exp (x :: [TYPE rep]) y where + Lam :: Exp (a:xs) b -> Exp xs (a -> b) diff --git a/testsuite/tests/polykinds/T14555.stderr b/testsuite/tests/polykinds/T14555.stderr new file mode 100644 index 0000000000..66fb55ae4f --- /dev/null +++ b/testsuite/tests/polykinds/T14555.stderr @@ -0,0 +1,6 @@ + +T14555.hs:12:34: error: + • Expected kind ‘TYPE rep’, but ‘a -> b’ has kind ‘*’ + • In the second argument of ‘Exp’, namely ‘(a -> b)’ + In the type ‘Exp xs (a -> b)’ + In the definition of data constructor ‘Lam’ diff --git a/testsuite/tests/polykinds/T14561.hs b/testsuite/tests/polykinds/T14561.hs new file mode 100644 index 0000000000..7b1f17e08e --- /dev/null +++ b/testsuite/tests/polykinds/T14561.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MagicHash #-} + +module T14561 where + +import GHC.Types +import GHC.Prim + +badId :: forall (a :: TYPE r). a -> a +badId = unsafeCoerce# +-- Un-saturated application of a levity-polymorphic +-- function that must be eta-expanded + +goodId :: forall (a :: Type). a -> a +goodId = unsafeCoerce# +-- But this one is OK diff --git a/testsuite/tests/polykinds/T14561.stderr b/testsuite/tests/polykinds/T14561.stderr new file mode 100644 index 0000000000..d39dec4d7b --- /dev/null +++ b/testsuite/tests/polykinds/T14561.stderr @@ -0,0 +1,5 @@ + +T14561.hs:12:9: error: + Cannot use primitive with levity-polymorphic arguments: + unsafeCoerce# :: a -> a + Levity-polymorphic arguments: a :: TYPE r diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs new file mode 100644 index 0000000000..bdc05dd6df --- /dev/null +++ b/testsuite/tests/polykinds/T14563.hs @@ -0,0 +1,9 @@ +{-# Language RankNTypes, KindSignatures, PolyKinds #-} +{-# OPTIONS_GHC -fprint-explicit-runtime-reps #-} + +import GHC.Types (TYPE) +import Data.Kind + +data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where + Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. + (g xx -> a) -> h xx -> Lan g h a diff --git a/testsuite/tests/polykinds/T14563.stderr b/testsuite/tests/polykinds/T14563.stderr new file mode 100644 index 0000000000..1265ec0e3a --- /dev/null +++ b/testsuite/tests/polykinds/T14563.stderr @@ -0,0 +1,7 @@ + +T14563.hs:9:39: error: + • Expected kind ‘TYPE rep -> TYPE rep''’, + but ‘h’ has kind ‘TYPE rep -> *’ + • In the second argument of ‘Lan’, namely ‘h’ + In the type ‘Lan g h a’ + In the definition of data constructor ‘Lan’ diff --git a/testsuite/tests/polykinds/T14580.hs b/testsuite/tests/polykinds/T14580.hs new file mode 100644 index 0000000000..58983cc117 --- /dev/null +++ b/testsuite/tests/polykinds/T14580.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE PolyKinds, DataKinds, TypeOperators #-} +module T14580 where +import Data.Kind + +type Cat ob = ob -> ob -> Type +data ISO' :: Cat i -> i -> i -> Type +type ISO cat a b = ISO' cat a b -> Type +type (a <--> b) iso cat = ISO (iso :: cat a b) diff --git a/testsuite/tests/polykinds/T14580.stderr b/testsuite/tests/polykinds/T14580.stderr new file mode 100644 index 0000000000..babbb49cf8 --- /dev/null +++ b/testsuite/tests/polykinds/T14580.stderr @@ -0,0 +1,6 @@ + +T14580.hs:8:31: error: + • Expected kind ‘Cat a’, but ‘(iso :: cat a b)’ has kind ‘cat a b’ + • In the first argument of ‘ISO’, namely ‘(iso :: cat a b)’ + In the type ‘ISO (iso :: cat a b)’ + In the type declaration for ‘<-->’ diff --git a/testsuite/tests/polykinds/T14710.hs b/testsuite/tests/polykinds/T14710.hs new file mode 100644 index 0000000000..2fec10a7a1 --- /dev/null +++ b/testsuite/tests/polykinds/T14710.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +module T14710 where + +import Data.Proxy + +class C a b where + c1 :: Proxy (x :: a) -> b + c2 :: forall (x :: a). Proxy x -> b + +f :: forall a. a -> a +f x = const x (const g1 g2) + where + g1 :: Proxy (x :: a) + g1 = Proxy + + g2 :: forall (x :: a). Proxy x + g2 = Proxy + +h1 :: forall k a. Proxy (a :: k) +h1 = Proxy + +h2 :: forall k (a :: k). Proxy a +h2 = Proxy diff --git a/testsuite/tests/polykinds/T14710.stderr b/testsuite/tests/polykinds/T14710.stderr new file mode 100644 index 0000000000..0bbfb0d641 --- /dev/null +++ b/testsuite/tests/polykinds/T14710.stderr @@ -0,0 +1,30 @@ + +T14710.hs:9:21: error: + Unexpected kind variable ‘a’ + Perhaps you intended to use PolyKinds + In a class method signature for ‘c1’ + +T14710.hs:10:22: error: + Unexpected kind variable ‘a’ + Perhaps you intended to use PolyKinds + In a class method signature for ‘c2’ + +T14710.hs:15:23: error: + Unexpected kind variable ‘a’ + Perhaps you intended to use PolyKinds + In the type signature for ‘g1’ + +T14710.hs:18:24: error: + Unexpected kind variable ‘a’ + Perhaps you intended to use PolyKinds + In the type signature for ‘g2’ + +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: + Unexpected kind variable ‘k’ + Perhaps you intended to use PolyKinds + In the type signature for ‘h2’ diff --git a/testsuite/tests/polykinds/T14723.hs b/testsuite/tests/polykinds/T14723.hs new file mode 100644 index 0000000000..9b2f3bf75e --- /dev/null +++ b/testsuite/tests/polykinds/T14723.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module T14723 () where + +import Data.Coerce( coerce ) +import Data.Kind (Type) +import Data.Proxy (Proxy(..)) +import Data.String (fromString) +import Data.Int (Int64) +import GHC.Stack (HasCallStack) +import GHC.TypeLits (Nat, Symbol) + +data JType = Iface Symbol + +data J (a :: JType) + +newIterator + :: IO (J ('Iface "java.util.Iterator")) +newIterator = do + let tblPtr :: Int64 + tblPtr = undefined + iterator <- + (qqMarker (Proxy :: Proxy "wuggle") + (Proxy :: Proxy "waggle") + (Proxy :: Proxy "tblPtr") + (Proxy :: Proxy 106) + (tblPtr, ()) + Proxy + (undefined :: IO Int)) + undefined + +class Coercible (a :: Type) where + type Ty a :: JType + +instance Coercible Int64 where + type Ty Int64 = Iface "Int64" +instance Coercible Int where + type Ty Int = Iface "Int" + +class Coercibles xs (tys :: k) | xs -> tys +instance Coercibles () () +instance (ty ~ Ty x, Coercible x, Coercibles xs tys) => Coercibles (x, xs) '(ty, tys) + +qqMarker + :: forall + -- k -- the kind variable shows up in Core + (args_tys :: k) -- JType's of arguments + tyres -- JType of result + (input :: Symbol) -- input string of the quasiquoter + (mname :: Symbol) -- name of the method to generate + (antiqs :: Symbol) -- antiquoted variables as a comma-separated list + (line :: Nat) -- line number of the quasiquotation + args_tuple -- uncoerced argument types + b. -- uncoerced result type + (tyres ~ Ty b, Coercibles args_tuple args_tys, Coercible b, HasCallStack) + => Proxy input + -> Proxy mname + -> Proxy antiqs + -> Proxy line + -> args_tuple + -> Proxy args_tys + -> IO b + -> IO b +qqMarker = undefined diff --git a/testsuite/tests/polykinds/T14846.hs b/testsuite/tests/polykinds/T14846.hs new file mode 100644 index 0000000000..0f70962562 --- /dev/null +++ b/testsuite/tests/polykinds/T14846.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DataKinds, PolyKinds #-} +module T14846 where + +import Data.Kind +import Data.Proxy + +type Cat ob = ob -> ob -> Type + +data Struct :: (k -> Constraint) -> Type where + S :: Proxy (a::k) -> Struct (cls::k -> Constraint) + +type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls) + +data AStruct :: Struct cls -> Type where + AStruct :: cls a => AStruct (Structured a cls) + +class StructI xx (structured::Struct (cls :: k -> Constraint)) where + struct :: AStruct structured + +instance (Structured xx cls ~ structured, cls xx) => StructI xx structured where + struct :: AStruct (Structured xx cls) + struct = AStruct + +data Hom :: Cat k -> Cat (Struct cls) where + +class Category (cat::Cat ob) where + i :: StructI xx a => ríki a a + +instance Category riki => Category (Hom riki :: Cat (Struct cls)) where + i :: forall xx a. StructI xx a => Hom riki a a + i = case struct :: AStruct (Structured a cls) of diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr new file mode 100644 index 0000000000..1d852031d9 --- /dev/null +++ b/testsuite/tests/polykinds/T14846.stderr @@ -0,0 +1,48 @@ + +T14846.hs:38:8: error: + • Couldn't match type ‘ríki’ with ‘Hom riki’ + ‘ríki’ is a rigid type variable bound by + the type signature for: + i :: forall k5 (cls2 :: k5 + -> Constraint) k6 (xx :: k6) (a :: Struct cls2) (ríki :: Struct + cls2 + -> Struct + cls2 + -> *). + StructI xx a => + ríki a a + at T14846.hs:38:8-48 + Expected type: ríki a a + Actual type: Hom riki a a + • When checking that instance signature for ‘i’ + is more general than its signature in the class + Instance sig: forall k1 (cls :: k1 + -> Constraint) k2 (xx :: k2) (a :: Struct cls). + StructI xx a => + Hom riki a a + Class sig: forall k1 (cls :: k1 + -> Constraint) k2 (xx :: k2) (a :: Struct + cls) (ríki :: Struct + cls + -> Struct + cls + -> *). + StructI xx a => + ríki a a + In the instance declaration for ‘Category (Hom riki)’ + +T14846.hs:39:31: error: + • Couldn't match kind ‘k4’ with ‘Struct cls2’ + ‘k4’ is a rigid type variable bound by + the instance declaration + at T14846.hs:37:10-65 + When matching kinds + cls1 :: k4 -> Constraint + cls0 :: Struct cls -> Constraint + Expected kind ‘Struct cls0’, + but ‘Structured a cls’ has kind ‘Struct cls1’ + • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’ + In an expression type signature: AStruct (Structured a cls) + In the expression: struct :: AStruct (Structured a cls) + • Relevant bindings include + i :: Hom riki a a (bound at T14846.hs:39:3) diff --git a/testsuite/tests/polykinds/T14873.hs b/testsuite/tests/polykinds/T14873.hs new file mode 100644 index 0000000000..9450a019bc --- /dev/null +++ b/testsuite/tests/polykinds/T14873.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +module T14873 where + +import Data.Kind (Type) + +data family Sing (a :: k) + +newtype instance Sing (f :: k1 ~> k2) = + SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } + +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> +type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 + +class SingI (a :: k) where + sing :: Sing a + +data ColSym1 :: f a -> a ~> Bool +type instance Apply (ColSym1 x) y = Col x y + +class PColumn (f :: Type -> Type) where + type Col (x :: f a) (y :: a) :: Bool + +class SColumn (f :: Type -> Type) where + sCol :: forall (x :: f a) (y :: a). + Sing x -> Sing y -> Sing (Col x y :: Bool) + +instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where + sing = SLambda (sCol (sing @_ @x)) + +{- When the bug was present, this smaller kind-incorrect version also + elicited the same piResultTy crash + + But it's kind-incorrect, whereas the main test case should compile file + +class SingI (a :: k) where + +class SColumn (f :: Type -> Type) where + +instance -- forall (f :: Type -> Type) a (x :: f a). + SColumn f => SingI (x :: f a) +-} + diff --git a/testsuite/tests/polykinds/T14939.hs b/testsuite/tests/polykinds/T14939.hs new file mode 100644 index 0000000000..eb3c700f9f --- /dev/null +++ b/testsuite/tests/polykinds/T14939.hs @@ -0,0 +1,19 @@ +{-# Language RankNTypes, ConstraintKinds, TypeInType, GADTs #-} + +module T14939 where + +import Data.Kind + +type Cat ob = ob -> ob -> Type + +type Alg cls ob = ob + +newtype Frí (cls::Type -> Constraint) :: (Type -> Alg cls Type) where + Frí :: { with :: forall x. cls x => (a -> x) -> x } + -> Frí cls a + +data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where + AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b + +leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b) +leftAdj (AlgCat f) a = undefined
\ No newline at end of file diff --git a/testsuite/tests/polykinds/T15116.hs b/testsuite/tests/polykinds/T15116.hs new file mode 100644 index 0000000000..7089b52383 --- /dev/null +++ b/testsuite/tests/polykinds/T15116.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs, PolyKinds, DataKinds #-} +module T15116 where + +import Data.Proxy + +data A (a :: k) where + MkA :: A MkA + + diff --git a/testsuite/tests/polykinds/T15116.stderr b/testsuite/tests/polykinds/T15116.stderr new file mode 100644 index 0000000000..bcbf89f8dc --- /dev/null +++ b/testsuite/tests/polykinds/T15116.stderr @@ -0,0 +1,7 @@ + +T15116.hs:7:12: error: + • Data constructor ‘MkA’ cannot be used here + (it is defined and used in the same recursive group) + • In the first argument of ‘A’, namely ‘MkA’ + In the type ‘A MkA’ + In the definition of data constructor ‘MkA’ diff --git a/testsuite/tests/polykinds/T15116a.hs b/testsuite/tests/polykinds/T15116a.hs new file mode 100644 index 0000000000..8f69e4d87a --- /dev/null +++ b/testsuite/tests/polykinds/T15116a.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE PolyKinds, DataKinds #-} +module T15116a where + +import Data.Proxy + +data B = MkB (Proxy 'MkB) diff --git a/testsuite/tests/polykinds/T15116a.stderr b/testsuite/tests/polykinds/T15116a.stderr new file mode 100644 index 0000000000..7e4788f5b8 --- /dev/null +++ b/testsuite/tests/polykinds/T15116a.stderr @@ -0,0 +1,7 @@ + +T15116a.hs:6:21: error: + • Data constructor ‘MkB’ cannot be used here + (it is defined and used in the same recursive group) + • In the first argument of ‘Proxy’, namely ‘ 'MkB’ + In the type ‘(Proxy 'MkB)’ + In the definition of data constructor ‘MkB’ diff --git a/testsuite/tests/polykinds/T15170.hs b/testsuite/tests/polykinds/T15170.hs new file mode 100644 index 0000000000..02de90ae12 --- /dev/null +++ b/testsuite/tests/polykinds/T15170.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DataKinds, PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +module T15170 where + +import Data.Kind +import Data.Proxy + +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 +type f @@ x = Apply f x +infixl 9 @@ + +wat :: forall (a :: Type) + (b :: a ~> Type) + (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type) + (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y) + (x :: a). + (forall (xx :: a) (yy :: b @@ xx). Proxy (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy))) + -> () +wat _ = () diff --git a/testsuite/tests/polykinds/T15577.hs b/testsuite/tests/polykinds/T15577.hs new file mode 100644 index 0000000000..18ebc42f92 --- /dev/null +++ b/testsuite/tests/polykinds/T15577.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +module Bug where + +import Data.Kind +import Data.Proxy +import Data.Type.Equality + +type family F (x :: f (a :: k)) :: f a + +f :: forall k (f :: k -> Type) (a :: k) (r :: f a). Proxy r -> F r :~: r +f = undefined + +g :: forall (f :: Type -> Type) (a :: Type) (r :: f a). Proxy r -> F r :~: r +g r | Refl <- f -- Uncommenting the line below makes it work again + -- @Type + @f @a @r r + = Refl diff --git a/testsuite/tests/polykinds/T15577.stderr b/testsuite/tests/polykinds/T15577.stderr new file mode 100644 index 0000000000..fef17090f8 --- /dev/null +++ b/testsuite/tests/polykinds/T15577.stderr @@ -0,0 +1,71 @@ + +T15577.hs:20:18: error: + • Expecting one more argument to ‘f’ + Expected a type, but ‘f’ has kind ‘* -> *’ + • In the type ‘f’ + In a stmt of a pattern guard for + an equation for ‘g’: + Refl <- f @f @a @r r + In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl + +T15577.hs:20:21: error: + • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’ + • In the type ‘a’ + In a stmt of a pattern guard for + an equation for ‘g’: + Refl <- f @f @a @r r + In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl + • Relevant bindings include + r :: Proxy r1 (bound at T15577.hs:18:3) + g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1) + +T15577.hs:20:24: error: + • Couldn't match kind ‘* -> *’ with ‘*’ + When matching kinds + f1 :: * -> * + f1 a1 :: * + Expected kind ‘f1’, but ‘r’ has kind ‘f1 a1’ + • In the type ‘r’ + In a stmt of a pattern guard for + an equation for ‘g’: + Refl <- f @f @a @r r + In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl + • Relevant bindings include + r :: Proxy r1 (bound at T15577.hs:18:3) + g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1) + +T15577.hs:20:26: error: + • Couldn't match kind ‘* -> *’ with ‘*’ + When matching kinds + f1 :: * -> * + a1 :: * + • In the fourth argument of ‘f’, namely ‘r’ + In a stmt of a pattern guard for + an equation for ‘g’: + Refl <- f @f @a @r r + In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl + • Relevant bindings include + r :: Proxy r1 (bound at T15577.hs:18:3) + g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1) + +T15577.hs:21:7: error: + • Could not deduce: F r1 ~ r1 + from the context: r0 ~ F r0 + bound by a pattern with constructor: + Refl :: forall k (a :: k). a :~: a, + in a pattern binding in + a pattern guard for + an equation for ‘g’ + at T15577.hs:18:7-10 + ‘r1’ is a rigid type variable bound by + the type signature for: + g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1). + Proxy r1 -> F r1 :~: r1 + at T15577.hs:17:1-76 + Expected type: F r1 :~: r1 + Actual type: r1 :~: r1 + • In the expression: Refl + In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl + • Relevant bindings include + r :: Proxy r1 (bound at T15577.hs:18:3) + g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1) 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 d85166b0bb..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)’ - In the type ‘I (U1 DFInt)’ - In the definition of data constructor ‘I1’ +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)’ 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 deleted file mode 100644 index 4c31bb4aa4..0000000000 --- a/testsuite/tests/polykinds/T6039.stderr +++ /dev/null @@ -1,5 +0,0 @@ - -T6039.hs:5:14: error: - • Expecting one fewer arguments to ‘j’ - Expected kind ‘* -> *’, but ‘j’ has kind ‘*’ - • In the kind ‘j k’ 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/T7224.stderr b/testsuite/tests/polykinds/T7224.stderr index daab1c40a9..774a4bce69 100644 --- a/testsuite/tests/polykinds/T7224.stderr +++ b/testsuite/tests/polykinds/T7224.stderr @@ -2,6 +2,12 @@ T7224.hs:6:19: error: • Expected kind ‘i’, but ‘i’ has kind ‘*’ • In the first argument of ‘m’, namely ‘i’ + In the type signature: ret' :: a -> m i i a + In the class declaration for ‘PMonad'’ + +T7224.hs:7:14: error: + • Expected kind ‘i’, but ‘i’ has kind ‘*’ + • In the first argument of ‘m’, namely ‘i’ In the type signature: - ret' :: a -> m i i a + bind' :: m i j a -> (a -> m j k b) -> m i k b In the class declaration for ‘PMonad'’ diff --git a/testsuite/tests/polykinds/T7278.stderr b/testsuite/tests/polykinds/T7278.stderr index 676be2cb0f..265e27892b 100644 --- a/testsuite/tests/polykinds/T7278.stderr +++ b/testsuite/tests/polykinds/T7278.stderr @@ -1,6 +1,5 @@ T7278.hs:9:43: error: - • Expecting two fewer arguments to ‘t’ - Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’ + • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’ • In the type signature: f :: (C (t :: k) (TF t)) => TF t p1 p0 -> t p1 p0 diff --git a/testsuite/tests/polykinds/T7332.hs b/testsuite/tests/polykinds/T7332.hs index 0d3e7e5a13..75a6cbc991 100644 --- a/testsuite/tests/polykinds/T7332.hs +++ b/testsuite/tests/polykinds/T7332.hs @@ -9,9 +9,10 @@ module T7332 where import GHC.Exts( IsString(..) ) import Data.Monoid +import Data.Semigroup newtype DC d = DC d - deriving (Show, Monoid) + deriving (Show, Semigroup, Monoid) instance IsString (DC String) where fromString = DC diff --git a/testsuite/tests/polykinds/T7404.stderr b/testsuite/tests/polykinds/T7404.stderr deleted file mode 100644 index a8b953e5df..0000000000 --- a/testsuite/tests/polykinds/T7404.stderr +++ /dev/null @@ -1,5 +0,0 @@ - -T7404.hs:4:32: error: - Type variable ‘x’ used in a kind. - Did you mean to use TypeInType? - the declaration for type family ‘Foo’ diff --git a/testsuite/tests/polykinds/T7433.stderr b/testsuite/tests/polykinds/T7433.stderr index 1cd2ad2f29..4dce12a653 100644 --- a/testsuite/tests/polykinds/T7433.stderr +++ b/testsuite/tests/polykinds/T7433.stderr @@ -1,6 +1,6 @@ -T7433.hs:2:10: - Data constructor ‘Z’ cannot be used here - (Perhaps you intended to use DataKinds) - In the type ‘ 'Z’ - In the type declaration for ‘T’ +T7433.hs:2:10: error: + • Data constructor ‘Z’ cannot be used here + (perhaps you intended to use DataKinds) + • In the type ‘ 'Z’ + In the type declaration for ‘T’ diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr index a198657754..6c4eec47f2 100644 --- a/testsuite/tests/polykinds/T7438.stderr +++ b/testsuite/tests/polykinds/T7438.stderr @@ -1,16 +1,16 @@ T7438.hs:6:14: error: • Couldn't match expected type ‘p1’ with actual type ‘p’ - ‘p1’ is untouchable + ‘p’ is untouchable inside the constraints: b ~ a bound by a pattern with constructor: Nil :: forall k (a :: k). Thrist a a, in an equation for ‘go’ at T7438.hs:6:4-6 - ‘p1’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16 ‘p’ is a rigid type variable bound by the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16 + ‘p1’ is a rigid type variable bound by + the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16 Possible fix: add a type signature for ‘go’ • In the expression: acc In an equation for ‘go’: go Nil acc = acc 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..5632e97707 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:12-16 ‘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/T8132.stderr b/testsuite/tests/polykinds/T8132.stderr index a1aaa1319a..f53a78cd6d 100644 --- a/testsuite/tests/polykinds/T8132.stderr +++ b/testsuite/tests/polykinds/T8132.stderr @@ -1,4 +1,4 @@ -T8132.hs:7:1: error: +T8132.hs:7:10: error: • Class ‘Typeable’ does not support user-specified instances • In the instance declaration for ‘Typeable K’ 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 1e7818c5ef..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 (r :: [*]) v (t :: v) (as :: [U *]). I ('AA t as) r, + 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/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr index 00c9c6328e..9aa4ab50d9 100644 --- a/testsuite/tests/polykinds/T8616.stderr +++ b/testsuite/tests/polykinds/T8616.stderr @@ -1,8 +1,14 @@ -T8616.hs:8:29: error: - • Expected a type, but ‘Any’ has kind ‘k’ - • In an expression type signature: (Any :: k) - In the expression: undefined :: (Any :: k) +T8616.hs:8:16: error: + • Couldn't match kind ‘k’ with ‘*’ + ‘k’ is a rigid type variable bound by + the type signature for: + withSomeSing :: forall k (kproxy :: k). Proxy kproxy + at T8616.hs:7:1-50 + When matching types + a0 :: * + Any :: k + • In the expression: undefined :: (Any :: k) In an equation for ‘withSomeSing’: withSomeSing = undefined :: (Any :: k) • Relevant bindings include 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/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr index 79a9a4617f..d9483c8490 100644 --- a/testsuite/tests/polykinds/T9017.stderr +++ b/testsuite/tests/polykinds/T9017.stderr @@ -1,12 +1,16 @@ T9017.hs:8:7: error: - • Couldn't match kind ‘k’ with ‘*’ - ‘k’ is a rigid type variable bound by + • Couldn't match kind ‘k1’ with ‘*’ + ‘k1’ is a rigid type variable bound by the type signature for: foo :: forall k k1 (a :: k -> k1 -> *) (b :: k) (m :: k -> k1). a b (m b) at T9017.hs:7:1-16 - When matching the kind of ‘a’ + When matching types + a1 :: * -> * -> * + a :: k -> k1 -> * + Expected type: a b (m b) + Actual type: a1 a0 (m0 a0) • In the expression: arr return In an equation for ‘foo’: foo = arr return • Relevant bindings include diff --git a/testsuite/tests/polykinds/T9200b.stderr b/testsuite/tests/polykinds/T9200b.stderr index 22f9df73f1..7c3cb65bd0 100644 --- a/testsuite/tests/polykinds/T9200b.stderr +++ b/testsuite/tests/polykinds/T9200b.stderr @@ -1,5 +1,5 @@ T9200b.hs:8:5: error: - Expected kind ‘k’, but ‘'True’ has kind ‘Bool’ - In the first argument of ‘F’, namely ‘True’ - In the type family declaration for ‘F’ + • Expected kind ‘k’, but ‘True’ has kind ‘Bool’ + • In the first argument of ‘F’, namely ‘True’ + In the type family declaration for ‘F’ 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 6e143e0cf9..94e0c16f95 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’: + bound by a type expected by the context: (a ~ '(b0, c0)) => Proxy b0 - at T9222.hs:13:3 + 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 + 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/T9574.stderr b/testsuite/tests/polykinds/T9574.stderr deleted file mode 100644 index 50b42ad590..0000000000 --- a/testsuite/tests/polykinds/T9574.stderr +++ /dev/null @@ -1,4 +0,0 @@ - -T9574.hs:11:5: - The RHS of an associated type declaration mentions ‘o’ - All such variables must be bound on the LHS diff --git a/testsuite/tests/polykinds/T9725.hs b/testsuite/tests/polykinds/T9725.hs new file mode 100644 index 0000000000..9a3d529d96 --- /dev/null +++ b/testsuite/tests/polykinds/T9725.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables #-} +module T9725 where + +data En = M Bool +class Kn (l :: En) + +instance Kn (M b) + +data Fac :: En -> * where + Mo :: Kn (M b) => Fac (M b) + +data Fm :: * -> * where + HiF :: Kn (ent b) => Fm (Fac (ent b)) -> Fm (O ent) + MoF :: Kn (M b) => Fm (Fac (M b)) + +data O :: (k -> En) -> * where + Hi :: Fac (ent k) -> O ent + +data Co :: (* -> *) -> * -> * where + Ab :: (t -> f t) -> Co f t + +-- Restricted kind signature: +--test :: forall (ent :: Bool -> En) . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) + +test :: forall ent . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) +test de = Ab h + where h :: O ent -> Fm (O ent) + h (Hi m@Mo) = HiF (d m) + d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i)) + d _ = de + +{- +9725.hs:27:25: + Could not deduce (Kn (ent k1)) arising from a use of ‘HiF’ + from the context (ent k1 ~ 'M b, Kn ('M b)) + bound by a pattern with constructor + Mo :: forall (b :: Bool). Kn ('M b) => Fac ('M b), + in an equation for ‘h’ + at 9725.hs:27:19-20 + In the expression: HiF (d m) + In an equation for ‘h’: h (Hi m@Mo) = HiF (d m) + In an equation for ‘test’: + test de + = Ab h + where + h :: O ent -> Fm (O ent) + h (Hi m@Mo) = HiF (d m) + d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i)) + d _ = de +Failed, modules loaded: none. +-} diff --git a/testsuite/tests/polykinds/SigTvKinds.hs b/testsuite/tests/polykinds/TyVarTvKinds.hs index 782a7b3f8b..a3a0de3da4 100644 --- a/testsuite/tests/polykinds/SigTvKinds.hs +++ b/testsuite/tests/polykinds/TyVarTvKinds.hs @@ -1,6 +1,6 @@ {-# LANGUAGE PolyKinds #-} -module SigTvKinds where +module TyVarTvKinds where data T (a :: k1) x = MkT (S a ()) data S (b :: k2) y = MkS (T b ()) diff --git a/testsuite/tests/polykinds/SigTvKinds2.hs b/testsuite/tests/polykinds/TyVarTvKinds2.hs index 1ec1ebb0f6..49817d7925 100644 --- a/testsuite/tests/polykinds/SigTvKinds2.hs +++ b/testsuite/tests/polykinds/TyVarTvKinds2.hs @@ -1,6 +1,6 @@ {-# LANGUAGE PolyKinds #-} -module SigTvKinds2 where +module TyVarTvKinds2 where data SameKind :: k -> k -> * diff --git a/testsuite/tests/polykinds/SigTvKinds2.stderr b/testsuite/tests/polykinds/TyVarTvKinds2.stderr index 9f523705a6..1a552883d2 100644 --- a/testsuite/tests/polykinds/SigTvKinds2.stderr +++ b/testsuite/tests/polykinds/TyVarTvKinds2.stderr @@ -1,5 +1,5 @@ -SigTvKinds2.hs:7:48: error: +TyVarTvKinds2.hs:7:48: error: • Expected kind ‘k1’, but ‘b’ has kind ‘k2’ • In the second argument of ‘SameKind’, namely ‘b’ In the type ‘SameKind a b’ diff --git a/testsuite/tests/polykinds/TyVarTvKinds3.hs b/testsuite/tests/polykinds/TyVarTvKinds3.hs new file mode 100644 index 0000000000..570078c863 --- /dev/null +++ b/testsuite/tests/polykinds/TyVarTvKinds3.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs, ExplicitForAll, PolyKinds #-} + +module TyVarTvKinds3 where + +import Data.Kind + +data SameKind :: k -> k -> Type +data Bad a where + MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b) diff --git a/testsuite/tests/polykinds/TyVarTvKinds3.stderr b/testsuite/tests/polykinds/TyVarTvKinds3.stderr new file mode 100644 index 0000000000..67da965d09 --- /dev/null +++ b/testsuite/tests/polykinds/TyVarTvKinds3.stderr @@ -0,0 +1,6 @@ + +TyVarTvKinds3.hs:9:62: error: + • Expected kind ‘k1’, but ‘b’ has kind ‘k2’ + • In the second argument of ‘SameKind’, namely ‘b’ + In the first argument of ‘Bad’, namely ‘(SameKind a b)’ + In the type ‘Bad (SameKind a b)’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 900faca994..ae4ee51a21 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -37,8 +37,8 @@ test('T6035', normal, compile, ['']) 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('T6039', normal, compile, ['']) +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,['']) @@ -103,10 +103,11 @@ test('T9263', normal, run_command, ['$MAKE -s --no-print-directory T9263']) test('T9063', normal, compile, ['']) test('T9200', normal, compile, ['']) test('T9200b', normal, compile_fail, ['']) +test('T9725', normal, compile, ['']) test('T9750', normal, compile, ['']) test('T9569', normal, compile, ['']) test('T9838', normal, multimod_compile, ['T9838.hs','-v0']) -test('T9574', normal, compile_fail, ['']) +test('T9574', normal, compile, ['']) test('T9833', normal, compile, ['']) test('T7908', normal, compile, ['']) test('PolyInstances', normal, compile, ['']) @@ -121,8 +122,8 @@ test('T10134', normal, multimod_compile, ['T10134.hs','-v0']) test('T10742', normal, compile, ['']) test('T10934', normal, compile, ['']) test('T11142', normal, compile_fail, ['']) -test('SigTvKinds', normal, compile, ['']) -test('SigTvKinds2', expect_broken(11203), compile_fail, ['']) +test('TyVarTvKinds', normal, compile, ['']) +test('TyVarTvKinds2', expect_broken(11203), compile_fail, ['']) test('T9017', normal, compile_fail, ['']) test('TidyClassKinds', normal, compile_fail, ['-fprint-explicit-kinds']) test('T11249', normal, compile, ['']) @@ -142,10 +143,10 @@ test('T11399', normal, compile_fail, ['']) test('T11611', normal, compile_fail, ['']) test('T11616', normal, compile, ['']) test('T11648', normal, compile, ['']) -test('T11648b', normal, compile_fail, ['']) +test('T11648b', normal, compile, ['']) test('KindVType', normal, compile_fail, ['']) test('T11821', normal, compile, ['']) -test('T11821a', normal, compile, ['']) +test('T11821a', normal, compile_fail, ['']) test('T11640', normal, compile, ['']) test('T11554', normal, compile_fail, ['']) test('T12055', normal, compile, ['']) @@ -160,6 +161,35 @@ test('T13394a', normal, compile, ['']) test('T13394', normal, compile, ['']) test('T13371', normal, compile, ['']) test('T13393', normal, compile_fail, ['']) -test('T13555', normal, compile_fail, ['']) +test('T13555', normal, compile, ['']) test('T13659', normal, compile_fail, ['']) test('T13625', normal, compile_fail, ['']) +test('T13985', normal, compile_fail, ['']) +test('T14110', normal, compile_fail, ['']) +test('BadKindVar', normal, compile_fail, ['']) +test('T13738', normal, compile_fail, ['']) +test('T14209', normal, compile, ['']) +test('T14265', normal, compile_fail, ['']) +test('T13391a', normal, compile, ['']) +test('T14270', normal, compile, ['']) +test('T14450', normal, compile_fail, ['']) +test('T14172', normal, multimod_compile_fail, ['T14172.hs','-v0']) +test('T14174', normal, compile_fail, ['']) +test('T14174a', normal, compile, ['']) +test('T14520', normal, compile_fail, ['-fprint-explicit-kinds']) +test('T11203', normal, compile_fail, ['']) +test('T14555', normal, compile_fail, ['-fprint-explicit-runtime-reps']) +test('T14563', normal, compile_fail, ['-fprint-explicit-runtime-reps']) +test('T14561', normal, compile_fail, ['']) +test('T14580', normal, compile_fail, ['']) +test('T14515', normal, compile, ['']) +test('T14710', normal, compile_fail, ['']) +test('T14723', normal, compile, ['']) +test('T14846', normal, compile_fail, ['']) +test('T14873', normal, compile, ['']) +test('TyVarTvKinds3', normal, compile_fail, ['']) +test('T15116', normal, compile_fail, ['']) +test('T15116a', normal, compile_fail, ['']) +test('T15170', normal, compile, ['']) +test('T14939', normal, compile, ['-O']) +test('T15577', normal, compile_fail, ['-O']) |