type inference with OverloadedRecordDot

[jeukshi]

Hello. Just finished porting my little lib to Bluefin and so far I like it. So thanks!

I did encounter this behavior, but I am not sure what to do about it. I'm on GHC 9.6.6.

It is a minor annoyance, but, I guess, worth reporting.

data Env e = MkEnv {stateA :: State Int e}

runEnv
    :: Int
    -> (forall e. Env e -> Eff (e :& es) r)
    -> Eff es r
runEnv a action =
    evalState a $ \sA -> do
        useImplIn action MkEnv{stateA = mapHandle sA}

run :: Int
run = runPureEff do
    runEnv 1 \env -> do
        let sA = env.stateA
        a <- get sA -- This is fine.
        a' <- get (stateA env) -- This is fine.
        a'' <- get env.stateA
        {-  ^ This doesn't compile:
           error: [GHC-39999]
           • No instance for ‘e :> es’ arising from a use of ‘get’
             Possible fix:
               add (e :> es) to the context of
                 a type expected by the context:
                   forall (e :: Effects). Env e -> Eff (e :& es) Int -}
        return a

run2 :: Int
run2 = runPureEff do
    runEnv 1 \env -> do
        useEnv env
  where
    useEnv :: (e :> es) => Env e -> Eff es Int
    useEnv env = do
        a <- get env.stateA -- This is fine.
        return a

[tomjaguarpaw]

Interesting! This appears to be an awkward interaction between how GHC desugars record dot and the incoherent instances that Bluefin uses to encode its set index types. I simplified it to an example not involving record dot. I don't have any immediate plans to address this, because I'm skeptical that the situation can be improved, unfortunately.

Thank you for the report and please do file any other issues you come across, and feel free to ask any questions.

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE OverloadedRecordDot #-}

import Bluefin.Eff
import Bluefin.Compound
import Bluefin.State
import Prelude

data Env e = MkEnv {stateA :: State Int e}

runEnv
    :: Int
    -> (forall e. Env e -> Eff (e :& es) r)
    -> Eff es r
runEnv a action =
    evalState a $ \sA -> do
        useImplIn action MkEnv{stateA = mapHandle sA}

