Treat '_' consistently in type declarations

GHC doesn't treat _ consistently in type declarations

-- Example A
data T _ = MkT            -- Not allowed

-- Example B
class C a where
  type T a

-- Example C
instance C [_] where         -- Not allowed
  type T [_] = Int           -- Not allowed

-- Example D
data family D a
data instance D [_] = MkD   -- Allowed

-- Example E
type family F a
type instance F [_] = Int   -- Allowed

This seems inconsistent and annoying (see email thread).

Really, we should consistently treat _ in a binding position simply as a binder that binds nothing, just like at the term level.

But in Haskell 98 _ is a reserved identifier, so these programs are illegal. We use PartialTypeSignatures to allow _ in occurrence positions in types. Should the same flag enable _ in binding positions? It would seem a little odd to require PartialTypeSignatures for (A) and (C).

Any suggestions?

A couple of wrinkles. First, since _ binds nothing, it certainly doesn't bind occurrences of _. Thus for example, with PartialTypeSignatures

instance C [_] where
  op = .... (let f :: _ -> _
                f = e
             in ...) ...

The occurrences of _ in op's RHS are not bound by the _ in the instance header. (The would be if all three were a, say.) Rather the occurrences of _ are holes in the type signature and should be separately reported as such.

Second, the implementation would be tricky in one spot:

class C a where
  type T a

instance C (Either _ _) where
  type T (Either _ _) = ...

We must check that the type family instance is at the same type as the class. Do we want to insist that it looks exactly the same, or would you be allowed to say this?

instance C (Either _ _) where
  type T (Either a b) = a -> b

My instinct is to say "exactly the same" for now anyway.