Re: Use of forall as a sigil

Hi Richard, > In the end, I've never loved the forall ... -> syntax, but I've never seen > anything better. What about the forall @a. syntax? For example: sizeOf :: forall @a. Sized a => Int We already use @ to explicitly specify types, so it seems natural mark type parameters that must be

Questions about System F and data types

Hi, I know that this is probably not the correct place to ask as my question is not directly related to GHC itself, but I thought here are the people that can most likely answer this. To better understand PL papers, especially those involving System Fc and its extensions, I started to write a for

Re: Use of forall as a sigil

I have thought about this too, and don't believe it has been widely discussed. - We are already getting `forall {a}.`, so it fits nicely with that. - However, it would have to be `forall @a ->`, because `forall a.` is already an invisible quantification, unless one wants to just change the me

RE: Use of forall as a sigil

Hi John, > - We are already getting `forall {a}.`, so it fits nicely with that. Interesting, I wasn't aware of this. Could you point me to the relevant proposal? > - However, it would have to be `forall @a ->`, Oh, that seems even worse than `forall a ->` to me. > because `forall a.` is alre

Re: Use of forall as a sigil

For me, the problem with `forall @a .` is that it seems to go in the wrong direction: parameters declared with @ must not have @ when passed, and parameters declared without @ must have a @ if the parameter is passed explicitly. However, if we say that @ makes a thing that is normally implicit

Re: Questions about System F and data types

> On Nov 22, 2020, at 6:49 AM, Jan van Brügge wrote: > To better understand PL papers, especially those involving System Fc and its > extensions, I started to write a formal proof of type safety including > alpha-equivalence. Currently I have a complete proof for System F >

Re: Adding a way to reduce type families in type errors

> On Nov 21, 2020, at 10:38 PM, Jakob Brünker wrote: > > Three questions: > - Is there already a way to do this that I'm missing? Not that I'm aware of. GHC sometimes expands type families and sometimes doesn't. The general philosophy has been that expanding type families is usually good an

Re: Adding a way to reduce type families in type errors

Ah, the result produced by !4149 does indeed look good. Thanks! Jakob On Mon, Nov 23, 2020 at 4:54 AM Richard Eisenberg wrote: > > > > On Nov 21, 2020, at 10:38 PM, Jakob Brünker > wrote: > > > > Three questions: > > - Is there already a way to do this that I'm missing? > > Not that I'm aware