diff options
Diffstat (limited to 'testsuite/tests/dependent')
73 files changed, 183 insertions, 160 deletions
diff --git a/testsuite/tests/dependent/ghci/T11549.script b/testsuite/tests/dependent/ghci/T11549.script index d8a0e97a61..3e0811f921 100644 --- a/testsuite/tests/dependent/ghci/T11549.script +++ b/testsuite/tests/dependent/ghci/T11549.script @@ -1,4 +1,4 @@ -:set -XTypeInType +:set -XPolyKinds import GHC.Exts putStrLn "-fno-print-explicit-runtime-reps" diff --git a/testsuite/tests/dependent/ghci/T14238.stdout b/testsuite/tests/dependent/ghci/T14238.stdout index fddbc0de54..729f821af7 100644 --- a/testsuite/tests/dependent/ghci/T14238.stdout +++ b/testsuite/tests/dependent/ghci/T14238.stdout @@ -1 +1 @@ -Foo :: forall k -> k -> * +Foo :: forall k -> k -> Type diff --git a/testsuite/tests/dependent/should_compile/Dep1.hs b/testsuite/tests/dependent/should_compile/Dep1.hs index 6f8fe0720d..086d759bbe 100644 --- a/testsuite/tests/dependent/should_compile/Dep1.hs +++ b/testsuite/tests/dependent/should_compile/Dep1.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module Dep1 where diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/dependent/should_compile/Dep2.hs index df1cb51e08..34be3cffc6 100644 --- a/testsuite/tests/dependent/should_compile/Dep2.hs +++ b/testsuite/tests/dependent/should_compile/Dep2.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, GADTs #-} +{-# LANGUAGE PolyKinds, GADTs #-} module Dep2 where diff --git a/testsuite/tests/dependent/should_compile/Dep3.hs b/testsuite/tests/dependent/should_compile/Dep3.hs index cba5043a08..db10d2a8c6 100644 --- a/testsuite/tests/dependent/should_compile/Dep3.hs +++ b/testsuite/tests/dependent/should_compile/Dep3.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, TypeInType, GADTs #-} +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs #-} module Dep3 where diff --git a/testsuite/tests/dependent/should_compile/DkNameRes.hs b/testsuite/tests/dependent/should_compile/DkNameRes.hs new file mode 100644 index 0000000000..4110b33882 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/DkNameRes.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} + +module DkNameRes where + +import Data.Proxy +import Data.Kind + +type family IfK (e :: Proxy (j :: Bool)) :: Type where + IfK (_ :: Proxy True) = () diff --git a/testsuite/tests/dependent/should_compile/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs deleted file mode 100644 index 47957d47d6..0000000000 --- a/testsuite/tests/dependent/should_compile/InferDependency.hs +++ /dev/null @@ -1,6 +0,0 @@ -{-# LANGUAGE TypeInType #-} - -module InferDependency where - -data Proxy k (a :: k) -data Proxy2 k a = P (Proxy k a) diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs index 4cba8281ca..1caa46f7c3 100644 --- a/testsuite/tests/dependent/should_compile/KindEqualities.hs +++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-} +{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module KindEqualities where diff --git a/testsuite/tests/dependent/should_compile/KindEqualities2.hs b/testsuite/tests/dependent/should_compile/KindEqualities2.hs index 5a6f60d40b..0bdfcfa034 100644 --- a/testsuite/tests/dependent/should_compile/KindEqualities2.hs +++ b/testsuite/tests/dependent/should_compile/KindEqualities2.hs @@ -1,6 +1,5 @@ {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll, - TemplateHaskell, UndecidableInstances, ScopedTypeVariables, - TypeInType #-} + TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-} module KindEqualities2 where diff --git a/testsuite/tests/dependent/should_compile/KindLevels.hs b/testsuite/tests/dependent/should_compile/KindLevels.hs index 1aad299df3..5540ce40cd 100644 --- a/testsuite/tests/dependent/should_compile/KindLevels.hs +++ b/testsuite/tests/dependent/should_compile/KindLevels.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module KindLevels where diff --git a/testsuite/tests/dependent/should_compile/RAE_T32b.hs b/testsuite/tests/dependent/should_compile/RAE_T32b.hs index 7e067099c9..ddd21db18d 100644 --- a/testsuite/tests/dependent/should_compile/RAE_T32b.hs +++ b/testsuite/tests/dependent/should_compile/RAE_T32b.hs @@ -1,23 +1,27 @@ {-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, DataKinds, PolyKinds, - RankNTypes, TypeOperators, TypeInType #-} + RankNTypes, TypeOperators #-} module RAE_T32b where import Data.Kind -data family Sing (k :: *) :: k -> * +data family Sing (k :: Type) :: k -> Type -data TyArr (a :: *) (b :: *) :: * -type family (a :: TyArr k1 k2 -> *) @@ (b :: k1) :: k2 +data TyArr (a :: Type) (b :: Type) :: Type +type family (a :: TyArr k1 k2 -> Type) @@ (b :: k1) :: k2 $(return []) -data Sigma (p :: *) (r :: TyArr p * -> *) :: * where - Sigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a). - Sing * p -> Sing (TyArr p * -> *) r -> Sing p a -> Sing (r @@ a) b -> Sigma p r +data Sigma (p :: Type) (r :: TyArr p Type -> Type) :: Type where + Sigma :: forall (p :: Type) (r :: TyArr p Type -> Type) + (a :: p) (b :: r @@ a). + Sing Type p -> Sing (TyArr p Type -> Type) r -> Sing p a -> + Sing (r @@ a) b -> Sigma p r $(return []) -data instance Sing (Sigma p r) (x :: Sigma p r) :: * where - SSigma :: forall (p :: *) (r :: TyArr p * -> *) (a :: p) (b :: r @@ a) - (sp :: Sing * p) (sr :: Sing (TyArr p * -> *) r) (sa :: Sing p a) (sb :: Sing (r @@ a) b). +data instance Sing (Sigma p r) (x :: Sigma p r) :: Type where + SSigma :: forall (p :: Type) (r :: TyArr p Type -> Type) + (a :: p) (b :: r @@ a) + (sp :: Sing Type p) (sr :: Sing (TyArr p Type -> Type) r) + (sa :: Sing p a) (sb :: Sing (r @@ a) b). Sing (Sing (r @@ a) b) sb -> Sing (Sigma p r) ('Sigma sp sr sa sb) diff --git a/testsuite/tests/dependent/should_compile/Rae31.hs b/testsuite/tests/dependent/should_compile/Rae31.hs index cedc019cf3..7a50b606ee 100644 --- a/testsuite/tests/dependent/should_compile/Rae31.hs +++ b/testsuite/tests/dependent/should_compile/Rae31.hs @@ -1,24 +1,27 @@ {-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds, - TypeFamilies, TypeInType #-} + TypeFamilies #-} module A where import Data.Kind -data family Sing (k :: *) :: k -> * +data family Sing (k :: Type) :: k -> Type type Sing' (x :: k) = Sing k x -data TyFun' (a :: *) (b :: *) :: * -type TyFun (a :: *) (b :: *) = TyFun' a b -> * +data TyFun' (a :: Type) (b :: Type) :: Type +type TyFun (a :: Type) (b :: Type) = TyFun' a b -> Type type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2 -data TyPi' (a :: *) (b :: TyFun a *) :: * -type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> * +data TyPi' (a :: Type) (b :: TyFun a Type) :: Type +type TyPi (a :: Type) (b :: TyFun a Type) = TyPi' a b -> Type type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b $(return []) -data A (a :: *) (b :: a) (c :: TyFun' a *) -- A :: forall a -> a -> a ~> * -type instance (@@) (A a b) c = * +data A (a :: Type) (b :: a) (c :: TyFun' a Type) + -- A :: forall a -> a -> a ~> Type +type instance (@@) (A a b) c = Type $(return []) -data B (a :: *) (b :: TyFun' a *) -- B :: forall a -> a ~> * +data B (a :: Type) (b :: TyFun' a Type) + -- B :: forall a -> a ~> Type type instance (@@) (B a) b = TyPi a (A a b) $(return []) -data C (a :: *) (b :: TyPi a (B a)) (c :: a) (d :: a) (e :: TyFun' (b @@@ c @@@ d) *) +data C (a :: Type) (b :: TyPi a (B a)) (c :: a) (d :: a) + (e :: TyFun' (b @@@ c @@@ d) Type) diff --git a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs index e99c7b5dd5..b048a49e44 100644 --- a/testsuite/tests/dependent/should_compile/RaeBlogPost.hs +++ b/testsuite/tests/dependent/should_compile/RaeBlogPost.hs @@ -1,5 +1,4 @@ -{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies, - TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-} {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-} module RaeBlogPost where @@ -8,7 +7,7 @@ import Data.Kind -- a Proxy type with an explicit kind data Proxy k (a :: k) = P -prox :: Proxy * Bool +prox :: Proxy Type Bool prox = P prox2 :: Proxy Bool 'True @@ -16,11 +15,11 @@ prox2 = P -- implicit kinds still work data A -data B :: A -> * -data C :: B a -> * -data D :: C b -> * -data E :: D c -> * --- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> * +data B :: A -> Type +data C :: B a -> Type +data D :: C b -> Type +data E :: D c -> Type +-- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> Type -- a kind-indexed GADT data TypeRep (a :: k) where @@ -37,7 +36,7 @@ type family a + b where 'Zero + b = b ('Succ a) + b = 'Succ (a + b) -data Vec :: * -> Nat -> * where +data Vec :: Type -> Nat -> Type where Nil :: Vec a 'Zero (:>) :: a -> Vec a n -> Vec a ('Succ n) infixr 5 :> @@ -47,17 +46,17 @@ type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where 'Nil ++ y = y (h ':> t) ++ y = h ':> (t ++ y) --- datatype that mentions * -data U = Star (*) +-- datatype that mentions Type +data U = Star (Type) | Bool Bool -- kind synonym -type Monadish = * -> * +type Monadish = Type -> Type class MonadTrans (t :: Monadish -> Monadish) where lift :: Monad m => m a -> t m a data Free :: Monadish where Return :: a -> Free a Bind :: Free a -> (a -> Free b) -> Free b --- yes, * really does have type *. -type Star = (* :: (* :: (* :: *))) +-- yes, Type really does have type Type. +type Star = (Type :: (Type :: (Type :: Type))) diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs index 480db090c3..1a22573109 100644 --- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs +++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs @@ -3,7 +3,7 @@ {-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes, ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies, - TypeInType, ConstraintKinds, UndecidableInstances, + DataKinds, PolyKinds , ConstraintKinds, UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, StandaloneDeriving, InstanceSigs, RankNTypes, UndecidableSuperClasses #-} diff --git a/testsuite/tests/dependent/should_compile/T11405.hs b/testsuite/tests/dependent/should_compile/T11405.hs index cdb713f118..5fdd7baed1 100644 --- a/testsuite/tests/dependent/should_compile/T11405.hs +++ b/testsuite/tests/dependent/should_compile/T11405.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ImplicitParams, TypeInType, ExplicitForAll #-} +{-# LANGUAGE ImplicitParams, PolyKinds, ExplicitForAll #-} module T11405 where diff --git a/testsuite/tests/dependent/should_compile/T11635.hs b/testsuite/tests/dependent/should_compile/T11635.hs index 2292def966..61d9978e55 100644 --- a/testsuite/tests/dependent/should_compile/T11635.hs +++ b/testsuite/tests/dependent/should_compile/T11635.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll, RankNTypes #-} +{-# LANGUAGE PolyKinds, KindSignatures, ExplicitForAll, RankNTypes #-} module T11635 where diff --git a/testsuite/tests/dependent/should_compile/T11711.hs b/testsuite/tests/dependent/should_compile/T11711.hs index 0cd4dceb42..814b2a4a68 100644 --- a/testsuite/tests/dependent/should_compile/T11711.hs +++ b/testsuite/tests/dependent/should_compile/T11711.hs @@ -5,7 +5,6 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} diff --git a/testsuite/tests/dependent/should_compile/T11719.hs b/testsuite/tests/dependent/should_compile/T11719.hs index ba4d7c9db4..e4c2a89bf2 100644 --- a/testsuite/tests/dependent/should_compile/T11719.hs +++ b/testsuite/tests/dependent/should_compile/T11719.hs @@ -1,12 +1,12 @@ -{-# LANGUAGE RankNTypes, TypeFamilies, TypeInType, TypeOperators, +{-# LANGUAGE RankNTypes, TypeFamilies, TypeOperators, DataKinds, PolyKinds, UndecidableInstances #-} module T11719 where import Data.Kind -data TyFun :: * -> * -> * -type a ~> b = TyFun a b -> * +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type type family (f :: a ~> b) @@ (x :: a) :: b diff --git a/testsuite/tests/dependent/should_compile/T11966.hs b/testsuite/tests/dependent/should_compile/T11966.hs index 0262a0aed3..daad450f13 100644 --- a/testsuite/tests/dependent/should_compile/T11966.hs +++ b/testsuite/tests/dependent/should_compile/T11966.hs @@ -3,7 +3,6 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module T11966 where diff --git a/testsuite/tests/dependent/should_compile/T12176.hs b/testsuite/tests/dependent/should_compile/T12176.hs index 0e340068a7..a11c151567 100644 --- a/testsuite/tests/dependent/should_compile/T12176.hs +++ b/testsuite/tests/dependent/should_compile/T12176.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, TypeInType, GADTs, TypeFamilies #-} +{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies #-} module T12176 where diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs index f9dbf0a486..c76dfb962e 100644 --- a/testsuite/tests/dependent/should_compile/T12442.hs +++ b/testsuite/tests/dependent/should_compile/T12442.hs @@ -1,7 +1,7 @@ -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr -{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, TypeApplications, - GADTs, TypeFamilies, AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators, + TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes #-} module T12442 where diff --git a/testsuite/tests/dependent/should_compile/T12742.hs b/testsuite/tests/dependent/should_compile/T12742.hs index baa3e2c071..988d7c318a 100644 --- a/testsuite/tests/dependent/should_compile/T12742.hs +++ b/testsuite/tests/dependent/should_compile/T12742.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-} +{-# LANGUAGE DataKinds, PolyKinds, RankNTypes, TypeFamilies #-} module T12742 where diff --git a/testsuite/tests/dependent/should_compile/T13910.hs b/testsuite/tests/dependent/should_compile/T13910.hs index 82d47e45bc..b3707dd365 100644 --- a/testsuite/tests/dependent/should_compile/T13910.hs +++ b/testsuite/tests/dependent/should_compile/T13910.hs @@ -7,7 +7,8 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilyDependencies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} module T13910 where @@ -17,7 +18,7 @@ import Data.Type.Equality data family Sing (a :: k) class SingKind k where - type Demote k = (r :: *) | r -> k + type Demote k = (r :: Type) | r -> k fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k @@ -33,8 +34,8 @@ withSomeSing x f = case toSing x of SomeSing x' -> f x' -data TyFun :: * -> * -> * -type a ~> b = TyFun a b -> * +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs index dd4f3d6c7c..1ce77d194f 100644 --- a/testsuite/tests/dependent/should_compile/T13938.hs +++ b/testsuite/tests/dependent/should_compile/T13938.hs @@ -4,7 +4,8 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module T13938 where diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs index 3a09292922..5197747e87 100644 --- a/testsuite/tests/dependent/should_compile/T13938a.hs +++ b/testsuite/tests/dependent/should_compile/T13938a.hs @@ -7,7 +7,8 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} module T13938a where diff --git a/testsuite/tests/dependent/should_compile/T14038.hs b/testsuite/tests/dependent/should_compile/T14038.hs index 839220a0ce..04b24b9f9e 100644 --- a/testsuite/tests/dependent/should_compile/T14038.hs +++ b/testsuite/tests/dependent/should_compile/T14038.hs @@ -6,7 +6,8 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} module T14038 where diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs index e1a6255520..30b203d31b 100644 --- a/testsuite/tests/dependent/should_compile/T14066a.hs +++ b/testsuite/tests/dependent/should_compile/T14066a.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, TypeInType, ExplicitForAll, GADTs, +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs, UndecidableInstances, RankNTypes, ScopedTypeVariables #-} module T14066a where diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs index eebbdca888..133a9e6a44 100644 --- a/testsuite/tests/dependent/should_compile/T14556.hs +++ b/testsuite/tests/dependent/should_compile/T14556.hs @@ -1,4 +1,5 @@ -{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} +{-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds, + TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} module T14556 where diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs index c26a184689..0f053756f5 100644 --- a/testsuite/tests/dependent/should_compile/T14720.hs +++ b/testsuite/tests/dependent/should_compile/T14720.hs @@ -3,7 +3,8 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} module T14720 where diff --git a/testsuite/tests/dependent/should_compile/T14749.hs b/testsuite/tests/dependent/should_compile/T14749.hs index 79bcce66ff..c4480fad0f 100644 --- a/testsuite/tests/dependent/should_compile/T14749.hs +++ b/testsuite/tests/dependent/should_compile/T14749.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-} +{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, PolyKinds #-} module T14749 where diff --git a/testsuite/tests/dependent/should_compile/T14991.hs b/testsuite/tests/dependent/should_compile/T14991.hs index f435c37690..b2f5642ec5 100644 --- a/testsuite/tests/dependent/should_compile/T14991.hs +++ b/testsuite/tests/dependent/should_compile/T14991.hs @@ -1,5 +1,6 @@ {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module T14991 where diff --git a/testsuite/tests/dependent/should_compile/T9632.hs b/testsuite/tests/dependent/should_compile/T9632.hs index bea468fff3..f2099aa22b 100644 --- a/testsuite/tests/dependent/should_compile/T9632.hs +++ b/testsuite/tests/dependent/should_compile/T9632.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T9632 where diff --git a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs index 19f605c8cd..0e2f0c7744 100644 --- a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs +++ b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, UnicodeSyntax, GADTs, NoImplicitPrelude, +{-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude, TypeOperators, TypeFamilies #-} {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index e153cafe41..40ba2110f9 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -48,3 +48,4 @@ test('T14720', normal, compile, ['']) test('T14066a', normal, compile, ['']) test('T14749', normal, compile, ['']) test('T14991', normal, compile, ['']) +test('DkNameRes', normal, compile, [''])
\ No newline at end of file diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs index 1aa4ee54d9..2c284cfeea 100644 --- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs +++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs @@ -7,7 +7,7 @@ Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -} {-# LANGUAGE RankNTypes, PolyKinds, TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances, UndecidableInstances, RebindableSyntax, - DataKinds, MagicHash, AutoDeriveTypeable, TypeInType #-} + DataKinds, MagicHash, AutoDeriveTypeable #-} {-# OPTIONS_GHC -Wno-missing-methods -Wno-redundant-constraints #-} {-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} -- Because we define a local Typeable class and have @@ -127,7 +127,7 @@ gcast x = do Refl <- eqT (typeRep :: TypeRep a) (typeRep :: TypeRep b) return x -data SameKind :: k -> k -> * +data SameKind :: k -> k -> Type type CheckAppResult = SameKind AppResult AppResultNoKind -- not the most thorough check foo :: AppResult x -> AppResultNoKind x @@ -170,17 +170,20 @@ dynFst :: Dynamic -> Maybe Dynamic dynFst (Dyn (rpab :: TypeRep pab) (x :: pab)) = do App (rpa :: TypeRep pa ) (rb :: TypeRep b) <- splitApp rpab - -- introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2| + -- introduces kind |k2|, and types |pa :: k2 -> Type|, |b :: k2| App (rp :: TypeRep p ) (ra :: TypeRep a) <- splitApp rpa - -- introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1| + -- introduces kind |k1|, and types |p :: k1 -> k2 -> Type|, + -- |a :: k1| Refl <- eqT rp (typeRep :: TypeRep (,)) - -- introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)| + -- introduces |p ~ (,)| and + -- |(k1 -> k2 -> Type) ~ (Type -> Type -> Type)| return (Dyn ra (fst x)) -eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b) +eqT :: forall k1 k2 (a :: k1) (b :: k2). + TypeRep a -> TypeRep b -> Maybe (a :~: b) data (a :: k1) :~: (b :: k2) where Refl :: forall k (a :: k). a :~: a @@ -201,11 +204,13 @@ data SomeTypeRep where type TyMapLessTyped = Map SomeTypeRep Dynamic -insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped -insertLessTyped x = Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x) +insertLessTyped :: forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped +insertLessTyped x + = Map.insert (SomeTypeRep (typeRep :: TypeRep a)) (toDynamic x) -lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a -lookupLessTyped = fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a)) +lookupLessTyped :: forall a. Typeable a => TyMapLessTyped -> Maybe a +lookupLessTyped + = fromDynamic <=< Map.lookup (SomeTypeRep (typeRep :: TypeRep a)) instance Ord SomeTypeRep where compare (SomeTypeRep tr1) (SomeTypeRep tr2) = compareTypeRep tr1 tr2 @@ -329,7 +334,7 @@ dynApplyOld (DynOld trf f) (DynOld trx x) = data DynamicClosed where DynClosed :: TypeRepClosed a -> a -> DynamicClosed -data TypeRepClosed (a :: *) where +data TypeRepClosed (a :: Type) where TBool :: TypeRepClosed Bool TFun :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b) TProd :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b) diff --git a/testsuite/tests/dependent/should_compile/mkGADTVars.hs b/testsuite/tests/dependent/should_compile/mkGADTVars.hs index 1e74c6980a..9b48e8c395 100644 --- a/testsuite/tests/dependent/should_compile/mkGADTVars.hs +++ b/testsuite/tests/dependent/should_compile/mkGADTVars.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE GADTs, TypeInType #-} +{-# LANGUAGE GADTs, PolyKinds #-} module GADTVars where diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.hs b/testsuite/tests/dependent/should_fail/BadTelescope.hs index acabffec54..11b52f36e2 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope.hs +++ b/testsuite/tests/dependent/should_fail/BadTelescope.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module BadTelescope where diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs index 6237df4488..b12adbd8e3 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs +++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, ExplicitForAll #-} +{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-} module BadTelescope2 where diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.hs b/testsuite/tests/dependent/should_fail/BadTelescope3.hs index 807479f634..470f5fb9fe 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope3.hs +++ b/testsuite/tests/dependent/should_fail/BadTelescope3.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, ExplicitForAll #-} +{-# LANGUAGE PolyKinds, ExplicitForAll #-} module BadTelescope3 where diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.hs b/testsuite/tests/dependent/should_fail/BadTelescope4.hs index 566922a4a0..bdaf674c2f 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope4.hs +++ b/testsuite/tests/dependent/should_fail/BadTelescope4.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ExistentialQuantification, TypeInType #-} +{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds #-} module BadTelescope4 where import Data.Proxy diff --git a/testsuite/tests/dependent/should_fail/DepFail1.hs b/testsuite/tests/dependent/should_fail/DepFail1.hs index 425a8159c4..26e5d46832 100644 --- a/testsuite/tests/dependent/should_fail/DepFail1.hs +++ b/testsuite/tests/dependent/should_fail/DepFail1.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} module DepFail1 where diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_fail/InferDependency.hs index 47957d47d6..c2bec19d44 100644 --- a/testsuite/tests/dependent/should_fail/InferDependency.hs +++ b/testsuite/tests/dependent/should_fail/InferDependency.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} module InferDependency where diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.hs b/testsuite/tests/dependent/should_fail/KindLevelsB.hs deleted file mode 100644 index 80762978b2..0000000000 --- a/testsuite/tests/dependent/should_fail/KindLevelsB.hs +++ /dev/null @@ -1,9 +0,0 @@ -{-# LANGUAGE DataKinds, PolyKinds #-} - -module KindLevels where - -data A -data B :: A -> * -data C :: B a -> * -data D :: C b -> * -data E :: D c -> * diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr b/testsuite/tests/dependent/should_fail/KindLevelsB.stderr deleted file mode 100644 index 587eb97bfa..0000000000 --- a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr +++ /dev/null @@ -1,5 +0,0 @@ - -KindLevelsB.hs:7:13: error: - • Expected kind ‘A’, but ‘a’ has kind ‘*’ - • In the first argument of ‘B’, namely ‘a’ - In the kind ‘B a -> *’ diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.hs b/testsuite/tests/dependent/should_fail/PromotedClass.hs index 6c3f415e5d..53d581015d 100644 --- a/testsuite/tests/dependent/should_fail/PromotedClass.hs +++ b/testsuite/tests/dependent/should_fail/PromotedClass.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType, GADTs #-} +{-# LANGUAGE DataKinds, GADTs #-} module PromotedClass where diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.hs b/testsuite/tests/dependent/should_fail/RAE_T32a.hs index 08a4ad78a8..d71b863f02 100644 --- a/testsuite/tests/dependent/should_fail/RAE_T32a.hs +++ b/testsuite/tests/dependent/should_fail/RAE_T32a.hs @@ -1,34 +1,36 @@ {-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds, - PolyKinds, TypeFamilies, GADTs, TypeInType #-} + PolyKinds, TypeFamilies, GADTs #-} module RAE_T32a where import Data.Kind -data family Sing (k :: *) :: k -> * +data family Sing (k :: Type) :: k -> Type -data TyArr' (a :: *) (b :: *) :: * -type TyArr (a :: *) (b :: *) = TyArr' a b -> * +data TyArr' (a :: Type) (b :: Type) :: Type +type TyArr (a :: Type) (b :: Type) = TyArr' a b -> Type type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2 -data TyPi' (a :: *) (b :: TyArr a *) :: * -type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> * +data TyPi' (a :: Type) (b :: TyArr a Type) :: Type +type TyPi (a :: Type) (b :: TyArr a Type) = TyPi' a b -> Type type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b $(return []) -data MkStar (p :: *) (x :: TyArr' p *) -type instance MkStar p @@ x = * +data MkStar (p :: Type) (x :: TyArr' p Type) +type instance MkStar p @@ x = Type $(return []) -data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where +data Sigma (p :: Type) (r :: TyPi p (MkStar p)) :: Type where Sigma :: - forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a). - Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b -> Sigma p r + forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a). + Sing Type p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> + Sing (r @@@ a) b -> Sigma p r $(return []) data instance Sing Sigma (Sigma p r) x where SSigma :: - forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a) - (sp :: Sing * p) (sr :: Sing (TyPi p (MkStar p)) r) (sa :: Sing p a) (sb :: Sing (r @@@ a) b). + forall (p :: Type) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a) + (sp :: Sing Type p) (sr :: Sing (TyPi p (MkStar p)) r) + (sa :: Sing p a) (sb :: Sing (r @@@ a) b). Sing (Sing (r @@@ a) b) sb -> Sing (Sigma p r) ('Sigma sp sr sa sb) diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr index 046a1e1aa4..41f5d7cd4c 100644 --- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr +++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr @@ -1,10 +1,10 @@ -RAE_T32a.hs:28:1: error: +RAE_T32a.hs:29:1: error: • Expected kind ‘k0 -> *’, but ‘Sing Sigma (Sigma p r)’ has kind ‘*’ • In the data instance declaration for ‘Sing’ -RAE_T32a.hs:28:20: error: +RAE_T32a.hs:29:20: error: • Expecting two more arguments to ‘Sigma’ Expected a type, but ‘Sigma’ has kind @@ -12,7 +12,7 @@ RAE_T32a.hs:28:20: error: • In the first argument of ‘Sing’, namely ‘Sigma’ In the data instance declaration for ‘Sing’ -RAE_T32a.hs:28:27: error: +RAE_T32a.hs:29:27: error: • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’ • In the second argument of ‘Sing’, namely ‘(Sigma p r)’ In the data instance declaration for ‘Sing’ diff --git a/testsuite/tests/dependent/should_fail/RenamingStar.hs b/testsuite/tests/dependent/should_fail/RenamingStar.hs index 255021c8d9..f9344b0fd9 100644 --- a/testsuite/tests/dependent/should_fail/RenamingStar.hs +++ b/testsuite/tests/dependent/should_fail/RenamingStar.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE KindSignatures, NoStarIsType #-} module RenamingStar where diff --git a/testsuite/tests/dependent/should_fail/RenamingStar.stderr b/testsuite/tests/dependent/should_fail/RenamingStar.stderr index 5efda699fd..4001811f1f 100644 --- a/testsuite/tests/dependent/should_fail/RenamingStar.stderr +++ b/testsuite/tests/dependent/should_fail/RenamingStar.stderr @@ -1,11 +1,5 @@ RenamingStar.hs:5:13: error: - Not in scope: type constructor or class ‘*’ - NB: With TypeInType, you must import * from Data.Kind - -RenamingStar.hs:5:13: error: - Illegal operator ‘*’ in type ‘*’ - Use TypeOperators to allow operators in types - -RenamingStar.hs:5:13: error: Operator applied to too few arguments: * + With NoStarIsType, ‘*’ is treated as a regular type operator. + Did you mean to use ‘Type’ from Data.Kind instead? diff --git a/testsuite/tests/dependent/should_fail/SelfDep.hs b/testsuite/tests/dependent/should_fail/SelfDep.hs index f54b92752b..22ac9ede98 100644 --- a/testsuite/tests/dependent/should_fail/SelfDep.hs +++ b/testsuite/tests/dependent/should_fail/SelfDep.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE KindSignatures #-} + module SelfDep where data T :: T -> * diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr index f4014f7277..8ac4be8c0c 100644 --- a/testsuite/tests/dependent/should_fail/SelfDep.stderr +++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr @@ -1,5 +1,5 @@ -SelfDep.hs:3:11: error: - Type constructor ‘T’ cannot be used here - (it is defined and used in the same recursive group) - In the kind ‘T -> *’ +SelfDep.hs:5:11: error: + • Type constructor ‘T’ cannot be used here + (it is defined and used in the same recursive group) + • In the kind ‘T -> *’ diff --git a/testsuite/tests/dependent/should_fail/T11407.hs b/testsuite/tests/dependent/should_fail/T11407.hs index 533870f94b..e94eaba1e7 100644 --- a/testsuite/tests/dependent/should_fail/T11407.hs +++ b/testsuite/tests/dependent/should_fail/T11407.hs @@ -1,5 +1,5 @@ {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T11407 where import Data.Kind diff --git a/testsuite/tests/dependent/should_fail/T11473.hs b/testsuite/tests/dependent/should_fail/T11473.hs index 12d95caac6..ebfeeb8a13 100644 --- a/testsuite/tests/dependent/should_fail/T11473.hs +++ b/testsuite/tests/dependent/should_fail/T11473.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, TypeInType, RankNTypes #-} +{-# LANGUAGE PolyKinds, TypeFamilies, MagicHash, DataKinds, RankNTypes #-} module T11473 where diff --git a/testsuite/tests/dependent/should_fail/T12081.hs b/testsuite/tests/dependent/should_fail/T12081.hs index f68de420cb..0bf03b1950 100644 --- a/testsuite/tests/dependent/should_fail/T12081.hs +++ b/testsuite/tests/dependent/should_fail/T12081.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T12081 where diff --git a/testsuite/tests/dependent/should_fail/T12174.hs b/testsuite/tests/dependent/should_fail/T12174.hs index 29064d6a96..800759d690 100644 --- a/testsuite/tests/dependent/should_fail/T12174.hs +++ b/testsuite/tests/dependent/should_fail/T12174.hs @@ -1,7 +1,7 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeInType #-} module T12174 where data V a diff --git a/testsuite/tests/dependent/should_fail/T13135.hs b/testsuite/tests/dependent/should_fail/T13135.hs index 772ac78bfa..8f78ccbfb1 100644 --- a/testsuite/tests/dependent/should_fail/T13135.hs +++ b/testsuite/tests/dependent/should_fail/T13135.hs @@ -8,11 +8,11 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} -{-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeFamilyDependencies #-} -module T12135 where + +module T13135 where import Data.Kind (Type) diff --git a/testsuite/tests/dependent/should_fail/T13601.hs b/testsuite/tests/dependent/should_fail/T13601.hs index 5e98c7a657..a8fa34d4a0 100644 --- a/testsuite/tests/dependent/should_fail/T13601.hs +++ b/testsuite/tests/dependent/should_fail/T13601.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, DataKinds, TypeInType #-} +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} import GHC.Exts import Prelude (Bool(True,False),Integer,Ordering,undefined) diff --git a/testsuite/tests/dependent/should_fail/T13780a.hs b/testsuite/tests/dependent/should_fail/T13780a.hs index 1f7c95c40a..b7e1510672 100644 --- a/testsuite/tests/dependent/should_fail/T13780a.hs +++ b/testsuite/tests/dependent/should_fail/T13780a.hs @@ -1,6 +1,6 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T13780a where data family Sing (a :: k) diff --git a/testsuite/tests/dependent/should_fail/T13780b.hs b/testsuite/tests/dependent/should_fail/T13780b.hs index 238e7a1af9..dc6ac89c08 100644 --- a/testsuite/tests/dependent/should_fail/T13780b.hs +++ b/testsuite/tests/dependent/should_fail/T13780b.hs @@ -1,6 +1,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} module T13780b where data family Sing (a :: k) diff --git a/testsuite/tests/dependent/should_fail/T13780c.hs b/testsuite/tests/dependent/should_fail/T13780c.hs index eee6436237..78e09f5ef1 100644 --- a/testsuite/tests/dependent/should_fail/T13780c.hs +++ b/testsuite/tests/dependent/should_fail/T13780c.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T13780c where import Data.Kind diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr index 065c700dfc..9a196f4bd7 100644 --- a/testsuite/tests/dependent/should_fail/T13780c.stderr +++ b/testsuite/tests/dependent/should_fail/T13780c.stderr @@ -2,11 +2,13 @@ [2 of 2] Compiling T13780c ( T13780c.hs, T13780c.o ) T13780c.hs:11:16: error: - • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’ + • Data constructor ‘SFalse’ cannot be used here + (it comes from a data family instance) • In the third argument of ‘ElimBool’, namely ‘SFalse’ In the type family declaration for ‘ElimBool’ T13780c.hs:12:16: error: - • Expected kind ‘Sing _1’, but ‘STrue’ has kind ‘Sing 'True’ + • Data constructor ‘STrue’ cannot be used here + (it comes from a data family instance) • In the third argument of ‘ElimBool’, namely ‘STrue’ In the type family declaration for ‘ElimBool’ diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs index 58396df591..709d507a34 100644 --- a/testsuite/tests/dependent/should_fail/T14066.hs +++ b/testsuite/tests/dependent/should_fail/T14066.hs @@ -1,7 +1,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PolyKinds #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE KindSignatures #-} + + module T14066 where diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs index b4597d2cec..4dd6f41973 100644 --- a/testsuite/tests/dependent/should_fail/T14066c.hs +++ b/testsuite/tests/dependent/should_fail/T14066c.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-} +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, UndecidableInstances #-} module T14066c where diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs index ea47644688..dd5676826d 100644 --- a/testsuite/tests/dependent/should_fail/T14066d.hs +++ b/testsuite/tests/dependent/should_fail/T14066d.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-} +{-# LANGUAGE RankNTypes, ScopedTypeVariables, PolyKinds #-} module T14066d where diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs index 9b799e542c..9bce332527 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.hs +++ b/testsuite/tests/dependent/should_fail/T14066e.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-} +{-# LANGUAGE MonoLocalBinds, PolyKinds, ScopedTypeVariables #-} module T14066e where diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs index ccb7ceac0e..b2035f2c3d 100644 --- a/testsuite/tests/dependent/should_fail/T14066f.hs +++ b/testsuite/tests/dependent/should_fail/T14066f.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} module T14066f where diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs index df0e03b173..b07a2c36a9 100644 --- a/testsuite/tests/dependent/should_fail/T14066g.hs +++ b/testsuite/tests/dependent/should_fail/T14066g.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE DataKinds, PolyKinds #-} module T14066g where diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs index 7e7ecd31c9..a20ae30958 100644 --- a/testsuite/tests/dependent/should_fail/T14066h.hs +++ b/testsuite/tests/dependent/should_fail/T14066h.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-} +{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-} module T14066h where diff --git a/testsuite/tests/dependent/should_fail/T15245.hs b/testsuite/tests/dependent/should_fail/T15245.hs new file mode 100644 index 0000000000..86d9c221e0 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15245.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeApplications #-} + +module T15245 where + +import Type.Reflection + +data family K +data instance K = MkK + +main = print (typeRep @'MkK) diff --git a/testsuite/tests/dependent/should_fail/T15245.stderr b/testsuite/tests/dependent/should_fail/T15245.stderr new file mode 100644 index 0000000000..b41076636f --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15245.stderr @@ -0,0 +1,7 @@ + +T15245.hs:10:24: error: + • Data constructor ‘MkK’ cannot be used here + (it comes from a data family instance) + • In the type ‘ 'MkK’ + In the first argument of ‘print’, namely ‘(typeRep @ 'MkK)’ + In the expression: print (typeRep @ 'MkK) diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs index 02b7737499..1f958de426 100644 --- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs +++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-} +{-# LANGUAGE RankNTypes, PolyKinds #-} -- NB: -fprint-explicit-runtime-reps enabled in all.T module TypeSkolEscape where diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 7273445548..5ae037dc54 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, ['']) test('RenamingStar', normal, compile_fail, ['']) test('T11407', normal, compile_fail, ['']) test('T11334b', normal, compile_fail, ['']) -test('KindLevelsB', normal, compile_fail, ['']) test('T11473', normal, compile_fail, ['']) test('T11471', normal, compile_fail, ['']) test('T12174', normal, compile_fail, ['']) @@ -28,3 +27,4 @@ test('T14066f', normal, compile_fail, ['']) test('T14066g', normal, compile_fail, ['']) test('T14066h', normal, compile_fail, ['']) test('InferDependency', normal, compile_fail, ['']) +test('T15245', normal, compile_fail, ['']) diff --git a/testsuite/tests/dependent/should_run/T11964a.hs b/testsuite/tests/dependent/should_run/T11964a.hs index f0576542b6..2c6993fef0 100644 --- a/testsuite/tests/dependent/should_run/T11964a.hs +++ b/testsuite/tests/dependent/should_run/T11964a.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds #-} module T11964a where import Data.Kind type Star = Type |