Non-injectivity of type families sometimes hinders type inference. Consider

> Set' (Set.singleton 'c')

Naively, we only know that (Char ~ NominalArg a). Since type families are not necessarily injective, this usually means we cannot determine the type variable `a' from this constraint. However, since the NominalArg instance is parametric in `a', I suspect GHC might successfully infer (Char ~ a) in this case.

… A quick ghci test confirms that GHC does infer (Char ~ a) here. I apologize for not just experimenting in the first place, but maybe this email will save someone slightly more time than is required to read it. :P

On Sun, Aug 18, 2013 at 3:37 PM, Joachim Breitner <mail@joachim-breitner.de> wrote:
Hi,

not sure – where would injectivity be needed?

Greetings,
Joachim

Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb Nicolas Frisby:
> Is the non-injectivity not an issue here because the type family
> application gets immediately simplified?
>
>
> On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner
> <mail@joachim-breitner.de> wrote:
>         Hi,
>
>         now that roles are in HEAD, I could play around a bit with it.
>         They were
>         introduced to solve the unsoundness of newtype deriving, but
>         there is
>         also the problem of abstraction: If I define a set type based
>         on an ord
>         instance, e.g.
>
>                 data Set a = Set a -- RHS here just for demonstration
>
>         the I don’t want my users to replace a "Set Int" by a "Set
>         (Down Int)",
>         even though the latter is a newtype of the former. This can be
>         prevented
>         by forcing the role of "a" to be Nominal (and not
>         Representational, as
>         it is by default). What I just noticed is that one does not
>         even have to
>         introduce new syntax for it, one can just use:
>
>                 type family NominalArg x
>                 type instance (NominalArg x) = x
>                 data Set' a = Set' (NominalArg a)
>
>         and get different roles; here the excerpt from --show-iface
>         (is there an
>         easier way to see role annotations):
>
>                 5b7b2f7c3883ef0d9fc7934ac56c4805
>                   data Set a@R
>                 [..]
>                 8e15d783d58c18b8205191ed3fd87e27
>                   data Set' a@N
>
>         The type family does not get into the way, e.g.
>
>                 conv (Set a) = Set' a
>
>         works as usual.
>
>         (I now also notice that the parser actually supports role
>         annotations...
>         but still a nice, backward-compatible trick here).
>
>         Greetings,
>         Joachim
>
>         --
>         Joachim “nomeata” Breitner
>           mail@joachim-breitner.de • http://www.joachim-breitner.de/
>           Jabber: nomeata@joachim-breitner.de  • GPG-Key: 0x4743206C
>           Debian Developer: nomeata@debian.org
>
>         _______________________________________________
>         Glasgow-haskell-users mailing list
>         Glasgow-haskell-users@haskell.org
>         http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

--
Joachim “nomeata” Breitner
  mail@joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata@joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata@debian.org

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users