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
[Resending to the list, I used the wrong address. Sorry for the duplicate
copies.]
On 19 dec. 2013, at 05:30, Richard Eisenberg e...@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
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
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 only
