When (if ever) can type synonyms be partially applied?

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?

Jelle

This behaviour is enabled by LiberalTypeSynonyms. Specifically, with it enabled, the compiler will expand out all type synonyms before doing the check for partially applied type synonyms. I'm guessing that one of TypeFamilies or ContraintKinds implies LiberalTypeSynonyms. – Whorl

@Whorl Strangely enough, they don't imply it. – Mandiemandingo

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.

Prolusion

Answer 2

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.

Tlemcen

Answer 3

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.

Crystallization