packaged up polykinded types can't index type families?
Nicolas Frisby
nicolas.frisby at gmail.com
Tue Mar 13 20:17:56 CET 2012
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/3bf54e78cfd4b94756e3f21c00ae187f80c3341d
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
More information about the Glasgow-haskell-users
mailing list