Re: How to best display type variables with the same name

[Christopher Done]

On 26 October 2016 at 11:43, Simon Peyton Jones  wrote:
> As far as I understand it:
>
> · You are plucking a type from the midst of a syntax tree, and
> displaying it.
>
> · That type might well mention type variables that are bound
> “further out”
>
> o   either by a forall (if this is a sub-tree of a type)
>
> o   or by a big lambda
>
> · There are some tricky UI issues in how to display such types to
> the user.

Right.

> Generally, I think it’s mainly up to you to track which type variables are
> in scope from “further out”.  It’s not a property that is stable under
> transformation, so it’s not part of the TyVar.

Fair enough. That's useful to know, thanks. In that case I can explore
alternative approaches.

> The typechecker itself uses “tidying” to avoid accidentally displaying
> distinct type variables in the same way.  See TyCoRep.tidyType and related
> functions.  They may be useful to you too.

Ah, the TidyEnv makes sense to me. I think that'll come in handy to
review the code to make sure I don't miss anything.

> Hard for me to say more… I’m swamped, and there are genuine UI issues here.
> Maybe some folk on Haskell Café might be interested.

Thanks! I've also got low bandwidth for this, I just posted it to have
it out there, as it probably requires some brewing before anything
will be implemented anyway.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: How to best display type variables with the same name

[Simon Peyton Jones via ghc-devs]

Chris

As far as I understand it:

· You are plucking a type from the midst of a syntax tree, and 
displaying it.

· That type might well mention type variables that are bound “further 
out”

o   either by a forall (if this is a sub-tree of a type)

o   or by a big lambda

· There are some tricky UI issues in how to display such types to the 
user.

Generally, I think it’s mainly up to you to track which type variables are in 
scope from “further out”.  It’s not a property that is stable under 
transformation, so it’s not part of the TyVar.

The typechecker itself uses “tidying” to avoid accidentally displaying distinct 
type variables in the same way.  See TyCoRep.tidyType and related functions.  
They may be useful to you too.

Hard for me to say more… I’m swamped, and there are genuine UI issues here.  
Maybe some folk on Haskell Café might be interested.

Simon

From: Christopher Done [mailto:chrisd...@gmail.com]
Sent: 21 October 2016 15:07
To: Simon Peyton Jones <simo...@microsoft.com>
Cc: ghc-devs@haskell.org
Subject: Re: How to best display type variables with the same name


On 19 October 2016 at 17:00, Simon Peyton Jones 
simo...@microsoft.com<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmailto%3Asimonpj%40microsoft.com=02%7C01%7Csimonpj%40microsoft.com%7C4c125c4fe1834a3a959708d3f9bb9d1b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636126556597550377=hGnspUNnWUxTUXA%2FS%2F%2B7mw6J2WyqirrsacU21TGRk0U%3D=0>
 wrote:

I’m afraid I didn’t understand the issue in the link below. It
speaks of “querying the type”, but I’m not sure what that means. A
GHCi session perhaps? Does this relate to the way GHCi displays
types?

I’m a bit lost. A from-the-beginning example, showing steps and
what the unexpected behaviour is would be helpful (to me anyway)

Sure. I’ll explain from top-level down:

· In this case “querying the type” means running the :type-at
command in Intero (which itself is a fork of GHCi’s codebase around
GHC 7.10):
https://github.com/commercialhaskell/intero/blob/master/src/InteractiveUI.hs#L1693-L1713<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fcommercialhaskell%2Fintero%2Fblob%2Fmaster%2Fsrc%2FInteractiveUI.hs%23L1693-L1713=02%7C01%7Csimonpj%40microsoft.com%7C4c125c4fe1834a3a959708d3f9bb9d1b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636126556597550377=C9rd1twSgpzdJ9UbdUZL4h8oCMBUrXJKGYjSlaoqrqc%3D=0>
It accepts a file name, line-col to line-col span and prints the
type of that expression/pattern. As you can see in that function it
uses printForUserModInfo (from GhcMonad), similar to (scroll above)
the printForUser for GHCi’s regular :type command.

· Where does that info come from? When we load a module in Intero, we
perform an additional step of “collecting info” here:
https://github.com/commercialhaskell/intero/blob/master/src/GhciInfo.hs#L73<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fcommercialhaskell%2Fintero%2Fblob%2Fmaster%2Fsrc%2FGhciInfo.hs%23L73=02%7C01%7Csimonpj%40microsoft.com%7C4c125c4fe1834a3a959708d3f9bb9d1b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636126556597550377=lI4KU9JbM3tb7ZrEp684eHi1EixchPn1aeOXsUab6sU%3D=0>
That info, for each node in the AST, is ultimately stored in a
SpanInfo:
https://github.com/commercialhaskell/intero/blob/master/src/GhciTypes.hs#L28-L39<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fcommercialhaskell%2Fintero%2Fblob%2Fmaster%2Fsrc%2FGhciTypes.hs%23L28-L39=02%7C01%7Csimonpj%40microsoft.com%7C4c125c4fe1834a3a959708d3f9bb9d1b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636126556597550377=MLkyE0K2jJL%2FOE%2BnMMl1IuJ633u2jTL16BIz%2F0lK%2FEo%3D=0>
Which we then use for :type-at.

So in summary we collect info from tm_typechecked_source, keep that
for later, and then when the user’s editor asks via e.g. :type-at X.hs 1 5 1 7 
“what is the type of the thing at this point?” we use
GHC’s regular pretty printing function to print that type.

That actually all works splendidly. For example, if we query

foo g f = maybe g f

--  ^ here or   ^ here yields g :: b

foo g f = maybe g f

--^ here or   ^ here yields: f :: a -> b

The tricky part arises in this example:
https://github.com/commercialhaskell/intero/issues/280#issuecomment-254784904<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fcommercialhaskell%2Fintero%2Fissues%2F280%23issuecomment-254784904=02%7C01%7Csimonpj%40microsoft.com%7C4c125c4fe1834a3a959708d3f9bb9d1b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636126556597550377=r6WMD%2BUl6ilAyDX4V%2FibPSQqM9UPlBPrOUCMjjmHj9c%3D=0>

Which is that we have two perfectly cromulent types from the AST that
are both a in isolation, but are actually different. They will have
different Unique values in their Name’s and come from different
implicit forall‘s. The question is what’s a good way to communicate
this to the user?

Thi

Re: How to best display type variables with the same name

[Christopher Done]

On 19 October 2016 at 17:00, Simon Peyton Jones simo...@microsoft.com
 wrote:

I’m afraid I didn’t understand the issue in the link below. It
speaks of “querying the type”, but I’m not sure what that means. A
GHCi session perhaps? Does this relate to the way GHCi displays
types?

I’m a bit lost. A from-the-beginning example, showing steps and
what the unexpected behaviour is would be helpful (to me anyway)

Sure. I’ll explain from top-level down:

   -

   In this case “querying the type” means running the :type-at
   command in Intero (which itself is a fork of GHCi’s codebase around
   GHC 7.10):

   
https://github.com/commercialhaskell/intero/blob/master/src/InteractiveUI.hs#L1693-L1713
   It accepts a file name, line-col to line-col span and prints the
   type of that expression/pattern. As you can see in that function it
   uses printForUserModInfo (from GhcMonad), similar to (scroll above)
   the printForUser for GHCi’s regular :type command.
   -

   Where does that info come from? When we load a module in Intero, we
   perform an additional step of “collecting info” here:

   https://github.com/commercialhaskell/intero/blob/master/src/GhciInfo.hs#L73
   That info, for each node in the AST, is ultimately stored in a
   SpanInfo:

   
https://github.com/commercialhaskell/intero/blob/master/src/GhciTypes.hs#L28-L39
   Which we then use for :type-at.

So in summary we collect info from tm_typechecked_source, keep that
for later, and then when the user’s editor asks via e.g. :type-at X.hs 1 5
1 7 “what is the type of the thing at this point?” we use
GHC’s regular pretty printing function to print that type.

That actually all works splendidly. For example, if we query

foo g f = maybe g f--  ^ here or   ^ here yields g :: bfoo g f = maybe
g f--^ here or   ^ here yields: f :: a -> b

The tricky part arises in this example:
https://github.com/commercialhaskell/intero/issues/280#issuecomment-254784904

Which is that we have two perfectly cromulent types from the AST that
are both a in isolation, but are actually different. They will have
different Unique values in their Name’s and come from different
implicit forall‘s. The question is what’s a good way to communicate
this to the user?

This is partly a “user interface” question, and on the side a “given
an ideal UI, do we have the necessary info the GHC API?”

If it helps, I could probably spend some time making an isolated
module that uses the GHC API to compile a file and then report these
types.

Ciao!
​
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: How to best display type variables with the same name

[Simon Peyton Jones via ghc-devs]

I’m afraid I didn’t understand the issue in the link below.  It speaks of 
“querying the type”, but I’m not sure what that means.  A GHCi session perhaps? 
 Does this relate to the way GHCi displays types?

I’m a bit lost.  A from-the-beginning example, showing steps and what the 
unexpected behaviour is would be helpful (to me anyway)

Simon

From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Christopher 
Done
Sent: 19 October 2016 12:46
To: ghc-devs@haskell.org
Subject: How to best display type variables with the same name

We've encountered a problem in Intero which is that when inspecting types of 
expressions and patterns, sometimes it happens that the type, when pretty 
printing, yields variables of the same name but which have different provenance.

