When (if ever) can type synonyms be partially appl

Question

Apparently a bit absent-mindedly, I wrote something like the following:

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE TypeFamilies        #-}

class Foo f where
  type Bar f :: *
  retbar :: Bar f -> IO f

type Baz f = (Foo f, Eq f)

  -- WithBar :: * -> (*->Constraint) -> * -> Constraint
type WithBar b c f = (c f, Bar f ~ b)

instance Foo () where
  type Bar () = ()
  retbar = return

naim :: WithBar () Baz u => IO u  -- why can I do this?
naim = retbar ()

main = naim :: IO ()

Only after successfully compiling, I realised this shouldn't actually work: Baz is defined as a type synonym with one argument, but here I use it without a direct argument. Usually GHC barks at me Type synonym ‘Baz’ should have 1 argument, but has been given none when I try something like that.

Now, don't get me wrong: I would really like being able to write that, and it's easy enough to see how it could work in this particular example (simply inlining WithBar would yield the signature naim :: (Foo u, Bar u ~ ()) => IO u, which is certainly fine), but what I don't understand why it actually works just like that here. Is it perhaps only a bug in ghc-7.8.2 to allow this?

Answer 1

Your file compiles in GHC 7.8, but in GHC 7.10 I get an error:

Type synonym ‘Baz’ should have 1 argument, but has been given none

In the type signature for ‘naim’: naim :: WithBar () Baz u => IO u

Adding -XLiberalTypeSynonyms fixes the error. Therefore, this is a bug in 7.8.

Answer 2

I don't know what the official rules are, but it seems reasonable for this sort of thing to work on the basis of a leftmost-outermost type synonym expansion strategy. The only thing that matters is that type synonyms can be disposed of in a separate and terminating phase, before the rest of typechecking happens. I don't know whether it's intended that you can use a partially applied type synonym F as an argument to another type synonym G, just as long as G ensures that F receives its missing arguments, but that's certainly consistent with the idea that type synonyms are a shallow convenience.

Answer 3

Partial application should be enabled by the LiberalTypeSynonyms extension.

Basically this defers most consistency checking of type synonyms until they have been expanded, so your "inlining" explanation is essentially the right idea.

The strange thing here, though, is that this extension is not implied by the ones in your module. I just tested, and partial application doesn't work in general with just ConstraintKinds, TypeFamilies and PolyKinds. (I added the latter because kinds are checked before expansion and my test types got inferred the wrong ones otherwise.)

Nevertheless, your file loads fine for me in GHCi 7.8.3. Maybe this is some kind of bug, even if there is an extension to make it properly legal.