Hint.interpret gives a compiler error when used on a Polysemy.Sem value

Question

I'm trying to compile Polysemy monad values at runtime using Hint (Language.Haskell.Interpreter).

When I try to do this I reliably get an error about improper use of the : operator in "interactive" code; it seems as if the text hint is passing to GHC has a syntax error in it.

{-# LANGUAGE DataKinds #-}

module Main where

import Polysemy (Embed, embed, runM, Sem)
import Language.Haskell.Interpreter (as, interpret, Interpreter, runInterpreter, setImportsQ)
import Data.Typeable (typeOf)
import Control.Monad.IO.Class (liftIO)

main :: IO ()
main = do
  -- Hint works fine to interpret a String:
  m <- interpretWithErrors exampleHint
  print m
  -- And Sem works fine:
  runM exampleSem
  -- But notice the weird detected type:
  print $ typeOf exampleSem
  -- And now Hint fails to interpret a Sem:
  s <- interpretWithErrors exampleBoth
  print $ typeOf s
  runM s

type MyEffect = Sem '[Embed IO] ()

exampleSem :: MyEffect
exampleSem = embed $ print "Successful Sem!"

exampleHint :: Interpreter String
exampleHint = do
  setImportsQ [("Prelude", Nothing)]
  interpret "\"Successful Hint!\"" (as :: String)

exampleBoth :: Interpreter MyEffect
exampleBoth = do
  setImportsQ [("Prelude", Nothing), ("Polysemy", Nothing)]
  liftIO $ print "Successfully imported!"
  -- This is where it fails:
  s <- interpret "embed $ print \"Success!\"" (as :: MyEffect)
  liftIO $ print "Successfully interpreted!"
  return s

interpretWithErrors :: Interpreter a -> IO a
interpretWithErrors i_a = do
  e_e_a <- runInterpreter i_a
  either (ioError . userError . show) (return) e_e_a

Running the above prints:

"Successful Hint!"
"Successful Sem!"
Sem (': ((* -> *) -> * -> *) (Embed IO) ('[] ((* -> *) -> * -> *))) ()
"Successfully imported!"
Hint-Polysemy: user error (WontCompile [GhcError {errMsg = "<interactive>:3:41: error: Operator applied to too few arguments: :"}])

Some notes:

• I'm using cabal, and in order to pass the import line within the interpreter monad I have to run this from within a cabal sandboxed shell because Polysemy isn't installed to my machine at large.
• That said, I don't think cabal or importing Polysemy is the problem. I can get the exact same error message as above if I just neglect to import Polysemy and just setImportsQ [("Prelude", Nothing)].
• The string I'm interpreting doesn't even need to be a valid expression; I can put jibberish in there without changing the error. This suggests to me that the problem is with (as :: MyEffect).
• I include typeOf to demonstrate that MyEffect is in fact Typeable.
• I have no idea why typeOf exampleSem is giving such a long and weird type signature. I do think that this somehow is the problem. Rearranging MyEffect to type MyEffect = Sem ((Embed IO) : []) () has no effect.

Is it clear to anyone if I'm doing something wrong? How should I try to debug this problem?
Supposing this were a bug in hint, polysemy, or (less likely) in Type.Reflection.Typeable, what would my next step be to try to fix it? I assume I'd somehow have to pin down which library it is that having the problem?

This is a refinement of an earlier question. Here's the original.

Answer 1

Not an answer, but I've made some discoveries which you might find helpful.

I thought it might be the bogus prefix type operator syntax ': x xs which is not valid Haskell (you would have to either write it infix or use (':)). So I implemented a SemWorkaround wrapper module which used Cons and Nil instead of the standard list syntax. Seemed like mostly the same problem with a more verbose error message (hmm).

Then I thought it might be the explicit kind application, since the error messages keep talking about things being given too many arguments. So I tried changing the type-level list representation to the way we used to do it back in the old days.

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}

module SemWorkaround where

import Polysemy (Sem, Embed)
import Data.Kind (Type)

data Nil 
data Cons (a :: (Type -> Type) -> Type -> Type) (as :: Type)

type family ListToList xs where
    ListToList Nil = '[]
    ListToList (Cons x xs) = x ': ListToList xs

newtype Sem' l a = Sem' { getSem' :: Sem (ListToList l) a }

And used Sem' to marshal the hint boundary. E.g.

type MyEffect' = Sem' (Cons (Embed IO) Nil) ()

...

s <- interpret "Sem' . embed $ print \"Success\"" (as :: MyEffect')
pure $ getSem' s

This worked. So it seems like whoever is producing the type is emitting an explicit kind argument for polymorphic lifted constructors, but the consumer is expecting it to be implicit. To confirm I changed the workaround module to use a monomorphic datakind List.

data List
    = Nil
    | Cons ((Type -> Type) -> Type -> Type) List

Which again worked.

Finally, I tested the infix problem just to be sure by changing it to:

data List
    = Nil
    | ((Type -> Type) -> Type -> Type) ::: List

Which, to my surprise, failed with your familiar error message Operator applied to too few arguments. So it seems you have found two bugs. Somebody doesn't understand polykinds who should, and somebody doesn't understand type operators who should. I haven't dug deep enough to find out who is wrong.