Por que precisamos especificar um tipo refinado (ou seu equivalente Aux) para a saída de determinados cálculos de tipo?
Nohttps://jto.github.io/articles/typelevel_quicksort :
Estamos expostos a umSum
tipo cujaapply
se parece com isso:
def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]): Aux[A, B, sum.Out] = sum
Agora, poderíamos usar o refinamento de tipo diretamente em vez de Aux, mas a pergunta permanece: por que isso (o tipo de retorno explícito) é necessário? Não seria "óbvio" que o tipo de retorno deapply
teria um tipo Sum # Out igual a sum.Out?
Se a removermos e apenas usarmosval x = Sum[_0, _1]
, parece bom, exceto adicionandoval y = Sum[x.Out, _1]
não funcionará, dizendo que o compilador não conseguiu encontrar a soma implícita.
Como o compilador parece "esquecer" o tipo exato de x.Out?