Re: [ANNOUNCE] GHC 9.4.1-rc1 is now available

2022-07-22 Thread Ben Gamari
George Colpitts  writes:

> Hi Ben,
>
> I expected https://gitlab.haskell.org/ghc/ghc/-/issues/21506 (ghc-9.4.1-alpha1
> does not install on macos: ghc-pkg-9.4.0-20220501 cannot be opened because
> the developer cannot be verified) to be fixed in rc1 but it is not. Are my
> expectations wrong? What is the ETA for fixing it?
>
Thanks for letting us know, George. The fix that we have [1] is present
in 9.4.1-rc1. If that commit doesn't resolve the issue then there is
something that we don't understand. Does `/usr/bin/xattr` exist? Running
`xattr -rc` manually on the binary distribution allow you to run the
compiler?

Cheers,

- Ben


[1] 
https://gitlab.haskell.org/ghc/ghc/-/commit/641972d65b476aac11424bde6c3bcfda1c65aef5



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: [ANNOUNCE] GHC 9.4.1-rc1 is now available

2022-07-22 Thread George Colpitts
Hi Ben,

I expected https://gitlab.haskell.org/ghc/ghc/-/issues/21506 (ghc-9.4.1-alpha1
does not install on macos: ghc-pkg-9.4.0-20220501 cannot be opened because
the developer cannot be verified) to be fixed in rc1 but it is not. Are my
expectations wrong? What is the ETA for fixing it?

Thanks
George


On Fri, Jul 22, 2022 at 10:05 AM Ben Gamari  wrote:

>
> The GHC developers are happy to announce the availability of the first
> (and likely last) release candidate of GHC 9.4.1. Binary distributions,
> source
> distributions, and documentation are available at [downloads.haskell.org].
>
> This major release will include:
>
>  - A new profiling mode, `-fprof-late`, which adds automatic cost-center
>annotations to all top-level functions *after* Core optimisation has
>run. This provides informative profiles while interfering
>significantly less with GHC's aggressive optimisations, making it
>easier to understand the performance of programs which depend upon
>simplification..
>
>  - A variety of plugin improvements including the introduction of a new
>plugin type, *defaulting plugins*, and the ability for typechecking
>plugins to rewrite type-families.
>
>  - An improved constructed product result analysis, allowing unboxing of
>nested structures, and a new boxity analysis, leading to less reboxing.
>
>  - Introduction of a tag-check elision optimisation, bringing
>significant performance improvements in strict programs.
>
>  - Generalisation of a variety of primitive types to be levity
>polymorphic. Consequently, the `ArrayArray#` type can at long last be
>retired, replaced by standard `Array#`.
>
>  - Introduction of the `\cases` syntax from [GHC proposal 0302]
>
>  - A complete overhaul of GHC's Windows support. This includes a
>migration to a fully Clang-based C toolchain, a deep refactoring of
>the linker, and many fixes in WinIO.
>
>  - Support for multiple home packages, significantly improving support
>in IDEs and other tools for multi-package projects.
>
>  - A refactoring of GHC's error message infrastructure, allowing GHC to
>provide diagnostic information to downstream consumers as structured
>data, greatly easing IDE support.
>
>  - Significant compile-time improvements to runtime and memory consumption.
>
>  - On overhaul of our packaging infrastructure, allowing full
>traceability of release artifacts and more reliable binary
>distributions.
>
>  - Reintroduction of deep subsumption (which was previously dropped with
> the
>*simplified subsumption* change) as a language extension.
>
>  - ... and much more. See the [release notes] for a full accounting.
>
> Note that, as 9.4.1 is the first release for which the released artifacts
> will
> all be generated by our Hadrian build system, it is possible that there
> will be
> packaging issues. If you enounter trouble while using a binary
> distribution,
> please open a [ticket]. Likewise, if you are a downstream packager, do
> consider
> migrating to [Hadrian] to run your build; the Hadrian build system can be
> built
> using `cabal-install`, `stack`, or the in-tree [bootstrap script]. We will
> be
> publishing a blog post describing the migration process to Hadrian in the
> coming weeks.
>
> We would like to thank Microsoft Azure, GitHub, IOG, the Zw3rk
> stake pool, Tweag I/O, Serokell, Equinix, SimSpace, the Haskell
> Foundation, and other anonymous contributors whose on-going financial
> and in-kind support has facilitated GHC maintenance and release
> management over the years. Finally, this release would not have been
> possible without the hundreds of open-source contributors whose work
> comprise this release.
>
> As always, do give this release a try and open a [ticket] if you see
> anything amiss.
>
> Happy testing,
>
> - Ben
>
> [downloads.haskell.org]: https://downloads.haskell.org/ghc/9.4.1-rc1/
> [GHC proposal 0302]:
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0302-cases.rst
> [ticket]: https://gitlab.haskell.org/ghc/ghc/-/issues/new
> [bootstrap script]:
> https://gitlab.haskell.org/ghc/ghc/-/blob/e2520df3fffa0cf22fb19c5fb872832d11c07d35/hadrian/bootstrap/README.md
> [Hadrian]:
> https://gitlab.haskell.org/ghc/ghc/-/blob/e2520df3fffa0cf22fb19c5fb872832d11c07d35/hadrian
> [release notes]:
> https://downloads.haskell.org/~ghc/9.4.1-rc1/docs/users_guide/9.4.1-notes.html
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Wildcards in type synonyms

