GHC: failure to infer phantom type parameter

Question

So I'm trying to make a type for variable-length tuples, basically as a prettier version of Either a (Either (a,b) (Either (a,b,c) ...)) and Either (Either (Either ... (x,y,z)) (y,z)) z.

{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
module Temp where

-- type level addition
data Unit
data Succ n

class Summable n m where
  type Sum n m :: *

instance Summable Unit m where
  type Sum Unit m = Succ m

instance Summable n m => Summable (Succ n) m where
  type Sum (Succ n) m = Succ (Sum n m)

-- variable length tuple, left-to-right
data a :+ b = a :+ Maybe b
infixr 5 :+

class Prependable t r s where
  type Prepend t r s :: *
  prepend :: r -> Maybe s -> Prepend t r s

instance Prependable Unit x y where
  type Prepend Unit x y = x :+ y
  prepend = (:+)

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where
  type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y
  prepend (w :+ Nothing) _ = w :+ Nothing
  prepend (w :+ Just x) y = w :+ Just (prepend x y)

-- variable length tuple, right-to-left
data a :- b = Maybe a :- b
infixl 5 :-

class Appendable t r s where
  type Append t r s :: *
  append :: Maybe r -> s -> Append t r s

instance Appendable Unit x y where
  type Append Unit x y = x :- y
  append = (:-)

instance Appendable n x y => Appendable (Succ n) x (y :- z) where
  type Append (Succ n) x (y :- z) = Append n x y :- z
  append _ (Nothing :- z) = Nothing :- z
  append x (Just y :- z) = Just (append x y) :- z

However, the compiler seems unable to infer the phantom type parameter of prepend or append in the recursive cases:

Temp.hs:32:40:
    Could not deduce (Prepend t1 x y ~ Prepend n x y)
    from the context (Prependable n x y)
      bound by the instance declaration at Temp.hs:29:10-61
    NB: `Prepend' is a type function, and may not be injective
    In the return type of a call of `prepend'
    In the first argument of `Just', namely `(prepend x y)'
    In the second argument of `(:+)', namely `Just (prepend x y)'

Temp.hs:49:34:
    Could not deduce (Append t0 x y ~ Append n x y)
    from the context (Appendable n x y)
      bound by the instance declaration at Temp.hs:46:10-59
    NB: `Append' is a type function, and may not be injective
    In the return type of a call of `append'
    In the first argument of `Just', namely `(append x y)'
    In the first argument of `(:-)', namely `Just (append x y)'

Is there anything I can do to help the compiler make this inference?

Answer 1

The important part of the error message here is the:

NB: `Prepend' is a type function, and may not be injective

What does this mean? It means that there might be multiple instance Prependable such that their type Prepend ... = a, so that if you infer some Prepend to be a, you don't necessarily know which instance it belongs to.

You can solve this by using data types in type families, which have the advantage that you don't deal with type functions, which are surjective but might be injective, and instead with type "relations", which are bijective (So every Prepend type can only belong to one type family, and every type family has a distinct Prepend type).

(If you want me to show a solution with data types in type families, leave a comment! Basically, just use a data Prepend instead of type Prepend)

Answer 2

The solution I came up with was to add a dummy argument to tie prepend and append to the phantom parameter:

-- as above, except...

unsucc :: Succ n -> n
unsucc _ = undefined

class Prependable t r s where
  type Prepend t r s :: *
  prepend :: t -> r -> Maybe s -> Prepend t r s

instance Prependable Unit x y where
  type Prepend Unit x y = x :+ y
  prepend _ = (:+)

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where
  type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y
  prepend _ (w :+ Nothing) _ = w :+ Nothing
  prepend t (w :+ Just x) y = w :+ Just (prepend (unsucc t) x y)

class Appendable t r s where
  type Append t r s :: *
  append :: t -> Maybe r -> s -> Append t r s

instance Appendable Unit x y where
  type Append Unit x y = x :- y
  append _ = (:-)

instance Appendable n x y => Appendable (Succ n) x (y :- z) where
  type Append (Succ n) x (y :- z) = Append n x y :- z
  append _ _ (Nothing :- z) = Nothing :- z
  append t x (Just y :- z) = Just (append (unsucc t) x y) :- z