Optimizing "counting" GADTs

[Edward Z. Yang]

Excerpts from David Feuer's message of 2016-06-18 19:47:54 -0700:
> I would think the provided equalities could be constructed in a view
> pattern, possibly using unsafeCoerce.

Yes, this does work.

    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE ViewPatterns #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE GADTs #-}
    {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
    module GhostBuster where

    import GHC.TypeLits
    import Unsafe.Coerce

    newtype Vec a (n :: Nat) = Vec { unVec :: [a] }

    -- "Almost" Vec GADT, but the inside is a Vec
    -- (so only the top-level is unfolded.)
    data Vec' a (n :: Nat) where
        VNil'  :: Vec' a 0
        VCons' :: a -> Vec a n -> Vec' a (n + 1)

    upVec :: Vec a n -> Vec' a n
    upVec (Vec [])     = unsafeCoerce VNil'
    upVec (Vec (x:xs)) = unsafeCoerce (VCons' x (Vec xs))

    pattern VNil :: () => (n ~ 0) => Vec a n
    pattern VNil <- (upVec -> VNil') where
        VNil = Vec []

    pattern VCons :: () => ((n + 1) ~ n') => a -> Vec a n -> Vec a n'
    pattern VCons x xs <- (upVec -> VCons' x xs) where
        VCons x (Vec xs) = Vec (x : xs)

    headVec :: Vec a (n + 1) -> a
    headVec (VCons x _) = x

    mapVec :: (a -> b) -> Vec a n -> Vec b n
    mapVec f VNil = (VNil :: Vec a 0)
    mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)

> Dictionaries are harder to come by,
> but reflection might be an option.

If I understand correctly, even if you have a Typeable dictionary you
don't necessarily have a way of constructing the other dictionaries
that are available at that type.  Maybe that is something worth fixing.

Edward