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).