Note [Decomposing newtypes a bit more aggressively]

GHC/Tc/Solver/Equality.hs:1257 compiler 1 ticket

IMPORTANT: the ideas in this Note are *not* implemented. Instead, the
current approach is detailed in Note [Decomposing newtype equalities]
and Note [Unwrap newtypes first].
For more details about the ideas in this Note see
  * GHC propoosal: https://github.com/ghc-proposals/ghc-proposals/pull/549
  * issue #22441
  * discussion on !9282.

Consider [G] c, [W] (IO Int) ~R (IO Age)
where IO is abstract, and
   newtype Age = MkAge Int   -- Not abstract
With the above rules, if there any Given Irreds,
the Wanted is insoluble because we can't decompose it.  But in fact,
if we look at the defn of IO, roughly,
    newtype IO a = State# -> (State#, a)
we can see that decomposing [W] (IO Int) ~R (IO Age) to
    [W] Int ~R Age
definitely does not lose completeness. Why not? Because the role of
IO's argment is representational.  Hence:

  DecomposeNewtypeIdea:
     decompose [W] (N s1 .. sn) ~R (N t1 .. tn)
     if the roles of all N's arguments are representational

If N's arguments really /are/ representational this will not lose
completeness.  Here "really are representational" means "if you expand
all newtypes in N's RHS, we'd infer a representational role for each
of N's type variables in that expansion".  See Note [Role inference]
in GHC.Tc.TyCl.Utils.

But the user might /override/ a phantom role with an explicit role
annotation, and then we could (obscurely) get incompleteness.
Consider

   module A( silly, T ) where
     newtype T a = MkT Int
     type role T representational  -- Override phantom role

     silly :: Coercion (T Int) (T Bool)
     silly = Coercion  -- Typechecks by unwrapping the newtype

     data Coercion a b where  -- Actually defined in Data.Type.Coercion
       Coercion :: Coercible a b => Coercion a b

   module B where
     import A
     f :: T Int -> T Bool
     f = case silly of Coercion -> coerce

Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose,
we'll get stuck with (Int ~R Bool).  Instead we want to use the
[G] (T Int) ~R (T Bool), which will be in the Irreds.

Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very
obscure incompleteness (above).  But no one is reporting a problem from
the lack of decompostion, so we'll just leave it for now.  This long
Note is just to record the thinking for our future selves.

References 3

Referenced by 1