[Haskell-cafe] Question about kinds

[Derek Elkins]

On Fri, 2008-06-06 at 15:41 -0700, Klaus Ostermann wrote:
> Why does the code below not pass the type checker?
> 
> 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.
> 
> 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

Down this path is higher-order unification which is undecidable.

You can use a newtype.