Edward Z. Yang ezyang at mit.edu
Sun Jun 19 03:21:24 UTC 2016

```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 #-}
{-# 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
```