Type aliases for constraints do not use the same variable binding behavior as contexts

Question

I played with -XConstraintKindsto facilitate overly detailed contexts and found an interesting inconsistency regarding 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 any workaround for this other than casting callTreeto the top-level area?

Answer 1

There is no real inconsistency, just that

• Free type variables in the type signature are automatically added quantifiers forall, so the first case is really equivalent

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

• type , , .

, , forall , , .

( OtherTypeFunc input ~ SomeTypeFunc output ) , , , .

, -, :

{-# 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