I see I've collected a number of 👍s but no discussion. I've been keeping #3709 up to date when conflicts arise; is there anything else I can do to move this proposal along?

Sorry, but there isn’t really - I think it’s mostly that this is more of a ‘nice to have’ feature, and in particular it doesn’t enable anything which is not currently possible, which makes it difficult to justify prioritising maintainer time for it over certain other things (like, say, poly kinds, or getting try purescript updated, which I think is where most maintainer time has been going recently).

Those are indeed more worthy uses of maintainer time, if such time must be allocated exclusively to one or the other. I'll only ask that if it becomes feasible to take a few minutes to spin off some tasks—theoretical investigation, alternate implementations, whatever—that a non-maintainer can work on, please let me know!

I'm not opposed to this, but is there a significant advantage to desugaring to top-level declarations with name munging, vs just supporting them in the type checker under it's normal scoping? While it's true that it can be desugared this way (as a way to say it's equivalent to anything you can write now), it's not clear to me if this is actually advantageous or simpler than supporting it for "real".

Not necessarily. I do think it's simpler to specify as a desugaring, but to me, the main advantages of implementing this as a desugaring are sidestepping the anticipated objection against ‘future additions of type-level features’ and having more confidence that the patch doesn't introduce bugs into existing language features. Supporting type synonym scopes ‘natively’ probably would be less net complexity added than doing it with name mangling, if complexity in a desugaring step and complexity in the type checker core is weighted equally. But I'm assuming the maintainers take the view that complexity in the type checker core ought to have more weight—whether enough weight to justify some name mangling hacks, I can't say.

Speaking from the perspective of purs ide this would be a net-negative. We don't do contextual completions and would have to filter these type declarations even if the desugaring made them end up in the externs. This is obviously a consequence of the current simple design the IDE uses, but I think it's still something we need to be aware of.

I'd like to at least consider the question of which kinds of declarations we want to allow to be 'local' and which we don't. Right now it's just value declarations that can exist within a where or let, and with this proposal we would be allowing type synonym declarations to exist within a where or let too. What about if people propose allowing other kinds of declarations to exist within a local scope? I suppose data and class declarations are more difficult because you'd have to ensure that values whose types refer to them don't escape their scope, whereas with type synonyms that's less of an issue because you can just expand them. Instance declarations are global by nature, too, so it seems reasonable to disallow using them locally. You could maybe make a case for foreign import declarations for values but that seems like it would be a very minor change and probably not worth the effort. All this to say: I think it does make sense to only allow value and type declarations to exist in a local scope so actually we're probably fine on this front?

I'm also just a little concerned that this might complicate the work we'd like to do soonish to make type synonyms appear in error messages where appropriate, because we'd probably need to make sure that local type synonyms only appear in errors which arise somewhere where they are in scope, and outside of that scope they're expanded. But that's probably surmountable? Perhaps this suggests that it would be better to implement type synonym scopes 'natively' inside the type checker after all?

@kritzcreek would you have concerns with the IDE if this were implemented 'natively' inside the type checker, i.e. without the hoisting and name mangling?

@kritzcreek

We don't do contextual completions and would have to filter these type declarations

Forgive me, I know nothing about purs ide, but: what do you do for local value declarations, and why not do the same for local types?

@hdgarrood

I'd like to at least consider the question of which kinds of declarations we want to allow to be 'local' and which we don't.

Yeah, I largely agree with your conclusions. Local foreign imports seem silly to me, since they already presumably have to coexist in a top-level namespace in the foreign file, so there's really very little point to scoping them only on the PureScript side.

The motivating story for local data alone would probably be centered on defining local sum types that are very specifically coupled to an internal bit of computation, perhaps as a nicer alternative to purescript-variant. Concern with that would be, as you say, not letting the type escape, but IMO that wouldn't look too different from not letting existential type variables escape; I suspect local data could be implemented as a desugaring as well. But I think the best argument against it, if local type is a thing, is that hoisting the data yourself and then using local type and constructors to refer to it is not so bad.

I've done some idle speculation about a world with all of local data, instance, and class, and I think it could be done soundly if you restricted instances to be declared at either the scope of the data or the class, whichever is narrower. That opens up a set of use cases like creating an ad-hoc instance for a local newtype that uses local values in the instance members, which would be more compelling in terms of expressive power than local data alone. But this is a solution in search of a problem, for me.

Bottom line, I don't think there's much potential for nontrivial interaction between local type and any of local data, instance, or class. I wouldn't say let's never have local data/instance/class, but I do think it makes a lot more sense to start with type and possibly revisit those three as a group in the future, if someone can attest to needing them.

@kritzcreek would you have concerns with the IDE if this were implemented 'natively' inside the type checker, i.e. without the hoisting and name mangling?

Yeah the result wouldn't change. The IDE indexes and queries top-level identifiers. It doesn't do it on a per definition granularity.

Forgive me, I know nothing about purs ide, but: what do you do for local value declarations, and why not do the same for local types?

We don't do anything for local value declarations, that's what I'm saying. When I say net-negative I don't mean that things that used to work will stop working, but where you could previously go-to-definition, show kind etc. on every type since they're always toplevel, it's now only going to work for a subset of the types in your program. That's the net-negative

@natefaubion raised some polykinds-related questions over in #3709; I'd like to discuss them here.

The initial proposal assumed a context where unannotated type parameters in forall and in type declarations, if their kinds could not be inferred from the body of the forall/declaration, were inferred to have kind Type; this is no longer the case. So the question becomes, what to do about something like this:

foo :: forall f. Proxy f -> Int
foo _ = 0
  where
  type LocalApp a = f a

Per the proposal as currently written, this would be equivalent to

type HoistedLocalApp f a = f a
foo :: forall f. Proxy f -> Int
foo _ = 0

which leads to a generalized type warning.

After consideration, I think the best thing to do is to behave as if a t0 -> t1 kind for f were inferred, by analogy with something like

foo :: forall f. Proxy f -> Int
foo _ = 0
  where
  test = Proxy :: Proxy (f Int)

This means issuing no warnings, and making sure there is a unification error if foo is used in a way where f's kind can't unify with t0 -> t1.

I don't know if this is quite fatal for the desugaring approach, but it does seem to complicate matters. The saving grace might be that, weird pointless test cases aside, any practical real-world application would give the compiler enough information to infer the correct kind when the generalized hoisted local type is used. By which I mean, as soon as you actually have to use LocalApp in the example above:

foo :: forall f. Proxy f -> Int
foo _ = 0
  where
  type LocalApp a = f a
  test = Proxy :: Proxy (LocalApp Int)

the compiler now infers that f in foo's type has kind Type -> t0, and a foo (Proxy :: Proxy Type) causes TypesDoNotUnify.

So the question may be, how much do we care about pointless test cases where local type synonyms are declared but not used? If the answer is not at all, then I think desugaring otherwise behaves correctly as long as the generalization warning is suppressed for the prepended parameters in the hoisted type synonyms.

Anyone else have any thoughts?

Something else to consider is scoped type variables within kind signatures of local type synonyms.

foo :: forall k (a :: k). Proxy a -> ...
foo _ = ...
  where
  type Foo (b :: k) = ...

And by ‘consider’ you mean ‘support’, right? There would be no reason not to want that to work, would there?

Yes, it is something I would expect to work with PolyKinds. Kinds and types are in a unified namespace, so scoped type variables apply. This is tricky to do with desugaring steps. For example, scoped type variables and PolyKinds don't currently work together in class declaration bodies because the desugaring step happens before kind checking, so there is no (easy) way to tie the scope on the original class declaration to the desugared record synonym. Fixing this means delaying desugaring to when it is checked.

For reference, I think in order to support this in the type checker, one would need to:

• Update TypeChecker.Types.inferLetBinding to handle type synonym and kind signature declarations. This code already exists in TypeChecker.typeCheckAll, but I think we should avoid doing kind generalization in let bindings. bindLocalTypeVariables can be used to put the synonym in scope, and drop it when the scope is left.
• Update TypeChecker.Skolems.skolemizeTypesInValue to rewrite type synonym and kind signature declarations.

I don't think anything else would be necessary (however there can always be subtle cases to handle). Sugar.BindingGroups should already sort everything, and type synonyms will always appear before value declarations, and cycles are already disallowed between type synonyms.

I think that generalization should be avoided, because I think we should have a consistent rule for when it happens:

• Top-level declarations get generalized with a warning (both types and kinds).
• Let-bound declarations do not get generalized.

Just to be clear: when you propose that a let-bound type synonym not be generalized, do you mean that unconstrained type parameters have their kinds inferred from one use of the type synonym in the scope, the same way that local functions have their parameter types inferred? Or do you mean that unconstrained type parameters have kind Type, the way that type synonyms used to behave prior to PolyKinds?

The first. I don't think we should Type-default.

I think this is a great addition. This seems to be related to also allowing let and where in the type declaration as well like Rust allows.

fun
  :: forall a b.
  let A = {someLongFieldName :: a, anotherLongFieldName :: b}
      B = Either a b
      C = Tuple a b
  => C -> B -> A

It's been some time since this has been discussed. I think I'm for supporting this. There's been a few places where a local type synonym would clean up code in some where clauses.