Problems with polymorphic kinds imported from module
There seems to be a problem when importing polymorphic kinds from a module in a cabalized package. One way to spot the problem is to cabal install singletons
, import Singletons.Lib
and run :t SNil
in ghci. ghci reports a stack overflow. Another way to access (what I think is) the same error is to compile the following:
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators,
GADTs, RankNTypes #-}
import Singletons.Lib
type family Map (f :: k1 -> k2) (a :: [k1]) :: [k2]
type instance Map f '[] = '[]
type instance Map f (h ': t) = (f h) ': (Map f t)
sMap :: forall (f :: k1 -> k2) (b :: [k1]).
(forall a. Sing a -> Sing (f a)) -> Sing b -> Sing (Map f b)
sMap _ SNil = SNil
sMap f (SCons h t) = SCons (f h) (sMap f t)
The error message is
Couldn't match kind `BOX' against `[k1]'
Kind incompatibility when matching types:
k1 :: BOX
b :: [k1]
In the pattern: SNil
In an equation for `sMap': sMap _ SNil = SNil
Neither of these problems surface when checking the type of SNil
or compiling the above code when the singletons sources are at hand and are interpreted.
I tried to make a small test case for this but was unable to reproduce the error after a number of attempts, including using Template Haskell to generate the Sing
instance for type-level lists, as is done in the singletons library.
This was all tested on 7.5.20120620. There's a good chance this bug is related to #7022 (closed).
Trac metadata
Trac field | Value |
---|---|
Version | 7.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |