Como provar a igualdade de tipos indutivamente sem classes?

Estou tentando provar a associatividade das listas em nível de tipo de maneira que me permita converter entre tipos equivalentes sem contornar restrições.

Assumindo a definição padrão de concatenação:

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

Suponha que eu receba uma função:

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

e eu gostaria de chamar essa função e usar associatividade:

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)’

Essa igualdade de tipos não é trivial, portanto, não é uma surpresa que o compilador não entenda, mas eu posso provar! Infelizmente, não sei como convencer o compilador que posso.

Meu primeiro pensamento natural é fazer algo como:

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

e depois mude minha função para:

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

Mas ainda tenho que definir proofe, para isso, preciso executar a indução em seus argumentos de tipo. A única maneira de fazer a indução de tipos no Haskell que eu sei é definir uma classe de tipo, mas então terei que adicionar a restrição correspondente ao tipo de myqual eu não quero fazer - o fato de chamar givene coagir o resultado é um "detalhe de implementação".

Existe alguma maneira de provar esse tipo de igualdade de tipo em Haskell sem recorrer a postulados inseguros?

Não, você não pode provar isso sem uma restrição de classe, porque não é verdade. Em particular, aqui está um contra-exemplo:

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

Para descartar a existência (estúpida) de Any, você deve usar uma classe de tipo que não possui uma Anyinstância; nenhuma outra escolha.