Opened 10 months ago

Last modified 9 months ago

#15942 new bug

Associated type family can't be used at the kind level within other parts of parent class

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.2
Keywords: TypeApplications, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11962, #12612 Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

I want to run the following past you (using Visible Kind Applications but may be unrelated). The following compiles

{-# 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

{-# 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

Change History (7)

comment:1 Changed 10 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 10 months ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 10 months ago 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:

{-# 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.

comment:4 Changed 10 months ago by goldfire

I think this is independent from #12612, though a full fix for #11962 should almost certainly fix both #12612 and this ticket. That said, #11962 is a Major Engineering Project (Google Summer of Code, anyone?) and it's likely a fine idea to take slices off that pie like this ticket.

comment:5 Changed 10 months ago by simonpj

Keywords: TypeInType added

comment:6 Changed 10 months ago by RyanGlScott

Summary: Type family used invisibly (with Visible Kind Applications)Associated type family can't be used at the kind level within other parts of parent class

comment:7 Changed 9 months ago by bgamari

Milestone: 8.6.3

Ticket retargeted after milestone closed

Note: See TracTickets for help on using tickets.