Advice on type families and non-injectivity?

older
Re: [Haskell-cafe] Advice on type...

Conal Elliott

13 Jan 2013 13 Jan '13

2:10 p.m.

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

Attachments:

attachment.html (text/html — 1.3 KB)

Show replies by date

Christian Höner zu Siederdissen

13 Jan 13 Jan

2:36 p.m.

Hi, How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely. My question is not completely retorical, if there is an answer I would like to know it :-) Gruss, Christian * Conal Elliott [13.01.2013 20:13]:

...

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

Conal Elliott

3:13 p.m.

Hi Christian, Given "bar :: Bool", I can't see how one could go from "Bool" to "F a =

...

Bool" and determine "a" uniquely.

The same question applies to "foo :: Bool", right? Yet no error message there. Regards, - Conal On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen < choener@tbi.univie.ac.at> wrote:

...

Hi,

How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely.

My question is not completely retorical, if there is an answer I would like to know it :-)

Gruss, Christian

* Conal Elliott [13.01.2013 20:13]:

...
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

Christian Höner zu Siederdissen

6:20 p.m.

Hi Conal, if you take your example program and write "foo :: Bool", ghci accepts it? For me it complains, and I would think rightly so, that "couldn't match expected type Fa with actual type Bool". It actually only works with the following quite useless "type instance F a = Bool". By the way, using above instance, the original example works... ;-) Ultimatively, injective type families would be useful. Thinking about roman's vector library for example. For my code, I am switching more and more to data families to get the desired behaviour of: F a ~ F b => a ~ b Gruss, Christian * Conal Elliott [13.01.2013 21:14]:

...

Hi Christian,

Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely.

The same question applies to "foo :: Bool", right? Yet no error message there.

Regards, - Conal On Sun, Jan 13, 2013 at 11:36 AM, Christian Ho:ner zu Siederdissen wrote:

Hi,

How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely.

My question is not completely retorical, if there is an answer I would like to know it :-)

Gruss, Christian

* Conal Elliott [13.01.2013 20:13]: > 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

Iavor Diatchki

2:39 p.m.

Hello Conal, The issue with your example is that it is ambiguous, so GHC can't figure out how to instantiate the use of `foo`. It might be easier to see why this is if you write it in this form:

...

foo :: (F a ~ b) => b foo = ...

Now, we can see that only `b` appears on the RHS of the `=>`, so there is really no way for GHC to figure out what is the intended value for `a`. Replacing `a` with a concrete type (such as `Bool`) eliminates the problem, because now GHC does not need to come up with a value for `a`. Another way to eliminate the ambiguity would be if `F` was injective---then we'd know that `b` uniquely determines `a` so again there would be no ambiguity. If `F` is not injective, however, the only workaround would be to write the type in such a way that the function arguments appear in the signature directly (e.g., something like 'a -> F a' would be ok). -Iavor On Sun, Jan 13, 2013 at 11:10 AM, 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

Conal Elliott

3:05 p.m.

Hi Iavor, Thanks for the remarks. so there is really no way for GHC to figure out what is the intended value

...

for `a`.

Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`? -- Conal On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki wrote:

...

Hello Conal,

The issue with your example is that it is ambiguous, so GHC can't figure out how to instantiate the use of `foo`. It might be easier to see why this is if you write it in this form:

...
foo :: (F a ~ b) => b foo = ...

Now, we can see that only `b` appears on the RHS of the `=>`, so there is really no way for GHC to figure out what is the intended value for `a`. Replacing `a` with a concrete type (such as `Bool`) eliminates the problem, because now GHC does not need to come up with a value for `a`. Another way to eliminate the ambiguity would be if `F` was injective---then we'd know that `b` uniquely determines `a` so again there would be no ambiguity.

If `F` is not injective, however, the only workaround would be to write the type in such a way that the function arguments appear in the signature directly (e.g., something like 'a -> F a' would be ok).

-Iavor

On Sun, Jan 13, 2013 at 11:10 AM, 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

Iavor Diatchki

3:52 p.m.

Hello, On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott wrote:

...

so there is really no way for GHC to figure out what is the intended value

...
for `a`.

Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`?

Wouldn't that make `F` a constant type family, and so one could just skip the `a` parameter? Anyway, if there was a way to assert something like that about a type-function, than there would be no problem. When something like that happens (i.e., GHC figures out that it does not know how to instantiate a type variable, but it is sure that the actual instantiation does not matter), GHC instantiates the variable a special type called `Any`, which has a very polymorphic kind. By the way, Simon recently reworked the ambiguity checker in GHC, and now HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check uses exactly what's in your example: a value `f :: S` is ambiguous, if `g :: S; g = f` results in an error). -Iavor

Richard Eisenberg

10:46 p.m.

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

Simon Peyton-Jones

14 Jan 14 Jan

6:39 a.m.

| > > {-# 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

Conal Elliott

3:51 p.m.

...

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

Simon Peyton-Jones

4:19 p.m.

Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1 installation doesn't complain. -- Conal Yes, it is rejected. Simon From: conal.elliott@gmail.com [mailto:conal.elliott@gmail.com] On Behalf Of Conal Elliott Sent: 14 January 2013 20:52 To: Simon Peyton-Jones Cc: Richard Eisenberg; glasgow-haskell-users@haskell.org; Haskell Cafe Subject: Re: 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 mailto:simonpj@microsoft.com> 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.orgmailto:glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-mailto:glasgow-haskell- | users-bounces@haskell.orgmailto:users-bounces@haskell.org] On Behalf Of Richard Eisenberg | Sent: 14 January 2013 03:47 | To: Conal Elliott | Cc: glasgow-haskell-users@haskell.orgmailto: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 mailto:conal@conal.net> 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.orgmailto:Glasgow-haskell-users@haskell.org | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users | | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

J. Garrett Morris

3:59 p.m.

On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones wrote:

...

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

This seems, to me, like a somewhat round-about way to express the problem. Iavor's explanation (which approach I have also found useful to explain the behavior of type functions in the past) captures the ambiguity in both descriptions:

...

foo :: (T a ~ b) => b foo = undefined

That this is ambiguous should be obvious. Accepting such a definition could presumably be used to generate values of undefined type; for example, I could get a generic instance

...

foo :: T Int

whether or not T Int is defined in my program! This also, to me, seems to make it clear that past GHC's acceptance of foo was in error. /g -- Sent from my mail client.

4511

Age (days ago)

4512

Last active (days ago)

List overview

Download

11 comments

6 participants

participants (6)

Christian Höner zu Siederdissen
Conal Elliott
Iavor Diatchki
J. Garrett Morris
Richard Eisenberg
Simon Peyton-Jones