Find constraints over type

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Find constraints over type

Alejandro Serrano Mena
Dear GHC devs,
I am trying to figure out a way to obtain the constraints that hold over a type. Let me give you an example: suppose that I write the following function:

f :: Eq a => [a] -> Bool
f xs = xs == []

If I ask for the type of the Var ' xs', I get back '[a]'. This is correct, but I am missing the crucial information that '[a]' must be Eq.

Is there an easy way to get it? It seems that 'varType' doesn't give me enough information.

Regards,
Alejandro

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Find constraints over type

Ben Gamari-2
Alejandro Serrano Mena <[hidden email]> writes:

> Dear GHC devs,
> I am trying to figure out a way to obtain the constraints that hold over a
> type. Let me give you an example: suppose that I write the following
> function:
>
> f :: Eq a => [a] -> Bool
> f xs = xs == []
>
> If I ask for the type of the Var ' xs', I get back '[a]'. This is correct,
> but I am missing the crucial information that '[a]' must be Eq.
>
> Is there an easy way to get it? It seems that 'varType' doesn't give me
> enough information.
>
Indeed `varType` of `xs` will only give you the type `a`. How to get
back to the constraints that mention `xs` is a bit trick and will depend
upon where in the compiler you are. As far as I can tell, getting
constraints after desugaring will be quite difficult since they will
have been lowered to dictionaries at that point.

If you have access to hsSyn then you can of course easily compute the
constraints explicitly provided by the signature for `xs` (assuming
there is one). However, this will of course miss any inferred
constraints.

During typechecking it may be possible to compute some sort of
constraint set by looking at the typechecking environment, although I'll
admit this sounds quite dodgy.

Can you provide more details on what you are trying to do?

Cheers,

- Ben


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (497 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

RE: Find constraints over type

GHC - devs mailing list
In reply to this post by Alejandro Serrano Mena

There is definitely no pure way to get from ‘a’ to its constraints.

  • It is far from clear what “its constraints” are.   Is (C a b) such a constraint?  C [a] b?  What about superclasses?
  • Constraints vary depending on where  you are.  GADT matches can bring into scope extra constraints on existing type variables.

 

So as Ben says, to give a sensible response you’ll need to explain more about your goal

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 16 January 2020 16:19
To: GHC developers <[hidden email]>
Subject: Find constraints over type

 

Dear GHC devs,

I am trying to figure out a way to obtain the constraints that hold over a type. Let me give you an example: suppose that I write the following function:

 

f :: Eq a => [a] -> Bool

f xs = xs == []

 

If I ask for the type of the Var ' xs', I get back '[a]'. This is correct, but I am missing the crucial information that '[a]' must be Eq.

 

Is there an easy way to get it? It seems that 'varType' doesn't give me enough information.

 

Regards,

Alejandro


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Find constraints over type

Alejandro Serrano Mena
My goal is to add type information on hover within `ghcide`. Right now, when you select a variable, we give back the type as reported in the corresponding Var. However, when this type involved a type variable, it misses a lot of important information about the typing context in which we are working. So the goal is to report back some of this typing context.

Going back to my original example:

f :: Eq a => [a] -> Bool
f xs = xs == []

It would be great if by hovering over the 'xs', one would get '[a] where Eq a', or some other representation of the known constraints.

Since this is intended to be a help for the programmer, it doesn't really matter whether we get "too many" constraints (for example, if we had "Ord a" it's OK to get "Eq a" too, since that's interesting constraint information).

Right now I am working with TypecheckModules most of the time.

Regards,
Alejandro

El jue., 16 ene. 2020 a las 19:47, Simon Peyton Jones (<[hidden email]>) escribió:

There is definitely no pure way to get from ‘a’ to its constraints.

  • It is far from clear what “its constraints” are.   Is (C a b) such a constraint?  C [a] b?  What about superclasses?
  • Constraints vary depending on where  you are.  GADT matches can bring into scope extra constraints on existing type variables.

 

So as Ben says, to give a sensible response you’ll need to explain more about your goal

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 16 January 2020 16:19
To: GHC developers <[hidden email]>
Subject: Find constraints over type

 

Dear GHC devs,

I am trying to figure out a way to obtain the constraints that hold over a type. Let me give you an example: suppose that I write the following function:

 

f :: Eq a => [a] -> Bool

f xs = xs == []

 

If I ask for the type of the Var ' xs', I get back '[a]'. This is correct, but I am missing the crucial information that '[a]' must be Eq.

 

Is there an easy way to get it? It seems that 'varType' doesn't give me enough information.

 

Regards,

Alejandro


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Find constraints over type

GHC - devs mailing list

Starting from any point in the typechecked syntax tree, you can look outwards to find binding sites for enclosing constraints, and then use whatever method you like to decide if they are relevant. Binding sites are:

 

  • ConPatOut; binds dictionaries from GADT matches
  • AbsBinds: abs_ev_vars binds dictionaries from let-bindings

 

Simon

 

From: Alejandro Serrano Mena <[hidden email]>
Sent: 17 January 2020 08:26
To: Simon Peyton Jones <[hidden email]>
Cc: GHC developers <[hidden email]>
Subject: Re: Find constraints over type

 

My goal is to add type information on hover within `ghcide`. Right now, when you select a variable, we give back the type as reported in the corresponding Var. However, when this type involved a type variable, it misses a lot of important information about the typing context in which we are working. So the goal is to report back some of this typing context.

 

Going back to my original example:

 

f :: Eq a => [a] -> Bool
f xs = xs == []

 

It would be great if by hovering over the 'xs', one would get '[a] where Eq a', or some other representation of the known constraints.

 

Since this is intended to be a help for the programmer, it doesn't really matter whether we get "too many" constraints (for example, if we had "Ord a" it's OK to get "Eq a" too, since that's interesting constraint information).

 

Right now I am working with TypecheckModules most of the time.

 

Regards,

Alejandro

 

El jue., 16 ene. 2020 a las 19:47, Simon Peyton Jones (<[hidden email]>) escribió:

There is definitely no pure way to get from ‘a’ to its constraints.

  • It is far from clear what “its constraints” are.   Is (C a b) such a constraint?  C [a] b?  What about superclasses?
  • Constraints vary depending on where  you are.  GADT matches can bring into scope extra constraints on existing type variables.

 

So as Ben says, to give a sensible response you’ll need to explain more about your goal

 

Simon

 

From: ghc-devs <[hidden email]> On Behalf Of Alejandro Serrano Mena
Sent: 16 January 2020 16:19
To: GHC developers <[hidden email]>
Subject: Find constraints over type

 

Dear GHC devs,

I am trying to figure out a way to obtain the constraints that hold over a type. Let me give you an example: suppose that I write the following function:

 

f :: Eq a => [a] -> Bool

f xs = xs == []

 

If I ask for the type of the Var ' xs', I get back '[a]'. This is correct, but I am missing the crucial information that '[a]' must be Eq.

 

Is there an easy way to get it? It seems that 'varType' doesn't give me enough information.

 

Regards,

Alejandro


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs