Type variables allowed to unify in a partial type signature (PartialTypeSignatures)

During a discussion today, Richard discovered the following bug:

The function f is accepted in GHC 8.2.1 (and HEAD too):

{-# LANGUAGE PartialTypeSignatures #-}

f :: a -> b -> _
f x y = [x, y]

with the warning:

Bug.hs:3:16: warning: [-Wpartial-type-signatures]
    • Found type wildcard ‘_’ standing for ‘[a]’
      Where: ‘a’ is a rigid type variable bound by
               the inferred type of f :: a -> a -> [a] at Bug.hs:4:1-13
    • In the type signature: f :: a -> b -> _
  |
3 | f :: a -> b -> _
  |                ^
Ok, 1 module loaded.

This is a regression compared to 8.0.1, where the following error is produced (rightly):

Bug.hs:4:12: error:
    • Couldn't match expected type ‘a’ with actual type ‘b’
      ‘b’ is a rigid type variable bound by
        the inferred type of f :: a -> b -> [a]
        at Bug.hs:3:6
      ‘a’ is a rigid type variable bound by
        the inferred type of f :: a -> b -> [a]
        at Bug.hs:3:6
    • In the expression: y
      In the expression: [x, y]
      In an equation for ‘f’: f x y = [x, y]
    • Relevant bindings include
        y :: b (bound at Bug.hs:4:5)
        x :: a (bound at Bug.hs:4:3)
        f :: a -> b -> [a]
          (bound at Bug.hs:4:1)
Failed, modules loaded: none.

Note that the inferred type of f is still correct: f :: a -> a -> a, but the type variables a and b are allowed to unify during inference, and they shouldn't be. If I understood correctly, this implies that when inferring the type of functions with partial type signatures, the type variables are (wrongly) treated as SigTvs, instead of skolem constants.

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire, simonpj
Operating system
Architecture