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