[Haskell-cafe] Selda: confused about type signtures

[Tom Ellis]

On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:
> On Mon, 23 Apr 2018, Tom Ellis wrote:
> >I had an error in what I said and also it was imprecise.  It's
> >`Res (Cols s a)` which is `a`, but only in the cases where you're actually
> >going to use it, and the compiler cannot take that into account when
> >solving the constraint.  Anyway, as Li-yao Xia points out in a sibling
> >message, the type variable `s` in not constrained and therefore it seems
> >impossible to solve.
> 
> I have pushed the repo to Github:
> 
> https://github.com/waiting-for-dev/hedger

Thanks for that Marc, it's very helpful.  I extracted the parts that are
relevant to the problem and created a version that doesn't depend on Selda:

    https://gist.github.com/tomjaguarpaw/f4db46671e2f39b790a25b8907dc53a3

I think I now understand what the situation is.  Interestingly your code
works on 8.0 but not 7.10.

Contrary to my earlier presumptions, the compiler *is* able to give a type
to `list` because `Cols` is a closed type family.  I suppose it can
determine that `Cols s a` does not actually depend on `s` so giving list the
type

    (Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a)

is fine.  The type of `s` will never be needed.  When `list` is applied to
`categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of
what `s` is.

Subtly changing the definition of Cols will break things.  For example, if
you add the clause

        Cols () a = Col Int a

then you won't be able to define `list` any more, even though `Res (Cols s
a)` is still just `a` because the `Columns (Cols s a)` instance might then
depend on what `s` is.

On the other hand, I do not yet understand why you cannot provide an
explicit signature for `list`.  I suspect this is some hairy compiler bug. 
Either it should be possible to give `list` its inferred type or it should
be forbidden.  It's probably worth filing an issue about this on GHC Trac.
I would be interested to hear Li-yao's thoughts on the matter.

Incidentally, this is why I try to avoid type families as much as possible. 
When they go wrong it's very hard to understand why, and indeed when they go
right it's also very hard to understand why.

Tom