2022-07-22 Thread Richard Eisenberg


> On Jul 22, 2022, at 4:53 AM, Simon Peyton Jones  
> wrote:
> 
> expand them during
> typechecking,

Just to expand on this point (haha): your new type macros (distinct from type 
synonyms) would have to be eagerly expanded during type checking. You say this 
(quoted above), but I wanted to highlight that this is in opposition to the way 
today's type synonyms work, which are expanded only when necessary. (Rationale: 
programmers probably want to retain the very clever synonym name they came up 
with, which is hopefully easier to reason about.)

Interestingly, type macros may solve another problem that has come up recently: 
Gershom proposed (a quick search couldn't find where this was, but it was 
around restoring deep-subsumption behavior) a change to the way polytypes work 
in type synonyms. Specifically, he wondered about, e.g.

type T a = forall b. b -> Either a b

meaning to take the `forall b` and lift it to the top of whatever type T 
appears in. So that

f :: [a] -> T a

would really mean

f :: forall a b. [a] -> b -> Either a b

and not

f :: forall a. [a] -> forall b. b -> Either a b

as it does today. With deep subsumption, you can spot the difference between 
these types only with type applications, but they are incomparable types with 
simple subsumption.

At the time, I didn't understand what the semantics of Gershon's new type 
synonyms were, but in the context of Gergo's type macros, they make sense. To 
wit, we could imagine

type T a = b -> Either a b

Note: b is unbound. This is actually a type *macro*, not a type synonym, and it 
expands to a form that mentions a free variable b. (Presumably, this b would 
not capture a b in scope at the usage site.) This macro behavior delivers what 
Gershom was looking for.

I'm not saying Gergo should necessarily implement this new aspect of type 
macros (that don't mention wildcards), but if this ever does come to a 
proposal, I think these kind of variables are a new motivator for such a 
proposal. I'd probably favor some explicit notation to introduce a macro (e.g. 
`type macro T a = Either _ a`) instead of using a syntactic marker like the 
presence of a _ or an unbound variable, but we can debate that later.

Good luck with the implementation, Gergo!
Richard___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


[ANNOUNCE] GHC 9.4.1-rc1 is now available

2022-07-22 Thread Ben Gamari

The GHC developers are happy to announce the availability of the first
(and likely last) release candidate of GHC 9.4.1. Binary distributions, source
distributions, and documentation are available at [downloads.haskell.org].

