Introducing type variables in class constraint, using ConstraintKinds.

ConstraintCategory.hs

-- * Introducing type variables in class constraint, using ConstraintKinds.
-- * (Using ghc-7.6.3)

{-# LANGUAGE ConstraintKinds, GADTs, TypeFamilies #-}
module ConstraintCategory where

import GHC.Exts (Constraint)

-- Version of Category that can put constraints on the i/o of the category.

class Category cat where
  type C cat a b c :: Constraint
  cid :: C cat a b c => cat a a
  (!) :: C cat a b c
      => cat b c
      -> cat a b
      -> cat a c

-- Two functions combined in a single data type, all variables nicely curried.

data Curried g i f o = Curried (g -> i) (f -> o)

-- A `Curried` packed into a GADT, now the type variables are nicely packed
-- pairwise which *might* allow us to write a constraint `Category` instance
-- for it.

data Uncurried f o where
  Uncurried :: Curried g i f o -> Uncurried (f, g) (o, i)

-- Writing a composition function for `Uncurried` is easy by unpacking,
-- composing the functions, and packing again.

compose
  :: Uncurried (p, j) (o, i)
  -> Uncurried (f, g) (p, j)
  -> Uncurried (f, g) (o, i)
compose (Uncurried (Curried f g))
        (Uncurried (Curried h i))
  = Uncurried (Curried (f . h) (g . i))

-- But NOW... I want to be able to make the `Uncurried` an instance of the
-- constraint Category type class above. Is it possible to give a proper
-- constraint `C` for it? I'm not able to.

-- Unfortunately, this won't type check:

instance Category Uncurried where
  type C Uncurried a b c = ( a ~ (f, g)
                           , b ~ (p, j)
                           , c ~ (o, i)
                           )
  cid = undefined
  (!) = compose

-- Because I cannot just introduce new type variables in the constraint:

-- ConstraintCategory.hs:47:35: Not in scope: type variable `f'
-- ConstraintCategory.hs:47:38: Not in scope: type variable `g'
-- ConstraintCategory.hs:48:35: Not in scope: type variable `p'
-- ConstraintCategory.hs:48:38: Not in scope: type variable `j'
-- ConstraintCategory.hs:49:35: Not in scope: type variable `o'
-- ConstraintCategory.hs:49:38: Not in scope: type variable `i'