Kinds in type synonym/data declarations can unexpectedly unify

While trying out ideas to fix this lens issue, I noticed a couple of peculiar things about kinds in type synonym and data declarations. For example:

$ /opt/ghc/head/bin/ghci -XTypeInType -XRankNTypes -XTypeOperators
GHCi, version 8.1.20160113: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/xnux/.ghci
λ> import Data.Kind
λ> type Wat (a :: k2) (b :: k3) = forall (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
  forall (f :: k1 -> *). Either (f a) (f b)
        -- Defined at <interactive>:2:1

This is pretty odd for two reasons. One, the kind k1 was never specified (either existentially or as a visible kind binder), so that definition should have been rejected. But even if we do use an existential kind:

λ> type Wat (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)
λ> :i Wat
type Wat (a :: k1) (b :: k1) =
  forall k2 (f :: k2 -> *). Either (f a) (f b)
        -- Defined at <interactive>:4:1

We still see the second issue: GHC thinks that the type variables a and b have the same kind k1, when they should have separate kinds k1 and k2! That behavior is very surprising to me, since it seems like GHC is choosing to unify two kind variables that should be rigid.

Note that this doesn't happen if you use explicit kind binders:

type Wat k2 k3 (a :: k2) (b :: k3) = forall k1 (f :: k1 -> *). Either (f a) (f b)

<interactive>:6:74: error:
    • Expected kind ‘k1’, but ‘a’ has kind ‘k2’
    • In the first argument of ‘f’, namely ‘a’
      In the first argument of ‘Either’, namely ‘f a’
      In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’

<interactive>:6:80: error:
    • Expected kind ‘k1’, but ‘b’ has kind ‘k3’
    • In the first argument of ‘f’, namely ‘b’
      In the second argument of ‘Either’, namely ‘f b’
      In the type ‘forall k1 (f :: k1 -> *). Either (f a) (f b)’

only when the kinds are specified but not visible.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture

mentioned in issue #11203 (closed)

changed weight to 5

added Tbug Trac import TypeInType typechecker labels

closed

These weirdnesses are all a direct consequence of #11203 (closed). They are not a consequence of TypeInType.

However, these are very helpful examples in looking at #11203 (closed).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

mentioned in issue #14451 (closed)

added error messages label

added Pnormal label