id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
6035	Kind-indexed type family failure with polymorphic kinds	goldfire		"The following code fails to compile:

{{{
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators
 #-}

data Nat = Zero | Succ Nat

type family Sing (a :: k) :: k -> *

data SNat n where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

data SList (a :: [k]) where
  SNil :: SList '[]
  SCons :: Sing h h -> SList t -> SList (h ': t)

type instance Sing (a :: Nat) = SNat
type instance Sing (a :: [k]) = SList

term :: SList '[ '[Zero], '[]]
term = SCons (SCons SZero SNil) (SCons SNil SNil)
}}}

The error generated is

{{{

/Users/rae/temp/Scratch.hs:27:15:
    Couldn't match type `Sing [Nat] ((':) Nat 'Zero ('[] Nat))'
                  with `SList Nat'
    Expected type: Sing
                     [Nat] ((':) Nat 'Zero ('[] Nat)) ((':) Nat 'Zero ('[] Nat))
      Actual type: SList Nat ((':) Nat 'Zero ('[] Nat))
    In the return type of a call of `SCons'
    In the first argument of `SCons', namely `(SCons SZero SNil)'
    In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)

/Users/rae/temp/Scratch.hs:27:40:
    Couldn't match type `Sing [Nat] ('[] Nat)' with `SList Nat'
    Expected type: Sing [Nat] ('[] Nat) ('[] Nat)
      Actual type: SList Nat ('[] Nat)
    In the first argument of `SCons', namely `SNil'
    In the second argument of `SCons', namely `(SCons SNil SNil)'
    In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)
}}}

It seems that the {{{Sing}}} kind-indexed type family isn't quite working. My guess is that the problem is that we really want, say, {{{Sing '[Zero]}}} to be {{{SList Nat}}}, where {{{Nat}}} is the implicit kind parameter to {{{SList}}}. But, we can't say that. I would hope that the explicit kind annotation on the result of {{{Sing}}} would fix the implicit kind parameter to {{{SList}}}, but it doesn't seem to.

This was tested on 7.5.20120420."	bug	closed	normal		Compiler (Type checker)	7.5	fixed	PolyKinds TypeFamilies	pho@…	Unknown/Multiple	Unknown/Multiple	None/Unknown	Unknown	polykinds/T6035