No Thinking With TypesExercício 11.2-i é escrever a função com a seguinte assinatura de tipo.
weaken :: OpenSum f ts -> OpenSum f (x ': ts)
data OpenSum (f :: k -> Type) (ts :: [k]) where
UnsafeOpenSum :: Int -> f t -> OpenSum f ts
Acredito que o parágrafo anterior ao exercício forneça contexto suficiente para saber o que essa função realiza, mas não está claro para mim.
Na prática, também é útil poder ampliar as possibilidades de um montante em aberto. Uma nova função, enfraquecer, alinha o tipo machado na frente da lista de possibilidades.
Se eu tivesse alguns exemplos de uso dessa função, seria uma grande ajuda para eu concluir este exercício.