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

[GHC]

#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:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

Old description:

> I want to run the following past you (using
> [https://phabricator.haskell.org/D5229 Visible Kind Applications] but may
> be unrelated). The following compiles
>
> {{{#!hs
> {-# Language DataKinds           #-}
> {-# Language KindSignatures      #-}
> {-# Language TypeFamilies        #-}
> {-# Language AllowAmbiguousTypes #-}
>
> import Data.Kind
>
> type Cat ob = Bool -> Type
>
> data Fun :: Cat Type
>
> class F (bool :: Bool) where
>   type Not bool :: Bool
>   foo :: Fun (Not bool)
> }}}
>
> but quantifying `Bool` invisibly all of a sudden I can't use `Not`
>
> {{{#!hs
> {-# Language DataKinds           #-}
> {-# Language RankNTypes          #-}
> {-# Language TypeApplications    #-}
> {-# Language PolyKinds           #-}
> {-# Language KindSignatures      #-}
> {-# Language TypeFamilies        #-}
> {-# Language AllowAmbiguousTypes #-}
>
> import Data.Kind
>
> type Cat ob = forall (b :: Bool). Type
>
> data Fun :: Cat Type
>
> class F (bool :: Bool) where
>   type Not bool :: Bool
>   foo :: Fun @(Not bool)
> }}}
>
> {{{
> $ ghc-stage2 --interactive -ignore-dot-ghci 739_bug.hs
> GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
> [1 of 1] Compiling Main             ( 739_bug.hs, interpreted )
>
> 739_bug.hs:17:16: error:
>     • Type constructor ‘Not’ cannot be used here
>         (it is defined and used in the same recursive group)
>     • In the first argument of ‘Fun’, namely ‘(Not bool)’
>       In the type signature: foo :: Fun @(Not bool)
>       In the class declaration for ‘F’
>    |
> 17 |   foo :: Fun @(Not bool)
>    |                ^^^
> Failed, no modules loaded.
> }}}
>
> Is this restriction warranted

New description:

 I want to run the following past you (using
 [https://phabricator.haskell.org/D5229 Visible Kind Applications] but may
 be unrelated). The following compiles

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

 import Data.Kind

 type Cat = Bool -> Type

 data Fun :: Cat

 class F (bool :: Bool) where
   type Not bool :: Bool
   foo :: Fun (Not bool)
 }}}

 but quantifying `Bool` invisibly all of a sudden I can't use `Not`

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

 import Data.Kind

 type Cat = forall (b :: Bool). Type

 data Fun :: Cat

 class F (bool :: Bool) where
   type Not bool :: Bool
   foo :: Fun @(Not bool)
 }}}

 {{{
 $ ghc-stage2 --interactive -ignore-dot-ghci 739_bug.hs
 GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( 739_bug.hs, interpreted )

 739_bug.hs:17:16: error:
     • Type constructor ‘Not’ cannot be used here
         (it is defined and used in the same recursive group)
     • In the first argument of ‘Fun’, namely ‘(Not bool)’
       In the type signature: foo :: Fun @(Not bool)
       In the class declaration for ‘F’
    |
 17 |   foo :: Fun @(Not bool)
    |                ^^^
 Failed, no modules loaded.
 }}}

 Is this restriction warranted

--

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