#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:7 chak]:
> > > {{{
> > > 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
> }}}
>
> Why do you think `Const` is fishy?
because:
- type synonym `C` appears partially applied in what amounts to a type
class instance parameter position (the rhs of the Const instance)
- the implementation definitely does not behave as if your decomposition
played any role (parameters of both `Const Bool Int` and `Const Bool Char`
are used as/converted to `Bool`, hence equal types even though `Int` does
not equal `Char`). nor do the permitted and not-permitted conversions in
`f` seem consistent - compare also:
http://www.haskell.org/pipermail/haskell-cafe/2008-March/040788.html
http://www.haskell.org/pipermail/haskell-cafe/2008-March/040790.html
> Maybe I should make more precise what I regard as ''partial
application'' in the context of type families.
it isn't about partial applications of type families (even though the
different sorts of parameters there take some getting used to), but about
good old-fashioned partial applications of type synonyms in new contexts.
i guess they are permitted here because the rhs of a type instance uses
the same grammar non-terminal as the rhs of a type synonym, but i suspect
that the rhs of a type instance might have to be treated like a type
parameter of a type class instance.
but that is just a guess - the main issues here are the decomposition
rule, which i don't quite understand, and which doesn't quite seem to be
used in the implementation, and the equalities/conversions permitted in
the implementation, which do not seem to be consistent.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2157#comment:9>
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
