Type Aliases for Constraints don't share the same variable binding behavior as Contexts

Question

I've been playing with -XConstraintKinds to help alleviate excessively verbose contexts, and have found an interesting inconsistency in terms of variable binding:

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

-- works
foo :: ( callTree ~ SomeTypeFunc output
       , OtherTypeFunc input ~ callTree
       ) => input -> output


type FooCtx input output =
  ( callTree ~ SomeTypeFunc output
  , OtherTypeFunc input ~ callTree
  )

-- doesn't work
foo' :: FooCtx input output =>
        input -> output

Is there a work-around for this, other than bringing callTree to the top-level scope?

Answer 1

There is no real inconsistency, it's just that

1. Free type variables in a type signature have forall quantifiers automatically added, so the first case is really equivalent to

   foo :: forall callTree output input. ( callTree ~ SomeTypeFunc output
          , OtherTypeFunc input ~ callTree
          ) => input -> output
   

2. All free type variables on the right side of a type declaration must be parameters, you cannot have any that are not in scope.

This is not specific to constraint kinds, except for the unfortunate fact that you cannot apply forall quantifiers directly to a constraint, which means I don't know a general workaround to make such a constraint type declaration work.

In your particular example, ( OtherTypeFunc input ~ SomeTypeFunc output ) should be equivalent, but I assume you're really interested in a more complicated example where such a rewriting doesn't work.

I can think of a different kind of workaround that changes the parameters to the type declaration in a different way, by including the value on the right side of the constraint:

{-# LANGUAGE TypeFamilies, ConstraintKinds, FlexibleContexts, RankNTypes #-}

type family OtherTypeFunc a
type family SomeTypeFunc a

type FooCtx input output value =
  forall callTree. ( callTree ~ SomeTypeFunc output
  , OtherTypeFunc input ~ callTree
  ) => value

-- This now works
foo' :: FooCtx input output ( input -> output )

foo' = undefined