Decomposition of given equalities

Mon Dec 30 18:00:28 UTC 2013

| 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 at haskell.org] On Behalf Of Gábor Lehel
| Sent: 19 December 2013 16:12
| To: Richard Eisenberg
| Cc: glasgow-haskell-users at 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 <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
| >>
| >
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users