#2157: Equality Constraints with Type Families
----------------------------------------+-----------------------------------
Reporter: hpacheco | Owner: chak
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.9
Severity: normal | Resolution:
Keywords: | Testcase:
Architecture: Multiple | Os: Multiple
----------------------------------------+-----------------------------------
Comment (by claus):
Replying to [comment:2 chak]:
> On the other hand, given
> {{{
> type family F a :: * -> *
> }}}
> an equality of the form `F a1 b1 ~ F a2 b2` implies `F a1 ~ F a2` and
`b1 ~ b2` as always in Haskell
i had problems with this statement, until i stopped thinking of "type
functions" (which would allow constant functions violating your
assumption) and thought of "phantom types" (all type parameters matter,
even if they disappear in the result). if that association is useful,
though, you might want to disallow partially applied type synonyms in type
instances - `Const` and `f` seem fishy here (wrt your implication, at
least):
{{{
{-# LANGUAGE TypeFamilies #-}
type family Const a :: * -> *
type instance Const a = C a
type C a t = a
f :: Const Bool Int -> Const Bool Char -> Const Bool Bool
f i c = False
-- f i c = i
-- f i c = i && True
-- f i c = (i || c)
type family Const2 a :: * -> *
type instance Const2 a = Ct a
newtype Ct a t = Ct a
g :: Const2 Bool Int -> Const2 Bool Char -> Const2 Bool Bool
g i c = Ct False
-- g i c = Ct i
-- g i c = Ct (i && True)
-- g i c = Ct (i || c)
}}}
for `Const` and `f`, `GHCi, version 6.9.20080217` happily accepts `i &&
True` and `i || c`, converting between `Const Bool *` and `Bool`, but does
not accept `i`.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2157#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
