Incorrect error reported with poly-kinded type families

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.

changed weight to 5

added Tbug Trac import labels

changed the description

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

Happily, I believe that this works on the 7.8 branch, and HEAD, and hence is already fixed. I don't know what the fix was! Still pending: add the test case to HEAD

Simon

mentioned in commit 2745dfb5

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	→ polykinds/T9144

added Pnormal label