Decomposition of given equalities

[Gábor Lehel]

Thanks for the reply. Still digesting what you wrote, but in the
meantime I did extract the essential parts of the example:

{-# LANGUAGE GADTs, PolyKinds, ExplicitForAll #-}

data InnerEq (i :: k_i) (a :: k_a) where
    InnerEq :: forall (f :: k_i -> k_a) (i :: k_i) (a :: k_a). f i ~ a
=> InnerEq i a

maybeInnerEq :: InnerEq i1 (f i2) -> InnerEq i1 a -> Maybe (InnerEq i2 a)
maybeInnerEq InnerEq InnerEq = Just InnerEq

On Thu, Dec 19, 2013 at 5:30 AM, Richard Eisenberg <eir at cis.upenn.edu> 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
>>
>