[GHC] #11453: Kinds in type synonym/data declarations can unexpectedly unify

[GHC]

#11453: Kinds in type synonym/data declarations can unexpectedly unify
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 While trying out ideas to fix [https://github.com/ekmett/lens/issues/626
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11453>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler