Referring to a type variable in the result of a type family


{-# LANGUAGE TypeFamilies #-}

type family TF1 a

data T1 a
data T2 a

class C a where
  type TF2 a

instance (TF1 a ~ T1 b) => C (T2 a) where
  type TF2 (T2 a) = b

Compilation fails with the error:

• Type variable ‘b’ is mentioned in the RHS,
    but not bound on the LHS of the family instance
• In the type instance declaration for ‘TF2’
  In the instance declaration for ‘C (T2 a)’

type TF2 (T2 a) = TF1 a compiles, evaluating to T1 b, but I want just b.

How do acheive what I am trying to do - get a type variable from the result of a type family application? It would seem that I would need some form of ‘type-level pattern match’.

You can do this kind of type level pattern matching with closed type families (this requires UndecidableInstances):

type family TF3 a where
  TF3 (T1 a) = a

instance (TF1 a ~ T1 b) => C (T2 a) where
  type TF2 (T2 a) = TF3 (TF1 a)

type instance TF1 Bool = T1 Int

x :: TF2 (T2 Bool) -- Int
x = 10

But I don’t think it looks very elegant in this example.

I guess it would be more straightforward to use MultiParamTypeClasses. I came to Haskell after TypeFamilies, and never felt the need to get my head around functional dependencies, but here goes…

My bad - I think this would work without fundeps. I still prefer the elegance of type families, but not today.