List instances for a type in GHCi

[xldenis]

The proposal has been accepted; the following discussion is mostly of historic interest.

---

This is a proposal to add a GHCi command that lists all valid instances for a given complete or partial type signature.

Rendered

[ElvishJerricco]

This is awesome. It'd also be great if you could list the instances of a given class.

[Icelandjack]

@ElvishJerricco listing every instance of Eq when will it stop?

Eq ()
Eq Int
Eq ((), ())
Eq ((), Int)
..
Eq ((), ((), ((), ..

edit ah same as :info

[ElvishJerricco]

@Icelandjack Would that just show this?

Eq ()
Eq Int
(Eq a, Eq b) => Eq (a, b)
(Eq a, Eq b, Eq c) => Eq (a, b, c)
(Eq a, Eq b, Eq c, Eq d) => Eq (a, b, c, d)
...

Anyway, I just realized you can already get this with :i ClassName.

[xldenis]

Currently the :info command has some heuristics to decide which instances to show. I think in general this is a problem because a class is likely to have many more instances than a type does.

Here is what the docs on the relevant method for :info say:

-- Filter the instances by the ones whose tycons (or clases resp)
-- are in scope (qualified or otherwise).  Otherwise we list a whole lot too many!
-- The exact choice of which ones to show, and which to hide, is a judgement call.
--      (see Trac #1581)

Additionally, currently :info does list every tuple instance for Eq.

[RyanGlScott]

Thank you for opening a GHC proposal for this. After reading the proposal, I'm left with a number of questions:

1. What happens if you give a type class an an argument to :instances? (e.g., :instances Eq.) After reading this proposal, I get the general impression that :instances ty only enumerates instances where ty appears as an argument to some other type class, and that :instances C isn't intended to list all instances of a class C. (So if you typed :instances Eq, it would most likely list nothing.) Is this true? If so, it would be helpful to say so explicitly.

2. Am I correct in saying that all arguments given after :instances are parsed as a single type? That is to say, :instances Sum [] [] will never be interpreted to mean "find an instance of a multi-parameter type class with Sum, [], and [] as arguments"? It would be good to make note of this, especially since this would be a challenge one would have to overcome if one were to extend :instances in the future to support this kind of behavior.

3. How are type variables treated? For instance, what happens if you type :instances a or :instances Either a b? Would these error out due to the type variables not being bound (similarly to how :kind a errors out, but :kind (forall a. a) does not), and if so, would you require the user to instead type in :instances (forall a. a) or :instances (forall a b. Either a b)? If not, how would they behave? What is the relationship between type variables and type wildcards? (e.g., :instances Maybe a vs. :instances Maybe _.)

4. After reading the change specification, I'm unclear on what the exact scope of this proposal is. You list three intriguing ideas, but it's preceded with the phrase "some further work", which makes me unsure if these ideas are really part of the proposal at all, or if these are half-completed thoughts that are intended to be fleshed out at some separate point in the future.

   I'll go ahead and assume that these are part of the proposal for the rest of this comment.

5. In your description of :noinstance, you say ":noinstance would output a list of the unsatisfied constraints that prevent an instance from existing for a specific type". I'm very unclear on what this means. Can you describe what kind of output, say, :noinstance Eq (a -> b), would produce?

6. The discussion of multi-parameter type classes in the Proposed Change Specification section sounds very unsure of itself, especially since this is supposed to be a specification. Perhaps it would be better to move this to the Costs and Drawbacks section.

7. "Trace Info: Provide the source for every instance a type has." Provide an example of this, please!

8. I didn't really gain much from reading the Effects and Interactions section. The first three paragraphs of that section read like they belong in the Motivation section instead, since they only describe why someone might want this feature. As for the last paragraph, well, I'm unsure if it really has no interaction whatsoever with the language itself, which leads into my next question...

9. ...How does this feature interact with overlapping instances? For example, suppose you had the following instances:

   instance (Applicative f, Monoid a) => Monoid (f a)
   instance Alternative f => Monoid (f a)

   Assuming that you can query for something like :instances Monoid (f a) (see question 3), will it return both of these? Only one? Will the presence of incoherent instances affect what answer is returned?

[xldenis]

Hi @RyanGlScott, thanks for commenting and raising some great points. I've made some changes to the proposal which should clarify things already but I'll respond here as well.

1. This command isn't intended to list all instances for a class if it's provided as an argument. I don't believe you can actually write instances for classes themselves even with -XConstraintKinds (ie class MyClass (a :: * -> Constraint)), but I haven't tried either.
2. Yes, you are correct in thinking that all the arguments following :instances are intended to be parsed as a single type, I've clarified that in the proposal.
3. (NOTE: I changed this section, look at past versions of this comment to see it). Turns out that the :kind command in GHCi also supports wildcards. I think in light of this, we can be satisfied with just accepting types according to the same rules. If you want to use a named type variable, then you use explicit quantification otherwise you can use wildcards.

For 4-9, I've moved it to a future work section as well as expanded the sections and added an example for the traces.

[Icelandjack]

Thanks for the feedback @RyanGlScott. @xldenis gave a good response,

1. My guiding intuition is, candidates (instances) of :instance <ty/cls> are drawn from :info of the outermost type constructor of <ty/cls> (and maybe of all constructors that appear). It is possible to write instances of constraints (but they are rare¹). In this example I expect :instances of both Eq and Int to list instance Cls (Eq Int) because it is given by :info:

   class    Cls (cls :: Constraint)
   instance Cls (Eq Int)
   
   -- >> :info Eq
   -- instance Cls (Eq Int) ..
   -- >> :info Int
   -- instance Cls (Eq Int) ..

   On the other hand, I don't expect any input to :instances to list instance (cls a, cls' a) => (cls & cls') a. Even though there is an instance for (Eq & Show) Int I don't expect to see that listed by :instances Eq (or :instances Show or :instances Int)

   -- (&) :: (k -> Constraint) -> (k -> Constraint) -> (k -> Constraint)
   class    (cls a, cls' a) => (cls & cls') a
   instance (cls a, cls' a) => (cls & cls') a

2. Yes as @xldenis says, I don't see value in having them 'float'

3. Ideally I want implicit quantification, where multiple occurrences of a type variable imply an equality constraint (this query being equal to forall f f'. f ~ f' => Sum f f')

   >> :instances Sum f f
   Functor f => Functor (Sum f f)
   Foldable f => Foldable (Sum f f) ..
   

4. I don't care about this feature but I see at least one interesting path:

   • Following the intuition: If it appears in the original :info but fails for some reason, we list it:

     >> :info (,)
     instance (Eq a, Eq b) => Eq (a, b) 
     >> :instances (Int -> Int, Bool -> Bool)
     <no Eq instance>
     >> :noinstances (Int -> Int, Bool -> Bool)
     NO instance for Eq (Int -> Int, Bool -> Bool), because
       NO instance for Eq (Int -> Int)
       NO instance for Eq (Bool -> Bool)
     

   • (uninteresting) the user explicitly lists the expected type class :noinstance Eq (Int -> Int, Bool -> Bool) giving the same result as the beginning of :noinstance (Int -> Int, Bool -> Bool) above

¹ Examples of type classes over Constraint, apart from kind polymorphic constraints such as (~) and Coercible:

• from constraints
  • Class :: Constraint -> Constraint -> Constraint
  • (:=>) :: Constraint -> Constraint -> Constraint
  • Deferrable :: Constraint -> Constraint
  • Lifting :: (k -> Constraint) -> (k -> k) -> Constraint
• Static :: Constraint -> Constraint
• Universally :: (k -> Type) -> (Type -> Constraint) -> Constraint
• Cartesian :: (Type -> Constraint) -> Constraint

  class Cartesian cls where
    cartesian :: (cls a, cls b) :- cls (a, b)

[xldenis]

I've added a section for further examples as well as clarified what happens when a typeclass is provided as an argument to :instances. Are there any further questions or should we proceed to notify the committee?

[Ericson2314]

I might prefer writing constraints with wildcards, for sake of working with multi-parameter type classes or aggregate constraints. Basically, something like a prolog REPL

[xldenis]

@RyanGlScott I know you were busy with ICFP (congrats on your talk!), do you feel like your concerns have been addressed?

@Ericson2314 I think we'll just use the same syntax as the :kind command which allows writing types like _ -> Int, if you want to name your variables then you can bind them explicitly with forall.

[RyanGlScott]

I haven't reviewed the changes closely, but things look reasonable from a glance. Then again, I'm not part of the committee, so you don't need my permission to continue :)

[xldenis]

Well then I think I'll ping @nomeata to bring this before the comittee!

As a summary of the changes that occurred throughout the discussion:

• Properly split out future work that could be done :noinstance, etc..
• Provided more examples
• Clarified behaviour when a class is provided as an argument

I don't believe there are any open objections to this proposal as it stands so it should be ready for committee review?

[xldenis]

Bump @nomeata :)

[nomeata]

Thanks for the bump, I guess it got lost during ICFP.

[yav]

I think I get the basic idea of what we'd like to do here, and it seems useful enough. However, I think the proposal could use a little more details on how things are supposed to work. In particular:

1. The proposal suggests using forall to name variables in queries, but the meaning is not clear. For example, would :instances forall a. Maybe a match instance C (Maybe Int)?

   1. If yes, then I don't think that forall is a very good choice as clearly we don't mean that the instance should work for all types. It would seem more natural to simply allow variable without a quantifier, e.g., say :instances Maybe a instead.
   2. If no, then it seems the proposal is missing something potentially useful: it mentions using wild cards, but those can't express that two types should be the same (yet arbitrary).

2. How exactly does matching a query work? For the sake of concreteness, consider a query :instances forall a. (a,b,[Int]), where I am assuming that a is universally quantified (i.e., we don't want to instantiate it), and b is existentially quantified (i.e., it is like a named wild-card). There are at least two dimensions in which we can make choices, when deciding if an instance matches this query:

   1. Where in the instance head can the query appear? Here are some options, illustrate with examples:

       instance C1 (a,b,[Int])     -- A: only in single parameter classes
       instance C2 x (a,b,[Int])   -- B: as any parameter of a mult-parameter class 
       instance C3 (Maybe (a,b,[Int])) -- C: arbitrarily nested in a parameter
      

   2. Is it enough to match the instance head, or do we want use the instance context as well? Here are some examples:

      instance C4 (Int,b,c)              -- Does not match: `a` universal
      instance C5 (a,Int,c)              -- Matches `b`: is existential
      instance Num c  => C6 (a,Int,c)    -- Matches head, but no instance for `Num [Int]`
      instance Num b => C7 (a,[b],c)     -- Matches head, can't simplify context (existential)
      instance Num a => C8 (a,Int,c)     -- Matches head, cant't simplify context (universal)
      instance (b ~ Char) => C9 (a,b,c)  -- context improves instance
      instance (c ~ Char)  => C10 (a,b,c) -- head matches, context unsatisfiable
      

Sorry for the long post, I hope this will help things more precise.

[simonpj]

I rather agree with Iavor. The "proposed change specification" is not really a specification, in the sense of precisely specifying what should and should not happen.

I think that the intent is something like this.

• You enter :instances <type> to GHCi,
• Here, <type> can contain wildcards (underscores), but not variables (like a, b)
• GHCi should report all the instances that unify with <type>, treating each wildcard as a variable that can be unified.

For example

• :instances Eq (Maybe _) would report the instance for Eq (Maybe a)
• :instances Eq (Maybe Int) would report exactly the same
• :instances Eq _ would report all instances for Eq

I don't think there is any need for the forall stuff, and I don't understand what is intended by it.

Optional extra: allow named wildcards. So then :instances C (_a, Int, _a) would unify with instance C (Bool, Int, Bool) but not with instance C (Bool, Int, Int).

[yav]

@xldenis do you think you could make some changes to the proposal to clarify how things should work?

[xldenis]

Hi @yav, yes I was travelling over the past week so I didn't have time to address your comments but I just got back today so I'll push a revision of the proposal tomorrow.

Response to @yav's and @simonpj's comments:

The proposal suggests using forall to name variables in queries, but the meaning is not clear. For example, would :instances forall a. Maybe a match instance C (Maybe Int)?

That was discussed and proposed at first but the intention at this point is to used type holes to represent variables in queries. Since it appears that parsing mechanism used in GHCi has special case support for unnamed holes, it will need to be extended to support named ones as well.

How exactly does matching a query work?

Where in the instance head can the query appear? Here are some options, illustrate with examples:

I personally think that the instances command should only match directly against the instance head, and only for single-parameter type classes. If anyone feels that the query should match arbitrarily deep into an instance I'd be interested in seeing usecases. Matching multi-parameter typeclasses would require new syntax since we need to delineate each argument. I figured that if someone had an idea for that it could be discussed in a future proposal to extend the command.

Is it enough to match the instance head, or do we want use the instance context as well? Here are some examples:

Out of the listed potential matches, here is what I would expect the command to return:

Num b => C7 (a,[b],c)     -- Matches head, can't simplify context (existential)
Num a => C8 (a,Int,c)     -- Matches head, cant't simplify context (universal)
C9 (a,Char,c)  -- context improves instance
C10 (a,b,Char) -- head matches, context unsatisfiable

Notably, we also discharge the equality constraint for the last two instances.

@simonpj I think your comment reflects the largest ambiguity / ux problem with this proposal:

:instances Eq (Maybe _) would report the instance for Eq (Maybe a)

As stated, the command would actually return any class instances for the type Eq (Maybe _) , such as the class Static listed in @Icelandjack's example above:

class c => Static c where
  closureDict :: Closure (Dict c)

So the output we'd expect would be something like:

> :instances Eq (Maybe _)
Static (Eq (Maybe _))
....

@ElvishJerricco made the same mistake earlier in the thread, so this is not an isolated event. Obviously the proposal should be clarified but maybe there's something that could be done to avoid users confusing the command in ghci.

[xldenis]

I don't know if I worded this properly, but the intent is to say that given: :instances T, we look for all unifiable instances C T, for all visible classes C.

[yav]

Thanks for making the changes. Just one more clarification: the part about having to satisfy all implied constraints seems a little fishy to me. If I write:

:instances (Maybe _)

I would expect to see the Eq instance, correct? The instance looks like this:

 instance Eq a => Eq (Maybe a)

When deciding if it should display it, GHC will unify the head against my query, which will succeed. However, we can't simplify the context any further, as we are left with Eq a and we don't know how to simplify this.

OTOH, if I'd written :instances (Maybe (_ -> _)), then I probably wouldn't want to see that instance as there aren't any instances that match Eq (_ -> _).

So we need some sort of a rule that will tell us which left-over constraints are OK, as in the first example, vs. not OK as in the second.

My suggestion would be that an instance should be displayed if we can unify with the head, and then simplify the instance context to constraints that only involve variables. I haven't thought very deeply about that, so please take it with a grain of salt.

[xldenis]

OTOH, if I'd written :instances (Maybe (_ -> )), then I probably wouldn't want to see that instance as there aren't any instances that match Eq ( -> _).

Wouldn't this just be a matter of going through the normal instance resolution process? When we attempt to reduce the context GHC should tell us that there is no instance for Eq (_ -> _)?

[yav]

Indeed.

The point I was trying to make is that in both examples (:instances (Maybe _) and :instances (Maybe (_ -> _))) we can't fully simplify the constraints in the instance context: in the first case we are left with Eq _x and in the second with Eq (_x -> _y). But (I think?) we'd like to consider the first one matching and the second one not matching.

So we need some way to distinguish these two: one way would be the rule I suggested (the first one matches because the left-over constraints only mention variables, while the second one is rejected as it mentions a concrete type constrctor)

Another option would be to say that neither of these examples should match, which is what I think the current specification suggests, although I think that might be somewhat surprising. If that's the intention, let's add the example to the document to make it more explicit.

[xldenis]

Hmm, yea I see the problem now, I'll add that specific example and reword that sentence. What we'd like is effectively that only constraints on the type-holes remain after simplifying.

[Icelandjack]

Wish list item: To generate DerivingVia deriving clauses, as a flag to :instances or :via

>> :via Cont (Result i o)
deriving
  (Functor, Applicative, Monad, MonadCont)
via
  Cont (Result i o)

[deepfire]

A suggestion for the MPTC syntax: use TypeApplication's @ to delineate single typeclass parameters -- while allowing the currently accepted proposal to stand as is.

Notes:

1. The syntax for the currently accepted proposal would then get an extra form:
   • current :instances Type (Foo b) c
   • will mean in the extended version: :instances @(Type (Foo b) c)
2. The newly-admitted MPTC queries will look like:
   :instances @(Type1 a (f b)) @[] @(->)
3. We're riding on/extending the concept of applying types to something that consumes types.
4. There's likely some synergy here with @ existing notions of what is admissible.

cc @xldenis

[Icelandjack]

newtype Gen a = Gen (Int -> StdGen -> a) where
 deriving 
  Functor
 via
  (Compose ((->) Int) ((->) StdGen))

It would be good to see

>> :instances Compose ((->) Int) ((->) StdGen)
instance Functor ..
instance Applicative ..

---

Sometimes instances have complicated constraints, like cls being closed under Compose and Identity. This is probably a separate request

>> :instances Category (C cls)
instance Category (C Functor)
instance Category (C Applicative)
..

but not Category (C Monad) because Monad is not closed under Compose.

[xldenis]

I need to rebase my branch on the latest master but I expect that your example will work.

@deepfire that seems like a pretty reasonable idea but I think we should revisit it once I've finished implementing the current proposal :)

[Icelandjack]

>> :instances Kleisli (f `Compose` Maybe)