Opened 3 years ago

Closed 3 years 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)

    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)

    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 3 years ago by goldfire

Description: modified (diff)

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

comment:2 Changed 3 years 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


comment:3 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

comment:4 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T9144
Note: See TracTickets for help on using tickets.