[GHC] #11324: Missing Kind Inference

[GHC]

#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