Re: [GHC] #15942: Type family used invisibly (with Visible Kind Applications)

24 Nov 2018

      #15942: Type family used invisibly (with Visible Kind Applications)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
                                     |  TypeApplications
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I don't think this has anything to do with VKA. The distinction that GHC
 appears to be making is whether `Not` is used in a kind position (as
 opposed to a type position) within `F`. Note that the following is also
 rejected:

 {{{#!hs
 {-# Language DataKinds           #-}
 {-# Language KindSignatures      #-}
 {-# Language PolyKinds           #-}
 {-# Language TypeFamilies        #-}
 {-# Language AllowAmbiguousTypes #-}

 import Data.Kind
 import Data.Proxy

 type G = Bool -> Type

 data Fun :: G

 class F (bool :: Bool) where
   type Not bool :: Bool
   foo :: Proxy (x :: Proxy (Not bool))
 }}}
 {{{
 $ ~/Software/haskell/ghc-8.6.2/bin/ghc Bug.hs
 [1 of 1] Compiling Main             ( Bug.hs, Bug.o )

 Bug.hs:16:29: error:
     • Type constructor ‘Not’ cannot be used here
         (it is defined and used in the same recursive group)
     • In the first argument of ‘Proxy’, namely ‘(Not bool)’
       In the kind ‘Proxy (Not bool)’
       In the first argument of ‘Proxy’, namely ‘(x :: Proxy (Not bool))’
    |
 16 |   foo :: Proxy (x :: Proxy (Not bool))
    |                             ^^^
 }}}

 As for whether this restriction is warranted in the first place, I don't
 know if I'm qualified to say. I do know that there are other tickets that
 aim to relax this restriction under certain scenarios: see #11962 and
 #12612. It's unclear to me whether this ticket is covered by one of those
 tickets already, however.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15942#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler