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.