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

18 Jan 2019

      #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