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
- 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 -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 ofhr
. 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
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.