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 <m...@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 > > <m...@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 > > m...@joachim-breitner.de • http://www.joachim-breitner.de/ > > Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C > > Debian Developer: nome...@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 > m...@joachim-breitner.de • http://www.joachim-breitner.de/ > Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C > Debian Developer: nome...@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
