An easy way to fix this is to use the LiberalTypeSynonyms extension. This extension allows GHC to first treat the type synonyms as substitutions and only afterwards check that the synonyms are fully applied. Note that GHC can be a little silly at kind inference, so you'll need to be very clear with it (i.e., an explicit signature). Try this:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
module Test where
import Data.Kind (Constraint)
type Con a = (Num a, Show a)
type App c a b = (c a, c b) :: Constraint
program :: App Con a b => a -> b -> String
program a b = show a ++ " " ++ show (b+1)
Before I understood that this could be solved with LiberalTypeSynonyms, I had a different solution, which I'll keep here in case anyone's interested.
Although the error message you're getting is a bit misleading, the fundamental problem with your code comes down to the fact that GHC does not support partial application of type synonyms, which you have in App Con a b. There are a few ways to fix this, but I find the simplest is to convert the type synonym constraint into a class constraint following this pattern:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
type Con' a = (Num a, Show a)
class Con' a => Con a
instance Con' a => Con a
You can use this definition of Con anywhere you were intending to use your old one.
If you're interested in how/why this works, it's basically a trick to get around GHC's lack of support for partial type synonym/family application for the particular cases where those type synonyms/families define simple constraints.
What we're doing is defining a class, and every class comes with a constraint of the same name. Now, notice that the class has no body, but critically, the class itself has a constraint (in the above case Con' a), which means that every instance of the class must have that same constraint.
Next, we make an incredibly generic instance of Con, one that covers any type so long as the constraint Con' holds on that type. In essence, this assures that any type that is an instance of Con' is also an instance of Con, and the Con' constraint on the Con class instance assures that GHC knows that anything that's an instance of Con also satisfies Con'. In total, the Con constraint is functionally equivalent to Con', but it can be partially applied. Success!
As another side note, the GHC proposal for unsaturated type families was recently accepted, so there may be a not-too-far-off future where these tricks are unnecessary because partial application of type families becomes allowed.
