Re: [Haskell-cafe] Advice on type families and non-injectivity?

There is a real difficulty here with type-checking 'bar'. (And that difficulty is why 'foo' is also rejected.)

Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1 installation doesn't complain. -- Conal On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones wrote:

| > > {-# LANGUAGE TypeFamilies #-} | > > | > > type family F a | > > | > > foo :: F a | > > foo = undefined | > > | > > bar :: F a | > > bar = foo

There is a real difficulty here with type-checking 'bar'. (And that difficulty is why 'foo' is also rejected.)

Namely, when typechecking 'bar', we must instantiate foo with an unknown type, say alpha. So now we must find a type 'alpha' such that F a ~ F alpha Certainly alpha=1 is one solution, but there might be others. For example, suppose type instance F [b] = F b Then alpha=[a] would also be a solution.

In this particular case any solution will do, but suppose there was an addition constraint (C alpha) arising from the right hand side, where C is a class. Then if we had instance C [b] where ... then the second solution (alpha=[a]) would work, but not the first. This can get arbitrarily complicated, and GHC's type inference does not "search" various solutions; it follows one path.

The solution is to provide a way to fix alpha. For example, foo :: a -> F a is fine.

Simon

| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Richard Eisenberg | Sent: 14 January 2013 03:47 | To: Conal Elliott | Cc: glasgow-haskell-users@haskell.org; Haskell Cafe | Subject: Re: Advice on type families and non-injectivity? | | Hi Conal, | | I agree that your initial example is a little puzzling, and I'm glad | that the new ambiguity checker prevents both definitions, not just one. | | However, your initial question seems broader than just this example. I | have run into this problem (wanting injective type functions) several | times myself, and have been successful at finding workarounds. But, I | can't think of any unifying principle or solid advice. If you can post | more information about your problem, perhaps I or others can contribute. | | For what it's worth, the desire for injective type functions has been | entered as ticket #6018 in the GHC Trac, but I see you're already on the | cc: list. I believe Simon PJ has given serious thought to implementing | this feature and may have even put in some very basic code toward this | end. | | Richard | | On Jan 13, 2013, at 2:10 PM, Conal Elliott wrote: | | > I sometimes run into trouble with lack of injectivity for type | families. I'm trying to understand what's at the heart of these | difficulties and whether I can avoid them. Also, whether some of the | obstacles could be overcome with simple improvements to GHC. | > | > Here's a simple example: | > | > > {-# LANGUAGE TypeFamilies #-} | > > | > > type family F a | > > | > > foo :: F a | > > foo = undefined | > > | > > bar :: F a | > > bar = foo | > | > The error message: | > | > Couldn't match type `F a' with `F a1' | > NB: `F' is a type function, and may not be injective | > In the expression: foo | > In an equation for `bar': bar = foo | > | > A terser (but perhaps subtler) example producing the same error: | > | > > baz :: F a | > > baz = baz | > | > Replacing `a` with a monotype (e.g., `Bool`) eliminates the error. | > | > Does the difficulty here have to do with trying to *infer* the type | and then compare with the given one? Or is there an issue even with type | *checking* in such cases? | > | > Other insights welcome, as well as suggested work-arounds. | > | > I know about (injective) data families but don't want to lose the | convenience of type synonym families. | > | > Thanks, -- Conal | > | > _______________________________________________ | > 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