On one hand, this change is very reasonable and I'd like to see it accepted.

On the other hand, it introduces an inconsistency with terms, where this continues to be accepted:

x = const :: a -> Bool -> a

I would, by analogy, expect this to be accepted:

type X = Const :: a -> Bool -> a

But with this proposal it will be rejected since a is not bound on the LHS. Well then, the term-level x should be rejected by the same reasoning.

I ran into something that seems relevant a couple weeks ago, so I'm curious how it would interact with this example:

data Relation n m = MkR

type Trans :: forall a b c . Relation a b -> Relation b c -> Relation a c
type family Trans pa pb where
  Trans rel MkR = rel -- this type checks but is a partial type family
  -- Trans @a @b @c rel MkR = rel -- this would not type check
  -- Trans @a @b @b rel MkR = rel -- this would type check

Am I understanding correctly that the equation that's not commented out here would not type check under this proposal? If so, I'd very much appreciate that change, since I found it extremely confusing when a type family that looked total judging by the lhss turned out not to be.

On the other hand, it introduces an inconsistency with terms, where this continues to be accepted

It doesn't introduce such an inconsistency, it merely continues it.

When you write (e :: a -> a) in a term, if a isn't already in scope, the forall-or-nothing rule adds foralls, thus e :: forall a. a->a.

But that doesn't happen after the :: in kind signatures. Consider

f :: forall a. Proxy (a :: k->k) -> Int

You might think that would mean

forall a. Proxy (a :: forall k. k->k) -> Int

but it doesn't. The outer :: wins, and we get

f :: forall k. forall (a :: k->k). Proxy a -> Int

We might consider changing that but I didn't think this was the place to do so.

Am I understanding correctly that the equation that's not commented out here would not type check under this proposal?

Yes you are! I've taken the liberty of adding your example to the proposal.

I do like seeing these things discussed :).

I was thinking we'd get there via #326 + #285 's NoPatternSignatureBinds, which would create the consistency @int-index worries about by prohibit the implicit binding in terms and types alike.

One of the interesting things to think about is that:

t2 = Just (Nothing :: Maybe a)

works not by immediately turning into

t2 @a = Just (Nothing :: Maybe a)

but by becoming

t2 = Just (Nothing :: forall a. Maybe a)

and then type inference instantiating that.

Besides some inline comments, there's a typo in the title of this PR itself (s/syononym/synonym/).

I'm in support. This is a nice simplification, enabled by the introduction of new syntax.

No comments for a month. @nomeata I'd like to submit this to the committee.

Hmm, I am confused. The proposal says “It depends on proposal #326 (Invisible parameters for declarations).” but #326 is still in draft state. Seems to be too early to submit #386 then?

Also, since #386 fixes problems that can’t be fixed without #326, if I am not mistaken, would it make sense to just make them part of #326?

Also, since #386 fixes problems that can’t be fixed without #326, if I am not mistaken, would it make sense to just make them part of #326?

I'd forgotten that. And John has dropped #326 for lack of time (NOT because it is controversial or unimportant). Bother maybe someone can pick up #326. Maybe even me. Anyone else?

I'd be happy to see them combined.

While modifying some code in GHC related to this proposal, I realized that Change #1 in this proposal doesn't really say what should happen to data family instances. For example, would this be illegal?

data family D (a :: k)
data instance D :: Maybe a -> Type

That is, you'd instead be expected to write this?

data instance D @(Maybe a) :: Maybe a -> Type

I think that's the case, based on my understanding of Change #1—the internals of GHC treat the :: Maybe a -> Type bit as part of the data instance's RHS. But this example was just different enough from the examples in this proposal that I'd thought I'd double-check.

I realized that Change #1 in this proposal doesn't really say what should happen to data family instances.

Ah yes, very true. It should be absolutely specific.

I think that data instances should be distinguishable (from each other) from the argument(s) to the left of the ::. So yes, these are all OK

data instance forall b. D @(Maybe b) :: Maybe b -> Type where ...
data instance D @[c] (d :: [c]) where ...
data instance D (e :: (p,q)) where ...

(The forall in the first is optional, just added for variation.)

But these are not OK.

data instance D :: Maybe b -> Type where ...
data instance D :: [c] -> Type where ...
data instance D :: (p,q) -> Type where ...