Note [Implementation of Unsatisfiable constraints]

The Unsatisfiable constraint was introduced in GHC proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst).
See Note [The Unsatisfiable constraint] in GHC.TypeError.

Its implementation consists of the following:

  A. The definitions.

     The Unsatisfiable class is defined in GHC.TypeError, in base.
     It consists of the following definitions:

       type Unsatisfiable :: ErrorMessage -> Constraint
       class Unsatisfiable msg where
         unsatisfiableLifted :: a

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

     The class TyCon as well as the unsatisfiable Id have known-key Names
     in GHC; they are not wired-in.

  B. Unsatisfiable instances.

     The Unsatisfiable typeclass has no instances (see GHC.Tc.Instance.Class.matchGlobalInst).

     Users are prevented from writing instances in GHC.Tc.Validity.check_special_inst_head.
     This is done using the same mechanism as for, say, Coercible or WithDict.

  C. Using [G] Unsatisfiable msg to solve any Wanted.

     In GHC.Tc.Solver.simplifyTopWanteds, after defaulting happens, when an
     implication contains Givens of the form [G] Unsatisfiable msg, and the
     implication supports term-level evidence (as per Note [Coercion evidence only]
     in GHC.Tc.Types.Evidence), we use any such Given to solve all the Wanteds
     in that implication. See GHC.Tc.Solver.useUnsatisfiableGivens.

     The way we construct the evidence terms is slightly complicated by
     Type vs Constraint considerations; see Note [Evidence terms from Unsatisfiable Givens]
     in GHC.Tc.Solver.

     The proposal explains why this happens after defaulting: if there are other
     ways to solve the Wanteds, we would prefer to use that, as that will make
     user programs "as defined as possible".

     Wrinkle [Ambiguity]

       We also use an Unsatisfiable Given to solve Wanteds when performing an
       ambiguity check. See the call to "useUnsatisfiableGivens" in
       GHC.Tc.Solver.simplifyAmbiguityCheck.

       This is, for example, required to typecheck the definition
       of "unsatisfiable" itself:

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

       The ambiguity check on this type signature will produce

         [G] Unsatisfiable msg1, [W] Unsatisfiable msg2

       and we want to ensure the Given solves the Wanted, to accept the definition.

       NB:

         An alternative would be to add a functional dependency on Unsatisfiable:

           class Unsatisfiable msg | -> msg

         Then we would unify msg1 and msg2 in the above constraint solving problem,
         and would be able to solve the Wanted using the Given in the normal way.
         However, adding such a functional dependency solely for this purpose
         could have undesirable consequences. For example, one might have

           [W] Unsatisfiable (Text "msg1"), [W] Unsatisfiable (Text "msg2")

         and W-W fundep interaction would produce the insoluble constraint

           [W] "msg1" ~ "msg2"

         which we definitely wouldn't want to report to the user.

  D. Adding "meth = unsatisfiable @msg" method bindings.

     When a class instance has an "Unsatisfiable msg" constraint in its context,
     and the user has omitted methods, we add method bindings of the form
     "meth = unsatisfiable @msg".
     See GHC.Tc.TyCl.Instance.tcMethods, in particular "tc_default".

     Example:

         class C a where { op :: a -> a }
         instance Unsatisfiable Msg => C [a] where {}

       elaborates to

         instance Unsatisfiable Msg => C [a] where { op = unsatisfiable @Msg }

       due to the (Unsatisfiable Msg) constraint in the instance context.

     We also switch off the "missing methods" warning in this situation.
     See "checkMinimalDefinition" in GHC.Tc.TyCl.Instance.tcMethods.

     Note that we do this even when there is a default method available. This
     ensures we run into the unsatisfiable error message when deferring type
     errors; otherwise we could end up with a runtime loop as seen in #23816.

  E. Switching off functional dependency coverage checks when there is
     an "Unsatisfiable msg" context.

     This is because we want to allow users to rule out certain instances with
     an "unsatisfiable" error, even when that would violate a functional
     dependency. For example:

       class C a b | a -> b
       instance Unsatisfiable (Text "No") => C a b

     See GHC.Tc.Instance.FunDeps.checkInstCoverage.

  F. Error reporting of "Unsatisfiable msg" constraints.

     This is done in GHC.Tc.Errors.reportWanteds: we detect when a constraint
     is of the form "Unsatisfiable msg" and just emit the custom message
     as an error to the user.

     This is the only way that "Unsatisfiable msg" constraints are reported,
     which makes their behaviour much more predictable than TypeError.