[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
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Old description:

> 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.

New description:

 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 (BarTerm 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.

--

Comment (by goldfire):

 Corrected typo in initial report (`FooTerm` --> `BarTerm` in a critical
 spot).

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