Suppose that we want to define an instance of `Functor`

for vectors, whose type is tracked in the type system. Just making a direct recursive definition is straight-forward, but we'd like to define the instance in such a way that GHC will unroll the loop when performing dictionary specialization.

We may start with a definition that looks something like this:

```
instance Functor (Vec 0) where ...
instance Functor (Vec (n + 1)) where ...
```

Unfortunately, in GHC type-families may not appear in the "head" of a class instance, and (+) is just a type family.

In general, this make sense because such instances do not always make sense. Consider, for example, the following code:

```
class C a where
f :: a -> String
type family F a
type instance F Int = Char
type instance F Bool = Char
-- bad instance
instance C (F a)
```

Now, if GHC encounters a constraint `C Char`

, there is no way to know if `a`

should be `Int`

or `Bool`

. One could make the case that such instances should be allowed as long as `F`

is injective, but no one has implemented that yet.

One possible work-around is to change:

`instance C (F a)`

into

`instance (F a ~ b) => C b`

This is a valid instance, but one has to be careful, as GHC consults only the instance "head" (i.e., the predicate on the RHS of the fat arrow) when selecting instances, and the context is ignored. Since in this case the instance "head" is just a variable, we have end up with a very general instance.

The rest of the file has two solutions. The first one, which is more natural, requires the use of a type-checker plugin, which can be enabled with the following flag (if installed):

`{-# OPTIONS_GHC -fplugin=TypeNatSolver #-} -- use plugin`

```
{-# LANGUAGE GADTs #-}
-- To define the type `Vec`
```

```
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
-- For working with type level literals
```

```
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
-- For defining "exotic" instances
```

```
module VecFuntorInstance where
import GHC.TypeLits
import Data.Proxy
```

We start by defining the type of vectors of a fixed length.

```
data Vec (n::Nat) a where
Nil :: Vec 0 a
Cons :: a -> Vec n a -> Vec (n+1) a
-- | Convert a vector to a list; useful for debugging.
toList :: Vec n a -> [a]
toList vec =
case vec of
Nil -> []
Cons x xs -> x : toList xs
instance Show a => Show (Vec n a) where
showsPrec p = showsPrec p . toList
```

We illustrate the basic idea by defining an overloaded function that generates a constant vector of a given length, by consulting the type of the vector.

```
class ConstVec n where
constVec :: a -> Vec n a
```

The base case instance is nothing special:

```
instance ConstVec 0 where
constVec _ = Nil
```

The interesting case arises when we define the inductive step:

```
instance {-# OVERLAPS #-}
(ConstVec prev, (prev + 1) ~ n) => ConstVec n
where
constVec a = Cons a (constVec a)
```

Note that, as discussed before, We moved the type-function to the instance's context and, also, we added the `OVERLAPS`

pragma. This pragma tells GHC that we are defining an instance that overlaps another one, and so before committing to the more general one, it should make sure that the more specific one is guaranteed to not work.

Here is an example of this at work:

```
make5 :: Char -> Vec 5 Char
make5 = constVec
```

```
*Test> make5 'b'
"bbbbb"
```

If we look at the generated Core for `make5`

after compiling with optimizations, we see that GHC has fully unrolled all the loops:

```
make5
make5 = ($sconstVec2) `cast` ...
$sconstVec2
$sconstVec2 =
\ @ a_X2et a1_X1Vj ->
Cons
@~ <4 + 1>_N
a1_X1Vj
((Cons
@~ <3 + 1>_N
a1_X1Vj
((Cons
@~ <2 + 1>_N
a1_X1Vj
((Cons
@~ <1 + 1>_N
a1_X1Vj
((Cons @~ <0 + 1>_N a1_X1Vj ($WNil)) `cast` ...))
`cast` ...))
`cast` ...))
`cast` ...)
```

To define an instance of the `Functor`

class we use the same pattern:

```
class MapVec (n :: Nat) where
mapVec :: proxy n -> (a -> b) -> Vec n a -> Vec n b
instance MapVec 0 where
mapVec _ _ _ = Nil
```

```
-- Only works with plugin
instance {-# OVERLAPS #-} (MapVec prev, (prev + 1) ~ n) => MapVec n where
mapVec p f (Cons x xs) = Cons (f x) (mapVec (prev p) f xs)
where prev :: proxy (a + 1) -> Proxy a
prev _ = Proxy
```

```
instance MapVec n => Functor (Vec n) where
fmap = mapVec Proxy
```

Unfortunately the inductive instance is rejected by vanilla GHC 7.10 because it has very little knowledge about how numbers work---the only thing GHC knows is how to evaluate functions on numbers (e.g., it knows that 7 + 3 is 10). However, for this instance to be accepted we need to know about cancellation, in particular that if `(x + 1) ~ (y + 1)`

, then it must be the case that `x ~ y`

.

This, and other facts about numbers, are implemented as a separate GHC plug-in, available from:

`https://github.com/yav/type-nat-solver`

To use the plugin one needs to invoke GHC with the `-fplugin=TypeNatSolver`

(or add it as an `OPTION`

pragma at the top of the file). The plug-in uses the `z3`

(or another) SMT-solver to solve many of the linear numeric constraints arising from type-checking numbers.

The simple solver built into GHC works only in simple cases (generally, if one uses GADTs, it is very likely that the advanced solver would be needed). However, in this case we can get a working implementation by reformulating the definition of the GADT as follows:

```
data Vec' (n::Nat) a where
Nil' :: Vec' 0 a
Cons' :: a -> Vec' (n - 1) a -> Vec' n a
-- | Convert a vector to a list; useful for debugging.
toList' :: Vec' n a -> [a]
toList' vec =
case vec of
Nil' -> []
Cons' x xs -> x : toList' xs
instance Show a => Show (Vec' n a) where
showsPrec p = showsPrec p . toList'
```

```
class ConstVec' n where
constVec' :: a -> Vec' n a
instance ConstVec' 0 where
constVec' _ = Nil'
instance {-# OVERLAPS #-} (ConstVec' (n-1)) => ConstVec' n where
constVec' a = Cons' a (constVec' a)
```

```
make5' :: a -> Vec' 5 a
make5' = constVec'
```

```
class MapVec' (n :: Nat) where
mapVec' :: proxy n -> (a -> b) -> Vec' n a -> Vec' n b
instance MapVec' 0 where
mapVec' _ _ _ = Nil'
```

```
instance {-# OVERLAPS #-} (MapVec' (n-1)) => MapVec' n where
mapVec' p f (Cons' x xs) = Cons' (f x) (mapVec' (prev p) f xs)
where prev :: proxy a -> Proxy (a - 1)
prev _ = Proxy
```

```
instance MapVec' n => Functor (Vec' n) where
fmap = mapVec' Proxy
```