#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 chak):
Replying to [comment:3 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
}}}
Why do you think `Const` is fishy? Maybe I should make more precise what
I regard as ''partial application'' in the context of type families. If
you look at [http://haskell.org/haskellwiki/GHC/Type_families the type
family specification] in Section 7.1, it says that the arity of a type
family is the number of parameters given in the type family declaration.
In the case of `Const`, this is 1 (namely `a`), '''not''' 2 (as you might
think if you only consider the kind of `Const`). Whenever a type family
is used, you must supply '''at least''' as many type arguments as the
arity of the type family suggests. So, in the case of `Const`, a single
argument suffices. Do you think Section 7 of
[http://haskell.org/haskellwiki/GHC/Type_families the type family
specification] is unclear on that matter. If so, I'd be grateful for any
suggestions that make the specification clearer.
NB: The rules for what constitutes a valid partial application of a
vanilla type synonym are different, see
[http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-
extensions.html#type-synonyms] This may be somewhat confusing, but I
don't think there is much we can do about this, as the present definitions
are crucial to get a sound type system. (Well, we could restrict what you
can do with vanilla synonyms, but we'd like to stay backwards compatible
to H98 and, I guess, people would also not be happy to sacrifice any of
the currently offered expressiveness.)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2157#comment:7>
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
