[Haskell] Problem when mixing type classes and type families

Question

Hi! 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

It means that you aren't allowed to use type synomym families when declaring type instances. See section 7.7.2.4 ("Type families and instance declarations") of the GHC manual

The only way you can fix it is to refactor so as to not need it somehow.

Answer 2

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.