Don't zap naughty quantification candidates: error instead

Note [Naughty quantification candidates] in TcMType describes a scenario like forall arg. ... (alpha[tau] :: arg) ..., where alpha, a unification variable, has a bound skolem in its type. If alpha is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to Any.

However, we recently decided not to Any-ify in type declarations. And I think we are wrong to Any-ify here, too. We should just error. If not, we risk having Any leak in error messages, and it seems a nice goal not to ever let users see Any (short of TH or reflection or other dastardly deeds).

The example is partial-sigs/should_fail/T14040a. You can find the program in question at the top of #14040 (closed). #14040 (comment 168778) reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locally-bound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that tcHsPartialSigType was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions Any.

Here is a simpler test case:

foo :: forall (f :: forall a (b :: a -> Type). b _). f _
foo = foo

Note that the type of the first _ must be a, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get

    • Expected kind ‘k -> *’, but ‘f’ has kind ‘k -> Any @*’
    • In the type ‘f _’
      In the type signature:
        foo :: forall (f :: forall a (b :: a -> Type). b _). f _

This is correct enough, but there's Any in the error message. I think it would be much better just to reject the type signature a priori.

If I make the program correct (by wrapping the f _ in a call to Proxy, I get

Scratch.hs:44:50: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘Any @a :: a’
      Where: ‘a’ is a rigid type variable bound by
               ‘forall a (b :: a -> Type). b _’
               at Scratch.hs:44:28
    • In the first argument of ‘b’, namely ‘_’
      In the kind ‘forall a (b :: a -> Type). b _’
      In the type signature:
        foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
   |
44 | foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
   |                                                  ^

Scratch.hs:44:63: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘_ :: k’
      Where: ‘k’, ‘_’ are rigid type variables bound by
               the inferred type of
                 foo :: Proxy
                          @{Any @Type} (f @Type @((->) @{'LiftedRep} @{'LiftedRep} k) _)
               at Scratch.hs:45:1-9
    • In the first argument of ‘f’, namely ‘_’
      In the first argument of ‘Proxy’, namely ‘(f _)’
      In the type ‘Proxy (f _)’
   |
44 | foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
   |                                                               ^

More Anys. No! Reject!

What think you (for any value of you)?