Multiple occurrences of the same polykinded type don't unify
Summary
Multiple occurrences of the same polykinded type in a type signature are treated as distinct types, leading to type errors. Type inference creates different kind variables for each occurrence of the type, and won't unify them.
Steps to reproduce
Compiling the following file, GHC reports an error.
{-# LANGUAGE PolyKinds #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where
data Proxy a = P
data Indexed (f :: k -> *) = I
idpi :: Indexed Proxy -> Indexed Proxy
idpi x = x
It infers the type idpi :: forall k k1. Indexed k (Proxy k) -> Indexed k1 (Proxy k1)
, and it reports an error at the expression x
because it's returning the parameter type (with k
) where the return type (with k1
) is expected.
This is just a fancy id function, and I would have liked for GHC to infer forall k. Indexed k (Proxy k) -> Indexed k (Proxy k)
.
Environment
- GHC version used: 8.6.5 (Stack lts-13.22)