[GHC] #14147: Confusing error messages with PolyKinds and superclasses
#14147: Confusing error messages with PolyKinds and superclasses -------------------------------------+------------------------------------- Reporter: enolan | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 program compiles fine: {{{#!hs {-# LANGUAGE FlexibleInstances #-} import Data.Typeable newtype Tagged t v = Tagged v deriving Typeable class (Typeable t) => MyClass t where classF :: t -> Int instance Typeable t => MyClass (Tagged t Int) where classF (Tagged n) = n }}} But if I add `PolyKinds` to the `LANGUAGE` pragma I get: {{{ code/junk/typeable-problems.hs:17:10: error: • Could not deduce (Typeable k) arising from the superclasses of an instance declaration from the context: Typeable t bound by the instance declaration at code/junk/typeable-problems.hs:17:10-45 • In the instance declaration for ‘MyClass (Tagged t Int)’ | 17 | instance Typeable t => MyClass (Tagged t Int) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} Which is very confusing since I don't have a `k` variable anywhere. Adding `-fprint-explicit-kinds` is somewhat better: {{{ code/junk/typeable-problems.hs:17:10: error: • Could not deduce (Typeable * k) arising from the superclasses of an instance declaration from the context: Typeable k t bound by the instance declaration at code/junk/typeable-problems.hs:17:10-45 • In the instance declaration for ‘MyClass (Tagged k t Int)’ | 17 | instance Typeable t => MyClass (Tagged t Int) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} But still confusing. It doesn't really point me towards the solution - specifying that the kind of t is `*` explicitly - if I don't already know how the extension works. It's also annoying that turning on an extension causes a type error, but I don't know if that's fixable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14147 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14147: Confusing error messages with PolyKinds and superclasses -------------------------------------+------------------------------------- Reporter: enolan | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 RyanGlScott): So here is what's going on. Nowadays, every datatype automatically has a `Typeable` instance emitted (so `deriving Typeable` is redundant). A datatype is `Typeable` only if all of its type parameters are also `Typeable`. So //without// `PolyKinds` enabled, the emitted `Typeable` instance for `Tagged` is: {{{#!hs instance (Typeable t, Typeable v) => Typeable (Tagged t v) }}} So far, so good. Now what happens when you turn on `PolyKinds`? By default, `PolyKinds` generalizes the kind of every type variable to the fullest extent it can. Notice that in the definition of `Tagged`: {{{#!hs newtype Tagged t v = Tagged v }}} Here, `v` is used as a field, so its kind must be `*`. But `t` is completely unconstrained, so its kind is generalized to `k`, a kind variable. Now, you claimed that "don't have a `k` variable anywhere". But that's not true—`Tagged` //does// have a `k` parameter, except that it's invisible (as opposed to `t` and `v`, which are visible). If you enable `-fprint- explicit-foralls`, it's much easier to see this in action: {{{ λ> :set -XPolyKinds λ> newtype Tagged t v = Tagged v λ> :set -fprint-explicit-foralls λ> :type +v Tagged Tagged :: forall {k} (t :: k) v. v -> Tagged t v }}} With this in mind, let's revisit the `Typeable` instance for `Tagged`. Recall that a datatype is `Typeable` only if all of its type parameters are also `Typeable`. Therefore, with `PolyKinds` enabled, the emitted `Typeable` instance is: {{{#!hs instance (Typeable k, Typeable t, Typeable v) => Typeable (Tagged (t :: k) v) }}} Hopefully now it will become clear why you experienced that `Could not deduce (Typeable k)` error message: you had written this instance: {{{#!hs instance Typeable t => MyClass (Tagged t Int) }}} Because `Typeable` is a superclass of `MyClass`, there needs to be a `Typeable (Tagged (t :: k) Int)` instance in scope for this to typecheck. But the only constraint on this instance is `Typeable t`—we don't know that `k` is also `Typeable`! Therefore, fixing this is a matter of adding an extra constraint: {{{#!hs instance (Typeable k, Typeable t) => MyClass (Tagged (t :: k) Int) }}} (This requires the `TypeInType` language extension, which is essentially a beefed up version of `PolyKinds`.) So to recap, I'd argue that there's no bug here, just a tricky interaction between the `Typeable` solver and language extensions. Enabling `PolyKinds` (and thus generalizing kinds) is certainly not guaranteed to keep your existing code compiling! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14147#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14147: Confusing error messages with PolyKinds and superclasses -------------------------------------+------------------------------------- Reporter: enolan | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 enolan): OK, I'm willing to accept that code that compiles without `PolyKinds` shouldn't necessarily compile with it turned on. I still think this is a bad error message though. Yes, `k` is a variable that exists, but it's not one I wrote. From the user's perspective this message is very unhelpful. Perhaps something along these lines could be appended to the message when an error like this is emmited: "where k is an inferred kind parameter in Tagged's kind: `forall {k}. k -> * -> *`". Then I'd know where `k` comes from and can figure out that I can add a `Typeable` constraint for it or fix it at `*`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14147#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC