Type-threaded heterogenous lists and defaulting(?) with type families?

Question

I'm working on a library where I want to define a recursive class that I've simplified here to:

{-# LANGUAGE MultiParamTypeClasses 
           , FlexibleInstances #-}

data Snoc st b c = Snoc (st b) (c -> b) 
data Top a = Top

class StackTo a st c  where
     runStack :: st c -> (c -> a)
instance StackTo a Top a where
     runStack _ = id
instance (StackTo a st b) => StackTo a (Snoc st b) c where
     runStack (Snoc st' cb) = runStack st' . cb

This lets me do, e.g.

*Main Data.Label> let f = runStack $ Snoc (Snoc Top fst) head :: [(a,x)] -> a
*Main Data.Label> f [('a',undefined)] 
'a'

But this seems to require careful use of type annotations, otherwise...

*Main Data.Label> let f = runStack $ Snoc (Snoc Top fst) head

<interactive>:1:1:
    No instance for (StackTo a0 Top b0)
      arising from a use of `runStack'
    Possible fix: add an instance declaration for (StackTo a0 Top b0)
    In the expression: runStack
    In the expression: runStack $ Snoc (Snoc Top fst) head
    In an equation for `it': it = runStack $ Snoc (Snoc Top fst) head

I think these are the same issues addressed in this question, but I'm having trouble adapting that solution here. Can I use type families or some other method to come up with a more user-friendly solution to my recursive continuation stack?

Answer 1

The answer to the linked question hides the following quite useful trick: generalize the instance head, and specialize in the instance context.

instance a ~ b => StackTo a Top b where
    runStack _ = id

When choosing an instance to use, GHC inspects available instance heads only -- not contexts -- and picks the one (if any) that matches what is currently known about a type. It will not specialize a type before making this choice, even if specializing would allow one or more of the available instance heads to match. Thus, the difference between the instance given here and the one in the question above is that this one is more general: this one applies whenever the middle type is Top, whereas yours applies only when the middle type is Top and we know enough about the two other types to know they're equal.

Yours will overlap with fewer other potential instances, but this will encourage the inference engine more strongly.

Answer 2

Is there some particular reason why the Kleene star GADT won't do this job?

data Star r a b where
  Nil   :: Star r a a
  Cons  :: r a b -> Star r b c -> Star r a c

compose :: Star (->) a b -> a -> b
compose Nil          = id
compose (Cons f fs)  = compose fs . f

But if you need a type class approach, I wouldn't interfere.