I've got a type family defined as follows:
type family Vec a (n :: Nat) where
Vec a Z = a
Vec a (S n) = (a, Vec a n)
I'd like to assert that the result of applying this type family always fulfills the SymVal class constraint from the SBV package:
forall a . (SymVal a) => SymVal (Vec a n)
There is SymVal
instances a,b
, so whenever SymVal a
holds, then SymVal (Vec a n)
should hold, for any value of n
. How can I ensure GHC sees that SymVal
is always implemented for the result of the type family application?
However, I don't know how to express this. Do I write an instance? A deriving clause? I'm not creating a new type, simply mapping numbers to existing ones.
Or am I totally on the wrong track? Should I be using a data family, or functional dependencies?
I don't know the precise context in which you require these
SymVal (Vec a n)
instances, but generally speaking if you have a piece of code that requires the instanceSymVal (Vec a n)
then you should add it as a context:When
foo
is called with a specificn
, the constraint solver will reduce the type family application and use the instancesAt the end of that process, the constraint solver will want an instance for
SymVal a
. So you'll be able to callfoo
:n
, allowing the type family applications to fully reduce, and use a typea
which has an instance forSymVal
:GHC can't automatically deduce
SymVal (Vec a n)
fromSymVal a
, because without further context it cannot reduce the type family application, and thus doesn't know which instance to choose. If you want GHC to be able to perform this deduction, you would have to passn
explicitly as an argument. This can be emulated with singletons :(Note that these obnoxious case statements would be eliminated with type applications in patterns, mais c'est la vie.)
You can then use this function to allow GHC to deduce a
SymVal (Vec a n)
constraint from aSymVal a
constraint, as long as you are able to provide a singleton forn
(which amounts to passingn
explicitly as opposed to being parametric over it):