Type inference for nested bindings
This ticket is spun out from a side-saga in !10123.
In the package statistics
this extremely delicate function is in Statistic.Sample.Histogram
:
histogram_ :: (Num b, RealFrac a, G.Vector v0 a, G.Vector v1 b) =>
Int -> a -> a -> v0 a -> v1 b
histogram_ numBins lo hi xs0 = G.create (GM.replicate numBins 0 >>= bin xs0)
where
bin xs bins = go 0
where
go i | i >= len = return bins
| otherwise = do
let x = xs `G.unsafeIndex` i
b = truncate $ (x - lo) / d
write' bins b . (+1) =<< GM.read bins b
go (i+1)
write' bins' b !e = GM.write bins' b e
len = G.length xs
d = ((hi - lo) / fromIntegral numBins) * (1 + realToFrac m_epsilon)
Here bin
gets this inferred type:
bin :: forall {m1 :: * -> *} {v1 :: * -> *} {v2 :: * -> * -> *} {b1}.
(GM.PrimMonad m1, G.Vector v1 a)
=> v1 a -> v2 (GM.PrimState m1) b1 -> m (v2 (GM.PrimState m1) b1)
And go
ends up with this inferred type:
go :: forall m2. (GM.PrimState m2 ~ GM.PrimState m1, GM.PrimMonad m2)
=> Int -> m2 (v2 (GM.PrimState m1) b1)
Critically, go
has the following residual constraint
[W] Num b1
[W] GM.MVector v2 b1
The problem is that bin
is quantified over b1
, but not over Num b1
. So in the end we get a complaint that Num b1
isn't solvable, as indeed it isn't in
bin
's definition (which remember has a forall b1
at the top).
It is a mistake to quantify over b1
but not over constraints that mention b1
! Why does that happen? Because currently:
-
approximateWC
ignores all constraints under an equality
The function go
has just such an equality, so the approximateWC
for bin
sees:
WC { wc_simple = ...bin's simple constraints...
, wc_implict = IC { ic_info = "Binding for g"
, ic_skols = m2 -- g's foralls
, ic_givens = (PrimState m2 ~ PrimState m1), ...
, ic_wanteds = [W] Num b1, ... } }
Note that equality wrapping the Num b1
constraint.
Conclusion. Gah! With these doubly-nested definitions, type familes, etc, it is not surprising that type inference is terribly delicate.
The right solution
The right solution is to add type signatures. Here they are. So much simpler than the ones GHC infers, and they make the code vastly easier to understand:
histogram_ :: forall a b v0 v1.
(Num b, RealFrac a, G.Vector v0 a, G.Vector v1 b) =>
Int -> a -> a -> v0 a -> v1 b
bin :: forall s. v0 a -> Mutable v1 s b -> ST s (Mutable v1 s b)
go :: Int -> ST s (Mutable v1 s b)
We need a couple of extra imports to support these signatures:
import Control.Monad.ST( ST )
import Data.Vector.Generic.Base( Mutable )
The "make GHC cleverer" solution
We can make approximateWC
a bit cleverer. Read Note [ApproximateWC]
in
GHC.Tc.Solver. You'll see that the reason for not
floating a constraint past an equality is really all about equality
constraints.
However, we can probably float class constraints just fine. In general, abstracting over too many constraints is fine -- it just moves them to the call site.
The ice is thin here. But in these very subtle situations, it's best to write a type signature anyway.
When partial type signatures are involved, it's even more tricky: see #19106 (closed).