[GHC] #9144: Incorrect error reported with poly-kinded type families

[GHC]

#9144: Incorrect error reported with poly-kinded type families
------------------------------------+-------------------------------------
       Reporter:  goldfire          |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.8.2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 When I compile

 {{{
 {-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, RankNTypes #-}

 module Bug where

 import Data.Proxy
 import GHC.TypeLits

 data family Sing (a :: k)

 data SomeSing :: KProxy k -> * where
   SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)

 class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where
   fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k)
   toSing :: DemoteRep ('KProxy :: KProxy k) -> SomeSing ('KProxy :: KProxy
 k)

 type family DemoteRep (kproxy :: KProxy k) :: *

 data Foo = Bar Nat
 data FooTerm = BarTerm Integer

 data instance Sing (x :: Foo) where
   SBar :: Sing n -> Sing (Bar n)

 type instance DemoteRep ('KProxy :: KProxy Nat) = Integer
 type instance DemoteRep ('KProxy :: KProxy Foo) = FooTerm

 instance SingKind ('KProxy :: KProxy Nat) where
   fromSing = undefined
   toSing = undefined

 instance SingKind ('KProxy :: KProxy Foo) where
   fromSing (SBar n) = BarTerm (fromSing n)
   toSing n = case toSing n of SomeSing n' -> SomeSing (SBar n')
 }}}

 I get (with `-fprint-explicit-kinds`)

 {{{
 /Users/rae/temp/Bug.hs:33:32:
     Couldn't match type ‘FooTerm’ with ‘Integer’
     Expected type: Integer
       Actual type: DemoteRep Nat ('KProxy Nat)
     In the first argument of ‘BarTerm’, namely ‘(fromSing n)’
     In the expression: BarTerm (fromSing n)

 /Users/rae/temp/Bug.hs:34:26:
     Couldn't match type ‘Integer’ with ‘FooTerm’
     Expected type: DemoteRep Nat ('KProxy Nat)
       Actual type: DemoteRep Foo ('KProxy Foo)
     In the first argument of ‘toSing’, namely ‘n’
     In the expression: toSing n
 }}}

 The second error reported is correct -- the last line in the code should
 start `toSing (FooTerm n) = ...` to fix the code. However, the first error
 reported is bogus, given that `DemoteRep ('KProxy :: KProxy Nat)` is
 clearly `Integer`.

 I tried to simplify the test case with no luck -- sorry.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9144>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler