Commit 62e48fbc authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Test kind inference for closed type families/T7939.

parent fe2397fe
{-# 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
: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
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
......@@ -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
......
......@@ -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
......
{-# LANGUAGE TypeFamilies, PolyKinds #-}
module T7939a where
type family F a where
F Int = Bool
F Maybe = Char
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’
......@@ -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
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment