Note [Case of cast]

Consider        case (x `cast` co) of b { I# ->
                ... (case (x `cast` co) of {...}) ...
We'd like to eliminate the inner case.  That is the motivation for
equation (2) in Note [Binder swap].  When we get to the inner case, we
inline x, cancel the casts, and away we go.

Historical Note [Care with binder-swap on dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This Note is now out-dated; it has been rendered irrelevant by
Note [Unary class magic] in GHC.Core.TyCon.  I'm leaving it here in
case we are every tempted to return to newtype classes.

This (historical) Note explains why we need isDictId in scrutOkForBinderSwap.
Consider this tricky example (#21229, #21470):

  class Sing (b :: Bool) where sing :: Bool
  instance Sing 'True  where sing = True
  instance Sing 'False where sing = False

  f :: forall a. Sing a => blah

  h = \ @(a :: Bool) ($dSing :: Sing a)
      let the_co =  Main.N:Sing[0] <a> :: Sing a ~R# Bool
      case ($dSing |> the_co) of wild
        True  -> f @'True (True |> sym the_co)
        False -> f @a     dSing

Now do a binder-swap on the case-expression:

  h = \ @(a :: Bool) ($dSing :: Sing a)
      let the_co =  Main.N:Sing[0] <a> :: Sing a ~R# Bool
      case ($dSing |> the_co) of wild
        True  -> f @'True (True |> sym the_co)
        False -> f @a     (wild |> sym the_co)

And now substitute `False` for `wild` (since wild=False in the False branch):

  h = \ @(a :: Bool) ($dSing :: Sing a)
      let the_co =  Main.N:Sing[0] <a> :: Sing a ~R# Bool
      case ($dSing |> the_co) of wild
        True  -> f @'True (True  |> sym the_co)
        False -> f @a     (False |> sym the_co)

And now we have a problem.  The specialiser will specialise (f @a d)a (for all
vtypes a and dictionaries d!!) with the dictionary (False |> sym the_co), using
Note [Specialising polymorphic dictionaries] in GHC.Core.Opt.Specialise.

The real problem is the binder-swap.  It swaps a dictionary variable $dSing
(of kind Constraint) for a term variable wild (of kind Type).  And that is
dangerous: a dictionary is a /singleton/ type whereas a general term variable is
not.  In this particular example, Bool is most certainly not a singleton type!

Conclusion:
  for a /dictionary variable/ do not perform
  the clever cast version of the binder-swap

Hence the subtle isDictId in scrutOkForBinderSwap.

Why this Note is now outdated.  Using Note [Unary class magic] in GHC.Core.TyCon
the program above becomes
  h = \ @(a :: Bool) ($dSing :: Sing a)
      case sing @a $dSing of (wild::Bool)
        True  -> f @'True $dSing
        False -> f @a     $dSing
so the issue of binder-swapping doesn't arise.

End of Historical Note.