Type-level constraints in instances of type families

Question

Is it possible to have type synonym families for parametrized data such as Data.Param.FSVec?

Ideally, I would like this to compile:

class A e where
  type Arg e a
  f :: (Arg e a -> b) -> e a -> e b

instance A X where
  type Arg X a = Nat size => FSVec size a
  f = {- implementation -}

I have tried several workarounds, like wrapping FSVec size a in a newtype, or constraint synonyms, but it seems that I could not get anything reasonable right.

Context + minimal working example

A is a class previously defined (for example) as such:

class OldA e where
  f :: (Maybe a -> b) -> [e (Maybe a)] -> [e b]

An example of type inheriting OldA is:

data Y a = Y a

instance Functor Y where
  fmap f (Y a) = Y (f a)

instance OldA Y where
  f = fmap . fmap

I want to extend this class to be able to express more general function arguments for f. Let's say we have a type X and an associated function fIndependent:

import qualified Data.Param.FSVec as V
import Data.TypeLevel hiding ((==))

data X a = X a deriving Show
fromX (X a) = a

fIndependent :: (Nat size) => (V.FSVec size (Maybe a) -> b) -> [X (Maybe a)] -> [X b]
fIndependent _ [] = []
fIndependent f xs = let x'  = (V.reallyUnsafeVector . take c . fmap fromX) xs
                        xs' = drop c xs
                        c   = V.length x'
                    in if c == length (V.fromVector x') then X (f x') : fIndependent f xs' else []

fIndependent is sane itself. Testing it with a function

test :: V.FSVec D2 x -> Int
test a = V.length a

will grant the result:

>>> fIndependent test $ map (X . Just) [1,2,3,4,5,6,7,8,9]
[X 2, X 2, X 2, X 2]

Ok, now how to extend OldA? The most "natural" thing that came into my mind is to equip class A with a type synonym family Arg e a as below.

class NewA e where
  type Arg e a
  f :: (Arg e a -> b) -> [e (Maybe a)] -> [e b]

Converting all existing instances is easy:

instance NewA Y where
  type Arg Y a = Maybe a
  f = fmap . fmap  -- old implementation

To express fIndependent as f is the difficult part, since just adding

instance NewA X where
  type Arg X a = (Nat size) => FSVec size (Maybe a)  -- wrong!!!
  f = {- same as fIndependent -}

does not work. This is what I have trouble with.

Try-outs

Most solutions I saw propose wrapping FSVec inside a newtype. Doing so does not help since the following code:

{-# LANGUAGE RankNTypes #-}

newtype ArgV a = ArgV (forall rate.Nat rate => V.FSVec rate (Maybe a))

instance NewA X where
  type Arg X a = ArgV a
  g f xs = let x'  = (V.reallyUnsafeVector . take c . fmap fromX) xs
               xs' = drop c xs
               c   = V.length x'
           in if c == length (V.fromVector x') then X (f $ ArgV x') : g f xs' else []

the type inference system seems to lose the information about size:

Couldn't match type ‘s0’ with ‘rate’ …
      because type variable ‘rate’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: Nat rate => V.FSVec rate (Maybe a)
    Expected type: V.FSVec rate (Maybe a)
      Actual type: V.FSVec s0 (Maybe a)
    Relevant bindings include
      x' :: V.FSVec s0 (Maybe a)
        (bound at ...)
    In the first argument of ‘Args’, namely ‘x'’
    In the second argument of ‘($)’, namely ‘Args x'’
Compilation failed.

I would appreciate any lead or hint in this matter.

What are you trying to accomplish? What problem are you trying to solve? What is A if there are "many existing instances of A imported from external libraries which work just fine"? — Cirdec
Sorry for not providing a context, but it's rather knotty. Here is a more elaborated Git issue providing also code snippets. In short: I am trying to include functions with a type signature like f :: (Nat size) => (FSVec size a -> b) -> ... into a class where f's signature is f :: (Value a -> b) -> .... Needless to say, I can modify the code for the class, but it will take too much effort to modify the code for every instance, that is why I prefer type synonyms. I will shortly update the questions as well. — Iedu
It's unclear what you are asking. Please include a complete minimal example, explanations of what the parts of the example are, and the resulting error from the compiler. That's the minimum information for a question to be on topic and useful for other stack overflow users. Without that information a potential answerer can't tell if e.g. X is an attempt to "wrap FSVec size a in a newtype". — Cirdec
@Cirdec : it is done! I doubt that more details such as my attempts and errors could not shed more light into this matter. Moreover, I fear that it would fall into the "debugging help" category (as per the guide you sent), which I desperately wanted to avoid by formulating a general question for a general problem. — Iedu

Cirdec Cirdec · Accepted Answer · 2016-06-30T09:42:31

It appears that you are using a class Nat :: k -> Constraint and a data type FSVec :: k -> * -> *. The data type is constrained with the old DatatypeContexts extension.

{-# LANGUAGE DatatypeContexts #-}

class Nat n

data Nat n => FSVec n a = FSVec -- ...

You have an existing class A :: (* -> *) -> Constraint which you'd like to write an FSVec instance for.

class A e where
  --- ...
  f :: ( {- ... -} b) -> e a -> e b

But FSVec can never have an A instance, because it's a kind mismatch. The class A requires a type argument with the kind * -> * but FSVec has the kind k -> * -> *. You've already run into a problem, and aren't even using the type family yet. If you try to do this (hand waving away what the type family argument is for now)

data X = X

instance A (FSVec) where
  type Arg FSVec a = X
  f = undefined

You get a compiler error.

    Expecting one more argument to `FSVec'
    The first argument of `A' should have kind `* -> *',
      but `FSVec' has kind `* -> * -> *'
    In the instance declaration for `A (FSVec)'

Everything before here, including the compiler error, is useful information for communicating the problem you are having and is useful in asking for help.

Fortunately it's a really easy problem to fix. If you pick some natural number n, then FSVec n has the kind * -> *, which matches the kind of the type argument to A. You can start writing an instance A (FSVec n)

instance A (FSVec n) where
  f = -- ...

When you reintroduce the complete class definition with type families

{-# LANGUAGE TypeFamilies #-}

class A e where
  type Arg e a
  f :: (Arg e a -> b) -> e a -> e b

The solution is still to write an A instance for FSVec n instead of for FSVec. Now that n has moved into the instance declaration, there's an obvious place to capture the needed Nat n context.

instance Nat n => A (FSVec n) where
  type Arg (FSVec n) a = FSVec n a
  f = undefined -- ...

Type-level constraints in instances of type families

Context + minimal working example

Try-outs

2 Answers