#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

#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: -------------------------------------+------------------------------------ Comment (by Simon Peyton Jones ): In [changeset:"2745dfb56414269ea53e75136166a5ed0452b2af/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="2745dfb56414269ea53e75136166a5ed0452b2af" Test Trac #9144 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9144#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler