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

Updates to support closed type families.

parent a26bf928
...@@ -17,8 +17,6 @@ instance C Int where ...@@ -17,8 +17,6 @@ instance C Int where
instance C () where instance C () where
type D () () = Bool type D () () = Bool
type family E a type family E a where
type instance where
E () = Bool E () = Bool
E Int = String E Int = String
\ No newline at end of file
type family A a b :: * -- Defined at T4175.hs:4:13 type family A a b :: * -- Defined at T4175.hs:4:13
type instance A (Maybe a) a -- Defined at T4175.hs:6:15 type instance A (Maybe a) a -- Defined at T4175.hs:6:1
type instance A Int Int -- Defined at T4175.hs:5:15 type instance A Int Int -- Defined at T4175.hs:5:1
data family B a -- Defined at T4175.hs:8:13 data family B a -- Defined at T4175.hs:8:13
data instance B () -- Defined at T4175.hs:9:15 data instance B () -- Defined at T4175.hs:9:15
class C a where class C a where
type family D a b :: * type family D a b :: *
-- Defined at T4175.hs:12:10 -- Defined at T4175.hs:12:10
type D () () -- Defined at T4175.hs:18:10 type D () () -- Defined at T4175.hs:18:5
type D Int () -- Defined at T4175.hs:15:10 type D Int () -- Defined at T4175.hs:15:5
type family E a :: * -- Defined at T4175.hs:20:13 type family E a :: * where
type instance where E () = Bool
E () -- Defined at T4175.hs:23:5 E Int = String
E Int -- Defined at T4175.hs:24:5 -- Defined at T4175.hs:20:13
data () = () -- Defined in ‛GHC.Tuple’ data () = () -- Defined in ‛GHC.Tuple’
instance C () -- Defined at T4175.hs:17:10 instance C () -- Defined at T4175.hs:17:10
instance Bounded () -- Defined in ‛GHC.Enum’ instance Bounded () -- Defined in ‛GHC.Enum’
instance Enum () -- Defined in ‛GHC.Enum’ instance Enum () -- Defined in ‛GHC.Enum’
instance Eq () -- Defined in ‛GHC.Classes’ instance Eq () -- Defined in ‛GHC.Classes’
instance Ord () -- Defined in ‛GHC.Classes’ instance Ord () -- Defined in ‛GHC.Classes’
instance Read () -- Defined in ‛GHC.Read’ instance Read () -- Defined in ‛GHC.Read’
instance Show () -- Defined in ‛GHC.Show’ instance Show () -- Defined in ‛GHC.Show’
type instance where type D () () -- Defined at T4175.hs:18:5
E () -- Defined at T4175.hs:23:5 type D Int () -- Defined at T4175.hs:15:5
E Int -- Defined at T4175.hs:24:5 data instance B () -- Defined at T4175.hs:9:15
type D () () -- Defined at T4175.hs:18:10 data Maybe a = Nothing | Just a -- Defined in ‛Data.Maybe’
type D Int () -- Defined at T4175.hs:15:10 instance Eq a => Eq (Maybe a) -- Defined in ‛Data.Maybe’
data instance B () -- Defined at T4175.hs:9:15 instance Monad Maybe -- Defined in ‛Data.Maybe’
data Maybe a = Nothing | Just a -- Defined in ‛Data.Maybe’ instance Functor Maybe -- Defined in ‛Data.Maybe’
instance Eq a => Eq (Maybe a) -- Defined in ‛Data.Maybe’ instance Ord a => Ord (Maybe a) -- Defined in ‛Data.Maybe’
instance Monad Maybe -- Defined in ‛Data.Maybe’ instance Read a => Read (Maybe a) -- Defined in ‛GHC.Read’
instance Functor Maybe -- Defined in ‛Data.Maybe’ instance Show a => Show (Maybe a) -- Defined in ‛GHC.Show’
instance Ord a => Ord (Maybe a) -- Defined in ‛Data.Maybe’ type instance A (Maybe a) a -- Defined at T4175.hs:6:1
instance Read a => Read (Maybe a) -- Defined in ‛GHC.Read’ data Int = GHC.Types.I# GHC.Prim.Int# -- Defined in ‛GHC.Types’
instance Show a => Show (Maybe a) -- Defined in ‛GHC.Show’ instance C Int -- Defined at T4175.hs:14:10
type instance A (Maybe a) a -- Defined at T4175.hs:6:15 instance Bounded Int -- Defined in ‛GHC.Enum’
data Int = GHC.Types.I# GHC.Prim.Int# -- Defined in ‛GHC.Types’ instance Enum Int -- Defined in ‛GHC.Enum’
instance C Int -- Defined at T4175.hs:14:10 instance Eq Int -- Defined in ‛GHC.Classes’
instance Bounded Int -- Defined in ‛GHC.Enum’ instance Integral Int -- Defined in ‛GHC.Real’
instance Enum Int -- Defined in ‛GHC.Enum’ instance Num Int -- Defined in ‛GHC.Num’
instance Eq Int -- Defined in ‛GHC.Classes’ instance Ord Int -- Defined in ‛GHC.Classes’
instance Integral Int -- Defined in ‛GHC.Real’ instance Read Int -- Defined in ‛GHC.Read’
instance Num Int -- Defined in ‛GHC.Num’ instance Real Int -- Defined in ‛GHC.Real’
instance Ord Int -- Defined in ‛GHC.Classes’ instance Show Int -- Defined in ‛GHC.Show’
instance Read Int -- Defined in ‛GHC.Read’ type D Int () -- Defined at T4175.hs:15:5
instance Real Int -- Defined in ‛GHC.Real’ type instance A Int Int -- Defined at T4175.hs:5:1
instance Show Int -- Defined in ‛GHC.Show’
type instance where
E () -- Defined at T4175.hs:23:5
E Int -- Defined at T4175.hs:24:5
type D Int () -- Defined at T4175.hs:15:10
type instance A Int Int -- Defined at T4175.hs:5:15
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap1 where module Overlap1 where
type family F a type family F a where
type instance where
F Int = Int F Int = Int
F a = Bool F a = Bool
......
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap12 where module Overlap12 where
type family And (a :: Bool) (b :: Bool) :: Bool type family And (a :: Bool) (b :: Bool) :: Bool where
type instance where
And False x = False And False x = False
And True x = x And True x = x
And x False = False And x False = False
...@@ -12,5 +11,17 @@ type instance where ...@@ -12,5 +11,17 @@ type instance where
data Proxy p = P data Proxy p = P
i :: Proxy (And False x) a :: Proxy (And False x)
i = (P :: Proxy False) a = (P :: Proxy False)
\ No newline at end of file
b :: Proxy x -> Proxy (And True x)
b x = x
c :: Proxy (And x False)
c = (P :: Proxy False)
d :: Proxy x -> Proxy (And x True)
d x = x
e :: Proxy x -> Proxy (And x x)
e x = x
{-# LANGUAGE TypeFamilies #-}
module Overlap13 where
type family F a b where
F a a = Int
F a Int = Int
F a b = b
g :: a -> F a Int
g x = (5 :: Int)
{-# LANGUAGE TypeFamilies #-}
module Overlap14 where
type family F a b c where
F a a a = Int
F Int b c = Bool
type family G x
foo :: F Int (G Bool) Bool
foo = False
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap2 where module Overlap2 where
type family F a b type family F a b where
type instance where
F a a = Int F a a = Int
F a b = Bool F a b = Bool
......
TYPE SIGNATURES TYPE SIGNATURES
emptyL :: forall a. ListColl a emptyL :: forall a. ListColl a
test2 :: test2 ::
forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c
TYPE CONSTRUCTORS TYPE CONSTRUCTORS
Coll :: * -> Constraint Coll :: * -> Constraint
class Coll c class Coll c
RecFlag NonRecursive RecFlag NonRecursive
type family Elem c :: * type family Elem c :: *
empty :: c insert :: Elem c -> c -> c empty :: c insert :: Elem c -> c -> c
ListColl :: * -> * ListColl :: * -> *
data ListColl a data ListColl a
No C type associated No C type associated
RecFlag NonRecursive, Promotable RecFlag NonRecursive, Promotable
= L :: forall a. [a] -> ListColl a Stricts: _ = L :: forall a. [a] -> ListColl a Stricts: _
FamilyInstance: none FamilyInstance: none
COERCION AXIOMS COERCION AXIOMS
axiom Foo.TFCo:R:ElemListColl :: Elem (ListColl a) = a axiom Foo.TFCo:R:ElemListColl :: Elem (ListColl a) = a
INSTANCES INSTANCES
instance Coll (ListColl a) -- Defined at T3017.hs:12:11 instance Coll (ListColl a) -- Defined at T3017.hs:12:11
FAMILY INSTANCES FAMILY INSTANCES
type Elem (ListColl a) -- Defined at T3017.hs:13:9 type Elem (ListColl a) -- Defined at T3017.hs:13:4
Dependent modules: [] Dependent modules: []
Dependent packages: [base, ghc-prim, integer-gmp] Dependent packages: [base, ghc-prim, integer-gmp]
...@@ -11,8 +11,7 @@ data SList :: [Bool] -> * where ...@@ -11,8 +11,7 @@ data SList :: [Bool] -> * where
SNil :: SList '[] SNil :: SList '[]
SCons :: SBool h -> SList t -> SList (h ': t) SCons :: SBool h -> SList t -> SList (h ': t)
type family (a :: k) :==: (b :: k) :: Bool type family (a :: k) :==: (b :: k) :: Bool where
type instance where
'[] :==: '[] = True '[] :==: '[] = True
(h1 ': t1) :==: (h2 ': t2) = True (h1 ': t1) :==: (h2 ': t2) = True
a :==: b = False a :==: b = False
......
...@@ -200,6 +200,8 @@ test('T7082', normal, compile, ['']) ...@@ -200,6 +200,8 @@ test('T7082', normal, compile, [''])
test('Overlap1', normal, compile, ['']) test('Overlap1', normal, compile, [''])
test('Overlap2', normal, compile, ['']) test('Overlap2', normal, compile, [''])
test('Overlap12', normal, compile, ['']) test('Overlap12', normal, compile, [''])
test('Overlap13', normal, compile, [''])
test('Overlap14', normal, compile, [''])
test('T7156', normal, compile, ['']) test('T7156', normal, compile, [''])
test('T5591a', normal, compile, ['']) test('T5591a', normal, compile, [''])
test('T5591b', normal, compile, ['']) test('T5591b', normal, compile, [''])
......
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilies #-}
module Overlap8 where
type family F a b type family F a b
type instance F a Int = Int type instance F a a = Int
type instance where type instance F [a] a = Bool
F Int a = Int
F a b = Bool
T7560.hs:8:3: NoGood.hs:4:15:
Conflicting family instance declarations: Conflicting family instance declarations:
F Int -- Defined at T7560.hs:8:3 F a a -- Defined at NoGood.hs:4:15
F Int -- Defined at T7560.hs:12:3 F [a] a -- Defined at NoGood.hs:5:15
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap10 where module Overlap10 where
type family F a b type family F a b where
type instance where
F a a = Int F a a = Int
F a b = b F a b = b
......
Overlap10.hs:11:7: Overlap10.hs:10:7:
Couldn't match expected type ‛F a Bool’ with actual type ‛Bool’ Couldn't match expected type ‛F a Bool’ with actual type ‛Bool’
Relevant bindings include Relevant bindings include
g :: a -> F a Bool (bound at Overlap10.hs:11:1) g :: a -> F a Bool (bound at Overlap10.hs:10:1)
x :: a (bound at Overlap10.hs:11:3) x :: a (bound at Overlap10.hs:10:3)
In the expression: False In the expression: False
In an equation for ‛g’: g x = False In an equation for ‛g’: g x = False
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap11 where module Overlap11 where
type family F a b type family F a b where
type instance where
F a a = Int F a a = Int
F a b = b F a b = b
......
Overlap11.hs:11:8: Overlap11.hs:10:8:
Couldn't match expected type ‛F a Int’ with actual type ‛Int’ Couldn't match expected type ‛F a Int’ with actual type ‛Int’
Relevant bindings include Relevant bindings include
g :: a -> F a Int (bound at Overlap11.hs:11:1) g :: a -> F a Int (bound at Overlap11.hs:10:1)
x :: a (bound at Overlap11.hs:11:3) x :: a (bound at Overlap11.hs:10:3)
In the expression: (5 :: Int) In the expression: (5 :: Int)
In an equation for ‛g’: g x = (5 :: Int) In an equation for ‛g’: g x = (5 :: Int)
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap3 where module Overlap3 where
type family F a b type family F a b where
type instance where
F a a = Int F a a = Int
F a b = Bool F a b = Bool
type instance F Char Char = Int type instance F Char Char = Int
......
Overlap3.hs:7:3: Overlap3.hs:8:1:
Conflicting family instance declarations: Illegal instance for closed family ‛F’
F a a -- Defined at Overlap3.hs:7:3 In the type instance declaration for ‛F’
F Char Char -- Defined at Overlap3.hs:9:15
Overlap3.hs:8:3:
Conflicting family instance declarations:
F a b -- Defined at Overlap3.hs:8:3
F Char Char -- Defined at Overlap3.hs:9:15
...@@ -2,15 +2,7 @@ ...@@ -2,15 +2,7 @@
module Overlap4 where module Overlap4 where
type family F a b type family F a b where
type instance F Char Char = Int F Int Int = Bool
type instance where F Bool = Maybe
F a a = Int
F a b = Bool
g :: F Char Double
g = False
h :: F Double Double
h = -2
Overlap4.hs:6:15: Overlap4.hs:7:3:
Conflicting family instance declarations: Number of parameters must match family declaration; expected 2
F Char Char -- Defined at Overlap4.hs:6:15 In the equations for closed type family ‛F’
F a a -- Defined at Overlap4.hs:8:3 In the family declaration for ‛F’
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-} {-# LANGUAGE TypeFamilies #-}
module Overlap5 where module Overlap5 where
type family And (a :: Bool) (b :: Bool) :: Bool type family G a
type instance where type family F a where
And False x = False F Int = Bool
And True x = x G Int = Char
And x False = False F a = Int
And x True = x \ No newline at end of file
And x x = x
data Proxy p = P
g :: Proxy x -> Proxy (And x True)
g x = x
h :: Proxy x -> Proxy (And x x)
h x = x
i :: Proxy x -> Proxy (And False x)
i x = (P :: Proxy False)
\ No newline at end of file
Overlap5.hs:16:7: Overlap5.hs:8:3:
Couldn't match type ‛x’ with ‛And x 'True’ Mismatched type names in closed type family declaration.
‛x’ is a rigid type variable bound by First name was F; this one is G
the type signature for In the family declaration for ‛F’
g :: Proxy Bool x -> Proxy Bool (And x 'True)
at Overlap5.hs:15:6
Expected type: Proxy Bool (And x 'True)
Actual type: Proxy Bool x
Relevant bindings include
g :: Proxy Bool x -> Proxy Bool (And x 'True)
(bound at Overlap5.hs:16:1)
x :: Proxy Bool x (bound at Overlap5.hs:16:3)
In the expression: x
In an equation for ‛g’: g x = x
Overlap5.hs:19:7:
Couldn't match type ‛x’ with ‛And x x’
‛x’ is a rigid type variable bound by
the type signature for h :: Proxy Bool x -> Proxy Bool (And x x)
at Overlap5.hs:18:6
Expected type: Proxy Bool (And x x)
Actual type: Proxy Bool x
Relevant bindings include
h :: Proxy Bool x -> Proxy Bool (And x x)
(bound at Overlap5.hs:19:1)
x :: Proxy Bool x (bound at Overlap5.hs:19:3)
In the expression: x
In an equation for ‛h’: h x = x
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap6 where module Overlap6 where
type family And (a :: Bool) (b :: Bool) :: Bool type family And (a :: Bool) (b :: Bool) :: Bool where
type instance where
And False x = False And False x = False
And True x = False -- this is wrong! And True x = False -- this is wrong!
And x False = False And x False = False
......
Overlap6.hs:16:7: Overlap6.hs:15:7:
Couldn't match type ‛x’ with ‛And x 'True’ Couldn't match type ‛x’ with ‛And x 'True’
‛x’ is a rigid type variable bound by ‛x’ is a rigid type variable bound by
the type signature for the type signature for
g :: Proxy Bool x -> Proxy Bool (And x 'True) g :: Proxy Bool x -> Proxy Bool (And x 'True)
at Overlap6.hs:15:6 at Overlap6.hs:14:6
Expected type: Proxy Bool (And x 'True) Expected type: Proxy Bool (And x 'True)
Actual type: Proxy Bool x Actual type: Proxy Bool x
Relevant bindings include Relevant bindings include
g :: Proxy Bool x -> Proxy Bool (And x 'True) g :: Proxy Bool x -> Proxy Bool (And x 'True)
(bound at Overlap6.hs:16:1) (bound at Overlap6.hs:15:1)
x :: Proxy Bool x (bound at Overlap6.hs:16:3) x :: Proxy Bool x (bound at Overlap6.hs:15:3)
In the expression: x In the expression: x
In an equation for ‛g’: g x = x In an equation for ‛g’: g x = x
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap7 where module Overlap7 where
type family F a b type family F a b where
type instance where
F Int a = Int F Int a = Int
F a b = Bool F a b = Bool
type instance F a Int = Int type instance F a Int = Int
......
Overlap7.hs:7:3: Overlap7.hs:8:1:
Conflicting family instance declarations: Illegal instance for closed family ‛F’
F Int a -- Defined at Overlap7.hs:7:3 In the type instance declaration for ‛F’
F a Int -- Defined at Overlap7.hs:9:15
Overlap7.hs:8:3:
Conflicting family instance declarations:
F a b -- Defined at Overlap7.hs:8:3
F a Int -- Defined at Overlap7.hs:9:15
Overlap8.hs:6:15:
Conflicting family instance declarations:
F a Int -- Defined at Overlap8.hs:6:15
F Int a -- Defined at Overlap8.hs:8:3
...@@ -2,8 +2,7 @@ ...@@ -2,8 +2,7 @@
module Overlap9 where module Overlap9 where
type family F a type family F a where
type instance where
F Int = Bool F Int = Bool
F a = Int F a = Int
......
Overlap9.hs:11:7: Overlap9.hs:10:7:
Could not deduce (F a ~ Int) Could not deduce (F a ~ Int)
from the context (Show a) from the context (Show a)
bound by the type signature for g :: Show a => a -> F a bound by the type signature for g :: Show a => a -> F a
at Overlap9.hs:10:6-23 at Overlap9.hs:9:6-23
Relevant bindings include Relevant bindings include
g :: a -> F a (bound at Overlap9.hs:11:1) g :: a -> F a (bound at Overlap9.hs:10:1)
x :: a (bound at Overlap9.hs:11:3) x :: a (bound at Overlap9.hs:10:3)
In the expression: length (show x) In the expression: length (show x)
In an equation for ‛g’: g x = length (show x) In an equation for ‛g’: g x = length (show x)
SimpleFail1a.hs:4:1: SimpleFail1a.hs:4:1:
Number of parameters must match family declaration; expected 2 Couldn't match kind ‛* -> *’ against ‛*’
In the data instance declaration for ‛T1’ In the data instance declaration for ‛T1’