[GHC] #15869: Discrepancy between seemingly equivalent type synonym and type family

7 Nov 2018

      #15869: Discrepancy between seemingly equivalent type synonym and type family
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.2
  (Type checker)                     |
           Keywords:  TypeFamilies   |  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:
-------------------------------------+-------------------------------------
 Consider the following code:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}

 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind

 type KindOf1 (a :: k) = k
 type family KindOf2 (a :: k) :: Type where
   KindOf2 (a :: k) = k

 data A (a :: Type) :: a -> Type
 type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
   Apply1 f a x = f a x
 }}}

 `Apply1` kind-checks, which is just peachy. Note that `Apply1` uses
 `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1`
 for `KindOf2`, which is (seemingly) an equivalent type family. I can
 define this:

 {{{#!hs
 type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type)
                    (a :: Type)
                    (x :: a)
                 :: Type where
   Apply2 f a x = f a x
 }}}

 However, GHC rejects this!

 {{{
 $ /opt/ghc/8.6.2/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:25:10: error:
     • Expecting two more arguments to ‘f’
       Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’
     • In the first argument of ‘Apply2’, namely ‘f’
       In the type family declaration for ‘Apply2’
    |
 25 |   Apply2 f a x = f a x
    |          ^
 }}}

 I find this quite surprising, since I would have expected `KindOf1` and
 `KindOf2` to be functionally equivalent. Even providing explicit `forall`s
 does not make it kind-check:

 {{{#!hs
 type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type)
                    (a :: Type)
                    (x :: a)
                 :: Type where
   forall (f :: KindOf2 A) (a :: Type) (x :: a).
     Apply2 f a x = f a x
 }}}

 Although the error message does change a bit:

 {{{
 $ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:26:20: error:
     • Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’
     • In the type ‘f a x’
       In the type family declaration for ‘Apply2’
    |
 26 |     Apply2 f a x = f a x
    |                    ^^^^^
 }}}

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