[GHC] #14887: Explicitly quantifying a kind variable causes a type family to fail to typecheck

[GHC]

#14887: Explicitly quantifying a kind variable causes a type family to fail to
typecheck
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
  (Type checker)                     |
           Keywords:  TypeFamilies,  |  Operating System:  Unknown/Multiple
  TypeInType                         |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program:

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fprint-explicit-kinds #-}
 module Bug where

 import Data.Kind
 import Data.Type.Equality

 type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
   Foo1 (e :: a :~: a) = a :~: a

 type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
   Foo2 k (e :: a :~: a) = a :~: a
 }}}

 `Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind
 variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2`
 does not!

 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/ryanglscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:13:10: error:
     • Couldn't match kind ‘k’ with ‘k1’
       When matching the kind of ‘a’
       Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
     • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
       In the type family declaration for ‘Foo2’
    |
 13 |   Foo2 k (e :: a :~: a) = a :~: a
    |          ^^^^^^^^^^^^^^
 }}}

 (Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k
 a a` is not the same kind as `(:~:) k a a`.)

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