Problems with ISubset in vinyl

Question

I have the following code:

type Drawable = '["object" ::: Object, "transform" ::: M44 GL.GLfloat]
objXfrm :: "transform" ::: M44 GL.GLfloat
objXfrm = Field
objRec :: "object" ::: Object
objRec = Field

drawObject :: (Drawable `ISubset` a) => M44 GL.GLfloat -> PlainRec a -> IO ()
drawObject camera obj =
    withVAO vao $ do
        GL.currentProgram $= Just (program shdr)
        setUniforms shdr (modelView =: (rGet objXfrm obj !*! camera))
        GL.polygonMode $= (GL.Line, GL.Line)
        GL.drawElements GL.Triangles inds GL.UnsignedInt nullPtr
    where Object {objVAO = vao, objNumIndices = inds, objShader = shdr}
              = rGet objRec obj

When I get rid of the type on drawObject it compiles fine, but with the type I get

  Could not deduce (IElem * ("transform" ::: V4 (V4 GL.GLfloat)) a)
      arising from a use of `rGet'
    from the context (ISubset * Drawable a)
...
  Could not deduce (IElem * ("object" ::: Object) a)
      arising from a use of `rGet'
    from the context (ISubset * Drawable a)

The type that GHC deduces for me is

drawObject
  :: (IElem * ("object" ::: Object) rs,
      IElem * ("transform" ::: V4 (V4 GL.GLfloat)) rs) =>
     V4 (V4 GL.GLfloat)
     -> Rec rs Data.Functor.Identity.Identity -> IO ()

And that works fine as a type signature, but the one with ISubset does not. The error is exactly the same if I interchange the arguments to ISubset. What is going on here?

Answer 1

Looking at the source code for Vinyl, IElem x xs (which is a synonym for Implicit (Elem x xs)) has two instances:

instance Implicit (Elem x (x ': xs)) where
    implicitly = Here
instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where
    implicitly = There implicitly

Note that there is no mention of Subset here. Logically, (x ∈ xs) ∧ (xs ⊆ ys) ⇒ (x ∈ ys), but since there is no instance with the signature Implicit (Subset xs ys), Implicit (Elem x xs) => Implicit (Elem x ys), Haskell has no way of inferring the appropriate instance. Furthermore, no such instance can be written because doing so would result in some nasty instance overlap.

As a possible workaround, we can manipulate the membership witnesses (Elem and Subset) directly in order to force the appropriate instances (this is totally untested, and may fail miserably):

{-# LANGUAGE RankNTypes, ScopedTypeVariables, and possibly more... #-}

-- Lift an Elem value to a constraint.
withElem :: Elem x xs -> (forall r. IElem x xs => r) -> r
withElem Here x = x
withElem (There e) x = withElem e x

-- Witness of (x ∈ xs) ⇒ (xs ⊆ ys) ⇒ (x ∈ ys)
subsetElem :: Elem x xs -> Subset xs ys -> Elem x ys
subsetElem Here (SubsetCons e _) = e
subsetElem (There e) (SubsetCons _ s) = There (subsetElem e s)

-- Utility for retrieving Elem values from Fields (:::).
fieldElem :: IElem x xs => x -> Elem x xs
fieldElem _ = implicitly

inSubset :: IElem x xs => x -> Subset xs ys -> (forall r. IElem x ys => r) -> r
inSubset f s x = withElem (subsetElem (fieldElem f) s) x

drawObject :: forall a. (Drawable `ISubset` a) => M44 GL.GLfloat-> PlainRec a -> IO ()
drawObject camera obj =
    inSubset objRec subset $
    inSubset objXfrm subset $
        -- The desired instances should now be available here
        ...
  where
    subset = implicitly :: Subset Drawable a
    ...

Answer 2

From briefly looking over the Vinyl code, it seems that the whole "subset" idea hasn't been completely implemented (meaning, there are more functions and instances needed for it to be really useful). Could you not just use the "subtype" relationship between records instead? Then you can do

drawObject :: (PlainRec a <: PlainRec Drawable) => M44 GL.GLfloat -> PlainRec a -> IO ()
drawObject camera obj' =
    ... -- as before
  where
    obj :: PlainRec Drawable
    obj = cast obj'
    ... -- rest as before