Pre-SIP: Divergence Checking for Match Type Reduction

[bishabosha]

@lluc

type Tail [ X ] = X match
    case _ *: t = > t

type Apply [ C [ _ ] , T ] = T match
    case h *: _ = > C [ h ] *: Apply [C , Tail [ T ]]

@lluc

the check can’t use the fact that Tail shrinks a concrete tuple

in the case h *: _ => branch you call Tail[T], so isnt case _ *: t => t guaranteed to reduce as we already have the evidence that _ *: _ matches?

[etaconversion]

Hi,

There seems to be a misunderstanding: I was summoned on the question by @bjornregnell whether a SIP is necessary, or not. And that is what I tried to answer. The context of the OP should make it clear they decided to proceed with a SIP, which I merely pointed out. If they want to start the process instead of just merging the PR, then that’s how it’s going to be.

As to the concrete merits of this proposal, I leave it to you to have productive discussions in this thread with the student who put a lot of work into this and would like to contribute his first ever SIP.