[Haskell-cafe] Question about kinds

[Claus Reinke]

short answer: use newtype instead of type (and check the
language spec for the difference between the two).

> Why does the code below not pass the type checker?

because of the type error?-) seriously, though, it is useful to
accompany such questions with some indication of what you're
trying to do, to put a cap on the wide variety of possible answers
(depending on what it is you're trying to achieve, there are many
different techniques or tricks that might apply), and to have 
something to compare the non-working code against (also in
case the intention needs to be edited before working code
can be suggested).
 
> If I could explictly parameterize y with the type constructor Id (as e.g. in
> System F), then 'y Id' should have the type Int -> Int
> and hence "y Id x" should be OK, but with Haskell's implicit type parameters
> it does not work.

schemes that rely on implicit 'Id' tend to be doomed to failure
in haskell and often suggest a need to get better acquainted
with the limitations of haskell's type system (such schemes 
often arise from invalid generalisations of promising features,
and many of us, myself included, have fallen into that trap at 
one point or other, often while working with type constructor
classes):

- type synonyms are syntactic macros, not part of the
    type system proper; the error message is a bit 
    confusing by trying to be helpful (giving type synonym
    applications instead of their expansion: the type system
    has seen 'Int', not 'Id Int')
- things of kind (* -> *) are type _constructors_, not
    arbitrary type functions
- type families are a restricted kind of type function, but
    can only be applied forwards (F t1 ~> t2), not be
    inferred or abstracted over

simplified, if the type system had to _infer_ 'Id' (or the
composition of type constructors, a related favourite;-),
it could do so anywhere, any number of times. in haskell's
approach to this, programmers have to indicate where
such things are meant to occur (eg, by using newtypes).

hth,
claus

> So, how can I make this work?
> 
> Klaus
> ------------
> 
> type Id a = a
> 
> x :: Id Int
> x = undefined
> 
> y :: (a Int) -> (a Int)
> y = undefined
> 
> test = y x
> 
> Error:
>  Couldn't match expected type `a Int' against inferred type `Id Int'
>  In the first argument of `y', namely `x'
>  In the expression: y x
>  In the definition of `test': test = y x
> 
> 
> -- 
> View this message in context: http://www.nabble.com/Question-about-kinds-tp17701553p17701553.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe