Deciding constraints for a GADT tag datatypes?

Not sure how to name this question, so the title may be misleading. The question is clear I think: let’s say you have a datatype like

data TRep a where
  TInt :: TRep Int
  TList :: TRep a -> TRep [a]
  TFun :: TRep a -> TRep b -> TRep (a -> b)

Is there a way to “autoderive” a function like

decideConstr :: forall c a. Typeable c => TRep a -> Maybe (Dict (c a))

Currently I need to implement it for every “interesting” constraint, like

decideEq :: TRep a -> Maybe (Dict (Eq a))
decideEq TInt = pure Dict
decideEq (TList a) = do
  Dict <- decideEq a
  pure Dict
decideEq (TFun _a _b) = empty

and so on (obviously I have many more representable types, so it’s a very annoying copypaste exercise). Is there any existing library that deals with it? I understand it can be tad complicated, as it’s not a matter of simply lifting Dict from all cases (like in the Eq function example).

You can create a template for the GADT that constrains the types it is indexed by. cls Int means the constraint holds for TInt and for TList we need a quantified constraint forall x. cls x => cls [x] saying if it holds for the element type it holds for the list.

The template assumes the class does not hold for function types.

decideConstr
  :: forall cls a. ()
  => cls Int
  => (forall x. cls x => cls [x])
  => TRep a
  -> Maybe (Dict (cls a))
decideConstr = \case
  TInt ->
    pure Dict
  TList rep -> do
    Dict <- decideConstr @cls rep
    pure Dict
  TFun{} ->
    empty

You can specialize this to whatever cls satisfies those constraints.

-- >> decideEq TInt
-- Just Dict
-- >> decideEq do TList do TList TInt
-- Just Dict
-- >> decideEq do TFun TInt TInt
-- Nothing
decideEq :: TRep a -> Maybe (Dict (Eq a))
decideEq = decideConstr @Eq
2 Likes