Test kind inference for closed type families/T7939.
authorRichard Eisenberg <eir@cis.upenn.edu>
Wed, 26 Jun 2013 16:19:42 +0000 (17:19 +0100)
committerRichard Eisenberg <eir@cis.upenn.edu>
Thu, 27 Jun 2013 12:28:44 +0000 (13:28 +0100)
testsuite/tests/ghci/scripts/T7939.hs
testsuite/tests/ghci/scripts/T7939.script
testsuite/tests/ghci/scripts/T7939.stdout
testsuite/tests/indexed-types/should_compile/T7585.hs
testsuite/tests/polykinds/T7020.hs
testsuite/tests/polykinds/T7939a.hs [new file with mode: 0644]
testsuite/tests/polykinds/T7939a.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index ead42d9..93b9016 100644 (file)
@@ -1,8 +1,27 @@
-{-# LANGUAGE TypeFamilies, PolyKinds #-}
+{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators #-}
 
 module T7939 where
 
 class Foo a where
-   type Bar a
+   type Bar a b
 
+type family F a
+type instance F Int = Bool
 
+type family G a where
+  G Int = Bool
+
+type family H a where
+  H False = True
+
+type family J a where
+  J '[] = False
+  J (h ': t) = True
+
+type family K a where
+  K '[] = Nothing
+  K (h ': t) = Just h
+
+type family L (a :: k) b :: k where
+  L Int Int = Bool
+  L Maybe Bool = IO
\ No newline at end of file
index 03470e8..920a3ba 100644 (file)
@@ -1,3 +1,13 @@
 :l T7939
 :i Bar
 :k Bar
+:i F
+:k F
+:i G
+:k G
+:i H
+:k H
+:i J
+:k J
+:i K
+:k K
\ No newline at end of file
index c62de9b..9a01bac 100644 (file)
@@ -1,4 +1,23 @@
 class Foo (k :: BOX) (a :: k) where
-  type family Bar (k :: BOX) (k :: BOX) (a :: k) :: k
+  type family Bar (k :: BOX) (a :: k) b :: *
        -- Defined at T7939.hs:6:9
-Bar :: k1 -> k
+Bar :: k -> * -> *
+type family F a :: *   -- Defined at T7939.hs:8:13
+type instance F Int -- Defined at T7939.hs:9:1
+F :: * -> *
+type family G a :: * where G Int = Bool
+       -- Defined at T7939.hs:11:13
+G :: * -> *
+type family H (a :: Bool) :: Bool where H 'False = 'True
+       -- Defined at T7939.hs:14:13
+H :: Bool -> Bool
+type family J (k :: BOX) (a :: [k]) :: Bool where
+    J k ('[] k) = 'False
+    J k ((':) k h t) = 'True
+       -- Defined at T7939.hs:17:13
+J :: [k] -> Bool
+type family K (k :: BOX) (a :: [k]) :: Maybe k where
+    K k ('[] k) = 'Nothing k
+    K k ((':) k h t) = 'Just k h
+       -- Defined at T7939.hs:21:13
+K :: [k] -> Maybe k
index 93a85b6..a21c04d 100644 (file)
@@ -11,7 +11,7 @@ data SList :: [Bool] -> * where
   SNil :: SList '[]
   SCons :: SBool h -> SList t -> SList (h ': t)
 
-type family (a :: k) :==: (b :: k) :: Bool where
+type family (a :: [k]) :==: (b :: [k]) :: Bool where
   '[] :==: '[] = True
   (h1 ': t1) :==: (h2 ': t2) = True
   a :==: b = False
index b67c1d8..9143583 100644 (file)
@@ -10,7 +10,7 @@ data family Sing (a :: k)
 class SingKind (Any :: k) => SingI (s :: k) where
    sing :: Sing s
 
-data SingInstance :: k -> * where
+data SingInstance (a :: k) where
    SingInstance :: SingI a => SingInstance a
 
 class (b ~ Any) => SingKind (b :: k) where
diff --git a/testsuite/tests/polykinds/T7939a.hs b/testsuite/tests/polykinds/T7939a.hs
new file mode 100644 (file)
index 0000000..1ed2c51
--- /dev/null
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, PolyKinds #-}
+
+module T7939a where
+
+type family F a where
+  F Int = Bool
+  F Maybe = Char
diff --git a/testsuite/tests/polykinds/T7939a.stderr b/testsuite/tests/polykinds/T7939a.stderr
new file mode 100644 (file)
index 0000000..7485eb0
--- /dev/null
@@ -0,0 +1,7 @@
+
+T7939a.hs:7:5:
+    Expecting one more argument to ‛Maybe’
+    The first argument of ‛F’ should have kind ‛*’,
+      but ‛Maybe’ has kind ‛* -> *’
+    In the type ‛Maybe’
+    In the family declaration for ‛F’
index 9ffc682..c69453c 100644 (file)
@@ -88,3 +88,4 @@ test('T7601', normal, compile,[''])
 test('T7805', normal, compile_fail,[''])
 test('T7916', normal, compile,[''])
 test('T7973', normal, compile,['-O'])
+test('T7939a', normal, compile_fail, [''])
\ No newline at end of file