[GHC] #13909: Can't partially apply a data type with a visible quantifier in its kind
#13909: Can't partially apply a data type with a visible quantifier in its kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck: {{{#!hs {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind data Hm (k :: Type) (a :: k) :: Type class HasName (a :: k) where getName :: proxy a -> String instance HasName Hm where getName _ = "Hm" }}} This is rejected, however: {{{ $ /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/ryanglscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:11:18: error: • Expecting two more arguments to ‘Hm’ Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’ • In the first argument of ‘HasName’, namely ‘Hm’ In the instance declaration for ‘HasName Hm’ | 11 | instance HasName Hm where | ^^ }}} The culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13909 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13909: Can't partially apply a data type with a visible quantifier in its kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Comment (by goldfire): Other than the "expecting two more arguments" part (it should be "one", not "two"), this is correct behavior. What you're trying to do would require impredicative polymorphism in kinds, as you want the kind variable `k` to expand to a type involving a `forall`. We can keep this open as an example of a misphrased error message, but rejection is the correct action until we have impredicativity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13909#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13909: Misleading error message when partially applying a data type with a visible quantifier in its kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13909#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13909: Misleading error message when partially applying a data type with a visible
quantifier in its kind
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords: 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: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#13909: Misleading error message when partially applying a data type with a visible quantifier in its kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T13909 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => typecheck/should_fail/T13909 * status: new => closed * resolution: => fixed * milestone: => 8.4.1 Comment: As noted above, we can't really "fix" this any further without implementing support for impredicative types, so I consider this ticket to be resolved. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13909#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC