[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
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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

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