Reducing satisfied constraints to ordinary types

Question

I understand the following type family shouldn't and perhaps can't be implemented in GHC:

type family MatchesConstraint c a :: Bool where
  MatchesConstraint c a is True if (c a)
  MatchesConstraint c a is False otherwise

This is problematic because classes are open, so MatchesConstraint c a could evaluate to True for some parts of the program and False in others depending on what instances are in scope, which I imagine could be potentially quite disastrous.

But consider the following:

type family MatchesConstraint c a :: Bool where
  MatchesConstraint c a is True if (c a)
  MatchesConstraint c a doesn't reduce otherwise

This seems quite safe. In some parts of our program we might fail to reduce if an instance is not in scope, but we'll never have an inconsistency.

Can I make something like this work in GHC?

The reason I'm asking for this, is because one could perhaps select instances based on not just type directly but class. Which could be a useful thing in some contexts I believe.

Answer 1

I answered a similar question from you here on the cafe.

As @Carl says, all instances should be in scope everywhere. The exception is compiling so-called 'orphan instances' -- which is a Bad Thing and easy to avoid.

For the record here, the approach is to use an Associated type in your class, with a default definition. This works if you are genuinely happy for the Associated type to throw a 'no instance' error if there's no match to the constraint:

class A t where
  type MatchesA t :: Bool           -- Associated type
  type instance MatchesA t = True   -- default instance
  ...                               -- methods for A

instance A Int where
                                    -- uses default instance for MatchesA
  ...                               -- method implementations as usual

-- undefined :: (MatchesA Int)      -- gives type True
-- undefined :: (MatchesA Bool)     -- gives 'no instance' error

You can get an either-or Matches constraint I think -- see the cafe post for MatchesA or MatchesB. (I've tested that quickly, it might be a bit flakey, depending how eager is the type family reduction.)

What you can't do with this approach is opt for one thing if the constraint holds, but a different thing if it doesn't. So the best you can get is the "fail to reduce". In the cafe post I've linked to a (rather old) wiki page with a more comprehensive approach, which relies on overlapping instances. Associated types don't allow overlaps :-(.

EDIT: There's a deep reason why the compiler won't expose whether some constraint matches, in the way you want for Prelude classes in your comment: you might be using the fact of matching to select some instance of another class C; and there might be a further class D whose instance selection depends on C matching; and A, B's instance selection depends on D. So now we have circular dependencies. This could be further complicated by other instances in other modules the compiler hasn't yet seen.

So all those (apparently) duplicated instances on the wiki page represent that the programmer knows all the instances and how they inter-depend, in a way that the compiler can't figure out.