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,,,