Test kind inference for closed type families/T7939.

tests/ghci/scripts/T7939.hs

@@ -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

tests/ghci/scripts/T7939.script

@@ -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

tests/ghci/scripts/T7939.stdout

@@ -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

tests/indexed-types/should_compile/T7585.hs

@@ -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

tests/polykinds/T7020.hs

@@ -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

tests/polykinds/T7939a.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, PolyKinds #-}
+
+module T7939a where
+
+type family F a where
+  F Int = Bool
+  F Maybe = Char

tests/polykinds/T7939a.stderr

@@ -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’

tests/polykinds/all.T

@@ -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, [''])