summaryrefslogtreecommitdiff
path: root/testsuite/tests/polykinds
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/polykinds')
-rw-r--r--testsuite/tests/polykinds/T11203.stderr2
-rw-r--r--testsuite/tests/polykinds/T11821a.stderr2
-rw-r--r--testsuite/tests/polykinds/T12593.stderr8
-rw-r--r--testsuite/tests/polykinds/T13985.hs1
-rw-r--r--testsuite/tests/polykinds/T13985.stderr41
-rw-r--r--testsuite/tests/polykinds/T14450.stderr11
-rw-r--r--testsuite/tests/polykinds/T14846.stderr36
-rw-r--r--testsuite/tests/polykinds/T14887a.hs16
-rw-r--r--testsuite/tests/polykinds/T14887a.stderr1
-rw-r--r--testsuite/tests/polykinds/T15592.stderr2
-rw-r--r--testsuite/tests/polykinds/T15592b.stderr4
-rw-r--r--testsuite/tests/polykinds/T15789.hs10
-rw-r--r--testsuite/tests/polykinds/T15789.stderr6
-rw-r--r--testsuite/tests/polykinds/T15804.hs5
-rw-r--r--testsuite/tests/polykinds/T15804.stderr4
-rw-r--r--testsuite/tests/polykinds/T15817.hs10
-rw-r--r--testsuite/tests/polykinds/T15874.hs18
-rw-r--r--testsuite/tests/polykinds/T15881.hs8
-rw-r--r--testsuite/tests/polykinds/T15881.stderr5
-rw-r--r--testsuite/tests/polykinds/T15881a.hs8
-rw-r--r--testsuite/tests/polykinds/T15881a.stderr4
-rw-r--r--testsuite/tests/polykinds/T8616.stderr9
-rw-r--r--testsuite/tests/polykinds/all.T7
23 files changed, 162 insertions, 56 deletions
diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr
index 5d62e00304..f5c72133ae 100644
--- a/testsuite/tests/polykinds/T11203.stderr
+++ b/testsuite/tests/polykinds/T11203.stderr
@@ -1,4 +1,4 @@
T11203.hs:7:24: error:
• Couldn't match ‘k1’ with ‘k2’
- • In the data declaration for ‘Q’
+ • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr
index 2e443e637b..f55c703524 100644
--- a/testsuite/tests/polykinds/T11821a.stderr
+++ b/testsuite/tests/polykinds/T11821a.stderr
@@ -1,4 +1,4 @@
T11821a.hs:4:31: error:
• Couldn't match ‘k1’ with ‘k2’
- • In the type declaration for ‘SameKind’
+ • In the type synonym declaration for ‘SameKind’
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 27123a8bc8..e150299ea1 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -92,8 +92,8 @@ T12593.hs:14:6: error:
• 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
+ run :: Free k k4 k8 p a b
+ -> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
(bound at T12593.hs:14:1)
T12593.hs:14:18: error:
@@ -111,6 +111,6 @@ T12593.hs:14:18: error:
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
+ run :: Free k k4 k8 p a b
+ -> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
(bound at T12593.hs:14:1)
diff --git a/testsuite/tests/polykinds/T13985.hs b/testsuite/tests/polykinds/T13985.hs
index c0555d8f69..6a844b366e 100644
--- a/testsuite/tests/polykinds/T13985.hs
+++ b/testsuite/tests/polykinds/T13985.hs
@@ -1,5 +1,6 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr
index f60314a443..2df92c34da 100644
--- a/testsuite/tests/polykinds/T13985.stderr
+++ b/testsuite/tests/polykinds/T13985.stderr
@@ -1,39 +1,28 @@
-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?
+T13985.hs:13:41: error:
+ • Type variable ‘k’ is mentioned in the RHS,
+ but not bound on the LHS of the family instance
• 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?
+T13985.hs:16:43: error:
+ • Type variable ‘a’ is mentioned in the RHS,
+ but not bound on the LHS of the family instance
• 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?
+T13985.hs:23:26: error:
+ • Type variable ‘k’ is mentioned in the RHS,
+ but not bound on the LHS of the family instance
• 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?
+T13985.hs:24:37: error:
+ • Type variable ‘a’ is mentioned in the RHS,
+ but not bound on the LHS of the family instance
• 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)
+T13985.hs:28:39: error:
+ • Type variable ‘x’ is mentioned in the RHS,
+ but not bound on the LHS of the family instance
• In the default type instance declaration for ‘ZT’
In the class declaration for ‘Z’
diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr
index 8a987b7a56..107f4aa2ce 100644
--- a/testsuite/tests/polykinds/T14450.stderr
+++ b/testsuite/tests/polykinds/T14450.stderr
@@ -1,8 +1,7 @@
-T14450.hs:33:13: 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’
+T14450.hs:33:3: error:
+ • Type indexes must match class instance head
+ Expected: Dom @k @k (IddSym0 @k)
+ Actual: Dom @* @* (IddSym0 @*) -- Defined at T14450.hs:33:8
+ • In the type instance declaration for ‘Dom’
In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 062dc49e1f..43d81c5e1e 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -3,12 +3,8 @@ 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 k6 (cls2 :: k6
- -> Constraint) (xx :: k5) (a :: Struct cls2) (ríki :: Struct
- cls2
- -> Struct
- cls2
- -> *).
+ i :: forall k5 k6 (cls2 :: k6 -> Constraint) (xx :: k5)
+ (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *).
StructI xx a =>
ríki a a
at T14846.hs:38:8-48
@@ -16,21 +12,31 @@ T14846.hs:38:8: error:
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 k2 (cls :: k2
- -> Constraint) (xx :: k1) (a :: Struct cls).
+ Instance sig: forall k1 k2 (cls :: k2 -> Constraint) (xx :: k1)
+ (a :: Struct cls).
StructI xx a =>
Hom riki a a
- Class sig: forall k1 k2 (cls :: k2
- -> Constraint) (xx :: k1) (a :: Struct
- cls) (ríki :: Struct
- cls
- -> Struct
- cls
- -> *).
+ Class sig: forall k1 k2 (cls :: k2 -> Constraint) (xx :: k1)
+ (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:12: error:
+ • Couldn't match kind ‘k3’ with ‘Struct cls2’
+ ‘k3’ is a rigid type variable bound by
+ the instance declaration
+ at T14846.hs:37:10-65
+ When matching kinds
+ cls0 :: Struct cls -> Constraint
+ cls1 :: k3 -> Constraint
+ • In the expression: struct :: AStruct (Structured a cls)
+ In the expression: case struct :: AStruct (Structured a cls) of
+ In an equation for ‘i’:
+ i = case struct :: AStruct (Structured a cls) of
+ • Relevant bindings include
+ i :: Hom riki a a (bound at T14846.hs:39:3)
+
T14846.hs:39:31: error:
• Couldn't match kind ‘k3’ with ‘Struct cls2’
‘k3’ is a rigid type variable bound by
diff --git a/testsuite/tests/polykinds/T14887a.hs b/testsuite/tests/polykinds/T14887a.hs
new file mode 100644
index 0000000000..2e5cf02212
--- /dev/null
+++ b/testsuite/tests/polykinds/T14887a.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-implicit-kind-vars #-}
+module Bug where
+
+import Data.Proxy
+
+f1 :: forall (x :: a). Proxy (x :: _)
+-- This one has an implicitly-quantified kind var 'a', which
+-- we will stop accepting in the future, under the forall-or-nothing
+-- rule. Hence -Wno-implicit-kind-vars
+f1 = Proxy
+
+f2 :: forall a (x :: a). Proxy (x :: _)
+f2 = Proxy
diff --git a/testsuite/tests/polykinds/T14887a.stderr b/testsuite/tests/polykinds/T14887a.stderr
new file mode 100644
index 0000000000..0519ecba6e
--- /dev/null
+++ b/testsuite/tests/polykinds/T14887a.stderr
@@ -0,0 +1 @@
+ \ No newline at end of file
diff --git a/testsuite/tests/polykinds/T15592.stderr b/testsuite/tests/polykinds/T15592.stderr
index c1b823e738..4086c12bf6 100644
--- a/testsuite/tests/polykinds/T15592.stderr
+++ b/testsuite/tests/polykinds/T15592.stderr
@@ -1,6 +1,6 @@
TYPE CONSTRUCTORS
type role T nominal nominal representational nominal nominal
- T :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> *
+ T{5} :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> *
DATA CONSTRUCTORS
MkT :: forall {k} k1 (f :: k1 -> k -> *) (a :: k1) (b :: k).
f a b -> T f a b -> T f a b
diff --git a/testsuite/tests/polykinds/T15592b.stderr b/testsuite/tests/polykinds/T15592b.stderr
index c51416f4c5..d07b3a1ac7 100644
--- a/testsuite/tests/polykinds/T15592b.stderr
+++ b/testsuite/tests/polykinds/T15592b.stderr
@@ -1,7 +1,7 @@
TYPE CONSTRUCTORS
- C :: forall {k}. k -> Constraint
+ C{2} :: forall {k}. k -> Constraint
type role T nominal nominal nominal nominal
- T :: forall {k} (a :: k) (f :: k -> *). f a -> *
+ T{4} :: forall k (f :: k -> *) (a :: k). f a -> *
Dependent modules: []
Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/polykinds/T15789.hs b/testsuite/tests/polykinds/T15789.hs
new file mode 100644
index 0000000000..6465da2a9b
--- /dev/null
+++ b/testsuite/tests/polykinds/T15789.hs
@@ -0,0 +1,10 @@
+{-# Language LiberalTypeSynonyms #-}
+{-# Language PolyKinds #-}
+{-# Language RankNTypes #-}
+{-# Language DataKinds #-}
+
+import Data.Kind
+
+type Cat ob = ob -> ob -> Type
+
+data Zero :: forall (cat :: forall xx. xx -> Type) a. forall b. Cat (forall b. cat b u)
diff --git a/testsuite/tests/polykinds/T15789.stderr b/testsuite/tests/polykinds/T15789.stderr
new file mode 100644
index 0000000000..c0fd4eab34
--- /dev/null
+++ b/testsuite/tests/polykinds/T15789.stderr
@@ -0,0 +1,6 @@
+
+T15789.hs:10:80: error:
+ • Expected kind ‘k2 -> *’, but ‘cat b’ has kind ‘*’
+ • In the first argument of ‘Cat’, namely ‘(forall b. cat b u)’
+ In the kind ‘forall (cat :: forall xx. xx -> Type) a.
+ forall b. Cat (forall b. cat b u)’
diff --git a/testsuite/tests/polykinds/T15804.hs b/testsuite/tests/polykinds/T15804.hs
new file mode 100644
index 0000000000..be5fa165a3
--- /dev/null
+++ b/testsuite/tests/polykinds/T15804.hs
@@ -0,0 +1,5 @@
+{-# Language PolyKinds #-}
+
+module T15804 where
+
+data T :: (a :: k) -> *
diff --git a/testsuite/tests/polykinds/T15804.stderr b/testsuite/tests/polykinds/T15804.stderr
new file mode 100644
index 0000000000..52262b675f
--- /dev/null
+++ b/testsuite/tests/polykinds/T15804.stderr
@@ -0,0 +1,4 @@
+
+T15804.hs:5:12: error:
+ • Expected a type, but ‘a :: k’ has kind ‘k’
+ • In the kind ‘(a :: k) -> *’
diff --git a/testsuite/tests/polykinds/T15817.hs b/testsuite/tests/polykinds/T15817.hs
new file mode 100644
index 0000000000..a5f3eb78db
--- /dev/null
+++ b/testsuite/tests/polykinds/T15817.hs
@@ -0,0 +1,10 @@
+{-# Language RankNTypes #-}
+{-# Language PolyKinds #-}
+{-# Language TypeFamilies #-}
+
+module T15817 where
+
+import Data.Kind
+
+data family X :: forall (a :: Type). Type
+data instance X = MkX
diff --git a/testsuite/tests/polykinds/T15874.hs b/testsuite/tests/polykinds/T15874.hs
new file mode 100644
index 0000000000..fd560db095
--- /dev/null
+++ b/testsuite/tests/polykinds/T15874.hs
@@ -0,0 +1,18 @@
+{-# Language RankNTypes #-}
+{-# Language DataKinds #-}
+{-# Language PolyKinds #-}
+{-# Language GADTs #-}
+{-# Language TypeFamilies #-}
+
+module T15874 where
+
+import Data.Kind
+
+data Var where
+ Op :: Var
+ Id :: Var
+
+type Varianced = (forall (var :: Var). Type)
+
+data family Parser :: Varianced
+data instance Parser = P
diff --git a/testsuite/tests/polykinds/T15881.hs b/testsuite/tests/polykinds/T15881.hs
new file mode 100644
index 0000000000..a49b7fd436
--- /dev/null
+++ b/testsuite/tests/polykinds/T15881.hs
@@ -0,0 +1,8 @@
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+
+module T15881 where
+
+import Data.Kind
+
+data A n (a :: n n) :: Type
diff --git a/testsuite/tests/polykinds/T15881.stderr b/testsuite/tests/polykinds/T15881.stderr
new file mode 100644
index 0000000000..4fde71dab7
--- /dev/null
+++ b/testsuite/tests/polykinds/T15881.stderr
@@ -0,0 +1,5 @@
+
+T15881.hs:8:18: error:
+ • Occurs check: cannot construct the infinite kind: k0 ~ k0 -> *
+ • In the first argument of ‘n’, namely ‘n’
+ In the kind ‘n n’
diff --git a/testsuite/tests/polykinds/T15881a.hs b/testsuite/tests/polykinds/T15881a.hs
new file mode 100644
index 0000000000..a29c63f706
--- /dev/null
+++ b/testsuite/tests/polykinds/T15881a.hs
@@ -0,0 +1,8 @@
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+
+module T15881a where
+
+import Data.Kind
+
+data A n (a :: n) :: a -> Type
diff --git a/testsuite/tests/polykinds/T15881a.stderr b/testsuite/tests/polykinds/T15881a.stderr
new file mode 100644
index 0000000000..84014c7abc
--- /dev/null
+++ b/testsuite/tests/polykinds/T15881a.stderr
@@ -0,0 +1,4 @@
+
+T15881a.hs:8:22: error:
+ • Expected a type, but ‘a’ has kind ‘n’
+ • In the kind ‘a -> Type’
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 9aa4ab50d9..f9e5132a34 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -13,3 +13,12 @@ T8616.hs:8:16: error:
withSomeSing = undefined :: (Any :: k)
• Relevant bindings include
withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1)
+
+T8616.hs:8:30: error:
+ • Expected a type, but ‘Any :: k’ has kind ‘k’
+ • In an expression type signature: (Any :: k)
+ In the expression: undefined :: (Any :: k)
+ In an equation for ‘withSomeSing’:
+ withSomeSing = undefined :: (Any :: k)
+ • Relevant bindings include
+ withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1)
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 6ffb3181ce..8be2c59bf0 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -196,3 +196,10 @@ test('T15577', normal, compile_fail, ['-O'])
test('T15592', normal, compile, [''])
test('T15592b', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
test('T15787', normal, compile_fail, [''])
+test('T15789', normal, compile_fail, [''])
+test('T15804', normal, compile_fail, [''])
+test('T15881', normal, compile_fail, [''])
+test('T15881a', normal, compile_fail, [''])
+test('T15817', normal, compile, [''])
+test('T15874', normal, compile, [''])
+test('T14887a', normal, compile, [''])