diff options
Diffstat (limited to 'testsuite/tests')
106 files changed, 615 insertions, 322 deletions
diff --git a/testsuite/tests/dependent/should_compile/T15743.stderr b/testsuite/tests/dependent/should_compile/T15743.stderr index 7162a877a2..f44c430d8d 100644 --- a/testsuite/tests/dependent/should_compile/T15743.stderr +++ b/testsuite/tests/dependent/should_compile/T15743.stderr @@ -1,6 +1,6 @@ TYPE CONSTRUCTORS type role T nominal nominal nominal phantom phantom phantom - T :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> * + T{6} :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> * 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/dependent/should_compile/T15743e.stderr b/testsuite/tests/dependent/should_compile/T15743e.stderr index c77bf3849c..f96da68a7f 100644 --- a/testsuite/tests/dependent/should_compile/T15743e.stderr +++ b/testsuite/tests/dependent/should_compile/T15743e.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS type role T nominal nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal phantom - T :: + T{14} :: forall {k1} {k2} {k3} (k4 :: k2) k5. forall k6 -> k6 -> Proxy k4 @@ -10,13 +10,13 @@ TYPE CONSTRUCTORS -> forall (k7 :: k1). Proxy k7 -> forall (k8 :: k5). Proxy k8 -> * type role T2 nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal nominal phantom - T2 :: - forall {k1} {k2} (k3 :: k1) k7. forall k4 -> + T2{14} :: + forall {k1} {k2} (k3 :: k2) k7. forall k4 -> k4 -> Proxy k3 -> (k7 -> *) -> k7 - -> forall (k5 :: k2). + -> forall (k5 :: k1). Proxy k5 -> forall k6 (k8 :: k6). Proxy k8 -> * DATA CONSTRUCTORS MkT2 :: forall {k7} {k1} {k2 :: k1} {k3} {k4 :: k3} {k5} {k6 :: k5} diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr index 5fa8efd502..078d7377da 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr @@ -1,6 +1,7 @@ BadTelescope.hs:9:1: error: - • These kind and type variables: a k (b :: k) (c :: SameKind a b) - are out of dependency order. Perhaps try this ordering: - k (a :: k) (b :: k) (c :: SameKind a b) + • The kind of ‘X’ is ill-scoped + Inferred kind: X :: forall (a :: k) k (b :: k) -> SameKind a b -> * + Perhaps try this order instead: + k (a :: k) (b :: k) (c :: SameKind a b) • In the data type declaration for ‘X’ diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr index 1137f28c4d..c36ad07c42 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr @@ -1,6 +1,6 @@ BadTelescope3.hs:9:1: error: - • These kind and type variables: a k (b :: k) - are out of dependency order. Perhaps try this ordering: - k (a :: k) (b :: k) + • The kind of ‘S’ is ill-scoped + Inferred kind: S :: k -> forall k -> k -> * + Perhaps try this order instead: k (a :: k) (b :: k) • In the type synonym declaration for ‘S’ diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr index f7c281e983..039389bed0 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr @@ -1,15 +1,16 @@ BadTelescope4.hs:9:1: error: - • These kind and type variables: a - (c :: Proxy b) - (d :: Proxy a) - (x :: SameKind b d) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘Bad’ is ill-scoped + Inferred kind: Bad :: forall k (b :: Proxy a). forall (a :: k) -> + Proxy b -> forall (d :: Proxy a) -> SameKind b d -> * + NB: Inferred variables + (namely: k) always come first + then Specified variables (namely: (b :: Proxy a)) + Perhaps try this order instead: k (a :: k) (b :: Proxy a) (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘Bad’ diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr index 3ced11a79d..adfebdd113 100644 --- a/testsuite/tests/dependent/should_fail/T13895.stderr +++ b/testsuite/tests/dependent/should_fail/T13895.stderr @@ -1,38 +1,7 @@ -T13895.hs:8:14: error: - • Could not deduce (Typeable (t dict)) - from the context: (Data a, Typeable (t dict)) - bound by the type signature for: - dataCast1 :: forall k1 a (c :: * -> *) (t :: forall k2. - Typeable k2 => - k2 -> *). - (Data a, Typeable (t dict)) => - (forall d. Data d => c (t dict1 d)) -> Maybe (c a) - at T13895.hs:(8,14)-(14,24) - The type variable ‘k0’ is ambiguous - • In the ambiguity check for ‘dataCast1’ - To defer the ambiguity check to use sites, enable AllowAmbiguousTypes - In the type signature: - dataCast1 :: forall (a :: Type). - Data a => - forall (c :: Type -> Type) - (t :: forall (k :: Type). Typeable k => k -> Type). - Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) - -T13895.hs:12:23: error: - • Illegal constraint in a kind: Typeable k0 - • In the first argument of ‘Typeable’, namely ‘t’ - In the type signature: - dataCast1 :: forall (a :: Type). - Data a => - forall (c :: Type -> Type) - (t :: forall (k :: Type). Typeable k => k -> Type). - Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) - -T13895.hs:13:38: error: - • Illegal constraint in a kind: Typeable k0 - • In the first argument of ‘c’, namely ‘(t d)’ - In the type signature: +T13895.hs:10:14: error: + • Illegal constraint in a kind: forall k. Typeable k => k -> * + • In the type signature: dataCast1 :: forall (a :: Type). Data a => forall (c :: Type -> Type) diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr index 44c4ed293c..10aa1b9da4 100644 --- a/testsuite/tests/dependent/should_fail/T14066f.stderr +++ b/testsuite/tests/dependent/should_fail/T14066f.stderr @@ -1,6 +1,6 @@ T14066f.hs:8:1: error: - • These kind and type variables: a k - are out of dependency order. Perhaps try this ordering: - k (a :: k) + • The kind of ‘P’ is ill-scoped + Inferred kind: P :: k -> forall k -> * + Perhaps try this order instead: k (a :: k) • In the type synonym declaration for ‘P’ diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr index 22ca786343..23f0a4c9d0 100644 --- a/testsuite/tests/dependent/should_fail/T14066g.stderr +++ b/testsuite/tests/dependent/should_fail/T14066g.stderr @@ -1,7 +1,9 @@ T14066g.hs:9:1: error: - • These kind and type variables: a (b :: a) (d :: SameKind c b) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘Q’ is ill-scoped + Inferred kind: Q :: forall (c :: a). forall a (b :: a) -> + SameKind c b -> * + NB: Specified variables (namely: (c :: a)) always come first + Perhaps try this order instead: a (c :: a) (b :: a) (d :: SameKind c b) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘Q’ diff --git a/testsuite/tests/dependent/should_fail/T15591b.stderr b/testsuite/tests/dependent/should_fail/T15591b.stderr index 838ee51c8f..91d9a948f4 100644 --- a/testsuite/tests/dependent/should_fail/T15591b.stderr +++ b/testsuite/tests/dependent/should_fail/T15591b.stderr @@ -1,7 +1,8 @@ T15591b.hs:9:3: error: - • These kind and type variables: a c - are out of dependency order. Perhaps try this ordering: - a (b :: Proxy a) (c :: Proxy b) - NB: Implicitly declared variables come before others. + • The kind of ‘T4’ is ill-scoped + Inferred kind: T4 :: forall (b :: Proxy a). forall a -> + Proxy b -> * + NB: Inferred variables (namely: (b :: Proxy a)) always come first + Perhaps try this order instead: a (b :: Proxy a) (c :: Proxy b) • In the associated type family declaration for ‘T4’ diff --git a/testsuite/tests/dependent/should_fail/T15591c.stderr b/testsuite/tests/dependent/should_fail/T15591c.stderr index 2f2b47fc8d..ecaa66048c 100644 --- a/testsuite/tests/dependent/should_fail/T15591c.stderr +++ b/testsuite/tests/dependent/should_fail/T15591c.stderr @@ -1,7 +1,8 @@ T15591c.hs:9:3: error: - • These kind and type variables: c a - are out of dependency order. Perhaps try this ordering: - a (b :: Proxy a) (c :: Proxy b) - NB: Implicitly declared variables come before others. + • The kind of ‘T5’ is ill-scoped + Inferred kind: T5 :: forall (b :: Proxy a). + Proxy b -> forall a -> * + NB: Inferred variables (namely: (b :: Proxy a)) always come first + Perhaps try this order instead: a (b :: Proxy a) (c :: Proxy b) • In the associated type family declaration for ‘T5’ diff --git a/testsuite/tests/dependent/should_fail/T15743c.stderr b/testsuite/tests/dependent/should_fail/T15743c.stderr index 9d28b68998..8e3ad5077f 100644 --- a/testsuite/tests/dependent/should_fail/T15743c.stderr +++ b/testsuite/tests/dependent/should_fail/T15743c.stderr @@ -1,16 +1,15 @@ T15743c.hs:10:1: error: - • These kind and type variables: k - (c :: k) - (a :: Proxy c) - b - (x :: SimilarKind a b) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘T’ is ill-scoped + Inferred kind: T :: forall (d :: k). + forall k (c :: k) (a :: Proxy c) (b :: Proxy d) -> + SimilarKind a b -> * + NB: Inferred variables (namely: (d :: k)) always come first + Perhaps try this order instead: k (d :: k) (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘T’ diff --git a/testsuite/tests/dependent/should_fail/T15743d.stderr b/testsuite/tests/dependent/should_fail/T15743d.stderr index d982d16980..51d1fad66f 100644 --- a/testsuite/tests/dependent/should_fail/T15743d.stderr +++ b/testsuite/tests/dependent/should_fail/T15743d.stderr @@ -1,16 +1,15 @@ T15743d.hs:10:1: error: - • These kind and type variables: k - (c :: k) - (a :: Proxy c) - (b :: Proxy d) - (x :: SimilarKind a b) - are out of dependency order. Perhaps try this ordering: + • The kind of ‘T2’ is ill-scoped + Inferred kind: T2 :: forall (d :: k). + forall k (c :: k) (a :: Proxy c) (b :: Proxy d) -> + SimilarKind a b -> * + NB: Specified variables (namely: (d :: k)) always come first + Perhaps try this order instead: k (d :: k) (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) - NB: Implicitly declared variables come before others. • In the data type declaration for ‘T2’ diff --git a/testsuite/tests/ghci/scripts/T10059.stdout b/testsuite/tests/ghci/scripts/T10059.stdout index 92fbb45ef7..955c95a966 100644 --- a/testsuite/tests/ghci/scripts/T10059.stdout +++ b/testsuite/tests/ghci/scripts/T10059.stdout @@ -1,4 +1,4 @@ -class (a ~ b) => (~) (a :: k0) (b :: k0) -- Defined in ‘GHC.Types’ -(~) :: k0 -> k0 -> Constraint -class (a GHC.Prim.~# b) => (~) (a :: k0) (b :: k0) +class (a ~ b) => (~) (a :: k) (b :: k) -- Defined in ‘GHC.Types’ +(~) :: k -> k -> Constraint +class (a GHC.Prim.~# b) => (~) (a :: k) (b :: k) -- Defined in ‘GHC.Types’ diff --git a/testsuite/tests/ghci/scripts/T15591.hs b/testsuite/tests/ghci/scripts/T15591.hs index f333fe0194..a27f8f0269 100644 --- a/testsuite/tests/ghci/scripts/T15591.hs +++ b/testsuite/tests/ghci/scripts/T15591.hs @@ -13,11 +13,15 @@ class C (a :: Type) where type T2 (x :: f a) class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where - type T3 (x :: Proxy '(a, c)) + type T3 (x :: Proxy '(a, (c :: Proxy b))) + -- NB: we have to put (c :: Proxy b) so that 'b' is Specified + -- in the kind of T3; else 'b' is Inferred and comes + -- first, which is ill-scoped -- no CUSK class C3 (a :: Type) (b :: Proxy a) (c :: Proxy b) d where - type T4 (x :: Proxy '(a, c)) + type T4 (x :: Proxy '(a, (c :: Proxy b))) + -- Ditto to T3 class C4 (a :: Type) b where type T5 (x :: f a) diff --git a/testsuite/tests/ghci/scripts/T15591.stdout b/testsuite/tests/ghci/scripts/T15591.stdout index b4673d5174..b0d4f8b34d 100644 --- a/testsuite/tests/ghci/scripts/T15591.stdout +++ b/testsuite/tests/ghci/scripts/T15591.stdout @@ -1,6 +1,6 @@ T1 :: forall (f :: * -> *) a. f a -> * -T2 :: forall a (f :: * -> *). f a -> * +T2 :: forall (f :: * -> *) a. f a -> * T3 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> * T4 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> * -T5 :: forall a (f :: * -> *). f a -> * -T6 :: forall {k} (a :: k) (f :: k -> *). f a -> * +T5 :: forall (f :: * -> *) a. f a -> * +T6 :: forall {k} (f :: k -> *) (a :: k). f a -> * diff --git a/testsuite/tests/ghci/scripts/T15743b.stdout b/testsuite/tests/ghci/scripts/T15743b.stdout index 03e593e5bd..2850a685fc 100644 --- a/testsuite/tests/ghci/scripts/T15743b.stdout +++ b/testsuite/tests/ghci/scripts/T15743b.stdout @@ -1 +1 @@ -F :: forall k k2. k -> k2 -> * +F :: forall {k} k2. k -> k2 -> * diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr index 15e19cf105..c6698d2944 100644 --- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr +++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr @@ -39,9 +39,9 @@ <interactive>:55:41: error: Type family equation violates injectivity annotation. - Kind variable ‘k2’ cannot be inferred from the right-hand side. + Kind variable ‘k1’ cannot be inferred from the right-hand side. In the type family equation: - PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1 + PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2 -- Defined at <interactive>:55:41 <interactive>:60:15: error: diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr index 731a216a1a..b4759714c2 100644 --- a/testsuite/tests/ghci/scripts/T7873.stderr +++ b/testsuite/tests/ghci/scripts/T7873.stderr @@ -5,4 +5,4 @@ of its type variables. Perhaps you meant to bind it explicitly somewhere? Type variables with inferred kinds: (k :: *) - • In the data declaration for ‘D1’ + • In the data type declaration for ‘D1’ diff --git a/testsuite/tests/ghci/scripts/ghci059.stdout b/testsuite/tests/ghci/scripts/ghci059.stdout index 9e9adb9ff1..7e734f1ccc 100644 --- a/testsuite/tests/ghci/scripts/ghci059.stdout +++ b/testsuite/tests/ghci/scripts/ghci059.stdout @@ -4,6 +4,6 @@ It is not a class. Please see section 9.14.4 of the user's guide for details. -} type role Coercible representational representational -class Coercible a b => Coercible (a :: k0) (b :: k0) +class Coercible a b => Coercible (a :: k) (b :: k) -- Defined in ‘GHC.Types’ coerce :: Coercible a b => a -> b -- Defined in ‘GHC.Prim’ diff --git a/testsuite/tests/indexed-types/should_compile/T15711.stderr b/testsuite/tests/indexed-types/should_compile/T15711.stderr index 1d23612cfc..2a012489e7 100644 --- a/testsuite/tests/indexed-types/should_compile/T15711.stderr +++ b/testsuite/tests/indexed-types/should_compile/T15711.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS - C :: * -> Constraint + C{1} :: * -> Constraint type role F nominal nominal - F :: forall a. Maybe a -> * + F{2} :: forall a. Maybe 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/indexed-types/should_compile/T15740a.hs b/testsuite/tests/indexed-types/should_compile/T15740a.hs new file mode 100644 index 0000000000..2d79a99878 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15740a.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-} + +module T15740a where + +import Data.Kind +import Data.Proxy + +type family F2 :: forall k. k -> Type + +-- This should succeed +type instance F2 = Proxy + diff --git a/testsuite/tests/indexed-types/should_compile/T15764a.hs b/testsuite/tests/indexed-types/should_compile/T15764a.hs new file mode 100644 index 0000000000..91d348bd96 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T15764a.hs @@ -0,0 +1,14 @@ +{-# Language PolyKinds #-} +{-# Language TypeFamilies #-} +{-# Language KindSignatures #-} +{-# Language DataKinds #-} +{-# Language MultiParamTypeClasses #-} + +module T15764a where + +import Data.Kind +import Data.Proxy +import GHC.TypeLits + +class C6 (k :: Type) (a :: k) (b :: Proxy (a :: k)) where + type T6 (proxy :: Proxy '(k, (b :: Proxy a))) diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr index bc5fd2a72e..6908d000ab 100644 --- a/testsuite/tests/indexed-types/should_compile/T15852.stderr +++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr @@ -1,13 +1,14 @@ TYPE CONSTRUCTORS type role DF nominal nominal nominal - DF :: forall k. * -> k -> * + DF{3} :: forall k. * -> k -> * COERCION AXIOMS axiom T15852.D:R:DFProxyProxy0 :: - forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j). - DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 c j a - -- Defined at T15852.hs:10:15 + forall k1 k2 (j :: k1) (c :: k2). + DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c FAMILY INSTANCES - data instance DF (Proxy c) c j a + data instance forall k1 k2 (j :: k1) (c :: k2). + DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c + -- Defined at T15852.hs:10:15 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/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr index 3b4361a2a5..9cf31965a4 100644 --- a/testsuite/tests/indexed-types/should_compile/T3017.stderr +++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr @@ -5,19 +5,18 @@ TYPE SIGNATURES test2 :: forall c a b. (Coll c, Num a, Num b, Elem c ~ (a, b)) => c -> c TYPE CONSTRUCTORS - Coll :: * -> Constraint + Coll{1} :: * -> Constraint type role Elem nominal - Elem :: * -> * - ListColl :: * -> * + Elem{1} :: * -> * + ListColl{1} :: * -> * COERCION AXIOMS - axiom Foo.D:R:ElemListColl :: - Elem (ListColl a) = a -- Defined at T3017.hs:13:9 + axiom Foo.D:R:ElemListColl :: Elem (ListColl a) = a DATA CONSTRUCTORS L :: forall a. [a] -> ListColl a CLASS INSTANCES instance Coll (ListColl a) -- Defined at T3017.hs:12:11 FAMILY INSTANCES - type Elem (ListColl a) + type instance Elem (ListColl a) = a -- Defined at T3017.hs:13:9 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/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 409e1efce1..484d843672 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -298,3 +298,5 @@ test('T15943', normal, compile, ['']) test('T15704', normal, compile, ['']) test('T15711', normal, compile, ['-ddump-types']) test('T15852', normal, compile, ['-ddump-types']) +test('T15764a', normal, compile, ['']) +test('T15740a', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr index ecbd7d9e79..776ee19592 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4a.stderr @@ -1,8 +1,12 @@ ExplicitForAllFams4a.hs:7:12: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ - • In the type family declaration for ‘H’ + • Type variable ‘b’ is bound by a forall, + but not used in the family instance + • In the equations for closed type family ‘H’ + In the type family declaration for ‘H’ ExplicitForAllFams4a.hs:8:10: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ - • In the type family declaration for ‘H’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance + • In the equations for closed type family ‘H’ + In the type family declaration for ‘H’ diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs index cb5665401b..c488f45a65 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.hs @@ -22,5 +22,6 @@ class C a where instance C Int where type forall a b. CT [a] (a,a) = Float type forall b. CT _ _ = Maybe b + data forall a b. CD [a] (a,a) = CD5 Float data forall b. CD _ _ = CD6 (Maybe b) diff --git a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr index 0861a8a756..8e268d6301 100644 --- a/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr +++ b/testsuite/tests/indexed-types/should_fail/ExplicitForAllFams4b.stderr @@ -1,44 +1,107 @@ ExplicitForAllFams4b.hs:7:24: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is bound by a forall, + but not used in the family instance • In the type instance declaration for ‘J’ +ExplicitForAllFams4b.hs:7:27: error: + Conflicting family instance declarations: + J [a] = Float -- Defined at ExplicitForAllFams4b.hs:7:27 + J _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:8:27 + ExplicitForAllFams4b.hs:8:22: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the type instance declaration for ‘J’ ExplicitForAllFams4b.hs:11:24: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘K’ +ExplicitForAllFams4b.hs:11:27: error: + Conflicting family instance declarations: + K (a, Bool) -- Defined at ExplicitForAllFams4b.hs:11:27 + K _ -- Defined at ExplicitForAllFams4b.hs:12:27 + ExplicitForAllFams4b.hs:12:22: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the data instance declaration for ‘K’ ExplicitForAllFams4b.hs:15:27: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the newtype instance declaration for ‘L’ +ExplicitForAllFams4b.hs:15:30: error: + Conflicting family instance declarations: + L (a, Bool) -- Defined at ExplicitForAllFams4b.hs:15:30 + L _ -- Defined at ExplicitForAllFams4b.hs:16:30 + ExplicitForAllFams4b.hs:16:25: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is mentioned in the RHS, + but not bound on the LHS of the family instance • In the newtype instance declaration for ‘L’ +ExplicitForAllFams4b.hs:23:3: error: + • Type indexes must match class instance head + Expected: CT Int _ + Actual: CT [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:23:20 + • In the type instance declaration for ‘CT’ + In the instance declaration for ‘C Int’ + ExplicitForAllFams4b.hs:23:17: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ is bound by a forall, + but not used in the family instance + • In the type instance declaration for ‘CT’ + In the instance declaration for ‘C Int’ + +ExplicitForAllFams4b.hs:23:20: error: + Conflicting family instance declarations: + CT [a] (a, a) = Float -- Defined at ExplicitForAllFams4b.hs:23:20 + CT _ _ = Maybe b -- Defined at ExplicitForAllFams4b.hs:24:20 + +ExplicitForAllFams4b.hs:24:3: error: + • Type indexes must match class instance head + Expected: CT Int _ + Actual: CT _ _ -- Defined at ExplicitForAllFams4b.hs:24:20 • In the type instance declaration for ‘CT’ In the instance declaration for ‘C Int’ ExplicitForAllFams4b.hs:24:15: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ + • Type variable ‘b’ 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 Int’ -ExplicitForAllFams4b.hs:25:17: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ +ExplicitForAllFams4b.hs:26:3: error: + • Type indexes must match class instance head + Expected: CD Int _ + Actual: CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20 + • In the data instance declaration for ‘CD’ + In the instance declaration for ‘C Int’ + +ExplicitForAllFams4b.hs:26:17: error: + • Type variable ‘b’ 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 Int’ + +ExplicitForAllFams4b.hs:26:20: error: + Conflicting family instance declarations: + CD [a] (a, a) -- Defined at ExplicitForAllFams4b.hs:26:20 + CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20 + +ExplicitForAllFams4b.hs:27:3: error: + • Type indexes must match class instance head + Expected: CD Int _ + Actual: CD _ _ -- Defined at ExplicitForAllFams4b.hs:27:20 • In the data instance declaration for ‘CD’ In the instance declaration for ‘C Int’ -ExplicitForAllFams4b.hs:26:15: error: - • Explicitly quantified but not used in LHS pattern: type variable ‘b’ +ExplicitForAllFams4b.hs:27:15: error: + • Type variable ‘b’ 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 Int’ diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr index cfbab576b9..eb54cf2e11 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr @@ -1,5 +1,5 @@ -SimpleFail13.hs:9:1: error: +SimpleFail13.hs:9:15: error: • Illegal type synonym family application ‘C a’ in instance: D [C a] • In the data instance declaration for ‘D’ diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs index fc773af0ff..7d78a15baa 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs @@ -8,7 +8,7 @@ class C a where type St a :: * instance C Int where - data Sd a :: * -- Looks like a nullary data instance decl + data Sd a = MkSd -- :: * -- Looks like a nullary data instance decl data Sd Int = SdC Char newtype Sn Int = SnC Char type St Int = Char diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr index 9bd571e2b9..b21375ceb2 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr @@ -2,6 +2,11 @@ SimpleFail2a.hs:11:3: error: • Type indexes must match class instance head Expected: Sd Int - Actual: Sd a :: * + Actual: Sd a -- Defined at SimpleFail2a.hs:11:11 • In the data instance declaration for ‘Sd’ In the instance declaration for ‘C Int’ + +SimpleFail2a.hs:11:11: error: + Conflicting family instance declarations: + Sd a -- Defined at SimpleFail2a.hs:11:11 + Sd Int -- Defined at SimpleFail2a.hs:12:11 diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs index 9c1c4a82d2..0f20f78e95 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs @@ -2,8 +2,10 @@ module ShouldFail where +import Data.Kind + class C7 a b where - data S7 b :: * + data S7 b :: Type instance C7 Char (a, Bool) where data S7 (a, Bool) = S7_1 diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr index b0c421fce8..b3dd8ef839 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr @@ -1,7 +1,7 @@ -SimpleFail9.hs:14:3: error: +SimpleFail9.hs:16:3: error: • Type indexes must match class instance head Expected: S7 (a, Int) - Actual: S7 (b, Int) + Actual: S7 (b, Int) -- Defined at SimpleFail9.hs:16:8 • In the data instance declaration for ‘S7’ In the instance declaration for ‘C7 Char (a, Int)’ diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr index 715febdc25..af8acae33a 100644 --- a/testsuite/tests/indexed-types/should_fail/T10817.stderr +++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr @@ -1,6 +1,7 @@ T10817.hs:9:3: error: - The type family application ‘F a’ - is no smaller than the instance head ‘F a’ - (Use UndecidableInstances to permit this) - In the class declaration for ‘C’ + • The type family application ‘F a’ + is no smaller than the instance head ‘F a’ + (Use UndecidableInstances to permit this) + • In the default type instance declaration for ‘F’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T10899.stderr b/testsuite/tests/indexed-types/should_fail/T10899.stderr index 925e4348fe..0dd92ef9bf 100644 --- a/testsuite/tests/indexed-types/should_fail/T10899.stderr +++ b/testsuite/tests/indexed-types/should_fail/T10899.stderr @@ -1,4 +1,5 @@ T10899.hs:7:3: error: • Illegal polymorphic type: forall (m :: * -> *). m a - • In the class declaration for ‘C’ + • In the default type instance declaration for ‘F’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T11450.stderr b/testsuite/tests/indexed-types/should_fail/T11450.stderr index a6fe961fcf..f5be9d48c3 100644 --- a/testsuite/tests/indexed-types/should_fail/T11450.stderr +++ b/testsuite/tests/indexed-types/should_fail/T11450.stderr @@ -1,7 +1,7 @@ -T11450.hs:9:8: error: +T11450.hs:9:3: error: • Type indexes must match class instance head Expected: T (Either a b) - Actual: T (Either b a) + Actual: T (Either b a) -- Defined at T11450.hs:9:8 • In the type instance declaration for ‘T’ In the instance declaration for ‘C (Either a b)’ diff --git a/testsuite/tests/indexed-types/should_fail/T12041.stderr b/testsuite/tests/indexed-types/should_fail/T12041.stderr index 006ca37bae..d16a9cc49c 100644 --- a/testsuite/tests/indexed-types/should_fail/T12041.stderr +++ b/testsuite/tests/indexed-types/should_fail/T12041.stderr @@ -1,7 +1,7 @@ -T12041.hs:12:15: error: - • Expected kind ‘i -> Constraint’, - but ‘(~) Int’ has kind ‘* -> Constraint’ - • In the type ‘(~) Int’ - In the type instance declaration for ‘Ob’ +T12041.hs:12:3: error: + • Type indexes must match class instance head + Expected: Ob @i (I @{i} @{i}) + Actual: Ob @* (I @{*} @{*}) -- Defined at T12041.hs:12:8 + • In the type instance declaration for ‘Ob’ In the instance declaration for ‘Category I’ diff --git a/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr b/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr index 9df66e7cd1..c13bde5ad8 100644 --- a/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13092/T13092.stderr @@ -2,4 +2,4 @@ Main.hs:10:15: error: Conflicting family instance declarations: A (a, Y) = Bool -- Defined at Main.hs:10:15 - A (B.X, b) = () -- Defined in ‘B’ + A (B.X, b) = () -- Defined in module B diff --git a/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr b/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr index 6676684ec1..ab714e3ecc 100644 --- a/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13092c/T13092c.stderr @@ -2,4 +2,4 @@ T13092c_4.hs:7:15: error: Conflicting family instance declarations: F (a, Char) = String -- Defined at T13092c_4.hs:7:15 - F (T13092c_2.X, b) = Bool -- Defined in ‘T13092c_2’ + F (T13092c_2.X, b) = Bool -- Defined in module T13092c_2 diff --git a/testsuite/tests/indexed-types/should_fail/T13972.hs b/testsuite/tests/indexed-types/should_fail/T13972.hs index a0a203d30a..9a5af411e2 100644 --- a/testsuite/tests/indexed-types/should_fail/T13972.hs +++ b/testsuite/tests/indexed-types/should_fail/T13972.hs @@ -8,5 +8,11 @@ import Data.Kind class C (a :: k) where type T k :: Type +-- This used to fail, with a mysterious error messate +-- Type indexes must match class instance head +-- Expected: T (a1 -> Either a1 b1) +-- Actual: T (a -> Either a b) +-- but now it succeeds fine + instance C Left where type T (a -> Either a b) = Int diff --git a/testsuite/tests/indexed-types/should_fail/T13972.stderr b/testsuite/tests/indexed-types/should_fail/T13972.stderr deleted file mode 100644 index b1f05b3105..0000000000 --- a/testsuite/tests/indexed-types/should_fail/T13972.stderr +++ /dev/null @@ -1,7 +0,0 @@ - -T13972.hs:12:8: error: - • Type indexes must match class instance head - Expected: T (a1 -> Either a1 b1) - Actual: T (a -> Either a b) - • In the type instance declaration for ‘T’ - In the instance declaration for ‘C Left’ diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.hs b/testsuite/tests/indexed-types/should_fail/T14045a.hs index fc545a8d41..985220c472 100644 --- a/testsuite/tests/indexed-types/should_fail/T14045a.hs +++ b/testsuite/tests/indexed-types/should_fail/T14045a.hs @@ -7,6 +7,11 @@ import Data.Kind class C (a :: k) where data S (a :: k) +-- This used to fail with the mysterious error +-- Type indexes must match class instance head +-- Expected: S z +-- Actual: S a +-- But now it is fine instance C (z :: Bool) where data S :: Bool -> Type where SF :: S False diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.stderr b/testsuite/tests/indexed-types/should_fail/T14045a.stderr deleted file mode 100644 index 0306bd2a07..0000000000 --- a/testsuite/tests/indexed-types/should_fail/T14045a.stderr +++ /dev/null @@ -1,7 +0,0 @@ - -T14045a.hs:11:3: error: - • Type indexes must match class instance head - Expected: S z - Actual: S :: Bool -> Type - • In the data instance declaration for ‘S’ - In the instance declaration for ‘C (z :: Bool)’ diff --git a/testsuite/tests/indexed-types/should_fail/T14179.stderr b/testsuite/tests/indexed-types/should_fail/T14179.stderr index 38d77f1cca..bb956c7b51 100644 --- a/testsuite/tests/indexed-types/should_fail/T14179.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14179.stderr @@ -6,8 +6,8 @@ T14179.hs:7:15: error: T14179.hs:11:15: error: Conflicting family instance declarations: - Foo2 a -- Defined at T14179.hs:11:15 - Foo2 a -- Defined at T14179.hs:12:15 + Foo2 -- Defined at T14179.hs:11:15 + Foo2 -- Defined at T14179.hs:12:15 T14179.hs:15:15: error: Conflicting family instance declarations: diff --git a/testsuite/tests/indexed-types/should_fail/T14887.hs b/testsuite/tests/indexed-types/should_fail/T14887.hs new file mode 100644 index 0000000000..63fbbd3943 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T14887.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fprint-explicit-kinds #-} +module T14887 where + +import Data.Kind +import Data.Type.Equality + +type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where + Foo1 (e :: a :~: a) = a :~: a + +type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where + Foo2 k (e :: a :~: a) = a :~: a diff --git a/testsuite/tests/indexed-types/should_fail/T14887.stderr b/testsuite/tests/indexed-types/should_fail/T14887.stderr new file mode 100644 index 0000000000..56875a7628 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T14887.stderr @@ -0,0 +1,12 @@ + +T14887.hs:13:1: error: + • The kind of ‘Foo2’ is ill-scoped + Inferred kind: Foo2 :: forall (a :: k). forall k -> (a :~: a) -> * + NB: Specified variables (namely: (a :: k)) always come first + Perhaps try this order instead: k (a :: k) (e :: a :~: a) + • In the type family declaration for ‘Foo2’ + +T14887.hs:14:11: error: + • Expected kind ‘a0 :~: a0’, but ‘e :: a :~: a’ has kind ‘a :~: a’ + • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ + In the type family declaration for ‘Foo2’ diff --git a/testsuite/tests/indexed-types/should_fail/T15740.hs b/testsuite/tests/indexed-types/should_fail/T15740.hs new file mode 100644 index 0000000000..e564a87509 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15740.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeInType, TypeFamilies, KindSignatures, RankNTypes #-} + +module T15740 where + +import Data.Kind + +type family F2 :: forall k. k -> Type +data SBool :: Bool -> Type +data Nat +data SNat :: Nat -> Type +type instance F2 = SBool +type instance F2 = SNat diff --git a/testsuite/tests/indexed-types/should_fail/T15740.stderr b/testsuite/tests/indexed-types/should_fail/T15740.stderr new file mode 100644 index 0000000000..9d7cdcfee7 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15740.stderr @@ -0,0 +1,11 @@ + +T15740.hs:11:20: error: + • Expected kind ‘forall k. k -> *’, + but ‘SBool’ has kind ‘Bool -> *’ + • In the type ‘SBool’ + In the type instance declaration for ‘F2’ + +T15740.hs:12:20: error: + • Expected kind ‘forall k. k -> *’, but ‘SNat’ has kind ‘Nat -> *’ + • In the type ‘SNat’ + In the type instance declaration for ‘F2’ diff --git a/testsuite/tests/indexed-types/should_fail/T15764.hs b/testsuite/tests/indexed-types/should_fail/T15764.hs new file mode 100644 index 0000000000..f4c164cd05 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15764.hs @@ -0,0 +1,14 @@ +{-# Language PolyKinds #-} +{-# Language TypeFamilies #-} +{-# Language KindSignatures #-} +{-# Language DataKinds #-} +{-# Language MultiParamTypeClasses #-} + +module T15764 where + +import Data.Kind +import Data.Proxy +import GHC.TypeLits + +class C6 (k :: Type) (a :: k) (b :: Proxy (a :: k)) where + type T6 (proxy :: Proxy '(k, b)) diff --git a/testsuite/tests/indexed-types/should_fail/T15764.stderr b/testsuite/tests/indexed-types/should_fail/T15764.stderr new file mode 100644 index 0000000000..5c04427841 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15764.stderr @@ -0,0 +1,11 @@ + +T15764.hs:14:2: error: + • The kind of ‘T6’ is ill-scoped + Inferred kind: T6 :: forall (a :: k) k (b :: Proxy a). + Proxy '(k, b) -> * + NB: Inferred variables + (namely: (a :: k)) always come first + then Specified variables (namely: k (b :: Proxy a)) + Perhaps try this order instead: + k (a :: k) (b :: Proxy a) (proxy :: Proxy '(k, b)) + • In the associated type family declaration for ‘T6’ diff --git a/testsuite/tests/indexed-types/should_fail/T15870.hs b/testsuite/tests/indexed-types/should_fail/T15870.hs new file mode 100644 index 0000000000..0a07c3e5e5 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15870.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module T15870 where + +data Optic a where + --Index :: Nat -> Optic a + --Name :: Symbol -> Optic a + (:.:) :: Optic a -> Optic b -> Optic a -- composition + +class Gettable a (optic :: Optic a) where + type Get a (optic :: Optic a) + +{- +some basic instances, e.g. +instance Gettable (a,b) (Index 0) where + type Get (a,b) (Index 0) = a +... +-} + +instance forall a b (g1 :: Optic a) (g2 :: Optic b). + ( Gettable a g1 + , b ~ Get a g1 + , Gettable b g2 + ) => Gettable a (g1 :.: g2) where + type Get a (g1 :.: g2) = Get a g2 diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr new file mode 100644 index 0000000000..4acacbab50 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr @@ -0,0 +1,6 @@ + +T15870.hs:32:34: error: + • Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’ + • In the second argument of ‘Get’, namely ‘g2’ + In the type ‘Get a g2’ + In the type instance declaration for ‘Get’ diff --git a/testsuite/tests/indexed-types/should_fail/T7536.stderr b/testsuite/tests/indexed-types/should_fail/T7536.stderr index 9e7ed3010e..22c565be62 100644 --- a/testsuite/tests/indexed-types/should_fail/T7536.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7536.stderr @@ -1,5 +1,6 @@ -T7536.hs:8:15: - Family instance purports to bind type variable ‘a’ - but the real LHS (expanding synonyms) is: TF Int = ... - In the type instance declaration for ‘TF’ +T7536.hs:8:21: error: + • Type variable ‘a’ is mentioned in the RHS, + but not bound on the LHS of the family instance + The real LHS (expanding synonyms) is: TF Int + • In the type instance declaration for ‘TF’ diff --git a/testsuite/tests/indexed-types/should_fail/T7938.hs b/testsuite/tests/indexed-types/should_fail/T7938.hs index 405a7e54d0..246015ddf7 100644 --- a/testsuite/tests/indexed-types/should_fail/T7938.hs +++ b/testsuite/tests/indexed-types/should_fail/T7938.hs @@ -9,4 +9,4 @@ class Foo (a :: k1) (b :: k2) where type Bar a instance Foo (a :: k1) (b :: k2) where - type Bar a = (KP :: KProxy k2)
\ No newline at end of file + type Bar a = (KP :: KProxy k2) diff --git a/testsuite/tests/indexed-types/should_fail/T7938.stderr b/testsuite/tests/indexed-types/should_fail/T7938.stderr index 890be7b7b8..5751c4e992 100644 --- a/testsuite/tests/indexed-types/should_fail/T7938.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7938.stderr @@ -1,6 +1,6 @@ T7938.hs:12:17: error: - • Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k4’ + • Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k2’ • In the type ‘(KP :: KProxy k2)’ In the type instance declaration for ‘Bar’ In the instance declaration for ‘Foo (a :: k1) (b :: k2)’ diff --git a/testsuite/tests/indexed-types/should_fail/T9160.stderr b/testsuite/tests/indexed-types/should_fail/T9160.stderr index 4ed166cfdb..36a1cb6767 100644 --- a/testsuite/tests/indexed-types/should_fail/T9160.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9160.stderr @@ -1,7 +1,7 @@ -T9160.hs:19:12: error: - Expecting one more argument to ‘Maybe’ - Expected a type, but ‘Maybe’ has kind ‘* -> *’ - In the type ‘Maybe’ - In the type instance declaration for ‘F’ - In the instance declaration for ‘C (a :: *)’ +T9160.hs:19:3: error: + • Type indexes must match class instance head + Expected: F @* + Actual: F @(* -> *) -- Defined at T9160.hs:19:8 + • In the type instance declaration for ‘F’ + In the instance declaration for ‘C (a :: *)’ diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 12fa999a9f..6273f595b0 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -139,12 +139,16 @@ test('T13271', normal, compile_fail, ['']) test('T13674', normal, compile_fail, ['']) test('T13784', normal, compile_fail, ['']) test('T13877', normal, compile_fail, ['']) -test('T13972', normal, compile_fail, ['']) +test('T13972', normal, compile, ['']) test('T14033', normal, compile_fail, ['']) -test('T14045a', normal, compile_fail, ['']) +test('T14045a', normal, compile, ['']) test('T14175', normal, compile_fail, ['']) test('T14179', normal, compile_fail, ['']) test('T14246', normal, compile_fail, ['']) test('T14369', normal, compile_fail, ['']) test('T15172', normal, compile_fail, ['']) test('T14904', normal, compile_fail, ['']) +test('T15740', normal, compile_fail, ['']) +test('T15764', normal, compile_fail, ['']) +test('T15870', normal, compile_fail, ['']) +test('T14887', normal, compile_fail, ['']) diff --git a/testsuite/tests/partial-sigs/should_compile/ADT.stderr b/testsuite/tests/partial-sigs/should_compile/ADT.stderr index 0569722f24..385a44b737 100644 --- a/testsuite/tests/partial-sigs/should_compile/ADT.stderr +++ b/testsuite/tests/partial-sigs/should_compile/ADT.stderr @@ -1,7 +1,7 @@ TYPE SIGNATURES bar :: Int -> Foo Bool () Int TYPE CONSTRUCTORS - Foo :: * -> * -> * -> * + Foo{3} :: * -> * -> * -> * DATA CONSTRUCTORS Foo :: forall x y z. x -> y -> z -> Foo x y z Dependent modules: [] diff --git a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr index 12982a740c..6f68f3cd66 100644 --- a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr @@ -1,20 +1,20 @@ TYPE SIGNATURES foo :: Sing 'A TYPE CONSTRUCTORS - MyKind :: * + MyKind{0} :: * type role Sing nominal nominal - Sing :: forall k. k -> * + Sing{2} :: forall k. k -> * COERCION AXIOMS axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 :: - Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1 - -- Defined at DataFamilyInstanceLHS.hs:8:15 + Sing = DataFamilyInstanceLHS.R:SingMyKind_ DATA CONSTRUCTORS A :: MyKind B :: MyKind SingA :: Sing 'A SingB :: Sing 'B FAMILY INSTANCES - data instance Sing + data instance Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _ + -- Defined at DataFamilyInstanceLHS.hs:8:15 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/partial-sigs/should_compile/Meltdown.stderr b/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr index 750a951222..a40ecfeee0 100644 --- a/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr +++ b/testsuite/tests/partial-sigs/should_compile/Meltdown.stderr @@ -5,7 +5,7 @@ TYPE SIGNATURES NukeMonad param1 param2 () -> NukeMonad param1 param2 () TYPE CONSTRUCTORS type role NukeMonad phantom phantom phantom - NukeMonad :: * -> * -> * -> * + NukeMonad{3} :: * -> * -> * -> * CLASS INSTANCES instance Functor (NukeMonad a b) -- Defined at Meltdown.hs:8:10 instance Applicative (NukeMonad a b) diff --git a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr index 1cd0417e54..94245d6aa2 100644 --- a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr @@ -1,11 +1,10 @@ TYPE CONSTRUCTORS - MyKind :: * + MyKind{0} :: * type role Sing nominal nominal - Sing :: forall k. k -> * + Sing{2} :: forall k. k -> * COERCION AXIOMS axiom NamedWildcardInDataFamilyInstanceLHS.D:R:SingMyKind_a0 :: - Sing _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a - -- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15 + Sing = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a DATA CONSTRUCTORS A :: MyKind B :: MyKind @@ -13,6 +12,8 @@ DATA CONSTRUCTORS SingB :: Sing 'B FAMILY INSTANCES data instance Sing + _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a + -- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15 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/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr index 0554f0a6e7..5a709fff9d 100644 --- a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr @@ -1,10 +1,8 @@ TYPE CONSTRUCTORS type role F nominal - F :: * -> * + F{1} :: * -> * COERCION AXIOMS - axiom NamedWildcardInTypeFamilyInstanceLHS.D:R:F :: - F _t = Int - -- Defined at NamedWildcardInTypeFamilyInstanceLHS.hs:5:3 + axiom NamedWildcardInTypeFamilyInstanceLHS.D:R:F :: F _t = Int 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/partial-sigs/should_compile/SkipMany.stderr b/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr index a821a6970a..0ee0a34564 100644 --- a/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr +++ b/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr @@ -4,7 +4,7 @@ TYPE SIGNATURES skipMany' :: forall tok st a. GenParser tok st a -> GenParser tok st () TYPE CONSTRUCTORS - GenParser :: * -> * -> * -> * + GenParser{3} :: * -> * -> * -> * DATA CONSTRUCTORS GenParser :: forall tok st a. tok -> st -> a -> GenParser tok st a Dependent modules: [] diff --git a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr index ae82437e1d..8f24ba1384 100644 --- a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr +++ b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr @@ -2,15 +2,15 @@ TYPE SIGNATURES foo :: F Int Char -> Int TYPE CONSTRUCTORS type role F nominal nominal - F :: * -> * -> * + F{2} :: * -> * -> * COERCION AXIOMS - axiom TypeFamilyInstanceLHS.D:R:FBool_1 :: - F Bool _1 = Bool -- Defined at TypeFamilyInstanceLHS.hs:8:15 - axiom TypeFamilyInstanceLHS.D:R:FInt_1 :: - F Int _1 = Int -- Defined at TypeFamilyInstanceLHS.hs:7:15 + axiom TypeFamilyInstanceLHS.D:R:FBool_1 :: F Bool _1 = Bool + axiom TypeFamilyInstanceLHS.D:R:FInt_1 :: F Int _1 = Int FAMILY INSTANCES - type instance F Int _1 - type instance F Bool _1 + type instance F Int _ = Int + -- Defined at TypeFamilyInstanceLHS.hs:7:15 + type instance F Bool _ = Bool + -- Defined at TypeFamilyInstanceLHS.hs:8:15 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/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index 20a0fa51ca..67fae7b31e 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,10 +1,10 @@ T14040a.hs:34:8: error: - • Cannot apply expression of type ‘Sing wl - -> (forall y. p w0 'WeirdNil) + • Cannot apply expression of type ‘Sing wl0 + -> (forall y. p0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). - Sing x -> Sing xs -> p w1 xs -> p w2 ('WeirdCons x xs)) - -> p w3 wl’ + Sing x -> Sing xs -> p0 w1 xs -> p0 w2 ('WeirdCons x xs)) + -> p0 w3 wl0’ to a visible type argument ‘(WeirdList z)’ • In the sixth argument of ‘pWeirdCons’, namely ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ 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, ['']) diff --git a/testsuite/tests/roles/should_compile/Roles1.stderr b/testsuite/tests/roles/should_compile/Roles1.stderr index 3278701048..c2678b71d7 100644 --- a/testsuite/tests/roles/should_compile/Roles1.stderr +++ b/testsuite/tests/roles/should_compile/Roles1.stderr @@ -1,16 +1,16 @@ TYPE CONSTRUCTORS type role T1 nominal - T1 :: * -> * - T2 :: * -> * + T1{1} :: * -> * + T2{1} :: * -> * type role T3 nominal phantom - T3 :: forall k. k -> * + T3{2} :: forall k. k -> * type role T4 nominal nominal - T4 :: (* -> *) -> * -> * - T5 :: * -> * + T4{2} :: (* -> *) -> * -> * + T5{1} :: * -> * type role T6 nominal phantom - T6 :: forall {k}. k -> * + T6{2} :: forall {k}. k -> * type role T7 nominal phantom representational - T7 :: forall {k}. k -> * -> * + T7{3} :: forall {k}. k -> * -> * DATA CONSTRUCTORS K7 :: forall {k} (a :: k) b. b -> T7 a b K6 :: forall {k} (a :: k). T6 a diff --git a/testsuite/tests/roles/should_compile/Roles14.stderr b/testsuite/tests/roles/should_compile/Roles14.stderr index 57899142d9..1745332a6b 100644 --- a/testsuite/tests/roles/should_compile/Roles14.stderr +++ b/testsuite/tests/roles/should_compile/Roles14.stderr @@ -2,9 +2,9 @@ TYPE SIGNATURES meth2 :: forall a. C2 a => a -> a TYPE CONSTRUCTORS type role C2 representational - C2 :: * -> Constraint + C2{1} :: * -> Constraint COERCION AXIOMS - axiom Roles12.N:C2 :: C2 a = a -> a -- Defined at Roles14.hs:6:1 + axiom Roles12.N:C2 :: C2 a = a -> 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/roles/should_compile/Roles2.stderr b/testsuite/tests/roles/should_compile/Roles2.stderr index 4cb55ec063..170315111d 100644 --- a/testsuite/tests/roles/should_compile/Roles2.stderr +++ b/testsuite/tests/roles/should_compile/Roles2.stderr @@ -1,7 +1,7 @@ TYPE CONSTRUCTORS - T1 :: * -> * + T1{1} :: * -> * type role T2 phantom - T2 :: * -> * + T2{1} :: * -> * DATA CONSTRUCTORS K2 :: forall a. FunPtr a -> T2 a K1 :: forall a. IO a -> T1 a diff --git a/testsuite/tests/roles/should_compile/Roles3.stderr b/testsuite/tests/roles/should_compile/Roles3.stderr index b3507b0564..bf76b72987 100644 --- a/testsuite/tests/roles/should_compile/Roles3.stderr +++ b/testsuite/tests/roles/should_compile/Roles3.stderr @@ -4,25 +4,22 @@ TYPE SIGNATURES meth3 :: forall a b. C3 a b => a -> F3 b -> F3 b meth4 :: forall a b. C4 a b => a -> F4 b -> F4 b TYPE CONSTRUCTORS - C1 :: * -> Constraint - C2 :: * -> * -> Constraint - C3 :: * -> * -> Constraint - C4 :: * -> * -> Constraint + C1{1} :: * -> Constraint + C2{2} :: * -> * -> Constraint + C3{2} :: * -> * -> Constraint + C4{2} :: * -> * -> Constraint type role F3 nominal - F3 :: * -> * + F3{1} :: * -> * type role F4 nominal - F4 :: * -> * + F4{1} :: * -> * type role Syn1 nominal - Syn1 :: * -> * - Syn2 :: * -> * + Syn1{1} :: * -> * + Syn2{1} :: * -> * COERCION AXIOMS - axiom Roles3.N:C1 :: C1 a = a -> a -- Defined at Roles3.hs:6:1 - axiom Roles3.N:C2 :: - C2 a b = (a ~ b) => a -> b -- Defined at Roles3.hs:9:1 - axiom Roles3.N:C3 :: - C3 a b = a -> F3 b -> F3 b -- Defined at Roles3.hs:12:1 - axiom Roles3.N:C4 :: - C4 a b = a -> F4 b -> F4 b -- Defined at Roles3.hs:18:1 + axiom Roles3.N:C1 :: C1 a = a -> a + axiom Roles3.N:C2 :: C2 a b = (a ~ b) => a -> b + axiom Roles3.N:C3 :: C3 a b = a -> F3 b -> F3 b + axiom Roles3.N:C4 :: C4 a b = a -> F4 b -> F4 b 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/roles/should_compile/Roles4.stderr b/testsuite/tests/roles/should_compile/Roles4.stderr index 93a86a514c..dbca015edb 100644 --- a/testsuite/tests/roles/should_compile/Roles4.stderr +++ b/testsuite/tests/roles/should_compile/Roles4.stderr @@ -2,13 +2,12 @@ TYPE SIGNATURES meth1 :: forall a. C1 a => a -> a meth3 :: forall a. C3 a => a -> Syn1 a TYPE CONSTRUCTORS - C1 :: * -> Constraint - C3 :: * -> Constraint - Syn1 :: * -> * + C1{1} :: * -> Constraint + C3{1} :: * -> Constraint + Syn1{1} :: * -> * COERCION AXIOMS - axiom Roles4.N:C1 :: C1 a = a -> a -- Defined at Roles4.hs:6:1 - axiom Roles4.N:C3 :: - C3 a = a -> Syn1 a -- Defined at Roles4.hs:11:1 + axiom Roles4.N:C1 :: C1 a = a -> a + axiom Roles4.N:C3 :: C3 a = a -> Syn1 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/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr index eaad63859d..4e2fe00e87 100644 --- a/testsuite/tests/roles/should_compile/T8958.stderr +++ b/testsuite/tests/roles/should_compile/T8958.stderr @@ -3,12 +3,12 @@ T8958.hs:1:31: warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language. TYPE CONSTRUCTORS type role Map nominal representational - Map :: * -> * -> * - Nominal :: * -> Constraint + Map{2} :: * -> * -> * + Nominal{1} :: * -> Constraint type role Representational representational - Representational :: * -> Constraint + Representational{1} :: * -> Constraint COERCION AXIOMS - axiom T8958.N:Map :: Map k v = [(k, v)] -- Defined at T8958.hs:13:1 + axiom T8958.N:Map :: Map k v = [(k, v)] DATA CONSTRUCTORS MkMap :: forall k v. [(k, v)] -> Map k v CLASS INSTANCES diff --git a/testsuite/tests/showIface/Orphans.stdout b/testsuite/tests/showIface/Orphans.stdout index 63fcd79a19..38e4066d9e 100644 --- a/testsuite/tests/showIface/Orphans.stdout +++ b/testsuite/tests/showIface/Orphans.stdout @@ -2,5 +2,5 @@ instance [orphan] GHC.Exts.IsList [GHC.Types.Bool] = $fIsListBool instance GHC.Exts.IsList [X] = $fIsListX family instance GHC.Exts.Item [X] = D:R:ItemX family instance [orphan] GHC.Exts.Item [GHC.Types.Bool] -"myrule1" [orphan] forall @ a -"myrule2" forall GHC.Base.id @ (X -> X) f = f +"myrule1" [orphan] forall @ a. +"myrule2" GHC.Base.id @ (X -> X) f = f diff --git a/testsuite/tests/th/TH_Roles2.stderr b/testsuite/tests/th/TH_Roles2.stderr index c988015622..3807609678 100644 --- a/testsuite/tests/th/TH_Roles2.stderr +++ b/testsuite/tests/th/TH_Roles2.stderr @@ -1,6 +1,6 @@ TYPE CONSTRUCTORS type role T nominal representational - T :: forall k. k -> * + T{2} :: forall k. k -> * Dependent modules: [] Dependent packages: [array-0.5.2.0, base-4.12.0.0, deepseq-1.4.4.0, ghc-boot-th-8.7, ghc-prim-0.5.3, integer-gmp-1.0.2.0, diff --git a/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr b/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr index 6205547873..673f09e2e0 100644 --- a/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr +++ b/testsuite/tests/th/TH_reifyExplicitForAllFams.stderr @@ -13,4 +13,4 @@ type family TH_reifyExplicitForAllFams.H (a_0 :: *) (b_1 :: *) :: * where (Data.Proxy.Proxy y_3) = Data.Either.Either x_2 y_3 forall (z_4 :: *). TH_reifyExplicitForAllFams.H z_4 - z_4 = GHC.Maybe.Maybe z_4
\ No newline at end of file + z_4 = GHC.Maybe.Maybe z_4 diff --git a/testsuite/tests/typecheck/should_compile/T12763.stderr b/testsuite/tests/typecheck/should_compile/T12763.stderr index ad3460c2da..99a66bd59e 100644 --- a/testsuite/tests/typecheck/should_compile/T12763.stderr +++ b/testsuite/tests/typecheck/should_compile/T12763.stderr @@ -2,9 +2,9 @@ TYPE SIGNATURES f :: Int -> () m :: forall a. C a => a -> () TYPE CONSTRUCTORS - C :: * -> Constraint + C{1} :: * -> Constraint COERCION AXIOMS - axiom T12763.N:C :: C a = a -> () -- Defined at T12763.hs:6:1 + axiom T12763.N:C :: C a = a -> () CLASS INSTANCES instance C Int -- Defined at T12763.hs:9:10 Dependent modules: [] diff --git a/testsuite/tests/typecheck/should_compile/tc231.stderr b/testsuite/tests/typecheck/should_compile/tc231.stderr index 6c785b4a40..18beabd3a1 100644 --- a/testsuite/tests/typecheck/should_compile/tc231.stderr +++ b/testsuite/tests/typecheck/should_compile/tc231.stderr @@ -6,13 +6,11 @@ TYPE SIGNATURES huh :: forall s a b chain. Zork s a b => Q s a chain -> ST s () s :: forall t t1. Q t (Z [Char]) t1 -> Q t (Z [Char]) t1 TYPE CONSTRUCTORS - Q :: * -> * -> * -> * - Z :: * -> * - Zork :: * -> * -> * -> Constraint + Q{3} :: * -> * -> * -> * + Z{1} :: * -> * + Zork{3} :: * -> * -> * -> Constraint COERCION AXIOMS - axiom N:Zork :: - Zork s a b = forall chain. Q s a chain -> ST s () - -- Defined at tc231.hs:25:1 + axiom N:Zork :: Zork s a b = forall chain. Q s a chain -> ST s () DATA CONSTRUCTORS Z :: forall a. a -> Z a Node :: forall s a chain. s -> a -> chain -> Q s a chain diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr index 21ae68ab85..afa8330765 100644 --- a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr +++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr @@ -3,3 +3,8 @@ LevPolyBounded.hs:10:15: error: • Expected a type, but ‘a’ has kind ‘TYPE r’ • In the type signature: LevPolyBounded.minBound :: a In the class declaration for ‘XBounded’ + +LevPolyBounded.hs:11:15: error: + • Expected a type, but ‘a’ has kind ‘TYPE r’ + • In the type signature: LevPolyBounded.maxBound :: a + In the class declaration for ‘XBounded’ diff --git a/testsuite/tests/typecheck/should_fail/T13983.stderr b/testsuite/tests/typecheck/should_fail/T13983.stderr index 5c7a031654..d1b2fe067b 100644 --- a/testsuite/tests/typecheck/should_fail/T13983.stderr +++ b/testsuite/tests/typecheck/should_fail/T13983.stderr @@ -5,4 +5,4 @@ T13983.hs:7:1: error: of its type variables. Perhaps you meant to bind it explicitly somewhere? Type variables with inferred kinds: (k :: *) - • In the type declaration for ‘Wat’ + • In the type synonym declaration for ‘Wat’ diff --git a/testsuite/tests/typecheck/should_fail/T14607.hs b/testsuite/tests/typecheck/should_fail/T14607.hs index 86c738dc19..af2e1c7677 100644 --- a/testsuite/tests/typecheck/should_fail/T14607.hs +++ b/testsuite/tests/typecheck/should_fail/T14607.hs @@ -31,4 +31,4 @@ instance Mk a where -- So now the kind error can be deferred. -- Consequence of a fast-path for tcImplicitTKBndrsX I think. - +-- Later (Nov 18) we are back to a kind error, which is fine diff --git a/testsuite/tests/typecheck/should_fail/T14607.stderr b/testsuite/tests/typecheck/should_fail/T14607.stderr index 5e0b66a340..b7d60593e1 100644 --- a/testsuite/tests/typecheck/should_fail/T14607.stderr +++ b/testsuite/tests/typecheck/should_fail/T14607.stderr @@ -1,21 +1,12 @@ -T14607.hs:22:9: warning: [-Wdeferred-type-errors (in -Wdefault)] +T14607.hs:22:9: error: • Expecting one more argument to ‘LamCons a '()’ - Expected a type, but ‘LamCons a '()’ has kind ‘() -> *’ - • In the type signature: mk :: LamCons a '() + Expected a type, but ‘LamCons a '()’ has kind ‘() -> *’ + • In the type signature: mk :: LamCons a '() In the instance declaration for ‘Mk a’ -T14607.hs:22:19: warning: [-Wdeferred-type-errors (in -Wdefault)] +T14607.hs:22:19: error: • Expected a type, but ‘'()’ has kind ‘()’ • In the second argument of ‘LamCons’, namely ‘'()’ In the type signature: mk :: LamCons a '() In the instance declaration for ‘Mk a’ - -T14607.hs:23:8: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Couldn't match expected type ‘LamCons a '()’ - with actual type ‘LamCons a0 a0 '()’ - • In the expression: mk - In an equation for ‘mk’: mk = mk - In the instance declaration for ‘Mk a’ - • Relevant bindings include - mk :: LamCons a '() (bound at T14607.hs:23:3) diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr index 2b2ca0d22a..63379a03b9 100644 --- a/testsuite/tests/typecheck/should_fail/T2688.stderr +++ b/testsuite/tests/typecheck/should_fail/T2688.stderr @@ -2,9 +2,11 @@ T2688.hs:8:14: error: • Couldn't match expected type ‘v’ with actual type ‘s’ ‘s’ is a rigid type variable bound by - the class declaration for ‘VectorSpace’ at T2688.hs:5:21 + the class declaration for ‘VectorSpace’ + at T2688.hs:(5,1)-(8,23) ‘v’ is a rigid type variable bound by - the class declaration for ‘VectorSpace’ at T2688.hs:5:19 + the class declaration for ‘VectorSpace’ + at T2688.hs:(5,1)-(8,23) • In the expression: v *^ (1 / s) In an equation for ‘^/’: v ^/ s = v *^ (1 / s) • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr index 0e230e62c8..84af180b20 100644 --- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr +++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr @@ -59,9 +59,9 @@ T6018fail.hs:53:15: error: T6018fail.hs:61:10: error: Type family equation violates injectivity annotation. - Kind variable ‘k2’ cannot be inferred from the right-hand side. + Kind variable ‘k1’ cannot be inferred from the right-hand side. In the type family equation: - PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1 + PolyKindVarsF @{[k1]} @[k2] ('[] @k1) = '[] @k2 -- Defined at T6018fail.hs:61:10 T6018fail.hs:64:15: error: diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 3805315398..7dca65b499 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -469,7 +469,7 @@ test('T14350', normal, compile_fail, ['']) test('T14390', normal, compile_fail, ['']) test('MissingExportList03', normal, compile_fail, ['']) test('T14618', normal, compile_fail, ['']) -test('T14607', normal, compile, ['']) +test('T14607', normal, compile_fail, ['']) test('T14605', normal, compile_fail, ['']) test('T14761a', normal, compile_fail, ['']) test('T14761b', normal, compile_fail, ['']) |