#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