Standalone derived Typeable instance for promoted lists is not found

On GHC 7.10.2, if I try and compile the following short program:

{-# LANGUAGE DataKinds, PolyKinds, DeriveDataTypeable, StandaloneDeriving #-}
module Test where 

import Data.Typeable

deriving instance Typeable '[]
deriving instance Typeable '(:)

nilTyCon  = typeRepTyCon (typeRep (Proxy :: Proxy '[]))
consTyCon = typeRepTyCon (typeRep (Proxy :: Proxy '(:) ))

Then GHC reports the following errors:

Test.hs:9:27:
    No instance for (Typeable '[]) arising from a use of ‘typeRep’
    In the first argument of ‘typeRepTyCon’, namely
      ‘(typeRep (Proxy :: Proxy '[]))’
    In the expression: typeRepTyCon (typeRep (Proxy :: Proxy '[]))
    In an equation for ‘nilTyCon’:
        nilTyCon = typeRepTyCon (typeRep (Proxy :: Proxy '[]))

Test.hs:10:27:
    No instance for (Typeable (':))
      (maybe you haven't applied enough arguments to a function?)
      arising from a use of ‘typeRep’
    In the first argument of ‘typeRepTyCon’, namely
      ‘(typeRep (Proxy :: Proxy (:)))’
    In the expression: typeRepTyCon (typeRep (Proxy :: Proxy (:)))
    In an equation for ‘consTyCon’:
        consTyCon = typeRepTyCon (typeRep (Proxy :: Proxy (:)))

It seems a bug to me that the very instances I asked to be derived (and apparently were without complaint from GHC) are now not found by the typechecker in the very next line.

I think that if the instance cannot be derived, GHC should say so, or if it can, then GHC should find it. I can't really see what's going on with the dump flags, because the typechecker fails before the desugarer runs.

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

Trac metadata

Trac field	Value
Component	Compiler → Compiler (Type checker)

The error is correct, though the error message is bad (especially the second one).

With -fprint-explicit-kinds the error is better:

Test2.hs:10:28:
    No instance for (Typeable [k1] ('[] k1))
      arising from a use of ‘typeRep’
    In the first argument of ‘typeRepTyCon’, namely
      ‘(typeRep (Proxy :: Proxy []))’
    In the expression: typeRepTyCon (typeRep (Proxy :: Proxy []))
    In an equation for ‘nilTyCon’:
        nilTyCon = typeRepTyCon (typeRep (Proxy :: Proxy []))

Test2.hs:11:28:
    No instance for (Typeable (k0 -> [k0] -> [k0]) ((':) k0))
      (maybe you haven't applied enough arguments to a function?)
      arising from a use of ‘typeRep’
    In the first argument of ‘typeRepTyCon’, namely
      ‘(typeRep (Proxy :: Proxy (:)))’
    In the expression: typeRepTyCon (typeRep (Proxy :: Proxy (:)))
    In an equation for ‘consTyCon’:
        consTyCon = typeRepTyCon (typeRep (Proxy :: Proxy (:)))

The type '[] can have any kind [k1], and these must have different Typeable instances. So, the (implicit, and not even mentioned in the original error message) kind variable is really ambiguous. You could choose a particular kind with a signature:

nilStarTyCon  = typeRepTyCon (typeRep (Proxy :: Proxy ('[] :: [*])))

changed milestone to %8.0.1

changed weight to 7

(Written concurrently with ticket:11052#comment:109360)

This is actually expected behavior, but perhaps shouldn't be.

The problem is that, at your call sites of typeRep, GHC doesn't know what kinds you want to specialize '[] and '(:) to. We can't have type representations of poly-kinded things (for various good reasons that would take a bit of academic research to sort out), so compilation fails.

But we sure can improve the error message.

Trac metadata

Trac field	Value
Priority	normal → high

closed

It appears that the error message has been improved. With master as of today the test above produces the following error,

$ inplace/bin/ghc-stage2 hi.hs
[1 of 1] Compiling Test             ( hi.hs, hi.o )

hi.hs:9:27: error:
    No instance for (Typeable '[]) arising from a use of ‘typeRep’
      GHC can't yet do polykinded Typeable ('[] :: [k1])
    In the first argument of ‘typeRepTyCon’, namely
      ‘(typeRep (Proxy :: Proxy '[]))’
    In the expression: typeRepTyCon (typeRep (Proxy :: Proxy '[]))
    In an equation for ‘nilTyCon’:
        nilTyCon = typeRepTyCon (typeRep (Proxy :: Proxy '[]))

hi.hs:10:27: error:
    No instance for (Typeable (':)) arising from a use of ‘typeRep’
      GHC can't yet do polykinded Typeable ((':) :: k0 -> [k0] -> [k0])
    In the first argument of ‘typeRepTyCon’, namely
      ‘(typeRep (Proxy :: Proxy (:)))’
    In the expression: typeRepTyCon (typeRep (Proxy :: Proxy (:)))
    In an equation for ‘consTyCon’:
        consTyCon = typeRepTyCon (typeRep (Proxy :: Proxy (:)))

Given that representation of polykinded types is an open research question it seems that the bug covered by this issue (the error message) has been resolved. Closing.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Phigh label