GitLab

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