The GADT debate

[wren romano]

On Sun, May 8, 2016 at 11:25 AM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> On May 7, 2016, at 11:05 PM, Gershom B <gershomb at gmail.com> wrote:
>>
>> an attempt (orthogonal to the prime committee at first) to specify an algorithm for inference that is easier to describe and implement than OutsideIn, and which is strictly less powerful. (And indeed whose specification can be given in a page or two of the report).
>
> Stephanie Weirich and I indeed considered doing such a thing, which conversation was inspired by my joining the Haskell Prime committee. We concluded that this would indeed be a research question that is, as yet, unanswered in the literature. The best we could come up with based on current knowledge would be to require type signatures on:
>
> 1. The scrutinee
> 2. Every case branch
> 3. The case as a whole
>
> With all of these type signatures in place, GADT type inference is indeed straightforward.

If all three of those signatures are present, doesn't that make
"inference" trivial? If I understand you correctly, the only thing to
do here would be to check the types, right?

I am curious though. Since we don't have true/anonymous type-level
functions, why do we need the signatures on every branch (assuming the
scrutinee and whole-expression types are given)? I can see why they'd
be required in Coq/Agda/etc, but it's less clear why they'd be
required in Haskell per se

-- 
Live well,
~wren