[GHC] #11324: Missing Kind Inference
#11324: Missing Kind Inference -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 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: -------------------------------------+------------------------------------- The following example doesn't compile, but I expected it to. {{{ {-# LANGUAGE RankNTypes, ConstraintKinds, ScopedTypeVariables, KindSignatures, PolyKinds, DataKinds, FlexibleInstances, UndecidableInstances, TypeFamilies #-} module Test where data Proxy a data Tagged t s = Tag s type family CharOf fp :: k class Reflects (a :: k) where value :: Proxy a instance Reflects (a :: Bool) type MyConstraint (x :: Bool) = (x~x) foo :: forall fp . (MyConstraint (CharOf fp)) => Tagged fp Int foo= let x = value::Proxy (CharOf fp) in Tag 2 }}} The error in 7.10.2 (unable to test with HEAD) is `Could not deduce (Reflects k (CharOf k fp)) arising from a use of ‘value’`, basically that it was unable to figure out the kind of `CharOf fp`. I think GHC should know the kind from the constraint on `foo`. I've found two workarounds: {{{ foo :: forall fp . (MyConstraint (CharOf fp)) => Tagged fp Int foo= let x = value::Proxy (CharOf fp :: Bin) in Tag 2 }}} and {{{ foo :: forall fp x . (MyConstraint x, x~CharOf fp) => Tagged fp Int foo= let x = value::Proxy x in Tag 2 }}} but both seem unnecessary. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11324 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11324: Missing Kind Inference -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: invalid | 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: | -------------------------------------+------------------------------------- Changes (by rwbarton): * status: new => closed * resolution: => invalid Comment:
I think GHC should know the kind from the constraint on `foo`.
The kind of what? Since `CharOf` is polykinded in its result kind, there could be two different instances {{{ type instance CharOf T = True -- really "type instance CharOf Bool T = True" type instance CharOf T = () -- really "type instance CharOf * T = ()" }}} The occurrence of `CharOf fp` in `MyConstraint (CharOf fp)` must have kind `Bool`, because that is the kind that `MyConstraint` takes. But there is no reason why the subsequent occurrence of `CharOf fp` must have the same kind. This is illustrated by your two working examples. In the first one, `Bin` is not `Bool`! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11324#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11324: Missing Kind Inference -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: invalid | 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 crockeea): Erp, the `Bin` is a typo, it was supposed to be `Bool`. But surely the two type instances you gave conflict? That's what GHC tells me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11324#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11324: Missing Kind Inference -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: invalid | 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 rwbarton): No, they don't conflict, because they have different (non-overlapping) arguments, when the implicit kind parameter of `CharOf` is taken into account. It's easy to think that `type family CharOf fp :: k` means the kind of the result of `CharOf` depends on the type `fp` in some unspecified way. But actually, it means there is a type `CharOf fp` of kind `k` for *every* pair `fp`, `k`. (Much like a function of type, say, `Int -> t` produces any type `t` of the caller's choice, not a type of the function's own choice.) Try this version of your program. {{{ -# LANGUAGE RankNTypes, ConstraintKinds, ScopedTypeVariables, KindSignatures, PolyKinds, DataKinds, FlexibleInstances, UndecidableInstances, TypeFamilies #-} module Test where data Proxy a data Tagged t s = Tag s type family CharOf fp :: k data T type instance CharOf T = True -- really "type instance CharOf Bool T = True" type instance CharOf T = () -- really "type instance CharOf * T = ()" class Reflects (a :: k) where value :: Proxy a instance Reflects (a :: Bool) instance Reflects (a :: *) type MyConstraint (x :: Bool) = (x~x) foo :: forall fp . (MyConstraint (CharOf fp)) => Tagged fp Int foo= let x = value::Proxy (CharOf fp :: *) -- N.B. Not Bool! in Tag 2 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11324#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC