Let me revise slightly. GHC wouldn't guess that f3 would be f just because f is the only well-kinded thing in sight. Instead, it would use (f2 i ~ a) to reduce the target equality, (f3 i2 ~ a), to (f3 i2 ~ f2 i). It would then try to break this down into (f3 ~ f2) and (i2 ~ i). Here is where the kind problem comes in -- these equalities are ill-kinded. So, GHC (rightly, in my view) rejects this code, and reports an appropriate error message. Of course, more context in the error message might be an improvement, but I don't think the current message is wrong. As for Thijs's comment about lack of decomposition in GHC 7.6.3: You're right, that code fails in GHC 7.6.3 because of an attempt (present in GHC 7.6.x) to redesign the Core type system to allow for unsaturated type families (at least in Core, if not in Haskell). There were a few cases that came up that the redesign couldn't handle, like Thijs's. So, the redesign was abandoned. In GHC HEAD, Thijs's code works just fine. (The redesign was to get rid of the "left" and "right" coercions, which allow decomposition of things like (f a ~ g b), in favor of an "nth" coercion, which allows decomposition of things like (T a ~ T b).) Good -- I feel much better about this answer, where there's no guess for the value of f3! Richard On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote:

I'd say GHC has it right in this case.

(f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's initial problem, we have (with all type, kind, and coercion variables made explicit)

...

data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq :: forall (f :: j -> k). f i ~ a => InnerEq j k i a

class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). t (f i) -> t a -> Maybe (InnerEq j k i a)

instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 -> k) (i2 :: j2) (a :: k). InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 i ~ f i2)) (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) = Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a))

GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. Using the two equalities we have, we can rewrite this as a need to prove `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). But, this is exactly the case where the kinds *don't* match up. So, I agree that GHC can't deduce that equality, but I think that, even if it could, it wouldn't be able to type-check the whole term.... unless I've made a mistake somewhere.

I don't see an immediate way to fix the problem, but I haven't thought much about it.

Does this help? Does anyone see a mistake in what I've done?

Richard

On Dec 18, 2013, at 6:38 PM, Gábor Lehel wrote:

...

Hello,

The upcoming GHC 7.8 recently gave me this error:

Could not deduce (i ~ i1) from the context (f1 i ~ f i1)

Which is strange to me: shouldn't (f1 i ~ f i1) exactly imply (f1 ~ f, i ~ i1)? (Or with nicer variable names: (f a ~ g b) => (f ~ g, a ~ b)?)

When I inquired about this in #haskell on IRC, a person going by the name xnyhps had this to say:

...

I've also noticed that, given type equality constraints are never decomposed. I'm quite curious why.

and later:

...

It's especially weird because a given f a ~ g b can not be used to solve a wanted f a ~ g b, because the wanted constraint is decomposed before it can interact with the given constraint.

I'm not quite so well versed in the workings of GHC's type checker as she or he is, but I don't understand why it's this way either.

Is this a relic of https://ghc.haskell.org/trac/ghc/ticket/5591 and https://ghc.haskell.org/trac/ghc/ticket/7205? Is there a principled reason this shouldn't be true? Is it an intentional limitation of the constraint solver? Or is it just a bug?

Thanks in advance, Gábor

P.S. I got the error on this line: https://github.com/glaebhoerl/type-eq/blob/master/Type/Eq.hs#L181, possibly after having added kind annotations to `InnerEq` (which also gets a less general kind inferred than the one I expect). If it's important I can try to create a reduced test case. _______________________________________________ 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

Yes, that's right. If (f a ~ g b) and `f` and `g` have syntactically different kinds, then we would hope that those kinds are in fact equal. But, GHC has no way of doing this currently -- though it does store kind equalities, it is an invariant that all such equalities must be simply reflexivity. Hopefully, this will change soon. :) Richard On Dec 19, 2013, at 11:11 AM, Gábor Lehel wrote:

Does this boil down to the fact that GHC doesn't have kind GADTs? I.e. given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` and `g` might have different kinds (how could you ever have constructed `f a ~ g b` if they did?), but GHC isn't equipped to reason about that (to store evidence for it and retrieve it later)?

On Thu, Dec 19, 2013 at 4:01 PM, Richard Eisenberg wrote:

...

Let me revise slightly. GHC wouldn't guess that f3 would be f just because f is the only well-kinded thing in sight.

Instead, it would use (f2 i ~ a) to reduce the target equality, (f3 i2 ~ a), to (f3 i2 ~ f2 i). It would then try to break this down into (f3 ~ f2) and (i2 ~ i). Here is where the kind problem comes in -- these equalities are ill-kinded. So, GHC (rightly, in my view) rejects this code, and reports an appropriate error message. Of course, more context in the error message might be an improvement, but I don't think the current message is wrong.

As for Thijs's comment about lack of decomposition in GHC 7.6.3: You're right, that code fails in GHC 7.6.3 because of an attempt (present in GHC 7.6.x) to redesign the Core type system to allow for unsaturated type families (at least in Core, if not in Haskell). There were a few cases that came up that the redesign couldn't handle, like Thijs's. So, the redesign was abandoned. In GHC HEAD, Thijs's code works just fine.

(The redesign was to get rid of the "left" and "right" coercions, which allow decomposition of things like (f a ~ g b), in favor of an "nth" coercion, which allows decomposition of things like (T a ~ T b).)

Good -- I feel much better about this answer, where there's no guess for the value of f3!

Richard

On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote:

...

I'd say GHC has it right in this case.

(f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's initial problem, we have (with all type, kind, and coercion variables made explicit)

...

data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq :: forall (f :: j -> k). f i ~ a => InnerEq j k i a

class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). t (f i) -> t a -> Maybe (InnerEq j k i a)

instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 -> k) (i2 :: j2) (a :: k). InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 i ~ f i2)) (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) = Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a))

GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. Using the two equalities we have, we can rewrite this as a need to prove `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). But, this is exactly the case where the kinds *don't* match up. So, I agree that GHC can't deduce that equality, but I think that, even if it could, it wouldn't be able to type-check the whole term.... unless I've made a mistake somewhere.

I don't see an immediate way to fix the problem, but I haven't thought much about it.

Does this help? Does anyone see a mistake in what I've done?

Richard

On Dec 18, 2013, at 6:38 PM, Gábor Lehel wrote:

...

Hello,

The upcoming GHC 7.8 recently gave me this error:

Could not deduce (i ~ i1) from the context (f1 i ~ f i1)

Which is strange to me: shouldn't (f1 i ~ f i1) exactly imply (f1 ~ f, i ~ i1)? (Or with nicer variable names: (f a ~ g b) => (f ~ g, a ~ b)?)

When I inquired about this in #haskell on IRC, a person going by the name xnyhps had this to say:

...

I've also noticed that, given type equality constraints are never decomposed. I'm quite curious why.

and later:

...

It's especially weird because a given f a ~ g b can not be used to solve a wanted f a ~ g b, because the wanted constraint is decomposed before it can interact with the given constraint.

I'm not quite so well versed in the workings of GHC's type checker as she or he is, but I don't understand why it's this way either.

Is this a relic of https://ghc.haskell.org/trac/ghc/ticket/5591 and https://ghc.haskell.org/trac/ghc/ticket/7205? Is there a principled reason this shouldn't be true? Is it an intentional limitation of the constraint solver? Or is it just a bug?

Thanks in advance, Gábor

P.S. I got the error on this line: https://github.com/glaebhoerl/type-eq/blob/master/Type/Eq.hs#L181, possibly after having added kind annotations to `InnerEq` (which also gets a less general kind inferred than the one I expect). If it's important I can try to create a reduced test case. _______________________________________________ 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

| given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` | and `g` might have different kinds (how could you ever have constructed | `f a ~ g b` if they did?) Wait. It's quite possible for them to have different kinds. E.g. f :: (* -> *) -> * a :: (* -> *) g :: * -> * b :: * Then (f a :: *) and (g b :: *), and it'd be quite reasonable to form the equality (f a ~ g b). Simon | -----Original Message----- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Gábor Lehel | Sent: 19 December 2013 16:12 | To: Richard Eisenberg | Cc: glasgow-haskell-users@haskell.org | Subject: Re: Decomposition of given equalities | | Does this boil down to the fact that GHC doesn't have kind GADTs? I.e. | given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` | and `g` might have different kinds (how could you ever have constructed | `f a ~ g b` if they did?), but GHC isn't equipped to reason about that | (to store evidence for it and retrieve it later)? | | On Thu, Dec 19, 2013 at 4:01 PM, Richard Eisenberg | wrote: | > Let me revise slightly. GHC wouldn't guess that f3 would be f just | because f is the only well-kinded thing in sight. | > | > Instead, it would use (f2 i ~ a) to reduce the target equality, (f3 i2 | ~ a), to (f3 i2 ~ f2 i). It would then try to break this down into (f3 ~ | f2) and (i2 ~ i). Here is where the kind problem comes in -- these | equalities are ill-kinded. So, GHC (rightly, in my view) rejects this | code, and reports an appropriate error message. Of course, more context | in the error message might be an improvement, but I don't think the | current message is wrong. | > | > As for Thijs's comment about lack of decomposition in GHC 7.6.3: | You're right, that code fails in GHC 7.6.3 because of an attempt | (present in GHC 7.6.x) to redesign the Core type system to allow for | unsaturated type families (at least in Core, if not in Haskell). There | were a few cases that came up that the redesign couldn't handle, like | Thijs's. So, the redesign was abandoned. In GHC HEAD, Thijs's code works | just fine. | > | > (The redesign was to get rid of the "left" and "right" coercions, | > which allow decomposition of things like (f a ~ g b), in favor of an | > "nth" coercion, which allows decomposition of things like (T a ~ T | > b).) | > | > Good -- I feel much better about this answer, where there's no guess | for the value of f3! | > | > Richard | > | > On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote: | > | >> I'd say GHC has it right in this case. | >> | >> (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the | >> kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), | >> and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's | >> initial problem, we have (with all type, kind, and coercion variables | >> made explicit) | >> | >>> data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq | >>> :: forall (f :: j -> k). f i ~ a => InnerEq j k i a | >>> | >>> class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: | >>> forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). | >>> t (f i) -> t a -> Maybe (InnerEq j k i a) | >>> | >>> instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k | >>> (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 - | > k) (i2 :: j2) (a :: k). | >>> InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe | >>> (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 | i ~ f i2)) | >>> (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) | >>> = Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a)) | >> | >> GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying | >> around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. | Using the two equalities we have, we can rewrite this as a need to prove | `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that | it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). | But, this is exactly the case where the kinds *don't* match up. So, I | agree that GHC can't deduce that equality, but I think that, even if it | could, it wouldn't be able to type-check the whole term.... unless I've | made a mistake somewhere. | >> | >> I don't see an immediate way to fix the problem, but I haven't | thought much about it. | >> | >> Does this help? Does anyone see a mistake in what I've done? | >> | >> Richard | >> | >> On Dec 18, 2013, at 6:38 PM, Gábor Lehel | wrote: | >> | >>> Hello, | >>> | >>> The upcoming GHC 7.8 recently gave me this error: | >>> | >>> Could not deduce (i ~ i1) | >>> from the context (f1 i ~ f i1) | >>> | >>> Which is strange to me: shouldn't (f1 i ~ f i1) exactly imply (f1 ~ | >>> f, i ~ i1)? (Or with nicer variable names: (f a ~ g b) => (f ~ g, a | >>> ~ | >>> b)?) | >>> | >>> When I inquired about this in #haskell on IRC, a person going by the | >>> name xnyhps had this to say: | >>> | >>>> I've also noticed that, given type equality constraints are never | decomposed. I'm quite curious why. | >>> | >>> and later: | >>> | >>>> It's especially weird because a given f a ~ g b can not be used to | solve a wanted f a ~ g b, because the wanted constraint is decomposed | before it can interact with the given constraint. | >>> | >>> I'm not quite so well versed in the workings of GHC's type checker | >>> as she or he is, but I don't understand why it's this way either. | >>> | >>> Is this a relic of https://ghc.haskell.org/trac/ghc/ticket/5591 and | >>> https://ghc.haskell.org/trac/ghc/ticket/7205? Is there a principled | >>> reason this shouldn't be true? Is it an intentional limitation of | >>> the constraint solver? Or is it just a bug? | >>> | >>> Thanks in advance, | >>> Gábor | >>> | >>> P.S. I got the error on this line: | >>> https://github.com/glaebhoerl/type-eq/blob/master/Type/Eq.hs#L181, | >>> possibly after having added kind annotations to `InnerEq` (which | >>> also gets a less general kind inferred than the one I expect). If | >>> it's important I can try to create a reduced test case. | >>> _______________________________________________ | >>> 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 | >> | > | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Yes, it's quite possible, given f, a, g, and b of different kinds, to make `f a` and `g b` have the same *kind*. But how could they ever be the same type? Ah I see. Good point. Anyway, the conclusion is that decomposing a well-kinded (f a ~ g b) into ill-kinded goals is indeed a bad thing, so it's good that GHC doesn't do it. Simon From: Gábor Lehel [mailto:glaebhoerl@gmail.com] Sent: 30 December 2013 18:11 To: Simon Peyton-Jones Cc: Richard Eisenberg; glasgow-haskell-users@haskell.org Subject: Re: Decomposition of given equalities On Mon, Dec 30, 2013 at 7:00 PM, Simon Peyton-Jones mailto:simonpj@microsoft.com> wrote: | given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` | and `g` might have different kinds (how could you ever have constructed | `f a ~ g b` if they did?) Wait. It's quite possible for them to have different kinds. E.g. f :: (* -> *) -> * a :: (* -> *) g :: * -> * b :: * Then (f a :: *) and (g b :: *), and it'd be quite reasonable to form the equality (f a ~ g b). Yes, it's quite possible, given f, a, g, and b of different kinds, to make `f a` and `g b` have the same *kind*. But how could they ever be the same type? Is it not the case that (f a ~ g b) iff (f ~ g) and (a ~ b) (obviously impossible if those are of different kinds)? You would have to worry about this possibility if type constructor variables weren't injective, but they are. Simon | -----Original Message----- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users-mailto:glasgow-haskell-users- | bounces@haskell.orgmailto:bounces@haskell.org] On Behalf Of Gábor Lehel | Sent: 19 December 2013 16:12 | To: Richard Eisenberg | Cc: glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org | Subject: Re: Decomposition of given equalities | | Does this boil down to the fact that GHC doesn't have kind GADTs? I.e. | given `(f a ~ g b)` there's no possible way that `a` and `b`, resp. `f` | and `g` might have different kinds (how could you ever have constructed | `f a ~ g b` if they did?), but GHC isn't equipped to reason about that | (to store evidence for it and retrieve it later)? | | On Thu, Dec 19, 2013 at 4:01 PM, Richard Eisenberg mailto:eir@cis.upenn.edu> | wrote: | > Let me revise slightly. GHC wouldn't guess that f3 would be f just | because f is the only well-kinded thing in sight. | > | > Instead, it would use (f2 i ~ a) to reduce the target equality, (f3 i2 | ~ a), to (f3 i2 ~ f2 i). It would then try to break this down into (f3 ~ | f2) and (i2 ~ i). Here is where the kind problem comes in -- these | equalities are ill-kinded. So, GHC (rightly, in my view) rejects this | code, and reports an appropriate error message. Of course, more context | in the error message might be an improvement, but I don't think the | current message is wrong. | > | > As for Thijs's comment about lack of decomposition in GHC 7.6.3: | You're right, that code fails in GHC 7.6.3 because of an attempt | (present in GHC 7.6.x) to redesign the Core type system to allow for | unsaturated type families (at least in Core, if not in Haskell). There | were a few cases that came up that the redesign couldn't handle, like | Thijs's. So, the redesign was abandoned. In GHC HEAD, Thijs's code works | just fine. | > | > (The redesign was to get rid of the "left" and "right" coercions, | > which allow decomposition of things like (f a ~ g b), in favor of an | > "nth" coercion, which allows decomposition of things like (T a ~ T | > b).) | > | > Good -- I feel much better about this answer, where there's no guess | for the value of f3! | > | > Richard | > | > On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote: | > | >> I'd say GHC has it right in this case. | >> | >> (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the | >> kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), | >> and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's | >> initial problem, we have (with all type, kind, and coercion variables | >> made explicit) | >> | >>> data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq | >>> :: forall (f :: j -> k). f i ~ a => InnerEq j k i a | >>> | >>> class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: | >>> forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). | >>> t (f i) -> t a -> Maybe (InnerEq j k i a) | >>> | >>> instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k | >>> (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 - | > k) (i2 :: j2) (a :: k). | >>> InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe | >>> (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 | i ~ f i2)) | >>> (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) | >>> = Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a)) | >> | >> GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying | >> around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. | Using the two equalities we have, we can rewrite this as a need to prove | `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that | it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). | But, this is exactly the case where the kinds *don't* match up. So, I | agree that GHC can't deduce that equality, but I think that, even if it | could, it wouldn't be able to type-check the whole term.... unless I've | made a mistake somewhere. | >> | >> I don't see an immediate way to fix the problem, but I haven't | thought much about it. | >> | >> Does this help? Does anyone see a mistake in what I've done? | >> | >> Richard | >> | >> On Dec 18, 2013, at 6:38 PM, Gábor Lehel mailto:glaebhoerl@gmail.com> | wrote: | >> | >>> Hello, | >>> | >>> The upcoming GHC 7.8 recently gave me this error: | >>> | >>> Could not deduce (i ~ i1) | >>> from the context (f1 i ~ f i1) | >>> | >>> Which is strange to me: shouldn't (f1 i ~ f i1) exactly imply (f1 ~ | >>> f, i ~ i1)? (Or with nicer variable names: (f a ~ g b) => (f ~ g, a | >>> ~ | >>> b)?) | >>> | >>> When I inquired about this in #haskell on IRC, a person going by the | >>> name xnyhps had this to say: | >>> | >>>> I've also noticed that, given type equality constraints are never | decomposed. I'm quite curious why. | >>> | >>> and later: | >>> | >>>> It's especially weird because a given f a ~ g b can not be used to | solve a wanted f a ~ g b, because the wanted constraint is decomposed | before it can interact with the given constraint. | >>> | >>> I'm not quite so well versed in the workings of GHC's type checker | >>> as she or he is, but I don't understand why it's this way either. | >>> | >>> Is this a relic of https://ghc.haskell.org/trac/ghc/ticket/5591 and | >>> https://ghc.haskell.org/trac/ghc/ticket/7205? Is there a principled | >>> reason this shouldn't be true? Is it an intentional limitation of | >>> the constraint solver? Or is it just a bug? | >>> | >>> Thanks in advance, | >>> Gábor | >>> | >>> P.S. I got the error on this line: | >>> https://github.com/glaebhoerl/type-eq/blob/master/Type/Eq.hs#L181, | >>> possibly after having added kind annotations to `InnerEq` (which | >>> also gets a less general kind inferred than the one I expect). If | >>> it's important I can try to create a reduced test case. | >>> _______________________________________________ | >>> 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 | >> | > | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.orgmailto:Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users