diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2012-09-18 09:19:33 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2012-09-18 09:19:33 +0100 |
commit | 1f49b82985d42562091b7499c2cdbf2d7ff373f6 (patch) | |
tree | 3ed063342581349ee15999873ef334343528c909 | |
parent | 00922ef98298b13b21e4238531943e8cd3fa971d (diff) | |
download | haskell-1f49b82985d42562091b7499c2cdbf2d7ff373f6.tar.gz |
Test Trac #7224 and #7230
-rw-r--r-- | testsuite/tests/polykinds/T7224.hs | 7 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T7224.stderr | 5 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T7230.hs | 49 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T7230.stderr | 25 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 4 |
5 files changed, 89 insertions, 1 deletions
diff --git a/testsuite/tests/polykinds/T7224.hs b/testsuite/tests/polykinds/T7224.hs new file mode 100644 index 0000000000..a065bc8494 --- /dev/null +++ b/testsuite/tests/polykinds/T7224.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PolyKinds #-} + +module T7224 where + +class PMonad' (m :: i -> i -> * -> *) where + ret' :: a -> m i i a + bind' :: m i j a -> (a -> m j k b) -> m i k b diff --git a/testsuite/tests/polykinds/T7224.stderr b/testsuite/tests/polykinds/T7224.stderr new file mode 100644 index 0000000000..c1508e9b7d --- /dev/null +++ b/testsuite/tests/polykinds/T7224.stderr @@ -0,0 +1,5 @@ + +T7224.hs:6:19: + Kind variable `i' used as a type + In the type `a -> m i i a' + In the class declaration for PMonad' diff --git a/testsuite/tests/polykinds/T7230.hs b/testsuite/tests/polykinds/T7230.hs new file mode 100644 index 0000000000..d3c6a51ae5 --- /dev/null +++ b/testsuite/tests/polykinds/T7230.hs @@ -0,0 +1,49 @@ +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} +{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies #-} +{-# LANGUAGE TypeOperators, UndecidableInstances #-} +module T7230 where + +data Nat = Zero | Succ Nat deriving (Show, Eq, Ord) + +data family Sing (x :: k) + +data instance Sing (n :: Nat) where + SZero :: Sing Zero + SSucc :: Sing n -> Sing (Succ n) + +type SNat (n :: Nat) = Sing n + +data instance Sing (b :: Bool) where + STrue :: Sing True + SFalse :: Sing False + +type SBool (b :: Bool) = Sing b + +data instance Sing (xs :: [k]) where + SNil :: Sing ('[] :: [k]) + SCons :: Sing x -> Sing xs -> Sing (x ': xs) + +type SList (xs :: [k]) = Sing (xs :: [k]) + +type family (:<<=) (n :: Nat) (m :: Nat) :: Bool +type instance Zero :<<= n = True +type instance Succ n :<<= Zero = False +type instance Succ n :<<= Succ m = n :<<= m + +(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m) +SZero %:<<= _ = STrue +SSucc _ %:<<= SZero = SFalse +SSucc n %:<<= SSucc m = n %:<<= m + +type family (b :: Bool) :&& (b' :: Bool) :: Bool +type instance True :&& b = b +type instance False :&& b = False + +type family Increasing (xs :: [Nat]) :: Bool +type instance Increasing '[] = True +type instance Increasing '[n] = True +type instance Increasing (n ': m ': ns) = n :<<= m :&& Increasing (m ': ns) + +crash :: (Increasing xs) ~ True => SList xs -> SBool (Increasing xs) +crash (SCons x (SCons y xs)) = x %:<<= y +crash _ = STrue diff --git a/testsuite/tests/polykinds/T7230.stderr b/testsuite/tests/polykinds/T7230.stderr new file mode 100644 index 0000000000..ee82a2bb19 --- /dev/null +++ b/testsuite/tests/polykinds/T7230.stderr @@ -0,0 +1,25 @@ + +T7230.hs:48:32: + Could not deduce ((x :<<= x1) ~ 'True) + from the context (Increasing xs ~ 'True) + bound by the type signature for + crash :: Increasing xs ~ 'True => + SList Nat xs -> SBool (Increasing xs) + at T7230.hs:47:10-68 + or from (xs ~ (':) Nat x xs1) + bound by a pattern with constructor + SCons :: forall (k :: BOX) (x :: k) (xs :: [k]). + Sing k x -> Sing [k] xs -> Sing [k] ((':) k x xs), + in an equation for `crash' + at T7230.hs:48:8-27 + or from (xs1 ~ (':) Nat x1 xs2) + bound by a pattern with constructor + SCons :: forall (k :: BOX) (x :: k) (xs :: [k]). + Sing k x -> Sing [k] xs -> Sing [k] ((':) k x xs), + in an equation for `crash' + at T7230.hs:48:17-26 + Expected type: SBool (Increasing xs) + Actual type: SBool (x :<<= x1) + In the expression: x %:<<= y + In an equation for `crash': + crash (SCons x (SCons y xs)) = x %:<<= y diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index f2d2532b8d..1ad1b31d63 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -63,6 +63,8 @@ test('T7128', normal, compile,['']) test('T7151', normal, compile_fail,['']) test('T7095', normal, compile,['']) test('T7090', normal, compile,['']) -test('T7176', expect_broken(7176), compile,['']) +test('T7176', normal, compile,['']) +test('T7224', normal, compile_fail,['']) +test('T7230', normal, compile_fail,['']) |