[Haskell-cafe] Selda: confused about type signtures

[Marc Busqué]

Tom, thank you very much for your deep inspection. Your gist can be
really helpful in trying to understand the problem. I will study it
carefully. I have been reading books about Haskell and also Category
Theory for some months, but I have just started coding few weeks ago, so
I'm bit overwhelmed about having found a compiler bug so soon :D I'll
look into all of this and also about Li-yao recommendations and if it is
suitable I'll fill the issue and also report here.

Marc Busqué
http://waiting-for-dev.github.io/about/

On Mon, 23 Apr 2018, Tom Ellis wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.