Here's a summary of the issue:

https://github.com/commercialhaskell/intero/issues/280#issuecomment-254784904<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fcommercialhaskell%2Fintero%2Fissues%2F280%23issuecomment-254784904=02%7C01%7Csimonpj%40microsoft.com%7C58538b7f7532497970c708d3f8158e45%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636124743872989785=2AkHss5Io%2BHqJjF8CtFwSErBuUca6N2gJ3DELC03nFY%3D=0>

And a strawman proposal of how it could be solved:

https://github.com/commercialhaskell/intero/issues/280#issuecomment-254787927<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fcommercialhaskell%2Fintero%2Fissues%2F280%23issuecomment-254787927=02%7C01%7Csimonpj%40microsoft.com%7C58538b7f7532497970c708d3f8158e45%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636124743872989785=ev%2FJQg4xKrZVyi0uP9PxS756t41IO4%2BoI0AlJoT9F7U%3D=0>

What do you think?

Also, if I were to implement the strawman proposal, is it possible to recover 
from a `tyvar :: Type` its original quantification/its "forall"? I've had a 
look through the API briefly and it looks like a _maybe_.

Ciao!
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: How to best display type variables with the same name

[Alan & Kim Zimmerman]

This sounds like a thing that should be in the GHC API (the tyvar to
provenance lookup).

Alan

On Wed, Oct 19, 2016 at 2:48 PM, Richard Eisenberg 
wrote:

> Interesting problem & solution.
>
> Here's a wacky idea, from a position of utter ignorance about your
> environment: could you use color? Already, when I saw `b :: a` in the
> commentary there, where `b` is in scope as a type variable, it seemed wrong
> to me.
>
> In any case, I can answer your simpler question: yes, with some work, you
> can get from a tyvar to its provenance. A tyvar's Name will have its
> binding location in it. If you also keep track of binding locations as you
> spot foralls, you should be able to match them up. In theory.
>
> Richard
>
> On Oct 19, 2016, at 7:45 AM, Christopher Done  wrote:
>
> We've encountered a problem in Intero which is that when inspecting types
> of expressions and patterns, sometimes it happens that the type, when
> pretty printing, yields variables of the same name but which have different
> provenance.
>
> Here's a summary of the issue:
>
> https://github.com/commercialhaskell/intero/issues/280#
> issuecomment-254784904
>
> And a strawman proposal of how it could be solved:
>
> https://github.com/commercialhaskell/intero/issues/280#
> issuecomment-254787927
>
> What do you think?
>
> Also, if I were to implement the strawman proposal, is it possible to
> recover from a `tyvar :: Type` its original quantification/its "forall"?
> I've had a look through the API briefly and it looks like a _maybe_.
>
> Ciao!
> ___
> 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: How to best display type variables with the same name

[Richard Eisenberg]

Interesting problem & solution.

Here's a wacky idea, from a position of utter ignorance about your environment: 
could you use color? Already, when I saw `b :: a` in the commentary there, 
where `b` is in scope as a type variable, it seemed wrong to me.

In any case, I can answer your simpler question: yes, with some work, you can 
get from a tyvar to its provenance. A tyvar's Name will have its binding 
location in it. If you also keep track of binding locations as you spot 
foralls, you should be able to match them up. In theory.

Richard

> On Oct 19, 2016, at 7:45 AM, Christopher Done  wrote:
> 
> We've encountered a problem in Intero which is that when inspecting types of 
> expressions and patterns, sometimes it happens that the type, when pretty 
> printing, yields variables of the same name but which have different 
> provenance.
> 
> Here's a summary of the issue:
> 
> https://github.com/commercialhaskell/intero/issues/280#issuecomment-254784904 
> 
> 
> And a strawman proposal of how it could be solved:
> 
> https://github.com/commercialhaskell/intero/issues/280#issuecomment-254787927 
> 
> 
> What do you think? 
> 
> Also, if I were to implement the strawman proposal, is it possible to recover 
> from a `tyvar :: Type` its original quantification/its "forall"? I've had a 
> look through the API briefly and it looks like a _maybe_.
> 
> Ciao!
> ___
> 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

How to best display type variables with the same name

[Christopher Done]

We've encountered a problem in Intero which is that when inspecting types
of expressions and patterns, sometimes it happens that the type, when
pretty printing, yields variables of the same name but which have different
provenance.

Here's a summary of the issue:

https://github.com/commercialhaskell/intero/issues/280#issuecomment-
254784904

And a strawman proposal of how it could be solved:

https://github.com/commercialhaskell/intero/issues/280#issuecomment-
254787927

What do you think?

Also, if I were to implement the strawman proposal, is it possible to
recover from a `tyvar :: Type` its original quantification/its "forall"?
I've had a look through the API briefly and it looks like a _maybe_.

Ciao!
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs