[GHC] #15942: Type family used invisibly (with Visible Kind Applications)
#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
#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
#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
#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
#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 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15942#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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, TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeApplications => TypeApplications, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15942#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15942: Associated type family can't be used at the kind level within other parts of parent class -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: | TypeApplications, TypeInType 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #11962, #12612 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15942#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC