diff options
Diffstat (limited to 'testsuite/tests/dependent/should_compile/T14066a.hs')
| -rw-r--r-- | testsuite/tests/dependent/should_compile/T14066a.hs | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs index 1d6b72491e..b743568673 100644 --- a/testsuite/tests/dependent/should_compile/T14066a.hs +++ b/testsuite/tests/dependent/should_compile/T14066a.hs @@ -1,5 +1,6 @@ {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs, - UndecidableInstances, RankNTypes, ScopedTypeVariables #-} + UndecidableInstances, RankNTypes, ScopedTypeVariables, + StandaloneKindSignatures #-} module T14066a where @@ -31,7 +32,8 @@ type family G x a where -- this last example just checks that GADT pattern-matching on kinds still works. -- nothing new here. -data T (a :: k) where +type T :: k -> Type +data T a where MkT :: T (a :: Type -> Type) data S (a :: Type -> Type) where @@ -53,9 +55,12 @@ type P k a = Proxy (a :: k) -- Naively, we don't know about c's kind early enough. data SameKind :: forall k. k -> k -> Type -type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where + +type IfK :: Proxy (j :: Bool) -> m -> n -> If j m n +type family IfK e f g where IfK (_ :: Proxy True) f _ = f IfK (_ :: Proxy False) _ g = g + x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True)) x _ = Proxy |