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/3bf54e78cfd4b94756e3f21c00ae18... 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