Problem when mixing type classes and type families

Question

This code compiles fine:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
  UndecidableInstances, FlexibleContexts, EmptyDataDecls, ScopedTypeVariables,
  TypeOperators, TypeSynonymInstances, TypeFamilies #-}
class Sel a s b where
  type Res a s b :: *

instance Sel a s b where
  type Res a s b = (s -> (b,s))

instance Sel a s (b->(c,a)) where
  type Res a s (b->(c,a)) = (b -> s -> (c,s))

but as soon as I add the R predicate ghc fails:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
  UndecidableInstances, FlexibleContexts, EmptyDataDecls, ScopedTypeVariables,
  TypeOperators, TypeSynonymInstances, TypeFamilies #-}
class Sel a s b where
  type Res a s b :: *

instance Sel a s b where
  type Res a s b = (s -> (b,s))

class R a where
  type Rec a :: *
  cons :: a -> Rec a
  elim :: Rec a -> a
instance Sel a s (b->(c,Rec a)) where
  type Res a s (b->(c,Rec a)) = (b -> s -> (c,s))

complaining that:

    Illegal type synonym family application in instance:
        b -> (c, Rec a)
    In the instance declaration for `Sel a s (b -> (c, Rec a))'

what does it mean and (most importantly) how do I fix it?

Thanks

Answer 1

Type families are one-way: you can expand Rec a to its computed type, but you cannot (uniquely) go from the expansion back to Rec a. This makes applications of type functions unsuitable for instance signatures, as they can never trigger the instance to apply.

You could try instead:

instance Rec a ~ reca => Sel a s (b->(c,reca))

This means something else: it says any function b -> (c, reca) is an instance, and then when it has irrevocably matched, the compiler checks that Rec a ~ reca. But this might be good enough to do want in your case.

Answer 2

Rec is not a type constructor; it's a type function. Maybe you can use it only in the type of a value of type definition, not in a class declaration? I'm guessing wildly here; I don't understand all the rules for type families.

I don't know how to fix it, but some things to try include:

• Get rid of class Sel and just define type family Res a s b :: *. Use type instance instead of the class mechanism.

• It's barely possible that making type Rec injective using data will help, but I don't think so.

• Cut back to the smallest number of language extensions that could possibly work—it will make it easier for others to help you, and it might help the compiler as well.