Note [Specialising polymorphic dictionaries]

GHC/Core/Opt/Specialise.hs:2835 compiler 5 tickets

Note June 2023: This has proved to be quite a tricky optimisation to get right
see (#23469, #23109, #21229, #23445) so it is now guarded by a flag
`-fpolymorphic-specialisation`.

Consider
    class M a where { foo :: a -> Int }

    instance M (ST s) where ...
    dMST :: forall s. M (ST s)

    wimwam :: forall a. M a => a -> Int
    wimwam = /\a \(d::M a). body

    f :: ST s -> Int
    f = /\s \(x::ST s). wimwam @(ST s) (dMST @s) dx + 1

We'd like to specialise wimwam at (ST s), thus
    $swimwam :: forall s. ST s -> Int
    $swimwam = /\s. body[ST s/a, (dMST @s)/d]

    RULE forall s (d :: M (ST s)).
         wimwam @(ST s) d = $swimwam @s

Here are the moving parts:

(MP1) We must /not/ dump the CallInfo
        CIS wimwam (CI { ci_key = [@(ST s), dMST @s]
                       , ci_fvs = {dMST} })
      when we come to the /\s.  Instead, we simply let it continue to float
      upwards. Hence ci_fvs is an IdSet, listing the /Ids/ that
      are free in the call, but not the /TyVars/.  Hence using specArgFreeIds
      in singleCall.

  NB to be fully kosher we should explicitly quantifying the CallInfo
  over 's', but we don't bother.  This would matter if there was an
  enclosing binding of the same 's', which I don't expect to happen.

(MP2) When we come to specialise the call, we must remember to quantify
      over 's'.  That is done in the SpecType case of specHeader, where
      we add 's' (called qvars) to the binders of the RULE and the specialised
      function.

(MP3) If we have f :: forall m. Monoid m => blah, and two calls
        (f @(Endo b)      (d1 :: Monoid (Endo b))
        (f @(Endo (c->c)) (d2 :: Monoid (Endo (c->c)))
      we want to generate a specialisation only for the first.  The second
      is just a substitution instance of the first, with no greater specialisation.
      Hence the use of `removeDupCalls` in `filterCalls`.

      You might wonder if `d2` might be more specialised than `d1`; but no.
      This `removeDupCalls` thing is at the definition site of `f`, and both `d1`
      and `d2` are in scope. So `d1` is simply more polymorphic than `d2`, but
      is just as specialised.

      This distinction is sadly lost once we build a RULE, so `alreadyCovered`
      can't be so clever.  E.g if we have an existing RULE
            forall @a (d1:Ord Int) (d2: Eq a). f @a @Int d1 d2 = ...
      and a putative new rule
            forall (d1:Ord Int) (d2: Eq Int). f @Int @Int d1 d2 = ...
      we /don't/ want the existing rule to subsume the new one.

      So we sadly put up with having two rather different places where we
      eliminate duplicates: `alreadyCovered` and `removeDupCalls`.

All this arose in #13873, in the unexpected form that a SPECIALISE
pragma made the program slower!  The reason was that the specialised
function $sinsertWith arising from the pragma looked rather like `f`
above, and failed to specialise a call in its body like wimwam.
Without the pragma, the original call to `insertWith` was completely
monomorpic, and specialised in one go.

Wrinkles.

* See Note [Weird special case for SpecDict]

* With -XOverlappingInstances you might worry about this:
    class C a where ...
    instance C (Maybe Int) where ...   -- $df1 :: C (Maybe Int)
    instance C (Maybe a)   where ...   -- $df2 :: forall a. C (Maybe a)

    f :: C a => blah
    f = rhs

    g = /\a.  ...(f @(Maybe a) ($df2 a))...
    h = ...f @(Maybe Int) $df1

  There are two calls to f, but with different evidence.  This patch will
  combine them into one.  But it's OK: this code will never arise unless you
  use -XIncoherentInstances.  Even with -XOverlappingInstances, GHC tries hard
  to keep dictionaries as singleton types.  But that goes out of the window
  with -XIncoherentInstances -- and that is true even with ordianry type-class
  specialisation (at least if any inlining has taken place).

  GHC makes very few guarantees when you use -XIncoherentInstances, and its
  not worth crippling the normal case for the incoherent corner.  (The best
  thing might be to switch off specialisation altogether if incoherence is
  involved... but incoherence is a property of an instance, not a class, so
  it's a hard test to make.)

  But see Note [Specialisation and overlapping instances].

References 2

Referenced by 10