Allow type variables to declared out of dependency order

[goldfirere]

Rendered

[simonpj]

What about forall (a:k). forall k. blah. Is that ok? Currently nested foralls behave identically to foralls with multiple binders.

It's not just implementation difficulty! Core, and Core types, are by design as simple and compositional as possible. I'm uncomfortable with having source language types that are notationally and behaviourally different. (Especially with higher rank and impredicative polymorphism.)

I have not thought hard about this but the design here looks unattractive to me, even aside from the implementation consequences.

[goldfirere]

forall (a:k). forall k. blah would be rejected. But your statement that nested foralls always work like foralls with multiple binders is already far from true today:

f1 :: forall a. forall b. blah
f2 :: forall a b. blah

f1 gets a in scope in its definition; f2 gets a and b in scope.

data X where
  K1 :: forall a. forall b. blah
  K2 :: forall a b. blah

K1 is rejected while K2 is accepted.

There may be other places, too, where we make this distinction.

I'm afraid I don't see the Haskell-level difficulty here. (I do easily see the Core-level difficulty!) Do you have another example you're unsure of?

[Bj0rnen]

At least as a thought experiment, as far as I can tell, one way to implement this is by first implementing #99.

Once you have that, this proposal can be implemented by e.g. desugaring

typeRep :: forall (a :: k) k. Typeable a => TypeRep a

to

typeRep :: forall {k'} (a :: k') k. k ~ k' => Typeable a => TypeRep a

Or, if as an extension to #99 you can also name type variables multiple times (semantics should be quite clear):

typeRep :: forall {k} (a :: k) k. Typeable a => TypeRep a

If that desugaring makes sense, and isn't exceedingly hard to implement (I haven't put much thought into it), then it's more a matter of what syntax to expose to the end user. The #99 syntax doesn't necessarily need to be exposed, even if it's used under the hood.

[nomeata]

Little activity recently, marking this as dormant.