Apply constraint within constraint in Haskell

Question

Is there anyway to apply a constraint within another constraint such that this

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}

module Test where

type Con a = (Num a, Show a)
type App c a b = (c a, c b)

program :: App Con a b => a -> b -> String
program a b = show a ++ " " ++ show (b+1)

will work?

Currently GHC is giving me the following errors:

[1 of 1] Compiling Test             ( Test.hs, interpreted )

Test.hs:9:12: error:
    • Expected a constraint, but ‘App Con a b’ has kind ‘*’
    • In the type signature: program :: App Con a b => a -> b -> String
  |
9 | program :: App Con a b => a -> b -> String
  |            ^^^^^^^^^^^

Test.hs:9:16: error:
    • Expected kind ‘* -> *’, but ‘Con’ has kind ‘* -> Constraint’
    • In the first argument of ‘App’, namely ‘Con’
      In the type signature: program :: App Con a b => a -> b -> String
  |
9 | program :: App Con a b => a -> b -> String
  |                ^^^
Failed, no modules loaded.

Thanks!

Answer 1

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.

Answer 2

Haskell does not support type-level lambdas, nor partial application of type families / type synonyms. Your Con must always be fully applied, it can not passed unapplied to another type synonym.

At best, we can try to use "defunctionalization" as follows, effectively giving names to the type-level lambdas we need.

{-# LANGUAGE ConstraintKinds, KindSignatures, TypeFamilies #-}

import Data.Kind

-- Generic application operator
type family Apply f x :: Constraint

-- A name for the type-level lambda we need
data Con
-- How it can be applied
type instance Apply Con x = (Show x, Num x)

-- The wanted type-level function
type App c a b = (Apply c a, Apply c b)

-- Con can now be passed since it's a name, not a function
program :: App Con a b => a -> b -> String
program a b = show a ++ " " ++ show (b+1)

To call App with a different first argument, one would need to repeat this technique: define a custom dummy type name (like Con) and describe how to apply it (using type instance Apply ... = ...).