Opened 3 years ago

Last modified 3 years ago

#9183 new feature request

GHC shouldn't expand constraint synonyms

Reported by: Feuerbach Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


{-# LANGUAGE ConstraintKinds #-}

type ShowX = Show

showX :: ShowX a => a -> String
showX = show

If I now ask for the type of showX, I get:

*Main> :t showX
showX :: Show a => a -> String

Change History (10)

comment:1 Changed 3 years ago by simonpj

I see what you want, but I don't see how to achieve it.

Recall that

  • :info f takes a name f and tells you stuff about f
  • :type e takes an abritrary expression e and tells you its type

If you use :info showX you'll see the type you expect. If you use :type showX you are using :type with an "arbitrary expression" that turns out to be a single identifier. So GHC instantiates it with fresh type variables, generates constraints, simplifies them, and then re-generalises. The instantiation, constraint simplification, and regeneration is what expands the constraint synonym, and I don't see a robust way to stop that happening.

We could make :type behave like :info when given a bare identifier. Or, in those same circumstances, we would make :type refrain from the "instantiate, simplify, generalise" hoopla. But that would make :type on a bare identifier behave subtly differently to the way it does now.Is that special case worth it? Or would it be better to encourage users to use :info whenever possible?

comment:2 Changed 3 years ago by Feuerbach

I just assumed this can be similar to how ghc doesn't expand ordinary type synonyms unless necessary, but from what you're saying it sounds like it's different for constraints?

An even more important feature would be to preserve the synonym names in type errors. That'd allow to make such errors more domain-specific and informative, while an expanded version is very complex and essentially reveals a lot of internal details of the library.

Would it make sense to have something like

newtype MyConstraint (a :: *) = MyConstraint (Show a, Eq a, Num a) :: Constraint


data MyConstraint (a :: *) = MyConstraint (Show a) (Eq a) (Num a) :: Constraint

that wouldn't expand automatically? Just like we can improve the quality of error messages in ordinary Haskell by replacing type synonyms with newtypes or data types?

(I don't have a clear vision of how this should work; this is just an idea.)

comment:3 Changed 3 years ago by goldfire

You can do the MyConstraint trick today:

class (Show a, Eq a, Num a) => MyConstraint a
instance (Show a, Eq a, Num a) => MyConstraint a

Haven't tested this in error messages, exactly, but my guess is that it will behave better.

comment:4 Changed 3 years ago by Feuerbach

Ah, right! I've used this trick in the past many times, but every now and then I get lured by the nice-looking constraint synonyms, and forget about the alternative.

So, it looks like the semantics is not a problem. Perhaps it'd be possible to introduce a better syntax for it?

comment:5 Changed 3 years ago by goldfire

Have you tested this idea in your use case? Do the error messages improve?

Personally, I don't think it's necessary to introduce a new syntax for this idiom (just one more thing to remember/maintain), but I don't feel strongly.

comment:6 Changed 3 years ago by Feuerbach

Just tested it — doesn't seem to work.

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}

class Show a => MyC a
instance Show a => MyC a

foo :: MyC a => a -> String
foo = show

:t foo shows

foo :: Show a => a -> String

comment:7 Changed 3 years ago by goldfire

That doesn't surprise me terribly, because of the reasons Simon cites above. How does it work in proper error messages, though? I think more care is taken there than in :t.

comment:8 Changed 3 years ago by Feuerbach

Doesn't help there, either.

*Main> foo id

    No instance for (Show (a0 -> a0)) arising from a use of ‘foo’
    In the expression: foo id
    In an equation for ‘it’: it = foo id

comment:9 Changed 3 years ago by goldfire

Hm. I guess this fruit isn't as low-hanging as I thought... deferring to others for now.

comment:10 Changed 3 years ago by simonpj

I really don't see what we can reasonably do here. e.g.

type Foo a = (Eq a, Ix a)

Now if you instantiate and re-generalise it's really not possible to reconstruct the Foo a. I suppose you could have a magical special case when there is a type synonym for a single constraint. That might, just, be possible. But it'd be a bit of effort to push it through, so I propose to wait until more people yell.


Note: See TracTickets for help on using tickets.