Type family equation violates injectivity?

Carter Schonwald carter.schonwald at gmail.com
Sun Dec 30 00:44:40 UTC 2018


i did some digging to see if theres a simple fix ... but then i realized
that the current design they have for inlineR always assumes theres IO
available in pure computations ... which they use the s parameter to thread
into the pure vector code via reflection tricks

so it looks like the "right" way fix this would be to have the MVector data
type have both the state token for the the underlying resource AND whatever
PrimMonad its running in, rather than smashing them together... especially
since the ST monad and friend wont wont have the same state token as the
underlying IO resource

either way, what seems to be going on is that theres a mutex on which
computations talk with the R RTS/instance the haskell code talks to, and
theres a little bit of a mismatch in how they handle that ..

either way, its not a ghc issue, its a design issue around vector and the
api contract as the maintainers understand it vs how the package uses it.
(though i repeat: i do think theres an issue in how they factor thestate
token stuff )

On Sat, Dec 29, 2018 at 7:06 PM Carter Schonwald <carter.schonwald at gmail.com>
wrote:

> To be clear : I’m annoyed with myself that this impacted a package that
> depends on vector, but this does seem to be the case that the newest bug
> fix release for vector actually revealed a broken design for the vector
> instances / data types in the inline-r package.
>
> To;dr — I suggest patching inline-r to remove the s parameter in its
> immutable vector data types
>
> On Sat, Dec 29, 2018 at 6:48 PM Carter Schonwald <
> carter.schonwald at gmail.com> wrote:
>
>> so i took a look .. (also the inline-r devs seem to have done a hackage
>> revision so you wont hit that issue in your current setup if you do a cabal
>> update ..)
>> and it seems like the type definitions in inline-r are kinda bogus  and
>> you should get them patched ...
>>
>> the MVector type class, and related type families, all assume your
>> mutable type has the last two arguments as the io/state token and then the
>> element type
>>
>> eg
>> basicLength :: v s a -> Int
>> <http://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Int.html#t:Int>
>>
>>
>> i looked at
>> https://github.com/tweag/HaskellR/blob/1292c8a9562764d34ee4504b54d93248eb7346fe/inline-r/src/Data/Vector/SEXP.hs#L346-L374
>> and
>>
>>
>>
>> as a point of grounding this chat
>> the injective type familly in question is defined by the follwoing
>>
>>
>> --#if MIN_VERSION_base(4,9,0)type family Mutable <http://hackage.haskell.org/package/vector-0.12.0.2/docs/src/Data.Vector.Generic.Base.html#Mutable> (v <http://hackage.haskell.org/package/vector-0.12.0.2/docs/src/Data.Vector.Generic.Base.html#local-6989586621679032525> :: * -> *) = (mv <http://hackage.haskell.org/package/vector-0.12.0.2/docs/src/Data.Vector.Generic.Base.html#local-6989586621679032526> :: * -> * -> *) | mv -> v#elsetype family Mutable (v :: * -> *) :: * -> * -> *#endif
>>
>> anyways, it looks like the Pure / immutable vector data type in inline-r
>> has a spurious state token argument in its definition that shouldn't be
>> there, OR there need to be two "s" params in inline-r instead of the one
>>
>> heres the full code i linked to in question
>>
>>
>> -- | Mutable R vector. Represented in memory with the same header as
>> 'SEXP'
>>
>> -- nodes. The second type parameter is phantom, reflecting at the type
>> level the
>> -- tag of the vector when viewed as a 'SEXP'. The tag of the vector and
>> the
>> -- representation type are related via 'ElemRep'.
>> data MVector s ty a = MVector
>> { mvectorBase :: {-# UNPACK #-} !(SEXP s ty)
>> , mvectorOffset :: {-# UNPACK #-} !Int32
>> , mvectorLength :: {-# UNPACK #-} !Int32
>> }
>> -- | Internal wrapper type for reflection. First type parameter is the
>> reified
>> -- type to reflect.
>> newtype W t ty s a = W { unW :: MVector s ty a }
>> instance (Reifies t (AcquireIO s), VECTOR s ty a) => G.MVector (W t ty) a
>> where
>>
>> data Vector s (ty :: SEXPTYPE) a = Vector
>>     { vectorBase :: {-# UNPACK #-} !(ForeignSEXP ty) , vectorOffset ::
>> {-# UNPACK #-} !Int32 , vectorLength :: {-# UNPACK #-} !Int32
>> }
>>
>>
>> type instance G.Mutable (W t ty s) = Mutable.W t ty
>> Anyways, the fix here is to remove the s param from the Pure version of W
>> and "Sexp Vector"
>>
>>
>>
>> On Sat, Dec 29, 2018 at 6:16 PM Carter Schonwald <
>> carter.schonwald at gmail.com> wrote:
>>
>>> were you using the same version of vector in both setups?
>>>
>>> in the most recent  vector release  we made mutable type family
>>> injective in the vector package for ghc's that support it ...
>>>
>>> On Sat, Dec 29, 2018 at 1:50 PM Dominick Samperi <djsamperi at gmail.com>
>>> wrote:
>>>
>>>> When I use v8.6.3 of GHC under Ubuntu to install the inline-r package
>>>> I get the error "Type family equation violates injectivity annotation,"
>>>> and
>>>> a type variable on the LHS cannot be inferred from the RHS, due to
>>>> the lack of injectivity (I suppose).
>>>>
>>>> On the other hand, v8.0.2 of GHC (shipped with Haskell Platform under
>>>> Ubuntu) does not have this problem (it has other problems).
>>>>
>>>> Has something changed in the latest version of the compiler that might
>>>> cause this? Possible work-around?
>>>>
>>>> FYI, the line that triggers the error is:
>>>> type instance G.Mutable (W t ty s) = Mutable.W t ty
>>>>
>>>> The variable that cannot be inferred is 's'.
>>>>
>>>> Thanks,
>>>> Dominick
>>>> _______________________________________________
>>>> ghc-devs mailing list
>>>> ghc-devs at haskell.org
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>>
>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20181229/e6ec160d/attachment.html>


More information about the ghc-devs mailing list