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

23 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:                    |
-------------------------------------+-------------------------------------
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 = 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
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 G = Bool -> Type

 data Fun :: G

 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 G = forall (b :: Bool). Type

 data Fun :: G

 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:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler