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 deadgiven 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
 Whether the type signatures pass the ambiguity check
 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 constrainta ~ 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
andg1
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.InteractinteractIrred 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 fdefertypeerrors

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 (fragilely) 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 uncallable function is on the left of an arrow, so it wan't cause problems for the caller ofhr
. Arguably, then, it should not give rise to any ambiguitycheck complaints. But under RestrictivePlan, if we also useXDeepSubsumption
I think we would get an error in the ambiguity check; and it is one that is hard to avoid. (With the default simplesubsumption 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
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 off
will get an ambiguous constraintEq alpha
. But a constraint likef :: (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.