How to prove type equality inductively without classes?

Question

I am trying to prove associativity of type-level lists in such a way that will allow me to convert between equivalent types without carrying around any constraints.

Assuming the standard definition of concatenation:

type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

Suppose, I am given a function:

given :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy ((a ++ b) ++ c)
given = Proxy  -- Proxy is just an example

and I would like to call this function and then use associativity:

my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my = given @k @a @b @c  -- Couldn't match type ‘(a ++ b) ++ c’ with ‘a ++ (b ++ c)’

This type equality is not trivial indeed, so it is not a surprise that the compiler doesn’t understand it, however I can prove it! Unfortunately, I don’t know how to convince the compiler that I can.

My natural first thought is to do something like:

proof :: forall k (a :: [k]) (b :: [k]) (c :: [k]). (a ++ (b ++ c)) :~: ((a ++ b) ++ c)
proof = _

and then change my function to:

my :: forall k (a :: [k]) (b :: [k]) (c :: [k]). Proxy (a ++ (b ++ c))
my = case proof @k @a @b @c of Refl -> given @k @a @b @c

But I still have to define proof and for this I need to perform induction on its type arguments. The only way to do induction on types in Haskell that I know is to define a type class, but I then I will have to add the corresponding constraint to the type of my, which I don’t want to do – the fact that it calls given and coerces the result is an “implementation detail”.

Is there any way to prove this kind of type equality in Haskell without resorting to unsafe postulates?

Answer 1

No, you cannot prove this without a typeclass constraint, because it isn't true. In particular, here is a counterexample:

Any ++ ([] ++ []) -- reduces to Any ++ []
(Any ++ []) ++ [] -- does not reduce

To rule out the (stupid) existence of Any, you must use a typeclass that does not have an Any instance; no other choice.