type error trying to specialize polymorphic function

[nr]

The attached module won't compile---definition of 'wrap' is rejected. The error message is

[ 1 of 13] Compiling Pain             ( Pain.hs, Pain.o )

Pain.hs:18:7:
    Couldn't match expected type `n C O' against inferred type `C'
      Expected type: ExTriple (Counter n)
      Inferred type: ExTriple (->)
    In the expression: scalar
    In the definition of `wrap': wrap = scalar

The inferred type is alarming, and in any case the type of wrap is a straightforward specialization of the type of scalar.

Could the problem be with liberal type synonyms? I don't think we're doing anything unreasonable...

[igloo]

Slightly simplified:

{-# LANGUAGE RankNTypes, EmptyDataDecls, LiberalTypeSynonyms #-}

module Pain
where

data O
data C

type Counter n e x = n e x -> Int

scalar :: (forall e x . a e x)
       -> (a C O, a O O, a O C)
scalar z = (z, z, z)

wrap :: (forall e x . Counter n e x)
     -> (Counter n C O, Counter n O O, Counter n O C)
wrap = scalar

with HEAD:

Pain.hs:17:8:
    Couldn't match expected type `n C O' against inferred type `C'
      Expected type: (Counter n C O, Counter n O O, Counter n O C)
      Inferred type: (C -> O, O -> O, O -> C)
    In the expression: scalar
    In the definition of `wrap': wrap = scalar

(LiberalTypeSynonyms is actually no longer needed).

[simonpj]

The program isn't well-typed, and is rightly rejected. Remember that type checking proceeds as if type synonyms were expanded eagerly. So the type signature for 'scalar' is identical to

wrap :: (forall e x . n e x -> Int)
       -> (n C O -> Int, n O O -> Int, n O C -> Int)

Now when matching, say (a C O ~ (n C O -> Int)), the only solution is that a is instantiate to (->), and you can see how things go wrong.

In short, GHC does not do higher order unification. You could make htis work by using a newtype for Counter.

Simon