This major release will include:

 - A new profiling mode, `-fprof-late`, which adds automatic cost-center
   annotations to all top-level functions *after* Core optimisation has
   run. This provides informative profiles while interfering
   significantly less with GHC's aggressive optimisations, making it
   easier to understand the performance of programs which depend upon
   simplification..

 - A variety of plugin improvements including the introduction of a new
   plugin type, *defaulting plugins*, and the ability for typechecking
   plugins to rewrite type-families.

 - An improved constructed product result analysis, allowing unboxing of
   nested structures, and a new boxity analysis, leading to less reboxing.

 - Introduction of a tag-check elision optimisation, bringing
   significant performance improvements in strict programs.

 - Generalisation of a variety of primitive types to be levity
   polymorphic. Consequently, the `ArrayArray#` type can at long last be
   retired, replaced by standard `Array#`.

 - Introduction of the `\cases` syntax from [GHC proposal 0302]

 - A complete overhaul of GHC's Windows support. This includes a
   migration to a fully Clang-based C toolchain, a deep refactoring of
   the linker, and many fixes in WinIO.

 - Support for multiple home packages, significantly improving support
   in IDEs and other tools for multi-package projects.

 - A refactoring of GHC's error message infrastructure, allowing GHC to
   provide diagnostic information to downstream consumers as structured
   data, greatly easing IDE support.

 - Significant compile-time improvements to runtime and memory consumption.

 - On overhaul of our packaging infrastructure, allowing full
   traceability of release artifacts and more reliable binary
   distributions.

 - Reintroduction of deep subsumption (which was previously dropped with the
   *simplified subsumption* change) as a language extension.

 - ... and much more. See the [release notes] for a full accounting.

Note that, as 9.4.1 is the first release for which the released artifacts will
all be generated by our Hadrian build system, it is possible that there will be
packaging issues. If you enounter trouble while using a binary distribution,
please open a [ticket]. Likewise, if you are a downstream packager, do consider
migrating to [Hadrian] to run your build; the Hadrian build system can be built
using `cabal-install`, `stack`, or the in-tree [bootstrap script]. We will be
publishing a blog post describing the migration process to Hadrian in the
coming weeks.

We would like to thank Microsoft Azure, GitHub, IOG, the Zw3rk
stake pool, Tweag I/O, Serokell, Equinix, SimSpace, the Haskell
Foundation, and other anonymous contributors whose on-going financial
and in-kind support has facilitated GHC maintenance and release
management over the years. Finally, this release would not have been
possible without the hundreds of open-source contributors whose work
comprise this release.

As always, do give this release a try and open a [ticket] if you see
anything amiss.

Happy testing,

- Ben

[downloads.haskell.org]: https://downloads.haskell.org/ghc/9.4.1-rc1/
[GHC proposal 0302]: 
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0302-cases.rst
 
[ticket]: https://gitlab.haskell.org/ghc/ghc/-/issues/new
[bootstrap script]: 
https://gitlab.haskell.org/ghc/ghc/-/blob/e2520df3fffa0cf22fb19c5fb872832d11c07d35/hadrian/bootstrap/README.md
[Hadrian]: 
https://gitlab.haskell.org/ghc/ghc/-/blob/e2520df3fffa0cf22fb19c5fb872832d11c07d35/hadrian
[release notes]: 
https://downloads.haskell.org/~ghc/9.4.1-rc1/docs/users_guide/9.4.1-notes.html



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Wildcards in type synonyms

2022-07-22 Thread Simon Peyton Jones
>
> So it seems that instead of shoehorning it into the existing type
> synonyms, a better bet would be to branch off to a separate path quite
> early (maybe as soon as during renaming), expand them during
> typechecking, and *not* touch how/when existing "normal" type synonyms
> are resolved.
>

That sounds plausible, yes.

Simon

On Fri, 22 Jul 2022 at 09:50, Gergő Érdi  wrote:

