Note [Evidence terms from Unsatisfiable Givens]

An Unsatisfiable Given constraint, of the form [G] Unsatisfiable msg, should be
able to solve ANY Wanted constraint whatsoever.

Recall that we have

  unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep)
                .  Unsatisfiable msg => a

We want to use this function, together with the evidence
[G] unsat_ev :: Unsatisfiable msg, to solve any other constraint [W] wtd_ty.

We could naively think that a valid evidence term for the Wanted might be:

  wanted_ev = unsatisfiable @{rep} @msg @wtd_ty unsat_ev

Unfortunately, this is a kind error: "wtd_ty :: CONSTRAINT rep", but
"unsatisfiable" expects the third type argument to be of kind "TYPE rep".

Instead, we use a boxing data constructor to box the constraint into a type.
In the end, we construct the following evidence for the implication:

  [G] unsat_ev :: Unsatisfiable msg
    ==>
      [W] wtd_ev :: wtd_ty

  wtd_ev =
    case unsatisfiable @{LiftedRep} @msg @(Dict ((##) -=> wtd_ty)) unsat_ev of
      MkDictBox ct -> ct (# #)

Note that we play the same trick with the function arrow -=> that we did
in order to define "unsatisfiable" in terms of "unsatisfiableLifted", as described
in Note [The Unsatisfiable representation-polymorphism trick] in base:GHC.TypeError.
This allows us to indirectly box constraints with different representations
(such as primitive equality constraints).