GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201215T12:32:56Zhttps://gitlab.haskell.org/ghc/ghc//issues/16775Don't zap naughty quantification candidates: error instead20201215T12:32:56ZRichard Eisenbergrae@richarde.devDon't zap naughty quantification candidates: error insteadNote [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 `partialsigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_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 locallybound 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: [Wpartialtypesignatures]
• 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: [Wpartialtypesignatures]
• 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:19
• 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 `Any`s. No! Reject!
What think you (for any value of you)?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 `partialsigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_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 locallybound 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: [Wpartialtypesignatures]
• 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: [Wpartialtypesignatures]
• 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:19
• 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 `Any`s. No! Reject!
What think you (for any value of you)?8.8.2