Partial application of type constructors?

Simon Peyton-Jones simonpj at
Wed Apr 20 00:00:43 EDT 2005

Allowing partially applied type synonyms amounts to allowing lambda at
the type level, and that requires higher-order unification, and loses
principal types (I think).  So as of today, they are definitely out.

If you look at the paper about "boxy types" on my home page, you'll see
ways of extending type inference to support higher rank types and
impredicativity.  Next on the list is lambdas at the type level, in the
same spirit: that is, support type inference by asking the programmer to
help at "key moments".  But don't hold your breath.


| -----Original Message-----
| From: glasgow-haskell-users-bounces at
| bounces at] On Behalf Of Conal Elliott
| Sent: 19 April 2005 05:21
| To: glasgow-haskell-users at
| Subject: Partial application of type constructors?
| GHC 6.4 objects to the following simple program, pointing to the
| application of the type constructor AddL.  Is there a work-around?
|     {-# OPTIONS -fglasgow-exts #-}
|     data LMap a b
|     type AddL arr a b = a `arr` LMap a b
|     data DFunA arr a b = DFunA (a `arr` b) (DFunA (AddL arr) a b)
| The complete error message:
|     Type synonym `AddL' should have 3 arguments, but has been given 1
|     When checking the data constructor:
|       forall arr a b. DFunA (arr a b) (DFunA (AddL arr) a b)
|     In the data type declaration for `DFunA'
| Is there a serious difficulty with handling partial type applications?
| 	- Conal
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at

More information about the Glasgow-haskell-users mailing list