[GHC] #13913: Can't apply higher-ranked kind in type family
#13913: Can't apply higher-ranked kind in type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This code doesn't typecheck due to `F2`: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind f :: (forall (a :: Type). a -> a) -> Bool f g = g True type F1 (g :: forall (a :: Type). a -> a) = g True type family F2 (g :: forall (a :: Type). a -> a) :: Bool where F2 g = g True }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:14:6: error: • Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’ • In the first argument of ‘F2’, namely ‘g’ In the type family declaration for ‘F2’ | 14 | F2 g = g True | ^ }}} This is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13913 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13913: Can't apply higher-ranked kind in type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I believe this is a dup of #11719. My recent [https://github.com/ghc- proposals/ghc-proposals/pull/55 proposal] around adding explicit `forall`s to type family equations will introduce a workaround. Perhaps a simple case like this, though, could be made to work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13913#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13913: Can't apply higher-ranked kind in type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11719 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate * related: => #11719 Comment: Oops, I didn't see that ticket! Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13913#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13913: Can't apply higher-ranked kind in type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11719 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I've found a workaround for this issue after much persistence. The trick is to associate `F2` with a type class: {{{#!hs class C (g :: forall a. a -> a) where type F2 g :: Bool }}} Then, define a flexible instance like so, using an explicit `forall` to give `g` the appropriate higher-rank kind: {{{#!hs instance forall (g :: forall a. a -> a). C g where type F2 g = g True }}} That's it! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13913#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13913: Can't apply higher-ranked kind in type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeFamilies, Resolution: duplicate | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11719 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeFamilies, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13913#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC