Note [Representing unary classes with newtypes: bad, bad, bad]
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
- Specialising polymorphic dictionaries GHC.Core.Opt.Specialise
Referenced by 1
- Unary class magic GHC.Core.TyCon