Re: [Haskell-cafe] Advice on type families and non-injectivity?
| {-# 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-boun...@haskell.org [mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Cc: glasgow-haskell-us...@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 co...@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-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|
|
| ___
| Glasgow-haskell-users mailing list
| glasgow-haskell-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
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
simo...@microsoft.comwrote:
| {-# 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-boun...@haskell.org [mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Cc: glasgow-haskell-us...@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 co...@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-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|
|
| ___
| Glasgow-haskell-users mailing list
| glasgow-haskell-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
Thanks, Jake! This suggestion helped a lot. -- Conal
On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur jake.mcart...@gmail.comwrote:
I have a trick that loses a little convenience, but may still be more
convenient than data families.
{-# LANGUAGE TypeFamilies #-}
import Data.Tagged
type family F a
foo :: Tagged a (F a)
foo = Tagged undefined
bar :: Tagged a (F a)
bar = foo
This allows you to use the same newtype wrapper consistently, regardless
of what the type instance actually is; one of the inconveniences of data
families is the need to use different constructors for different types.
On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott co...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
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.elli...@gmail.com [mailto:conal.elli...@gmail.com] On Behalf Of
Conal Elliott
Sent: 14 January 2013 20:52
To: Simon Peyton-Jones
Cc: Richard Eisenberg; glasgow-haskell-us...@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
simo...@microsoft.commailto:simo...@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-boun...@haskell.orgmailto:glasgow-haskell-users-boun...@haskell.org
[mailto:glasgow-haskell-mailto:glasgow-haskell-
| users-boun...@haskell.orgmailto:users-boun...@haskell.org] On Behalf Of
Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Cc:
glasgow-haskell-us...@haskell.orgmailto:glasgow-haskell-us...@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
co...@conal.netmailto:co...@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-us...@haskell.orgmailto:glasgow-haskell-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|
|
| ___
| Glasgow-haskell-users mailing list
| glasgow-haskell-us...@haskell.orgmailto:glasgow-haskell-us...@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
Re: [Haskell-cafe] Advice on type families and non-injectivity?
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 co...@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-us...@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
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
iavor.diatc...@gmail.comwrote:
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 co...@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-us...@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
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
choe...@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 co...@conal.net [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-us...@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
Hello, On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
I have a trick that loses a little convenience, but may still be more
convenient than data families.
{-# LANGUAGE TypeFamilies #-}
import Data.Tagged
type family F a
foo :: Tagged a (F a)
foo = Tagged undefined
bar :: Tagged a (F a)
bar = foo
This allows you to use the same newtype wrapper consistently, regardless of
what the type instance actually is; one of the inconveniences of data
families is the need to use different constructors for different types.
On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott co...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
On 1/13/13 3:52 PM, Iavor Diatchki wrote: On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net 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, I don't see why. If we translate this to dependent type notation we get: ((a::*) - F a) == ((b::*) - F b) This equality should hold in virtue of alpha-conversion. What F is, is irrelevant; the only thing that matters is that it has kind *-*. In particular, it doesn't matter whether F is arbitrary, injective, parametric, constant, etc. The problem is that the above isn't the equation GHC sees. GHC sees: F a == F b and it can't infer any correlation between a and b, where one of those is universally quantified in the context (the definition of bar) and the other is something we need to fabricate to hand off to the polymorphic value (the call to foo). Of course, in this particular case it *ought* to be fine, by parametricity in the definition of foo. That is, since we merely need to come up with some b, any b, such that F b is the type we need (namely: F a), the a we have will suffice for that. So if we're explicit about type passing, the following is fine: foo :: forall b. F b bar :: forall a. F a bar = /\a - foo @a The problem is that while the a is sufficient it's not (in general) necessary. And that's the ambiguity GHC is complaining about. GHC can't see that foo is parametric in b, and therefore that a is as good as any other type. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
