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: 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 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](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/ambiguous_types.html?highlight=switching%20off#ambiguous-types-and-the-ambiguity-check): "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 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.