> Thanks Simon, these are very useful hints. My plan is to just push
> ahead on a separate fork, with this "macro semantics", and maybe if it
> comes out nicer than I'd hope, I'll propose it.
>
> So it seems that instead of shoehorning it into the existing type
> synonyms, a better bet would be to branch off to a separate path quite
> early (maybe as soon as during renaming), expand them during
> typechecking, and *not* touch how/when existing "normal" type synonyms
> are resolved.
>
> On Fri, Jul 22, 2022 at 4:14 PM Simon Peyton Jones
>  wrote:
> >
> > Hi Gergo
> >
> >> I'd like to implement type synonyms containing wildcards. The idea is
> >> that if you have `type MySyn a = MyType a _ Int`, then during
> >> typechecking, every occurrence of `MySyn T` would be expanded into
> >> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
> >
> >
> > I imagine you mean that if you then write
> > f :: MySyn a -> a -> Int
> > then it's exactly as if you wrote (using PartialTypeSignatures)
> > f :: MyType a _ Int -> a -> Int
> > today.   So if I understand it right, you intend that these type
> synonyms are second-class citizens: they can occur precisely (and only)
> where wildcards are allowed to occur today.  For example, as Iavor
> suggests, you'd reject
> > data T a = MkT (MySyn a)
> >
> > If you want to do this in a fork of GHC, that's obviously fine. If you
> want to offer it as a language extension, the best thing would be to write
> a GHC Proposal.  Also you'd get a lot of useful design feedback that way,
> which might save you implementation cycles.
> >
> >> What is the reason for this? I would have expected type synonyms to be
> >> only relevant during typechecking, and then fully resolved in the
> >> elaborated Core output.
> >
> >
> > In GHC an Id has only one type.   It does not have a "source type" and a
> "Core type".  So we allow Core types to contain synonyms so that when we
> export that Id the importing scope (e.g. GHCi, and type error messages) can
> see it.  Synonyms can also allow types to take less space. E.g.  we have
> Type, where (if we fully expanded) we'd have to have (TYPE LiftedRep).  One
> could imagine a different design.
> >
> > I would expect that, by the time typechecking is over, all your wildcard
> synonyms are gone.  They really are second class.
> >
> > Just to mention too that the entire "wildcards in type signatures" story
> is (I think) jolly useful, but it also turned out to be pretty tricky to
> implement.  If you just macro-expand your new synonyms, you won't disturb
> the wildcard story, but I just wanted to advertise that it's a tricky area.
> >
> > Simon
> >
> > On Fri, 22 Jul 2022 at 07:30, ÉRDI Gergő  wrote:
> >>
> >> Hi,
> >>
> >> I'd like to implement type synonyms containing wildcards. The idea is
> >> that if you have `type MySyn a = MyType a _ Int`, then during
> >> typechecking, every occurrence of `MySyn T` would be expanded into
> >> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
> >>
> >> One worrying thing I noticed in my initial exploration of the GHC
> >> codebase is that the Core representation of `Type`s can still contain
> >> type synonym occurrences. And this doesn't seem like just an artefact
> >> of sharing the `Type` representation with `TcType`, since the
> >> `coreView` function also has code to look through type synonyms.
> >>
> >> What is the reason for this? I would have expected type synonyms to be
> >> only relevant during typechecking, and then fully resolved in the
> >> elaborated Core output. If that were the case, then a new version of
> >> `expand_syn` could live in `TcM` and take care of making these fresh
> >> metavariables.
> >>
> >> Beside this concrete question, taking a step back, I would also like
> >> to hear from people who know their way around this part of GHC, what
> >> they think about this and how they'd approach implementing it.
> >>
> >> Thanks,
> >>  Gergo
> >> ___
> >> ghc-devs mailing list
> >> ghc-devs@haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >
> > ___
> > ghc-devs mailing list
> > ghc-devs@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Wildcards in type synonyms

2022-07-22 Thread Gergő Érdi
Thanks Simon, these are very useful hints. My plan is to just push
ahead on a separate fork, with this "macro semantics", and maybe if it
comes out nicer than I'd hope, I'll propose it.

So it seems that instead of shoehorning it into the existing type
synonyms, a better bet would be to branch off to a separate path quite
early (maybe as soon as during renaming), expand them during
typechecking, and *not* touch how/when existing "normal" type synonyms
are resolved.

On Fri, Jul 22, 2022 at 4:14 PM Simon Peyton Jones
 wrote:
