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 <e...@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 <glaebho...@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.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
