I was playing around with Bluefin today when I found this curious case of type inference not working in HLS’s eval plugin and ghci:
module Bluefin.Examples.Experiments where
import Bluefin.State (get, put, runState)
-- Inferred type: multAdd :: (e :> es, Num b) => b -> b -> State b e -> Eff es b
multAdd x y st = do
s0 <- get st
put st (x * s0 + y * s0)
get st
-- Inferred type: multAdd' :: Eff es (Integer, Integer)
multAdd' = runState 1 $ multAdd 3 4
-- >>> :t runState 1 $ multAdd 3 4
-- Couldn't match expected type: forall (e :: Effects).
-- State s_a1dvX[sk:1] e -> Eff (e :& es_a1dvY[sk:1]) a_a1dvZ[sk:1]
-- with actual type: State b0_a1dw3[tau:1] e0_a1dw1[tau:1]
-- -> Eff es0_a1dw2[tau:1] b0_a1dw3[tau:1]
-- In the first argument of `($)', namely `runState 1'
-- In the expression: runState 1 $ multAdd 3 4
-- >>> :t runState 1 (multAdd 3 4)
-- runState 1 (multAdd 3 4) :: Num a => Eff es (a, a)
It looks like the culprit is the ($) operator, since removing it makes the type query succeed. But why? And why only in ghci/HLS?
Hi Ramiro, Bluefin author here. I can’t manage to replicate the failing behaviour. Could you post a log of a GHCi session where you see it (including the version of GHC)?
In short, the reason is the lack of generalization. The second argument of runState should be of type forall e. State s e -> Eff (e :& es) r, but in the failing cases, all that it is getting is State s e0 -> Eff (e0 :& es) r for some unknown e0. GHC is not “generalizing” that, by adding on the forall e0. for you.
That’s normally expected when you go “through” another function or operator, but $ is special: GHC has a special case to allow its argument to generalize.
So, I see this:
ghci> :t runState 1 $ multAdd 3 4
runState 1 $ multAdd 3 4 :: Num a => Bluefin.Internal.Eff es (a, a)
ghci> let a $$ b = a b
ghci> :t runState 1 $$ multAdd 3 4
<interactive>:1:1: error:
• Couldn't match expected type: forall (e :: Bluefin.Internal.Effects).
Bluefin.Internal.State s e
-> Bluefin.Internal.Eff (e Bluefin.Internal.:& es) a
with actual type: Bluefin.Internal.State b0 e0
-> Bluefin.Internal.Eff es0 b0
• In the first argument of ‘($$)’, namely ‘runState 1’
In the expression: runState 1 $$ multAdd 3 4
i.e. any other application operator than literally $ breaks inference. But I don’t know why your $ doesn’t work. If you can post a GHCi log perhaps I’ll be able to work it out. It’s also worth checking what happens on other versions of GHC.
1 Like
Sure, here goes a full log of the session. I’m using ghc 9.12.2:
[rama@tarkus:~/git/personal/bluefin/bluefin-examples]$ cabal repl
Configuration is affected by cabal.project at
'/home/rama/git/personal/bluefin'.
Build profile: -w ghc-9.12.2 -O1
In order, the following will be built (use -v for more details):
- bluefin-examples-0.2.0.0 (interactive) (lib) (configuration changed)
Configuring library for bluefin-examples-0.2.0.0...
Preprocessing library for bluefin-examples-0.2.0.0...
GHCi, version 9.12.2: https://www.haskell.org/ghc/ :? for help
[1 of 9] Compiling Bluefin.Examples.CloneableHandle ( src/Bluefin/Examples/CloneableHandle.hs, interpreted )
[2 of 9] Compiling Bluefin.Examples.DB ( src/Bluefin/Examples/DB.hs, interpreted )
[3 of 9] Compiling Bluefin.Examples.DslBuilder.Robots ( src/Bluefin/Examples/DslBuilder/Robots.hs, interpreted )
[4 of 9] Compiling Bluefin.Examples.Experiments ( src/Bluefin/Examples/Experiments.hs, interpreted )
src/Bluefin/Examples/Experiments.hs:6:1: warning: [GHC-38417] [-Wmissing-signatures]
Top-level binding with no type signature:
multAdd :: (e bluefin-internal-0.3.4.0:Bluefin.Internal.:> es,
Num b) =>
b
-> b
-> bluefin-internal-0.3.4.0:Bluefin.Internal.State b e
-> bluefin-internal-0.3.4.0:Bluefin.Internal.Eff es b
|
6 | multAdd x y st = do
| ^^^^^^^
src/Bluefin/Examples/Experiments.hs:12:1: warning: [GHC-38417] [-Wmissing-signatures]
Top-level binding with no type signature:
multAdd' :: bluefin-internal-0.3.4.0:Bluefin.Internal.Eff
es (Integer, Integer)
|
12 | multAdd' = runState 1 $ multAdd 3 4
| ^^^^^^^^
src/Bluefin/Examples/Experiments.hs:12:21: warning: [GHC-18042] [-Wtype-defaults]
• Defaulting the type variable ‘a0’ to type ‘Integer’ in the following constraints
(Num a0)
arising from the literal ‘1’
at src/Bluefin/Examples/Experiments.hs:12:21
(Num a0)
arising from a use of ‘multAdd’
at src/Bluefin/Examples/Experiments.hs:12:25-31
• In the first argument of ‘runState’, namely ‘1’
In the first argument of ‘($)’, namely ‘runState 1’
In the expression: runState 1 $ multAdd 3 4
|
12 | multAdd' = runState 1 $ multAdd 3 4
| ^
[5 of 9] Compiling Bluefin.Examples.HandleReader ( src/Bluefin/Examples/HandleReader.hs, interpreted )
[6 of 9] Compiling Bluefin.Examples.Random ( src/Bluefin/Examples/Random.hs, interpreted )
[7 of 9] Compiling Bluefin.Examples.Stream.InsideAndOut ( src/Bluefin/Examples/Stream/InsideAndOut.hs, interpreted )
[8 of 9] Compiling Bluefin.Examples.Stream.Many ( src/Bluefin/Examples/Stream/Many.hs, interpreted )
[9 of 9] Compiling Bluefin.Examples.Terminal ( src/Bluefin/Examples/Terminal.hs, interpreted )
Ok, 9 modules loaded.
ghci> :l Bluefin.Examples.Experiments
[1 of 1] Compiling Bluefin.Examples.Experiments ( src/Bluefin/Examples/Experiments.hs, interpreted )
src/Bluefin/Examples/Experiments.hs:6:1: warning: [GHC-38417] [-Wmissing-signatures]
Top-level binding with no type signature:
multAdd :: (e bluefin-internal-0.3.4.0:Bluefin.Internal.:> es,
Num b) =>
b
-> b
-> bluefin-internal-0.3.4.0:Bluefin.Internal.State b e
-> bluefin-internal-0.3.4.0:Bluefin.Internal.Eff es b
|
6 | multAdd x y st = do
| ^^^^^^^
src/Bluefin/Examples/Experiments.hs:12:1: warning: [GHC-38417] [-Wmissing-signatures]
Top-level binding with no type signature:
multAdd' :: bluefin-internal-0.3.4.0:Bluefin.Internal.Eff
es (Integer, Integer)
|
12 | multAdd' = runState 1 $ multAdd 3 4
| ^^^^^^^^
src/Bluefin/Examples/Experiments.hs:12:21: warning: [GHC-18042] [-Wtype-defaults]
• Defaulting the type variable ‘a0’ to type ‘Integer’ in the following constraints
(Num a0)
arising from the literal ‘1’
at src/Bluefin/Examples/Experiments.hs:12:21
(Num a0)
arising from a use of ‘multAdd’
at src/Bluefin/Examples/Experiments.hs:12:25-31
• In the first argument of ‘runState’, namely ‘1’
In the first argument of ‘($)’, namely ‘runState 1’
In the expression: runState 1 $ multAdd 3 4
|
12 | multAdd' = runState 1 $ multAdd 3 4
| ^
Ok, one module loaded.
ghci> :t runState 1 $ multAdd 3 4
<interactive>:1:1: error: [GHC-83865]
• Couldn't match expected type: forall (e :: bluefin-internal-0.3.4.0:Bluefin.Internal.Effects).
bluefin-internal-0.3.4.0:Bluefin.Internal.State s e
-> bluefin-internal-0.3.4.0:Bluefin.Internal.Eff
(e bluefin-internal-0.3.4.0:Bluefin.Internal.:& es) a
with actual type: bluefin-internal-0.3.4.0:Bluefin.Internal.State
b0 e0
-> bluefin-internal-0.3.4.0:Bluefin.Internal.Eff es0 b0
• In the first argument of ‘($)’, namely ‘runState 1’
In the expression: runState 1 $ multAdd 3 4
ghci>
Thanks. That helped me discover that it seems to be a 9.12 issue. It is fine in 9.10 and 9.14 as you can see below. Maybe it’s worth a bug report, but I don’t know. GHC GitLab new issue
% cabal repl -w ghc-9.10 -b bluefin
...
ghci> import Bluefin.State
ghci> :t runState () $ const (pure ())
runState () $ const (pure ()) :: Bluefin.Internal.Eff es ((), ())
ghci>
Leaving GHCi.
% cabal repl -w ghc-9.12.2 -b bluefin
...
ghci> import Bluefin.State
ghci> :t runState () $ const (pure ())
<interactive>:1:1: error: [GHC-83865]
• Couldn't match expected type: forall (e :: Bluefin.Internal.Effects).
State () e -> Bluefin.Internal.Eff (e Bluefin.Internal.:& es) a
with actual type: b0 -> f0 ()
• In the first argument of ‘($)’, namely ‘runState ()’
In the expression: runState () $ const (pure ())
% cabal repl -w ghc-9.14 -b bluefin
...
ghci> import Bluefin.State
ghci> :t runState () $ const (pure ())
runState () $ const (pure ()) :: Bluefin.Internal.Eff es ((), ())
1 Like
Here’s a simple way anyone can reproduce:
% cabal repl -w ghc-9.12.2 -b bluefin
...
ghci> import Bluefin.State
ghci> :t runState () $ const (pure ())
<interactive>:1:1: error: [GHC-83865]
• Couldn't match expected type: forall (e :: Bluefin.Internal.Effects).
State () e -> Bluefin.Internal.Eff (e Bluefin.Internal.:& es) a
with actual type: b0 -> f0 ()
• In the first argument of ‘($)’, namely ‘runState ()’
In the expression: runState () $ const (pure ())
1 Like
Thank you! Today I learnt something new about the type checker and the limits of generalization 
. I marked your second response as the answer, since this seems to be an issue with the specific GHC version I’m using.
You’re welcome! Hope you’re enjoying Bluefin. If you ever have any more questions feel free to ask here or on the Bluefin issue tracker. I’d also welcome your feedback on using Bluefin at the Bluefin discussion.
2 Likes