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