Specifying constraints on existentials from the outside

Learn
#1

I have a type wrapping an existential, where I want to choose the instances the wrapped value has “from the outside”:

data Foo :: [Type -> Constraint] -> Type where
  Foo :: (a `HasInstances` cs) => a -> Foo cs

type family HasInstances (x :: Type) (cs :: [Type -> Constraint]) :: Constraint where
  HasInstances x '[] = ()
  HasInstances x (c ': cs) = (c x, x `HasInstances` cs)

I can write instances for Foo if I explicitly specify the contents of the constraint constructor list:

instance Eq (Foo '[Eq, Typeable]) where
  (Foo (x :: a)) == (Foo (y :: a')) =
    fromMaybe False do
      HRefl <- eqTypeRep (typeRep @a) $ typeRep @a'
      pure $ x == y

But I’d like to not hard-code the contents of the type-level list. I’d rather specify that the list contains the things I need but it’s ok if the list contains other constraints.

I’ve tried this approach by ensuring that the specific Type -> Constraint constraint constructors are in the list:

instance
  ( Eq `Elem` cs
  , Typeable `Elem` cs
  ) => Eq (Foo cs) where
  (Foo (x :: a)) == (Foo (y :: a')) =
    fromMaybe False do
      HRefl <- eqTypeRep (typeRep @a) $ typeRep @a'
      pure $ x == y

type Elem a as = ElemGo a as as
type family ElemGo (a :: k) (as :: [k]) (as' :: [k]) :: Constraint where
  ElemGo a (a ': as) as' = ()
  ElemGo y (a ': as) as' = ElemGo y as as'
  ElemGo a '[] as' =
    TypeLits.TypeError
      ( 'TypeLits.ShowType a
          ':<>: 'TypeLits.Text " is not an element of "
          ':<>: 'TypeLits.ShowType as'
      )

That Eq (Foo cs) instance doesn’t compile, where GHC reports it could not deduce Typeable and Eq in the usages of typeRep and ==.

The combination of ensuring that the constraint constructors are in the list plus the fact that the Foo constructor specifies that every constraint constructor in the list is applied to the wrapped value aren’t enough to convince GHC that things are all good.

Is there a way I can nudge GHC towards allowing this? The full example is available in a gist.

1 Like
#2

A powerful approach to solve these kinds of problems is to provide and use value-level evidence for your desired type-level properties. In this particular case, you can introduce a GADT like

type Index :: k -> [k] -> Type
data Index x xs where
  IZ :: Index x (x : xs)
  IS :: Index x xs -> Index x (y : xs)

which is a value-level witness for type-level list membership. For example, when cs is [Eq, Show], IS :: Index Eq cs proves that Eq is in the list as the first element, and IZ IS :: Index Show cs that Show is in the list as the second element.

You can construct these Indexes automatically via typeclass induction:

class ElemIndex a as where
  elemIndex :: Index a as

instance {-# OVERLAPS #-} ElemIndex a (a : as) where
  elemIndex = IZ

instance (ElemIndex a as) => ElemIndex a (b : as) where
  elemIndex = IS elemIndex

We also write

type Elem a as = ElemIndex a as

for brevity, but you could also take this opportunity to display a nice error message when a is not an element of as as you do above.

I am going to use two small things from sop-core here for convenience, but they could also be easily inlined:

  • All c xs means that we have have c a for all list elements a in xs.
  • Dict c a is value-level evidence that the constraint c a is satisfied.

First, when a constraint c is satisfied for all xs, and a is an element in xs, then c is in particular satisfied for a:

dictIndexAll :: forall a c xs. (All c xs) => Index a xs -> Dict c a
dictIndexAll = \case
  IZ -> Dict
  IS ix -> dictIndexAll ix

Next, we define reverse constraint application, which also allows us to define your HasInstances in a different way:

type AppConstraint :: k -> (k -> Constraint) -> Constraint
class (c a) => AppConstraint a c
instance (c a) => AppConstraint a c

type HasInstances a cs = All (AppConstraint a) cs

Now, when a has instances for all constraints in cs, and c is a element of cs, a has an instance of c in particular:

dictElem :: forall a c cs. (a `HasInstances` cs, c `Elem` cs) => Dict c a
dictElem = case dictIndexAll @c @(AppConstraint a) @cs elemIndex of Dict -> Dict

Now, we have all the pieces to implement your desired Eq (Foo cs) instance:

instance (Eq `Elem` cs, Typeable `Elem` cs) => Eq (Foo cs) where
  Foo (a :: a) == Foo (a' :: a')
    | Dict <- dictElem @a @Typeable @cs,
      Dict <- dictElem @a' @Typeable @cs,
      Just Refl <- eqT @a @a',
      Dict <- dictElem @a @Eq @cs =
        a == a'
  _ == _ = False

We can test it by e.g. writing

test :: Foo [Show, Typeable, Eq] -> Bool
test a = a == Foo (123 :: Int)

and playing around with it in GHCI and check that the results are indeed what we expect:

 Λ test (Foo (123 :: Int))
True
 Λ test (Foo (42 :: Int))
False
 Λ test (Foo (123 :: Integer))
False
 Λ test (Foo "foo")
False

Full code is here: Foocs.hs · GitHub

1 Like
#3

Thank you - this looks to be just what I’m after!