Note [Representing unary classes with newtypes: bad, bad, bad]

GHC/Core/TyCon.hs:1573 compiler 1 ticket

In the past we represented a unary class with a newtype, but that led to
some at least three really subtle bad consequences.

* Problem 1: When we represented unary classes via a newtype, the
    newtype axiom looked like
           t1::CONSTRAINT r ~ t2::TYPE r
    If TYPE and CONSTRAINT are apart, this can create unsoundness, via KindCo;
    see #21623.  Now we never make such a coercion, so that worry about TYPE
    being apart from CONSTRAINT has gone away entirely.  Hooray.

* Problem 2: a horrible hack in GHC.Core.Opt.OccurAnal.scrutOkForBinderSwap;
  see Historical Note [Care with binder-swap on dictionaries].
  Now the hack is gone.

* Problem 3: bogus specialisation.  The gory details are explained
  at https://gitlab.haskell.org/ghc/ghc/-/issues/23109#note_499130

  We had (using newtype classes)
     newtype SNat a = MKSNat Natural           -- axiom  snCo a :: SNat a ~ Natural
     class KNat a where { natSing :: SNat a }  -- axiom  knCo a :: KNat a ~ SNat a
  and a pattern match
    K @a (g : 32 ~ a+1) -> ...(foo @a (d :: KNat a))...
  where K is a data constructor binding `a` as an existential.

  In the code I was looking at, after lots of inlining an simplification, we find
  that (d::KNat a) is built like this:
    (d1 :: KNat 32)    = 32 |> sym (snCo 32) |> sym (knCo 32)
    (d2 :: SNat (a+1)) = d1 |> knCo g
    (d3 :: Natural)    = d2 |> snCo (a+1)
    (d4 :: Natural)    = d3 - 1
    (d  :: KNat a)     = d4 |> sym (snCo a) |> sym (knCo a)

  But d3 :: Natural = 32 |> (co's involving g) :: Natural ~ Natural
  and that is just Refl.  So we drop all the co's, including the crucial `g`,
  and just say d3 = 32; and
        d :: KNat a = (32-1) |> sym (snCo a) |> sym (knCo a)
  Now, we can float `d` outwards, crucially aided by polymorphic specialisation,
  (Note [Specialising polymorphic dictionaries] in GHC.Core.Opt.Specialise)
  and use that evidence to get an utterly bogus specialisation for the function
      foo :: forall b. KNat b => blah

  Solution: don't use newtype classes.  Then we get
    (d1 :: KNat 32)    = MkKN @32 (32 |> sym (snCo 32))
    (d2 :: SNat (a+1)) = natSing d1 |> SN g
    (d3 :: Natural)    = d2 |> snCo (a+1)
    (d4 :: Natural)    = d3 -1
    (d  :: KNat a)     = MkKN @a (d4 |> sym (snCo a))
  Now we don't get cancelling-out coercions.


************************************************************************
*                                                                      *
                 TyConRepName
*                                                                      *
********************************************************************* 

References 1

Referenced by 1