Why is Int not promotable?

Question

I'd like to have points in two or three dimensions such that the two-dimensional points and the three-dimensional points can share code, but the compiler can tell them apart. Here's a first attempt.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Dimension = D2 | D3
data Point :: Dimension -> * where
  Point :: Dimension -> [Int] -> Point d
origin = Point D2 [0, 0]

That works OK so far. Here's a simplified version:

data Point' :: Int -> * where
  Point' :: Int -> [Int] -> Point' d
origin' = Point' 2 [0, 0]

This does not compile: ‘Int’ of kind ‘*’ is not promotable. The documentation on datatype promotion for GHC 7.10.3 lists various reasons that a type might not be promotable (for example, if it already involves promoted types), but I don't see why they would exclude Int.

(1) Why is it giving this error?

And as a bonus,

(2) Is there a reasonable fix or alternate approach? A search shows, for example, Fixed-Length Vector Types in Haskell, but that seems overcomplicated.

Answer 1

Int is promotable in principle, but the implementation work hasn't (yet?) been done. They are implemented at the term level as hardware words, with primitive operations implemented as C or assembly routines; each such operation one would want to use at the type level (including "convert this compile-time constant to an Int"!) would need to be promoted by hand, and as far as I know this hasn't been done.

Use a standard algebraic definition of numbers -- e.g. Peano nats or lists of bits -- instead, as algebraic types can be promoted with the existing implementation. Although I haven't done enough to have a recommendation for a specific one, there should be several implementations of these available on Hackage somewhere.