2

I also tried the following with the LiberalTypeSynonyms extension as suggested in When (if ever) can type synonyms be partially applied?, and have added an explicit kind signiture to f in Id's definition. I still got the same error. I don't know if there are other extensions that might help.

ghci> type Id a = a
ghci> type Const a b = a
ghci> data D f = D (f ())
ghci> (((() :: Id ()) :: ()) :: Const () a)
()
ghci> D () :: D Id

<interactive>:10:9:
    Type synonym ‘Id’ should have 1 argument, but has been given none
    In an expression type signature: D Id
    In the expression: D () :: D Id
    In an equation for ‘it’: it = D () :: D Id

This really confuses me. f in D is * -> * and Id is * -> *. What more is there to this?

JoL
  • 1,017
  • 10
  • 15
  • 1
    Partially applied type synonyms are essentially equivalent to type-level lambdas, which make the type checking algorithm much more complex. GHC does not allow them. Use `newtype`s or `data`s wrappers instead, and wrap/unwrap your values with a constructor as needed. Otherwise, switch to Agda or Coq :-P – chi Jun 23 '16 at 17:20
  • 2
    By the way, the liberal-type-synonyms rule does not give you much more flexibility, only a little. If after the expansion of all the type-synonyms, we still have partially applied ones, a type error is triggered. If you had `type D f = f ()` instead, the extension would allow for your code. But `D f` would be the same type as `f ()`. – chi Jun 23 '16 at 17:23
  • @chi that clarifies the extension for me. Unfortunately, in my particular problem, I can't have D be a type synonym, but I might manage with having Id and Const be newtypes. Your "it's too complex for GHC" comment qualifies as an answer. I might accept it if you post it as so, but maybe I should wait a little more, in case someone else wants to post too. – JoL Jun 23 '16 at 17:44
  • [I also fell for something like this once](http://stackoverflow.com/questions/24881351/why-cant-you-totally-apply-a-type-synonym-that-has-arguments-using-an-other-t). – Bakuriu Jun 23 '16 at 18:05
  • @Bakuriu looks like I posted a duplicate. I couldn't find your question. Sorry, guys. – JoL Jun 23 '16 at 18:18
  • 1
    @Bakuriu Both of the examples in your question compile with `LiberalTypeSynonyms`; whereas the example in this question does not compile even with `LiberalTypeSynonyms`. So I agree with you that it is related, but not with jlmg that it is a duplicate. – Daniel Wagner Jun 23 '16 at 23:15

1 Answers1

4

Haskell's type system does not support partially applied (also known as unsaturated) type synonyms or families. data types and newtypes do support partial application, though.

newtype D f = D (f ())
newtype Id a = Id a

d :: D Id
d = D (Id ())

newtypes are erased during compilation, so the only cost you're paying is a syntactic one.

Benjamin Hodgson
  • 42,952
  • 15
  • 108
  • 157
  • 3
    Except when it's not :(. Ed Kmett wants to add `liftCoercion :: Maybe (Coercion a b -> Coercion (f a) (f b))` to the `Functor` class, and similar methods to `Contravariant`, `Bifunctor` and `Profunctor`, to make coercions more generally applicable and thus more newtypes free. – dfeuer Jun 24 '16 at 00:42