[GHC] #13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family.
#13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family. -------------------------------------+------------------------------------- Reporter: isovector | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: polykinds, | Operating System: Unknown/Multiple type families | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following program doesn't compile: {{{#!hs {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Test where class Back k class Back (FrontBack k) => Front k where type FrontBack k :: k' instance Back Bool instance Front Int where type FrontBack Int = Bool }}} with the error message: {{{ • No instance for (Back (FrontBack Int)) arising from the superclasses of an instance declaration • In the instance declaration for ‘Front Int’ }}} The example successfully compiles if the kind annotation on FrontBack is removed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13814 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family. -------------------------------------+------------------------------------- Reporter: isovector | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: polykinds, | type families 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: | -------------------------------------+------------------------------------- Description changed by isovector: @@ -10,1 +10,1 @@ - class Back k + class Back t @@ -12,2 +12,2 @@ - class Back (FrontBack k) => Front k where - type FrontBack k :: k' + class Back (FrontBack t) => Front t where + type FrontBack t :: k New description: The following program doesn't compile: {{{#!hs {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Test where class Back t class Back (FrontBack t) => Front t where type FrontBack t :: k instance Back Bool instance Front Int where type FrontBack Int = Bool }}} with the error message: {{{ • No instance for (Back (FrontBack Int)) arising from the superclasses of an instance declaration • In the instance declaration for ‘Front Int’ }}} The example successfully compiles if the kind annotation on FrontBack is removed. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13814#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family. -------------------------------------+------------------------------------- Reporter: isovector | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: polykinds, | type families 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 RyanGlScott): Very strange indeed. If you comment out the `Front Int` instance and inspect the file using GHCi and `-fprint-explicit-kinds`, you'll uncover something odd: {{{ GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Test ( Bug.hs, interpreted ) Ok, modules loaded: Test. λ> :i Back class Back k (t :: k) -- Defined at Bug.hs:7:1 instance [safe] Back * Bool -- Defined at Bug.hs:12:10 λ> :i Front class Back (GHC.Prim.Any *) (FrontBack (GHC.Prim.Any *) k t) => Front k (t :: k) where type family FrontBack k1 k (t :: k) :: k1 -- Defined at Bug.hs:9:1 }}} The definition the `Back` class looks fine. But the definition of `Front` is quite bizarre! I'm not sure how `Any` is being introduced here, since I would have expected it to be this: {{{#!hs class Back k1 (FrontBack k1 k t) => Front k (t :: k) where type family FrontBack k1 k (t :: k) :: k1 }}} I suppose this also explains the confusing error message. If you try compiling the `Front Int` error message with `-fprint-explicit-kinds`, you'll see that: {{{ • No instance for (Back (GHC.Prim.Any *) (FrontBack (GHC.Prim.Any *) * Int)) arising from the superclasses of an instance declaration • In the instance declaration for ‘Front * Int’ }}} No wonder it's failing - we have an instance for `Back * (FrontBack * * Int)`, not for `Back (Any *) (FrontBack (Any *) * Int)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13814#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family. -------------------------------------+------------------------------------- Reporter: isovector | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: polykinds, | type families 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 simonpj): You say you expected {{{ class Back k1 (FrontBack k1 k t) => Front k (t :: k) where ... }}} But this is jolly odd, becuase the constraint mentions `k1`, which is not bound in the bit after the `=>`. Would you expect this to be OK? {{{ class C a b => D a where op1 :: a -> Int -> a }}} Well no! Think of the data type declaration that arises from class decl: {{{ data D a where MkD :: C a b => (a->Int->a) -> D a }}} That `b` can only be existential, which isn't at all what we want. So perhaps we want this {{{ class Back k1 (FrontBack k1 k t) => Front k k1 (t :: k) where ... }}} That makes more sense. (What is instead happening today is that the `k1` is being defaulted to `Any`.) But that too is problematic. Suppose there was a class-op: {{{ class Back k1 (FrontBack k1 k t) => Front k k1 (t :: k) where type family FrontBack k (t :: k) :: k1 op :: Proxy k t -> Int }}} Now the type of `op` is rather ambiguous {{{ op :: forall k k1 (t::k). Front k k1 t => Proxy k t -> Int }}} So nothing fixes `k1, so it'll be difficult to discharge the `Front` contraint from any givens. So simply addind kind variables from the superclass constraints isn't going to work. But defaulting them isn't very good either. Maybe we should complain about the unresolved kind variables in the class decl? The real problem is that `Back` is too polymorphic. If it had kind `k -> k` we'd probably be fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13814#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13814: Unable to resolve instance for polykinded superclass constraint on associated-type-family. -------------------------------------+------------------------------------- Reporter: isovector | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: polykinds, | type families 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 RyanGlScott): Replying to [comment:3 simonpj]:
The real problem is that `Back` is too polymorphic. If it had kind `k -> k` we'd probably be fine.
Ah, you're right. This program //does// typecheck, as expected: {{{#!hs {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Test where class Back t class Back (FrontBack t) => Front t where type FrontBack (t :: k) :: k instance Back Bool instance Front Int where type FrontBack Int = Bool }}}
Maybe we should complain about the unresolved kind variables in the class decl?
That sounds like a good approach, yes. The error message might be confusing since it mentions an inferred kind variable, but I'd argue that that error would be far clearer than the current one, which is rather enigmatic. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13814#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC