[GHC] #8084: Enabling PolyKinds makes some type errors weird
#8084: Enabling PolyKinds makes some type errors weird -------------------------------------------+------------------------------- Reporter: MartijnVanSteenbergen | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: -------------------------------------------+------------------------------- Consider this program: {{{ {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} module Existential where data Any (f :: k -> *) data X a data Y (a :: *) data Z (a :: Bool) x :: Any X -> () x 'c' = () y :: Any Y -> () y 'c' = () z :: Any Z -> () z 'c' = () }}} x, y and z are all ill-typed, but the shapes of the type errors are different in each case. They are respectively: {{{ Couldn't match expected type `Any k (X k)' with actual type `Char' Couldn't match expected type `Any * Y' with actual type `Char' Couldn't match expected type `Any Bool Z' with actual type `Char' }}} Aren't they supposed to say just 'Any X', 'Any Y' and 'Any Z'? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8084 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8084: Enabling PolyKinds makes some type errors weird --------------------------------------------+------------------------------ Reporter: MartijnVanSteenbergen | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by goldfire): I think the desired behavior here is up for debate. When I first started with `-XPolyKinds`, I thought the messages were strange, too. Now that I use it a lot, I find the explicit kind parameters really helpful (except in type-level lists!). Perhaps the principled approach would be to omit kind applications by default but enable them with a flag like `-fshow- explicit-kind-apps`. Seeing the kind applications also helps to teach the programmer more of what is going on under the hood. Sometimes, it is necessary to be thinking about the implicit kind parameters to make sense of a program, particularly with kind-polymorphic type families. For some examples where the type families only make sense when thinking about explicit kind application, see the discussion for #7939. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8084#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8084: Enabling PolyKinds makes some type errors weird --------------------------------------------+------------------------------ Reporter: MartijnVanSteenbergen | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by simonpj): I'd be interested to know what people think. * Should GHC display kind arguments by default (as now) or only with an explicit flag? One dificulty with the latter is that an explicit flag is not very discoverable. And if kind arguments are not displayed by default you might get messages like `Cannot unify X with X`, which looks like a bug, whereas `Cannot unify (X *) with (X (*->*))` makes more sense. * Should there be syntax to distinguish kind arguments? e.g. `(Any {*} Y)`, or `(Any @* Y)`. There are no major issues of principle here, just ones of design. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8084#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8084: Enabling PolyKinds makes some type errors weird --------------------------------------------+------------------------------ Reporter: MartijnVanSteenbergen | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by kosmikus): I agree that the information is very useful, but generally, I'd like information printed by GHC to be valid Haskell. One way to achieve that would be to print kind arguments as comments: {{{ Any {- * -} Y }}} But it's very noisy. I'm not even sure I like this myself ... Having a flag to enable/disable them definitely seems useful, too. I don't care much about the default. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8084#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8084: Enabling PolyKinds makes some type errors weird --------------------------------------------+------------------------------ Reporter: MartijnVanSteenbergen | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by MartijnVanSteenbergen): Ah, the messages make more sense now. It took me a while to see how to read those types. So, to make sure I understand everything correctly, the kinds are as follows: {{{ Any :: forall k. (k -> *) -> * X :: forall k. k -> * Y :: * -> * Z :: Bool -> * }}} And whenever a kind has a forall in it, GHC shows how it instantiated that kind variable. As for preference, I can imagine that having this information is very valuable, but I think it's confusing to use notation that is indistinguishable from normal type application. So something like `Any {*} Y` would help. I also think it would help if the User's Guide explained that GHC shows this extra information, with Simon's example of when this information is needed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8084#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC