packaged up polykinded types can't index type families?

[Simon Peyton-Jones]

I'm afraid that PolyKinds is not an advertised feature of 7.4.1, and we won't fix bugs in it.  The flag exists because we were working on it before releasing 7.4, but it was too far from completion to support.  We knew there were many bugs, but did not want to hold up 7.4 for them.  (Otherwise we'd never make a release!)  

Bug reports are very valuable though, so keep them coming.  Nicolas, happily your program works just fine with HEAD.  (If you don't want to compile from source, grab a binary snapshot.)

PolyKinds *will* be a feature in 7.6, and I believe that they are fully working right now.  So beat on HEAD!

Simon

|  -----Original Message-----
|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Nicolas Frisby
|  Sent: 13 March 2012 19:18
|  To: glasgow-haskell-users
|  Subject: packaged up polykinded types can't index type families?
|  
|  I suspect I'm tripping on a gap in the PolyKinds support. I'm trying
|  to package up a type-level generic view. It uses PolyKinds - and
|  DataKinds, but I think it's the PolyKinds that matter. If I compile
|  everything locally in the same build, it works fine. If I isolate the
|  spine view declarations in their own package, I get type errors.
|  
|  A quick search turned up this omnibus, which I'm guessing might fix my problem.
|  
|  
|  http://hackage.haskell.org/trac/ghc/changeset/3bf54e78cfd4b94756e3f21c00ae1
|  87f80c3341d
|  
|  I was hoping someone might be able to identify if that's the case. I
|  can wait for 7.6.1 if I must, but I was wondering if there's a
|  workaround.
|  
|  (If I avoid PolyKinds, it works. But I have to simulate PolyKinds for
|  a finite set of kinds, which is pretty obfuscating and not general. If
|  you're curious, checkout the type-spine package. This whole email
|  regards my trying to generalize and simplify that package with
|  PolyKinds.)
|  
|  In a distillation of my use case, we have two modules. The first is
|  the type-level spine view.
|  
|  > {-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators,
|  >   UndecidableInstances, TemplateHaskell, EmptyDataDecls #-}
|  > module Spine where
|  >
|  > type family Spine a :: *
|  >
|  > data Atom n -- represents a totally unapplied type name
|  > data f :@ a -- |represents a type-level application
|  >
|  > -- this is an "unsaturated instance", which might be a no-no, but
|  > -- at least isn't obviously causing the current problem
|  > type instance Spine (f a) = f :@ a
|  >
|  > -- all other instances are for unapplied types names:
|  > -----  e.g.   type instance Spine N = Atom N
|  > spineType :: Name -> Q [Dec]
|  > spineType n = let t = conT n in
|  >   (:[]) `fmap` tySynInstD ''Spine [t] [t| Atom $t |]
|  
|  The second module is a distilled use case.
|  
|  > {-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators,
|  TemplateHaskell #-}
|  >
|  > module Test where
|  >
|  > import Spine -- our first module above
|  >
|  > type family IsApp (a :: *) :: Bool
|  > type instance IsApp (Atom n) = False
|  > type instance IsApp (a :@ b) = True
|  >
|  > -- example types and use
|  > data A = A
|  > data F a = F a
|  >
|  > concat `fmap` mapM spineType [''A, ''F]
|  >
|  > isApp :: (True ~ IsApp (Spine a)) => a -> ()
|  > isApp _ = ()
|  >
|  > test :: ()
|  > test = isApp (F A)
|  
|  If Spine.hs and Test.hs are in the same directory and I load Test in
|  ghci, it type-checks fine. If I instead use cabal to install Spine as
|  its own package, the subsequent type-checking of Test.test fails with:
|  
|  > Couldn't match type `IsApp ((:@) (* -> *) * F A)' with `'True'
|  
|  The :bro Spine command returns the same information regardless of how
|  Test imports Spine.
|  
|  > *Test> :bro Spine
|  > type family Spine k a :: *
|  > data Atom k n
|  > data (:@) k k f a
|  > spineType :: ...snip...
|  
|  Why can "IsApp (... :@ ...)" reduce if Spine was locally compiled but
|  not if it's pulled from a package? Is there some crucial info that the
|  package interfaces can't yet express? Is there an open bug for this?
|  
|  Thanks for your time,
|  Nick
|  
|  _______________________________________________
|  Glasgow-haskell-users mailing list
|  Glasgow-haskell-users at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users