Opened 17 months ago
Closed 17 months ago
#9144 closed bug (fixed)
Incorrect error reported with poly-kinded type families
Reported by: | goldfire | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.8.2 |
Keywords: | Cc: | ||
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | polykinds/T9144 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by goldfire)
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.
Change History (4)
comment:1 Changed 17 months ago by goldfire
- Description modified (diff)
comment:2 Changed 17 months ago by simonpj
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
comment:3 Changed 17 months ago by Simon Peyton Jones <simonpj@…>
comment:4 Changed 17 months ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to polykinds/T9144
Note: See
TracTickets for help on using
tickets.
Corrected typo in initial report (FooTerm --> BarTerm in a critical spot).