#2627: GADT + Type family doesn't unify like I expect
------------------------+---------------------------------------------------
Reporter: ryani | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 6.9 | Severity: normal
Keywords: | Testcase:
Architecture: Unknown | Os: Unknown
------------------------+---------------------------------------------------
I'd expect this program to compile; the "given" equations in "conn" should
add additional constraints to the types determined by the GADT. Instead
it looks like (Dual a) is failing to unify with (R _ _), and the same for
(Dual b) and (W _ _).
{{{
{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}
module Dual where
data R a b
data W a b
data Z
type family Dual a
type instance Dual Z = Z
type instance Dual (R a b) = W a (Dual b)
type instance Dual (W a b) = R a (Dual b)
data Comm a where
Rd :: (a -> Comm b) -> Comm (R a b)
Wr :: a -> Comm b -> Comm (W a b)
Fin :: Int -> Comm Z
conn :: (Dual a ~ b, Dual b ~ a) => Comm a -> Comm b -> (Int, Int)
conn (Fin x) (Fin y) = (x,y)
conn (Rd k) (Wr a r) = conn (k a) r
conn (Wr a r) (Rd k) = conn r (k a)
}}}
Running off of GHC HEAD:
{{{The Glorious Glasgow Haskell Compilation System, version
6.11.20080925}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2627>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
