[GHC] #13913: Can't apply higher-ranked kind in type family

2 Jul 2017

      #13913: Can't apply higher-ranked kind in type family
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This code doesn't typecheck due to `F2`:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind

 f :: (forall (a :: Type). a -> a) -> Bool
 f g = g True

 type F1 (g :: forall (a :: Type). a -> a) = g True

 type family F2 (g :: forall (a :: Type). a -> a) :: Bool where
   F2 g = g True
 }}}

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:14:6: error:
     • Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’
     • In the first argument of ‘F2’, namely ‘g’
       In the type family declaration for ‘F2’
    |
 14 |   F2 g = g True
    |      ^
 }}}

 This is surprising to me, since `F2` seems like the type family
 counterpart to `f` and `F1`, both of which typecheck.

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