Hello,
I'm working on a lock-free algorithm that's meant to be used in a
concurrent setting, and I've run into a possible issue.
The crux of the matter is that a particular function needs to perform the
following:
> x <- MVector.read vec ix
> position <- readIORef posRef
and the algorithm is on
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 ev
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 th
[Resending to the list, I used the wrong address. Sorry for the duplicate
copies.]
On 19 dec. 2013, at 05:30, 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
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
