Insoluble constraints and dead code (again)

This ticket concerns GHC's treatment of insoluble constraints, a dark corner but alas one that is not unoccupied. Relevant prior discussion:

• #17543: a careful discussion of dead code
• #12466 (closed): examples where dead-given signatures might show up

Consider these definitions:

  f :: (Int ~ Bool) => Int -> Bool
  f x = f x

  g1 :: (Int ~ Bool) => Int -> Bool
  g1 x = f x

  g2 :: (Bool ~ Int) => Int -> Bool
  g2 x = f x

  h :: (Int ~ Bool) => Int -> Bool
  h x = x

Currently, GHC accepts f and g1 but rejects g2 and h. This is wildly inconsistent.

There are two things to consider

1. Whether the type signatures pass the ambiguity check
2. Whether the value definitions (e.g. g2 x = f x) typecheck

Background

Reminder: t1 ~ t2 is a class constraint for a class that behaves much as if we had:

   class (a ~# b) => a ~ b where {}
   instance (a ~# b) => a ~ b

So

• The unboxed coercion (a ~# b) is superclass of the boxed dictionary constraint a ~ b.
• To solve (a ~ b) we can instead solve (a ~# b), and box up the result.

Typechecking the terms: item 2

Let's begin with (2), assuming that the type signatures are accepted. Here's what happens:

• In f and g1 we have:

  [G] Int ~ Bool
  [W] Int ~ Bool

  and we solve the Wanted from the Given.

• In g2 we have

  [G] Int ~ Bool
  [W] Bool ~ Int

  The Wanted is not precisely equal to the Given, so we instead simplify to

  [W] Bool ~# Int

  We do have available [G] Int ~# Bool (via the superclass of [G] Int ~ Bool), but we always decline to use a Given to solve an insoluble Wanted. We could change that, but it's a deliberate choice in GHC.Tc.Solver.Interact

    interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
      | isInsolubleReason reason
               -- For insolubles, don't allow the constraint to be dropped
               -- which can happen with solveOneFromTheOther, so that
               -- we get distinct error messages with -fdefer-type-errors

• In h we have

  [G] Int ~ Bool
  [W] Int ~# Bool

  Just like in g2 we decline to use the Given to solve the insoluble Wanted.

So whether we reject or not is dependent in a very fragile way on (a) the orientation of the Wanted (Int ~ Bool), and (b) whether we decompose it to Int ~# Bool. The latter should be utterly innocuous, and indeed in !10415 (closed) I am decomposing equalities t1 ~ t2 into primitive equalities t1 ~~ t2 much more aggressively than before (for good, but unrelated, reasons).

Gah! We should either accept them all (by solving the Wanteds from the (unsatisfiable) Givens), or reject them all.

The ambiguity check: item 1

The user manual says: "even with ambiguity checking switched off -XAllowAmbiguousTypes, GHC will complain about a function that can never be called, such as this one:"

  f :: (Int ~ Bool) => a -> a

This simply isn't true. Function f above is accepted with or without -XAllowAmbiguousTypes. Why? Because the ambiguity check tries, in effect, to typecheck the definition f = f, which gives rise to

  [G] Int ~ Bool
  [W] Int ~ Bool

which, as we have seen, is (fragile-ly) accepted.

So GHC isn't obeying its own user manual.

What to do

There seem to be two consistent courses of action:

• PermissivePlan: allow insoluble Wanteds to be solved from (identical) insoluble Givens. This would accept all four definitions above.
• RestrictivePlan: do not allow insoluble Wanteds to be solved (at all). This would reject all four definitions.

RestrictivePlan is simple and consistent. But:

• It would reject some programs that are currently accepted, which might annoy some people.
• In particular, the ambiguity check would reject the above type signatures, just as the user manual claims. One possiblity is to say that -XAllowAmbiguousTypes would simply drop the ambiguity check altogether (just like it says!), so you could use that to accept such signatures.
• Consider the signature hr :: ((Int~Bool) => Int -> Bool) -> Int. Now the un-callable function is on the left of an arrow, so it wan't cause problems for the caller of hr. Arguably, then, it should not give rise to any ambiguity-check complaints. But under RestrictivePlan, if we also use -XDeepSubsumption I think we would get an error in the ambiguity check; and it is one that is hard to avoid. (With the default simple-subsumption there is no problem -- we drop to equality.)
• See #12466 (closed) and #17543

PermissivePlan might annoy fewer people, but:

• It is a bit fragile. For example consider

  [G] Int ~# Bool
  [W] F Int ~# Int

  and suppose we have type instance F Bool = Int. Maybe we can use that Given to rewrite the Wnated to [W] F Bool ~# Int, and now we could solve it. But we really, really are not going to do this. It would be difficult. The most we can do is solve an insoluble Wanted from an identical Given.
• It defers type errors. Ambiguity checking rejects f :: Eq a => Int -> Int on the grounds that caller of f will get an ambiguous constraint Eq alpha. But a constraint like f :: (Int~Bool) => blah is even worse: the caller has no chance of satisfying that! So if we like the ambiguity check at all, we should like it even more for insoluble constraints.