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