diff options
Diffstat (limited to 'testsuite/tests/dependent/should_compile')
34 files changed, 104 insertions, 85 deletions
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 |