run :: ()
run = runPureEff $ do
    runEnv 1 $ \(env :: Env e') -> do
        -- Just a convenient way of getting es into scope
        (_ :: Eff es ()) <-
          let nested :: Eff es (Eff es ())
              nested = pure (pure ())
          in nested

        -- This is fine.
        _ <- get (stateA env)

        -- This is fine.
        _ <- get @e' (stateAClass env)

        -- This is fine.
        _ <- get @e' (env.stateA)

        -- These don't work
        _ <- get @e' @(e' :& es) (stateAClass env)
        _ <- get @_ @(e' :& es) (stateAClass env)
        _ <- get (stateAClass env)

        pure ()

class r ~ Env e => IsEnv e r

instance r ~ Env e => IsEnv e r

stateAClass :: IsEnv e r => r -> State Int e
stateAClass = stateA

[jeukshi]

I'm fine with this solution.

run :: ()
run = runPureEff $ do
    runEnv 1 $ \(env :: Env e') -> do
                _ <- get @e' (env.stateA)

Most likely, I'd still pass env to a function first, as Bluefin requires quite a bit of indentation for effects setup, so it is nice to reset it. Although this might be a common pattern.

run = runPureEff $ do
    runEnv 1 $ \(env :: Env e') -> do
                res <- doImportantStuff env
                s <- get @e' env.something --inspect env
                return (res, s)

In which case, maybe it is worth documenting somewhere.

I'm fine with closing this issue, but I'll leave it up to you.

[tomjaguarpaw]

I'm fine with this solution.

Great!

Bluefin requires quite a bit of indentation for effects setup

Yeah, it does, but remember you can use StateSource to avoid intending for each State.

maybe it is worth documenting somewhere.

Do you mean documenting the solution that uses @e'?

I'm fine with closing this issue, but I'll leave it up to you.

Let's leave it open for a bit, at least until I've put something in the documentation.

[jeukshi]

Yeah, it does, but remember you can use StateSource to avoid intending for each State.

You should rename it to BadCodeSource. At least that reflects how it works for me. Just kidding, tho, I'm loving it.

Do you mean documenting the solution that uses @e'?

There is a Tips section, so maybe there? In rare circumstances, TypeApplication may be required or something like that.

There is another tip I'd add, passing effects as values works really well with \cases from LambdaCase, as we can keep pattern matching on what is important:

funcWithEff eff = \cases
    True -> ...
    False -> ...

[tomjaguarpaw]

You should rename it to BadCodeSource. At least that reflects how it works for me.

😂 Do you mean you're starting to write C in Haskell?

Just kidding, tho, I'm loving it.

Great!

There is a Tips section, so maybe there? In rare circumstances, TypeApplication may be required or something like that.

Yes, I see. I'll have to think how to explain this one and where it should be placed, so that it's helpful but doesn't cause additional confusion by simply existing.

There is another tip I'd add, passing effects as values works really well with \cases from LambdaCase

Oh, interesting, do you have a more fleshed out example you can provide, so I can see what this looks like in a real usage?

[jeukshi]

😂 Do you mean you're starting to write C in Haskell?

I went full circle. Thanks, I guess.

Oh, interesting, do you have a more fleshed out example you can provide, so I can see what this looks like in a real usage?

The major complaint I see about The Handle Pattern is passing those handles around. But for me, it is pattern matching. Let's steal some AST for the internet.

data Exp
    = Number Int
    | Add Exp Exp
    | Subtract Exp Exp
    | Multiply Exp Exp
    | Divide Exp Exp
    deriving (Show)

eval :: Exp -> Int
eval (Number i) = undefined
eval (Add e1 e2) = undefined
eval (Subtract e1 e2) = undefined
eval (Multiply e1 e2) = undefined
eval (Divide e1 e2) = undefined

So far so good, let's add some state.

evalS :: (e :> es) => State Int e -> Exp -> Eff es Int
evalS s (Number i) = undefined
evalS s (Add e1 e2) = undefined
evalS s (Subtract e1 e2) = undefined
evalS s (Multiply e1 e2) = undefined
evalS s (Divide e1 e2) = undefined

How about exceptions?

evalSE
    :: (e1 :> es, e2 :> es)
    => State Int e1
    -> Exception SomeException e2
    -> Exp
    -> Eff es Int
evalSE s ex (Number i) = undefined
evalSE s ex (Add e1 e2) = undefined
evalSE s ex (Subtract e1 e2) = undefined
evalSE s ex (Multiply e1 e2) = undefined
evalSE s ex (Divide e1 e2) = undefined

So now I have those ss and exs that do "nothing". It's not the end of the world, but they do serve no purpose here, obscuring my intent on matching constructors of Exp. Not a problem for Effectful ;)

But \cases can do it.

evalSE'
    :: (e1 :> es, e2 :> es)
    => State Int e1
    -> Exception SomeException e2
    -> Exp
    -> Eff es Int
evalSE' s ex = \cases
    (Number i) -> undefined
    (Add e1 e2) -> undefined
    (Subtract e1 e2) -> undefined
    (Multiply e1 e2) -> undefined
    (Divide e1 e2) -> undefined

-- With multiple params too.
evalSE''
    :: (e1 :> es, e2 :> es)
    => State Int e1
    -> Exception SomeException e2
    -> Exp
    -> Int
    -> Eff es Int
evalSE'' s ex = \cases
    (Number i) n -> undefined
    (Add e1 e2) n -> undefined
    (Subtract e1 e2) n -> undefined
    (Multiply e1 e2) n -> undefined
    (Divide e1 e2) n -> undefined

It is not strictly the same, because I can't hide s and ex per branch, but that is a minor thing.

This code of mine is probably ugly and dysfunctional enough to be considered real world.

Bonus: I just learned this about \cases while writing the examples, so I might share as well. Oh.

f :: Int -> Int -> Int -> Int
f _ = \cases
    _ -> id