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

[GHC]

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

Old description:

> 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
>    |                    ^^^^^
> }}}

New description:

 Consider the following code:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE LiberalTypeSynonyms #-}
 {-# 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#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler