[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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 While implementing visible dependent quantification (VDQ), I decided to
 revisit commment:2. Here are some of my findings:

 * I think (4) and (5) are ultimately non-issues, at least for the time
 being. This is because you won't be able to define `f` (or `g` or `h`) in
 the first place:

 {{{
 Bug.hs:17:6: error:
     • Illegal visible, dependent quantification in the type of a term:
       forall a -> a -> *
       (GHC does not yet support this)
     • In the expansion of type synonym ‘KindOf1’
       In the type signature: f :: KindOf1 A
    |
 17 | f :: KindOf1 A
    |      ^^^^^^^^^
 }}}

   Since terms aren't meant to have types with VDQ in them, I don't think
 it's worth fretting over (4) and (5). Of course, if VDQ //does// ever
 become permitted in terms, perhaps this will pop back up.
 * (1) appears to be unrelated to VDQ and is actually a quirk of
 `ImpredicativeTypes`. Here is an example to illustrate what I mean:

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

 import Data.Kind

 type family F (f :: forall a. a -> Type) where
   F f = f Int
 }}}

   This doesn't typecheck:

 {{{
 Bug.hs:9:5: error:
     • Expected kind ‘forall a. a -> *’, but ‘f’ has kind ‘* -> k0’
     • In the first argument of ‘F’, namely ‘f’
       In the type family declaration for ‘F’
   |
 9 |   F f = f Int
   |     ^
 }}}

   However, if you enable `ImpredicativeTypes`, then it //does// typecheck!
 It's unclear to me why exactly that is, however.

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