>
> Hi Gergo
>
>> I'd like to implement type synonyms containing wildcards. The idea is
>> that if you have `type MySyn a = MyType a _ Int`, then during
>> typechecking, every occurrence of `MySyn T` would be expanded into
>> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>
>
> I imagine you mean that if you then write
> f :: MySyn a -> a -> Int
> then it's exactly as if you wrote (using PartialTypeSignatures)
> f :: MyType a _ Int -> a -> Int
> today.   So if I understand it right, you intend that these type synonyms are 
> second-class citizens: they can occur precisely (and only) where wildcards 
> are allowed to occur today.  For example, as Iavor suggests, you'd reject
> data T a = MkT (MySyn a)
>
> If you want to do this in a fork of GHC, that's obviously fine. If you want 
> to offer it as a language extension, the best thing would be to write a GHC 
> Proposal.  Also you'd get a lot of useful design feedback that way, which 
> might save you implementation cycles.
>
>> What is the reason for this? I would have expected type synonyms to be
>> only relevant during typechecking, and then fully resolved in the
>> elaborated Core output.
>
>
> In GHC an Id has only one type.   It does not have a "source type" and a 
> "Core type".  So we allow Core types to contain synonyms so that when we 
> export that Id the importing scope (e.g. GHCi, and type error messages) can 
> see it.  Synonyms can also allow types to take less space. E.g.  we have 
> Type, where (if we fully expanded) we'd have to have (TYPE LiftedRep).  One 
> could imagine a different design.
>
> I would expect that, by the time typechecking is over, all your wildcard 
> synonyms are gone.  They really are second class.
>
> Just to mention too that the entire "wildcards in type signatures" story is 
> (I think) jolly useful, but it also turned out to be pretty tricky to 
> implement.  If you just macro-expand your new synonyms, you won't disturb the 
> wildcard story, but I just wanted to advertise that it's a tricky area.
>
> Simon
>
> On Fri, 22 Jul 2022 at 07:30, ÉRDI Gergő  wrote:
>>
>> Hi,
>>
>> I'd like to implement type synonyms containing wildcards. The idea is
>> that if you have `type MySyn a = MyType a _ Int`, then during
>> typechecking, every occurrence of `MySyn T` would be expanded into
>> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>>
>> One worrying thing I noticed in my initial exploration of the GHC
>> codebase is that the Core representation of `Type`s can still contain
>> type synonym occurrences. And this doesn't seem like just an artefact
>> of sharing the `Type` representation with `TcType`, since the
>> `coreView` function also has code to look through type synonyms.
>>
>> What is the reason for this? I would have expected type synonyms to be
>> only relevant during typechecking, and then fully resolved in the
>> elaborated Core output. If that were the case, then a new version of
>> `expand_syn` could live in `TcM` and take care of making these fresh
>> metavariables.
>>
>> Beside this concrete question, taking a step back, I would also like
>> to hear from people who know their way around this part of GHC, what
>> they think about this and how they'd approach implementing it.
>>
>> Thanks,
>>  Gergo
>> ___
>> ghc-devs mailing list
>> ghc-devs@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Wildcards in type synonyms

2022-07-22 Thread Simon Peyton Jones
Hi Gergo

I'd like to implement type synonyms containing wildcards. The idea is
> that if you have `type MySyn a = MyType a _ Int`, then during
> typechecking, every occurrence of `MySyn T` would be expanded into
> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>

I imagine you mean that if you then write
f :: MySyn a -> a -> Int
then it's exactly as if you wrote (using PartialTypeSignatures)
f :: MyType a _ Int -> a -> Int
today.   So if I understand it right, you intend that these type synonyms
are second-class citizens: *they can occur precisely (and only) where
wildcards are allowed to occur today*.  For example, as Iavor suggests,
you'd reject
data T a = MkT (MySyn a)

If you want to do this in a fork of GHC, that's obviously fine. If you want
to offer it as a language extension, the best thing would be to write a GHC
Proposal.  Also you'd get a lot of useful design feedback that way, which
might save you implementation cycles.

What is the reason for this? I would have expected type synonyms to be
> only relevant during typechecking, and then fully resolved in the
> elaborated Core output.
>

In GHC *an Id has only one type*.   It does not have a "source type" and a
"Core type".  So we allow Core types to contain synonyms so that when we
export that Id the importing scope (e.g. GHCi, and type error messages) can
see it.  Synonyms can also allow types to take less space. E.g.  we have
Type, where (if we fully expanded) we'd have to have (TYPE LiftedRep).  One
could imagine a different design.

I would expect that, by the time typechecking is over, all your wildcard
synonyms are gone.  They really are second class.

Just to mention too that the entire "wildcards in type signatures" story is
(I think) jolly useful, but it also turned out to be pretty tricky to
implement.  If you just macro-expand your new synonyms, you won't disturb
the wildcard story, but I just wanted to advertise that it's a tricky area.

Simon

On Fri, 22 Jul 2022 at 07:30, ÉRDI Gergő  wrote:

> Hi,
>
> I'd like to implement type synonyms containing wildcards. The idea is
> that if you have `type MySyn a = MyType a _ Int`, then during
> typechecking, every occurrence of `MySyn T` would be expanded into
> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>
> One worrying thing I noticed in my initial exploration of the GHC
> codebase is that the Core representation of `Type`s can still contain
> type synonym occurrences. And this doesn't seem like just an artefact
> of sharing the `Type` representation with `TcType`, since the
> `coreView` function also has code to look through type synonyms.
>
> What is the reason for this? I would have expected type synonyms to be
> only relevant during typechecking, and then fully resolved in the
> elaborated Core output. If that were the case, then a new version of
> `expand_syn` could live in `TcM` and take care of making these fresh
> metavariables.
>
> Beside this concrete question, taking a step back, I would also like
> to hear from people who know their way around this part of GHC, what
> they think about this and how they'd approach implementing it.
>
> Thanks,
>  Gergo
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Wildcards in type synonyms

2022-07-22 Thread ÉRDI Gergő

On Fri, 22 Jul 2022, Iavor Diatchki wrote:


I've implemented such a feature in Cryptol, not GHC, so it is quite doable, but 
I
think the implementation would be easier if you decided on the overall design 
of the
feature first.


I'm hoping the details pretty much fall out from what it would mean if I 
used the existing PartialTypeSignatures extension to write 'MyData T _ Int`

at those places.


Some things to consider:
  * these kind of "existential" variable make sense in other type signatures, 
not just
type synonyms
   * there might be some contexts where you may want to disallow such wildcards 
(e.
g., in a data declaration)
   * you have to be careful with the scoping of type variables.  For example, 
you
should not unify an existential/wildcard variable with a type that refers to 
variables
that are not in scope of the wildcard.  I don't remember if GHC already has a 
system
for such things, but in Cryptol we implanted this by having each unification 
variable
keep track of the quantified variables that it may depend on.___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Wildcards in type synonyms

2022-07-22 Thread Iavor Diatchki
Hello,

I've implemented such a feature in Cryptol, not GHC, so it is quite doable,
but I think the implementation would be easier if you decided on the
overall design of the feature first.

Some things to consider:
  * these kind of "existential" variable make sense in other type
signatures, not just type synonyms
   * there might be some contexts where you may want to disallow such
wildcards (e. g., in a data declaration)
   * you have to be careful with the scoping of type variables.  For
example, you should not unify an existential/wildcard variable with a type
that refers to variables that are not in scope of the wildcard.  I don't
remember if GHC already has a system for such things, but in Cryptol we
implanted this by having each unification variable keep track of the
quantified variables that it may depend on.

Hope this helps,
Iavor

On Fri, Jul 22, 2022, 09:30 ÉRDI Gergő  wrote:

> Hi,
>
> I'd like to implement type synonyms containing wildcards. The idea is
> that if you have `type MySyn a = MyType a _ Int`, then during
> typechecking, every occurrence of `MySyn T` would be expanded into
> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>
> One worrying thing I noticed in my initial exploration of the GHC
> codebase is that the Core representation of `Type`s can still contain
> type synonym occurrences. And this doesn't seem like just an artefact
> of sharing the `Type` representation with `TcType`, since the
> `coreView` function also has code to look through type synonyms.
>
> What is the reason for this? I would have expected type synonyms to be
> only relevant during typechecking, and then fully resolved in the
> elaborated Core output. If that were the case, then a new version of
> `expand_syn` could live in `TcM` and take care of making these fresh
> metavariables.
>
> Beside this concrete question, taking a step back, I would also like
> to hear from people who know their way around this part of GHC, what
> they think about this and how they'd approach implementing it.
>
> Thanks,
>  Gergo
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Wildcards in type synonyms

2022-07-22 Thread ÉRDI Gergő

Hi,

I'd like to implement type synonyms containing wildcards. The idea is
that if you have `type MySyn a = MyType a _ Int`, then during
typechecking, every occurrence of `MySyn T` would be expanded into
`MyType T w123 Int`, with a fresh type (meta)variable `w123`.

One worrying thing I noticed in my initial exploration of the GHC
codebase is that the Core representation of `Type`s can still contain
type synonym occurrences. And this doesn't seem like just an artefact
of sharing the `Type` representation with `TcType`, since the
`coreView` function also has code to look through type synonyms.

What is the reason for this? I would have expected type synonyms to be
only relevant during typechecking, and then fully resolved in the
elaborated Core output. If that were the case, then a new version of
`expand_syn` could live in `TcM` and take care of making these fresh
metavariables.

Beside this concrete question, taking a step back, I would also like
to hear from people who know their way around this part of GHC, what
they think about this and how they'd approach implementing it.

Thanks,
Gergo
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs