diff options
Diffstat (limited to 'testsuite/tests/indexed-types')
38 files changed, 298 insertions, 79 deletions
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, ['']) |