[GHC] #11719: Cannot use higher-rank kinds with type families
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1-rc2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell- cafe/2016-March/123462.html Here's the code that should work, but doesn't: {{{ import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * type family (f :: a ~> b) @@ (x :: a) :: b data Null a = Nullable a | NotNullable a type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where (f ∘ g) x = f @@ (g @@ x) type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :( -- BaseType k x = (@@) k x }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families
-------------------------------------+-------------------------------------
Reporter: ocharles | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1-rc2
checker) |
Resolution: | Keywords:
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 Richard Eisenberg
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => dependent/should_compile/T11719 * status: new => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * failure: None/Unknown => GHC rejects valid program * resolution: => fixed * milestone: => 8.0.1 @@ -7,1 +7,1 @@ - {{{ + {{{#!hs New description: This ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell- cafe/2016-March/123462.html Here's the code that should work, but doesn't: {{{#!hs import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * type family (f :: a ~> b) @@ (x :: a) :: b data Null a = Nullable a | NotNullable a type family ((f :: b ~> c) ∘ (g :: a ~> b)) (x :: a) :: c where (f ∘ g) x = f @@ (g @@ x) type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where -- this fails :( -- BaseType k x = (@@) k x }}} -- Comment: Merged as bae60f654ac5d99834818da9c50ad4bee54c334e. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ocharles): I see this ticket is now marked as "fixed", but the original code example above doesn't type check under this change (as Richard's commit message mentions). Should this ticket be re-opened, or should I open a new ticket? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: fixed => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.0.1 => 8.2.1 Comment: This is out of the scope of 8.0.1 (and perhaps 8.0 entirely). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) * related: => #13913 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Is this another consequence of this limitation? Consider the following program: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type family Sing :: k -> Type data SBool :: Bool -> Type where SFalse :: SBool False STrue :: SBool True type instance Sing = SBool sFalse :: Sing False sFalse = SFalse }}} This typechecks without issue. However, if you change the following line of code: {{{#!hs type family Sing :: k -> Type }}} To become this: {{{#!hs type family Sing :: forall k. k -> Type }}} Then it stops typechecking: {{{ $ /opt/ghc/8.6.1/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:18:10: error: • Couldn't match type ‘SBool’ with ‘Sing’ Expected type: Sing 'False Actual type: SBool 'False • In the expression: SFalse In an equation for ‘sFalse’: sFalse = SFalse | 18 | sFalse = SFalse | ^^^^^^ }}} I find this extremely surprising: I would have thought that GHC could treat `type family Sing :: k -> Type` and `type family Sing :: forall k. k -> Type` identically without the need for any fancy higher-rank business (like what the original program in this ticket requires). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): These two declarations have quite different meanings: {{{#!hs type family F1 :: k -> Type type family F2 :: forall k. k -> Type }}} `F1` takes one argument, `k`. `F2`, on the other hand, takes no arguments. `F1` can match on `k`, returning constructors of different kinds in different instances. On the other hand, `F2` must return a polykinded constructor, and can have only one instance. So, I think this is unrelated to the ticket... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:14 goldfire]:
On the other hand, `F2` must return a polykinded constructor, and can have only one instance.
That doesn't appear to be true, since this program (with multiple `F2` instances) typechecks: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type family F2 :: forall k. k -> Type type instance F2 = SBool type instance F2 = STuple0 data SBool :: Bool -> Type where SFalse :: SBool False STrue :: SBool True data STuple0 :: () -> Type where STuple0 :: STuple0 '() }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): It on HEAD but fails on 8.2.1 (after adding `{-# LANGUAGE TypeInType #-}`) {{{ $ ghci -ignore-dot-ghci 504.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Bug ( 504.hs, interpreted ) 504.hs:12:20: error: • Expected kind ‘forall k. k -> *’, but ‘SBool’ has kind ‘Bool -> *’ • In the type ‘SBool’ In the type instance declaration for ‘F2’ | 12 | type instance F2 = SBool | ^^^^^ 504.hs:13:20: error: • Expected kind ‘forall k. k -> *’, but ‘STuple0’ has kind ‘() -> *’ • In the type ‘STuple0’ In the type instance declaration for ‘F2’ | 13 | type instance F2 = STuple0 | ^^^^^^^ Failed, 0 modules loaded. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): Replying to [comment:14 goldfire]:
These two declarations have quite different meanings:
{{{#!hs type family F1 :: k -> Type type family F2 :: forall k. k -> Type }}}
`F1` takes one argument, `k`. `F2`, on the other hand, takes no arguments. `F1` can match on `k`, returning constructors of different kinds in different instances. On the other hand, `F2` must return a
This statement doesn't sit well with me. I expect to be able to introduce any type variable explicitly, and `F1` with an explicit `forall` for `k` turns out to be `F2`. These declarations ''must'' have the same meaning. Let's compare to term-level functions: {{{#!hs f :: k -> Type f :: forall k. k -> Type }}} These types are the same (modulo specificity of `k`)! polykinded constructor, and can have only one instance. So you mean that we treat `F1` as having kind `pi k. k -> Type`, while `F2` has kind `forall k. k -> Type`: `F1` can match on its parameter `k` and `F2` cannot. Why? I thought we always treat `forall` as `pi` in kinds, at least for now. Therefore, I agree with Ryan's expectations in comment:13. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-index): * cc: int-index (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The difference with terms is that the arity of type families matters. `F1` has arity 1, while `F2` has arity 0. The real question is: where is the `k` bound. In `F1`, `k` is bound "before the colon", while in `F2`, it's bound after the colon. In terms of [https://github.com/goldfirere/ghc- proposals/blob/pi/proposals/0000-pi.rst#the-quantifier-table this syntax]: {{{ F1 :: foreach k . k -> Type F2 :: foreach k '. k -> Type }}} Both are really `foreach`-kinds, like @int-index observed. The difference is that `F1`'s argument is not matchable. (Perversely, type families can pattern-match only on unmatchable arguments. Perhaps a name change is in order.) On the other hand, `F2`'s argument is matchable, as it's declared to be so. (Recall that every abstraction in a kind is currently interpreted as matchable, even though the future syntax for matchable kinds will change.) Accepting the program in comment:15 seems like an egregious bug, to me. I've reported it as #15740. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The difference with terms is that the arity of type families matters. F1 has arity 1, while F2 has arity 0. The real question is: where is the k bound. In F1, k is bound "before the colon", while in F2, it's bound after
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: csongor.kiss14@…, s.eisenbach@…, t.field@… (added) Comment: the colon. Tricky stuff! Could we document this in the user manual? If we end up adopting Csongor's ideas about unsaturated type families (when the matchability shows up in the kind), we'll need to adopt some notation for the forall-case too. I can't say I like `forall k '. k -> Type`! But we clearly need ''something''.
Perversely, type families can pattern-match only on unmatchable arguments. Perhaps a name change is in order.
That is indeed perverse. Worth considering as part of the same effort. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Something to consider (I don't know if I got the typing right, but allowing higher rank kinds in splitting type application) {{{#!hs type RudeWord a = forall xx. xx -> a type family Split (a :: res) :: forall arg. Maybe (RudeWord res, arg) where Split ((f :: RudeWord res) (a :: k)) = 'Just '(f, a) Split _ = 'Nothing }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913, #14268 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #13913 => #13913, #14268 Comment: I've found a workaround for the original issue in this ticket after much persistence. The trick is to associate `BaseType` with a type class: {{{#!hs class CBaseType (k :: forall a. a ~> Type) (x :: b) where type BaseType k x :: Type }}} Then, define a flexible instance like so, using an explicit `forall` to give `k` the appropriate higher-rank kind: {{{#!hs instance forall b (k :: forall a. a ~> Type) (x :: b). CBaseType k x where type BaseType k x = (@@) k x }}} That's it! Now you can use `BaseType` like you'd expect: {{{ λ> data ProxySym0 :: forall a. a ~> Type λ> type instance ProxySym0 @@ x = Proxy x λ> :kind! BaseType ProxySym0 Bool BaseType ProxySym0 Bool :: * = Proxy Bool λ> :kind! BaseType ProxySym0 Maybe BaseType ProxySym0 Maybe :: * = Proxy Maybe λ> :kind! BaseType ProxySym0 'Just BaseType ProxySym0 'Just :: * = Proxy 'Just }}} It's a bit gnarly, but this is the best that you can do until #14268 is implemented. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913, #14268 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Now that #14268 is implemented, we can work around this issue in a much less hacky way: {{{#!hs type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where forall (k :: forall a. a ~> Type) x. BaseType k x = (@@) k x }}} That being said, the way that I originally thought this type family should have been defined: {{{#!hs type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where BaseType (k :: forall a. a ~> Type) x = (@@) k x }}} Still does not kind-check: {{{ $ ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:22:13: error: • Expected kind ‘forall a. a ~> *’, but ‘k’ has kind ‘a0 ~> *’ • In the first argument of ‘BaseType’, namely ‘(k :: forall a. a ~> Type)’ In the type family declaration for ‘BaseType’ | 22 | BaseType (k :: forall a. a ~> Type) x = (@@) k x | ^ }}} This feels like it ought to Just Work™, though. Should we keep this ticket open until this is possible? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913, #14268 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:23 is a feature request. The use of a type variable in a type family equation -- even on the left-hand side -- is an occurrence, not a binding site. Type families aren't functions! So I think it's OK as is, myself. Someday, we'll just have type-level functions, and then all of this will be better. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11719: Cannot use higher-rank kinds with type families -------------------------------------+------------------------------------- Reporter: ocharles | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.1-rc2 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | dependent/should_compile/T11719 Blocked By: | Blocking: Related Tickets: #13913, #14268 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed Comment: Alright, you've convinced me. In that case, let's close this ticket. (We can always open a new one in the event that we want to accept the program in comment:23). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11719#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC