Is there a general way to apply constraints to a type application?

Question

A comment by user 2426021684 led me to investigate whether it was possible to come up with a type function F such that F c1 c2 fa demonstrates that for some f and a:

1. fa ~ f a
2. c1 f
3. c2 a

It turns out that the simplest form of this is quite easy. However, I found it rather difficult to work out how to write a poly-kinded version. Fortunately, I managed to find a way as I was writing this question.

Answer 1

First, some boilerplate:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module ConstrainApplications where

import GHC.Exts (Constraint)
import Data.Type.Equality

Now type families to deconstruct applications at arbitrary kinds.

type family GetFun a where
  GetFun (f _) = f
type family GetArg a where
  GetArg (_ a) = a

Now an extremely general type function, more general than necessary to answer the question. But this allows a constraint involving both components of the application.

type G (cfa :: (j -> k) -> j -> Constraint) (fa :: k)
  = ( fa ~ (GetFun fa :: j -> k) (GetArg fa :: j)
    , cfa (GetFun fa) (GetArg fa))

I don't like offering constraint functions without classes to match, so here's a first-class version of G.

class G cfa fa => GC cfa fa
instance G cfa fa => GC cfa fa

It's possible to express F using G and an auxiliary class:

class (cf f, ca a) => Q cf ca f a
instance (cf f, ca a) => Q cf ca f a

type F cf ca fa = G (Q cf ca) fa

class F cf ca fa => FC cf ca fa
instance F cf ca fa => FC cf ca fa

Here are some sample uses of F:

t1 :: FC ((~) Maybe) Eq a => a -> a -> Bool
t1 = (==)

-- In this case, we deconstruct the type *twice*:
-- we separate `a` into `e y`, and then separate
-- `e` into `Either x`.
t2 :: FC (FC ((~) Either) Show) Show a => a -> String
t2 x = case x of Left p -> show p
                 Right p -> show p

t3 :: FC Applicative Eq a => a -> a -> GetFun a Bool
t3 x y = (==) <$> x <*> y