Decomposition of given equalities

Fri Dec 20 18:38:12 UTC 2013

OK, it all makes sense then. Thanks!

On Fri, Dec 20, 2013 at 3:34 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> 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 <glaebhoerl at gmail.com> 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 <eir at 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 <glaebhoerl at 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 at haskell.org
> >>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >>>>
> >>>
> >>> _______________________________________________
> >>> Glasgow-haskell-users mailing list
> >>> Glasgow-haskell-users at haskell.org
> >>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >>>
> >>
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20131220/4fd3d061/attachment-0001.html>