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)